|
1 (* Title: HOL/BCV/Kildall.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 Kildall's algorithm |
|
7 *) |
|
8 |
|
9 header "Kildall's Algorithm" |
|
10 |
|
11 theory Kildall = DFA_Framework: |
|
12 |
|
13 constdefs |
|
14 bounded :: "(nat => nat list) => nat => bool" |
|
15 "bounded succs n == !p<n. !q:set(succs p). q<n" |
|
16 |
|
17 pres_type :: "(nat => 's => 's) => nat => 's set => bool" |
|
18 "pres_type step n A == !s:A. !p<n. step p s : A" |
|
19 |
|
20 mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool" |
|
21 "mono r step n A == |
|
22 !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t" |
|
23 |
|
24 consts |
|
25 iter :: "('s sl * (nat => 's => 's) * (nat => nat list)) |
|
26 * 's list * nat set => 's list" |
|
27 propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set" |
|
28 |
|
29 primrec |
|
30 "propa f [] t ss w = (ss,w)" |
|
31 "propa f (q#qs) t ss w = (let u = t +_f ss!q; |
|
32 w' = (if u = ss!q then w else insert q w) |
|
33 in propa f qs t (ss[q := u]) w')" |
|
34 |
|
35 recdef iter |
|
36 "same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r) |
|
37 (%((A,r,f),step,succs). |
|
38 {(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)" |
|
39 "iter(((A,r,f),step,succs),ss,w) = |
|
40 (if semilat(A,r,f) & acc r & (!p:w. p < size ss) & |
|
41 bounded succs (size ss) & set ss <= A & pres_type step (size ss) A |
|
42 then if w={} then ss |
|
43 else let p = SOME p. p : w |
|
44 in iter(((A,r,f),step,succs), |
|
45 propa f (succs p) (step p (ss!p)) ss (w-{p})) |
|
46 else arbitrary)" |
|
47 |
|
48 constdefs |
|
49 unstables :: |
|
50 "'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set" |
|
51 "unstables f step succs ss == |
|
52 {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}" |
|
53 |
|
54 kildall :: "'s sl => (nat => 's => 's) => (nat => nat list) |
|
55 => 's list => 's list" |
|
56 "kildall Arf step succs ss == |
|
57 iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)" |
|
58 |
|
59 consts merges :: "'s binop => 's => nat list => 's list => 's list" |
|
60 primrec |
|
61 "merges f s [] ss = ss" |
|
62 "merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])" |
|
63 |
|
64 |
|
65 lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]; |
|
66 |
|
67 |
|
68 lemma pres_typeD: |
|
69 "[| pres_type step n A; s:A; p<n |] ==> step p s : A" |
|
70 by (unfold pres_type_def, blast) |
|
71 |
|
72 lemma boundedD: |
|
73 "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n" |
|
74 by (unfold bounded_def, blast) |
|
75 |
|
76 lemma monoD: |
|
77 "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t" |
|
78 by (unfold mono_def, blast) |
|
79 |
|
80 (** merges **) |
|
81 |
|
82 lemma length_merges [rule_format, simp]: |
|
83 "!ss. size(merges f t ps ss) = size ss" |
|
84 by (induct_tac ps, auto) |
|
85 |
|
86 lemma merges_preserves_type [rule_format, simp]: |
|
87 "[| semilat(A,r,f) |] ==> |
|
88 !xs. xs : list n A --> x : A --> (!p : set ps. p<n) |
|
89 --> merges f x ps xs : list n A" |
|
90 apply (frule semilatDclosedI) |
|
91 apply (unfold closed_def) |
|
92 apply (induct_tac ps) |
|
93 apply auto |
|
94 done |
|
95 |
|
96 lemma merges_incr [rule_format]: |
|
97 "[| semilat(A,r,f) |] ==> |
|
98 !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs" |
|
99 apply (induct_tac ps) |
|
100 apply simp |
|
101 apply simp |
|
102 apply clarify |
|
103 apply (rule order_trans) |
|
104 apply simp |
|
105 apply (erule list_update_incr) |
|
106 apply assumption |
|
107 apply simp |
|
108 apply simp |
|
109 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
110 done |
|
111 |
|
112 lemma merges_same_conv [rule_format]: |
|
113 "[| semilat(A,r,f) |] ==> |
|
114 (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) --> |
|
115 (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))" |
|
116 apply (induct_tac ps) |
|
117 apply simp |
|
118 apply clarsimp |
|
119 apply (rename_tac p ps xs) |
|
120 apply (rule iffI) |
|
121 apply (rule context_conjI) |
|
122 apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs") |
|
123 apply (force dest!: le_listD simp add: nth_list_update) |
|
124 apply (erule subst, rule merges_incr) |
|
125 apply assumption |
|
126 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
127 apply assumption |
|
128 apply simp |
|
129 apply clarify |
|
130 apply (rotate_tac -2) |
|
131 apply (erule allE) |
|
132 apply (erule impE) |
|
133 apply assumption |
|
134 apply (erule impE) |
|
135 apply assumption |
|
136 apply (drule bspec) |
|
137 apply assumption |
|
138 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
139 apply clarify |
|
140 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
141 done |
|
142 |
|
143 |
|
144 lemma list_update_le_listI [rule_format]: |
|
145 "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs --> |
|
146 x <=_r ys!p --> semilat(A,r,f) --> x:A --> |
|
147 xs[p := x +_f xs!p] <=[r] ys" |
|
148 apply (unfold Listn.le_def lesub_def semilat_def) |
|
149 apply (simp add: list_all2_conv_all_nth nth_list_update) |
|
150 done |
|
151 |
|
152 lemma merges_pres_le_ub: |
|
153 "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A; |
|
154 !p. p:set ps --> t <=_r ts!p; |
|
155 !p. p:set ps --> p<size ts; |
|
156 ss <=[r] ts |] |
|
157 ==> merges f t ps ss <=[r] ts" |
|
158 proof - |
|
159 { fix A r f t ts ps |
|
160 have |
|
161 "!!qs. [| semilat(A,r,f); set ts <= A; t:A; |
|
162 !p. p:set ps --> t <=_r ts!p; |
|
163 !p. p:set ps --> p<size ts |] ==> |
|
164 set qs <= set ps --> |
|
165 (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)" |
|
166 apply (induct_tac qs) |
|
167 apply simp |
|
168 apply (simp (no_asm_simp)) |
|
169 apply clarify |
|
170 apply (rotate_tac -2) |
|
171 apply simp |
|
172 apply (erule allE, erule impE, erule_tac [2] mp) |
|
173 apply (simp (no_asm_simp) add: closedD) |
|
174 apply (simp add: list_update_le_listI) |
|
175 done |
|
176 } note this [dest] |
|
177 |
|
178 case antecedent |
|
179 thus ?thesis by blast |
|
180 qed |
|
181 |
|
182 |
|
183 lemma nth_merges [rule_format]: |
|
184 "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> |
|
185 (!p:set ps. p<n) --> |
|
186 (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)" |
|
187 apply (induct_tac "ps") |
|
188 apply simp |
|
189 apply (simp add: nth_list_update closedD listE_nth_in) |
|
190 done |
|
191 |
|
192 |
|
193 (** propa **) |
|
194 |
|
195 lemma decomp_propa [rule_format]: |
|
196 "!ss w. (!q:set qs. q < size ss) --> |
|
197 propa f qs t ss w = |
|
198 (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)" |
|
199 apply (induct_tac qs) |
|
200 apply simp |
|
201 apply (simp (no_asm)) |
|
202 apply clarify |
|
203 apply (rule conjI) |
|
204 apply (simp add: nth_list_update) |
|
205 apply blast |
|
206 apply (simp add: nth_list_update) |
|
207 apply blast |
|
208 done |
|
209 |
|
210 (** iter **) |
|
211 |
|
212 ML_setup {* |
|
213 let |
|
214 val thy = the_context () |
|
215 val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter"; |
|
216 in |
|
217 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf)); |
|
218 by (REPEAT(rtac wf_same_fstI 1)); |
|
219 by (split_all_tac 1); |
|
220 by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1); |
|
221 by (REPEAT(rtac wf_same_fstI 1)); |
|
222 by (rtac wf_lex_prod 1); |
|
223 by (rtac wf_finite_psubset 2); |
|
224 by (Clarify_tac 1); |
|
225 by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1); |
|
226 by (assume_tac 1); |
|
227 by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]); |
|
228 by (assume_tac 1); |
|
229 qed "iter_wf" |
|
230 end |
|
231 *} |
|
232 |
|
233 lemma inter_tc_lemma: |
|
234 "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> |
|
235 ss <[r] merges f t qs ss | |
|
236 merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w" |
|
237 apply (unfold lesssub_def) |
|
238 apply (simp (no_asm_simp) add: merges_incr) |
|
239 apply (rule impI) |
|
240 apply (rule merges_same_conv [THEN iffD1, elim_format]) |
|
241 apply assumption+ |
|
242 defer |
|
243 apply (rule sym, assumption) |
|
244 apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric]) |
|
245 apply (blast intro!: psubsetI elim: equalityE) |
|
246 apply simp |
|
247 done |
|
248 |
|
249 ML_setup {* |
|
250 let |
|
251 val thy = the_context () |
|
252 val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter"; |
|
253 in |
|
254 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc)); |
|
255 by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1); |
|
256 by (clarify_tac (claset() delrules [disjCI]) 1); |
|
257 by (subgoal_tac "(@p. p:w) : w" 1); |
|
258 by (fast_tac (claset() addIs [someI]) 2); |
|
259 by (subgoal_tac "ss : list (size ss) A" 1); |
|
260 by (blast_tac (claset() addSIs [thm "listI"]) 2); |
|
261 by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1); |
|
262 by (blast_tac (claset() addDs [thm "boundedD"]) 2); |
|
263 by (rotate_tac 1 1); |
|
264 by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"] |
|
265 addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma", |
|
266 bounded_nat_set_is_finite]) 1); |
|
267 qed "iter_tc" |
|
268 end |
|
269 *} |
|
270 |
|
271 |
|
272 lemma iter_induct: |
|
273 "(!!A r f step succs ss w. |
|
274 (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r & |
|
275 (!p:w. p < length ss) & bounded succs (length ss) & |
|
276 set ss <= A & pres_type step (length ss) A |
|
277 --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) |
|
278 ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p}))) |
|
279 ==> P A r f step succs ss w) ==> P A r f step succs ss w" |
|
280 proof - |
|
281 case antecedent |
|
282 show ?thesis |
|
283 apply (rule_tac P = P in iter_tc [THEN iter_wf [THEN iter.induct]]) |
|
284 apply (rule antecedent) |
|
285 apply clarify |
|
286 apply simp |
|
287 apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss") |
|
288 apply (rotate_tac -1) |
|
289 apply (simp add: decomp_propa) |
|
290 apply (subgoal_tac "(@p. p:w) : w") |
|
291 apply (blast dest: boundedD) |
|
292 apply (fast intro: someI) |
|
293 done |
|
294 qed |
|
295 |
|
296 lemma iter_unfold: |
|
297 "[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A; |
|
298 bounded succs (size ss); !p:w. p<size ss |] ==> |
|
299 iter(((A,r,f),step,succs),ss,w) = |
|
300 (if w={} then ss |
|
301 else let p = SOME p. p : w |
|
302 in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss, |
|
303 {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))" |
|
304 apply (rule iter_tc [THEN iter_wf [THEN iter.simps [THEN trans]]]) |
|
305 apply simp |
|
306 apply (rule impI) |
|
307 apply (subst decomp_propa) |
|
308 apply (subgoal_tac "(@p. p:w) : w") |
|
309 apply (blast dest: boundedD) |
|
310 apply (fast intro: someI) |
|
311 apply simp |
|
312 done |
|
313 |
|
314 lemma stable_pres_lemma: |
|
315 "[| semilat (A,r,f); pres_type step n A; bounded succs n; |
|
316 ss : list n A; p : w; ! q:w. q < n; |
|
317 ! q. q < n --> q ~: w --> stable r step succs ss q; q < n; |
|
318 q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; |
|
319 q ~: w | q = p |] |
|
320 ==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q" |
|
321 apply (unfold stable_def) |
|
322 apply (subgoal_tac "step p (ss!p) : A") |
|
323 defer |
|
324 apply (blast intro: listE_nth_in pres_typeD) |
|
325 apply simp |
|
326 apply clarify |
|
327 apply (subst nth_merges) |
|
328 apply assumption |
|
329 apply assumption |
|
330 prefer 2 |
|
331 apply assumption |
|
332 apply (blast dest: boundedD) |
|
333 apply (blast dest: boundedD) |
|
334 apply (subst nth_merges) |
|
335 apply assumption |
|
336 apply assumption |
|
337 prefer 2 |
|
338 apply assumption |
|
339 apply (blast dest: boundedD) |
|
340 apply (blast dest: boundedD) |
|
341 apply simp |
|
342 apply (rule conjI) |
|
343 apply clarify |
|
344 apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in |
|
345 intro: order_trans dest: boundedD) |
|
346 apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in |
|
347 intro: order_trans dest: boundedD) |
|
348 done |
|
349 |
|
350 lemma merges_bounded_lemma [rule_format]: |
|
351 "[| semilat (A,r,f); mono r step n A; bounded succs n; |
|
352 step p (ss!p) : A; ss : list n A; ts : list n A; p < n; |
|
353 ss <=[r] ts; ! p. p < n --> stable r step succs ts p |] |
|
354 ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts" |
|
355 apply (unfold stable_def) |
|
356 apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI |
|
357 intro: merges_pres_le_ub order_trans |
|
358 dest: pres_typeD boundedD) |
|
359 done |
|
360 |
|
361 ML_setup {* |
|
362 Unify.trace_bound := 80; |
|
363 Unify.search_bound := 90; |
|
364 *} |
|
365 |
|
366 lemma iter_properties [rule_format]: |
|
367 "semilat(A,r,f) & acc r & pres_type step n A & mono r step n A & |
|
368 bounded succs n & (! p:w. p < n) & ss:list n A & |
|
369 (!p<n. p~:w --> stable r step succs ss p) |
|
370 --> iter(((A,r,f),step,succs),ss,w) : list n A & |
|
371 stables r step succs (iter(((A,r,f),step,succs),ss,w)) & |
|
372 ss <=[r] iter(((A,r,f),step,succs),ss,w) & |
|
373 (! ts:list n A. |
|
374 ss <=[r] ts & stables r step succs ts --> |
|
375 iter(((A,r,f),step,succs),ss,w) <=[r] ts)" |
|
376 apply (unfold stables_def) |
|
377 apply (rule_tac A = A and r = r and f = f and step = step and ss = ss and w = w in iter_induct) |
|
378 apply clarify |
|
379 apply (frule listE_length) |
|
380 apply hypsubst |
|
381 apply (subst iter_unfold) |
|
382 apply assumption |
|
383 apply assumption |
|
384 apply (simp (no_asm_simp)) |
|
385 apply assumption |
|
386 apply assumption |
|
387 apply assumption |
|
388 apply (simp (no_asm_simp) del: listE_length) |
|
389 apply (rule impI) |
|
390 apply (erule allE) |
|
391 apply (erule impE) |
|
392 apply (simp (no_asm_simp) del: listE_length) |
|
393 apply (subgoal_tac "(@p. p:w) : w") |
|
394 prefer 2 |
|
395 apply (fast intro: someI) |
|
396 apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A") |
|
397 prefer 2 |
|
398 apply (blast intro: pres_typeD listE_nth_in) |
|
399 apply (erule impE) |
|
400 apply (simp (no_asm_simp) del: listE_length le_iff_plus_unchanged [symmetric]) |
|
401 apply (rule conjI) |
|
402 apply (blast dest: boundedD) |
|
403 apply (rule conjI) |
|
404 apply (blast intro: merges_preserves_type dest: boundedD) |
|
405 apply clarify |
|
406 apply (blast intro!: stable_pres_lemma) |
|
407 apply (simp (no_asm_simp) del: listE_length) |
|
408 apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss") |
|
409 prefer 2 |
|
410 apply (blast dest: boundedD) |
|
411 apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A") |
|
412 prefer 2 |
|
413 apply (blast intro: pres_typeD) |
|
414 apply (rule conjI) |
|
415 apply (blast intro!: merges_incr intro: le_list_trans) |
|
416 apply clarify |
|
417 apply (drule bspec, assumption, erule mp) |
|
418 apply (simp del: listE_length) |
|
419 apply (blast intro: merges_bounded_lemma) |
|
420 done |
|
421 |
|
422 |
|
423 lemma is_dfa_kildall: |
|
424 "[| semilat(A,r,f); acc r; pres_type step n A; |
|
425 mono r step n A; bounded succs n|] |
|
426 ==> is_dfa r (kildall (A,r,f) step succs) step succs n A" |
|
427 apply (unfold is_dfa_def kildall_def) |
|
428 apply clarify |
|
429 apply simp |
|
430 apply (rule iter_properties) |
|
431 apply (simp add: unstables_def stable_def) |
|
432 apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in |
|
433 dest: boundedD pres_typeD) |
|
434 done |
|
435 |
|
436 lemma is_bcv_kildall: |
|
437 "[| semilat(A,r,f); acc r; top r T; |
|
438 pres_type step n A; bounded succs n; |
|
439 mono r step n A |] |
|
440 ==> is_bcv r T step succs n A (kildall (A,r,f) step succs)" |
|
441 apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI) |
|
442 apply assumption+ |
|
443 done |
|
444 |
|
445 end |