author | paulson |
Tue, 27 Jan 2004 15:39:51 +0100 | |
changeset 14365 | 3d4df8c166ae |
parent 14191 | 2014eac694d2 |
child 16417 | 9bc16273c2d4 |
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 |
|
13062 | 11 |
theory Kildall = SemilatAlg + While_Combinator: |
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> |
|
12516 | 51 |
(merges f ps ss)!p = map snd [(p',t') \<in> 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 |
|
61 |
p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?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'" |
12516 | 64 |
hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" . |
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 |
|
69 |
from calculation |
|
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") |
|
130 |
apply (force dest!: le_listD simp add: nth_list_update) |
|
131 |
apply (erule subst, rule merges_incr) |
|
132 |
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) |
|
12516 | 133 |
apply clarify |
134 |
apply (rule conjI) |
|
135 |
apply simp |
|
136 |
apply (blast dest: boundedD) |
|
137 |
apply blast |
|
10496 | 138 |
apply clarify |
139 |
apply (erule allE) |
|
140 |
apply (erule impE) |
|
141 |
apply assumption |
|
142 |
apply (drule bspec) |
|
143 |
apply assumption |
|
144 |
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
12516 | 145 |
apply blast |
10496 | 146 |
apply clarify |
147 |
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) |
|
148 |
done |
|
149 |
||
150 |
||
13074 | 151 |
lemma (in semilat) list_update_le_listI [rule_format]: |
13006 | 152 |
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow> |
13074 | 153 |
x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys" |
154 |
apply(insert semilat) |
|
10496 | 155 |
apply (unfold Listn.le_def lesub_def semilat_def) |
156 |
apply (simp add: list_all2_conv_all_nth nth_list_update) |
|
157 |
done |
|
158 |
||
13074 | 159 |
lemma (in semilat) merges_pres_le_ub: |
160 |
shows "\<lbrakk> set ts <= A; set ss <= A; |
|
161 |
\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk> |
|
13006 | 162 |
\<Longrightarrow> merges f ps ss <=[r] ts" |
10496 | 163 |
proof - |
13074 | 164 |
{ fix t ts ps |
10496 | 165 |
have |
13074 | 166 |
"\<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 | 167 |
set qs <= set ps \<longrightarrow> |
168 |
(\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)" |
|
10496 | 169 |
apply (induct_tac qs) |
170 |
apply simp |
|
171 |
apply (simp (no_asm_simp)) |
|
172 |
apply clarify |
|
173 |
apply (rotate_tac -2) |
|
174 |
apply simp |
|
175 |
apply (erule allE, erule impE, erule_tac [2] mp) |
|
12516 | 176 |
apply (drule bspec, assumption) |
177 |
apply (simp add: closedD) |
|
178 |
apply (drule bspec, assumption) |
|
10496 | 179 |
apply (simp add: list_update_le_listI) |
12516 | 180 |
done |
10496 | 181 |
} note this [dest] |
182 |
||
11549 | 183 |
case rule_context |
10496 | 184 |
thus ?thesis by blast |
185 |
qed |
|
186 |
||
187 |
||
12516 | 188 |
(** propa **) |
10496 | 189 |
|
190 |
||
12516 | 191 |
lemma decomp_propa: |
13006 | 192 |
"\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> |
12516 | 193 |
propa f qs ss w = |
194 |
(merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)" |
|
195 |
apply (induct qs) |
|
196 |
apply simp |
|
10496 | 197 |
apply (simp (no_asm)) |
12516 | 198 |
apply clarify |
199 |
apply simp |
|
200 |
apply (rule conjI) |
|
10496 | 201 |
apply blast |
202 |
apply (simp add: nth_list_update) |
|
203 |
apply blast |
|
204 |
done |
|
205 |
||
206 |
(** iter **) |
|
207 |
||
13074 | 208 |
lemma (in semilat) stable_pres_lemma: |
209 |
shows "\<lbrakk>pres_type step n A; bounded step n; |
|
12516 | 210 |
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; |
211 |
\<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; |
|
212 |
\<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; |
|
13006 | 213 |
q \<notin> w \<or> q = p \<rbrakk> |
214 |
\<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q" |
|
10496 | 215 |
apply (unfold stable_def) |
12516 | 216 |
apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A") |
217 |
prefer 2 |
|
218 |
apply clarify |
|
219 |
apply (erule pres_typeD) |
|
220 |
prefer 3 apply assumption |
|
221 |
apply (rule listE_nth_in) |
|
222 |
apply assumption |
|
223 |
apply simp |
|
224 |
apply simp |
|
10496 | 225 |
apply simp |
226 |
apply clarify |
|
13074 | 227 |
apply (subst nth_merges) |
12516 | 228 |
apply simp |
229 |
apply (blast dest: boundedD) |
|
10496 | 230 |
apply assumption |
12516 | 231 |
apply clarify |
232 |
apply (rule conjI) |
|
233 |
apply (blast dest: boundedD) |
|
234 |
apply (erule pres_typeD) |
|
235 |
prefer 3 apply assumption |
|
236 |
apply simp |
|
13074 | 237 |
apply simp |
238 |
apply(subgoal_tac "q < length ss") |
|
239 |
prefer 2 apply simp |
|
240 |
apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *) |
|
241 |
apply assumption |
|
12516 | 242 |
apply clarify |
10496 | 243 |
apply (rule conjI) |
12516 | 244 |
apply (blast dest: boundedD) |
245 |
apply (erule pres_typeD) |
|
246 |
prefer 3 apply assumption |
|
247 |
apply simp |
|
248 |
apply simp |
|
249 |
apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst) |
|
250 |
apply assumption |
|
251 |
||
252 |
apply (simp add: plusplus_empty) |
|
253 |
apply (cases "q \<in> w") |
|
254 |
apply simp |
|
255 |
apply (rule ub1') |
|
256 |
apply assumption |
|
257 |
apply clarify |
|
258 |
apply (rule pres_typeD) |
|
259 |
apply assumption |
|
260 |
prefer 3 apply assumption |
|
261 |
apply (blast intro: listE_nth_in dest: boundedD) |
|
262 |
apply (blast intro: pres_typeD dest: boundedD) |
|
263 |
apply (blast intro: listE_nth_in dest: boundedD) |
|
264 |
apply assumption |
|
10496 | 265 |
|
12516 | 266 |
apply simp |
267 |
apply (erule allE, erule impE, assumption, erule impE, assumption) |
|
268 |
apply (rule order_trans) |
|
269 |
apply simp |
|
270 |
defer |
|
13074 | 271 |
apply (rule pp_ub2)(* |
272 |
apply assumption*) |
|
12516 | 273 |
apply simp |
274 |
apply clarify |
|
275 |
apply simp |
|
276 |
apply (rule pres_typeD) |
|
277 |
apply assumption |
|
278 |
prefer 3 apply assumption |
|
279 |
apply (blast intro: listE_nth_in dest: boundedD) |
|
280 |
apply (blast intro: pres_typeD dest: boundedD) |
|
281 |
apply (blast intro: listE_nth_in dest: boundedD) |
|
282 |
apply blast |
|
283 |
done |
|
13074 | 284 |
|
285 |
||
286 |
lemma (in semilat) merges_bounded_lemma: |
|
287 |
"\<lbrakk> mono r step n A; bounded step n; |
|
288 |
\<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; |
|
289 |
ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> |
|
13066 | 290 |
\<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" |
10496 | 291 |
apply (unfold stable_def) |
12516 | 292 |
apply (rule merges_pres_le_ub) |
293 |
apply simp |
|
294 |
apply simp |
|
295 |
prefer 2 apply assumption |
|
296 |
||
297 |
apply clarsimp |
|
298 |
apply (drule boundedD, assumption+) |
|
299 |
apply (erule allE, erule impE, assumption) |
|
300 |
apply (drule bspec, assumption) |
|
301 |
apply simp |
|
302 |
||
303 |
apply (drule monoD [of _ _ _ _ p "ss!p" "ts!p"]) |
|
304 |
apply assumption |
|
305 |
apply simp |
|
306 |
apply (simp add: le_listD) |
|
307 |
||
13066 | 308 |
apply (drule lesub_step_typeD, assumption) |
12516 | 309 |
apply clarify |
310 |
apply (drule bspec, assumption) |
|
311 |
apply simp |
|
312 |
apply (blast intro: order_trans) |
|
10496 | 313 |
done |
314 |
||
13074 | 315 |
lemma termination_lemma: includes semilat |
316 |
shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> |
|
12516 | 317 |
ss <[r] merges f qs ss \<or> |
318 |
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" |
|
13074 | 319 |
apply(insert semilat) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
320 |
apply (unfold lesssub_def) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
321 |
apply (simp (no_asm_simp) add: merges_incr) |
10496 | 322 |
apply (rule impI) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
323 |
apply (rule merges_same_conv [THEN iffD1, elim_format]) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
324 |
apply assumption+ |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
325 |
defer |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
326 |
apply (rule sym, assumption) |
12516 | 327 |
defer apply simp |
328 |
apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)") |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
329 |
apply (blast intro!: psubsetI elim: equalityE) |
12516 | 330 |
apply clarsimp |
331 |
apply (drule bspec, assumption) |
|
332 |
apply (drule bspec, assumption) |
|
333 |
apply clarsimp |
|
334 |
done |
|
10496 | 335 |
|
13074 | 336 |
lemma iter_properties[rule_format]: includes semilat |
337 |
shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A; |
|
12516 | 338 |
bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A; |
339 |
\<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow> |
|
340 |
iter f step ss0 w0 = (ss',w') |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
341 |
\<longrightarrow> |
12516 | 342 |
ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and> |
343 |
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)" |
|
13074 | 344 |
apply(insert semilat) |
11298 | 345 |
apply (unfold iter_def stables_def) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
346 |
apply (rule_tac P = "%(ss,w). |
12516 | 347 |
ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and> |
348 |
(\<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
|
349 |
(\<forall>p\<in>w. p < n)" and |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
350 |
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
|
351 |
in while_rule) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
352 |
|
12516 | 353 |
-- "Invariant holds initially:" |
13074 | 354 |
apply (simp add:stables_def) |
12516 | 355 |
|
356 |
-- "Invariant is preserved:" |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
357 |
apply(simp add: stables_def split_paired_all) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
358 |
apply(rename_tac ss w) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
359 |
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
|
360 |
prefer 2; apply (fast intro: someI) |
12516 | 361 |
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") |
362 |
prefer 2 |
|
363 |
apply clarify |
|
364 |
apply (rule conjI) |
|
365 |
apply(clarsimp, blast dest!: boundedD) |
|
366 |
apply (erule pres_typeD) |
|
367 |
prefer 3 |
|
368 |
apply assumption |
|
369 |
apply (erule listE_nth_in) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
370 |
apply simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
371 |
apply simp |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
372 |
apply (subst decomp_propa) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
373 |
apply fast |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
374 |
apply simp |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
375 |
apply (rule conjI) |
13074 | 376 |
apply (rule merges_preserves_type) |
377 |
apply blast |
|
12516 | 378 |
apply clarify |
379 |
apply (rule conjI) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14191
diff
changeset
|
380 |
apply(clarsimp, fast dest!: boundedD) |
12516 | 381 |
apply (erule pres_typeD) |
382 |
prefer 3 |
|
383 |
apply assumption |
|
384 |
apply (erule listE_nth_in) |
|
385 |
apply blast |
|
386 |
apply blast |
|
13074 | 387 |
apply (rule conjI) |
388 |
apply clarify |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
389 |
apply (blast intro!: stable_pres_lemma) |
13074 | 390 |
apply (rule conjI) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
391 |
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
|
392 |
apply (rule conjI) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
393 |
apply clarsimp |
12516 | 394 |
apply (blast intro!: merges_bounded_lemma) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
395 |
apply (blast dest!: boundedD) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
396 |
|
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
397 |
|
12516 | 398 |
-- "Postcondition holds upon termination:" |
13074 | 399 |
apply(clarsimp simp add: stables_def split_paired_all) |
12516 | 400 |
|
401 |
-- "Well-foundedness of the termination relation:" |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
402 |
apply (rule wf_lex_prod) |
13074 | 403 |
apply (insert orderI [THEN acc_le_listI]) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
404 |
apply (simp only: acc_def lesssub_def) |
12516 | 405 |
apply (rule wf_finite_psubset) |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
406 |
|
12516 | 407 |
-- "Loop decreases along termination relation:" |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
408 |
apply(simp add: stables_def split_paired_all) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
409 |
apply(rename_tac ss w) |
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
410 |
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
|
411 |
prefer 2; apply (fast intro: someI) |
12516 | 412 |
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") |
413 |
prefer 2 |
|
414 |
apply clarify |
|
415 |
apply (rule conjI) |
|
416 |
apply(clarsimp, blast dest!: boundedD) |
|
417 |
apply (erule pres_typeD) |
|
418 |
prefer 3 |
|
419 |
apply assumption |
|
420 |
apply (erule listE_nth_in) |
|
421 |
apply blast |
|
422 |
apply blast |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
423 |
apply (subst decomp_propa) |
12516 | 424 |
apply blast |
13074 | 425 |
apply clarify |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
426 |
apply (simp del: listE_length |
12516 | 427 |
add: lex_prod_def finite_psubset_def |
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
428 |
bounded_nat_set_is_finite) |
12516 | 429 |
apply (rule termination_lemma) |
430 |
apply assumption+ |
|
431 |
defer |
|
432 |
apply assumption |
|
433 |
apply clarsimp |
|
13074 | 434 |
done |
12516 | 435 |
|
11175
56ab6a5ba351
recoded function iter with the help of the while-combinator.
nipkow
parents:
10774
diff
changeset
|
436 |
|
13074 | 437 |
lemma kildall_properties: includes semilat |
438 |
shows "\<lbrakk> acc r; pres_type step n A; mono r step n A; |
|
12516 | 439 |
bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow> |
440 |
kildall r f step ss0 \<in> list n A \<and> |
|
441 |
stables r step (kildall r f step ss0) \<and> |
|
442 |
ss0 <=[r] kildall r f step ss0 \<and> |
|
443 |
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> |
|
444 |
kildall r f step ss0 <=[r] ts)" |
|
11229 | 445 |
apply (unfold kildall_def) |
12516 | 446 |
apply(case_tac "iter f step ss0 (unstables r step ss0)") |
11298 | 447 |
apply(simp) |
11229 | 448 |
apply (rule iter_properties) |
13074 | 449 |
by (simp_all add: unstables_def stable_def) |
450 |
||
10496 | 451 |
|
13074 | 452 |
lemma is_bcv_kildall: includes semilat |
453 |
shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk> |
|
13006 | 454 |
\<Longrightarrow> is_bcv r T step n A (kildall r f step)" |
11299 | 455 |
apply(unfold is_bcv_def wt_step_def) |
13074 | 456 |
apply(insert semilat kildall_properties[of A]) |
11229 | 457 |
apply(simp add:stables_def) |
458 |
apply clarify |
|
12516 | 459 |
apply(subgoal_tac "kildall r f step ss \<in> list n A") |
11229 | 460 |
prefer 2 apply (simp(no_asm_simp)) |
461 |
apply (rule iffI) |
|
12516 | 462 |
apply (rule_tac x = "kildall r f step ss" in bexI) |
11229 | 463 |
apply (rule conjI) |
13074 | 464 |
apply (blast) |
11229 | 465 |
apply (simp (no_asm_simp)) |
13074 | 466 |
apply(assumption) |
11229 | 467 |
apply clarify |
12516 | 468 |
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p") |
11229 | 469 |
apply simp |
470 |
apply (blast intro!: le_listD less_lengthI) |
|
471 |
done |
|
10496 | 472 |
|
14191 | 473 |
end |