src/HOL/UNITY/ProgressSets.thy
changeset 13866 b42d7983a822
parent 13861 0c18f31d901a
child 13870 cf947d1ec5ff
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 17 17:37:20 2003 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 17 17:37:48 2003 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  theory ProgressSets = Transformers:
     1.6  
     1.7 +subsection {*Complete Lattices and the Operator @{term cl}*}
     1.8 +
     1.9  constdefs
    1.10    lattice :: "'a set set => bool"
    1.11     --{*Meier calls them closure sets, but they are just complete lattices*}
    1.12 @@ -97,8 +99,7 @@
    1.13  
    1.14  lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
    1.15  apply (rule equalityI) 
    1.16 - prefer 2 
    1.17 -  apply (simp add: cl_def, blast)
    1.18 + prefer 2 apply (simp add: cl_def, blast)
    1.19  apply (rule cl_least)
    1.20   apply (blast intro: UN_in_lattice cl_in_lattice)
    1.21  apply (blast intro: subset_cl [THEN subsetD])  
    1.22 @@ -122,6 +123,8 @@
    1.23  by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
    1.24  
    1.25  
    1.26 +subsection {*Progress Sets and the Main Lemma*}
    1.27 +
    1.28  constdefs 
    1.29    closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
    1.30     "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
    1.31 @@ -136,93 +139,102 @@
    1.32      ==> T \<inter> (B \<union> wp act M) \<in> L"
    1.33  by (simp add: closed_def) 
    1.34  
    1.35 +text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
    1.36 +and @{term m} by @{term X}. *}
    1.37 +
    1.38 +text{*Part of the proof of the claim at the bottom of page 97.  It's
    1.39 +proved separately because the argument requires a generalization over
    1.40 +all @{term "act \<in> Acts F"}.*}
    1.41  lemma lattice_awp_lemma:
    1.42 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
    1.43 -      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
    1.44 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
    1.45 +      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
    1.46        and latt: "lattice C"
    1.47 -      and tc:   "T \<in> C"
    1.48 -      and qc:   "q \<in> C"
    1.49 -      and clos: "closed F T q C"
    1.50 -    shows "T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r))) \<in> C"
    1.51 +      and TC:   "T \<in> C"
    1.52 +      and BC:   "B \<in> C"
    1.53 +      and clos: "closed F T B C"
    1.54 +    shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
    1.55  apply (simp del: INT_simps add: awp_def INT_extend_simps) 
    1.56  apply (rule INT_in_lattice [OF latt]) 
    1.57  apply (erule closedD [OF clos]) 
    1.58 -apply (simp add: subset_trans [OF qsm Un_upper1]) 
    1.59 -apply (subgoal_tac "T \<inter> (m \<union> cl C (T\<inter>r)) = (T\<inter>m) \<union> cl C (T\<inter>r)")
    1.60 - prefer 2 apply (blast intro: tc rev_subsetD [OF _ cl_least]) 
    1.61 +apply (simp add: subset_trans [OF BsubX Un_upper1]) 
    1.62 +apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
    1.63 + prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least]) 
    1.64  apply (erule ssubst) 
    1.65 -apply (blast intro: Un_in_lattice latt cl_in_lattice tmc) 
    1.66 +apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
    1.67  done
    1.68  
    1.69 +text{*Remainder of the proof of the claim at the bottom of page 97.*}
    1.70  lemma lattice_lemma:
    1.71 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
    1.72 -      and qsm:  "q \<subseteq> m"   --{*holds in inductive step*}
    1.73 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
    1.74 +      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
    1.75        and act:  "act \<in> Acts F"
    1.76        and latt: "lattice C"
    1.77 -      and tc:   "T \<in> C"
    1.78 -      and qc:   "q \<in> C"
    1.79 -      and clos: "closed F T q C"
    1.80 -    shows "T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m) \<in> C"
    1.81 -apply (subgoal_tac "T \<inter> (q \<union> wp act m) \<in> C")
    1.82 - prefer 2 apply (simp add: closedD [OF clos] act qsm tmc)
    1.83 +      and TC:   "T \<in> C"
    1.84 +      and BC:   "B \<in> C"
    1.85 +      and clos: "closed F T B C"
    1.86 +    shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
    1.87 +apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
    1.88 + prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
    1.89  apply (drule Int_in_lattice
    1.90 -              [OF _ lattice_awp_lemma [OF tmc qsm latt tc qc clos, of r]
    1.91 +              [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
    1.92                      latt])
    1.93  apply (subgoal_tac
    1.94 -	 "T \<inter> (q \<union> wp act m) \<inter> (T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r)))) = 
    1.95 -	  T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)))") 
    1.96 +	 "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
    1.97 +	  T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
    1.98   prefer 2 apply blast 
    1.99  apply simp  
   1.100 -apply (drule Un_in_lattice [OF _ tmc latt]) 
   1.101 +apply (drule Un_in_lattice [OF _ TXC latt])  
   1.102  apply (subgoal_tac
   1.103 -	 "T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r))) \<union> T\<inter>m = 
   1.104 -	  T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m)")
   1.105 - prefer 2 apply (blast intro: qsm [THEN subsetD], simp) 
   1.106 +	 "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
   1.107 +	  T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
   1.108 + apply simp 
   1.109 +apply (blast intro: BsubX [THEN subsetD]) 
   1.110  done
   1.111  
   1.112  
   1.113 +text{*Induction step for the main lemma*}
   1.114  lemma progress_induction_step:
   1.115 -  assumes tmc:  "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
   1.116 +  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
   1.117        and act:  "act \<in> Acts F"
   1.118 -      and mwens: "m \<in> wens_set F q"
   1.119 +      and Xwens: "X \<in> wens_set F B"
   1.120        and latt: "lattice C"
   1.121 -      and  tc:  "T \<in> C"
   1.122 -      and  qc:  "q \<in> C"
   1.123 -      and clos: "closed F T q C"
   1.124 +      and  TC:  "T \<in> C"
   1.125 +      and  BC:  "B \<in> C"
   1.126 +      and clos: "closed F T B C"
   1.127        and Fstable: "F \<in> stable T"
   1.128 -  shows "T \<inter> wens F act m \<in> C"
   1.129 +  shows "T \<inter> wens F act X \<in> C"
   1.130  proof -
   1.131 -from mwens have qsm: "q \<subseteq> m"
   1.132 - by (rule wens_set_imp_subset) 
   1.133 -let ?r = "wens F act m"
   1.134 -have "?r \<subseteq> (wp act m \<inter> awp F (m\<union>?r)) \<union> m"
   1.135 - by (simp add: wens_unfold [symmetric])
   1.136 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m\<union>?r)) \<union> m)"
   1.137 - by blast
   1.138 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (T \<inter> (m\<union>?r))) \<union> m)"
   1.139 - by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   1.140 -then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   1.141 - by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   1.142 -then have "cl C (T\<inter>?r) \<subseteq> 
   1.143 -           cl C (T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m))"
   1.144 - by (rule cl_mono) 
   1.145 -then have "cl C (T\<inter>?r) \<subseteq> 
   1.146 -           T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
   1.147 - by (simp add: cl_ident lattice_lemma [OF tmc qsm act latt tc qc clos])
   1.148 -then have "cl C (T\<inter>?r) \<subseteq> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m"
   1.149 - by blast
   1.150 -then have "cl C (T\<inter>?r) \<subseteq> ?r"
   1.151 - by (blast intro!: subset_wens) 
   1.152 -then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   1.153 - by (simp add: Int_subset_iff cl_ident tc
   1.154 -               subset_trans [OF cl_mono [OF Int_lower1]]) 
   1.155 -show ?thesis
   1.156 - by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   1.157 +  from Xwens have BsubX: "B \<subseteq> X"
   1.158 +    by (rule wens_set_imp_subset) 
   1.159 +  let ?r = "wens F act X"
   1.160 +  have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
   1.161 +    by (simp add: wens_unfold [symmetric])
   1.162 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
   1.163 +    by blast
   1.164 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
   1.165 +    by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 
   1.166 +  then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   1.167 +    by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
   1.168 +  then have "cl C (T\<inter>?r) \<subseteq> 
   1.169 +             cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
   1.170 +    by (rule cl_mono) 
   1.171 +  then have "cl C (T\<inter>?r) \<subseteq> 
   1.172 +             T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
   1.173 +    by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
   1.174 +  then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
   1.175 +    by blast
   1.176 +  then have "cl C (T\<inter>?r) \<subseteq> ?r"
   1.177 +    by (blast intro!: subset_wens) 
   1.178 +  then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
   1.179 +    by (simp add: Int_subset_iff cl_ident TC
   1.180 +                  subset_trans [OF cl_mono [OF Int_lower1]]) 
   1.181 +  show ?thesis
   1.182 +    by (rule cl_subset_in_lattice [OF cl_subset latt]) 
   1.183  qed
   1.184  
   1.185 -
   1.186 +text{*The Lemma proved on page 96*}
   1.187  lemma progress_set_lemma:
   1.188 -      "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   1.189 +     "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
   1.190  apply (simp add: progress_set_def, clarify) 
   1.191  apply (erule wens_set.induct) 
   1.192    txt{*Base*}
   1.193 @@ -235,4 +247,49 @@
   1.194  apply (blast intro: UN_in_lattice) 
   1.195  done
   1.196  
   1.197 +
   1.198 +subsection {*The Progress Set Union Theorem*}
   1.199 +
   1.200 +lemma closed_mono:
   1.201 +  assumes BB':  "B \<subseteq> B'"
   1.202 +      and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
   1.203 +      and B'C:  "B' \<in> C"
   1.204 +      and TC:   "T \<in> C"
   1.205 +      and latt: "lattice C"
   1.206 +  shows "T \<inter> (B' \<union> wp act M) \<in> C"
   1.207 +proof -
   1.208 +  from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
   1.209 +    by (simp add: Int_Un_distrib)
   1.210 +  then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
   1.211 +    by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 
   1.212 +  show ?thesis
   1.213 +    by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 
   1.214 +        blast intro: BB' [THEN subsetD]) 
   1.215 +qed
   1.216 +
   1.217 +
   1.218 +lemma progress_set_mono:
   1.219 +    assumes BB':  "B \<subseteq> B'"
   1.220 +    shows
   1.221 +     "[| B' \<in> C;  C \<in> progress_set F T B|] 
   1.222 +      ==> C \<in> progress_set F T B'"
   1.223 +by (simp add: progress_set_def closed_def closed_mono [OF BB'] 
   1.224 +                 subset_trans [OF BB']) 
   1.225 +
   1.226 +theorem progress_set_Union:
   1.227 +  assumes prog: "C \<in> progress_set F T B"
   1.228 +      and BB':  "B \<subseteq> B'"
   1.229 +      and B'C:  "B' \<in> C"
   1.230 +      and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
   1.231 +      and leadsTo: "F \<in> A leadsTo B'"
   1.232 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
   1.233 +apply (insert prog) 
   1.234 +apply (rule leadsTo_Join [OF leadsTo]) 
   1.235 +  apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 
   1.236 +apply (simp add: awp_iff_constrains)
   1.237 +apply (drule progress_set_mono [OF BB' B'C]) 
   1.238 +apply (blast intro: progress_set_lemma Gco constrains_weaken_L 
   1.239 +                    BB' [THEN subsetD]) 
   1.240 +done
   1.241 +
   1.242  end