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