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