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