1 (* Title: HOL/MicroJava/BV/Kildall.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Gerwin Klein |
|
4 Copyright 2000 TUM |
|
5 |
|
6 Kildall's algorithm |
|
7 *) |
|
8 |
|
9 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} |
|
10 |
|
11 theory Kildall |
|
12 imports SemilatAlg While_Combinator |
|
13 begin |
|
14 |
|
15 |
|
16 consts |
|
17 iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow> |
|
18 's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set" |
|
19 propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" |
|
20 |
|
21 primrec |
|
22 "propa f [] ss w = (ss,w)" |
|
23 "propa f (q'#qs) ss w = (let (q,t) = q'; |
|
24 u = t +_f ss!q; |
|
25 w' = (if u = ss!q then w else insert q w) |
|
26 in propa f qs (ss[q := u]) w')" |
|
27 |
|
28 defs iter_def: |
|
29 "iter f step ss w == |
|
30 while (%(ss,w). w \<noteq> {}) |
|
31 (%(ss,w). let p = SOME p. p \<in> w |
|
32 in propa f (step p (ss!p)) ss (w-{p})) |
|
33 (ss,w)" |
|
34 |
|
35 constdefs |
|
36 unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set" |
|
37 "unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}" |
|
38 |
|
39 kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list" |
|
40 "kildall r f step ss == fst(iter f step ss (unstables r step ss))" |
|
41 |
|
42 consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list" |
|
43 primrec |
|
44 "merges f [] ss = ss" |
|
45 "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))" |
|
46 |
|
47 |
|
48 lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric] |
|
49 |
|
50 |
|
51 lemma (in Semilat) nth_merges: |
|
52 "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow> |
|
53 (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p" |
|
54 (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps") |
|
55 proof (induct ps) |
|
56 show "\<And>ss. ?P ss []" by simp |
|
57 |
|
58 fix ss p' ps' |
|
59 assume ss: "ss \<in> list n A" |
|
60 assume l: "p < length ss" |
|
61 assume "?steptype (p'#ps')" |
|
62 then obtain a b where |
|
63 p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'" |
|
64 by (cases p') auto |
|
65 assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'" |
|
66 from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" . |
|
67 |
|
68 from ss ab |
|
69 have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD) |
|
70 moreover |
|
71 from calculation l |
|
72 have "p < length (ss[a := b +_f ss!a])" by simp |
|
73 ultimately |
|
74 have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH) |
|
75 with p' l |
|
76 show "?P ss (p'#ps')" by simp |
|
77 qed |
|
78 |
|
79 |
|
80 (** merges **) |
|
81 |
|
82 lemma length_merges [rule_format, simp]: |
|
83 "\<forall>ss. size(merges f ps ss) = size ss" |
|
84 by (induct_tac ps, auto) |
|
85 |
|
86 |
|
87 lemma (in Semilat) merges_preserves_type_lemma: |
|
88 shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A) |
|
89 \<longrightarrow> merges f ps xs \<in> list n A" |
|
90 apply (insert closedI) |
|
91 apply (unfold closed_def) |
|
92 apply (induct_tac ps) |
|
93 apply simp |
|
94 apply clarsimp |
|
95 done |
|
96 |
|
97 lemma (in Semilat) merges_preserves_type [simp]: |
|
98 "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk> |
|
99 \<Longrightarrow> merges f ps xs \<in> list n A" |
|
100 by (simp add: merges_preserves_type_lemma) |
|
101 |
|
102 lemma (in Semilat) merges_incr_lemma: |
|
103 "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs" |
|
104 apply (induct_tac ps) |
|
105 apply simp |
|
106 apply simp |
|
107 apply clarify |
|
108 apply (rule order_trans) |
|
109 apply simp |
|
110 apply (erule list_update_incr) |
|
111 apply simp |
|
112 apply simp |
|
113 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
114 done |
|
115 |
|
116 lemma (in Semilat) merges_incr: |
|
117 "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> |
|
118 \<Longrightarrow> xs <=[r] merges f ps xs" |
|
119 by (simp add: merges_incr_lemma) |
|
120 |
|
121 |
|
122 lemma (in Semilat) merges_same_conv [rule_format]: |
|
123 "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> |
|
124 (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))" |
|
125 apply (induct_tac ps) |
|
126 apply simp |
|
127 apply clarsimp |
|
128 apply (rename_tac p x ps xs) |
|
129 apply (rule iffI) |
|
130 apply (rule context_conjI) |
|
131 apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs") |
|
132 apply (drule_tac p = p in le_listD) |
|
133 apply simp |
|
134 apply simp |
|
135 apply (erule subst, rule merges_incr) |
|
136 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
137 apply clarify |
|
138 apply (rule conjI) |
|
139 apply simp |
|
140 apply (blast dest: boundedD) |
|
141 apply blast |
|
142 apply clarify |
|
143 apply (erule allE) |
|
144 apply (erule impE) |
|
145 apply assumption |
|
146 apply (drule bspec) |
|
147 apply assumption |
|
148 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
149 apply blast |
|
150 apply clarify |
|
151 apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
152 done |
|
153 |
|
154 |
|
155 lemma (in Semilat) list_update_le_listI [rule_format]: |
|
156 "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow> |
|
157 x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys" |
|
158 apply(insert semilat) |
|
159 apply (unfold Listn.le_def lesub_def semilat_def) |
|
160 apply (simp add: list_all2_conv_all_nth nth_list_update) |
|
161 done |
|
162 |
|
163 lemma (in Semilat) merges_pres_le_ub: |
|
164 assumes "set ts <= A" and "set ss <= A" |
|
165 and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts" |
|
166 shows "merges f ps ss <=[r] ts" |
|
167 proof - |
|
168 { fix t ts ps |
|
169 have |
|
170 "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow> |
|
171 set qs <= set ps \<longrightarrow> |
|
172 (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)" |
|
173 apply (induct_tac qs) |
|
174 apply simp |
|
175 apply (simp (no_asm_simp)) |
|
176 apply clarify |
|
177 apply (rotate_tac -2) |
|
178 apply simp |
|
179 apply (erule allE, erule impE, erule_tac [2] mp) |
|
180 apply (drule bspec, assumption) |
|
181 apply (simp add: closedD) |
|
182 apply (drule bspec, assumption) |
|
183 apply (simp add: list_update_le_listI) |
|
184 done |
|
185 } note this [dest] |
|
186 |
|
187 from prems show ?thesis by blast |
|
188 qed |
|
189 |
|
190 |
|
191 (** propa **) |
|
192 |
|
193 |
|
194 lemma decomp_propa: |
|
195 "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> |
|
196 propa f qs ss w = |
|
197 (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)" |
|
198 apply (induct qs) |
|
199 apply simp |
|
200 apply (simp (no_asm)) |
|
201 apply clarify |
|
202 apply simp |
|
203 apply (rule conjI) |
|
204 apply blast |
|
205 apply (simp add: nth_list_update) |
|
206 apply blast |
|
207 done |
|
208 |
|
209 (** iter **) |
|
210 |
|
211 lemma (in Semilat) stable_pres_lemma: |
|
212 shows "\<lbrakk>pres_type step n A; bounded step n; |
|
213 ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; |
|
214 \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; |
|
215 \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; |
|
216 q \<notin> w \<or> q = p \<rbrakk> |
|
217 \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q" |
|
218 apply (unfold stable_def) |
|
219 apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A") |
|
220 prefer 2 |
|
221 apply clarify |
|
222 apply (erule pres_typeD) |
|
223 prefer 3 apply assumption |
|
224 apply (rule listE_nth_in) |
|
225 apply assumption |
|
226 apply simp |
|
227 apply simp |
|
228 apply simp |
|
229 apply clarify |
|
230 apply (subst nth_merges) |
|
231 apply simp |
|
232 apply (blast dest: boundedD) |
|
233 apply assumption |
|
234 apply clarify |
|
235 apply (rule conjI) |
|
236 apply (blast dest: boundedD) |
|
237 apply (erule pres_typeD) |
|
238 prefer 3 apply assumption |
|
239 apply simp |
|
240 apply simp |
|
241 apply(subgoal_tac "q < length ss") |
|
242 prefer 2 apply simp |
|
243 apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *) |
|
244 apply assumption |
|
245 apply clarify |
|
246 apply (rule conjI) |
|
247 apply (blast dest: boundedD) |
|
248 apply (erule pres_typeD) |
|
249 prefer 3 apply assumption |
|
250 apply simp |
|
251 apply simp |
|
252 apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst) |
|
253 apply assumption |
|
254 |
|
255 apply (simp add: plusplus_empty) |
|
256 apply (cases "q \<in> w") |
|
257 apply simp |
|
258 apply (rule ub1') |
|
259 apply (rule semilat) |
|
260 apply clarify |
|
261 apply (rule pres_typeD) |
|
262 apply assumption |
|
263 prefer 3 apply assumption |
|
264 apply (blast intro: listE_nth_in dest: boundedD) |
|
265 apply (blast intro: pres_typeD dest: boundedD) |
|
266 apply (blast intro: listE_nth_in dest: boundedD) |
|
267 apply assumption |
|
268 |
|
269 apply simp |
|
270 apply (erule allE, erule impE, assumption, erule impE, assumption) |
|
271 apply (rule order_trans) |
|
272 apply simp |
|
273 defer |
|
274 apply (rule pp_ub2)(* |
|
275 apply assumption*) |
|
276 apply simp |
|
277 apply clarify |
|
278 apply simp |
|
279 apply (rule pres_typeD) |
|
280 apply assumption |
|
281 prefer 3 apply assumption |
|
282 apply (blast intro: listE_nth_in dest: boundedD) |
|
283 apply (blast intro: pres_typeD dest: boundedD) |
|
284 apply (blast intro: listE_nth_in dest: boundedD) |
|
285 apply blast |
|
286 done |
|
287 |
|
288 |
|
289 lemma (in Semilat) merges_bounded_lemma: |
|
290 "\<lbrakk> mono r step n A; bounded step n; |
|
291 \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; |
|
292 ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> |
|
293 \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" |
|
294 apply (unfold stable_def) |
|
295 apply (rule merges_pres_le_ub) |
|
296 apply simp |
|
297 apply simp |
|
298 prefer 2 apply assumption |
|
299 |
|
300 apply clarsimp |
|
301 apply (drule boundedD, assumption+) |
|
302 apply (erule allE, erule impE, assumption) |
|
303 apply (drule bspec, assumption) |
|
304 apply simp |
|
305 |
|
306 apply (drule monoD [of _ _ _ _ p "ss!p" "ts!p"]) |
|
307 apply assumption |
|
308 apply simp |
|
309 apply (simp add: le_listD) |
|
310 |
|
311 apply (drule lesub_step_typeD, assumption) |
|
312 apply clarify |
|
313 apply (drule bspec, assumption) |
|
314 apply simp |
|
315 apply (blast intro: order_trans) |
|
316 done |
|
317 |
|
318 lemma termination_lemma: |
|
319 assumes semilat: "semilat (A, r, f)" |
|
320 shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> |
|
321 ss <[r] merges f qs ss \<or> |
|
322 merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P") |
|
323 proof - |
|
324 interpret Semilat A r f using assms by (rule Semilat.intro) |
|
325 show "PROP ?P" apply(insert semilat) |
|
326 apply (unfold lesssub_def) |
|
327 apply (simp (no_asm_simp) add: merges_incr) |
|
328 apply (rule impI) |
|
329 apply (rule merges_same_conv [THEN iffD1, elim_format]) |
|
330 apply assumption+ |
|
331 defer |
|
332 apply (rule sym, assumption) |
|
333 defer apply simp |
|
334 apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)") |
|
335 apply (blast intro!: psubsetI elim: equalityE) |
|
336 apply clarsimp |
|
337 apply (drule bspec, assumption) |
|
338 apply (drule bspec, assumption) |
|
339 apply clarsimp |
|
340 done |
|
341 qed |
|
342 |
|
343 lemma iter_properties[rule_format]: |
|
344 assumes semilat: "semilat (A, r, f)" |
|
345 shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A; |
|
346 bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A; |
|
347 \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow> |
|
348 iter f step ss0 w0 = (ss',w') |
|
349 \<longrightarrow> |
|
350 ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and> |
|
351 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)" |
|
352 (is "PROP ?P") |
|
353 proof - |
|
354 interpret Semilat A r f using assms by (rule Semilat.intro) |
|
355 show "PROP ?P" apply(insert semilat) |
|
356 apply (unfold iter_def stables_def) |
|
357 apply (rule_tac P = "%(ss,w). |
|
358 ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and> |
|
359 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and> |
|
360 (\<forall>p\<in>w. p < n)" and |
|
361 r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset" |
|
362 in while_rule) |
|
363 |
|
364 -- "Invariant holds initially:" |
|
365 apply (simp add:stables_def) |
|
366 |
|
367 -- "Invariant is preserved:" |
|
368 apply(simp add: stables_def split_paired_all) |
|
369 apply(rename_tac ss w) |
|
370 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
|
371 prefer 2; apply (fast intro: someI) |
|
372 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |
|
373 prefer 2 |
|
374 apply clarify |
|
375 apply (rule conjI) |
|
376 apply(clarsimp, blast dest!: boundedD) |
|
377 apply (erule pres_typeD) |
|
378 prefer 3 |
|
379 apply assumption |
|
380 apply (erule listE_nth_in) |
|
381 apply simp |
|
382 apply simp |
|
383 apply (subst decomp_propa) |
|
384 apply fast |
|
385 apply simp |
|
386 apply (rule conjI) |
|
387 apply (rule merges_preserves_type) |
|
388 apply blast |
|
389 apply clarify |
|
390 apply (rule conjI) |
|
391 apply(clarsimp, fast dest!: boundedD) |
|
392 apply (erule pres_typeD) |
|
393 prefer 3 |
|
394 apply assumption |
|
395 apply (erule listE_nth_in) |
|
396 apply blast |
|
397 apply blast |
|
398 apply (rule conjI) |
|
399 apply clarify |
|
400 apply (blast intro!: stable_pres_lemma) |
|
401 apply (rule conjI) |
|
402 apply (blast intro!: merges_incr intro: le_list_trans) |
|
403 apply (rule conjI) |
|
404 apply clarsimp |
|
405 apply (blast intro!: merges_bounded_lemma) |
|
406 apply (blast dest!: boundedD) |
|
407 |
|
408 |
|
409 -- "Postcondition holds upon termination:" |
|
410 apply(clarsimp simp add: stables_def split_paired_all) |
|
411 |
|
412 -- "Well-foundedness of the termination relation:" |
|
413 apply (rule wf_lex_prod) |
|
414 apply (insert orderI [THEN acc_le_listI]) |
|
415 apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric]) |
|
416 apply (rule wf_finite_psubset) |
|
417 |
|
418 -- "Loop decreases along termination relation:" |
|
419 apply(simp add: stables_def split_paired_all) |
|
420 apply(rename_tac ss w) |
|
421 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
|
422 prefer 2; apply (fast intro: someI) |
|
423 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |
|
424 prefer 2 |
|
425 apply clarify |
|
426 apply (rule conjI) |
|
427 apply(clarsimp, blast dest!: boundedD) |
|
428 apply (erule pres_typeD) |
|
429 prefer 3 |
|
430 apply assumption |
|
431 apply (erule listE_nth_in) |
|
432 apply blast |
|
433 apply blast |
|
434 apply (subst decomp_propa) |
|
435 apply blast |
|
436 apply clarify |
|
437 apply (simp del: listE_length |
|
438 add: lex_prod_def finite_psubset_def |
|
439 bounded_nat_set_is_finite) |
|
440 apply (rule termination_lemma) |
|
441 apply assumption+ |
|
442 defer |
|
443 apply assumption |
|
444 apply clarsimp |
|
445 done |
|
446 |
|
447 qed |
|
448 |
|
449 lemma kildall_properties: |
|
450 assumes semilat: "semilat (A, r, f)" |
|
451 shows "\<lbrakk> acc r; pres_type step n A; mono r step n A; |
|
452 bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow> |
|
453 kildall r f step ss0 \<in> list n A \<and> |
|
454 stables r step (kildall r f step ss0) \<and> |
|
455 ss0 <=[r] kildall r f step ss0 \<and> |
|
456 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> |
|
457 kildall r f step ss0 <=[r] ts)" |
|
458 (is "PROP ?P") |
|
459 proof - |
|
460 interpret Semilat A r f using assms by (rule Semilat.intro) |
|
461 show "PROP ?P" |
|
462 apply (unfold kildall_def) |
|
463 apply(case_tac "iter f step ss0 (unstables r step ss0)") |
|
464 apply(simp) |
|
465 apply (rule iter_properties) |
|
466 apply (simp_all add: unstables_def stable_def) |
|
467 apply (rule semilat) |
|
468 done |
|
469 qed |
|
470 |
|
471 lemma is_bcv_kildall: |
|
472 assumes semilat: "semilat (A, r, f)" |
|
473 shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk> |
|
474 \<Longrightarrow> is_bcv r T step n A (kildall r f step)" |
|
475 (is "PROP ?P") |
|
476 proof - |
|
477 interpret Semilat A r f using assms by (rule Semilat.intro) |
|
478 show "PROP ?P" |
|
479 apply(unfold is_bcv_def wt_step_def) |
|
480 apply(insert semilat kildall_properties[of A]) |
|
481 apply(simp add:stables_def) |
|
482 apply clarify |
|
483 apply(subgoal_tac "kildall r f step ss \<in> list n A") |
|
484 prefer 2 apply (simp(no_asm_simp)) |
|
485 apply (rule iffI) |
|
486 apply (rule_tac x = "kildall r f step ss" in bexI) |
|
487 apply (rule conjI) |
|
488 apply (blast) |
|
489 apply (simp (no_asm_simp)) |
|
490 apply(assumption) |
|
491 apply clarify |
|
492 apply(subgoal_tac "kildall r f step ss!p <=_r ts!p") |
|
493 apply simp |
|
494 apply (blast intro!: le_listD less_lengthI) |
|
495 done |
|
496 qed |
|
497 |
|
498 end |
|