author paulson Mon Mar 17 17:37:48 2003 +0100 (2003-03-17) changeset 13866 b42d7983a822 parent 13865 0a6bf71955b0 child 13867 1fdecd15437f
More "progress set" material
 src/HOL/UNITY/Comp/Progress.thy file | annotate | diff | revisions src/HOL/UNITY/ProgressSets.thy file | annotate | diff | revisions src/HOL/UNITY/Transformers.thy file | annotate | diff | revisions
```     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.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)
```
```     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.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.232 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
2.233 +apply (insert prog)
2.235 +  apply (force simp add: progress_set_def awp_iff_stable [symmetric])
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.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.20 @@ -274,10 +278,10 @@
3.21  apply (blast intro: wens_set.Union)
3.22  done
3.23
3.25 -  assumes awpF: "T-B \<subseteq> awp F T"
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.31    shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
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