src/HOL/UNITY/Transformers.thy
changeset 21026 3b2821e0d541
parent 16417 9bc16273c2d4
child 21312 1d39091a3208
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:28:51 2006 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:29:31 2006 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  done
     1.5  
     1.6  lemma wens_Id [simp]: "wens F Id B = B"
     1.7 -by (simp add: wens_def gfp_def wp_def awp_def, blast)
     1.8 +by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
     1.9  
    1.10  text{*These two theorems justify the claim that @{term wens} returns the
    1.11  weakest assertion satisfying the ensures property*}
    1.12 @@ -101,7 +101,7 @@
    1.13  
    1.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    1.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    1.16 -              ensures_def transient_def, blast) 
    1.17 +              ensures_def transient_def Join_set_eq, blast)
    1.18  
    1.19  text{*These two results constitute assertion (4.13) of the thesis*}
    1.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    1.21 @@ -110,7 +110,7 @@
    1.22  done
    1.23  
    1.24  lemma wens_weakening: "B \<subseteq> wens F act B"
    1.25 -by (simp add: wens_def gfp_def, blast)
    1.26 +by (simp add: wens_def gfp_def Join_set_eq, blast)
    1.27  
    1.28  text{*Assertion (6), or 4.16 in the thesis*}
    1.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    1.30 @@ -120,7 +120,7 @@
    1.31  
    1.32  text{*Assertion 4.17 in the thesis*}
    1.33  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
    1.34 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    1.35 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
    1.36    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
    1.37        is declared as an iff-rule, then it's almost impossible to prove. 
    1.38        One proof is via @{text meson} after expanding all definitions, but it's
    1.39 @@ -332,7 +332,7 @@
    1.40  
    1.41  lemma wens_single_eq:
    1.42       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
    1.43 -by (simp add: wens_def gfp_def wp_def, blast)
    1.44 +by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
    1.45  
    1.46  
    1.47  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}