author | paulson |
Tue, 13 Oct 1998 11:05:34 +0200 | |
changeset 5640 | 4a59d99b5ca3 |
parent 5620 | 3ac11c4af76a |
child 5648 | fe887910e32e |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/WFair |
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 |
||
11 |
||
5340 | 12 |
(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*) |
13 |
Blast.overloaded ("WFair.leadsto", |
|
14 |
#1 o HOLogic.dest_prodT o |
|
15 |
HOLogic.dest_setT o HOLogic.dest_setT o domain_type); |
|
16 |
||
17 |
overload_2nd_set "WFair.transient"; |
|
18 |
overload_2nd_set "WFair.ensures"; |
|
19 |
||
4776 | 20 |
(*** transient ***) |
21 |
||
5069 | 22 |
Goalw [stable_def, constrains_def, transient_def] |
5253 | 23 |
"[| stable acts A; transient acts A |] ==> A = {}"; |
4776 | 24 |
by (Blast_tac 1); |
25 |
qed "stable_transient_empty"; |
|
26 |
||
5069 | 27 |
Goalw [transient_def] |
5253 | 28 |
"[| transient acts A; B<=A |] ==> transient acts B"; |
4776 | 29 |
by (Clarify_tac 1); |
30 |
by (rtac bexI 1 THEN assume_tac 2); |
|
31 |
by (Blast_tac 1); |
|
32 |
qed "transient_strengthen"; |
|
33 |
||
5069 | 34 |
Goalw [transient_def] |
5490 | 35 |
"[| act:acts; A <= Domain act; act^^A <= -A |] ==> transient acts A"; |
4776 | 36 |
by (Blast_tac 1); |
37 |
qed "transient_mem"; |
|
38 |
||
39 |
||
40 |
(*** ensures ***) |
|
41 |
||
5069 | 42 |
Goalw [ensures_def] |
5253 | 43 |
"[| constrains acts (A-B) (A Un B); transient acts (A-B) |] \ |
44 |
\ ==> ensures acts A B"; |
|
4776 | 45 |
by (Blast_tac 1); |
46 |
qed "ensuresI"; |
|
47 |
||
5069 | 48 |
Goalw [ensures_def] |
5253 | 49 |
"ensures acts A B \ |
50 |
\ ==> constrains acts (A-B) (A Un B) & transient acts (A-B)"; |
|
4776 | 51 |
by (Blast_tac 1); |
52 |
qed "ensuresD"; |
|
53 |
||
54 |
(*The L-version (precondition strengthening) doesn't hold for ENSURES*) |
|
5069 | 55 |
Goalw [ensures_def] |
5253 | 56 |
"[| ensures acts A A'; A'<=B' |] ==> ensures acts A B'"; |
4776 | 57 |
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
58 |
qed "ensures_weaken_R"; |
|
59 |
||
5069 | 60 |
Goalw [ensures_def, constrains_def, transient_def] |
5253 | 61 |
"acts ~= {} ==> ensures acts A UNIV"; |
5340 | 62 |
by Auto_tac; |
4776 | 63 |
qed "ensures_UNIV"; |
64 |
||
5069 | 65 |
Goalw [ensures_def] |
5253 | 66 |
"[| stable acts C; \ |
67 |
\ constrains acts (C Int (A - A')) (A Un A'); \ |
|
68 |
\ transient acts (C Int (A-A')) |] \ |
|
69 |
\ ==> ensures acts (C Int A) (C Int A')"; |
|
4776 | 70 |
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, |
71 |
Diff_Int_distrib RS sym, |
|
72 |
stable_constrains_Int]) 1); |
|
73 |
qed "stable_ensures_Int"; |
|
74 |
||
5640 | 75 |
Goal "[| stable acts A; transient acts C; A <= B Un C |] \ |
76 |
\ ==> ensures acts A B"; |
|
77 |
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
|
78 |
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
|
79 |
qed "stable_transient_ensures"; |
|
80 |
||
4776 | 81 |
|
82 |
(*** leadsTo ***) |
|
83 |
||
84 |
(*Synonyms for the theorems produced by the inductive defn package*) |
|
85 |
bind_thm ("leadsTo_Basis", leadsto.Basis); |
|
86 |
bind_thm ("leadsTo_Trans", leadsto.Trans); |
|
87 |
||
5640 | 88 |
Goal "transient acts A ==> leadsTo acts A (-A)"; |
89 |
by (asm_simp_tac |
|
90 |
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); |
|
91 |
qed "transient_imp_leadsTo"; |
|
92 |
||
5253 | 93 |
Goal "act: acts ==> leadsTo acts A UNIV"; |
4776 | 94 |
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1); |
95 |
qed "leadsTo_UNIV"; |
|
96 |
Addsimps [leadsTo_UNIV]; |
|
97 |
||
98 |
(*Useful with cancellation, disjunction*) |
|
5253 | 99 |
Goal "leadsTo acts A (A' Un A') ==> leadsTo acts A A'"; |
4776 | 100 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
101 |
qed "leadsTo_Un_duplicate"; |
|
102 |
||
5253 | 103 |
Goal "leadsTo acts A (A' Un C Un C) ==> leadsTo acts A (A' Un C)"; |
4776 | 104 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
105 |
qed "leadsTo_Un_duplicate2"; |
|
106 |
||
107 |
(*The Union introduction rule as we should have liked to state it*) |
|
108 |
val prems = goal thy |
|
5253 | 109 |
"(!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B"; |
4776 | 110 |
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1); |
111 |
qed "leadsTo_Union"; |
|
112 |
||
113 |
val prems = goal thy |
|
5253 | 114 |
"(!!i. i : I ==> leadsTo acts (A i) B) ==> leadsTo acts (UN i:I. A i) B"; |
4776 | 115 |
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
116 |
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1); |
|
117 |
qed "leadsTo_UN"; |
|
118 |
||
119 |
(*Binary union introduction rule*) |
|
5253 | 120 |
Goal "[| leadsTo acts A C; leadsTo acts B C |] ==> leadsTo acts (A Un B) C"; |
4776 | 121 |
by (stac Un_eq_Union 1); |
122 |
by (blast_tac (claset() addIs [leadsTo_Union]) 1); |
|
123 |
qed "leadsTo_Un"; |
|
124 |
||
125 |
||
126 |
(*The INDUCTION rule as we should have liked to state it*) |
|
127 |
val major::prems = goal thy |
|
5253 | 128 |
"[| leadsTo acts za zb; \ |
129 |
\ !!A B. ensures acts A B ==> P A B; \ |
|
130 |
\ !!A B C. [| leadsTo acts A B; P A B; leadsTo acts B C; P B C |] \ |
|
4776 | 131 |
\ ==> P A C; \ |
5253 | 132 |
\ !!B S. ALL A:S. leadsTo acts A B & P A B ==> P (Union S) B \ |
4776 | 133 |
\ |] ==> P za zb"; |
5232 | 134 |
by (rtac (major RS leadsto.induct) 1); |
4776 | 135 |
by (REPEAT (blast_tac (claset() addIs prems) 1)); |
136 |
qed "leadsTo_induct"; |
|
137 |
||
138 |
||
5608 | 139 |
Goal "[| A<=B; Id: acts |] ==> leadsTo acts A B"; |
4776 | 140 |
by (rtac leadsTo_Basis 1); |
141 |
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); |
|
142 |
by (Blast_tac 1); |
|
143 |
qed "subset_imp_leadsTo"; |
|
144 |
||
145 |
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); |
|
146 |
Addsimps [empty_leadsTo]; |
|
147 |
||
148 |
||
149 |
(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it |
|
5608 | 150 |
needs the extra premise Id:acts*) |
5253 | 151 |
Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'"; |
4776 | 152 |
by (etac leadsTo_induct 1); |
153 |
by (Clarify_tac 3); |
|
154 |
by (blast_tac (claset() addIs [leadsTo_Union]) 3); |
|
155 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
156 |
by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1); |
|
157 |
qed_spec_mp "leadsTo_weaken_R"; |
|
158 |
||
159 |
||
5608 | 160 |
Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==> \ |
5253 | 161 |
\ leadsTo acts B A'"; |
4776 | 162 |
by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, |
163 |
subset_imp_leadsTo]) 1); |
|
164 |
qed_spec_mp "leadsTo_weaken_L"; |
|
165 |
||
166 |
(*Distributes over binary unions*) |
|
5608 | 167 |
Goal "Id: acts ==> \ |
5253 | 168 |
\ leadsTo acts (A Un B) C = (leadsTo acts A C & leadsTo acts B C)"; |
4776 | 169 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); |
170 |
qed "leadsTo_Un_distrib"; |
|
171 |
||
5608 | 172 |
Goal "Id: acts ==> \ |
5253 | 173 |
\ leadsTo acts (UN i:I. A i) B = (ALL i : I. leadsTo acts (A i) B)"; |
4776 | 174 |
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); |
175 |
qed "leadsTo_UN_distrib"; |
|
176 |
||
5608 | 177 |
Goal "Id: acts ==> \ |
5253 | 178 |
\ leadsTo acts (Union S) B = (ALL A : S. leadsTo acts A B)"; |
4776 | 179 |
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); |
180 |
qed "leadsTo_Union_distrib"; |
|
181 |
||
182 |
||
5608 | 183 |
Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \ |
5253 | 184 |
\ ==> leadsTo acts B B'"; |
5340 | 185 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, |
186 |
leadsTo_Trans]) 1); |
|
4776 | 187 |
qed "leadsTo_weaken"; |
188 |
||
189 |
||
190 |
(*Set difference: maybe combine with leadsTo_weaken_L??*) |
|
5608 | 191 |
Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \ |
5253 | 192 |
\ ==> leadsTo acts A C"; |
4776 | 193 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); |
194 |
qed "leadsTo_Diff"; |
|
195 |
||
196 |
||
197 |
(** Meta or object quantifier ??? |
|
198 |
see ball_constrains_UN in UNITY.ML***) |
|
199 |
||
200 |
val prems = goal thy |
|
5253 | 201 |
"(!! i. i:I ==> leadsTo acts (A i) (A' i)) \ |
202 |
\ ==> leadsTo acts (UN i:I. A i) (UN i:I. A' i)"; |
|
4776 | 203 |
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
204 |
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] |
|
205 |
addIs prems) 1); |
|
206 |
qed "leadsTo_UN_UN"; |
|
207 |
||
208 |
||
209 |
(*Version with no index set*) |
|
210 |
val prems = goal thy |
|
5253 | 211 |
"(!! i. leadsTo acts (A i) (A' i)) \ |
212 |
\ ==> leadsTo acts (UN i. A i) (UN i. A' i)"; |
|
4776 | 213 |
by (blast_tac (claset() addIs [leadsTo_UN_UN] |
214 |
addIs prems) 1); |
|
215 |
qed "leadsTo_UN_UN_noindex"; |
|
216 |
||
217 |
(*Version with no index set*) |
|
5253 | 218 |
Goal "ALL i. leadsTo acts (A i) (A' i) \ |
219 |
\ ==> leadsTo acts (UN i. A i) (UN i. A' i)"; |
|
4776 | 220 |
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1); |
221 |
qed "all_leadsTo_UN_UN"; |
|
222 |
||
223 |
||
224 |
(*Binary union version*) |
|
5253 | 225 |
Goal "[| leadsTo acts A A'; leadsTo acts B B' |] \ |
226 |
\ ==> leadsTo acts (A Un B) (A' Un B')"; |
|
4776 | 227 |
by (blast_tac (claset() addIs [leadsTo_Un, |
228 |
leadsTo_weaken_R]) 1); |
|
229 |
qed "leadsTo_Un_Un"; |
|
230 |
||
231 |
||
232 |
(** The cancellation law **) |
|
233 |
||
5608 | 234 |
Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \ |
5253 | 235 |
\ ==> leadsTo acts A (A' Un B')"; |
4776 | 236 |
by (blast_tac (claset() addIs [leadsTo_Un_Un, |
237 |
subset_imp_leadsTo, leadsTo_Trans]) 1); |
|
238 |
qed "leadsTo_cancel2"; |
|
239 |
||
5608 | 240 |
Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \ |
5253 | 241 |
\ ==> leadsTo acts A (A' Un B')"; |
4776 | 242 |
by (rtac leadsTo_cancel2 1); |
243 |
by (assume_tac 2); |
|
244 |
by (ALLGOALS Asm_simp_tac); |
|
245 |
qed "leadsTo_cancel_Diff2"; |
|
246 |
||
5608 | 247 |
Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \ |
5253 | 248 |
\ ==> leadsTo acts A (B' Un A')"; |
4776 | 249 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
250 |
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); |
|
251 |
qed "leadsTo_cancel1"; |
|
252 |
||
5608 | 253 |
Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \ |
5253 | 254 |
\ ==> leadsTo acts A (B' Un A')"; |
4776 | 255 |
by (rtac leadsTo_cancel1 1); |
256 |
by (assume_tac 2); |
|
257 |
by (ALLGOALS Asm_simp_tac); |
|
258 |
qed "leadsTo_cancel_Diff1"; |
|
259 |
||
260 |
||
261 |
||
262 |
(** The impossibility law **) |
|
263 |
||
5253 | 264 |
Goal "leadsTo acts A B ==> B={} --> A={}"; |
4776 | 265 |
by (etac leadsTo_induct 1); |
266 |
by (ALLGOALS Asm_simp_tac); |
|
267 |
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); |
|
268 |
by (Blast_tac 1); |
|
269 |
val lemma = result() RS mp; |
|
270 |
||
5253 | 271 |
Goal "leadsTo acts A {} ==> A={}"; |
4776 | 272 |
by (blast_tac (claset() addSIs [lemma]) 1); |
273 |
qed "leadsTo_empty"; |
|
274 |
||
275 |
||
276 |
(** PSP: Progress-Safety-Progress **) |
|
277 |
||
5640 | 278 |
(*Special case of PSP: Misra's "stable conjunction"*) |
5069 | 279 |
Goalw [stable_def] |
5253 | 280 |
"[| leadsTo acts A A'; stable acts B |] \ |
281 |
\ ==> leadsTo acts (A Int B) (A' Int B)"; |
|
4776 | 282 |
by (etac leadsTo_induct 1); |
283 |
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); |
|
284 |
by (blast_tac (claset() addIs [leadsTo_Union]) 3); |
|
285 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
|
286 |
by (rtac leadsTo_Basis 1); |
|
287 |
by (asm_full_simp_tac |
|
288 |
(simpset() addsimps [ensures_def, |
|
289 |
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); |
|
290 |
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
291 |
qed "psp_stable"; |
4776 | 292 |
|
5253 | 293 |
Goal "[| leadsTo acts A A'; stable acts B |] \ |
294 |
\ ==> leadsTo acts (B Int A) (B Int A')"; |
|
5536 | 295 |
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
296 |
qed "psp_stable2"; |
4776 | 297 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
298 |
Goalw [ensures_def, constrains_def] |
5253 | 299 |
"[| ensures acts A A'; constrains acts B B' |] \ |
300 |
\ ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))"; |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
301 |
by (blast_tac (claset() addIs [transient_strengthen]) 1); |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
302 |
qed "psp_ensures"; |
4776 | 303 |
|
5608 | 304 |
Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \ |
5253 | 305 |
\ ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))"; |
4776 | 306 |
by (etac leadsTo_induct 1); |
307 |
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); |
|
308 |
by (blast_tac (claset() addIs [leadsTo_Union]) 3); |
|
309 |
(*Transitivity case has a delicate argument involving "cancellation"*) |
|
310 |
by (rtac leadsTo_Un_duplicate2 2); |
|
311 |
by (etac leadsTo_cancel_Diff1 2); |
|
312 |
by (assume_tac 3); |
|
313 |
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); |
|
314 |
(*Basis case*) |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
315 |
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1); |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
316 |
qed "psp"; |
4776 | 317 |
|
5608 | 318 |
Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \ |
5253 | 319 |
\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))"; |
5536 | 320 |
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
321 |
qed "psp2"; |
4776 | 322 |
|
323 |
||
5069 | 324 |
Goalw [unless_def] |
5608 | 325 |
"[| leadsTo acts A A'; unless acts B B'; Id: acts |] \ |
5253 | 326 |
\ ==> leadsTo acts (A Int B) ((A' Int B) Un B')"; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
327 |
by (dtac psp 1); |
4776 | 328 |
by (assume_tac 1); |
329 |
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); |
|
330 |
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2); |
|
331 |
by (etac leadsTo_Diff 2); |
|
332 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2); |
|
333 |
by Auto_tac; |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
334 |
qed "psp_unless"; |
4776 | 335 |
|
336 |
||
337 |
(*** Proving the induction rules ***) |
|
338 |
||
5257 | 339 |
(** The most general rule: r is any wf relation; f is any variant function **) |
340 |
||
5239 | 341 |
Goal "[| wf r; \ |
5253 | 342 |
\ ALL m. leadsTo acts (A Int f-``{m}) \ |
5239 | 343 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ |
5608 | 344 |
\ Id: acts |] \ |
5253 | 345 |
\ ==> leadsTo acts (A Int f-``{m}) B"; |
4776 | 346 |
by (eres_inst_tac [("a","m")] wf_induct 1); |
5253 | 347 |
by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1); |
4776 | 348 |
by (stac vimage_eq_UN 2); |
349 |
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); |
|
350 |
by (blast_tac (claset() addIs [leadsTo_UN]) 2); |
|
351 |
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); |
|
352 |
val lemma = result(); |
|
353 |
||
354 |
||
355 |
(** Meta or object quantifier ????? **) |
|
5239 | 356 |
Goal "[| wf r; \ |
5253 | 357 |
\ ALL m. leadsTo acts (A Int f-``{m}) \ |
5239 | 358 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ |
5608 | 359 |
\ Id: acts |] \ |
5253 | 360 |
\ ==> leadsTo acts A B"; |
4776 | 361 |
by (res_inst_tac [("t", "A")] subst 1); |
362 |
by (rtac leadsTo_UN 2); |
|
363 |
by (etac lemma 2); |
|
364 |
by (REPEAT (assume_tac 2)); |
|
365 |
by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*) |
|
366 |
qed "leadsTo_wf_induct"; |
|
367 |
||
368 |
||
5239 | 369 |
Goal "[| wf r; \ |
5253 | 370 |
\ ALL m:I. leadsTo acts (A Int f-``{m}) \ |
5257 | 371 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ |
5608 | 372 |
\ Id: acts |] \ |
5253 | 373 |
\ ==> leadsTo acts A ((A - (f-``I)) Un B)"; |
4776 | 374 |
by (etac leadsTo_wf_induct 1); |
375 |
by Safe_tac; |
|
376 |
by (case_tac "m:I" 1); |
|
377 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
|
378 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
379 |
qed "bounded_induct"; |
|
380 |
||
381 |
||
5253 | 382 |
(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*) |
383 |
Goal "[| ALL m. leadsTo acts (A Int f-``{m}) \ |
|
5239 | 384 |
\ ((A Int f-``(lessThan m)) Un B); \ |
5608 | 385 |
\ Id: acts |] \ |
5253 | 386 |
\ ==> leadsTo acts A B"; |
4776 | 387 |
by (rtac (wf_less_than RS leadsTo_wf_induct) 1); |
388 |
by (assume_tac 2); |
|
389 |
by (Asm_simp_tac 1); |
|
390 |
qed "lessThan_induct"; |
|
391 |
||
5253 | 392 |
Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m}) \ |
5239 | 393 |
\ ((A Int f-``(lessThan m)) Un B); \ |
5608 | 394 |
\ Id: acts |] \ |
5253 | 395 |
\ ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)"; |
4776 | 396 |
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1); |
397 |
by (rtac (wf_less_than RS bounded_induct) 1); |
|
398 |
by (assume_tac 2); |
|
399 |
by (Asm_simp_tac 1); |
|
400 |
qed "lessThan_bounded_induct"; |
|
401 |
||
5253 | 402 |
Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m}) \ |
5239 | 403 |
\ ((A Int f-``(greaterThan m)) Un B); \ |
5608 | 404 |
\ Id: acts |] \ |
5253 | 405 |
\ ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)"; |
4776 | 406 |
by (res_inst_tac [("f","f"),("f1", "%k. l - k")] |
407 |
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); |
|
408 |
by (assume_tac 2); |
|
409 |
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); |
|
410 |
by (Clarify_tac 1); |
|
411 |
by (case_tac "m<l" 1); |
|
412 |
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2); |
|
413 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1); |
|
414 |
qed "greaterThan_bounded_induct"; |
|
415 |
||
416 |
||
417 |
||
418 |
(*** wlt ****) |
|
419 |
||
420 |
(*Misra's property W3*) |
|
5253 | 421 |
Goalw [wlt_def] "leadsTo acts (wlt acts B) B"; |
4776 | 422 |
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); |
423 |
qed "wlt_leadsTo"; |
|
424 |
||
5253 | 425 |
Goalw [wlt_def] "leadsTo acts A B ==> A <= wlt acts B"; |
4776 | 426 |
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); |
427 |
qed "leadsTo_subset"; |
|
428 |
||
429 |
(*Misra's property W2*) |
|
5608 | 430 |
Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)"; |
4776 | 431 |
by (blast_tac (claset() addSIs [leadsTo_subset, |
432 |
wlt_leadsTo RS leadsTo_weaken_L]) 1); |
|
433 |
qed "leadsTo_eq_subset_wlt"; |
|
434 |
||
435 |
(*Misra's property W4*) |
|
5608 | 436 |
Goal "Id: acts ==> B <= wlt acts B"; |
4776 | 437 |
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, |
438 |
subset_imp_leadsTo]) 1); |
|
439 |
qed "wlt_increasing"; |
|
440 |
||
441 |
||
442 |
(*Used in the Trans case below*) |
|
5069 | 443 |
Goalw [constrains_def] |
5111 | 444 |
"[| B <= A2; \ |
5253 | 445 |
\ constrains acts (A1 - B) (A1 Un B); \ |
446 |
\ constrains acts (A2 - C) (A2 Un C) |] \ |
|
447 |
\ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)"; |
|
5620 | 448 |
by (Blast_tac 1); |
4776 | 449 |
val lemma1 = result(); |
450 |
||
451 |
||
452 |
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
|
5608 | 453 |
Goal "[| leadsTo acts A A'; Id: acts |] ==> \ |
5253 | 454 |
\ EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')"; |
4776 | 455 |
by (etac leadsTo_induct 1); |
456 |
(*Basis*) |
|
457 |
by (blast_tac (claset() addIs [leadsTo_Basis] |
|
458 |
addDs [ensuresD]) 1); |
|
459 |
(*Trans*) |
|
460 |
by (Clarify_tac 1); |
|
461 |
by (res_inst_tac [("x", "Ba Un Bb")] exI 1); |
|
462 |
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1, |
|
463 |
leadsTo_Un_duplicate]) 1); |
|
464 |
(*Union*) |
|
465 |
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, |
|
466 |
bchoice, ball_constrains_UN]) 1);; |
|
467 |
by (res_inst_tac [("x", "UN A:S. f A")] exI 1); |
|
468 |
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1); |
|
469 |
qed "leadsTo_123"; |
|
470 |
||
471 |
||
472 |
(*Misra's property W5*) |
|
5608 | 473 |
Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)"; |
4776 | 474 |
by (forward_tac [wlt_leadsTo RS leadsTo_123] 1); |
475 |
by (Clarify_tac 1); |
|
5253 | 476 |
by (subgoal_tac "Ba = wlt acts B" 1); |
4776 | 477 |
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2); |
478 |
by (Clarify_tac 1); |
|
479 |
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); |
|
480 |
qed "wlt_constrains_wlt"; |
|
481 |
||
482 |
||
483 |
(*** Completion: Binary and General Finite versions ***) |
|
484 |
||
5253 | 485 |
Goal "[| leadsTo acts A A'; stable acts A'; \ |
5608 | 486 |
\ leadsTo acts B B'; stable acts B'; Id: acts |] \ |
5253 | 487 |
\ ==> leadsTo acts (A Int B) (A' Int B')"; |
488 |
by (subgoal_tac "stable acts (wlt acts B')" 1); |
|
4776 | 489 |
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2); |
490 |
by (EVERY [etac (constrains_Un RS constrains_weaken) 2, |
|
491 |
etac wlt_constrains_wlt 2, |
|
492 |
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3, |
|
493 |
Blast_tac 2]); |
|
5253 | 494 |
by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
495 |
by (blast_tac (claset() addIs [psp_stable]) 2); |
5253 | 496 |
by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
497 |
by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2); |
5253 | 498 |
by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1); |
4776 | 499 |
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, |
500 |
subset_imp_leadsTo]) 2); |
|
5479 | 501 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
4776 | 502 |
qed "stable_completion"; |
503 |
||
504 |
||
5608 | 505 |
Goal "[| finite I; Id: acts |] \ |
5253 | 506 |
\ ==> (ALL i:I. leadsTo acts (A i) (A' i)) --> \ |
507 |
\ (ALL i:I. stable acts (A' i)) --> \ |
|
508 |
\ leadsTo acts (INT i:I. A i) (INT i:I. A' i)"; |
|
4776 | 509 |
by (etac finite_induct 1); |
510 |
by (Asm_simp_tac 1); |
|
511 |
by (asm_simp_tac |
|
512 |
(simpset() addsimps [stable_completion, stable_def, |
|
513 |
ball_constrains_INT]) 1); |
|
514 |
qed_spec_mp "finite_stable_completion"; |
|
515 |
||
516 |
||
5253 | 517 |
Goal "[| W = wlt acts (B' Un C); \ |
518 |
\ leadsTo acts A (A' Un C); constrains acts A' (A' Un C); \ |
|
519 |
\ leadsTo acts B (B' Un C); constrains acts B' (B' Un C); \ |
|
5608 | 520 |
\ Id: acts |] \ |
5253 | 521 |
\ ==> leadsTo acts (A Int B) ((A' Int B') Un C)"; |
522 |
by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1); |
|
4776 | 523 |
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] |
524 |
MRS constrains_Un RS constrains_weaken]) 2); |
|
5253 | 525 |
by (subgoal_tac "constrains acts (W-C) W" 1); |
4776 | 526 |
by (asm_full_simp_tac |
527 |
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); |
|
5253 | 528 |
by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1); |
4776 | 529 |
by (simp_tac (simpset() addsimps [Int_Diff]) 2); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
530 |
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2); |
5456 | 531 |
(** LEVEL 7 **) |
5253 | 532 |
by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1); |
4776 | 533 |
by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
534 |
psp2 RS leadsTo_weaken_R, |
4776 | 535 |
subset_refl RS subset_imp_leadsTo, |
536 |
leadsTo_Un_duplicate2]) 2); |
|
537 |
by (dtac leadsTo_Diff 1); |
|
538 |
by (assume_tac 2); |
|
539 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
540 |
by (subgoal_tac "A Int B <= A Int W" 1); |
|
5456 | 541 |
by (blast_tac (claset() addSDs [leadsTo_subset] |
542 |
addSIs [subset_refl RS Int_mono]) 2); |
|
4776 | 543 |
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
544 |
bind_thm("completion", refl RS result()); |
|
545 |
||
546 |
||
5608 | 547 |
Goal "[| finite I; Id: acts |] \ |
5253 | 548 |
\ ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) --> \ |
549 |
\ (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \ |
|
550 |
\ leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)"; |
|
4776 | 551 |
by (etac finite_induct 1); |
552 |
by (ALLGOALS Asm_simp_tac); |
|
553 |
by (Clarify_tac 1); |
|
554 |
by (dtac ball_constrains_INT 1); |
|
555 |
by (asm_full_simp_tac (simpset() addsimps [completion]) 1); |
|
556 |
qed "finite_completion"; |
|
557 |