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