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
```