author | paulson |
Wed, 05 Aug 1998 18:20:25 +0200 | |
changeset 5257 | c03e3ba9cbcc |
parent 5253 | 82a5ca6290aa |
child 5277 | e4297d03e5d2 |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/SubstAx |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Weak Fairness versions of transient, ensures, LeadsTo. |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
5111 | 11 |
(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B) |
12 |
(reachable(Init,Acts) Int B') *) |
|
4776 | 13 |
bind_thm ("constrains_reachable", |
14 |
rewrite_rule [stable_def] stable_reachable RS constrains_Int); |
|
15 |
||
16 |
||
17 |
(*** Introduction rules: Basis, Trans, Union ***) |
|
18 |
||
5253 | 19 |
Goal "leadsTo (Acts prg) A B ==> LeadsTo prg A B"; |
5111 | 20 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 21 |
by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1); |
22 |
qed "leadsTo_imp_LeadsTo"; |
|
23 |
||
5253 | 24 |
Goal "ensures (Acts prg) (reachable prg Int A) (reachable prg Int A') \ |
25 |
\ ==> LeadsTo prg A A'"; |
|
26 |
by (full_simp_tac (simpset() addsimps [ensures_def, LeadsTo_def]) 1); |
|
4776 | 27 |
by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1); |
5253 | 28 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]))); |
29 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
4776 | 30 |
qed "LeadsTo_Basis"; |
31 |
||
5253 | 32 |
Goal "[| LeadsTo prg A B; LeadsTo prg B C |] \ |
33 |
\ ==> LeadsTo prg A C"; |
|
5111 | 34 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 35 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
36 |
qed "LeadsTo_Trans"; |
|
37 |
||
5111 | 38 |
val [prem] = goalw thy [LeadsTo_def] |
5253 | 39 |
"(!!A. A : S ==> LeadsTo prg A B) ==> LeadsTo prg (Union S) B"; |
5111 | 40 |
by (Simp_tac 1); |
4776 | 41 |
by (stac Int_Union 1); |
5111 | 42 |
by (blast_tac (claset() addIs [leadsTo_UN, |
43 |
simplify (simpset()) prem]) 1); |
|
4776 | 44 |
qed "LeadsTo_Union"; |
45 |
||
46 |
||
47 |
(*** Derived rules ***) |
|
48 |
||
5253 | 49 |
Goal "id: (Acts prg) ==> LeadsTo prg A UNIV"; |
4776 | 50 |
by (asm_simp_tac (simpset() addsimps [LeadsTo_def, |
51 |
Int_lower1 RS subset_imp_leadsTo]) 1); |
|
52 |
qed "LeadsTo_UNIV"; |
|
53 |
Addsimps [LeadsTo_UNIV]; |
|
54 |
||
55 |
(*Useful with cancellation, disjunction*) |
|
5253 | 56 |
Goal "LeadsTo prg A (A' Un A') ==> LeadsTo prg A A'"; |
4776 | 57 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
58 |
qed "LeadsTo_Un_duplicate"; |
|
59 |
||
5253 | 60 |
Goal "LeadsTo prg A (A' Un C Un C) ==> LeadsTo prg A (A' Un C)"; |
4776 | 61 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
62 |
qed "LeadsTo_Un_duplicate2"; |
|
63 |
||
64 |
val prems = goal thy |
|
5253 | 65 |
"(!!i. i : I ==> LeadsTo prg (A i) B) \ |
66 |
\ ==> LeadsTo prg (UN i:I. A i) B"; |
|
4776 | 67 |
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
68 |
by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); |
|
69 |
qed "LeadsTo_UN"; |
|
70 |
||
71 |
(*Binary union introduction rule*) |
|
5253 | 72 |
Goal "[| LeadsTo prg A C; LeadsTo prg B C |] ==> LeadsTo prg (A Un B) C"; |
4776 | 73 |
by (stac Un_eq_Union 1); |
74 |
by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
|
75 |
qed "LeadsTo_Un"; |
|
76 |
||
77 |
||
5253 | 78 |
Goal "[| reachable prg Int A <= B; id: (Acts prg) |] \ |
79 |
\ ==> LeadsTo prg A B"; |
|
5111 | 80 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 81 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
82 |
qed "Int_subset_imp_LeadsTo"; |
|
83 |
||
5253 | 84 |
Goal "[| A <= B; id: (Acts prg) |] ==> LeadsTo prg A B"; |
5111 | 85 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 86 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
87 |
qed "subset_imp_LeadsTo"; |
|
88 |
||
89 |
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
|
90 |
Addsimps [empty_LeadsTo]; |
|
91 |
||
5253 | 92 |
Goal "[| reachable prg Int A = {}; id: (Acts prg) |] \ |
93 |
\ ==> LeadsTo prg A B"; |
|
4776 | 94 |
by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1); |
95 |
qed "Int_empty_LeadsTo"; |
|
96 |
||
97 |
||
5253 | 98 |
Goal "[| LeadsTo prg A A'; \ |
99 |
\ reachable prg Int A' <= B' |] \ |
|
100 |
\ ==> LeadsTo prg A B'"; |
|
5111 | 101 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 102 |
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
103 |
qed_spec_mp "LeadsTo_weaken_R"; |
|
104 |
||
105 |
||
5253 | 106 |
Goal "[| LeadsTo prg A A'; \ |
107 |
\ reachable prg Int B <= A; id: (Acts prg) |] \ |
|
108 |
\ ==> LeadsTo prg B A'"; |
|
5111 | 109 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 110 |
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
111 |
qed_spec_mp "LeadsTo_weaken_L"; |
|
112 |
||
113 |
||
114 |
(*Distributes over binary unions*) |
|
5253 | 115 |
Goal "id: (Acts prg) ==> \ |
116 |
\ LeadsTo prg (A Un B) C = \ |
|
117 |
\ (LeadsTo prg A C & LeadsTo prg B C)"; |
|
4776 | 118 |
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
119 |
qed "LeadsTo_Un_distrib"; |
|
120 |
||
5253 | 121 |
Goal "id: (Acts prg) ==> \ |
122 |
\ LeadsTo prg (UN i:I. A i) B = \ |
|
123 |
\ (ALL i : I. LeadsTo prg (A i) B)"; |
|
4776 | 124 |
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
125 |
qed "LeadsTo_UN_distrib"; |
|
126 |
||
5253 | 127 |
Goal "id: (Acts prg) ==> \ |
128 |
\ LeadsTo prg (Union S) B = \ |
|
129 |
\ (ALL A : S. LeadsTo prg A B)"; |
|
4776 | 130 |
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
131 |
qed "LeadsTo_Union_distrib"; |
|
132 |
||
133 |
||
5253 | 134 |
Goal "[| LeadsTo prg A A'; id: (Acts prg); \ |
135 |
\ reachable prg Int B <= A; \ |
|
136 |
\ reachable prg Int A' <= B' |] \ |
|
137 |
\ ==> LeadsTo prg B B'"; |
|
4776 | 138 |
(*PROOF FAILED: why?*) |
139 |
by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R, |
|
140 |
LeadsTo_weaken_L]) 1); |
|
141 |
qed "LeadsTo_weaken"; |
|
142 |
||
143 |
||
5253 | 144 |
(*Set difference: maybe combine with leadsTo_weaken_L?? |
145 |
This is the most useful form of the "disjunction" rule*) |
|
146 |
Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: (Acts prg) |] \ |
|
5257 | 147 |
\ ==> LeadsTo prg A C"; |
4776 | 148 |
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); |
149 |
qed "LeadsTo_Diff"; |
|
150 |
||
151 |
||
152 |
(** Meta or object quantifier ??????????????????? |
|
153 |
see ball_constrains_UN in UNITY.ML***) |
|
154 |
||
155 |
val prems = goal thy |
|
5253 | 156 |
"(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \ |
157 |
\ ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)"; |
|
4776 | 158 |
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
159 |
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] |
|
160 |
addIs prems) 1); |
|
161 |
qed "LeadsTo_UN_UN"; |
|
162 |
||
163 |
||
164 |
(*Version with no index set*) |
|
5257 | 165 |
val prems = |
166 |
Goal "(!! i. LeadsTo prg (A i) (A' i)) \ |
|
167 |
\ ==> LeadsTo prg (UN i. A i) (UN i. A' i)"; |
|
4776 | 168 |
by (blast_tac (claset() addIs [LeadsTo_UN_UN] |
169 |
addIs prems) 1); |
|
170 |
qed "LeadsTo_UN_UN_noindex"; |
|
171 |
||
172 |
(*Version with no index set*) |
|
5253 | 173 |
Goal "ALL i. LeadsTo prg (A i) (A' i) \ |
5257 | 174 |
\ ==> LeadsTo prg (UN i. A i) (UN i. A' i)"; |
4776 | 175 |
by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
176 |
qed "all_LeadsTo_UN_UN"; |
|
177 |
||
178 |
||
179 |
(*Binary union version*) |
|
5253 | 180 |
Goal "[| LeadsTo prg A A'; LeadsTo prg B B' |] \ |
5257 | 181 |
\ ==> LeadsTo prg (A Un B) (A' Un B')"; |
4776 | 182 |
by (blast_tac (claset() addIs [LeadsTo_Un, |
183 |
LeadsTo_weaken_R]) 1); |
|
184 |
qed "LeadsTo_Un_Un"; |
|
185 |
||
186 |
||
187 |
(** The cancellation law **) |
|
188 |
||
5253 | 189 |
Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \ |
5257 | 190 |
\ id: (Acts prg) |] \ |
191 |
\ ==> LeadsTo prg A (A' Un B')"; |
|
4776 | 192 |
by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
193 |
subset_imp_LeadsTo, LeadsTo_Trans]) 1); |
|
194 |
qed "LeadsTo_cancel2"; |
|
195 |
||
5253 | 196 |
Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: (Acts prg) |] \ |
5257 | 197 |
\ ==> LeadsTo prg A (A' Un B')"; |
4776 | 198 |
by (rtac LeadsTo_cancel2 1); |
199 |
by (assume_tac 2); |
|
200 |
by (ALLGOALS Asm_simp_tac); |
|
201 |
qed "LeadsTo_cancel_Diff2"; |
|
202 |
||
5253 | 203 |
Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: (Acts prg) |] \ |
5257 | 204 |
\ ==> LeadsTo prg A (B' Un A')"; |
4776 | 205 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
206 |
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
|
207 |
qed "LeadsTo_cancel1"; |
|
208 |
||
5253 | 209 |
Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: (Acts prg) |] \ |
5257 | 210 |
\ ==> LeadsTo prg A (B' Un A')"; |
4776 | 211 |
by (rtac LeadsTo_cancel1 1); |
212 |
by (assume_tac 2); |
|
213 |
by (ALLGOALS Asm_simp_tac); |
|
214 |
qed "LeadsTo_cancel_Diff1"; |
|
215 |
||
216 |
||
217 |
||
218 |
(** The impossibility law **) |
|
219 |
||
5253 | 220 |
Goal "LeadsTo prg A {} ==> reachable prg Int A = {}"; |
5111 | 221 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 222 |
by (etac leadsTo_empty 1); |
223 |
qed "LeadsTo_empty"; |
|
224 |
||
225 |
||
226 |
(** PSP: Progress-Safety-Progress **) |
|
227 |
||
228 |
(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *) |
|
5253 | 229 |
Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \ |
5257 | 230 |
\ ==> LeadsTo prg (A Int B) (A' Int B)"; |
5111 | 231 |
by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, |
232 |
PSP_stable]) 1); |
|
4776 | 233 |
qed "R_PSP_stable"; |
234 |
||
5253 | 235 |
Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \ |
5257 | 236 |
\ ==> LeadsTo prg (B Int A) (B Int A')"; |
4776 | 237 |
by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1); |
238 |
qed "R_PSP_stable2"; |
|
239 |
||
240 |
||
5253 | 241 |
Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \ |
5257 | 242 |
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))"; |
5111 | 243 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 244 |
by (dtac PSP 1); |
245 |
by (etac constrains_reachable 1); |
|
246 |
by (etac leadsTo_weaken 2); |
|
247 |
by (ALLGOALS Blast_tac); |
|
248 |
qed "R_PSP"; |
|
249 |
||
5253 | 250 |
Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \ |
5257 | 251 |
\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))"; |
4776 | 252 |
by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1); |
253 |
qed "R_PSP2"; |
|
254 |
||
5069 | 255 |
Goalw [unless_def] |
5253 | 256 |
"[| LeadsTo prg A A'; unless (Acts prg) B B'; id: (Acts prg) |] \ |
5257 | 257 |
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un B')"; |
4776 | 258 |
by (dtac R_PSP 1); |
259 |
by (assume_tac 1); |
|
260 |
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); |
|
261 |
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2); |
|
262 |
by (etac LeadsTo_Diff 2); |
|
263 |
by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2); |
|
264 |
by Auto_tac; |
|
265 |
qed "R_PSP_unless"; |
|
266 |
||
267 |
||
268 |
(*** Induction rules ***) |
|
269 |
||
270 |
(** Meta or object quantifier ????? **) |
|
5232 | 271 |
Goal "[| wf r; \ |
5257 | 272 |
\ ALL m. LeadsTo prg (A Int f-``{m}) \ |
273 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ |
|
274 |
\ id: (Acts prg) |] \ |
|
275 |
\ ==> LeadsTo prg A B"; |
|
5111 | 276 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 277 |
by (etac leadsTo_wf_induct 1); |
278 |
by (assume_tac 2); |
|
279 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
|
280 |
qed "LeadsTo_wf_induct"; |
|
281 |
||
282 |
||
5232 | 283 |
Goal "[| wf r; \ |
5253 | 284 |
\ ALL m:I. LeadsTo prg (A Int f-``{m}) \ |
5257 | 285 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ |
5253 | 286 |
\ id: (Acts prg) |] \ |
287 |
\ ==> LeadsTo prg A ((A - (f-``I)) Un B)"; |
|
4776 | 288 |
by (etac LeadsTo_wf_induct 1); |
289 |
by Safe_tac; |
|
290 |
by (case_tac "m:I" 1); |
|
291 |
by (blast_tac (claset() addIs [LeadsTo_weaken]) 1); |
|
292 |
by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1); |
|
293 |
qed "R_bounded_induct"; |
|
294 |
||
295 |
||
5253 | 296 |
Goal "[| ALL m. LeadsTo prg (A Int f-``{m}) \ |
297 |
\ ((A Int f-``(lessThan m)) Un B); \ |
|
298 |
\ id: (Acts prg) |] \ |
|
299 |
\ ==> LeadsTo prg A B"; |
|
4776 | 300 |
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); |
301 |
by (assume_tac 2); |
|
302 |
by (Asm_simp_tac 1); |
|
303 |
qed "R_lessThan_induct"; |
|
304 |
||
5253 | 305 |
Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m}) \ |
4776 | 306 |
\ ((A Int f-``(lessThan m)) Un B); \ |
5253 | 307 |
\ id: (Acts prg) |] \ |
308 |
\ ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)"; |
|
4776 | 309 |
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1); |
310 |
by (rtac (wf_less_than RS R_bounded_induct) 1); |
|
311 |
by (assume_tac 2); |
|
312 |
by (Asm_simp_tac 1); |
|
313 |
qed "R_lessThan_bounded_induct"; |
|
314 |
||
5253 | 315 |
Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m}) \ |
5232 | 316 |
\ ((A Int f-``(greaterThan m)) Un B); \ |
5253 | 317 |
\ id: (Acts prg) |] \ |
318 |
\ ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)"; |
|
4776 | 319 |
by (res_inst_tac [("f","f"),("f1", "%k. l - k")] |
320 |
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1); |
|
321 |
by (assume_tac 2); |
|
322 |
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); |
|
323 |
by (Clarify_tac 1); |
|
324 |
by (case_tac "m<l" 1); |
|
325 |
by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2); |
|
326 |
by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1); |
|
327 |
qed "R_greaterThan_bounded_induct"; |
|
328 |
||
329 |
||
330 |
||
331 |
(*** Completion: Binary and General Finite versions ***) |
|
332 |
||
5253 | 333 |
Goal "[| LeadsTo prg A A'; stable (Acts prg) A'; \ |
334 |
\ LeadsTo prg B B'; stable (Acts prg) B'; id: (Acts prg) |] \ |
|
335 |
\ ==> LeadsTo prg (A Int B) (A' Int B')"; |
|
5111 | 336 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
4776 | 337 |
by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] |
338 |
addSIs [stable_Int, stable_reachable]) 1); |
|
339 |
qed "R_stable_completion"; |
|
340 |
||
341 |
||
5253 | 342 |
Goal "[| finite I; id: (Acts prg) |] \ |
343 |
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i)) --> \ |
|
344 |
\ (ALL i:I. stable (Acts prg) (A' i)) --> \ |
|
345 |
\ LeadsTo prg (INT i:I. A i) (INT i:I. A' i)"; |
|
4776 | 346 |
by (etac finite_induct 1); |
347 |
by (Asm_simp_tac 1); |
|
348 |
by (asm_simp_tac |
|
349 |
(simpset() addsimps [R_stable_completion, stable_def, |
|
350 |
ball_constrains_INT]) 1); |
|
351 |
qed_spec_mp "R_finite_stable_completion"; |
|
352 |
||
353 |
||
5253 | 354 |
Goal "[| LeadsTo prg A (A' Un C); constrains (Acts prg) A' (A' Un C); \ |
355 |
\ LeadsTo prg B (B' Un C); constrains (Acts prg) B' (B' Un C); \ |
|
356 |
\ id: (Acts prg) |] \ |
|
357 |
\ ==> LeadsTo prg (A Int B) ((A' Int B') Un C)"; |
|
5111 | 358 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1); |
4776 | 359 |
by (dtac completion 1); |
360 |
by (assume_tac 2); |
|
361 |
by (ALLGOALS |
|
362 |
(asm_simp_tac |
|
363 |
(simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym]))); |
|
364 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
|
365 |
qed "R_completion"; |
|
366 |
||
367 |
||
5253 | 368 |
Goal "[| finite I; id: (Acts prg) |] \ |
369 |
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) --> \ |
|
370 |
\ (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \ |
|
371 |
\ LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)"; |
|
4776 | 372 |
by (etac finite_induct 1); |
373 |
by (ALLGOALS Asm_simp_tac); |
|
374 |
by (Clarify_tac 1); |
|
375 |
by (dtac ball_constrains_INT 1); |
|
376 |
by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); |
|
377 |
qed "R_finite_completion"; |
|
378 |
||
5232 | 379 |
|
380 |
||
381 |
(*** Specialized laws for handling invariants ***) |
|
382 |
||
383 |
Goalw [transient_def] |
|
5253 | 384 |
"[| reachable prg <= INV; transient (Acts prg) (INV Int A) |] \ |
385 |
\ ==> transient (Acts prg) (reachable prg Int A)"; |
|
5232 | 386 |
by (Clarify_tac 1); |
387 |
by (rtac bexI 1); |
|
388 |
by (assume_tac 2); |
|
389 |
by (Blast_tac 1); |
|
390 |
qed "reachable_transient"; |
|
391 |
||
5253 | 392 |
(*Uses the premise "invariant prg". Raw theorem-proving on this |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
393 |
inclusion is slow: the term contains a copy of the program.*) |
5253 | 394 |
Goal "[| invariant prg INV; \ |
395 |
\ constrains (Acts prg) (INV Int (A-A')) (A Un A'); \ |
|
396 |
\ transient (Acts prg) (INV Int (A-A')) |] \ |
|
397 |
\ ==> ensures (Acts prg) (reachable prg Int A) (reachable prg Int A')"; |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
398 |
bd invariant_includes_reachable 1; |
5253 | 399 |
by (rtac ensuresI 1); |
400 |
by (ALLGOALS |
|
401 |
(full_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, |
|
402 |
Diff_Int_distrib RS sym]))); |
|
5232 | 403 |
by (blast_tac (claset() addSIs [reachable_transient]) 2); |
5253 | 404 |
br (stable_reachable RS stable_constrains_Int) 1; |
405 |
by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
406 |
qed "invariant_ensuresI"; |
|
407 |
||
408 |
bind_thm ("invariant_LeadsTo_Basis", invariant_ensuresI RS LeadsTo_Basis); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
409 |
|
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
410 |
|
5253 | 411 |
Goal "[| invariant prg INV; \ |
412 |
\ LeadsTo prg A A'; id: (Acts prg); \ |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
413 |
\ INV Int B <= A; INV Int A' <= B' |] \ |
5253 | 414 |
\ ==> LeadsTo prg B B'"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
415 |
by (blast_tac (claset() addDs [invariant_includes_reachable] |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
416 |
addIs [LeadsTo_weaken]) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
417 |
qed "invariant_LeadsTo_weaken"; |
5232 | 418 |
|
419 |
||
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
420 |
(** Constrains/Ensures tactics |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
421 |
main_def defines the main program as a set; |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
422 |
cmd_defs defines the separate commands |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
423 |
**) |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
424 |
|
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
425 |
(*proves "constrains" properties when the program is specified*) |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
426 |
fun constrains_tac (main_def::cmd_defs) = |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
427 |
SELECT_GOAL |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
428 |
(EVERY [TRY (rtac stableI 1), |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
429 |
rtac constrainsI 1, |
5253 | 430 |
full_simp_tac (simpset() addsimps [main_def]) 1, |
431 |
REPEAT_FIRST (eresolve_tac [disjE]), |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
432 |
rewrite_goals_tac cmd_defs, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
433 |
ALLGOALS (SELECT_GOAL Auto_tac)]); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
434 |
|
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
435 |
|
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
436 |
(*proves "ensures" properties when the program is specified*) |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
437 |
fun ensures_tac (main_def::cmd_defs) sact = |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
438 |
SELECT_GOAL |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
439 |
(EVERY [REPEAT (invariant_Int_tac 1), |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
440 |
etac invariant_LeadsTo_Basis 1 |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
441 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
442 |
REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
443 |
ensuresI] 1), |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
444 |
res_inst_tac [("act", sact)] transient_mem 2, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
445 |
simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
446 |
simp_tac (simpset() addsimps [main_def]) 2, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
447 |
constrains_tac (main_def::cmd_defs) 1, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
448 |
rewrite_goals_tac cmd_defs, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
449 |
ALLGOALS Clarify_tac, |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
450 |
Auto_tac]); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
451 |
|
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
452 |