src/HOL/Transfer.thy
changeset 47355 3d9d98e0f1a4
parent 47325 ec6187036495
child 47503 cb44d09d9d22
     1.1 --- a/src/HOL/Transfer.thy	Wed Apr 04 12:25:58 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Wed Apr 04 16:03:01 2012 +0200
     1.3 @@ -62,12 +62,19 @@
     1.4  definition transfer_implies where
     1.5    "transfer_implies \<equiv> op \<longrightarrow>"
     1.6  
     1.7 +definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
     1.8 +  where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
     1.9 +
    1.10  lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
    1.11    unfolding atomize_all transfer_forall_def ..
    1.12  
    1.13  lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
    1.14    unfolding atomize_imp transfer_implies_def ..
    1.15  
    1.16 +lemma transfer_bforall_unfold:
    1.17 +  "Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
    1.18 +  unfolding transfer_bforall_def atomize_imp atomize_all ..
    1.19 +
    1.20  lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q"
    1.21    unfolding Rel_def by simp
    1.22