src/HOL/Transfer.thy
changeset 47636 b786388b4b3a
parent 47635 ebb79474262c
child 47637 7a34395441ff
     1.1 --- a/src/HOL/Transfer.thy	Fri Apr 20 22:49:40 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Fri Apr 20 22:54:13 2012 +0200
     1.3 @@ -219,35 +219,35 @@
     1.4  
     1.5  subsection {* Transfer rules *}
     1.6  
     1.7 -lemma eq_parametric [transfer_rule]:
     1.8 +lemma eq_transfer [transfer_rule]:
     1.9    assumes "bi_unique A"
    1.10    shows "(A ===> A ===> op =) (op =) (op =)"
    1.11    using assms unfolding bi_unique_def fun_rel_def by auto
    1.12  
    1.13 -lemma All_parametric [transfer_rule]:
    1.14 +lemma All_transfer [transfer_rule]:
    1.15    assumes "bi_total A"
    1.16    shows "((A ===> op =) ===> op =) All All"
    1.17    using assms unfolding bi_total_def fun_rel_def by fast
    1.18  
    1.19 -lemma Ex_parametric [transfer_rule]:
    1.20 +lemma Ex_transfer [transfer_rule]:
    1.21    assumes "bi_total A"
    1.22    shows "((A ===> op =) ===> op =) Ex Ex"
    1.23    using assms unfolding bi_total_def fun_rel_def by fast
    1.24  
    1.25 -lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
    1.26 +lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
    1.27    unfolding fun_rel_def by simp
    1.28  
    1.29 -lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
    1.30 +lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
    1.31    unfolding fun_rel_def by simp
    1.32  
    1.33 -lemma id_parametric [transfer_rule]: "(A ===> A) id id"
    1.34 +lemma id_transfer [transfer_rule]: "(A ===> A) id id"
    1.35    unfolding fun_rel_def by simp
    1.36  
    1.37 -lemma comp_parametric [transfer_rule]:
    1.38 +lemma comp_transfer [transfer_rule]:
    1.39    "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
    1.40    unfolding fun_rel_def by simp
    1.41  
    1.42 -lemma fun_upd_parametric [transfer_rule]:
    1.43 +lemma fun_upd_transfer [transfer_rule]:
    1.44    assumes [transfer_rule]: "bi_unique A"
    1.45    shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
    1.46    unfolding fun_upd_def [abs_def] by transfer_prover
    1.47 @@ -270,8 +270,8 @@
    1.48  text {* Preferred rule for transferring universal quantifiers over
    1.49    bi-total correspondence relations (later rules are tried first). *}
    1.50  
    1.51 -lemma transfer_forall_parametric [transfer_rule]:
    1.52 +lemma forall_transfer [transfer_rule]:
    1.53    "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
    1.54 -  unfolding transfer_forall_def by (rule All_parametric)
    1.55 +  unfolding transfer_forall_def by (rule All_transfer)
    1.56  
    1.57  end