diff -r 10b0821a4d11 -r 3b2821e0d541 src/HOL/UNITY/Transformers.thy --- a/src/HOL/UNITY/Transformers.thy Fri Oct 13 18:28:51 2006 +0200 +++ b/src/HOL/UNITY/Transformers.thy Fri Oct 13 18:29:31 2006 +0200 @@ -88,7 +88,7 @@ done lemma wens_Id [simp]: "wens F Id B = B" -by (simp add: wens_def gfp_def wp_def awp_def, blast) +by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast) text{*These two theorems justify the claim that @{term wens} returns the weakest assertion satisfying the ensures property*} @@ -101,7 +101,7 @@ lemma wens_ensures: "act \ Acts F ==> F \ (wens F act B) ensures B" by (simp add: wens_def gfp_def constrains_def awp_def wp_def - ensures_def transient_def, blast) + ensures_def transient_def Join_set_eq, blast) text{*These two results constitute assertion (4.13) of the thesis*} lemma wens_mono: "(A \ B) ==> wens F act A \ wens F act B" @@ -110,7 +110,7 @@ done lemma wens_weakening: "B \ wens F act B" -by (simp add: wens_def gfp_def, blast) +by (simp add: wens_def gfp_def Join_set_eq, blast) text{*Assertion (6), or 4.16 in the thesis*} lemma subset_wens: "A-B \ wp act B \ awp F (B \ A) ==> A \ wens F act B" @@ -120,7 +120,7 @@ text{*Assertion 4.17 in the thesis*} lemma Diff_wens_constrains: "F \ (wens F act A - A) co wens F act A" -by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast) +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast) --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff} is declared as an iff-rule, then it's almost impossible to prove. One proof is via @{text meson} after expanding all definitions, but it's @@ -332,7 +332,7 @@ lemma wens_single_eq: "wens (mk_program (init, {act}, allowed)) act B = B \ wp act B" -by (simp add: wens_def gfp_def wp_def, blast) +by (simp add: wens_def gfp_def wp_def Join_set_eq, blast) text{*Next, we express the @{term "wens_set"} for single-assignment programs*}