author | paulson |
Fri, 17 Sep 1999 10:31:38 +0200 | |
changeset 7538 | 357873391561 |
parent 7537 | 875754b599df |
child 7546 | 36b26759147e |
permissions | -rw-r--r-- |
6297 | 1 |
(* Title: HOL/UNITY/Extend.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Extending of state sets |
|
7 |
function f (forget) maps the extended state to the original state |
|
8 |
function g (forgotten) maps the extended state to the "extending part" |
|
7482 | 9 |
*) |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
10 |
|
7482 | 11 |
(** These we prove OUTSIDE the locale. **) |
12 |
||
7537 | 13 |
|
14 |
(****************UNITY.ML****************) |
|
15 |
Goalw [stable_def, constrains_def] "stable UNIV = UNIV"; |
|
16 |
by Auto_tac; |
|
17 |
qed "stable_UNIV"; |
|
18 |
Addsimps [stable_UNIV]; |
|
19 |
||
20 |
||
7482 | 21 |
(*Possibly easier than reasoning about "inv h"*) |
22 |
val [surj_h,prem] = |
|
23 |
Goalw [good_map_def] |
|
24 |
"[| surj h; !! x x' y y'. h(x,y) = h(x',y') ==> x=x' |] ==> good_map h"; |
|
25 |
by (safe_tac (claset() addSIs [surj_h])); |
|
26 |
by (rtac prem 1); |
|
27 |
by (stac (surjective_pairing RS sym) 1); |
|
28 |
by (stac (surj_h RS surj_f_inv_f) 1); |
|
29 |
by (rtac refl 1); |
|
30 |
qed "good_mapI"; |
|
31 |
||
32 |
Goalw [good_map_def] "good_map h ==> surj h"; |
|
33 |
by Auto_tac; |
|
34 |
qed "good_map_is_surj"; |
|
35 |
||
36 |
(*A convenient way of finding a closed form for inv h*) |
|
37 |
val [surj,prem] = Goalw [inv_def] |
|
38 |
"[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; |
|
39 |
by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); |
|
7499 | 40 |
by (rtac selectI2 1); |
7482 | 41 |
by (dres_inst_tac [("f", "g")] arg_cong 2); |
42 |
by (auto_tac (claset(), simpset() addsimps [prem])); |
|
43 |
qed "fst_inv_equalityI"; |
|
44 |
||
6297 | 45 |
|
46 |
Open_locale "Extend"; |
|
47 |
||
48 |
val slice_def = thm "slice_def"; |
|
49 |
||
50 |
(*** Trivial properties of f, g, h ***) |
|
51 |
||
7482 | 52 |
val good_h = rewrite_rule [good_map_def] (thm "good_h"); |
53 |
val surj_h = good_h RS conjunct1; |
|
6297 | 54 |
|
55 |
val f_def = thm "f_def"; |
|
56 |
val g_def = thm "g_def"; |
|
57 |
||
58 |
Goal "f(h(x,y)) = x"; |
|
7482 | 59 |
by (simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
6297 | 60 |
qed "f_h_eq"; |
61 |
Addsimps [f_h_eq]; |
|
62 |
||
7482 | 63 |
Goal "h(x,y) = h(x',y') ==> x=x'"; |
64 |
by (dres_inst_tac [("f", "fst o inv h")] arg_cong 1); |
|
65 |
(*FIXME: If locales worked properly we could put just "f" above*) |
|
66 |
by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1); |
|
67 |
qed "h_inject1"; |
|
68 |
AddSDs [h_inject1]; |
|
6297 | 69 |
|
70 |
Goal "h(f z, g z) = z"; |
|
7482 | 71 |
by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym, |
72 |
surj_h RS surj_f_inv_f]) 1); |
|
6297 | 73 |
qed "h_f_g_eq"; |
74 |
||
75 |
(*** extend_set: basic properties ***) |
|
76 |
||
77 |
Goalw [extend_set_def] |
|
7341 | 78 |
"z : extend_set h A = (f z : A)"; |
79 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
|
6297 | 80 |
qed "mem_extend_set_iff"; |
81 |
AddIffs [mem_extend_set_iff]; |
|
82 |
||
7378 | 83 |
Goal "{s. P (f s)} = extend_set h {s. P s}"; |
84 |
by Auto_tac; |
|
85 |
qed "Collect_eq_extend_set"; |
|
86 |
||
7537 | 87 |
Goalw [extend_set_def, project_set_def] |
88 |
"project_set h (extend_set h F) = F"; |
|
7341 | 89 |
by Auto_tac; |
90 |
qed "extend_set_inverse"; |
|
91 |
Addsimps [extend_set_inverse]; |
|
92 |
||
6297 | 93 |
Goal "inj (extend_set h)"; |
7341 | 94 |
by (rtac inj_on_inverseI 1); |
95 |
by (rtac extend_set_inverse 1); |
|
6297 | 96 |
qed "inj_extend_set"; |
97 |
||
7482 | 98 |
(*** project_set: basic properties ***) |
99 |
||
100 |
(*project_set is simply image!*) |
|
101 |
Goalw [project_set_def] "project_set h C = f `` C"; |
|
102 |
by (auto_tac (claset() addIs [f_h_eq RS sym, h_f_g_eq RS ssubst], |
|
103 |
simpset())); |
|
104 |
qed "project_set_eq"; |
|
105 |
||
106 |
(*Converse appears to fail*) |
|
107 |
Goalw [project_set_def] "z : C ==> f z : project_set h C"; |
|
108 |
by (auto_tac (claset() addIs [h_f_g_eq RS ssubst], |
|
109 |
simpset())); |
|
110 |
qed "project_set_I"; |
|
111 |
||
112 |
||
113 |
(*** More laws ***) |
|
114 |
||
7341 | 115 |
(*Because A and B could differ on the "other" part of the state, |
116 |
cannot generalize result to |
|
117 |
project_set h (A Int B) = project_set h A Int project_set h B |
|
118 |
*) |
|
119 |
Goalw [project_set_def] |
|
120 |
"project_set h ((extend_set h A) Int B) = A Int (project_set h B)"; |
|
121 |
by Auto_tac; |
|
122 |
qed "project_set_extend_set_Int"; |
|
123 |
||
124 |
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B"; |
|
6297 | 125 |
by Auto_tac; |
126 |
qed "extend_set_Un_distrib"; |
|
127 |
||
7341 | 128 |
Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B"; |
6297 | 129 |
by Auto_tac; |
130 |
qed "extend_set_Int_distrib"; |
|
131 |
||
7341 | 132 |
Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"; |
133 |
by Auto_tac; |
|
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
134 |
qed "extend_set_INT_distrib"; |
6647 | 135 |
|
7341 | 136 |
Goal "extend_set h (A - B) = extend_set h A - extend_set h B"; |
6297 | 137 |
by Auto_tac; |
138 |
qed "extend_set_Diff_distrib"; |
|
139 |
||
7341 | 140 |
Goal "extend_set h (Union A) = (UN X:A. extend_set h X)"; |
6297 | 141 |
by (Blast_tac 1); |
142 |
qed "extend_set_Union"; |
|
143 |
||
7341 | 144 |
Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)"; |
6297 | 145 |
by Auto_tac; |
146 |
qed "extend_set_subset_Compl_eq"; |
|
147 |
||
7341 | 148 |
|
6297 | 149 |
(*** extend_act ***) |
150 |
||
7341 | 151 |
(*Actions could affect the g-part, so result Cannot be strengthened to |
152 |
((z, z') : extend_act h act) = ((f z, f z') : act) |
|
153 |
*) |
|
6297 | 154 |
Goalw [extend_act_def] |
155 |
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"; |
|
156 |
by Auto_tac; |
|
157 |
qed "mem_extend_act_iff"; |
|
158 |
AddIffs [mem_extend_act_iff]; |
|
159 |
||
7341 | 160 |
Goalw [extend_act_def] |
161 |
"(z, z') : extend_act h act ==> (f z, f z') : act"; |
|
162 |
by Auto_tac; |
|
163 |
qed "extend_act_D"; |
|
164 |
||
7537 | 165 |
(*Premise is still undesirably strong, since Domain act can include |
166 |
non-reachable states, but it seems necessary for this result.*) |
|
167 |
Goalw [extend_act_def,project_set_def, project_act_def] |
|
168 |
"Domain act <= project_set h C ==> project_act C h (extend_act h act) = act"; |
|
169 |
by (Force_tac 1); |
|
7341 | 170 |
qed "extend_act_inverse"; |
171 |
Addsimps [extend_act_inverse]; |
|
172 |
||
6297 | 173 |
Goal "inj (extend_act h)"; |
7341 | 174 |
by (rtac inj_on_inverseI 1); |
175 |
by (rtac extend_act_inverse 1); |
|
7537 | 176 |
by (force_tac (claset(), simpset() addsimps [project_set_def]) 1); |
6297 | 177 |
qed "inj_extend_act"; |
178 |
||
179 |
Goalw [extend_set_def, extend_act_def] |
|
180 |
"extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)"; |
|
181 |
by (Force_tac 1); |
|
182 |
qed "extend_act_Image"; |
|
183 |
Addsimps [extend_act_Image]; |
|
184 |
||
185 |
Goalw [extend_set_def, extend_act_def] |
|
186 |
"(extend_set h A <= extend_set h B) = (A <= B)"; |
|
187 |
by (Force_tac 1); |
|
188 |
qed "extend_set_strict_mono"; |
|
189 |
Addsimps [extend_set_strict_mono]; |
|
190 |
||
191 |
Goalw [extend_set_def, extend_act_def] |
|
192 |
"Domain (extend_act h act) = extend_set h (Domain act)"; |
|
193 |
by (Force_tac 1); |
|
194 |
qed "Domain_extend_act"; |
|
195 |
||
7341 | 196 |
Goalw [extend_act_def] |
6297 | 197 |
"extend_act h Id = Id"; |
198 |
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1); |
|
199 |
qed "extend_act_Id"; |
|
7341 | 200 |
|
201 |
Goalw [project_act_def] |
|
7537 | 202 |
"[| (z, z') : act; f z = f z' | z: C |] \ |
203 |
\ ==> (f z, f z') : project_act C h act"; |
|
7341 | 204 |
by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst], |
205 |
simpset())); |
|
206 |
qed "project_act_I"; |
|
207 |
||
208 |
Goalw [project_set_def, project_act_def] |
|
7537 | 209 |
"project_act C h Id = Id"; |
7341 | 210 |
by (Force_tac 1); |
211 |
qed "project_act_Id"; |
|
212 |
||
7537 | 213 |
(*premise can be weakened*) |
7482 | 214 |
Goalw [project_set_def, project_act_def] |
7537 | 215 |
"Domain act <= C \ |
216 |
\ ==> Domain (project_act C h act) = project_set h (Domain act)"; |
|
7499 | 217 |
by Auto_tac; |
7482 | 218 |
by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1); |
7499 | 219 |
by Auto_tac; |
7482 | 220 |
qed "Domain_project_act"; |
221 |
||
7341 | 222 |
Addsimps [extend_act_Id, project_act_Id]; |
6297 | 223 |
|
224 |
Goal "Id : extend_act h `` Acts F"; |
|
225 |
by (auto_tac (claset() addSIs [extend_act_Id RS sym], |
|
226 |
simpset() addsimps [image_iff])); |
|
227 |
qed "Id_mem_extend_act"; |
|
228 |
||
229 |
||
230 |
(**** extend ****) |
|
231 |
||
232 |
(*** Basic properties ***) |
|
233 |
||
7341 | 234 |
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)"; |
6297 | 235 |
by Auto_tac; |
236 |
qed "Init_extend"; |
|
237 |
||
7537 | 238 |
Goalw [project_def] "Init (project C h F) = project_set h (Init F)"; |
7341 | 239 |
by Auto_tac; |
240 |
qed "Init_project"; |
|
241 |
||
6297 | 242 |
Goal "Acts (extend h F) = (extend_act h `` Acts F)"; |
243 |
by (auto_tac (claset() addSIs [extend_act_Id RS sym], |
|
244 |
simpset() addsimps [extend_def, image_iff])); |
|
245 |
qed "Acts_extend"; |
|
246 |
||
7537 | 247 |
Goal "Acts (project C h F) = (project_act C h `` Acts F)"; |
7341 | 248 |
by (auto_tac (claset() addSIs [project_act_Id RS sym], |
249 |
simpset() addsimps [project_def, image_iff])); |
|
250 |
qed "Acts_project"; |
|
251 |
||
252 |
Addsimps [Init_extend, Init_project, Acts_extend, Acts_project]; |
|
6297 | 253 |
|
254 |
Goalw [SKIP_def] "extend h SKIP = SKIP"; |
|
255 |
by (rtac program_equalityI 1); |
|
7341 | 256 |
by Auto_tac; |
257 |
qed "extend_SKIP"; |
|
258 |
||
7537 | 259 |
Goalw [SKIP_def] "project C h SKIP = SKIP"; |
7341 | 260 |
by (rtac program_equalityI 1); |
6297 | 261 |
by (auto_tac (claset() addIs [h_f_g_eq RS sym], |
7341 | 262 |
simpset() addsimps [project_set_def])); |
263 |
qed "project_SKIP"; |
|
264 |
||
7537 | 265 |
Goalw [project_set_def] "UNIV <= project_set h UNIV"; |
266 |
by Auto_tac; |
|
267 |
qed "project_set_UNIV"; |
|
268 |
||
269 |
(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*) |
|
270 |
Goal "UNIV <= project_set h C \ |
|
271 |
\ ==> project C h (extend h F) = F"; |
|
7341 | 272 |
by (simp_tac (simpset() addsimps [extend_def, project_def]) 1); |
273 |
by (rtac program_equalityI 1); |
|
7537 | 274 |
by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, |
275 |
subset_UNIV RS subset_trans RS extend_act_inverse]) 2); |
|
7341 | 276 |
by (Simp_tac 1); |
277 |
qed "extend_inverse"; |
|
278 |
Addsimps [extend_inverse]; |
|
6297 | 279 |
|
280 |
Goal "inj (extend h)"; |
|
7341 | 281 |
by (rtac inj_on_inverseI 1); |
282 |
by (rtac extend_inverse 1); |
|
7537 | 283 |
by (force_tac (claset(), simpset() addsimps [project_set_def]) 1); |
6297 | 284 |
qed "inj_extend"; |
285 |
||
286 |
Goal "extend h (F Join G) = extend h F Join extend h G"; |
|
287 |
by (rtac program_equalityI 1); |
|
7537 | 288 |
by (simp_tac (simpset() addsimps [image_Un]) 2); |
6297 | 289 |
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1); |
290 |
qed "extend_Join"; |
|
291 |
Addsimps [extend_Join]; |
|
292 |
||
6647 | 293 |
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))"; |
294 |
by (rtac program_equalityI 1); |
|
7537 | 295 |
by (simp_tac (simpset() addsimps [image_UN]) 2); |
6834
44da4a2a9ef3
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
paulson
parents:
6822
diff
changeset
|
296 |
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1); |
6647 | 297 |
qed "extend_JN"; |
298 |
Addsimps [extend_JN]; |
|
299 |
||
7537 | 300 |
Goal "UNIV <= project_set h C \ |
301 |
\ ==> project C h ((extend h F) Join G) = F Join (project C h G)"; |
|
7387 | 302 |
by (rtac program_equalityI 1); |
7537 | 303 |
by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, |
304 |
subset_UNIV RS subset_trans RS extend_act_inverse]) 2); |
|
7387 | 305 |
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1); |
306 |
qed "project_extend_Join"; |
|
307 |
||
7537 | 308 |
Goal "UNIV <= project_set h C \ |
309 |
\ ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)"; |
|
310 |
by (dres_inst_tac [("f", "project C h")] arg_cong 1); |
|
311 |
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1); |
|
7387 | 312 |
qed "extend_Join_eq_extend_D"; |
313 |
||
6297 | 314 |
|
6536 | 315 |
(*** Safety: co, stable ***) |
6297 | 316 |
|
6536 | 317 |
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \ |
318 |
\ (F : A co B)"; |
|
6297 | 319 |
by (simp_tac (simpset() addsimps [constrains_def]) 1); |
320 |
qed "extend_constrains"; |
|
321 |
||
322 |
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)"; |
|
323 |
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1); |
|
324 |
qed "extend_stable"; |
|
325 |
||
326 |
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)"; |
|
327 |
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1); |
|
328 |
qed "extend_invariant"; |
|
329 |
||
7341 | 330 |
(** Safety and project **) |
331 |
||
332 |
Goalw [constrains_def] |
|
7538 | 333 |
"(F Join project C h G : A co B) = \ |
334 |
\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ |
|
335 |
\ F : A co B)"; |
|
336 |
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un])); |
|
337 |
by (force_tac (claset() addIs [extend_act_D], simpset()) 1); |
|
338 |
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1); |
|
339 |
(*the <== direction*) |
|
340 |
by (ball_tac 1); |
|
7537 | 341 |
by (rewtac project_act_def); |
7538 | 342 |
by Auto_tac; |
7537 | 343 |
by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1); |
344 |
by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
|
7538 | 345 |
qed "Join_project_constrains"; |
7341 | 346 |
|
7537 | 347 |
(*The condition is required to prove the left-to-right direction; |
7538 | 348 |
could weaken it to G : (C Int extend_set h A) co C*) |
7537 | 349 |
Goalw [stable_def] |
7538 | 350 |
"extend h F Join G : stable C \ |
351 |
\ ==> (F Join project C h G : stable A) = \ |
|
352 |
\ (extend h F Join G : stable (C Int extend_set h A) & \ |
|
353 |
\ F : stable A)"; |
|
354 |
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
7537 | 355 |
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
7538 | 356 |
qed "Join_project_stable"; |
7341 | 357 |
|
7538 | 358 |
Goal "(F Join project UNIV h G : increasing func) = \ |
359 |
\ (extend h F Join G : increasing (func o f))"; |
|
360 |
by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1); |
|
361 |
by (auto_tac (claset(), |
|
362 |
simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
|
363 |
extend_stable RS iffD1])); |
|
364 |
||
365 |
qed "Join_project_increasing"; |
|
366 |
||
367 |
Goal "(project C h F : A co B) = \ |
|
368 |
\ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
|
369 |
by (cut_inst_tac [("F", "SKIP")] Join_project_constrains 1); |
|
370 |
by (asm_full_simp_tac (simpset() addsimps [extend_SKIP]) 1); |
|
371 |
qed "project_constrains"; |
|
7387 | 372 |
|
7341 | 373 |
|
374 |
(*** Diff, needed for localTo ***) |
|
375 |
||
7387 | 376 |
(** project versions **) |
377 |
||
378 |
(*Opposite direction fails because Diff in the extended state may remove |
|
379 |
fewer actions, i.e. those that affect other state variables.*) |
|
7537 | 380 |
Goal "(UN act:acts. Domain act) <= project_set h C \ |
381 |
\ ==> Diff (project C h G) acts <= \ |
|
382 |
\ project C h (Diff G (extend_act h `` acts))"; |
|
383 |
by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def, |
|
384 |
UN_subset_iff]) 1); |
|
385 |
by (force_tac (claset() addSIs [image_diff_subset RS subsetD], |
|
386 |
simpset() addsimps [image_image_eq_UN]) 1); |
|
7387 | 387 |
qed "Diff_project_component_project_Diff"; |
388 |
||
7537 | 389 |
Goal |
390 |
"[| (UN act:acts. Domain act) <= project_set h C; \ |
|
391 |
\ Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\ |
|
392 |
\ ==> Diff (project C h G) acts : A co B"; |
|
393 |
by (etac (Diff_project_component_project_Diff RS component_constrains) 1); |
|
394 |
by (rtac (project_constrains RS iffD2) 1); |
|
395 |
by (ftac constrains_imp_subset 1); |
|
396 |
by (Asm_full_simp_tac 1); |
|
397 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
7341 | 398 |
qed "Diff_project_co"; |
399 |
||
400 |
Goalw [stable_def] |
|
7537 | 401 |
"[| (UN act:acts. Domain act) <= project_set h C; \ |
402 |
\ Diff G (extend_act h `` acts) : stable (extend_set h A) |] \ |
|
403 |
\ ==> Diff (project C h G) acts : stable A"; |
|
7341 | 404 |
by (etac Diff_project_co 1); |
7537 | 405 |
by (assume_tac 1); |
7341 | 406 |
qed "Diff_project_stable"; |
407 |
||
7387 | 408 |
(** extend versions **) |
409 |
||
410 |
Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)"; |
|
411 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
412 |
simpset() addsimps [Diff_def, |
|
7537 | 413 |
inj_extend_act RS image_set_diff RS sym])); |
7387 | 414 |
qed "Diff_extend_eq"; |
415 |
||
416 |
Goal "(Diff (extend h G) (extend_act h `` acts) \ |
|
417 |
\ : (extend_set h A) co (extend_set h B)) \ |
|
418 |
\ = (Diff G acts : A co B)"; |
|
419 |
by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1); |
|
7341 | 420 |
qed "Diff_extend_co"; |
421 |
||
7387 | 422 |
Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \ |
423 |
\ = (Diff G acts : stable A)"; |
|
424 |
by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1); |
|
7341 | 425 |
qed "Diff_extend_stable"; |
426 |
||
7387 | 427 |
(*Converse appears to fail*) |
7537 | 428 |
Goal "[| UNIV <= project_set h C; (H : (func o f) localTo extend h G) |] \ |
429 |
\ ==> (project C h H : func localTo G)"; |
|
7387 | 430 |
by (asm_full_simp_tac |
431 |
(simpset() addsimps [localTo_def, |
|
432 |
project_extend_Join RS sym, |
|
7537 | 433 |
subset_UNIV RS subset_trans RS Diff_project_stable, |
7387 | 434 |
Collect_eq_extend_set RS sym]) 1); |
435 |
qed "project_localTo_I"; |
|
436 |
||
7341 | 437 |
|
438 |
(*** Weak safety primitives: Co, Stable ***) |
|
6297 | 439 |
|
440 |
Goal "p : reachable (extend h F) ==> f p : reachable F"; |
|
441 |
by (etac reachable.induct 1); |
|
442 |
by (auto_tac |
|
443 |
(claset() addIs reachable.intrs, |
|
7341 | 444 |
simpset() addsimps [extend_act_def, image_iff])); |
6297 | 445 |
qed "reachable_extend_f"; |
446 |
||
447 |
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F"; |
|
448 |
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1); |
|
449 |
qed "h_reachable_extend"; |
|
450 |
||
451 |
Goalw [extend_set_def] |
|
452 |
"reachable (extend h F) = extend_set h (reachable F)"; |
|
453 |
by (rtac equalityI 1); |
|
454 |
by (force_tac (claset() addIs [h_f_g_eq RS sym] |
|
455 |
addSDs [reachable_extend_f], |
|
456 |
simpset()) 1); |
|
457 |
by (Clarify_tac 1); |
|
458 |
by (etac reachable.induct 1); |
|
459 |
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, |
|
460 |
simpset()))); |
|
461 |
qed "reachable_extend_eq"; |
|
462 |
||
6536 | 463 |
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \ |
464 |
\ (F : A Co B)"; |
|
6297 | 465 |
by (simp_tac |
466 |
(simpset() addsimps [Constrains_def, reachable_extend_eq, |
|
467 |
extend_constrains, extend_set_Int_distrib RS sym]) 1); |
|
468 |
qed "extend_Constrains"; |
|
469 |
||
470 |
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)"; |
|
471 |
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1); |
|
472 |
qed "extend_Stable"; |
|
473 |
||
6647 | 474 |
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)"; |
475 |
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1); |
|
476 |
qed "extend_Always"; |
|
477 |
||
6297 | 478 |
|
7341 | 479 |
(** Reachability and project **) |
480 |
||
7538 | 481 |
Goal "[| reachable (extend h F Join G) <= C; \ |
482 |
\ z : reachable (extend h F Join G) |] \ |
|
483 |
\ ==> f z : reachable (F Join project C h G)"; |
|
7341 | 484 |
by (etac reachable.induct 1); |
7538 | 485 |
by (force_tac (claset() delrules [Id_in_Acts] |
486 |
addIs [reachable.Acts, project_act_I, extend_act_D], |
|
7341 | 487 |
simpset()) 2); |
488 |
by (force_tac (claset() addIs [reachable.Init, project_set_I], |
|
489 |
simpset()) 1); |
|
490 |
qed "reachable_imp_reachable_project"; |
|
491 |
||
492 |
Goalw [Constrains_def] |
|
7538 | 493 |
"[| reachable (extend h F Join G) <= C; \ |
494 |
\ F Join project C h G : A Co B |] \ |
|
495 |
\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
|
496 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
7537 | 497 |
by (Clarify_tac 1); |
7538 | 498 |
by (etac constrains_weaken 1); |
7341 | 499 |
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset())); |
500 |
qed "project_Constrains_D"; |
|
501 |
||
7537 | 502 |
Goalw [Stable_def] |
7538 | 503 |
"[| reachable (extend h F Join G) <= C; \ |
504 |
\ F Join project C h G : Stable A |] \ |
|
505 |
\ ==> extend h F Join G : Stable (extend_set h A)"; |
|
7341 | 506 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
507 |
qed "project_Stable_D"; |
|
508 |
||
7537 | 509 |
Goalw [Always_def] |
7538 | 510 |
"[| reachable (extend h F Join G) <= C; \ |
511 |
\ F Join project C h G : Always A |] \ |
|
512 |
\ ==> extend h F Join G : Always (extend_set h A)"; |
|
7378 | 513 |
by (force_tac (claset() addIs [reachable.Init, project_set_I], |
514 |
simpset() addsimps [project_Stable_D]) 1); |
|
515 |
qed "project_Always_D"; |
|
516 |
||
517 |
Goalw [Increasing_def] |
|
7538 | 518 |
"[| reachable (extend h F Join G) <= C; \ |
519 |
\ F Join project C h G : Increasing func |] \ |
|
520 |
\ ==> extend h F Join G : Increasing (func o f)"; |
|
7378 | 521 |
by Auto_tac; |
522 |
by (stac Collect_eq_extend_set 1); |
|
523 |
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
|
524 |
qed "project_Increasing_D"; |
|
525 |
||
7537 | 526 |
|
527 |
(** Converse results for weak safety: benefits of the argument C *) |
|
528 |
||
7538 | 529 |
Goal "[| C <= reachable(extend h F Join G); \ |
530 |
\ x : reachable (F Join project C h G) |] \ |
|
531 |
\ ==> EX y. h(x,y) : reachable (extend h F Join G)"; |
|
7537 | 532 |
by (etac reachable.induct 1); |
7538 | 533 |
by (ALLGOALS Asm_full_simp_tac); |
534 |
(*SLOW: 6.7s*) |
|
535 |
by (force_tac (claset() delrules [Id_in_Acts] |
|
536 |
addIs [reachable.Acts, extend_act_D], |
|
7537 | 537 |
simpset() addsimps [project_act_def]) 2); |
538 |
by (force_tac (claset() addIs [reachable.Init], |
|
539 |
simpset() addsimps [project_set_def]) 1); |
|
540 |
qed "reachable_project_imp_reachable"; |
|
541 |
||
542 |
Goalw [Constrains_def] |
|
7538 | 543 |
"[| C <= reachable (extend h F Join G); \ |
544 |
\ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \ |
|
545 |
\ ==> F Join project C h G : A Co B"; |
|
546 |
by (full_simp_tac (simpset() addsimps [Join_project_constrains, |
|
7537 | 547 |
extend_set_Int_distrib]) 1); |
548 |
by (rtac conjI 1); |
|
549 |
by (etac constrains_weaken 1); |
|
550 |
by Auto_tac; |
|
7538 | 551 |
by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1); |
552 |
(*Some generalization of constrains_weaken_L would be better, but what is it?*) |
|
553 |
by (rewtac constrains_def); |
|
554 |
by Auto_tac; |
|
555 |
by (thin_tac "ALL act : Acts G. ?P act" 1); |
|
556 |
by (force_tac (claset() addSDs [reachable_project_imp_reachable], |
|
557 |
simpset()) 1); |
|
7537 | 558 |
qed "project_Constrains_I"; |
559 |
||
560 |
Goalw [Stable_def] |
|
7538 | 561 |
"[| C <= reachable (extend h F Join G); \ |
562 |
\ extend h F Join G : Stable (extend_set h A) |] \ |
|
563 |
\ ==> F Join project C h G : Stable A"; |
|
7537 | 564 |
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
565 |
qed "project_Stable_I"; |
|
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
566 |
|
7537 | 567 |
Goalw [Increasing_def] |
7538 | 568 |
"[| C <= reachable (extend h F Join G); \ |
569 |
\ extend h F Join G : Increasing (func o f) |] \ |
|
570 |
\ ==> F Join project C h G : Increasing func"; |
|
7537 | 571 |
by Auto_tac; |
572 |
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym, |
|
573 |
project_Stable_I]) 1); |
|
574 |
qed "project_Increasing_I"; |
|
575 |
||
7538 | 576 |
Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B) = \ |
577 |
\ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; |
|
7537 | 578 |
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
579 |
qed "project_Constrains"; |
|
580 |
||
581 |
Goalw [Stable_def] |
|
7538 | 582 |
"(F Join project (reachable (extend h F Join G)) h G : Stable A) = \ |
583 |
\ (extend h F Join G : Stable (extend_set h A))"; |
|
7537 | 584 |
by (rtac project_Constrains 1); |
585 |
qed "project_Stable"; |
|
586 |
||
7538 | 587 |
Goal |
588 |
"(F Join project (reachable (extend h F Join G)) h G : Increasing func) = \ |
|
589 |
\ (extend h F Join G : Increasing (func o f))"; |
|
7537 | 590 |
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
591 |
Collect_eq_extend_set RS sym]) 1); |
|
592 |
qed "project_Increasing"; |
|
593 |
||
7341 | 594 |
|
6297 | 595 |
(*** Progress: transient, ensures ***) |
596 |
||
597 |
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)"; |
|
598 |
by (auto_tac (claset(), |
|
599 |
simpset() addsimps [transient_def, extend_set_subset_Compl_eq, |
|
600 |
Domain_extend_act])); |
|
601 |
qed "extend_transient"; |
|
602 |
||
6536 | 603 |
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \ |
604 |
\ (F : A ensures B)"; |
|
6297 | 605 |
by (simp_tac |
606 |
(simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
607 |
extend_set_Un_distrib RS sym, |
|
608 |
extend_set_Diff_distrib RS sym]) 1); |
|
609 |
qed "extend_ensures"; |
|
610 |
||
6536 | 611 |
Goal "F : A leadsTo B \ |
612 |
\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"; |
|
6297 | 613 |
by (etac leadsTo_induct 1); |
614 |
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3); |
|
615 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
616 |
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1); |
|
617 |
qed "leadsTo_imp_extend_leadsTo"; |
|
618 |
||
619 |
(*** Proving the converse takes some doing! ***) |
|
620 |
||
621 |
Goalw [slice_def] "slice (Union S) y = (UN x:S. slice x y)"; |
|
622 |
by Auto_tac; |
|
623 |
qed "slice_Union"; |
|
624 |
||
625 |
Goalw [slice_def] "slice (extend_set h A) y = A"; |
|
626 |
by Auto_tac; |
|
627 |
qed "slice_extend_set"; |
|
628 |
||
7482 | 629 |
Goalw [slice_def, project_set_def] "project_set h A = (UN y. slice A y)"; |
6297 | 630 |
by Auto_tac; |
7482 | 631 |
qed "project_set_is_UN_slice"; |
6297 | 632 |
|
633 |
Goalw [slice_def, transient_def] |
|
634 |
"extend h F : transient A ==> F : transient (slice A y)"; |
|
635 |
by Auto_tac; |
|
636 |
by (rtac bexI 1); |
|
637 |
by Auto_tac; |
|
638 |
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1); |
|
639 |
qed "extend_transient_slice"; |
|
640 |
||
7482 | 641 |
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"; |
6297 | 642 |
by (full_simp_tac |
643 |
(simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
7482 | 644 |
project_set_eq, image_Un RS sym, |
6297 | 645 |
extend_set_Un_distrib RS sym, |
646 |
extend_set_Diff_distrib RS sym]) 1); |
|
647 |
by Safe_tac; |
|
648 |
by (full_simp_tac (simpset() addsimps [constrains_def, extend_act_def, |
|
649 |
extend_set_def]) 1); |
|
650 |
by (Clarify_tac 1); |
|
651 |
by (ball_tac 1); |
|
652 |
by (full_simp_tac (simpset() addsimps [slice_def, image_iff, Image_iff]) 1); |
|
653 |
by (force_tac (claset() addSIs [h_f_g_eq RS sym], simpset()) 1); |
|
654 |
(*transient*) |
|
655 |
by (dtac extend_transient_slice 1); |
|
656 |
by (etac transient_strengthen 1); |
|
657 |
by (force_tac (claset() addIs [f_h_eq RS sym], |
|
658 |
simpset() addsimps [slice_def]) 1); |
|
659 |
qed "extend_ensures_slice"; |
|
660 |
||
7482 | 661 |
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"; |
662 |
by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1); |
|
6297 | 663 |
by (blast_tac (claset() addIs [leadsTo_UN]) 1); |
664 |
qed "leadsTo_slice_image"; |
|
665 |
||
666 |
||
6536 | 667 |
Goal "extend h F : AU leadsTo BU \ |
7482 | 668 |
\ ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"; |
6297 | 669 |
by (etac leadsTo_induct 1); |
670 |
by (full_simp_tac (simpset() addsimps [slice_Union]) 3); |
|
671 |
by (blast_tac (claset() addIs [leadsTo_UN]) 3); |
|
672 |
by (blast_tac (claset() addIs [leadsTo_slice_image, leadsTo_Trans]) 2); |
|
673 |
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1); |
|
674 |
qed_spec_mp "extend_leadsTo_slice"; |
|
675 |
||
6536 | 676 |
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \ |
677 |
\ (F : A leadsTo B)"; |
|
6297 | 678 |
by Safe_tac; |
679 |
by (etac leadsTo_imp_extend_leadsTo 2); |
|
680 |
by (dtac extend_leadsTo_slice 1); |
|
681 |
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1); |
|
6647 | 682 |
qed "extend_leadsto"; |
6297 | 683 |
|
6536 | 684 |
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \ |
685 |
\ (F : A LeadsTo B)"; |
|
6454 | 686 |
by (simp_tac |
687 |
(simpset() addsimps [LeadsTo_def, reachable_extend_eq, |
|
6647 | 688 |
extend_leadsto, extend_set_Int_distrib RS sym]) 1); |
6454 | 689 |
qed "extend_LeadsTo"; |
690 |
||
6297 | 691 |
|
7341 | 692 |
(** Strong precondition and postcondition; doesn't seem very useful. **) |
693 |
||
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
694 |
Goal "F : X guarantees Y ==> \ |
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
695 |
\ extend h F : (extend h `` X) guarantees (extend h `` Y)"; |
6297 | 696 |
by (rtac guaranteesI 1); |
697 |
by Auto_tac; |
|
7537 | 698 |
by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, |
699 |
guaranteesD]) 1); |
|
6297 | 700 |
qed "guarantees_imp_extend_guarantees"; |
701 |
||
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
702 |
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \ |
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
703 |
\ ==> F : X guarantees Y"; |
6297 | 704 |
by (rtac guaranteesI 1); |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
705 |
by (auto_tac (claset(), simpset() addsimps [guar_def, component_def])); |
6297 | 706 |
by (dtac spec 1); |
707 |
by (dtac (mp RS mp) 1); |
|
708 |
by (Blast_tac 2); |
|
709 |
by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2); |
|
710 |
by Auto_tac; |
|
711 |
qed "extend_guarantees_imp_guarantees"; |
|
712 |
||
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
713 |
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \ |
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
714 |
\ (F : X guarantees Y)"; |
6297 | 715 |
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
716 |
extend_guarantees_imp_guarantees]) 1); |
|
717 |
qed "extend_guarantees_eq"; |
|
718 |
||
7341 | 719 |
(*Weak precondition and postcondition; this is the good one! |
7537 | 720 |
Not clear that it has a converse [or that we want one!] |
721 |
Can generalize project (C G) to the function variable "proj"*) |
|
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
722 |
val [xguary,project,extend] = |
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
723 |
Goal "[| F : X guarantees Y; \ |
7537 | 724 |
\ !!G. extend h F Join G : X' ==> F Join project (C G) h G : X; \ |
725 |
\ !!G. F Join project (C G) h G : Y ==> extend h F Join G : Y' |] \ |
|
7482 | 726 |
\ ==> extend h F : X' guarantees Y'"; |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
727 |
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1); |
7378 | 728 |
by (etac project 1); |
7341 | 729 |
qed "project_guarantees"; |
730 |
||
731 |
(** It seems that neither "guarantees" law can be proved from the other. **) |
|
732 |
||
733 |
||
734 |
(*** guarantees corollaries ***) |
|
735 |
||
7387 | 736 |
Goal "F : UNIV guarantees increasing func \ |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
737 |
\ ==> extend h F : UNIV guarantees increasing (func o f)"; |
7341 | 738 |
by (etac project_guarantees 1); |
7538 | 739 |
by (ALLGOALS |
740 |
(asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]))); |
|
7341 | 741 |
qed "extend_guar_increasing"; |
742 |
||
7387 | 743 |
Goal "F : UNIV guarantees Increasing func \ |
7362
f08fade5ea0d
new laws; changed "guar" back to "guarantees" (sorry)
paulson
parents:
7341
diff
changeset
|
744 |
\ ==> extend h F : UNIV guarantees Increasing (func o f)"; |
7341 | 745 |
by (etac project_guarantees 1); |
7537 | 746 |
by (rtac (subset_UNIV RS project_Increasing_D) 2); |
7341 | 747 |
by Auto_tac; |
748 |
qed "extend_guar_Increasing"; |
|
749 |
||
7387 | 750 |
Goal "F : (func localTo G) guarantees increasing func \ |
751 |
\ ==> extend h F : (func o f) localTo (extend h G) \ |
|
752 |
\ guarantees increasing (func o f)"; |
|
7341 | 753 |
by (etac project_guarantees 1); |
754 |
(*the "increasing" guarantee*) |
|
7387 | 755 |
by (asm_simp_tac |
7538 | 756 |
(simpset() addsimps [Join_project_increasing RS sym]) 2); |
7341 | 757 |
(*the "localTo" requirement*) |
7537 | 758 |
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
7387 | 759 |
by (asm_simp_tac |
7537 | 760 |
(simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
7341 | 761 |
qed "extend_localTo_guar_increasing"; |
762 |
||
7387 | 763 |
Goal "F : (func localTo G) guarantees Increasing func \ |
764 |
\ ==> extend h F : (func o f) localTo (extend h G) \ |
|
765 |
\ guarantees Increasing (func o f)"; |
|
7341 | 766 |
by (etac project_guarantees 1); |
767 |
(*the "Increasing" guarantee*) |
|
7538 | 768 |
by (etac (subset_UNIV RS project_Increasing_D) 2); |
7341 | 769 |
(*the "localTo" requirement*) |
7537 | 770 |
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
7387 | 771 |
by (asm_simp_tac |
7537 | 772 |
(simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
7341 | 773 |
qed "extend_localTo_guar_Increasing"; |
774 |
||
6297 | 775 |
Close_locale "Extend"; |
7482 | 776 |
|
777 |
(*Close_locale should do this! |
|
778 |
Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_inverse, |
|
779 |
extend_act_Image]; |
|
780 |
Delrules [make_elim h_inject1]; |
|
781 |
*) |