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.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  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  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"