More "progress set" material
authorpaulson
Mon Mar 17 17:37:48 2003 +0100 (2003-03-17)
changeset 13866b42d7983a822
parent 13865 0a6bf71955b0
child 13867 1fdecd15437f
More "progress set" material
src/HOL/UNITY/Comp/Progress.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Transformers.thy
     1.1 --- a/src/HOL/UNITY/Comp/Progress.thy	Mon Mar 17 17:37:20 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Progress.thy	Mon Mar 17 17:37:48 2003 +0100
     1.3 @@ -88,11 +88,11 @@
     1.4  apply (rule leadsTo_UN [OF atLeast_leadsTo]) 
     1.5  done
     1.6  
     1.7 -text{*Result (4.39): Applying the Union Theorem*}
     1.8 +text{*Result (4.39): Applying the leadsTo-Join Theorem*}
     1.9  theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
    1.10  apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
    1.11   apply simp
    1.12 -apply (rule_tac T = "atLeast 0" in leadsTo_Union)
    1.13 +apply (rule_tac T = "atLeast 0" in leadsTo_Join)
    1.14    apply (simp add: awp_iff FF_def, constrains)
    1.15   apply (simp add: awp_iff GG_def wens_set_FF, constrains)
    1.16  apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
     2.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 17 17:37:20 2003 +0100
     2.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 17 17:37:48 2003 +0100
     2.3 @@ -18,6 +18,8 @@
     2.4  
     2.5  theory ProgressSets = Transformers:
     2.6  
     2.7 +subsection {*Complete Lattices and the Operator @{term cl}*}
     2.8 +
     2.9  constdefs
    2.10    lattice :: "'a set set => bool"
    2.11     --{*Meier calls them closure sets, but they are just complete lattices*}
    2.12 @@ -97,8 +99,7 @@
    2.13  
    2.14  lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
    2.15  apply (rule equalityI) 
    2.16 - prefer 2 
    2.17 -  apply (simp add: cl_def, blast)
    2.18 + prefer 2 apply (simp add: cl_def, blast)
    2.19  apply (rule cl_least)
    2.20   apply (blast intro: UN_in_lattice cl_in_lattice)
    2.21  apply (blast intro: subset_cl [THEN subsetD])  
    2.22 @@ -122,6 +123,8 @@
    2.23  by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
    2.24  
    2.25  
    2.26 +subsection {*Progress Sets and the Main Lemma*}
    2.27 +
    2.28  constdefs 
    2.29    closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
    2.30     "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
    2.31 @@ -136,93 +139,102 @@
    2.32      ==> T \<inter> (B \<union> wp act M) \<in> L"
    2.33  by (simp add: closed_def) 
    2.34  
    2.35 +text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
    2.36 +and @{term m} by @{term X}. *}
    2.37 +
    2.38 +text{*Part of the proof of the claim at the bottom of page 97.  It's
    2.39 +proved separately because the argument requires a generalization over
    2.40 +all @{term "act \<in> Acts F"}.*}
    2.41  lemma lattice_awp_lemma:
    2.42 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
    2.43 -      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
    2.44 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
    2.45 +      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
    2.46        and latt: "lattice C"
    2.47 -      and tc:   "T \<in> C"
    2.48 -      and qc:   "q \<in> C"
    2.49 -      and clos: "closed F T q C"
    2.50 -    shows "T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r))) \<in> C"
    2.51 +      and TC:   "T \<in> C"
    2.52 +      and BC:   "B \<in> C"
    2.53 +      and clos: "closed F T B C"
    2.54 +    shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
    2.55  apply (simp del: INT_simps add: awp_def INT_extend_simps) 
    2.56  apply (rule INT_in_lattice [OF latt]) 
    2.57  apply (erule closedD [OF clos]) 
    2.58 -apply (simp add: subset_trans [OF qsm Un_upper1]) 
    2.59 -apply (subgoal_tac "T \<inter> (m \<union> cl C (T\<inter>r)) = (T\<inter>m) \<union> cl C (T\<inter>r)")
    2.60 - prefer 2 apply (blast intro: tc rev_subsetD [OF _ cl_least]) 
    2.61 +apply (simp add: subset_trans [OF BsubX Un_upper1]) 
    2.62 +apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
    2.63 + prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least]) 
    2.64  apply (erule ssubst) 
    2.65 -apply (blast intro: Un_in_lattice latt cl_in_lattice tmc) 
    2.66 +apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
    2.67  done
    2.68  
    2.69 +text{*Remainder of the proof of the claim at the bottom of page 97.*}
    2.70  lemma lattice_lemma:
    2.71 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
    2.72 -      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
    2.73 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
    2.74 +      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
    2.75        and act:  "act \<in> Acts F"
    2.76        and latt: "lattice C"
    2.77 -      and tc:   "T \<in> C"
    2.78 -      and qc:   "q \<in> C"
    2.79 -      and clos: "closed F T q C"
    2.80 -    shows "T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m) \<in> C"
    2.81 -apply (subgoal_tac "T \<inter> (q \<union> wp act m) \<in> C")
    2.82 - prefer 2 apply (simp add: closedD [OF clos] act qsm tmc)
    2.83 +      and TC:   "T \<in> C"
    2.84 +      and BC:   "B \<in> C"
    2.85 +      and clos: "closed F T B C"
    2.86 +    shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
    2.87 +apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
    2.88 + prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
    2.89  apply (drule Int_in_lattice
    2.90 -              [OF _ lattice_awp_lemma [OF tmc qsm latt tc qc clos, of r]
    2.91 +              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
    2.92                      latt])
    2.93  apply (subgoal_tac
    2.94 -	 "T \<inter> (q \<union> wp act m) \<inter> (T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r)))) = 
    2.95 -	  T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)))") 
    2.96 +	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
    2.97 +	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
    2.98   prefer 2 apply blast 
    2.99  apply simp  
   2.100 -apply (drule Un_in_lattice [OF _ tmc latt]) 
   2.101 +apply (drule Un_in_lattice [OF _ TXC latt])  
   2.102  apply (subgoal_tac
   2.103 -	 "T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r))) \<union> T\<inter>m = 
   2.104 -	  T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m)")
   2.105 - prefer 2 apply (blast intro: qsm [THEN subsetD], simp) 
   2.106 +	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
   2.107 +	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
   2.108 + apply simp 
   2.109 +apply (blast intro: BsubX [THEN subsetD]) 
   2.110  done
   2.111  
   2.112  
   2.113 +text{*Induction step for the main lemma*}
   2.114  lemma progress_induction_step:
   2.115 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
   2.116 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
   2.117        and act:  "act \<in> Acts F"
   2.118 -      and mwens: "m \<in> wens_set F q"
   2.119 +      and Xwens: "X \<in> wens_set F B"
   2.120        and latt: "lattice C"
   2.121 -      and  tc:  "T \<in> C"
   2.122 -      and  qc:  "q \<in> C"
   2.123 -      and clos: "closed F T q C"
   2.124 +      and  TC:  "T \<in> C"
   2.125 +      and  BC:  "B \<in> C"
   2.126 +      and clos: "closed F T B C"
   2.127        and Fstable: "F \<in> stable T"
   2.128 -  shows "T \<inter> wens F act m \<in> C"
   2.129 +  shows "T \<inter> wens F act X \<in> C"
   2.130  proof -
   2.131 -from mwens have qsm: "q \<subseteq> m"
   2.132 - by (rule wens_set_imp_subset) 
   2.133 -let ?r = "wens F act m"
   2.134 -have "?r \<subseteq> (wp act m \<inter> awp F (m\<union>?r)) \<union> m"
   2.135 - by (simp add: wens_unfold [symmetric])
   2.136 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m\<union>?r)) \<union> m)"
   2.137 - by blast
   2.138 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (T \<inter> (m\<union>?r))) \<union> m)"
   2.139 - by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   2.140 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   2.141 - by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   2.142 -then have "cl C (T\<inter>?r) \<subseteq> 
   2.143 -           cl C (T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m))"
   2.144 - by (rule cl_mono) 
   2.145 -then have "cl C (T\<inter>?r) \<subseteq> 
   2.146 -           T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   2.147 - by (simp add: cl_ident lattice_lemma [OF tmc qsm act latt tc qc clos])
   2.148 -then have "cl C (T\<inter>?r) \<subseteq> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m"
   2.149 - by blast
   2.150 -then have "cl C (T\<inter>?r) \<subseteq> ?r"
   2.151 - by (blast intro!: subset_wens) 
   2.152 -then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   2.153 - by (simp add: Int_subset_iff cl_ident tc
   2.154 -               subset_trans [OF cl_mono [OF Int_lower1]]) 
   2.155 -show ?thesis
   2.156 - by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   2.157 +  from Xwens have BsubX: "B \<subseteq> X"
   2.158 +    by (rule wens_set_imp_subset) 
   2.159 +  let ?r = "wens F act X"
   2.160 +  have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
   2.161 +    by (simp add: wens_unfold [symmetric])
   2.162 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
   2.163 +    by blast
   2.164 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
   2.165 +    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   2.166 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   2.167 +    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   2.168 +  then have "cl C (T\<inter>?r) \<subseteq> 
   2.169 +             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
   2.170 +    by (rule cl_mono) 
   2.171 +  then have "cl C (T\<inter>?r) \<subseteq> 
   2.172 +             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   2.173 +    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
   2.174 +  then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
   2.175 +    by blast
   2.176 +  then have "cl C (T\<inter>?r) \<subseteq> ?r"
   2.177 +    by (blast intro!: subset_wens) 
   2.178 +  then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   2.179 +    by (simp add: Int_subset_iff cl_ident TC
   2.180 +                  subset_trans [OF cl_mono [OF Int_lower1]]) 
   2.181 +  show ?thesis
   2.182 +    by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   2.183  qed
   2.184  
   2.185 -
   2.186 +text{*The Lemma proved on page 96*}
   2.187  lemma progress_set_lemma:
   2.188 -      "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   2.189 +     "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   2.190  apply (simp add: progress_set_def, clarify) 
   2.191  apply (erule wens_set.induct) 
   2.192    txt{*Base*}
   2.193 @@ -235,4 +247,49 @@
   2.194  apply (blast intro: UN_in_lattice) 
   2.195  done
   2.196  
   2.197 +
   2.198 +subsection {*The Progress Set Union Theorem*}
   2.199 +
   2.200 +lemma closed_mono:
   2.201 +  assumes BB':  "B \<subseteq> B'"
   2.202 +      and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
   2.203 +      and B'C:  "B' \<in> C"
   2.204 +      and TC:   "T \<in> C"
   2.205 +      and latt: "lattice C"
   2.206 +  shows "T \<inter> (B' \<union> wp act M) \<in> C"
   2.207 +proof -
   2.208 +  from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
   2.209 +    by (simp add: Int_Un_distrib)
   2.210 +  then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
   2.211 +    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
   2.212 +  show ?thesis
   2.213 +    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
   2.214 +        blast intro: BB' [THEN subsetD]) 
   2.215 +qed
   2.216 +
   2.217 +
   2.218 +lemma progress_set_mono:
   2.219 +    assumes BB':  "B \<subseteq> B'"
   2.220 +    shows
   2.221 +     "[| B' \<in> C;  C \<in> progress_set F T B|] 
   2.222 +      ==> C \<in> progress_set F T B'"
   2.223 +by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
   2.224 +                 subset_trans [OF BB']) 
   2.225 +
   2.226 +theorem progress_set_Union:
   2.227 +  assumes prog: "C \<in> progress_set F T B"
   2.228 +      and BB':  "B \<subseteq> B'"
   2.229 +      and B'C:  "B' \<in> C"
   2.230 +      and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
   2.231 +      and leadsTo: "F \<in> A leadsTo B'"
   2.232 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
   2.233 +apply (insert prog) 
   2.234 +apply (rule leadsTo_Join [OF leadsTo]) 
   2.235 +  apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
   2.236 +apply (simp add: awp_iff_constrains)
   2.237 +apply (drule progress_set_mono [OF BB' B'C]) 
   2.238 +apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
   2.239 +                    BB' [THEN subsetD]) 
   2.240 +done
   2.241 +
   2.242  end
     3.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Mar 17 17:37:20 2003 +0100
     3.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Mar 17 17:37:48 2003 +0100
     3.3 @@ -3,11 +3,15 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   2003  University of Cambridge
     3.6  
     3.7 -Predicate Transformers from 
     3.8 +Predicate Transformers.  From 
     3.9  
    3.10      David Meier and Beverly Sanders,
    3.11      Composing Leads-to Properties
    3.12      Theoretical Computer Science 243:1-2 (2000), 339-361.
    3.13 +
    3.14 +    David Meier,
    3.15 +    Progress Properties in Program Refinement and Parallel Composition
    3.16 +    Swiss Federal Institute of Technology Zurich (1997)
    3.17  *)
    3.18  
    3.19  header{*Predicate Transformers*}
    3.20 @@ -274,10 +278,10 @@
    3.21  apply (blast intro: wens_set.Union) 
    3.22  done
    3.23  
    3.24 -theorem leadsTo_Union:
    3.25 -  assumes awpF: "T-B \<subseteq> awp F T"
    3.26 +theorem leadsTo_Join:
    3.27 +  assumes leadsTo: "F \<in> A leadsTo B"
    3.28 +      and awpF: "T-B \<subseteq> awp F T"
    3.29        and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
    3.30 -      and leadsTo: "F \<in> A leadsTo B"
    3.31    shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
    3.32  apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
    3.33  apply (rule wens_Union [THEN bexE]) 
    3.34 @@ -472,10 +476,10 @@
    3.35  
    3.36  text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
    3.37  
    3.38 -lemma fp_leadsTo_Union:
    3.39 +lemma fp_leadsTo_Join:
    3.40      "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
    3.41 -apply (rule leadsTo_Union, assumption)
    3.42 - apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast, assumption)
    3.43 +apply (rule leadsTo_Join, assumption, blast)
    3.44 +apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 
    3.45  done
    3.46  
    3.47  end