# HG changeset patch
# User haftmann
# Date 1364055066 -3600
# Node ID 3c886fe611b85637c4fc092144ed63627336747c
# Parent  f4bfdee993045e99b1061f83b9b9eed7bb0f63dc
tuned proof

diff -r f4bfdee99304 -r 3c886fe611b8 src/HOL/UNITY/ProgressSets.thy
--- 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}*}