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 =)