author | nipkow |
Tue, 16 Aug 2005 19:25:42 +0200 | |
changeset 17087 | 0abf74bdf712 |
parent 16417 | 9bc16273c2d4 |
child 17090 | 603f23d71ada |
permissions | -rw-r--r-- |
8388 | 1 |
(* Title: HOL/MicroJava/BV/LBVComplete.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8388 | 6 |
|
12911 | 7 |
header {* \isaheader{Completeness of the LBV} *} |
8388 | 8 |
|
16417 | 9 |
theory LBVComplete imports LBVSpec Typing_Framework begin |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
10 |
|
8388 | 11 |
constdefs |
13078 | 12 |
is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" |
13 |
"is_target step phi pc' \<equiv> |
|
14 |
\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))" |
|
8388 | 15 |
|
13078 | 16 |
make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" |
17 |
"make_cert step phi B \<equiv> |
|
15425 | 18 |
map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]" |
13078 | 19 |
|
13101 | 20 |
constdefs |
21 |
list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
|
22 |
"list_ex P xs \<equiv> \<exists>x \<in> set xs. P x" |
|
23 |
||
24 |
lemma [code]: "list_ex P [] = False" by (simp add: list_ex_def) |
|
25 |
lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def) |
|
26 |
||
27 |
lemma [code]: |
|
28 |
"is_target step phi pc' = |
|
15425 | 29 |
list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]" |
17087 | 30 |
apply (simp add: list_ex_def is_target_def mem_iff) |
13101 | 31 |
apply force |
32 |
done |
|
33 |
||
13365 | 34 |
locale (open) lbvc = lbv + |
13078 | 35 |
fixes phi :: "'a list" ("\<phi>") |
36 |
fixes c :: "'a list" |
|
37 |
defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
|
9012 | 38 |
|
13078 | 39 |
assumes mono: "mono r step (length \<phi>) A" |
40 |
assumes pres: "pres_type step (length \<phi>) A" |
|
41 |
assumes phi: "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>" |
|
42 |
assumes bounded: "bounded step (length \<phi>)" |
|
43 |
||
44 |
assumes B_neq_T: "\<bottom> \<noteq> \<top>" |
|
45 |
||
8388 | 46 |
|
13078 | 47 |
lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A" |
48 |
proof (unfold cert_ok_def, intro strip conjI) |
|
49 |
note [simp] = make_cert_def cert_def nth_append |
|
50 |
||
51 |
show "c!length \<phi> = \<bottom>" by simp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
52 |
|
13078 | 53 |
fix pc assume pc: "pc < length \<phi>" |
54 |
from pc phi B_A show "c!pc \<in> A" by simp |
|
55 |
from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp |
|
56 |
qed |
|
57 |
||
9559 | 58 |
lemmas [simp del] = split_paired_Ex |
59 |
||
9012 | 60 |
|
13078 | 61 |
lemma (in lbvc) cert_target [intro?]: |
62 |
"\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc)); |
|
63 |
pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk> |
|
64 |
\<Longrightarrow> c!pc' = \<phi>!pc'" |
|
65 |
by (auto simp add: cert_def make_cert_def nth_append is_target_def) |
|
9012 | 66 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
67 |
|
13078 | 68 |
lemma (in lbvc) cert_approx [intro?]: |
69 |
"\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk> |
|
70 |
\<Longrightarrow> c!pc = \<phi>!pc" |
|
71 |
by (auto simp add: cert_def make_cert_def nth_append) |
|
13064 | 72 |
|
73 |
||
13078 | 74 |
lemma (in lbv) le_top [simp, intro]: |
75 |
"x <=_r \<top>" |
|
76 |
by (insert top) simp |
|
77 |
||
78 |
||
79 |
lemma (in lbv) merge_mono: |
|
80 |
assumes less: "ss2 <=|r| ss1" |
|
81 |
assumes x: "x \<in> A" |
|
82 |
assumes ss1: "snd`set ss1 \<subseteq> A" |
|
83 |
assumes ss2: "snd`set ss2 \<subseteq> A" |
|
84 |
shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1") |
|
13064 | 85 |
proof- |
13078 | 86 |
have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp |
13070 | 87 |
moreover { |
13078 | 88 |
assume merge: "?s1 \<noteq> T" |
89 |
from x ss1 have "?s1 = |
|
90 |
(if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc' |
|
91 |
then (map snd [(p', t')\<in>ss1 . p'=pc+1]) ++_f x |
|
92 |
else \<top>)" |
|
93 |
by (rule merge_def) |
|
94 |
with merge obtain |
|
95 |
app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" |
|
96 |
(is "?app ss1") and |
|
97 |
sum: "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++_f x) = ?s1" |
|
98 |
(is "?map ss1 ++_f x = _" is "?sum ss1 = _") |
|
99 |
by (simp split: split_if_asm) |
|
100 |
from app less |
|
101 |
have "?app ss2" by (blast dest: trans_r lesub_step_typeD) |
|
13070 | 102 |
moreover { |
13078 | 103 |
from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto |
104 |
with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed) |
|
105 |
with sum have "?s1 \<in> A" by simp |
|
106 |
moreover |
|
107 |
have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto |
|
108 |
from x map1 |
|
109 |
have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1" |
|
110 |
by clarify (rule pp_ub1) |
|
111 |
with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp |
|
112 |
with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1" |
|
113 |
by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r) |
|
114 |
moreover |
|
115 |
from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2) |
|
116 |
with sum have "x <=_r ?s1" by simp |
|
117 |
moreover |
|
118 |
from ss2 have "set (?map ss2) \<subseteq> A" by auto |
|
119 |
ultimately |
|
120 |
have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub) |
|
121 |
} |
|
122 |
moreover |
|
123 |
from x ss2 have |
|
124 |
"?s2 = |
|
125 |
(if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc' |
|
126 |
then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++_f x |
|
127 |
else \<top>)" |
|
128 |
by (rule merge_def) |
|
129 |
ultimately have ?thesis by simp |
|
13070 | 130 |
} |
13078 | 131 |
ultimately show ?thesis by (cases "?s1 = \<top>") auto |
13064 | 132 |
qed |
133 |
||
134 |
||
13078 | 135 |
lemma (in lbvc) wti_mono: |
136 |
assumes less: "s2 <=_r s1" |
|
137 |
assumes pc: "pc < length \<phi>" |
|
138 |
assumes s1: "s1 \<in> A" |
|
139 |
assumes s2: "s2 \<in> A" |
|
140 |
shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'") |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
141 |
proof - |
13078 | 142 |
from mono s2 have "step pc s2 <=|r| step pc s1" by - (rule monoD) |
13071 | 143 |
moreover |
13078 | 144 |
from pc cert have "c!Suc pc \<in> A" by - (rule cert_okD3) |
145 |
moreover |
|
146 |
from pres s1 pc |
|
147 |
have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2) |
|
13071 | 148 |
moreover |
149 |
from pres s2 pc |
|
13078 | 150 |
have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2) |
13071 | 151 |
ultimately |
13078 | 152 |
show ?thesis by (simp add: wti merge_mono) |
13071 | 153 |
qed |
9012 | 154 |
|
13078 | 155 |
lemma (in lbvc) wtc_mono: |
156 |
assumes less: "s2 <=_r s1" |
|
157 |
assumes pc: "pc < length \<phi>" |
|
158 |
assumes s1: "s1 \<in> A" |
|
159 |
assumes s2: "s2 \<in> A" |
|
160 |
shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'") |
|
161 |
proof (cases "c!pc = \<bottom>") |
|
162 |
case True |
|
163 |
moreover have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono) |
|
164 |
ultimately show ?thesis by (simp add: wtc) |
|
13071 | 165 |
next |
13078 | 166 |
case False |
167 |
have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp |
|
168 |
moreover { |
|
169 |
assume "?s1' \<noteq> \<top>" |
|
170 |
with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm) |
|
171 |
with less have "s2 <=_r c!pc" .. |
|
172 |
with False c have ?thesis by (simp add: wtc) |
|
173 |
} |
|
174 |
ultimately show ?thesis by (cases "?s1' = \<top>") auto |
|
9376 | 175 |
qed |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
|
9559 | 177 |
|
13078 | 178 |
lemma (in lbv) top_le_conv [simp]: |
179 |
"\<top> <=_r x = (x = \<top>)" |
|
180 |
by (insert semilat) (simp add: top top_le_conv) |
|
181 |
||
182 |
lemma (in lbv) neq_top [simp, elim]: |
|
183 |
"\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>" |
|
184 |
by (cases "x = T") auto |
|
185 |
||
186 |
||
187 |
lemma (in lbvc) stable_wti: |
|
188 |
assumes stable: "stable r step \<phi> pc" |
|
189 |
assumes pc: "pc < length \<phi>" |
|
190 |
shows "wti c pc (\<phi>!pc) \<noteq> \<top>" |
|
9559 | 191 |
proof - |
13078 | 192 |
let ?step = "step pc (\<phi>!pc)" |
13071 | 193 |
from stable |
13078 | 194 |
have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def) |
13071 | 195 |
|
13078 | 196 |
from cert pc |
197 |
have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3) |
|
13071 | 198 |
moreover |
13078 | 199 |
from phi pc have "\<phi>!pc \<in> A" by simp |
13071 | 200 |
with pres pc |
13078 | 201 |
have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2) |
13071 | 202 |
ultimately |
13078 | 203 |
have "merge c pc ?step (c!Suc pc) = |
204 |
(if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' |
|
205 |
then map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc |
|
206 |
else \<top>)" by (rule merge_def) |
|
13071 | 207 |
moreover { |
208 |
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1" |
|
13078 | 209 |
with less have "s' <=_r \<phi>!pc'" by auto |
210 |
also |
|
211 |
from bounded pc s' have "pc' < length \<phi>" by (rule boundedD) |
|
212 |
with s' suc_pc pc have "c!pc' = \<phi>!pc'" .. |
|
213 |
hence "\<phi>!pc' = c!pc'" .. |
|
214 |
finally have "s' <=_r c!pc'" . |
|
215 |
} hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto |
|
13071 | 216 |
moreover |
13078 | 217 |
from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto |
218 |
hence "map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" |
|
219 |
(is "?map ++_f _ \<noteq> _") |
|
13071 | 220 |
proof (rule disjE) |
13078 | 221 |
assume pc': "Suc pc = length \<phi>" |
222 |
with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2) |
|
13071 | 223 |
moreover |
13078 | 224 |
from pc' bounded pc |
13071 | 225 |
have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto) |
226 |
hence "[(p',t')\<in>?step.p'=pc+1] = []" by (blast intro: filter_False) |
|
227 |
hence "?map = []" by simp |
|
13078 | 228 |
ultimately show ?thesis by (simp add: B_neq_T) |
13071 | 229 |
next |
13078 | 230 |
assume pc': "Suc pc < length \<phi>" |
231 |
from pc' phi have "\<phi>!Suc pc \<in> A" by simp |
|
13071 | 232 |
moreover note cert_suc |
233 |
moreover from stepA |
|
13078 | 234 |
have "set ?map \<subseteq> A" by auto |
13071 | 235 |
moreover |
236 |
have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto |
|
13078 | 237 |
with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto |
13071 | 238 |
moreover |
13078 | 239 |
from pc' have "c!Suc pc <=_r \<phi>!Suc pc" |
240 |
by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx) |
|
13071 | 241 |
ultimately |
13078 | 242 |
have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub) |
243 |
moreover |
|
244 |
from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp |
|
245 |
ultimately |
|
246 |
show ?thesis by auto |
|
9559 | 247 |
qed |
13071 | 248 |
ultimately |
13078 | 249 |
have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp |
250 |
thus ?thesis by (simp add: wti) |
|
9376 | 251 |
qed |
9012 | 252 |
|
13078 | 253 |
lemma (in lbvc) wti_less: |
254 |
assumes stable: "stable r step \<phi> pc" |
|
255 |
assumes suc_pc: "Suc pc < length \<phi>" |
|
256 |
shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _") |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
257 |
proof - |
13078 | 258 |
let ?step = "step pc (\<phi>!pc)" |
13071 | 259 |
|
13078 | 260 |
from stable |
261 |
have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def) |
|
262 |
||
263 |
from suc_pc have pc: "pc < length \<phi>" by simp |
|
264 |
with cert have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3) |
|
13071 | 265 |
moreover |
13078 | 266 |
from phi pc have "\<phi>!pc \<in> A" by simp |
267 |
with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2) |
|
268 |
moreover |
|
269 |
from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti) |
|
270 |
hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti) |
|
13071 | 271 |
ultimately |
13078 | 272 |
have "merge c pc ?step (c!Suc pc) = |
273 |
map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) |
|
274 |
hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti) |
|
13071 | 275 |
also { |
13078 | 276 |
from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp |
13071 | 277 |
moreover note cert_suc |
13078 | 278 |
moreover from stepA have "set ?map \<subseteq> A" by auto |
13071 | 279 |
moreover |
280 |
have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto |
|
13078 | 281 |
with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto |
13071 | 282 |
moreover |
13078 | 283 |
from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc" |
284 |
by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx) |
|
13071 | 285 |
ultimately |
13078 | 286 |
have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub) |
13071 | 287 |
} |
288 |
finally show ?thesis . |
|
289 |
qed |
|
9012 | 290 |
|
13078 | 291 |
lemma (in lbvc) stable_wtc: |
292 |
assumes stable: "stable r step phi pc" |
|
293 |
assumes pc: "pc < length \<phi>" |
|
294 |
shows "wtc c pc (\<phi>!pc) \<noteq> \<top>" |
|
295 |
proof - |
|
296 |
have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti) |
|
297 |
show ?thesis |
|
298 |
proof (cases "c!pc = \<bottom>") |
|
299 |
case True with wti show ?thesis by (simp add: wtc) |
|
300 |
next |
|
301 |
case False |
|
302 |
with pc have "c!pc = \<phi>!pc" .. |
|
303 |
with False wti show ?thesis by (simp add: wtc) |
|
304 |
qed |
|
305 |
qed |
|
9012 | 306 |
|
13078 | 307 |
lemma (in lbvc) wtc_less: |
308 |
assumes stable: "stable r step \<phi> pc" |
|
309 |
assumes suc_pc: "Suc pc < length \<phi>" |
|
310 |
shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _") |
|
311 |
proof (cases "c!pc = \<bottom>") |
|
312 |
case True |
|
313 |
moreover have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less) |
|
314 |
ultimately show ?thesis by (simp add: wtc) |
|
13071 | 315 |
next |
13078 | 316 |
case False |
317 |
from suc_pc have pc: "pc < length \<phi>" by simp |
|
318 |
hence "?wtc \<noteq> \<top>" by - (rule stable_wtc) |
|
319 |
with False have "?wtc = wti c pc (c!pc)" |
|
320 |
by (unfold wtc) (simp split: split_if_asm) |
|
321 |
also from pc False have "c!pc = \<phi>!pc" .. |
|
322 |
finally have "?wtc = wti c pc (\<phi>!pc)" . |
|
323 |
also have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less) |
|
324 |
finally show ?thesis . |
|
13071 | 325 |
qed |
326 |
||
327 |
||
13078 | 328 |
lemma (in lbvc) wt_step_wtl_lemma: |
329 |
assumes wt_step: "wt_step r \<top> step \<phi>" |
|
330 |
shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> |
|
331 |
wtl ls c pc s \<noteq> \<top>" |
|
332 |
(is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _") |
|
333 |
proof (induct ls) |
|
334 |
fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp |
|
13071 | 335 |
next |
13078 | 336 |
fix pc s i ls |
337 |
assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> |
|
338 |
?wtl ls pc s \<noteq> \<top>" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
339 |
moreover |
13078 | 340 |
assume pc_l: "pc + length (i#ls) = length \<phi>" |
341 |
hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp |
|
13071 | 342 |
ultimately |
13078 | 343 |
have IH: "\<And>s. s <=_r \<phi>!Suc pc \<Longrightarrow> s \<in> A \<Longrightarrow> s \<noteq> \<top> \<Longrightarrow> ?wtl ls (Suc pc) s \<noteq> \<top>" . |
13071 | 344 |
|
13078 | 345 |
from pc_l obtain pc: "pc < length \<phi>" by simp |
346 |
with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def) |
|
13071 | 347 |
moreover |
13078 | 348 |
assume s_phi: "s <=_r \<phi>!pc" |
13071 | 349 |
ultimately |
13078 | 350 |
have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by - (rule stable_wtc) |
351 |
||
352 |
from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp |
|
13071 | 353 |
moreover |
13078 | 354 |
assume s: "s \<in> A" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
355 |
ultimately |
13078 | 356 |
have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" using s_phi by - (rule wtc_mono) |
357 |
with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp |
|
358 |
moreover |
|
359 |
assume s: "s \<noteq> \<top>" |
|
360 |
ultimately |
|
361 |
have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp |
|
13071 | 362 |
moreover { |
13078 | 363 |
assume "ls \<noteq> []" |
364 |
with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv) |
|
365 |
with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less) |
|
366 |
with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r) |
|
13071 | 367 |
moreover |
13078 | 368 |
from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" |
13071 | 369 |
by (auto simp add: cert_ok_def) |
13078 | 370 |
with pres have "wtc c pc s \<in> A" by (rule wtc_pres) |
371 |
ultimately |
|
372 |
have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast |
|
373 |
with s wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp |
|
13071 | 374 |
} |
13078 | 375 |
ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+ |
9580 | 376 |
qed |
9012 | 377 |
|
13078 | 378 |
|
379 |
theorem (in lbvc) wtl_complete: |
|
380 |
assumes "wt_step r \<top> step \<phi>" |
|
381 |
assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi" |
|
382 |
shows "wtl ins c 0 s \<noteq> \<top>" |
|
383 |
proof - |
|
13071 | 384 |
have "0+length ins = length phi" by simp |
13078 | 385 |
thus ?thesis by - (rule wt_step_wtl_lemma) |
13071 | 386 |
qed |
10592 | 387 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
388 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
389 |
end |