--- a/src/HOL/UNITY/Transformers.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/UNITY/Transformers.thy Sun Nov 12 19:22:10 2006 +0100
@@ -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 Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_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 \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Join_set_eq, blast)
+ ensures_def transient_def Sup_set_eq, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def Sup_set_eq, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -119,8 +119,8 @@
done
text{*Assertion 4.17 in the thesis*}
-lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
+lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_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 \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}