# HG changeset patch
# User kuncar
# Date 1393429695 -3600
# Node ID aaaccc8e015fd3844e5f1b68dae000f30d0b7f6d
# Parent  fe3d8f585c20e060ca793be7c50a6b6eb21df134
transfer domain rule for special case of functions - was missing

diff -r fe3d8f585c20 -r aaaccc8e015f src/HOL/Transfer.thy
--- 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 =)