--- a/src/HOL/Transfer.thy Wed Feb 26 15:33:52 2014 +0100
+++ b/src/HOL/Transfer.thy Wed Feb 26 16:48:15 2014 +0100
@@ -122,9 +122,17 @@
text {* Handling of domains *}
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
lemma Domaimp_refl[transfer_domain_rule]:
"Domainp T = Domainp T" ..
+lemma Domainp_prod_fun_eq[transfer_domain_rule]:
+ assumes "Domainp T = P"
+ shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
+by (auto intro: choice simp: assms[symmetric] Domainp_iff fun_rel_def fun_eq_iff)
+
subsection {* Predicates on relations, i.e. ``class constraints'' *}
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
@@ -275,9 +283,6 @@
subsection {* Transfer rules *}
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
-
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =)