src/HOL/Transfer.thy
changeset 47924 4e951258204b
parent 47789 71a526ee569a
child 47937 70375fa2679d
     1.1 --- a/src/HOL/Transfer.thy	Mon May 14 17:28:07 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Tue May 15 11:50:34 2012 +0200
     1.3 @@ -279,6 +279,14 @@
     1.4    "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
     1.5    unfolding fun_rel_def by (simp split: nat.split)
     1.6  
     1.7 +lemma nat_rec_transfer [transfer_rule]:
     1.8 +  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
     1.9 +  unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
    1.10 +
    1.11 +lemma funpow_transfer [transfer_rule]:
    1.12 +  "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
    1.13 +  unfolding funpow_def by transfer_prover
    1.14 +
    1.15  text {* Fallback rule for transferring universal quantifiers over
    1.16    correspondence relations that are not bi-total, and do not have
    1.17    custom transfer rules (e.g. relations between function types). *}