tuned proof
authorhaftmann
Sat Mar 23 17:11:06 2013 +0100 (2013-03-23)
changeset 514883c886fe611b8
parent 51487 f4bfdee99304
child 51489 f738e6dbd844
tuned proof
src/HOL/UNITY/ProgressSets.thy
     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}*}