|
1 (* Title: HOL/UNITY/Project.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1999 University of Cambridge |
|
5 |
|
6 Projections of state sets (also of actions and programs) |
|
7 |
|
8 Inheritance of GUARANTEES properties under extension |
|
9 *) |
|
10 |
|
11 Open_locale "Extend"; |
|
12 |
|
13 Goalw [restr_def] "Init (restr C h F) = Init F"; |
|
14 by Auto_tac; |
|
15 qed "Init_restr"; |
|
16 |
|
17 Goalw [restr_act_def, extend_act_def, project_act_def] |
|
18 "((x,x') : restr_act C h act) = ((x,x') : act & (EX y. h(x,y) : C))"; |
|
19 by (Blast_tac 1); |
|
20 qed "restr_act_iff"; |
|
21 Addsimps [restr_act_iff]; |
|
22 |
|
23 Goal "Acts (restr C h F) = insert Id (restr_act C h `` Acts F)"; |
|
24 by (auto_tac (claset(), |
|
25 simpset() addsimps [restr_def, symmetric restr_act_def, |
|
26 image_image_eq_UN])); |
|
27 qed "Acts_restr"; |
|
28 |
|
29 Addsimps [Init_restr, Acts_restr]; |
|
30 |
|
31 (*The definitions are RE-ORIENTED*) |
|
32 Addsimps [symmetric restr_act_def, symmetric restr_def]; |
|
33 |
|
34 Goal "project C h ((extend h F) Join G) = (restr C h F) Join (project C h G)"; |
|
35 by (rtac program_equalityI 1); |
|
36 by (asm_simp_tac (simpset() addsimps [symmetric restr_act_def, |
|
37 image_Un, image_image]) 2); |
|
38 by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1); |
|
39 qed "project_extend_Join_restr"; |
|
40 |
|
41 Goalw [project_set_def] |
|
42 "Domain act <= project_set h C ==> restr_act C h act = act"; |
|
43 by (Force_tac 1); |
|
44 qed "restr_act_ident"; |
|
45 Addsimps [restr_act_ident]; |
|
46 |
|
47 Goal "F : A co B ==> restr C h F : A co B"; |
|
48 by (auto_tac (claset(), simpset() addsimps [constrains_def])); |
|
49 by (Blast_tac 1); |
|
50 qed "restr_constrains"; |
|
51 |
|
52 Goal "F : stable A ==> restr C h F : stable A"; |
|
53 by (asm_full_simp_tac (simpset() addsimps [stable_def, restr_constrains]) 1); |
|
54 qed "restr_stable"; |
|
55 |
|
56 Goal "UNIV <= project_set h C ==> restr C h F = F"; |
|
57 by (rtac program_equalityI 1); |
|
58 by (force_tac (claset(), |
|
59 simpset() addsimps [image_def, |
|
60 subset_UNIV RS subset_trans RS restr_act_ident]) 2); |
|
61 by (Simp_tac 1); |
|
62 qed "restr_ident"; |
|
63 |
|
64 (*Ideally, uses of this should be eliminated. But often we see it re-oriented |
|
65 as project_extend_Join RS sym*) |
|
66 Goal "UNIV <= project_set h C \ |
|
67 \ ==> project C h ((extend h F) Join G) = F Join (project C h G)"; |
|
68 by (asm_simp_tac (simpset() addsimps [project_extend_Join_restr, |
|
69 restr_ident]) 1); |
|
70 qed "project_extend_Join"; |
|
71 |
|
72 Goal "UNIV <= project_set h C \ |
|
73 \ ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)"; |
|
74 by (dres_inst_tac [("f", "project C h")] arg_cong 1); |
|
75 by (asm_full_simp_tac (simpset() addsimps [project_extend_Join_restr, |
|
76 restr_ident]) 1); |
|
77 qed "extend_Join_eq_extend_D"; |
|
78 |
|
79 |
|
80 (** Safety **) |
|
81 |
|
82 Goalw [constrains_def] |
|
83 "(project C h F : A co B) = \ |
|
84 \ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"; |
|
85 by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un])); |
|
86 by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1); |
|
87 (*the <== direction*) |
|
88 by (rewtac project_act_def); |
|
89 by (force_tac (claset() addSDs [subsetD], simpset()) 1); |
|
90 qed "project_constrains"; |
|
91 |
|
92 Goalw [stable_def] |
|
93 "(project UNIV h F : stable A) = (F : stable (extend_set h A))"; |
|
94 by (simp_tac (simpset() addsimps [project_constrains]) 1); |
|
95 qed "project_stable"; |
|
96 |
|
97 (*This form's useful with guarantees reasoning*) |
|
98 Goal "(F Join project C h G : A co B) = \ |
|
99 \ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \ |
|
100 \ F : A co B)"; |
|
101 by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1); |
|
102 by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken] |
|
103 addDs [constrains_imp_subset]) 1); |
|
104 qed "Join_project_constrains"; |
|
105 |
|
106 (*The condition is required to prove the left-to-right direction; |
|
107 could weaken it to G : (C Int extend_set h A) co C*) |
|
108 Goalw [stable_def] |
|
109 "extend h F Join G : stable C \ |
|
110 \ ==> (F Join project C h G : stable A) = \ |
|
111 \ (extend h F Join G : stable (C Int extend_set h A) & \ |
|
112 \ F : stable A)"; |
|
113 by (simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
114 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1); |
|
115 qed "Join_project_stable"; |
|
116 |
|
117 Goal "(F Join project UNIV h G : increasing func) = \ |
|
118 \ (extend h F Join G : increasing (func o f))"; |
|
119 by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1); |
|
120 by (auto_tac (claset(), |
|
121 simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym, |
|
122 extend_stable RS iffD1])); |
|
123 qed "Join_project_increasing"; |
|
124 |
|
125 |
|
126 (*** Diff, needed for localTo ***) |
|
127 |
|
128 (*Opposite direction fails because Diff in the extended state may remove |
|
129 fewer actions, i.e. those that affect other state variables.*) |
|
130 Goal "(UN act:acts. Domain act) <= project_set h C \ |
|
131 \ ==> Diff (project C h G) acts <= \ |
|
132 \ project C h (Diff G (extend_act h `` acts))"; |
|
133 by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def, |
|
134 UN_subset_iff]) 1); |
|
135 by (force_tac (claset() addSIs [image_diff_subset RS subsetD], |
|
136 simpset() addsimps [image_image_eq_UN]) 1); |
|
137 qed "Diff_project_component_project_Diff"; |
|
138 |
|
139 Goal |
|
140 "[| (UN act:acts. Domain act) <= project_set h C; \ |
|
141 \ Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\ |
|
142 \ ==> Diff (project C h G) acts : A co B"; |
|
143 by (etac (Diff_project_component_project_Diff RS component_constrains) 1); |
|
144 by (rtac (project_constrains RS iffD2) 1); |
|
145 by (ftac constrains_imp_subset 1); |
|
146 by (Asm_full_simp_tac 1); |
|
147 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
148 qed "Diff_project_co"; |
|
149 |
|
150 Goalw [stable_def] |
|
151 "[| (UN act:acts. Domain act) <= project_set h C; \ |
|
152 \ Diff G (extend_act h `` acts) : stable (extend_set h A) |] \ |
|
153 \ ==> Diff (project C h G) acts : stable A"; |
|
154 by (etac Diff_project_co 1); |
|
155 by (assume_tac 1); |
|
156 qed "Diff_project_stable"; |
|
157 |
|
158 (*Converse appears to fail*) |
|
159 Goal "[| UNIV <= project_set h C; (H : (func o f) localTo extend h G) |] \ |
|
160 \ ==> (project C h H : func localTo G)"; |
|
161 by (asm_full_simp_tac |
|
162 (simpset() addsimps [localTo_def, |
|
163 project_extend_Join RS sym, |
|
164 subset_UNIV RS subset_trans RS Diff_project_stable, |
|
165 Collect_eq_extend_set RS sym]) 1); |
|
166 qed "project_localTo_I"; |
|
167 |
|
168 |
|
169 (** Reachability and project **) |
|
170 |
|
171 Goal "[| reachable (extend h F Join G) <= C; \ |
|
172 \ z : reachable (extend h F Join G) |] \ |
|
173 \ ==> f z : reachable (F Join project C h G)"; |
|
174 by (etac reachable.induct 1); |
|
175 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
|
176 simpset()) 1); |
|
177 by Auto_tac; |
|
178 by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)], |
|
179 simpset()) 2); |
|
180 by (res_inst_tac [("act","x")] reachable.Acts 1); |
|
181 by Auto_tac; |
|
182 by (etac extend_act_D 1); |
|
183 qed "reachable_imp_reachable_project"; |
|
184 |
|
185 Goalw [Constrains_def] |
|
186 "[| reachable (extend h F Join G) <= C; \ |
|
187 \ F Join project C h G : A Co B |] \ |
|
188 \ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"; |
|
189 by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1); |
|
190 by (Clarify_tac 1); |
|
191 by (etac constrains_weaken 1); |
|
192 by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset())); |
|
193 qed "project_Constrains_D"; |
|
194 |
|
195 Goalw [Stable_def] |
|
196 "[| reachable (extend h F Join G) <= C; \ |
|
197 \ F Join project C h G : Stable A |] \ |
|
198 \ ==> extend h F Join G : Stable (extend_set h A)"; |
|
199 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1); |
|
200 qed "project_Stable_D"; |
|
201 |
|
202 Goalw [Always_def] |
|
203 "[| reachable (extend h F Join G) <= C; \ |
|
204 \ F Join project C h G : Always A |] \ |
|
205 \ ==> extend h F Join G : Always (extend_set h A)"; |
|
206 by (force_tac (claset() addIs [reachable.Init, project_set_I], |
|
207 simpset() addsimps [project_Stable_D]) 1); |
|
208 qed "project_Always_D"; |
|
209 |
|
210 Goalw [Increasing_def] |
|
211 "[| reachable (extend h F Join G) <= C; \ |
|
212 \ F Join project C h G : Increasing func |] \ |
|
213 \ ==> extend h F Join G : Increasing (func o f)"; |
|
214 by Auto_tac; |
|
215 by (stac Collect_eq_extend_set 1); |
|
216 by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); |
|
217 qed "project_Increasing_D"; |
|
218 |
|
219 |
|
220 (** Converse results for weak safety: benefits of the argument C *) |
|
221 |
|
222 Goal "[| C <= reachable(extend h F Join G); \ |
|
223 \ x : reachable (F Join project C h G) |] \ |
|
224 \ ==> EX y. h(x,y) : reachable (extend h F Join G)"; |
|
225 by (etac reachable.induct 1); |
|
226 by (ALLGOALS Asm_full_simp_tac); |
|
227 (*SLOW: 6.7s*) |
|
228 by (force_tac (claset() delrules [Id_in_Acts] |
|
229 addIs [reachable.Acts, extend_act_D], |
|
230 simpset() addsimps [project_act_def]) 2); |
|
231 by (force_tac (claset() addIs [reachable.Init], |
|
232 simpset() addsimps [project_set_def]) 1); |
|
233 qed "reachable_project_imp_reachable"; |
|
234 |
|
235 Goalw [Constrains_def] |
|
236 "[| C <= reachable (extend h F Join G); \ |
|
237 \ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \ |
|
238 \ ==> F Join project C h G : A Co B"; |
|
239 by (full_simp_tac (simpset() addsimps [Join_project_constrains, |
|
240 extend_set_Int_distrib]) 1); |
|
241 by (rtac conjI 1); |
|
242 by (etac constrains_weaken 1); |
|
243 by Auto_tac; |
|
244 by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1); |
|
245 (*Some generalization of constrains_weaken_L would be better, but what is it?*) |
|
246 by (rewtac constrains_def); |
|
247 by Auto_tac; |
|
248 by (thin_tac "ALL act : Acts G. ?P act" 1); |
|
249 by (force_tac (claset() addSDs [reachable_project_imp_reachable], |
|
250 simpset()) 1); |
|
251 qed "project_Constrains_I"; |
|
252 |
|
253 Goalw [Stable_def] |
|
254 "[| C <= reachable (extend h F Join G); \ |
|
255 \ extend h F Join G : Stable (extend_set h A) |] \ |
|
256 \ ==> F Join project C h G : Stable A"; |
|
257 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1); |
|
258 qed "project_Stable_I"; |
|
259 |
|
260 Goalw [Increasing_def] |
|
261 "[| C <= reachable (extend h F Join G); \ |
|
262 \ extend h F Join G : Increasing (func o f) |] \ |
|
263 \ ==> F Join project C h G : Increasing func"; |
|
264 by Auto_tac; |
|
265 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym, |
|
266 project_Stable_I]) 1); |
|
267 qed "project_Increasing_I"; |
|
268 |
|
269 Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B) = \ |
|
270 \ (extend h F Join G : (extend_set h A) Co (extend_set h B))"; |
|
271 by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1); |
|
272 qed "project_Constrains"; |
|
273 |
|
274 Goalw [Stable_def] |
|
275 "(F Join project (reachable (extend h F Join G)) h G : Stable A) = \ |
|
276 \ (extend h F Join G : Stable (extend_set h A))"; |
|
277 by (rtac project_Constrains 1); |
|
278 qed "project_Stable"; |
|
279 |
|
280 Goal |
|
281 "(F Join project (reachable (extend h F Join G)) h G : Increasing func) = \ |
|
282 \ (extend h F Join G : Increasing (func o f))"; |
|
283 by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable, |
|
284 Collect_eq_extend_set RS sym]) 1); |
|
285 qed "project_Increasing"; |
|
286 |
|
287 |
|
288 (** Progress includes safety in the definition of ensures **) |
|
289 |
|
290 (*** Progress for (project C h F) ***) |
|
291 |
|
292 (** transient **) |
|
293 |
|
294 (*Premise is that C includes the domains of all actions that could be the |
|
295 transient one. Could have C=UNIV of course*) |
|
296 Goalw [transient_def] |
|
297 "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \ |
|
298 \ Domain act <= C; \ |
|
299 \ F : transient (extend_set h A) |] \ |
|
300 \ ==> project C h F : transient A"; |
|
301 by (auto_tac (claset() delrules [ballE], |
|
302 simpset() addsimps [Domain_project_act, Int_absorb2])); |
|
303 by (REPEAT (ball_tac 1)); |
|
304 by (auto_tac (claset(), |
|
305 simpset() addsimps [extend_set_def, project_set_def, |
|
306 project_act_def])); |
|
307 by (ALLGOALS Blast_tac); |
|
308 qed "transient_extend_set_imp_project_transient"; |
|
309 |
|
310 |
|
311 (*UNUSED. WHY?? |
|
312 Converse of the above...it requires a strong assumption about actions |
|
313 being enabled for all possible values of the new variables.*) |
|
314 Goalw [transient_def] |
|
315 "[| project C h F : transient A; \ |
|
316 \ ALL act: Acts F. project_act C h act ^^ A <= - A --> \ |
|
317 \ Domain act <= C \ |
|
318 \ & extend_set h (project_set h (Domain act)) <= Domain act |] \ |
|
319 \ ==> F : transient (extend_set h A)"; |
|
320 by (auto_tac (claset() delrules [ballE], |
|
321 simpset() addsimps [Domain_project_act])); |
|
322 by (ball_tac 1); |
|
323 by (rtac bexI 1); |
|
324 by (assume_tac 2); |
|
325 by Auto_tac; |
|
326 by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1); |
|
327 by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1); |
|
328 (*The Domain requirement's proved; must prove the Image requirement*) |
|
329 by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1); |
|
330 by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1); |
|
331 by Auto_tac; |
|
332 by (thin_tac "A <= ?B" 1); |
|
333 by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1); |
|
334 qed "project_transient_imp_transient_extend_set"; |
|
335 |
|
336 |
|
337 (** ensures **) |
|
338 |
|
339 (*For simplicity, the complicated condition on C is eliminated |
|
340 NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*) |
|
341 Goal "F : (extend_set h A) ensures (extend_set h B) \ |
|
342 \ ==> project UNIV h F : A ensures B"; |
|
343 by (asm_full_simp_tac |
|
344 (simpset() addsimps [ensures_def, project_constrains, |
|
345 transient_extend_set_imp_project_transient, |
|
346 extend_set_Un_distrib RS sym, |
|
347 extend_set_Diff_distrib RS sym]) 1); |
|
348 by (Blast_tac 1); |
|
349 qed "ensures_extend_set_imp_project_ensures"; |
|
350 |
|
351 (*A super-strong condition: G is not allowed to affect the |
|
352 shared variables at all.*) |
|
353 Goal "[| ALL x. project UNIV h G ~: transient {x}; \ |
|
354 \ F Join project UNIV h G : A ensures B |] \ |
|
355 \ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"; |
|
356 by (case_tac "A <= B" 1); |
|
357 by (etac (extend_set_mono RS subset_imp_ensures) 1); |
|
358 by (asm_full_simp_tac |
|
359 (simpset() addsimps [ensures_def, extend_constrains, extend_transient, |
|
360 extend_set_Un_distrib RS sym, |
|
361 extend_set_Diff_distrib RS sym, |
|
362 Join_transient, Join_constrains, |
|
363 project_constrains, Int_absorb1]) 1); |
|
364 by (blast_tac (claset() addIs [transient_strengthen]) 1); |
|
365 qed_spec_mp "Join_project_ensures"; |
|
366 |
|
367 Goal "[| ALL x. project UNIV h G ~: transient {x}; \ |
|
368 \ F Join project UNIV h G : A leadsTo B |] \ |
|
369 \ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"; |
|
370 by (etac leadsTo_induct 1); |
|
371 by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3); |
|
372 by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
373 by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1); |
|
374 qed "Join_project_leadsTo_I"; |
|
375 |
|
376 |
|
377 (** Strong precondition and postcondition; doesn't seem very useful. **) |
|
378 |
|
379 Goal "F : X guarantees Y ==> \ |
|
380 \ extend h F : (extend h `` X) guarantees (extend h `` Y)"; |
|
381 by (rtac guaranteesI 1); |
|
382 by Auto_tac; |
|
383 by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, |
|
384 guaranteesD]) 1); |
|
385 qed "guarantees_imp_extend_guarantees"; |
|
386 |
|
387 Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \ |
|
388 \ ==> F : X guarantees Y"; |
|
389 by (rtac guaranteesI 1); |
|
390 by (auto_tac (claset(), simpset() addsimps [guar_def, component_def])); |
|
391 by (dtac spec 1); |
|
392 by (dtac (mp RS mp) 1); |
|
393 by (Blast_tac 2); |
|
394 by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2); |
|
395 by Auto_tac; |
|
396 qed "extend_guarantees_imp_guarantees"; |
|
397 |
|
398 Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \ |
|
399 \ (F : X guarantees Y)"; |
|
400 by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees, |
|
401 extend_guarantees_imp_guarantees]) 1); |
|
402 qed "extend_guarantees_eq"; |
|
403 |
|
404 |
|
405 (*Weak precondition and postcondition; this is the good one! |
|
406 Not clear that it has a converse [or that we want one!]*) |
|
407 val [xguary,project,extend] = |
|
408 Goal "[| F : X guarantees Y; \ |
|
409 \ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \ |
|
410 \ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \ |
|
411 \ Disjoint (extend h F) G |] \ |
|
412 \ ==> extend h F Join G : Y' |] \ |
|
413 \ ==> extend h F : X' guarantees Y'"; |
|
414 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1); |
|
415 by (etac project 1); |
|
416 by (assume_tac 1); |
|
417 by (assume_tac 1); |
|
418 qed "project_guarantees"; |
|
419 |
|
420 (** It seems that neither "guarantees" law can be proved from the other. **) |
|
421 |
|
422 |
|
423 (*** guarantees corollaries ***) |
|
424 |
|
425 Goal "F : UNIV guarantees increasing func \ |
|
426 \ ==> extend h F : UNIV guarantees increasing (func o f)"; |
|
427 by (etac project_guarantees 1); |
|
428 by (ALLGOALS |
|
429 (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]))); |
|
430 qed "extend_guar_increasing"; |
|
431 |
|
432 Goal "F : UNIV guarantees Increasing func \ |
|
433 \ ==> extend h F : UNIV guarantees Increasing (func o f)"; |
|
434 by (etac project_guarantees 1); |
|
435 by (rtac (subset_UNIV RS project_Increasing_D) 2); |
|
436 by Auto_tac; |
|
437 qed "extend_guar_Increasing"; |
|
438 |
|
439 Goal "F : (func localTo G) guarantees increasing func \ |
|
440 \ ==> extend h F : (func o f) localTo (extend h G) \ |
|
441 \ guarantees increasing (func o f)"; |
|
442 by (etac project_guarantees 1); |
|
443 (*the "increasing" guarantee*) |
|
444 by (asm_simp_tac |
|
445 (simpset() addsimps [Join_project_increasing RS sym]) 2); |
|
446 (*the "localTo" requirement*) |
|
447 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
448 by (asm_simp_tac |
|
449 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
|
450 qed "extend_localTo_guar_increasing"; |
|
451 |
|
452 Goal "F : (func localTo G) guarantees Increasing func \ |
|
453 \ ==> extend h F : (func o f) localTo (extend h G) \ |
|
454 \ guarantees Increasing (func o f)"; |
|
455 by (etac project_guarantees 1); |
|
456 (*the "Increasing" guarantee*) |
|
457 by (etac (subset_UNIV RS project_Increasing_D) 2); |
|
458 (*the "localTo" requirement*) |
|
459 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
460 by (asm_simp_tac |
|
461 (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1); |
|
462 qed "extend_localTo_guar_Increasing"; |
|
463 |
|
464 |
|
465 (** Guarantees with a leadsTo postcondition **) |
|
466 |
|
467 Goal "[| G : f localTo extend h F; \ |
|
468 \ Disjoint (extend h F) G |] ==> project UNIV h G : stable {x}"; |
|
469 by (asm_full_simp_tac |
|
470 (simpset() addsimps [localTo_imp_stable, |
|
471 extend_set_sing, project_stable]) 1); |
|
472 qed "localTo_imp_project_stable"; |
|
473 |
|
474 |
|
475 Goal "F : stable{s} ==> F ~: transient {s}"; |
|
476 by (auto_tac (claset(), |
|
477 simpset() addsimps [FP_def, transient_def, |
|
478 stable_def, constrains_def])); |
|
479 qed "stable_sing_imp_not_transient"; |
|
480 |
|
481 Goal "F : (A co A') guarantees (B leadsTo B') \ |
|
482 \ ==> extend h F : ((extend_set h A) co (extend_set h A')) \ |
|
483 \ Int (f localTo (extend h F)) \ |
|
484 \ guarantees ((extend_set h B) leadsTo (extend_set h B'))"; |
|
485 by (etac project_guarantees 1); |
|
486 (*the safety precondition*) |
|
487 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1); |
|
488 by (asm_full_simp_tac |
|
489 (simpset() addsimps [project_constrains, Join_constrains, |
|
490 extend_constrains]) 1); |
|
491 by (fast_tac (claset() addDs [constrains_imp_subset]) 1); |
|
492 (*the liveness postcondition*) |
|
493 by (rtac Join_project_leadsTo_I 1); |
|
494 by Auto_tac; |
|
495 by (asm_full_simp_tac |
|
496 (simpset() addsimps [Join_localTo, self_localTo, |
|
497 localTo_imp_project_stable, |
|
498 stable_sing_imp_not_transient]) 1); |
|
499 qed "extend_co_guar_leadsTo"; |
|
500 |
|
501 Close_locale "Extend"; |