author | paulson |
Fri, 31 Jan 2003 20:12:44 +0100 | |
changeset 13798 | 4c1a53627500 |
parent 13792 | d1811693899c |
child 13805 | 3786b2fd6808 |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.thy |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
5 |
|
11190 | 6 |
From Chandy and Sanders, "Reasoning About Program Composition", |
7 |
Technical Report 2000-003, University of Florida, 2000. |
|
8 |
||
9 |
Revised by Sidi Ehmety on January 2001 |
|
10 |
||
11 |
Added: Compatibility, weakest guarantees, etc. |
|
12 |
||
13 |
and Weakest existential property, |
|
14 |
from Charpentier and Chandy "Theorems about Composition", |
|
15 |
Fifth International Conference on Mathematics of Program, 2000. |
|
16 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
17 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
18 |
|
13798 | 19 |
header{*Guarantees Specifications*} |
20 |
||
13792 | 21 |
theory Guar = Comp: |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
22 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11190
diff
changeset
|
23 |
instance program :: (type) order |
13792 | 24 |
by (intro_classes, |
25 |
(assumption | rule component_refl component_trans component_antisym |
|
26 |
program_less_le)+) |
|
27 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
28 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
29 |
constdefs |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
30 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
31 |
(*Existential and Universal properties. I formalize the two-program |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
32 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
33 |
|
13792 | 34 |
ex_prop :: "'a program set => bool" |
35 |
"ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
36 |
|
13792 | 37 |
strict_ex_prop :: "'a program set => bool" |
38 |
"strict_ex_prop X == \<forall>F G. F ok G --> (F:X | G: X) = (F Join G : X)" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
39 |
|
13792 | 40 |
uv_prop :: "'a program set => bool" |
41 |
"uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
42 |
|
13792 | 43 |
strict_uv_prop :: "'a program set => bool" |
44 |
"strict_uv_prop X == |
|
45 |
SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
46 |
|
13792 | 47 |
guar :: "['a program set, 'a program set] => 'a program set" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
48 |
(infixl "guarantees" 55) (*higher than membership, lower than Co*) |
13792 | 49 |
"X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}" |
11190 | 50 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
51 |
|
11190 | 52 |
(* Weakest guarantees *) |
13792 | 53 |
wg :: "['a program, 'a program set] => 'a program set" |
11190 | 54 |
"wg F Y == Union({X. F:X guarantees Y})" |
55 |
||
56 |
(* Weakest existential property stronger than X *) |
|
57 |
wx :: "('a program) set => ('a program)set" |
|
58 |
"wx X == Union({Y. Y<=X & ex_prop Y})" |
|
59 |
||
60 |
(*Ill-defined programs can arise through "Join"*) |
|
13792 | 61 |
welldef :: "'a program set" |
11190 | 62 |
"welldef == {F. Init F ~= {}}" |
63 |
||
13792 | 64 |
refines :: "['a program, 'a program, 'a program set] => bool" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
65 |
("(3_ refines _ wrt _)" [10,10,10] 10) |
11190 | 66 |
"G refines F wrt X == |
13792 | 67 |
\<forall>H. (F ok H & G ok H & F Join H : welldef Int X) --> |
68 |
(G Join H : welldef Int X)" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
69 |
|
13792 | 70 |
iso_refines :: "['a program, 'a program, 'a program set] => bool" |
11190 | 71 |
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) |
72 |
"G iso_refines F wrt X == |
|
73 |
F : welldef Int X --> G : welldef Int X" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
74 |
|
13792 | 75 |
|
76 |
lemma OK_insert_iff: |
|
77 |
"(OK (insert i I) F) = |
|
78 |
(if i:I then OK I F else OK I F & (F i ok JOIN I F))" |
|
79 |
by (auto intro: ok_sym simp add: OK_iff_ok) |
|
80 |
||
81 |
||
82 |
(*** existential properties ***) |
|
13798 | 83 |
lemma ex1 [rule_format]: |
13792 | 84 |
"[| ex_prop X; finite GG |] ==> |
85 |
GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X" |
|
86 |
apply (unfold ex_prop_def) |
|
87 |
apply (erule finite_induct) |
|
88 |
apply (auto simp add: OK_insert_iff Int_insert_left) |
|
89 |
done |
|
90 |
||
91 |
||
92 |
lemma ex2: |
|
93 |
"\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X |
|
94 |
==> ex_prop X" |
|
95 |
apply (unfold ex_prop_def, clarify) |
|
96 |
apply (drule_tac x = "{F,G}" in spec) |
|
97 |
apply (auto dest: ok_sym simp add: OK_iff_ok) |
|
98 |
done |
|
99 |
||
100 |
||
101 |
(*Chandy & Sanders take this as a definition*) |
|
102 |
lemma ex_prop_finite: |
|
103 |
"ex_prop X = |
|
104 |
(\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)" |
|
105 |
by (blast intro: ex1 ex2) |
|
106 |
||
107 |
||
108 |
(*Their "equivalent definition" given at the end of section 3*) |
|
109 |
lemma ex_prop_equiv: |
|
110 |
"ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))" |
|
111 |
apply auto |
|
112 |
apply (unfold ex_prop_def component_of_def, safe) |
|
113 |
apply blast |
|
114 |
apply blast |
|
115 |
apply (subst Join_commute) |
|
116 |
apply (drule ok_sym, blast) |
|
117 |
done |
|
118 |
||
119 |
||
120 |
(*** universal properties ***) |
|
121 |
lemma uv1 [rule_format]: |
|
122 |
"[| uv_prop X; finite GG |] |
|
123 |
==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X" |
|
124 |
apply (unfold uv_prop_def) |
|
125 |
apply (erule finite_induct) |
|
126 |
apply (auto simp add: Int_insert_left OK_insert_iff) |
|
127 |
done |
|
128 |
||
129 |
lemma uv2: |
|
130 |
"\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X |
|
131 |
==> uv_prop X" |
|
132 |
apply (unfold uv_prop_def) |
|
133 |
apply (rule conjI) |
|
134 |
apply (drule_tac x = "{}" in spec) |
|
135 |
prefer 2 |
|
136 |
apply clarify |
|
137 |
apply (drule_tac x = "{F,G}" in spec) |
|
138 |
apply (auto dest: ok_sym simp add: OK_iff_ok) |
|
139 |
done |
|
140 |
||
141 |
(*Chandy & Sanders take this as a definition*) |
|
142 |
lemma uv_prop_finite: |
|
143 |
"uv_prop X = |
|
144 |
(\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)" |
|
145 |
by (blast intro: uv1 uv2) |
|
146 |
||
147 |
(*** guarantees ***) |
|
148 |
||
149 |
lemma guaranteesI: |
|
150 |
"(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) |
|
151 |
==> F : X guarantees Y" |
|
152 |
by (simp add: guar_def component_def) |
|
153 |
||
154 |
lemma guaranteesD: |
|
155 |
"[| F : X guarantees Y; F ok G; F Join G : X |] |
|
156 |
==> F Join G : Y" |
|
157 |
by (unfold guar_def component_def, blast) |
|
158 |
||
159 |
(*This version of guaranteesD matches more easily in the conclusion |
|
160 |
The major premise can no longer be F<=H since we need to reason about G*) |
|
161 |
lemma component_guaranteesD: |
|
162 |
"[| F : X guarantees Y; F Join G = H; H : X; F ok G |] |
|
163 |
==> H : Y" |
|
164 |
by (unfold guar_def, blast) |
|
165 |
||
166 |
lemma guarantees_weaken: |
|
167 |
"[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'" |
|
168 |
by (unfold guar_def, blast) |
|
169 |
||
170 |
lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV" |
|
171 |
by (unfold guar_def, blast) |
|
172 |
||
173 |
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
|
174 |
lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y" |
|
175 |
by (unfold guar_def, blast) |
|
176 |
||
177 |
(*Remark at end of section 4.1 *) |
|
178 |
||
179 |
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" |
|
180 |
apply (simp (no_asm_use) add: guar_def ex_prop_equiv) |
|
181 |
apply safe |
|
182 |
apply (drule_tac x = x in spec) |
|
183 |
apply (drule_tac [2] x = x in spec) |
|
184 |
apply (drule_tac [2] sym) |
|
185 |
apply (auto simp add: component_of_def) |
|
186 |
done |
|
187 |
||
188 |
lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" |
|
189 |
apply (simp (no_asm_use) add: guar_def ex_prop_equiv) |
|
190 |
apply safe |
|
191 |
apply (auto simp add: component_of_def dest: sym) |
|
192 |
done |
|
193 |
||
194 |
lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" |
|
195 |
apply (rule iffI) |
|
196 |
apply (rule ex_prop_imp) |
|
197 |
apply (auto simp add: guarantees_imp) |
|
198 |
done |
|
199 |
||
200 |
||
201 |
(** Distributive laws. Re-orient to perform miniscoping **) |
|
202 |
||
203 |
lemma guarantees_UN_left: |
|
204 |
"(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)" |
|
205 |
by (unfold guar_def, blast) |
|
206 |
||
207 |
lemma guarantees_Un_left: |
|
208 |
"(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)" |
|
209 |
by (unfold guar_def, blast) |
|
210 |
||
211 |
lemma guarantees_INT_right: |
|
212 |
"X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)" |
|
213 |
by (unfold guar_def, blast) |
|
214 |
||
215 |
lemma guarantees_Int_right: |
|
216 |
"Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)" |
|
217 |
by (unfold guar_def, blast) |
|
218 |
||
219 |
lemma guarantees_Int_right_I: |
|
220 |
"[| F : Z guarantees X; F : Z guarantees Y |] |
|
221 |
==> F : Z guarantees (X Int Y)" |
|
222 |
by (simp add: guarantees_Int_right) |
|
223 |
||
224 |
lemma guarantees_INT_right_iff: |
|
225 |
"(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))" |
|
226 |
by (simp add: guarantees_INT_right) |
|
227 |
||
228 |
lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))" |
|
229 |
by (unfold guar_def, blast) |
|
230 |
||
231 |
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X" |
|
232 |
by (unfold guar_def, blast) |
|
233 |
||
234 |
(** The following two can be expressed using intersection and subset, which |
|
235 |
is more faithful to the text but looks cryptic. |
|
236 |
**) |
|
237 |
||
238 |
lemma combining1: |
|
239 |
"[| F : V guarantees X; F : (X Int Y) guarantees Z |] |
|
240 |
==> F : (V Int Y) guarantees Z" |
|
241 |
||
242 |
by (unfold guar_def, blast) |
|
243 |
||
244 |
lemma combining2: |
|
245 |
"[| F : V guarantees (X Un Y); F : Y guarantees Z |] |
|
246 |
==> F : V guarantees (X Un Z)" |
|
247 |
by (unfold guar_def, blast) |
|
248 |
||
249 |
(** The following two follow Chandy-Sanders, but the use of object-quantifiers |
|
250 |
does not suit Isabelle... **) |
|
251 |
||
252 |
(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) |
|
253 |
lemma all_guarantees: |
|
254 |
"\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)" |
|
255 |
by (unfold guar_def, blast) |
|
256 |
||
257 |
(*Premises should be [| F: X guarantees Y i; i: I |] *) |
|
258 |
lemma ex_guarantees: |
|
259 |
"\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)" |
|
260 |
by (unfold guar_def, blast) |
|
261 |
||
262 |
||
263 |
(*** Additional guarantees laws, by lcp ***) |
|
264 |
||
265 |
lemma guarantees_Join_Int: |
|
266 |
"[| F: U guarantees V; G: X guarantees Y; F ok G |] |
|
267 |
==> F Join G: (U Int X) guarantees (V Int Y)" |
|
268 |
apply (unfold guar_def) |
|
269 |
apply (simp (no_asm)) |
|
270 |
apply safe |
|
271 |
apply (simp add: Join_assoc) |
|
272 |
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") |
|
273 |
apply (simp add: ok_commute) |
|
274 |
apply (simp (no_asm_simp) add: Join_ac) |
|
275 |
done |
|
276 |
||
277 |
lemma guarantees_Join_Un: |
|
278 |
"[| F: U guarantees V; G: X guarantees Y; F ok G |] |
|
279 |
==> F Join G: (U Un X) guarantees (V Un Y)" |
|
280 |
apply (unfold guar_def) |
|
281 |
apply (simp (no_asm)) |
|
282 |
apply safe |
|
283 |
apply (simp add: Join_assoc) |
|
284 |
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") |
|
285 |
apply (simp add: ok_commute) |
|
286 |
apply (simp (no_asm_simp) add: Join_ac) |
|
287 |
done |
|
288 |
||
289 |
lemma guarantees_JN_INT: |
|
290 |
"[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |] |
|
291 |
==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)" |
|
292 |
apply (unfold guar_def, auto) |
|
293 |
apply (drule bspec, assumption) |
|
294 |
apply (rename_tac "i") |
|
295 |
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) |
|
296 |
apply (auto intro: OK_imp_ok |
|
297 |
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) |
|
298 |
done |
|
299 |
||
300 |
lemma guarantees_JN_UN: |
|
301 |
"[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |] |
|
302 |
==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)" |
|
303 |
apply (unfold guar_def, auto) |
|
304 |
apply (drule bspec, assumption) |
|
305 |
apply (rename_tac "i") |
|
306 |
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) |
|
307 |
apply (auto intro: OK_imp_ok |
|
308 |
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) |
|
309 |
done |
|
310 |
||
311 |
||
312 |
(*** guarantees laws for breaking down the program, by lcp ***) |
|
313 |
||
314 |
lemma guarantees_Join_I1: |
|
315 |
"[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" |
|
316 |
apply (unfold guar_def) |
|
317 |
apply (simp (no_asm)) |
|
318 |
apply safe |
|
319 |
apply (simp add: Join_assoc) |
|
320 |
done |
|
321 |
||
322 |
lemma guarantees_Join_I2: |
|
323 |
"[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" |
|
324 |
apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) |
|
325 |
apply (blast intro: guarantees_Join_I1) |
|
326 |
done |
|
327 |
||
328 |
lemma guarantees_JN_I: |
|
329 |
"[| i : I; F i: X guarantees Y; OK I F |] |
|
330 |
==> (JN i:I. (F i)) : X guarantees Y" |
|
331 |
apply (unfold guar_def, clarify) |
|
332 |
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) |
|
333 |
apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) |
|
334 |
done |
|
335 |
||
336 |
||
337 |
(*** well-definedness ***) |
|
338 |
||
339 |
lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef" |
|
340 |
by (unfold welldef_def, auto) |
|
341 |
||
342 |
lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef" |
|
343 |
by (unfold welldef_def, auto) |
|
344 |
||
345 |
(*** refinement ***) |
|
346 |
||
347 |
lemma refines_refl: "F refines F wrt X" |
|
348 |
by (unfold refines_def, blast) |
|
349 |
||
350 |
||
351 |
(* Goalw [refines_def] |
|
352 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" |
|
353 |
by Auto_tac |
|
354 |
qed "refines_trans"; *) |
|
355 |
||
356 |
||
357 |
||
358 |
lemma strict_ex_refine_lemma: |
|
359 |
"strict_ex_prop X |
|
360 |
==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) |
|
361 |
= (F:X --> G:X)" |
|
362 |
by (unfold strict_ex_prop_def, auto) |
|
363 |
||
364 |
lemma strict_ex_refine_lemma_v: |
|
365 |
"strict_ex_prop X |
|
366 |
==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = |
|
367 |
(F: welldef Int X --> G:X)" |
|
368 |
apply (unfold strict_ex_prop_def, safe) |
|
369 |
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) |
|
370 |
apply (auto dest: Join_welldef_D1 Join_welldef_D2) |
|
371 |
done |
|
372 |
||
373 |
lemma ex_refinement_thm: |
|
374 |
"[| strict_ex_prop X; |
|
375 |
\<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] |
|
376 |
==> (G refines F wrt X) = (G iso_refines F wrt X)" |
|
377 |
apply (rule_tac x = SKIP in allE, assumption) |
|
378 |
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) |
|
379 |
done |
|
380 |
||
381 |
||
382 |
lemma strict_uv_refine_lemma: |
|
383 |
"strict_uv_prop X ==> |
|
384 |
(\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)" |
|
385 |
by (unfold strict_uv_prop_def, blast) |
|
386 |
||
387 |
lemma strict_uv_refine_lemma_v: |
|
388 |
"strict_uv_prop X |
|
389 |
==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = |
|
390 |
(F: welldef Int X --> G:X)" |
|
391 |
apply (unfold strict_uv_prop_def, safe) |
|
392 |
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) |
|
393 |
apply (auto dest: Join_welldef_D1 Join_welldef_D2) |
|
394 |
done |
|
395 |
||
396 |
lemma uv_refinement_thm: |
|
397 |
"[| strict_uv_prop X; |
|
398 |
\<forall>H. F ok H & G ok H & F Join H : welldef Int X --> |
|
399 |
G Join H : welldef |] |
|
400 |
==> (G refines F wrt X) = (G iso_refines F wrt X)" |
|
401 |
apply (rule_tac x = SKIP in allE, assumption) |
|
402 |
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) |
|
403 |
done |
|
404 |
||
405 |
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) |
|
406 |
lemma guarantees_equiv: |
|
407 |
"(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))" |
|
408 |
by (unfold guar_def component_of_def, auto) |
|
409 |
||
410 |
lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)" |
|
411 |
by (unfold wg_def, auto) |
|
412 |
||
413 |
lemma wg_guarantees: "F:((wg F Y) guarantees Y)" |
|
414 |
by (unfold wg_def guar_def, blast) |
|
415 |
||
416 |
lemma wg_equiv: |
|
417 |
"(H: wg F X) = (F component_of H --> H:X)" |
|
418 |
apply (unfold wg_def) |
|
419 |
apply (simp (no_asm) add: guarantees_equiv) |
|
420 |
apply (rule iffI) |
|
421 |
apply (rule_tac [2] x = "{H}" in exI) |
|
422 |
apply (blast+) |
|
423 |
done |
|
424 |
||
425 |
||
426 |
lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)" |
|
427 |
by (simp add: wg_equiv) |
|
428 |
||
429 |
lemma wg_finite: |
|
430 |
"\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) |
|
431 |
--> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))" |
|
432 |
apply clarify |
|
433 |
apply (subgoal_tac "F component_of (JN F:FF. F) ") |
|
434 |
apply (drule_tac X = X in component_of_wg, simp) |
|
435 |
apply (simp add: component_of_def) |
|
436 |
apply (rule_tac x = "JN F: (FF-{F}) . F" in exI) |
|
437 |
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) |
|
438 |
done |
|
439 |
||
440 |
lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)" |
|
441 |
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) |
|
442 |
apply blast |
|
443 |
done |
|
444 |
||
445 |
(** From Charpentier and Chandy "Theorems About Composition" **) |
|
446 |
(* Proposition 2 *) |
|
447 |
lemma wx_subset: "(wx X)<=X" |
|
448 |
by (unfold wx_def, auto) |
|
449 |
||
450 |
lemma wx_ex_prop: "ex_prop (wx X)" |
|
451 |
apply (unfold wx_def) |
|
452 |
apply (simp (no_asm) add: ex_prop_equiv) |
|
453 |
apply safe |
|
454 |
apply blast |
|
455 |
apply auto |
|
456 |
done |
|
457 |
||
458 |
lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X" |
|
459 |
by (unfold wx_def, auto) |
|
460 |
||
461 |
(* Proposition 6 *) |
|
462 |
lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})" |
|
463 |
apply (unfold ex_prop_def, safe) |
|
464 |
apply (drule_tac x = "G Join Ga" in spec) |
|
465 |
apply (force simp add: ok_Join_iff1 Join_assoc) |
|
466 |
apply (drule_tac x = "F Join Ga" in spec) |
|
467 |
apply (simp (no_asm_use) add: ok_Join_iff1) |
|
468 |
apply safe |
|
469 |
apply (simp (no_asm_simp) add: ok_commute) |
|
470 |
apply (subgoal_tac "F Join G = G Join F") |
|
471 |
apply (simp (no_asm_simp) add: Join_assoc) |
|
472 |
apply (simp (no_asm) add: Join_commute) |
|
473 |
done |
|
474 |
||
475 |
(* Equivalence with the other definition of wx *) |
|
476 |
||
477 |
lemma wx_equiv: |
|
478 |
"wx X = {F. \<forall>G. F ok G --> (F Join G):X}" |
|
479 |
||
480 |
apply (unfold wx_def, safe) |
|
481 |
apply (simp (no_asm_use) add: ex_prop_def) |
|
482 |
apply (drule_tac x = x in spec) |
|
483 |
apply (drule_tac x = G in spec) |
|
484 |
apply (frule_tac c = "x Join G" in subsetD, safe) |
|
485 |
apply (simp (no_asm)) |
|
486 |
apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe) |
|
487 |
apply (rule_tac [2] wx'_ex_prop) |
|
488 |
apply (rotate_tac 1) |
|
489 |
apply (drule_tac x = SKIP in spec, auto) |
|
490 |
done |
|
491 |
||
492 |
||
493 |
(* Propositions 7 to 11 are about this second definition of wx. And |
|
494 |
they are the same as the ones proved for the first definition of wx by equivalence *) |
|
495 |
||
496 |
(* Proposition 12 *) |
|
497 |
(* Main result of the paper *) |
|
498 |
lemma guarantees_wx_eq: |
|
499 |
"(X guarantees Y) = wx(-X Un Y)" |
|
500 |
apply (unfold guar_def) |
|
501 |
apply (simp (no_asm) add: wx_equiv) |
|
502 |
done |
|
503 |
||
504 |
(* {* Corollary, but this result has already been proved elsewhere *} |
|
505 |
"ex_prop(X guarantees Y)" |
|
506 |
by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); |
|
507 |
qed "guarantees_ex_prop"; |
|
508 |
*) |
|
509 |
||
510 |
(* Rules given in section 7 of Chandy and Sander's |
|
511 |
Reasoning About Program composition paper *) |
|
512 |
||
513 |
lemma stable_guarantees_Always: |
|
514 |
"Init F <= A ==> F:(stable A) guarantees (Always A)" |
|
515 |
apply (rule guaranteesI) |
|
516 |
apply (simp (no_asm) add: Join_commute) |
|
517 |
apply (rule stable_Join_Always1) |
|
518 |
apply (simp_all add: invariant_def Join_stable) |
|
519 |
done |
|
520 |
||
521 |
(* To be moved to WFair.ML *) |
|
522 |
lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B" |
|
523 |
apply (drule_tac B = "A-B" in constrains_weaken_L) |
|
524 |
apply (drule_tac [2] B = "A-B" in transient_strengthen) |
|
525 |
apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) |
|
526 |
apply (blast+) |
|
527 |
done |
|
528 |
||
529 |
||
530 |
||
531 |
lemma constrains_guarantees_leadsTo: |
|
532 |
"F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))" |
|
533 |
apply (rule guaranteesI) |
|
534 |
apply (rule leadsTo_Basis') |
|
535 |
apply (drule constrains_weaken_R) |
|
536 |
prefer 2 apply assumption |
|
537 |
apply blast |
|
538 |
apply (blast intro: Join_transient_I1) |
|
539 |
done |
|
540 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
541 |
end |