author | haftmann |
Mon, 11 Aug 2008 14:50:00 +0200 | |
changeset 27824 | 97d2a3797ce0 |
parent 27681 | 8cedebf55539 |
child 29235 | 2d62b637fa80 |
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 |
|
27681 | 11 |
theory Kildall |
12 |
imports SemilatAlg While_Combinator |
|
13 |
begin |
|
12516 | 14 |
|
10496 | 15 |
|
16 |
consts |
|
12516 | 17 |
iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow> |
11298 | 18 |
's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set" |
13006 | 19 |
propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" |
10496 | 20 |
|
21 |
primrec |
|
12516 | 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')" |
|
10496 | 27 |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
28 |
defs iter_def: |
12516 | 29 |
"iter f step ss w == |
11298 | 30 |
while (%(ss,w). w \<noteq> {}) |
12516 | 31 |
(%(ss,w). let p = SOME p. p \<in> w |
32 |
in propa f (step p (ss!p)) ss (w-{p})) |
|
11298 | 33 |
(ss,w)" |
10496 | 34 |
|
35 |
constdefs |
|
13006 | 36 |
unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set" |
12516 | 37 |
"unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}" |
10496 | 38 |
|
13006 | 39 |
kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list" |
12516 | 40 |
"kildall r f step ss == fst(iter f step ss (unstables r step ss))" |
10496 | 41 |
|
13006 | 42 |
consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list" |
10496 | 43 |
primrec |
12516 | 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]))" |
|
10496 | 46 |
|
47 |
||
27681 | 48 |
lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric] |
10496 | 49 |
|
50 |
||
27681 | 51 |
lemma (in Semilat) nth_merges: |
13074 | 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> |
23281 | 53 |
(merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p" |
13074 | 54 |
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps") |
12516 | 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 |
|
23467 | 63 |
p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'" |
64 |
by (cases p') auto |
|
13074 | 65 |
assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'" |
23467 | 66 |
from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" . |
12516 | 67 |
|
13074 | 68 |
from ss ab |
12516 | 69 |
have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD) |
70 |
moreover |
|
23467 | 71 |
from calculation l |
12516 | 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) |
|
13074 | 75 |
with p' l |
12516 | 76 |
show "?P ss (p'#ps')" by simp |
77 |
qed |
|
78 |
||
79 |
||
10496 | 80 |
(** merges **) |
81 |
||
82 |
lemma length_merges [rule_format, simp]: |
|
12516 | 83 |
"\<forall>ss. size(merges f ps ss) = size ss" |
10496 | 84 |
by (induct_tac ps, auto) |
85 |
||
12516 | 86 |
|
27681 | 87 |
lemma (in Semilat) merges_preserves_type_lemma: |
13074 | 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 |
|
10496 | 96 |
|
27681 | 97 |
lemma (in Semilat) merges_preserves_type [simp]: |
13074 | 98 |
"\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk> |
13006 | 99 |
\<Longrightarrow> merges f ps xs \<in> list n A" |
13074 | 100 |
by (simp add: merges_preserves_type_lemma) |
101 |
||
27681 | 102 |
lemma (in Semilat) merges_incr_lemma: |
13074 | 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) |
|
10496 | 109 |
apply simp |
13074 | 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 |
|
10496 | 115 |
|
27681 | 116 |
lemma (in Semilat) merges_incr: |
13074 | 117 |
"\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> |
13006 | 118 |
\<Longrightarrow> xs <=[r] merges f ps xs" |
12516 | 119 |
by (simp add: merges_incr_lemma) |
120 |
||
121 |
||
27681 | 122 |
lemma (in Semilat) merges_same_conv [rule_format]: |
13074 | 123 |
"(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> |
12516 | 124 |
(merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))" |
10496 | 125 |
apply (induct_tac ps) |
126 |
apply simp |
|
127 |
apply clarsimp |
|
12516 | 128 |
apply (rename_tac p x ps xs) |
10496 | 129 |
apply (rule iffI) |
130 |
apply (rule context_conjI) |
|
131 |
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
|
132 |
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
|
133 |
apply simp |
3825229092f0
fixed proof script of lemma merges_same_conv (Why did it stop working?);
wenzelm
parents:
16417
diff
changeset
|
134 |
apply simp |
10496 | 135 |
apply (erule subst, rule merges_incr) |
136 |
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
12516 | 137 |
apply clarify |
138 |
apply (rule conjI) |
|
139 |
apply simp |
|
140 |
apply (blast dest: boundedD) |
|
141 |
apply blast |
|
10496 | 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]) |
|
12516 | 149 |
apply blast |
10496 | 150 |
apply clarify |
151 |
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
152 |
done |
|
153 |
||
154 |
||
27681 | 155 |
lemma (in Semilat) list_update_le_listI [rule_format]: |
13006 | 156 |
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow> |
13074 | 157 |
x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys" |
158 |
apply(insert semilat) |
|
10496 | 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 |
||
27681 | 163 |
lemma (in Semilat) merges_pres_le_ub: |
18372 | 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" |
|
10496 | 167 |
proof - |
13074 | 168 |
{ fix t ts ps |
10496 | 169 |
have |
13074 | 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> |
13006 | 171 |
set qs <= set ps \<longrightarrow> |
172 |
(\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)" |
|
10496 | 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) |
|
12516 | 180 |
apply (drule bspec, assumption) |
181 |
apply (simp add: closedD) |
|
182 |
apply (drule bspec, assumption) |
|
10496 | 183 |
apply (simp add: list_update_le_listI) |
12516 | 184 |
done |
10496 | 185 |
} note this [dest] |
186 |
||
18372 | 187 |
from prems show ?thesis by blast |
10496 | 188 |
qed |
189 |
||
190 |
||
12516 | 191 |
(** propa **) |
10496 | 192 |
|
193 |
||
12516 | 194 |
lemma decomp_propa: |
13006 | 195 |
"\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> |
12516 | 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 |
|
10496 | 200 |
apply (simp (no_asm)) |
12516 | 201 |
apply clarify |
202 |
apply simp |
|
203 |
apply (rule conjI) |
|
10496 | 204 |
apply blast |
205 |
apply (simp add: nth_list_update) |
|
206 |
apply blast |
|
207 |
done |
|
208 |
||
209 |
(** iter **) |
|
210 |
||
27681 | 211 |
lemma (in Semilat) stable_pres_lemma: |
13074 | 212 |
shows "\<lbrakk>pres_type step n A; bounded step n; |
12516 | 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; |
|
13006 | 216 |
q \<notin> w \<or> q = p \<rbrakk> |
217 |
\<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q" |
|
10496 | 218 |
apply (unfold stable_def) |
12516 | 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 |
|
10496 | 228 |
apply simp |
229 |
apply clarify |
|
13074 | 230 |
apply (subst nth_merges) |
12516 | 231 |
apply simp |
232 |
apply (blast dest: boundedD) |
|
10496 | 233 |
apply assumption |
12516 | 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 |
|
13074 | 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 |
|
12516 | 245 |
apply clarify |
10496 | 246 |
apply (rule conjI) |
12516 | 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') |
|
23467 | 259 |
apply (rule semilat) |
12516 | 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 |
|
10496 | 268 |
|
12516 | 269 |
apply simp |
270 |
apply (erule allE, erule impE, assumption, erule impE, assumption) |
|
271 |
apply (rule order_trans) |
|
272 |
apply simp |
|
273 |
defer |
|
13074 | 274 |
apply (rule pp_ub2)(* |
275 |
apply assumption*) |
|
12516 | 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 |
|
13074 | 287 |
|
288 |
||
27681 | 289 |
lemma (in Semilat) merges_bounded_lemma: |
13074 | 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> |
|
13066 | 293 |
\<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" |
10496 | 294 |
apply (unfold stable_def) |
12516 | 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 |
||
13066 | 311 |
apply (drule lesub_step_typeD, assumption) |
12516 | 312 |
apply clarify |
313 |
apply (drule bspec, assumption) |
|
314 |
apply simp |
|
315 |
apply (blast intro: order_trans) |
|
10496 | 316 |
done |
317 |
||
27611 | 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 - |
|
27681 | 324 |
interpret Semilat [A r f] using assms by (rule Semilat.intro) |
27611 | 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+ |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
331 |
defer |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
332 |
apply (rule sym, assumption) |
27611 | 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 |
|
10496 | 342 |
|
27611 | 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; |
|
12516 | 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') |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
349 |
\<longrightarrow> |
12516 | 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)" |
|
27611 | 352 |
(is "PROP ?P") |
353 |
proof - |
|
27681 | 354 |
interpret Semilat [A r f] using assms by (rule Semilat.intro) |
27611 | 355 |
show "PROP ?P" apply(insert semilat) |
11298 | 356 |
apply (unfold iter_def stables_def) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
357 |
apply (rule_tac P = "%(ss,w). |
12516 | 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> |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
360 |
(\<forall>p\<in>w. p < n)" and |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
361 |
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
|
362 |
in while_rule) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
363 |
|
12516 | 364 |
-- "Invariant holds initially:" |
13074 | 365 |
apply (simp add:stables_def) |
12516 | 366 |
|
367 |
-- "Invariant is preserved:" |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
368 |
apply(simp add: stables_def split_paired_all) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
369 |
apply(rename_tac ss w) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
370 |
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
|
371 |
prefer 2; apply (fast intro: someI) |
12516 | 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) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
381 |
apply simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
382 |
apply simp |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
383 |
apply (subst decomp_propa) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
384 |
apply fast |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
385 |
apply simp |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
386 |
apply (rule conjI) |
13074 | 387 |
apply (rule merges_preserves_type) |
388 |
apply blast |
|
12516 | 389 |
apply clarify |
390 |
apply (rule conjI) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
391 |
apply(clarsimp, fast dest!: boundedD) |
12516 | 392 |
apply (erule pres_typeD) |
393 |
prefer 3 |
|
394 |
apply assumption |
|
395 |
apply (erule listE_nth_in) |
|
396 |
apply blast |
|
397 |
apply blast |
|
13074 | 398 |
apply (rule conjI) |
399 |
apply clarify |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
400 |
apply (blast intro!: stable_pres_lemma) |
13074 | 401 |
apply (rule conjI) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
402 |
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
|
403 |
apply (rule conjI) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
404 |
apply clarsimp |
12516 | 405 |
apply (blast intro!: merges_bounded_lemma) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
406 |
apply (blast dest!: boundedD) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
407 |
|
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
408 |
|
12516 | 409 |
-- "Postcondition holds upon termination:" |
13074 | 410 |
apply(clarsimp simp add: stables_def split_paired_all) |
12516 | 411 |
|
412 |
-- "Well-foundedness of the termination relation:" |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
413 |
apply (rule wf_lex_prod) |
13074 | 414 |
apply (insert orderI [THEN acc_le_listI]) |
22271 | 415 |
apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric]) |
12516 | 416 |
apply (rule wf_finite_psubset) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
417 |
|
12516 | 418 |
-- "Loop decreases along termination relation:" |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
419 |
apply(simp add: stables_def split_paired_all) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
420 |
apply(rename_tac ss w) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
421 |
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
|
422 |
prefer 2; apply (fast intro: someI) |
12516 | 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 |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
434 |
apply (subst decomp_propa) |
12516 | 435 |
apply blast |
13074 | 436 |
apply clarify |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
437 |
apply (simp del: listE_length |
12516 | 438 |
add: lex_prod_def finite_psubset_def |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
439 |
bounded_nat_set_is_finite) |
12516 | 440 |
apply (rule termination_lemma) |
441 |
apply assumption+ |
|
442 |
defer |
|
443 |
apply assumption |
|
444 |
apply clarsimp |
|
13074 | 445 |
done |
12516 | 446 |
|
27611 | 447 |
qed |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
448 |
|
27611 | 449 |
lemma kildall_properties: |
450 |
assumes semilat: "semilat (A, r, f)" |
|
13074 | 451 |
shows "\<lbrakk> acc r; pres_type step n A; mono r step n A; |
12516 | 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)" |
|
27611 | 458 |
(is "PROP ?P") |
459 |
proof - |
|
27681 | 460 |
interpret Semilat [A r f] using assms by (rule Semilat.intro) |
27611 | 461 |
show "PROP ?P" |
11229 | 462 |
apply (unfold kildall_def) |
12516 | 463 |
apply(case_tac "iter f step ss0 (unstables r step ss0)") |
11298 | 464 |
apply(simp) |
11229 | 465 |
apply (rule iter_properties) |
23467 | 466 |
apply (simp_all add: unstables_def stable_def) |
467 |
apply (rule semilat) |
|
468 |
done |
|
27611 | 469 |
qed |
10496 | 470 |
|
27611 | 471 |
lemma is_bcv_kildall: |
472 |
assumes semilat: "semilat (A, r, f)" |
|
13074 | 473 |
shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk> |
13006 | 474 |
\<Longrightarrow> is_bcv r T step n A (kildall r f step)" |
27611 | 475 |
(is "PROP ?P") |
476 |
proof - |
|
27681 | 477 |
interpret Semilat [A r f] using assms by (rule Semilat.intro) |
27611 | 478 |
show "PROP ?P" |
11299 | 479 |
apply(unfold is_bcv_def wt_step_def) |
13074 | 480 |
apply(insert semilat kildall_properties[of A]) |
11229 | 481 |
apply(simp add:stables_def) |
482 |
apply clarify |
|
12516 | 483 |
apply(subgoal_tac "kildall r f step ss \<in> list n A") |
11229 | 484 |
prefer 2 apply (simp(no_asm_simp)) |
485 |
apply (rule iffI) |
|
12516 | 486 |
apply (rule_tac x = "kildall r f step ss" in bexI) |
11229 | 487 |
apply (rule conjI) |
13074 | 488 |
apply (blast) |
11229 | 489 |
apply (simp (no_asm_simp)) |
13074 | 490 |
apply(assumption) |
11229 | 491 |
apply clarify |
12516 | 492 |
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p") |
11229 | 493 |
apply simp |
494 |
apply (blast intro!: le_listD less_lengthI) |
|
495 |
done |
|
27611 | 496 |
qed |
10496 | 497 |
|
14191 | 498 |
end |