author | haftmann |

Sat Mar 23 17:11:06 2013 +0100 (2013-03-23) | |

changeset 51488 | 3c886fe611b8 |

parent 51487 | f4bfdee99304 |

child 51489 | f738e6dbd844 |

tuned proof

1.1 --- a/src/HOL/UNITY/ProgressSets.thy Sat Mar 23 17:11:06 2013 +0100 1.2 +++ b/src/HOL/UNITY/ProgressSets.thy Sat Mar 23 17:11:06 2013 +0100 1.3 @@ -536,33 +536,34 @@ 1.4 and TL: "T \<in> L" 1.5 and Fstable: "F \<in> stable T" 1.6 shows "commutes F T B L" 1.7 -apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify) 1.8 proof - 1.9 - fix M and act and t 1.10 - assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" 1.11 - then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" 1.12 - by (force simp add: cl_eq_Collect_relcl [OF lattice]) 1.13 - then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" 1.14 - by blast 1.15 - then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u" 1.16 - apply (intro ballI impI) 1.17 - apply (subst cl_ident [symmetric], assumption) 1.18 - apply (simp add: relcl_def) 1.19 - apply (blast intro: cl_mono [THEN [2] rev_subsetD]) 1.20 - done 1.21 - with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" 1.22 - by (force intro!: funof_in 1.23 - simp add: wp_def stable_def constrains_def determ total) 1.24 - with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" 1.25 - by (intro dcommutes) assumption+ 1.26 - with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)" 1.27 - by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) 1.28 - with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))" 1.29 - by (blast intro: funof_imp_wp determ) 1.30 - with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" 1.31 - by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) 1.32 - then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" 1.33 - by simp 1.34 + { fix M and act and t 1.35 + assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" 1.36 + then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" 1.37 + by (force simp add: cl_eq_Collect_relcl [OF lattice]) 1.38 + then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" 1.39 + by blast 1.40 + then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u" 1.41 + apply (intro ballI impI) 1.42 + apply (subst cl_ident [symmetric], assumption) 1.43 + apply (simp add: relcl_def) 1.44 + apply (blast intro: cl_mono [THEN [2] rev_subsetD]) 1.45 + done 1.46 + with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" 1.47 + by (force intro!: funof_in 1.48 + simp add: wp_def stable_def constrains_def determ total) 1.49 + with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" 1.50 + by (intro dcommutes) assumption+ 1.51 + with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)" 1.52 + by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) 1.53 + with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))" 1.54 + by (blast intro: funof_imp_wp determ) 1.55 + with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" 1.56 + by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) 1.57 + then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" 1.58 + by simp 1.59 + } 1.60 + then show "commutes F T B L" unfolding commutes_def by clarify 1.61 qed 1.62 1.63 text{*Version packaged with @{thm progress_set_Union}*}