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