src/HOL/Transfer.thy
changeset 47684 ead185e60b8c
parent 47660 7a5c681c0265
child 47789 71a526ee569a
     1.1 --- a/src/HOL/Transfer.thy	Sun Apr 22 22:02:52 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Sun Apr 22 21:32:35 2012 +0200
     1.3 @@ -238,6 +238,16 @@
     1.4  
     1.5  subsection {* Transfer rules *}
     1.6  
     1.7 +text {* Transfer rules using implication instead of equality on booleans. *}
     1.8 +
     1.9 +lemma eq_imp_transfer [transfer_rule]:
    1.10 +  "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
    1.11 +  unfolding right_unique_alt_def .
    1.12 +
    1.13 +lemma forall_imp_transfer [transfer_rule]:
    1.14 +  "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
    1.15 +  unfolding right_total_alt_def transfer_forall_def .
    1.16 +
    1.17  lemma eq_transfer [transfer_rule]:
    1.18    assumes "bi_unique A"
    1.19    shows "(A ===> A ===> op =) (op =) (op =)"
    1.20 @@ -297,14 +307,4 @@
    1.21    "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
    1.22    unfolding transfer_forall_def by (rule All_transfer)
    1.23  
    1.24 -text {* Transfer rules using implication instead of equality on booleans. *}
    1.25 -
    1.26 -lemma eq_imp_transfer [transfer_rule]:
    1.27 -  "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
    1.28 -  unfolding right_unique_alt_def .
    1.29 -
    1.30 -lemma forall_imp_transfer [transfer_rule]:
    1.31 -  "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
    1.32 -  unfolding right_total_alt_def transfer_forall_def .
    1.33 -
    1.34  end