src/HOL/Transfer.thy
 changeset 55760 aaaccc8e015f parent 55415 05f5fdb8d093 child 55811 aa1acc25126b
```     1.1 --- a/src/HOL/Transfer.thy	Wed Feb 26 15:33:52 2014 +0100
1.2 +++ b/src/HOL/Transfer.thy	Wed Feb 26 16:48:15 2014 +0100
1.3 @@ -122,9 +122,17 @@
1.4
1.5  text {* Handling of domains *}
1.6
1.7 +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
1.8 +  by auto
1.9 +
1.10  lemma Domaimp_refl[transfer_domain_rule]:
1.11    "Domainp T = Domainp T" ..
1.12
1.13 +lemma Domainp_prod_fun_eq[transfer_domain_rule]:
1.14 +  assumes "Domainp T = P"
1.15 +  shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
1.16 +by (auto intro: choice simp: assms[symmetric] Domainp_iff fun_rel_def fun_eq_iff)
1.17 +
1.18  subsection {* Predicates on relations, i.e. ``class constraints'' *}
1.19
1.20  definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
1.21 @@ -275,9 +283,6 @@
1.22
1.23  subsection {* Transfer rules *}
1.24
1.25 -lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
1.26 -  by auto
1.27 -
1.28  lemma Domainp_forall_transfer [transfer_rule]:
1.29    assumes "right_total A"
1.30    shows "((A ===> op =) ===> op =)
```