partially isarified proof
authorhaftmann
Fri Sep 18 09:07:51 2009 +0200 (2009-09-18)
changeset 326048b3e2bc91a46
parent 32603 e08fdd615333
child 32605 43ed78ee285d
partially isarified proof
src/HOL/UNITY/ProgressSets.thy
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Fri Sep 18 09:07:50 2009 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Fri Sep 18 09:07:51 2009 +0200
     1.3 @@ -534,7 +534,7 @@
     1.4  subsubsection{*Commutativity of Functions and Relation*}
     1.5  text{*Thesis, page 109*}
     1.6  
     1.7 -(*FIXME: this proof is an ungodly mess*)
     1.8 +(*FIXME: this proof is still an ungodly mess*)
     1.9  text{*From Meier's thesis, section 4.5.6*}
    1.10  lemma commutativity2_lemma:
    1.11    assumes dcommutes: 
    1.12 @@ -548,36 +548,35 @@
    1.13        and TL: "T \<in> L"
    1.14        and Fstable: "F \<in> stable T"
    1.15    shows  "commutes F T B L"
    1.16 -apply (simp add: commutes_def del: Int_subset_iff, clarify)  
    1.17 -apply (rename_tac t)
    1.18 -apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
    1.19 - prefer 2 
    1.20 - apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify) 
    1.21 -apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") 
    1.22 - prefer 2 
    1.23 - apply (intro ballI impI) 
    1.24 - apply (subst cl_ident [symmetric], assumption)
    1.25 - apply (simp add: relcl_def)  
    1.26 - apply (blast intro: cl_mono [THEN [2] rev_subsetD])  
    1.27 -apply (subgoal_tac "funof act s \<in> T\<inter>M") 
    1.28 - prefer 2 
    1.29 - apply (cut_tac Fstable) 
    1.30 - apply (force intro!: funof_in 
    1.31 -              simp add: wp_def stable_def constrains_def determ total) 
    1.32 -apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L")
    1.33 - prefer 2
    1.34 - apply (rule dcommutes [rule_format], assumption+) 
    1.35 -apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)")
    1.36 - prefer 2 
    1.37 - apply (simp add: relcl_def)
    1.38 - apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
    1.39 -apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))")
    1.40 - prefer 2
    1.41 - apply (blast intro: funof_imp_wp determ) 
    1.42 -apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])  
    1.43 -done
    1.44 -
    1.45 -
    1.46 +apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify)
    1.47 +proof -
    1.48 +  fix M and act and t
    1.49 +  assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)"
    1.50 +  then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M"
    1.51 +    by (force simp add: cl_eq_Collect_relcl [OF lattice])
    1.52 +  then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M"
    1.53 +    by blast
    1.54 +  then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u"
    1.55 +    apply (intro ballI impI) 
    1.56 +    apply (subst cl_ident [symmetric], assumption)
    1.57 +    apply (simp add: relcl_def)  
    1.58 +    apply (blast intro: cl_mono [THEN [2] rev_subsetD])
    1.59 +    done
    1.60 +  with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M"
    1.61 +    by (force intro!: funof_in 
    1.62 +      simp add: wp_def stable_def constrains_def determ total)
    1.63 +  with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
    1.64 +    by (intro dcommutes [rule_format]) assumption+ 
    1.65 +  with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)"
    1.66 +    by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
    1.67 +  with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))"
    1.68 +    by (blast intro: funof_imp_wp determ) 
    1.69 +  with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))"
    1.70 +    by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
    1.71 +  then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))"
    1.72 +    by simp
    1.73 +qed
    1.74 +  
    1.75  text{*Version packaged with @{thm progress_set_Union}*}
    1.76  lemma commutativity2:
    1.77    assumes leadsTo: "F \<in> A leadsTo B"