author | paulson |
Fri, 21 Mar 2003 18:16:18 +0100 | |
changeset 13874 | 0da2141606c6 |
parent 13870 | cf947d1ec5ff |
child 13885 | de6fac7d5351 |
permissions | -rw-r--r-- |
13853 | 1 |
(* Title: HOL/UNITY/ProgressSets |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2003 University of Cambridge |
|
5 |
||
6 |
Progress Sets. From |
|
7 |
||
8 |
David Meier and Beverly Sanders, |
|
9 |
Composing Leads-to Properties |
|
10 |
Theoretical Computer Science 243:1-2 (2000), 339-361. |
|
13861 | 11 |
|
12 |
David Meier, |
|
13 |
Progress Properties in Program Refinement and Parallel Composition |
|
14 |
Swiss Federal Institute of Technology Zurich (1997) |
|
13853 | 15 |
*) |
16 |
||
17 |
header{*Progress Sets*} |
|
18 |
||
19 |
theory ProgressSets = Transformers: |
|
20 |
||
13866 | 21 |
subsection {*Complete Lattices and the Operator @{term cl}*} |
22 |
||
13853 | 23 |
constdefs |
13861 | 24 |
lattice :: "'a set set => bool" |
25 |
--{*Meier calls them closure sets, but they are just complete lattices*} |
|
26 |
"lattice L == |
|
27 |
(\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)" |
|
13853 | 28 |
|
29 |
cl :: "['a set set, 'a set] => 'a set" |
|
30 |
--{*short for ``closure''*} |
|
13861 | 31 |
"cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}" |
13853 | 32 |
|
13861 | 33 |
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L" |
34 |
by (force simp add: lattice_def) |
|
13853 | 35 |
|
13861 | 36 |
lemma empty_in_lattice: "lattice L ==> {} \<in> L" |
37 |
by (force simp add: lattice_def) |
|
13853 | 38 |
|
13861 | 39 |
lemma Union_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Union>M \<in> L" |
40 |
by (simp add: lattice_def) |
|
13853 | 41 |
|
13861 | 42 |
lemma Inter_in_lattice: "[|M \<subseteq> L; lattice L|] ==> \<Inter>M \<in> L" |
43 |
by (simp add: lattice_def) |
|
13853 | 44 |
|
13861 | 45 |
lemma UN_in_lattice: |
46 |
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L" |
|
13853 | 47 |
apply (simp add: Set.UN_eq) |
13861 | 48 |
apply (blast intro: Union_in_lattice) |
13853 | 49 |
done |
50 |
||
13861 | 51 |
lemma INT_in_lattice: |
52 |
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i) \<in> L" |
|
13853 | 53 |
apply (simp add: INT_eq) |
13861 | 54 |
apply (blast intro: Inter_in_lattice) |
13853 | 55 |
done |
56 |
||
13861 | 57 |
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L" |
13853 | 58 |
apply (simp only: Un_eq_Union) |
13861 | 59 |
apply (blast intro: Union_in_lattice) |
13853 | 60 |
done |
61 |
||
13861 | 62 |
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L" |
13853 | 63 |
apply (simp only: Int_eq_Inter) |
13861 | 64 |
apply (blast intro: Inter_in_lattice) |
13853 | 65 |
done |
66 |
||
13861 | 67 |
lemma lattice_stable: "lattice {X. F \<in> stable X}" |
68 |
by (simp add: lattice_def stable_def constrains_def, blast) |
|
13853 | 69 |
|
13861 | 70 |
text{*The next three results state that @{term "cl L r"} is the minimal |
71 |
element of @{term L} that includes @{term r}.*} |
|
72 |
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L" |
|
73 |
apply (simp add: lattice_def cl_def) |
|
13853 | 74 |
apply (erule conjE) |
75 |
apply (drule spec, erule mp, blast) |
|
76 |
done |
|
77 |
||
13861 | 78 |
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" |
13853 | 79 |
by (force simp add: cl_def) |
80 |
||
81 |
text{*The next three lemmas constitute assertion (4.61)*} |
|
13861 | 82 |
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'" |
83 |
by (simp add: cl_def, blast) |
|
84 |
||
85 |
lemma subset_cl: "r \<subseteq> cl L r" |
|
86 |
by (simp add: cl_def, blast) |
|
87 |
||
13874 | 88 |
text{*A reformulation of @{thm subset_cl}*} |
89 |
lemma clI: "x \<in> r ==> x \<in> cl L r" |
|
90 |
by (simp add: cl_def, blast) |
|
91 |
||
92 |
text{*A reformulation of @{thm cl_least}*} |
|
93 |
lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B" |
|
94 |
by (force simp add: cl_def) |
|
95 |
||
13861 | 96 |
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)" |
13853 | 97 |
by (simp add: cl_def, blast) |
98 |
||
13861 | 99 |
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s" |
100 |
apply (rule equalityI) |
|
101 |
prefer 2 |
|
102 |
apply (simp add: cl_def, blast) |
|
103 |
apply (rule cl_least) |
|
104 |
apply (blast intro: Un_in_lattice cl_in_lattice) |
|
105 |
apply (blast intro: subset_cl [THEN subsetD]) |
|
106 |
done |
|
13853 | 107 |
|
13861 | 108 |
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))" |
13853 | 109 |
apply (rule equalityI) |
13866 | 110 |
prefer 2 apply (simp add: cl_def, blast) |
13853 | 111 |
apply (rule cl_least) |
13861 | 112 |
apply (blast intro: UN_in_lattice cl_in_lattice) |
13853 | 113 |
apply (blast intro: subset_cl [THEN subsetD]) |
114 |
done |
|
115 |
||
13874 | 116 |
lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s" |
117 |
by (simp add: cl_def, blast) |
|
118 |
||
13861 | 119 |
lemma cl_idem [simp]: "cl L (cl L r) = cl L r" |
13853 | 120 |
by (simp add: cl_def, blast) |
121 |
||
13861 | 122 |
lemma cl_ident: "r\<in>L ==> cl L r = r" |
13853 | 123 |
by (force simp add: cl_def) |
124 |
||
13874 | 125 |
lemma cl_empty [simp]: "lattice L ==> cl L {} = {}" |
126 |
by (simp add: cl_ident empty_in_lattice) |
|
127 |
||
128 |
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV" |
|
129 |
by (simp add: cl_ident UNIV_in_lattice) |
|
130 |
||
13853 | 131 |
text{*Assertion (4.62)*} |
13861 | 132 |
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" |
13853 | 133 |
apply (rule iffI) |
134 |
apply (erule subst) |
|
13861 | 135 |
apply (erule cl_in_lattice) |
13853 | 136 |
apply (erule cl_ident) |
137 |
done |
|
138 |
||
13861 | 139 |
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" |
140 |
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl) |
|
141 |
||
142 |
||
13866 | 143 |
subsection {*Progress Sets and the Main Lemma*} |
144 |
||
13861 | 145 |
constdefs |
146 |
closed :: "['a program, 'a set, 'a set, 'a set set] => bool" |
|
147 |
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L --> |
|
148 |
T \<inter> (B \<union> wp act M) \<in> L" |
|
149 |
||
150 |
progress_set :: "['a program, 'a set, 'a set] => 'a set set set" |
|
151 |
"progress_set F T B == |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
152 |
{L. lattice L & B \<in> L & T \<in> L & closed F T B L}" |
13861 | 153 |
|
154 |
lemma closedD: |
|
155 |
"[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] |
|
156 |
==> T \<inter> (B \<union> wp act M) \<in> L" |
|
157 |
by (simp add: closed_def) |
|
158 |
||
13866 | 159 |
text{*Note: the formalization below replaces Meier's @{term q} by @{term B} |
160 |
and @{term m} by @{term X}. *} |
|
161 |
||
162 |
text{*Part of the proof of the claim at the bottom of page 97. It's |
|
163 |
proved separately because the argument requires a generalization over |
|
164 |
all @{term "act \<in> Acts F"}.*} |
|
13861 | 165 |
lemma lattice_awp_lemma: |
13866 | 166 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
167 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*} |
|
13861 | 168 |
and latt: "lattice C" |
13866 | 169 |
and TC: "T \<in> C" |
170 |
and BC: "B \<in> C" |
|
171 |
and clos: "closed F T B C" |
|
172 |
shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C" |
|
13861 | 173 |
apply (simp del: INT_simps add: awp_def INT_extend_simps) |
174 |
apply (rule INT_in_lattice [OF latt]) |
|
175 |
apply (erule closedD [OF clos]) |
|
13866 | 176 |
apply (simp add: subset_trans [OF BsubX Un_upper1]) |
177 |
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)") |
|
13874 | 178 |
prefer 2 apply (blast intro: TC clD) |
13861 | 179 |
apply (erule ssubst) |
13866 | 180 |
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) |
13861 | 181 |
done |
182 |
||
13866 | 183 |
text{*Remainder of the proof of the claim at the bottom of page 97.*} |
13861 | 184 |
lemma lattice_lemma: |
13866 | 185 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
186 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*} |
|
13861 | 187 |
and act: "act \<in> Acts F" |
188 |
and latt: "lattice C" |
|
13866 | 189 |
and TC: "T \<in> C" |
190 |
and BC: "B \<in> C" |
|
191 |
and clos: "closed F T B C" |
|
192 |
shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C" |
|
193 |
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C") |
|
194 |
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC) |
|
13861 | 195 |
apply (drule Int_in_lattice |
13866 | 196 |
[OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r] |
13861 | 197 |
latt]) |
198 |
apply (subgoal_tac |
|
13866 | 199 |
"T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = |
200 |
T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") |
|
13861 | 201 |
prefer 2 apply blast |
202 |
apply simp |
|
13866 | 203 |
apply (drule Un_in_lattice [OF _ TXC latt]) |
13861 | 204 |
apply (subgoal_tac |
13866 | 205 |
"T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = |
206 |
T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)") |
|
207 |
apply simp |
|
208 |
apply (blast intro: BsubX [THEN subsetD]) |
|
13861 | 209 |
done |
210 |
||
211 |
||
13866 | 212 |
text{*Induction step for the main lemma*} |
13861 | 213 |
lemma progress_induction_step: |
13866 | 214 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
13861 | 215 |
and act: "act \<in> Acts F" |
13866 | 216 |
and Xwens: "X \<in> wens_set F B" |
13861 | 217 |
and latt: "lattice C" |
13866 | 218 |
and TC: "T \<in> C" |
219 |
and BC: "B \<in> C" |
|
220 |
and clos: "closed F T B C" |
|
13861 | 221 |
and Fstable: "F \<in> stable T" |
13866 | 222 |
shows "T \<inter> wens F act X \<in> C" |
13861 | 223 |
proof - |
13866 | 224 |
from Xwens have BsubX: "B \<subseteq> X" |
225 |
by (rule wens_set_imp_subset) |
|
226 |
let ?r = "wens F act X" |
|
227 |
have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X" |
|
228 |
by (simp add: wens_unfold [symmetric]) |
|
229 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)" |
|
230 |
by blast |
|
231 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)" |
|
232 |
by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) |
|
233 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" |
|
234 |
by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD]) |
|
235 |
then have "cl C (T\<inter>?r) \<subseteq> |
|
236 |
cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))" |
|
237 |
by (rule cl_mono) |
|
238 |
then have "cl C (T\<inter>?r) \<subseteq> |
|
239 |
T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" |
|
240 |
by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos]) |
|
241 |
then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X" |
|
242 |
by blast |
|
243 |
then have "cl C (T\<inter>?r) \<subseteq> ?r" |
|
244 |
by (blast intro!: subset_wens) |
|
245 |
then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r" |
|
246 |
by (simp add: Int_subset_iff cl_ident TC |
|
247 |
subset_trans [OF cl_mono [OF Int_lower1]]) |
|
248 |
show ?thesis |
|
249 |
by (rule cl_subset_in_lattice [OF cl_subset latt]) |
|
13861 | 250 |
qed |
251 |
||
13866 | 252 |
text{*The Lemma proved on page 96*} |
13861 | 253 |
lemma progress_set_lemma: |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
254 |
"[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C" |
13861 | 255 |
apply (simp add: progress_set_def, clarify) |
256 |
apply (erule wens_set.induct) |
|
257 |
txt{*Base*} |
|
258 |
apply (simp add: Int_in_lattice) |
|
259 |
txt{*The difficult @{term wens} case*} |
|
260 |
apply (simp add: progress_induction_step) |
|
261 |
txt{*Disjunctive case*} |
|
262 |
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") |
|
263 |
apply (simp add: Int_Union) |
|
264 |
apply (blast intro: UN_in_lattice) |
|
265 |
done |
|
266 |
||
13866 | 267 |
|
268 |
subsection {*The Progress Set Union Theorem*} |
|
269 |
||
270 |
lemma closed_mono: |
|
271 |
assumes BB': "B \<subseteq> B'" |
|
272 |
and TBwp: "T \<inter> (B \<union> wp act M) \<in> C" |
|
273 |
and B'C: "B' \<in> C" |
|
274 |
and TC: "T \<in> C" |
|
275 |
and latt: "lattice C" |
|
276 |
shows "T \<inter> (B' \<union> wp act M) \<in> C" |
|
277 |
proof - |
|
278 |
from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C" |
|
279 |
by (simp add: Int_Un_distrib) |
|
280 |
then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C" |
|
281 |
by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) |
|
282 |
show ?thesis |
|
283 |
by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], |
|
284 |
blast intro: BB' [THEN subsetD]) |
|
285 |
qed |
|
286 |
||
287 |
||
288 |
lemma progress_set_mono: |
|
289 |
assumes BB': "B \<subseteq> B'" |
|
290 |
shows |
|
291 |
"[| B' \<in> C; C \<in> progress_set F T B|] |
|
292 |
==> C \<in> progress_set F T B'" |
|
293 |
by (simp add: progress_set_def closed_def closed_mono [OF BB'] |
|
294 |
subset_trans [OF BB']) |
|
295 |
||
296 |
theorem progress_set_Union: |
|
13874 | 297 |
assumes leadsTo: "F \<in> A leadsTo B'" |
298 |
and prog: "C \<in> progress_set F T B" |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
299 |
and Fstable: "F \<in> stable T" |
13866 | 300 |
and BB': "B \<subseteq> B'" |
301 |
and B'C: "B' \<in> C" |
|
302 |
and Gco: "!!X. X\<in>C ==> G \<in> X-B co X" |
|
303 |
shows "F\<squnion>G \<in> T\<inter>A leadsTo B'" |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
304 |
apply (insert prog Fstable) |
13866 | 305 |
apply (rule leadsTo_Join [OF leadsTo]) |
306 |
apply (force simp add: progress_set_def awp_iff_stable [symmetric]) |
|
307 |
apply (simp add: awp_iff_constrains) |
|
308 |
apply (drule progress_set_mono [OF BB' B'C]) |
|
309 |
apply (blast intro: progress_set_lemma Gco constrains_weaken_L |
|
310 |
BB' [THEN subsetD]) |
|
311 |
done |
|
312 |
||
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
313 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
314 |
subsection {*Some Progress Sets*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
315 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
316 |
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
317 |
by (simp add: progress_set_def lattice_def closed_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
318 |
|
13874 | 319 |
|
320 |
||
321 |
subsubsection {*Derived Relation from a Lattice*} |
|
322 |
text{*From Meier's thesis, section 4.5.3*} |
|
323 |
||
324 |
constdefs |
|
325 |
relcl :: "'a set set => ('a * 'a) set" |
|
326 |
"relcl L == {(x,y). y \<in> cl L {x}}" |
|
327 |
||
328 |
lemma relcl_refl: "(a,a) \<in> relcl L" |
|
329 |
by (simp add: relcl_def subset_cl [THEN subsetD]) |
|
330 |
||
331 |
lemma relcl_trans: |
|
332 |
"[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L" |
|
333 |
apply (simp add: relcl_def) |
|
334 |
apply (blast intro: clD cl_in_lattice) |
|
335 |
done |
|
336 |
||
337 |
lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)" |
|
338 |
by (simp add: reflI relcl_def subset_cl [THEN subsetD]) |
|
339 |
||
340 |
lemma trans_relcl: "lattice L ==> trans (relcl L)" |
|
341 |
by (blast intro: relcl_trans transI) |
|
342 |
||
343 |
text{*Related to equation (4.71) of Meier's thesis*} |
|
344 |
lemma cl_eq_Collect_relcl: |
|
345 |
"lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" |
|
346 |
apply (cut_tac UN_singleton [of X, symmetric]) |
|
347 |
apply (erule ssubst) |
|
348 |
apply (force simp only: relcl_def cl_UN) |
|
349 |
done |
|
350 |
||
351 |
||
352 |
subsubsection {*Decoupling Theorems*} |
|
353 |
||
354 |
constdefs |
|
355 |
decoupled :: "['a program, 'a program] => bool" |
|
356 |
"decoupled F G == |
|
357 |
\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)" |
|
358 |
||
359 |
||
360 |
text{*Rao's Decoupling Theorem*} |
|
361 |
lemma stableco: "F \<in> stable A ==> F \<in> A-B co A" |
|
362 |
by (simp add: stable_def constrains_def, blast) |
|
363 |
||
364 |
theorem decoupling: |
|
365 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
366 |
and Gstable: "G \<in> stable B" |
|
367 |
and dec: "decoupled F G" |
|
368 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
369 |
proof - |
|
370 |
have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B" |
|
371 |
by (simp add: progress_set_def lattice_stable Gstable closed_def |
|
372 |
stable_Un [OF Gstable] dec [unfolded decoupled_def]) |
|
373 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
374 |
by (rule progress_set_Union [OF leadsTo prog], |
|
375 |
simp_all add: Gstable stableco) |
|
376 |
thus ?thesis by simp |
|
377 |
qed |
|
378 |
||
379 |
||
380 |
text{*Rao's Weak Decoupling Theorem*} |
|
381 |
theorem weak_decoupling: |
|
382 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
383 |
and stable: "F\<squnion>G \<in> stable B" |
|
384 |
and dec: "decoupled F (F\<squnion>G)" |
|
385 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
386 |
proof - |
|
387 |
have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" |
|
388 |
by (simp del: Join_stable |
|
389 |
add: progress_set_def lattice_stable stable closed_def |
|
390 |
stable_Un [OF stable] dec [unfolded decoupled_def]) |
|
391 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
392 |
by (rule progress_set_Union [OF leadsTo prog], |
|
393 |
simp_all del: Join_stable add: stable, |
|
394 |
simp add: stableco) |
|
395 |
thus ?thesis by simp |
|
396 |
qed |
|
397 |
||
398 |
text{*The ``Decoupling via @{term G'} Union Theorem''*} |
|
399 |
theorem decoupling_via_aux: |
|
400 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
401 |
and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B" |
|
402 |
and GG': "G \<le> G'" |
|
403 |
--{*Beware! This is the converse of the refinement relation!*} |
|
404 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
405 |
proof - |
|
406 |
from prog have stable: "G' \<in> stable B" |
|
407 |
by (simp add: progress_set_def) |
|
408 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
409 |
by (rule progress_set_Union [OF leadsTo prog], |
|
410 |
simp_all add: stable stableco component_stable [OF GG']) |
|
411 |
thus ?thesis by simp |
|
412 |
qed |
|
413 |
||
414 |
||
415 |
subsection{*Composition Theorems Based on Monotonicity and Commutativity*} |
|
416 |
||
417 |
constdefs |
|
418 |
commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" |
|
419 |
"commutes F T B L == |
|
420 |
\<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> |
|
421 |
cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" |
|
422 |
||
423 |
||
424 |
lemma commutativity1: |
|
425 |
assumes commutes: "commutes F T B L" |
|
426 |
and lattice: "lattice L" |
|
427 |
and BL: "B \<in> L" |
|
428 |
and TL: "T \<in> L" |
|
429 |
shows "closed F T B L" |
|
430 |
apply (simp add: closed_def, clarify) |
|
431 |
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice]) |
|
432 |
apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff |
|
433 |
cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1) |
|
434 |
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") |
|
435 |
prefer 2 |
|
436 |
apply (simp add: commutes [unfolded commutes_def]) |
|
437 |
apply (erule subset_trans) |
|
438 |
apply (simp add: cl_ident) |
|
439 |
apply (blast intro: rev_subsetD [OF _ wp_mono]) |
|
440 |
done |
|
441 |
||
442 |
text{*Possibly move to Relation.thy, after @{term single_valued}*} |
|
443 |
constdefs |
|
444 |
funof :: "[('a*'b)set, 'a] => 'b" |
|
445 |
"funof r == (\<lambda>x. THE y. (x,y) \<in> r)" |
|
446 |
||
447 |
lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y" |
|
448 |
by (simp add: funof_def single_valued_def, blast) |
|
449 |
||
450 |
lemma funof_Pair_in: |
|
451 |
"[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r" |
|
452 |
by (force simp add: funof_eq) |
|
453 |
||
454 |
lemma funof_in: |
|
455 |
"[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" |
|
456 |
by (force simp add: funof_eq) |
|
457 |
||
458 |
lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A" |
|
459 |
by (force simp add: in_wp_iff funof_eq) |
|
460 |
||
461 |
||
462 |
subsubsection{*Commutativity of Functions and Relation*} |
|
463 |
text{*Thesis, page 109*} |
|
464 |
||
465 |
(*FIXME: this proof is an unGodly mess*) |
|
466 |
lemma commutativity2: |
|
467 |
assumes dcommutes: |
|
468 |
"\<forall>act \<in> Acts F. |
|
469 |
\<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> |
|
470 |
s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" |
|
471 |
and determ: "!!act. act \<in> Acts F ==> single_valued act" |
|
472 |
and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" |
|
473 |
and lattice: "lattice L" |
|
474 |
and BL: "B \<in> L" |
|
475 |
and TL: "T \<in> L" |
|
476 |
and Fstable: "F \<in> stable T" |
|
477 |
shows "commutes F T B L" |
|
478 |
apply (simp add: commutes_def, clarify) |
|
479 |
apply (rename_tac t) |
|
480 |
apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") |
|
481 |
prefer 2 apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp) |
|
482 |
apply clarify |
|
483 |
apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") |
|
484 |
prefer 2 |
|
485 |
apply (intro ballI impI) |
|
486 |
apply (subst cl_ident [symmetric], assumption) |
|
487 |
apply (simp add: relcl_def) |
|
488 |
apply (blast intro: cl_mono [THEN [2] rev_subsetD]) |
|
489 |
apply (subgoal_tac "funof act s \<in> T\<inter>M") |
|
490 |
prefer 2 |
|
491 |
apply (cut_tac Fstable) |
|
492 |
apply (force intro!: funof_in |
|
493 |
simp add: wp_def stable_def constrains_def determ total) |
|
494 |
apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L") |
|
495 |
prefer 2 |
|
496 |
apply (rule dcommutes [rule_format], assumption+) |
|
497 |
apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)") |
|
498 |
prefer 2 |
|
499 |
apply (simp add: relcl_def) |
|
500 |
apply (blast intro: BL cl_mono [THEN [2] rev_subsetD]) |
|
501 |
apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))") |
|
502 |
prefer 2 |
|
503 |
apply (blast intro: funof_imp_wp determ) |
|
504 |
apply (blast intro: TL cl_mono [THEN [2] rev_subsetD]) |
|
505 |
done |
|
506 |
||
13853 | 507 |
end |