|
1 (* Title: ZF/UNITY/Union.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Unions of programs |
|
7 |
|
8 From Misra's Chapter 5: Asynchronous Compositions of Programs |
|
9 |
|
10 Proofs ported from HOL. |
|
11 |
|
12 *) |
|
13 |
|
14 (** SKIP **) |
|
15 |
|
16 Goal "reachable(SKIP) = state"; |
|
17 by (force_tac (claset() addEs [reachable.induct] |
|
18 addIs reachable.intrs, simpset()) 1); |
|
19 qed "reachable_SKIP"; |
|
20 |
|
21 Addsimps [reachable_SKIP]; |
|
22 |
|
23 (* Elimination programify from ok and Join *) |
|
24 |
|
25 Goal "programify(F) ok G <-> F ok G"; |
|
26 by (simp_tac (simpset() addsimps [ok_def]) 1); |
|
27 qed "ok_programify_left"; |
|
28 |
|
29 Goal "F ok programify(G) <-> F ok G"; |
|
30 by (simp_tac (simpset() addsimps [ok_def]) 1); |
|
31 qed "ok_programify_right"; |
|
32 |
|
33 Goal "programify(F) Join G = F Join G"; |
|
34 by (simp_tac (simpset() addsimps [Join_def]) 1); |
|
35 qed "Join_programify_left"; |
|
36 |
|
37 Goal "F Join programify(G) = F Join G"; |
|
38 by (simp_tac (simpset() addsimps [Join_def]) 1); |
|
39 qed "Join_programify_right"; |
|
40 |
|
41 Addsimps [ok_programify_left, ok_programify_right, |
|
42 Join_programify_left, Join_programify_right]; |
|
43 |
|
44 (** SKIP and safety properties **) |
|
45 |
|
46 Goalw [constrains_def] |
|
47 "[| A:condition; B:condition |] ==> (SKIP: A co B) <-> (A<=B)"; |
|
48 by Auto_tac; |
|
49 qed "SKIP_in_constrains_iff"; |
|
50 Addsimps [SKIP_in_constrains_iff]; |
|
51 |
|
52 |
|
53 Goalw [Constrains_def] |
|
54 "[| A:condition; B:condition |] ==> (SKIP : A Co B)<-> (A<=B)"; |
|
55 by (Asm_simp_tac 1); |
|
56 by (auto_tac (claset(), |
|
57 simpset() addsimps [condition_def])); |
|
58 qed "SKIP_in_Constrains_iff"; |
|
59 Addsimps [SKIP_in_Constrains_iff]; |
|
60 |
|
61 Goal "A:condition ==>SKIP : stable(A)"; |
|
62 by (auto_tac (claset(), |
|
63 simpset() addsimps [stable_def])); |
|
64 qed "SKIP_in_stable"; |
|
65 Addsimps [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable]; |
|
66 |
|
67 |
|
68 (** Join and JOIN types **) |
|
69 |
|
70 Goalw [Join_def] |
|
71 "F Join G : program"; |
|
72 by Auto_tac; |
|
73 qed "Join_in_program"; |
|
74 AddIffs [Join_in_program]; |
|
75 AddTCs [Join_in_program]; |
|
76 |
|
77 Goalw [JOIN_def] |
|
78 "JOIN(I,F):program"; |
|
79 by Auto_tac; |
|
80 qed "JOIN_in_program"; |
|
81 AddIffs [JOIN_in_program]; |
|
82 AddTCs [JOIN_in_program]; |
|
83 |
|
84 (* Init, Acts, and AllowedActs of Join and JOIN *) |
|
85 Goal "Init(F Join G) = Init(F) Int Init(G)"; |
|
86 by (simp_tac (simpset() |
|
87 addsimps [Int_assoc, Join_def]) 1); |
|
88 qed "Init_Join"; |
|
89 |
|
90 Goal "Acts(F Join G) = Acts(F) Un Acts(G)"; |
|
91 by (simp_tac (simpset() |
|
92 addsimps [Int_Un_distrib,cons_absorb,Join_def]) 1); |
|
93 qed "Acts_Join"; |
|
94 |
|
95 Goal "AllowedActs(F Join G) = \ |
|
96 \ AllowedActs(F) Int AllowedActs(G)"; |
|
97 by (simp_tac (simpset() |
|
98 addsimps [Int_assoc,cons_absorb,Join_def]) 1); |
|
99 qed "AllowedActs_Join"; |
|
100 Addsimps [Init_Join, Acts_Join, AllowedActs_Join]; |
|
101 |
|
102 |
|
103 (** Join's algebraic laws **) |
|
104 |
|
105 Goal "F Join G = G Join F"; |
|
106 by (simp_tac (simpset() addsimps |
|
107 [Join_def, Un_commute, Int_commute]) 1); |
|
108 qed "Join_commute"; |
|
109 |
|
110 |
|
111 Goal "A Join (B Join C) = B Join (A Join C)"; |
|
112 by (asm_simp_tac (simpset() addsimps |
|
113 Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1); |
|
114 qed "Join_left_commute"; |
|
115 |
|
116 |
|
117 Goal "(F Join G) Join H = F Join (G Join H)"; |
|
118 by (asm_simp_tac (simpset() addsimps |
|
119 Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib]) 1); |
|
120 qed "Join_assoc"; |
|
121 |
|
122 Goalw [Join_def, SKIP_def] |
|
123 "SKIP Join F = programify(F)"; |
|
124 by (simp_tac (simpset() addsimps [Int_absorb, cons_absorb,cons_eq]) 1); |
|
125 qed "Join_SKIP_left"; |
|
126 |
|
127 Goal "F Join SKIP = programify(F)"; |
|
128 by (stac Join_commute 1); |
|
129 by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1); |
|
130 qed "Join_SKIP_right"; |
|
131 |
|
132 |
|
133 Addsimps [Join_SKIP_left, Join_SKIP_right]; |
|
134 |
|
135 |
|
136 Goal "F Join F = programify(F)"; |
|
137 by (rtac program_equalityI 1); |
|
138 by Auto_tac; |
|
139 qed "Join_absorb"; |
|
140 |
|
141 Addsimps [Join_absorb]; |
|
142 |
|
143 Goal "F Join (F Join G) = F Join G"; |
|
144 by (asm_simp_tac (simpset() addsimps [Join_assoc RS sym]) 1); |
|
145 qed "Join_left_absorb"; |
|
146 |
|
147 |
|
148 (*Join is an AC-operator*) |
|
149 val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute]; |
|
150 |
|
151 (** Eliminating programify in JN and OK expressions **) |
|
152 |
|
153 Goal "OK(I, %x. programify(F(x))) <-> OK(I, F)"; |
|
154 by (simp_tac (simpset() addsimps [OK_def]) 1); |
|
155 qed "OK_programify"; |
|
156 |
|
157 Goal "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"; |
|
158 by (simp_tac (simpset() addsimps [JOIN_def]) 1); |
|
159 qed "JN_programify"; |
|
160 |
|
161 Addsimps [OK_programify, JN_programify]; |
|
162 |
|
163 (* JN *) |
|
164 |
|
165 Goalw [JOIN_def] |
|
166 "JOIN(0, F) = SKIP"; |
|
167 by Auto_tac; |
|
168 qed "JN_empty"; |
|
169 Addsimps [JN_empty]; |
|
170 AddSEs [not_emptyE]; |
|
171 Addsimps [Inter_0]; |
|
172 |
|
173 Goal |
|
174 "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))"; |
|
175 by (Asm_full_simp_tac 1); |
|
176 by (Clarify_tac 1); |
|
177 by (auto_tac (claset(), simpset() |
|
178 addsimps [JOIN_def,INT_Int_distrib2])); |
|
179 qed "Init_JN"; |
|
180 |
|
181 Goal |
|
182 "Acts(JOIN(I,F)) = cons(Id, UN i:I. Acts(F(i)))"; |
|
183 by (auto_tac (claset(), |
|
184 simpset() addsimps [JOIN_def, UN_Int_distrib])); |
|
185 qed "Acts_JN"; |
|
186 |
|
187 Goal |
|
188 "AllowedActs(JN i:I. F(i)) = (if I=0 then action else (INT i:I. AllowedActs(F(i))))"; |
|
189 by (auto_tac (claset(), simpset() |
|
190 addsimps [JOIN_def, INT_cons RS sym, INT_Int_distrib2])); |
|
191 qed "AllowedActs_JN"; |
|
192 |
|
193 Addsimps [Init_JN, Acts_JN, AllowedActs_JN]; |
|
194 |
|
195 |
|
196 Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))"; |
|
197 by (rtac program_equalityI 1); |
|
198 by Auto_tac; |
|
199 qed "JN_cons"; |
|
200 Addsimps[JN_cons]; |
|
201 |
|
202 |
|
203 val prems = Goalw [JOIN_def] |
|
204 "[| I=J; !!i. i:J ==> F(i) = G(i) |] ==> \ |
|
205 \ (JN i:I. F(i)) = (JN i:J. G(i))"; |
|
206 by (asm_simp_tac (simpset() addsimps prems) 1); |
|
207 qed "JN_cong"; |
|
208 |
|
209 Addcongs [JN_cong]; |
|
210 |
|
211 |
|
212 (*** JN laws ***) |
|
213 Goal "k:I ==>F(k) Join (JN i:I. F(i)) = (JN i:I. F(i))"; |
|
214 by (stac (JN_cons RS sym) 1); |
|
215 by (auto_tac (claset(), |
|
216 simpset() addsimps [cons_absorb])); |
|
217 qed "JN_absorb"; |
|
218 |
|
219 Goalw [Inter_def] "[| i:I; j:J |] ==> \ |
|
220 \ (INT i:I Un J. A(i)) = ((INT i:I. A(i)) Int (INT j:J. A(j)))"; |
|
221 by Auto_tac; |
|
222 by (Blast_tac 1); |
|
223 qed "INT_Un"; |
|
224 |
|
225 Goal "(JN i: I Un J. F(i)) = ((JN i: I. F(i)) Join (JN i:J. F(i)))"; |
|
226 by (rtac program_equalityI 1); |
|
227 by (ALLGOALS(Asm_full_simp_tac)); |
|
228 by Safe_tac; |
|
229 by (ALLGOALS(asm_full_simp_tac (simpset() |
|
230 addsimps [Int_absorb, INT_Int_distrib2, |
|
231 Int_INT_distrib, UN_cons, INT_cons]))); |
|
232 by (ALLGOALS(Clarify_tac)); |
|
233 by (REPEAT(Blast_tac 1)); |
|
234 qed "JN_Un"; |
|
235 |
|
236 Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))"; |
|
237 by (rtac program_equalityI 1); |
|
238 by Auto_tac; |
|
239 qed "JN_constant"; |
|
240 |
|
241 Goal |
|
242 "(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))"; |
|
243 by (rtac program_equalityI 1); |
|
244 by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb]))); |
|
245 by Safe_tac; |
|
246 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps |
|
247 [INT_Int_distrib, Int_absorb]))); |
|
248 by (Force_tac 1); |
|
249 qed "JN_Join_distrib"; |
|
250 |
|
251 Goal |
|
252 "(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))"; |
|
253 by (asm_simp_tac (simpset() |
|
254 addsimps [JN_Join_distrib, JN_constant]) 1); |
|
255 qed "JN_Join_miniscope"; |
|
256 |
|
257 (*Used to prove guarantees_JN_I*) |
|
258 |
|
259 Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)"; |
|
260 by (rtac program_equalityI 1); |
|
261 by Auto_tac; |
|
262 qed "JN_Join_diff"; |
|
263 |
|
264 (*** Safety: co, stable, FP ***) |
|
265 |
|
266 |
|
267 (*Fails if I=0 because it collapses to SKIP : A co B, i.e. to A<=B. So an |
|
268 alternative precondition is A<=B, but most proofs using this rule require |
|
269 I to be nonempty for other reasons anyway.*) |
|
270 |
|
271 Goalw [constrains_def, JOIN_def] |
|
272 "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)"; |
|
273 by Auto_tac; |
|
274 by (blast_tac (claset() addDs [ActsD]) 1); |
|
275 qed "JN_constrains"; |
|
276 |
|
277 Goal "(F Join G : A co B) <-> \ |
|
278 \ (programify(F):A co B & programify(G):A co B)"; |
|
279 by (auto_tac |
|
280 (claset(), simpset() addsimps [constrains_def])); |
|
281 qed "Join_constrains"; |
|
282 |
|
283 Goal "(F Join G : A unless B) <-> \ |
|
284 \ (programify(F) : A unless B & programify(G):A unless B)"; |
|
285 by (asm_simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1); |
|
286 qed "Join_unless"; |
|
287 |
|
288 Addsimps [Join_constrains, Join_unless]; |
|
289 |
|
290 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. |
|
291 reachable (F Join G) could be much bigger than reachable F, reachable G |
|
292 *) |
|
293 |
|
294 Goal "[| F : A co A'; G:B co B' |] \ |
|
295 \ ==> F Join G : (A Int B) co (A' Un B')"; |
|
296 by (subgoal_tac "A:condition&A':condition & B: condition& \ |
|
297 \ B': condition & F:program & G:program" 1); |
|
298 by (blast_tac (claset() addDs [constrainsD2]) 2); |
|
299 by (Asm_simp_tac 1); |
|
300 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
301 qed "Join_constrains_weaken"; |
|
302 |
|
303 (*If I=0, it degenerates to SKIP : UNIV co 0, which is false.*) |
|
304 Goal "[| ALL i:I. F(i) : A(i) co A'(i); i: I |] \ |
|
305 \ ==> (JN i:I. F(i)) : (INT i:I. A(i)) co (UN i:I. A'(i))"; |
|
306 by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); |
|
307 by (Clarify_tac 1); |
|
308 by (subgoal_tac "(ALL i:I. F(i):program & A(i):condition)&\ |
|
309 \ (Union(RepFun(I, A')):condition)&\ |
|
310 \ (Inter(RepFun(I, A)):condition)" 1); |
|
311 by (blast_tac (claset() addDs [constrainsD2]) 2); |
|
312 by (Asm_simp_tac 1); |
|
313 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
314 qed "JN_constrains_weaken"; |
|
315 |
|
316 |
|
317 Goal "A:condition ==> (JN i:I. F(i)) : stable(A) <-> \ |
|
318 \ (ALL i:I. programify(F(i)):stable(A))"; |
|
319 by (asm_simp_tac |
|
320 (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1); |
|
321 by Auto_tac; |
|
322 by (blast_tac (claset() addDs [ActsD]) 1); |
|
323 qed "JN_stable"; |
|
324 |
|
325 |
|
326 Goal "[| ALL i:I. F(i) : invariant(A); i : I |] \ |
|
327 \ ==> (JN i:I. F(i)) : invariant(A)"; |
|
328 by (subgoal_tac "A:condition" 1); |
|
329 by (blast_tac (claset() addDs [invariantD2]) 2); |
|
330 by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1); |
|
331 by (Blast_tac 1); |
|
332 bind_thm ("invariant_JN_I", ballI RS result()); |
|
333 Goal " (F Join G : stable(A)) <-> \ |
|
334 \ (programify(F) : stable(A) & programify(G): stable(A))"; |
|
335 by (asm_simp_tac (simpset() addsimps [stable_def]) 1); |
|
336 qed "Join_stable"; |
|
337 |
|
338 |
|
339 (* TO BE DONE: stable_increasing *) |
|
340 |
|
341 Addsimps [Join_stable]; |
|
342 |
|
343 Goal "[| F : invariant(A); G : invariant(A) |] \ |
|
344 \ ==> F Join G : invariant(A)"; |
|
345 by (subgoal_tac "F:program&G:program" 1); |
|
346 by (blast_tac (claset() addDs [invariantD2]) 2); |
|
347 by (full_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
348 by (auto_tac (claset() addIs [Join_in_program], simpset())); |
|
349 qed "invariant_JoinI"; |
|
350 |
|
351 |
|
352 (* Fails if I=0 because INT i:0. A(i) = 0 *) |
|
353 Goal "i:I ==> FP(JN i:I. F(i)) = (INT i:I. FP (programify(F(i))))"; |
|
354 by (asm_simp_tac (simpset() addsimps [FP_def, Inter_def]) 1); |
|
355 by (rtac equalityI 1); |
|
356 by Safe_tac; |
|
357 by (ALLGOALS(subgoal_tac "{x}:condition")); |
|
358 by (rotate_tac ~1 3); |
|
359 by (rotate_tac ~1 1); |
|
360 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable]))); |
|
361 by (rewrite_goals_tac [condition_def]); |
|
362 by (REPEAT(Blast_tac 1)); |
|
363 qed "FP_JN"; |
|
364 |
|
365 (*** Progress: transient, ensures ***) |
|
366 |
|
367 Goal "i:I==>(JN i:I. F(i)) : transient(A) <-> \ |
|
368 \ (EX i:I. programify(F(i)) : transient(A))"; |
|
369 by (auto_tac (claset(), |
|
370 simpset() addsimps [transient_def, JOIN_def])); |
|
371 by (auto_tac (claset(), simpset() addsimps |
|
372 [condition_def,UN_Int_distrib, INT_Int_distrib])); |
|
373 qed "JN_transient"; |
|
374 |
|
375 Goal "F Join G : transient(A) <-> \ |
|
376 \ (programify(F) : transient(A) | programify(G):transient(A))"; |
|
377 by (auto_tac (claset(), |
|
378 simpset() addsimps [transient_def, |
|
379 Join_def, Int_Un_distrib])); |
|
380 qed "Join_transient"; |
|
381 |
|
382 Addsimps [Join_transient]; |
|
383 |
|
384 |
|
385 Goal "F : transient(A) ==> F Join G : transient(A)"; |
|
386 by (asm_full_simp_tac (simpset() |
|
387 addsimps [Join_transient, transientD]) 1); |
|
388 qed "Join_transient_I1"; |
|
389 |
|
390 |
|
391 Goal "G : transient(A) ==> F Join G : transient(A)"; |
|
392 by (asm_full_simp_tac (simpset() |
|
393 addsimps [Join_transient, transientD]) 1); |
|
394 qed "Join_transient_I2"; |
|
395 |
|
396 (*If I=0 it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) |
|
397 Goal "i : I ==> \ |
|
398 \ (JN i:I. F(i)) : A ensures B <-> \ |
|
399 \ ((ALL i:I. programify(F(i)) : (A-B) co (A Un B)) & \ |
|
400 \ (EX i:I. programify(F(i)) : A ensures B))"; |
|
401 by (auto_tac (claset(), |
|
402 simpset() addsimps [ensures_def, JN_constrains, JN_transient])); |
|
403 qed "JN_ensures"; |
|
404 |
|
405 |
|
406 Goalw [ensures_def] |
|
407 "F Join G : A ensures B <-> \ |
|
408 \ (programify(F) : (A-B) co (A Un B) & programify(G) : (A-B) co (A Un B) & \ |
|
409 \ (programify(F): transient (A-B) | programify(G) : transient (A-B)))"; |
|
410 by (auto_tac (claset(), simpset() addsimps [Join_transient])); |
|
411 qed "Join_ensures"; |
|
412 |
|
413 |
|
414 |
|
415 Goalw [stable_def, constrains_def, Join_def] |
|
416 "[| F : stable(A); G : A co A' |] \ |
|
417 \ ==> F Join G : A co A'"; |
|
418 by Auto_tac; |
|
419 by (rewrite_goals_tac [condition_def]); |
|
420 by Auto_tac; |
|
421 by (blast_tac (claset() addDs [ActsD]) 3); |
|
422 by (dres_inst_tac [("x", "Id")] bspec 1); |
|
423 by (dres_inst_tac [("x", "Id")] bspec 2); |
|
424 by (dres_inst_tac [("x", "x")] bspec 4); |
|
425 by (dres_inst_tac [("x", "Id")] bspec 5); |
|
426 by Auto_tac; |
|
427 qed "stable_Join_constrains"; |
|
428 |
|
429 (*Premise for G cannot use Always because F: Stable A is |
|
430 weaker than G : stable A *) |
|
431 Goal "[| F : stable(A); G : invariant(A) |] ==> F Join G : Always(A)"; |
|
432 by (subgoal_tac "A:condition & F:program" 1); |
|
433 by (blast_tac (claset() addDs [stableD2]) 2); |
|
434 by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def, |
|
435 Stable_eq_stable]) 1); |
|
436 by (force_tac(claset() addIs [stable_Int], simpset()) 1); |
|
437 qed "stable_Join_Always1"; |
|
438 |
|
439 |
|
440 |
|
441 (*As above, but exchanging the roles of F and G*) |
|
442 Goal "[| F : invariant(A); G : stable(A) |] ==> F Join G : Always(A)"; |
|
443 by (stac Join_commute 1); |
|
444 by (blast_tac (claset() addIs [stable_Join_Always1]) 1); |
|
445 qed "stable_Join_Always2"; |
|
446 |
|
447 |
|
448 |
|
449 Goal "[| F : stable(A); G : A ensures B |] ==> F Join G : A ensures B"; |
|
450 by (subgoal_tac "F:program&G:program&A:condition&B:condition" 1); |
|
451 by (blast_tac (claset() addDs [stableD2, ensuresD2]) 2); |
|
452 by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1); |
|
453 by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); |
|
454 by (etac constrains_weaken 1); |
|
455 by Auto_tac; |
|
456 qed "stable_Join_ensures1"; |
|
457 |
|
458 |
|
459 (*As above, but exchanging the roles of F and G*) |
|
460 Goal "[| F : A ensures B; G : stable(A) |] ==> F Join G : A ensures B"; |
|
461 by (stac Join_commute 1); |
|
462 by (blast_tac (claset() addIs [stable_Join_ensures1]) 1); |
|
463 qed "stable_Join_ensures2"; |
|
464 |
|
465 |
|
466 (*** the ok and OK relations ***) |
|
467 |
|
468 Goal "SKIP ok F"; |
|
469 by (auto_tac (claset() addDs [ActsD], |
|
470 simpset() addsimps [ok_def])); |
|
471 qed "ok_SKIP1"; |
|
472 |
|
473 Goal "F ok SKIP"; |
|
474 by (auto_tac (claset() addDs [ActsD], |
|
475 simpset() addsimps [ok_def])); |
|
476 qed "ok_SKIP2"; |
|
477 |
|
478 AddIffs [ok_SKIP1, ok_SKIP2]; |
|
479 |
|
480 Goal "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))"; |
|
481 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
482 qed "ok_Join_commute"; |
|
483 |
|
484 Goal "(F ok G) <->(G ok F)"; |
|
485 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
486 qed "ok_commute"; |
|
487 |
|
488 bind_thm ("ok_sym", ok_commute RS iffD1); |
|
489 |
|
490 Goal "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"; |
|
491 by (asm_full_simp_tac |
|
492 (simpset() addsimps [ok_def, Join_def, OK_def, |
|
493 Int_assoc, cons_absorb, Int_Un_distrib, Ball_def]) 1); |
|
494 by (rtac iffI 1); |
|
495 by Safe_tac; |
|
496 by (REPEAT(Force_tac 1)); |
|
497 qed "ok_iff_OK"; |
|
498 |
|
499 Goal "F ok (G Join H) <-> (F ok G & F ok H)"; |
|
500 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
501 qed "ok_Join_iff1"; |
|
502 |
|
503 |
|
504 Goal "(G Join H) ok F <-> (G ok F & H ok F)"; |
|
505 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
506 qed "ok_Join_iff2"; |
|
507 AddIffs [ok_Join_iff1, ok_Join_iff2]; |
|
508 |
|
509 (*useful? Not with the previous two around*) |
|
510 Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"; |
|
511 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
512 qed "ok_Join_commute_I"; |
|
513 |
|
514 Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))"; |
|
515 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
516 by (blast_tac (claset() addDs [ActsD]) 1); |
|
517 by (REPEAT(Force_tac 1)); |
|
518 qed "ok_JN_iff1"; |
|
519 |
|
520 |
|
521 Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)"; |
|
522 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
|
523 by (blast_tac (claset() addDs [ActsD]) 1); |
|
524 qed "ok_JN_iff2"; |
|
525 AddIffs [ok_JN_iff1, ok_JN_iff2]; |
|
526 |
|
527 Goal "OK(I,F) <-> (ALL i: I. ALL j: I-{i}. F(i) ok (F(j)))"; |
|
528 by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def])); |
|
529 qed "OK_iff_ok"; |
|
530 |
|
531 |
|
532 Goal "[| OK(I,F); i: I; j: I; i~=j|] ==> F(i) ok F(j)"; |
|
533 by (auto_tac (claset(), simpset() addsimps [OK_iff_ok])); |
|
534 qed "OK_imp_ok"; |
|
535 |
|
536 |
|
537 (*** Allowed ***) |
|
538 |
|
539 Goal "Allowed(SKIP) = program"; |
|
540 by (auto_tac (claset() addDs [ActsD], |
|
541 simpset() addsimps [Allowed_def])); |
|
542 qed "Allowed_SKIP"; |
|
543 |
|
544 Goal "Allowed(F Join G) = \ |
|
545 \ Allowed(programify(F)) Int Allowed(programify(G))"; |
|
546 by (auto_tac (claset(), simpset() addsimps [Allowed_def])); |
|
547 qed "Allowed_Join"; |
|
548 |
|
549 Goal "i:I ==> \ |
|
550 \ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))"; |
|
551 by (auto_tac (claset(), simpset() addsimps [Allowed_def])); |
|
552 br equalityI 1; |
|
553 by Auto_tac; |
|
554 qed "Allowed_JN"; |
|
555 |
|
556 Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN]; |
|
557 |
|
558 Goal |
|
559 "F ok G <-> (programify(F):Allowed(programify(G)) & \ |
|
560 \ programify(G):Allowed(programify(F)))"; |
|
561 by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1); |
|
562 qed "ok_iff_Allowed"; |
|
563 |
|
564 |
|
565 Goal "OK(I,F) <-> \ |
|
566 \ (ALL i: I. ALL j: I-{i}. programify(F(i)) : Allowed(programify(F(j))))"; |
|
567 by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed])); |
|
568 qed "OK_iff_Allowed"; |
|
569 |
|
570 (*** safety_prop, for reasoning about given instances of "ok" ***) |
|
571 |
|
572 Goal "safety_prop(X) ==> (Acts(G) <= cons(Id, (UN F:X. Acts(F)))) <-> (programify(G):X)"; |
|
573 by (full_simp_tac( simpset() addsimps [safety_prop_def]) 1); |
|
574 by (Clarify_tac 1); |
|
575 by (case_tac "G:program" 1); |
|
576 by (ALLGOALS(Asm_full_simp_tac)); |
|
577 by (Blast_tac 1); |
|
578 by Safe_tac; |
|
579 by (Force_tac 2); |
|
580 by (force_tac (claset(), simpset() |
|
581 addsimps [programify_def]) 1); |
|
582 qed "safety_prop_Acts_iff"; |
|
583 |
|
584 Goal "X:property ==> \ |
|
585 \ (safety_prop(X) --> \ |
|
586 \ ((UN G:X. Acts(G)) <= AllowedActs(F)) <-> (X <= Allowed(programify(F))))"; |
|
587 by (auto_tac (claset(), |
|
588 simpset() addsimps [Allowed_def, |
|
589 safety_prop_Acts_iff RS iff_sym, property_def])); |
|
590 qed "safety_prop_AllowedActs_iff_Allowed"; |
|
591 |
|
592 |
|
593 Goal "X:property ==> \ |
|
594 \ safety_prop(X) --> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X"; |
|
595 by (asm_full_simp_tac (simpset() addsimps [Allowed_def, |
|
596 UN_Int_distrib,safety_prop_Acts_iff, property_def]) 1); |
|
597 by Auto_tac; |
|
598 qed "Allowed_eq"; |
|
599 |
|
600 Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); X:property; safety_prop(X) |] \ |
|
601 \ ==> Allowed(F) = X"; |
|
602 by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); |
|
603 qed "def_prg_Allowed"; |
|
604 |
|
605 (*For safety_prop to hold, the property must be satisfiable!*) |
|
606 Goal "B:condition ==> safety_prop(A co B) <-> (A <= B)"; |
|
607 by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1); |
|
608 by Auto_tac; |
|
609 by (Blast_tac 2); |
|
610 by (force_tac (claset(), simpset() addsimps [condition_def]) 1); |
|
611 qed "safety_prop_constrains"; |
|
612 Addsimps [safety_prop_constrains]; |
|
613 |
|
614 |
|
615 |
|
616 Goal "A:condition ==>safety_prop(stable(A))"; |
|
617 by (asm_simp_tac (simpset() addsimps [stable_def]) 1); |
|
618 qed "safety_prop_stable"; |
|
619 Addsimps [safety_prop_stable]; |
|
620 |
|
621 Goal "[| X:property; Y:property |] ==> \ |
|
622 \ safety_prop(X) --> safety_prop(Y) --> safety_prop(X Int Y)"; |
|
623 by (asm_full_simp_tac (simpset() |
|
624 addsimps [safety_prop_def, property_def]) 1); |
|
625 by Safe_tac; |
|
626 by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), |
|
627 ("C", "Union(RepFun(Y, Acts))")] subset_trans 2); |
|
628 by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), |
|
629 ("C", "Union(RepFun(X, Acts))")] subset_trans 1); |
|
630 by (REPEAT(Blast_tac 1)); |
|
631 qed "safety_prop_Int"; |
|
632 Addsimps [safety_prop_Int]; |
|
633 |
|
634 (* If I=0 the conclusion becomes safety_prop(0) which is false *) |
|
635 Goal "[| ALL i:I. X(i):property; i:I |] ==> \ |
|
636 \ (ALL i:I. safety_prop(X(i))) --> safety_prop(INT i:I. X(i))"; |
|
637 by (asm_full_simp_tac (simpset() addsimps [safety_prop_def, property_def]) 1); |
|
638 by Safe_tac; |
|
639 by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"), |
|
640 ("C", "Union(RepFun(X(xb), Acts))")] subset_trans 3); |
|
641 by (REPEAT(Blast_tac 1)); |
|
642 bind_thm ("safety_prop_Inter", ballI RS result()); |
|
643 |
|
644 Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X); X:property |] \ |
|
645 \ ==> F ok G <-> (programify(G):X & acts Int action <= AllowedActs(G))"; |
|
646 by (auto_tac (claset(), |
|
647 simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib, property_def])); |
|
648 qed "def_UNION_ok_iff"; |
|
649 |