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 |
|
|
88 |
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
|
13853
|
89 |
by (simp add: cl_def, blast)
|
|
90 |
|
13861
|
91 |
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s"
|
|
92 |
apply (rule equalityI)
|
|
93 |
prefer 2
|
|
94 |
apply (simp add: cl_def, blast)
|
|
95 |
apply (rule cl_least)
|
|
96 |
apply (blast intro: Un_in_lattice cl_in_lattice)
|
|
97 |
apply (blast intro: subset_cl [THEN subsetD])
|
|
98 |
done
|
13853
|
99 |
|
13861
|
100 |
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
|
13853
|
101 |
apply (rule equalityI)
|
13866
|
102 |
prefer 2 apply (simp add: cl_def, blast)
|
13853
|
103 |
apply (rule cl_least)
|
13861
|
104 |
apply (blast intro: UN_in_lattice cl_in_lattice)
|
13853
|
105 |
apply (blast intro: subset_cl [THEN subsetD])
|
|
106 |
done
|
|
107 |
|
13861
|
108 |
lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
|
13853
|
109 |
by (simp add: cl_def, blast)
|
|
110 |
|
13861
|
111 |
lemma cl_ident: "r\<in>L ==> cl L r = r"
|
13853
|
112 |
by (force simp add: cl_def)
|
|
113 |
|
|
114 |
text{*Assertion (4.62)*}
|
13861
|
115 |
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)"
|
13853
|
116 |
apply (rule iffI)
|
|
117 |
apply (erule subst)
|
13861
|
118 |
apply (erule cl_in_lattice)
|
13853
|
119 |
apply (erule cl_ident)
|
|
120 |
done
|
|
121 |
|
13861
|
122 |
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L"
|
|
123 |
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
|
|
124 |
|
|
125 |
|
13866
|
126 |
subsection {*Progress Sets and the Main Lemma*}
|
|
127 |
|
13861
|
128 |
constdefs
|
|
129 |
closed :: "['a program, 'a set, 'a set, 'a set set] => bool"
|
|
130 |
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
|
|
131 |
T \<inter> (B \<union> wp act M) \<in> L"
|
|
132 |
|
|
133 |
progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
|
|
134 |
"progress_set F T B ==
|
|
135 |
{L. F \<in> stable T & lattice L & B \<in> L & T \<in> L & closed F T B L}"
|
|
136 |
|
|
137 |
lemma closedD:
|
|
138 |
"[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|]
|
|
139 |
==> T \<inter> (B \<union> wp act M) \<in> L"
|
|
140 |
by (simp add: closed_def)
|
|
141 |
|
13866
|
142 |
text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
|
|
143 |
and @{term m} by @{term X}. *}
|
|
144 |
|
|
145 |
text{*Part of the proof of the claim at the bottom of page 97. It's
|
|
146 |
proved separately because the argument requires a generalization over
|
|
147 |
all @{term "act \<in> Acts F"}.*}
|
13861
|
148 |
lemma lattice_awp_lemma:
|
13866
|
149 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
|
|
150 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
|
13861
|
151 |
and latt: "lattice C"
|
13866
|
152 |
and TC: "T \<in> C"
|
|
153 |
and BC: "B \<in> C"
|
|
154 |
and clos: "closed F T B C"
|
|
155 |
shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
|
13861
|
156 |
apply (simp del: INT_simps add: awp_def INT_extend_simps)
|
|
157 |
apply (rule INT_in_lattice [OF latt])
|
|
158 |
apply (erule closedD [OF clos])
|
13866
|
159 |
apply (simp add: subset_trans [OF BsubX Un_upper1])
|
|
160 |
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
|
|
161 |
prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least])
|
13861
|
162 |
apply (erule ssubst)
|
13866
|
163 |
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
|
13861
|
164 |
done
|
|
165 |
|
13866
|
166 |
text{*Remainder of the proof of the claim at the bottom of page 97.*}
|
13861
|
167 |
lemma lattice_lemma:
|
13866
|
168 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
|
|
169 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
|
13861
|
170 |
and act: "act \<in> Acts F"
|
|
171 |
and latt: "lattice C"
|
13866
|
172 |
and TC: "T \<in> C"
|
|
173 |
and BC: "B \<in> C"
|
|
174 |
and clos: "closed F T B C"
|
|
175 |
shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
|
|
176 |
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
|
|
177 |
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
|
13861
|
178 |
apply (drule Int_in_lattice
|
13866
|
179 |
[OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
|
13861
|
180 |
latt])
|
|
181 |
apply (subgoal_tac
|
13866
|
182 |
"T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) =
|
|
183 |
T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))")
|
13861
|
184 |
prefer 2 apply blast
|
|
185 |
apply simp
|
13866
|
186 |
apply (drule Un_in_lattice [OF _ TXC latt])
|
13861
|
187 |
apply (subgoal_tac
|
13866
|
188 |
"T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X =
|
|
189 |
T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
|
|
190 |
apply simp
|
|
191 |
apply (blast intro: BsubX [THEN subsetD])
|
13861
|
192 |
done
|
|
193 |
|
|
194 |
|
13866
|
195 |
text{*Induction step for the main lemma*}
|
13861
|
196 |
lemma progress_induction_step:
|
13866
|
197 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
|
13861
|
198 |
and act: "act \<in> Acts F"
|
13866
|
199 |
and Xwens: "X \<in> wens_set F B"
|
13861
|
200 |
and latt: "lattice C"
|
13866
|
201 |
and TC: "T \<in> C"
|
|
202 |
and BC: "B \<in> C"
|
|
203 |
and clos: "closed F T B C"
|
13861
|
204 |
and Fstable: "F \<in> stable T"
|
13866
|
205 |
shows "T \<inter> wens F act X \<in> C"
|
13861
|
206 |
proof -
|
13866
|
207 |
from Xwens have BsubX: "B \<subseteq> X"
|
|
208 |
by (rule wens_set_imp_subset)
|
|
209 |
let ?r = "wens F act X"
|
|
210 |
have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
|
|
211 |
by (simp add: wens_unfold [symmetric])
|
|
212 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
|
|
213 |
by blast
|
|
214 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
|
|
215 |
by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
|
|
216 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
|
|
217 |
by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
|
|
218 |
then have "cl C (T\<inter>?r) \<subseteq>
|
|
219 |
cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
|
|
220 |
by (rule cl_mono)
|
|
221 |
then have "cl C (T\<inter>?r) \<subseteq>
|
|
222 |
T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
|
|
223 |
by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
|
|
224 |
then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
|
|
225 |
by blast
|
|
226 |
then have "cl C (T\<inter>?r) \<subseteq> ?r"
|
|
227 |
by (blast intro!: subset_wens)
|
|
228 |
then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
|
|
229 |
by (simp add: Int_subset_iff cl_ident TC
|
|
230 |
subset_trans [OF cl_mono [OF Int_lower1]])
|
|
231 |
show ?thesis
|
|
232 |
by (rule cl_subset_in_lattice [OF cl_subset latt])
|
13861
|
233 |
qed
|
|
234 |
|
13866
|
235 |
text{*The Lemma proved on page 96*}
|
13861
|
236 |
lemma progress_set_lemma:
|
13866
|
237 |
"[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
|
13861
|
238 |
apply (simp add: progress_set_def, clarify)
|
|
239 |
apply (erule wens_set.induct)
|
|
240 |
txt{*Base*}
|
|
241 |
apply (simp add: Int_in_lattice)
|
|
242 |
txt{*The difficult @{term wens} case*}
|
|
243 |
apply (simp add: progress_induction_step)
|
|
244 |
txt{*Disjunctive case*}
|
|
245 |
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
|
|
246 |
apply (simp add: Int_Union)
|
|
247 |
apply (blast intro: UN_in_lattice)
|
|
248 |
done
|
|
249 |
|
13866
|
250 |
|
|
251 |
subsection {*The Progress Set Union Theorem*}
|
|
252 |
|
|
253 |
lemma closed_mono:
|
|
254 |
assumes BB': "B \<subseteq> B'"
|
|
255 |
and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
|
|
256 |
and B'C: "B' \<in> C"
|
|
257 |
and TC: "T \<in> C"
|
|
258 |
and latt: "lattice C"
|
|
259 |
shows "T \<inter> (B' \<union> wp act M) \<in> C"
|
|
260 |
proof -
|
|
261 |
from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
|
|
262 |
by (simp add: Int_Un_distrib)
|
|
263 |
then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
|
|
264 |
by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
|
|
265 |
show ?thesis
|
|
266 |
by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
|
|
267 |
blast intro: BB' [THEN subsetD])
|
|
268 |
qed
|
|
269 |
|
|
270 |
|
|
271 |
lemma progress_set_mono:
|
|
272 |
assumes BB': "B \<subseteq> B'"
|
|
273 |
shows
|
|
274 |
"[| B' \<in> C; C \<in> progress_set F T B|]
|
|
275 |
==> C \<in> progress_set F T B'"
|
|
276 |
by (simp add: progress_set_def closed_def closed_mono [OF BB']
|
|
277 |
subset_trans [OF BB'])
|
|
278 |
|
|
279 |
theorem progress_set_Union:
|
|
280 |
assumes prog: "C \<in> progress_set F T B"
|
|
281 |
and BB': "B \<subseteq> B'"
|
|
282 |
and B'C: "B' \<in> C"
|
|
283 |
and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
|
|
284 |
and leadsTo: "F \<in> A leadsTo B'"
|
|
285 |
shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
|
|
286 |
apply (insert prog)
|
|
287 |
apply (rule leadsTo_Join [OF leadsTo])
|
|
288 |
apply (force simp add: progress_set_def awp_iff_stable [symmetric])
|
|
289 |
apply (simp add: awp_iff_constrains)
|
|
290 |
apply (drule progress_set_mono [OF BB' B'C])
|
|
291 |
apply (blast intro: progress_set_lemma Gco constrains_weaken_L
|
|
292 |
BB' [THEN subsetD])
|
|
293 |
done
|
|
294 |
|
13853
|
295 |
end
|