src/HOL/UNITY/Transformers.thy
changeset 13874 0da2141606c6
parent 13866 b42d7983a822
child 15102 04b0e943fcc9
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Mar 21 18:15:56 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Mar 21 18:16:18 2003 +0100
     1.3 @@ -38,6 +38,10 @@
     1.4  theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
     1.5  by (force simp add: wp_def) 
     1.6  
     1.7 +text{*This lemma is a good deal more intuitive than the definition!*}
     1.8 +lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
     1.9 +by (simp add: wp_def, blast)
    1.10 +
    1.11  lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    1.12  by (force simp add: wp_def) 
    1.13  
    1.14 @@ -70,6 +74,9 @@
    1.15  apply (simp add: awp_iff_stable) 
    1.16  done
    1.17  
    1.18 +lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B"
    1.19 +by (simp add: wp_def, blast)
    1.20 +
    1.21  lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    1.22  by (simp add: awp_def wp_def, blast)
    1.23