--- a/src/HOL/UNITY/ProgressSets.thy Sat Mar 23 17:11:06 2013 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Sat Mar 23 17:11:06 2013 +0100
@@ -536,33 +536,34 @@
and TL: "T \<in> L"
and Fstable: "F \<in> stable T"
shows "commutes F T B L"
-apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
proof -
- fix M and act and t
- assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
- then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
- by (force simp add: cl_eq_Collect_relcl [OF lattice])
- then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
- by blast
- then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
- apply (intro ballI impI)
- apply (subst cl_ident [symmetric], assumption)
- apply (simp add: relcl_def)
- apply (blast intro: cl_mono [THEN [2] rev_subsetD])
- done
- with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
- by (force intro!: funof_in
- simp add: wp_def stable_def constrains_def determ total)
- with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
- by (intro dcommutes) assumption+
- with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
- by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])
- with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
- by (blast intro: funof_imp_wp determ)
- with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
- by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
- then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
- by simp
+ { fix M and act and t
+ assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
+ then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
+ by (force simp add: cl_eq_Collect_relcl [OF lattice])
+ then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
+ by blast
+ then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
+ apply (intro ballI impI)
+ apply (subst cl_ident [symmetric], assumption)
+ apply (simp add: relcl_def)
+ apply (blast intro: cl_mono [THEN [2] rev_subsetD])
+ done
+ with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
+ by (force intro!: funof_in
+ simp add: wp_def stable_def constrains_def determ total)
+ with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
+ by (intro dcommutes) assumption+
+ with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
+ by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])
+ with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
+ by (blast intro: funof_imp_wp determ)
+ with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
+ by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
+ then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
+ by simp
+ }
+ then show "commutes F T B L" unfolding commutes_def by clarify
qed
text{*Version packaged with @{thm progress_set_Union}*}