author | kleing |
Wed, 07 Jan 2004 07:52:12 +0100 | |
changeset 14343 | 6bc647f472b9 |
parent 13365 | a2c4faad4d35 |
child 15109 | bba563cdd997 |
permissions | -rw-r--r-- |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
1 |
(* Title: HOL/MicroJava/BV/LBVSpec.thy |
8245 | 2 |
ID: $Id$ |
3 |
Author: Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8245 | 6 |
|
12911 | 7 |
header {* \isaheader{The Lightweight Bytecode Verifier} *} |
9054 | 8 |
|
13062 | 9 |
theory LBVSpec = SemilatAlg + Opt: |
10 |
||
8245 | 11 |
types |
13078 | 12 |
's certificate = "'s list" |
8245 | 13 |
|
12516 | 14 |
consts |
13078 | 15 |
merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" |
12516 | 16 |
primrec |
13078 | 17 |
"merge cert f r T pc [] x = x" |
18 |
"merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in |
|
19 |
if pc'=pc+1 then s' +_f x |
|
20 |
else if s' <=_r (cert!pc') then x |
|
21 |
else T)" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
22 |
|
13062 | 23 |
constdefs |
13078 | 24 |
wtl_inst :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> |
25 |
's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
|
26 |
"wtl_inst cert f r T step pc s \<equiv> merge cert f r T pc (step pc s) (cert!(pc+1))" |
|
8245 | 27 |
|
13078 | 28 |
wtl_cert :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
29 |
's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
|
30 |
"wtl_cert cert f r T B step pc s \<equiv> |
|
31 |
if cert!pc = B then |
|
32 |
wtl_inst cert f r T step pc s |
|
33 |
else |
|
34 |
if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
36 |
consts |
13078 | 37 |
wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
38 |
's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
|
8245 | 39 |
primrec |
13101 | 40 |
"wtl_inst_list [] cert f r T B step pc s = s" |
41 |
"wtl_inst_list (i#is) cert f r T B step pc s = |
|
13078 | 42 |
(let s' = wtl_cert cert f r T B step pc s in |
13101 | 43 |
if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')" |
8245 | 44 |
|
45 |
constdefs |
|
13078 | 46 |
cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool" |
47 |
"cert_ok cert n T B A \<equiv> (\<forall>i < n. cert!i \<in> A \<and> cert!i \<noteq> T) \<and> (cert!n = B)" |
|
48 |
||
49 |
constdefs |
|
50 |
bottom :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
|
51 |
"bottom r B \<equiv> \<forall>x. B <=_r x" |
|
52 |
||
53 |
||
13365 | 54 |
locale (open) lbv = semilat + |
13078 | 55 |
fixes T :: "'a" ("\<top>") |
56 |
fixes B :: "'a" ("\<bottom>") |
|
57 |
fixes step :: "'a step_type" |
|
58 |
assumes top: "top r \<top>" |
|
59 |
assumes T_A: "\<top> \<in> A" |
|
60 |
assumes bot: "bottom r \<bottom>" |
|
61 |
assumes B_A: "\<bottom> \<in> A" |
|
62 |
||
63 |
fixes merge :: "'a certificate \<Rightarrow> nat \<Rightarrow> (nat \<times> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" |
|
64 |
defines mrg_def: "merge cert \<equiv> LBVSpec.merge cert f r \<top>" |
|
13062 | 65 |
|
13078 | 66 |
fixes wti :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" |
67 |
defines wti_def: "wti cert \<equiv> wtl_inst cert f r \<top> step" |
|
68 |
||
69 |
fixes wtc :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
70 |
defines wtc_def: "wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step" |
|
71 |
||
72 |
fixes wtl :: "'b list \<Rightarrow> 'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
73 |
defines wtl_def: "wtl ins cert \<equiv> wtl_inst_list ins cert f r \<top> \<bottom> step" |
|
74 |
||
75 |
||
76 |
lemma (in lbv) wti: |
|
77 |
"wti c pc s \<equiv> merge c pc (step pc s) (c!(pc+1))" |
|
78 |
by (simp add: wti_def mrg_def wtl_inst_def) |
|
79 |
||
80 |
lemma (in lbv) wtc: |
|
81 |
"wtc c pc s \<equiv> if c!pc = \<bottom> then wti c pc s else if s <=_r c!pc then wti c pc (c!pc) else \<top>" |
|
82 |
by (unfold wtc_def wti_def wtl_cert_def) |
|
83 |
||
84 |
||
85 |
lemma cert_okD1 [intro?]: |
|
86 |
"cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<in> A" |
|
13062 | 87 |
by (unfold cert_ok_def) fast |
88 |
||
13078 | 89 |
lemma cert_okD2 [intro?]: |
90 |
"cert_ok c n T B A \<Longrightarrow> c!n = B" |
|
13071 | 91 |
by (simp add: cert_ok_def) |
92 |
||
13078 | 93 |
lemma cert_okD3 [intro?]: |
94 |
"cert_ok c n T B A \<Longrightarrow> B \<in> A \<Longrightarrow> pc < n \<Longrightarrow> c!Suc pc \<in> A" |
|
13071 | 95 |
by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2) |
96 |
||
13078 | 97 |
lemma cert_okD4 [intro?]: |
98 |
"cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<noteq> T" |
|
99 |
by (simp add: cert_ok_def) |
|
13062 | 100 |
|
101 |
declare Let_def [simp] |
|
102 |
||
103 |
section "more semilattice lemmas" |
|
104 |
||
13078 | 105 |
|
106 |
lemma (in lbv) sup_top [simp, elim]: |
|
107 |
assumes x: "x \<in> A" |
|
108 |
shows "x +_f \<top> = \<top>" |
|
13062 | 109 |
proof - |
13078 | 110 |
from top have "x +_f \<top> <=_r \<top>" .. |
111 |
moreover from x have "\<top> <=_r x +_f \<top>" .. |
|
112 |
ultimately show ?thesis .. |
|
13062 | 113 |
qed |
114 |
||
13078 | 115 |
lemma (in lbv) plusplussup_top [simp, elim]: |
116 |
"set xs \<subseteq> A \<Longrightarrow> xs ++_f \<top> = \<top>" |
|
13062 | 117 |
by (induct xs) auto |
13078 | 118 |
|
119 |
||
13062 | 120 |
|
13078 | 121 |
lemma (in semilat) pp_ub1': |
122 |
assumes S: "snd`set S \<subseteq> A" |
|
123 |
assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" |
|
124 |
shows "b <=_r map snd [(p', t')\<in>S . p' = a] ++_f y" |
|
125 |
proof - |
|
126 |
from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto |
|
127 |
with semilat y ab show ?thesis by - (rule ub1') |
|
128 |
qed |
|
13062 | 129 |
|
13078 | 130 |
lemma (in lbv) bottom_le [simp, intro]: |
131 |
"\<bottom> <=_r x" |
|
132 |
by (insert bot) (simp add: bottom_def) |
|
13062 | 133 |
|
13078 | 134 |
lemma (in lbv) le_bottom [simp]: |
135 |
"x <=_r \<bottom> = (x = \<bottom>)" |
|
136 |
by (blast intro: antisym_r) |
|
137 |
||
13062 | 138 |
|
139 |
||
140 |
section "merge" |
|
141 |
||
13078 | 142 |
lemma (in lbv) merge_Nil [simp]: |
143 |
"merge c pc [] x = x" by (simp add: mrg_def) |
|
144 |
||
145 |
lemma (in lbv) merge_Cons [simp]: |
|
146 |
"merge c pc (l#ls) x = merge c pc ls (if fst l=pc+1 then snd l +_f x |
|
147 |
else if snd l <=_r (c!fst l) then x |
|
148 |
else \<top>)" |
|
149 |
by (simp add: mrg_def split_beta) |
|
150 |
||
151 |
lemma (in lbv) merge_Err [simp]: |
|
152 |
"snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss \<top> = \<top>" |
|
13062 | 153 |
by (induct ss) auto |
8245 | 154 |
|
13078 | 155 |
lemma (in lbv) merge_not_top: |
156 |
"\<And>x. snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss x \<noteq> \<top> \<Longrightarrow> |
|
157 |
\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc'))" |
|
158 |
(is "\<And>x. ?set ss \<Longrightarrow> ?merge ss x \<Longrightarrow> ?P ss") |
|
13062 | 159 |
proof (induct ss) |
160 |
show "?P []" by simp |
|
161 |
next |
|
13078 | 162 |
fix x ls l |
163 |
assume "?set (l#ls)" then obtain set: "snd`set ls \<subseteq> A" by simp |
|
164 |
assume merge: "?merge (l#ls) x" |
|
13062 | 165 |
moreover |
166 |
obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) |
|
167 |
ultimately |
|
13078 | 168 |
obtain x' where "?merge ls x'" by simp |
169 |
assume "\<And>x. ?set ls \<Longrightarrow> ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" . |
|
13062 | 170 |
moreover |
13078 | 171 |
from merge set |
172 |
have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc')" by (simp split: split_if_asm) |
|
13062 | 173 |
ultimately |
174 |
show "?P (l#ls)" by simp |
|
175 |
qed |
|
176 |
||
9012 | 177 |
|
13078 | 178 |
lemma (in lbv) merge_def: |
13062 | 179 |
shows |
13078 | 180 |
"\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow> |
181 |
merge c pc ss x = |
|
182 |
(if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then |
|
183 |
map snd [(p',t') \<in> ss. p'=pc+1] ++_f x |
|
184 |
else \<top>)" |
|
13062 | 185 |
(is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x") |
186 |
proof (induct ss) |
|
187 |
fix x show "?P [] x" by simp |
|
188 |
next |
|
13078 | 189 |
fix x assume x: "x \<in> A" |
190 |
fix l::"nat \<times> 'a" and ls |
|
191 |
assume "snd`set (l#ls) \<subseteq> A" |
|
192 |
then obtain l: "snd l \<in> A" and ls: "snd`set ls \<subseteq> A" by auto |
|
193 |
assume "\<And>x. x \<in> A \<Longrightarrow> snd`set ls \<subseteq> A \<Longrightarrow> ?P ls x" |
|
194 |
hence IH: "\<And>x. x \<in> A \<Longrightarrow> ?P ls x" . |
|
13062 | 195 |
obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) |
196 |
hence "?merge (l#ls) x = ?merge ls |
|
13078 | 197 |
(if pc'=pc+1 then s' +_f x else if s' <=_r c!pc' then x else \<top>)" |
13062 | 198 |
(is "?merge (l#ls) x = ?merge ls ?if'") |
199 |
by simp |
|
200 |
also have "\<dots> = ?if ls ?if'" |
|
201 |
proof - |
|
13078 | 202 |
from l have "s' \<in> A" by simp |
203 |
with x have "s' +_f x \<in> A" by simp |
|
204 |
with x have "?if' \<in> A" by auto |
|
13062 | 205 |
hence "?P ls ?if'" by (rule IH) thus ?thesis by simp |
206 |
qed |
|
207 |
also have "\<dots> = ?if (l#ls) x" |
|
13078 | 208 |
proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'") |
13062 | 209 |
case True |
13078 | 210 |
hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto |
13062 | 211 |
moreover |
212 |
from True have |
|
13078 | 213 |
"map snd [(p',t')\<in>ls . p'=pc+1] ++_f ?if' = |
214 |
(map snd [(p',t')\<in>l#ls . p'=pc+1] ++_f x)" |
|
13062 | 215 |
by simp |
216 |
ultimately |
|
217 |
show ?thesis using True by simp |
|
218 |
next |
|
13078 | 219 |
case False |
220 |
moreover |
|
221 |
from ls have "set (map snd [(p', t')\<in>ls . p' = Suc pc]) \<subseteq> A" by auto |
|
222 |
ultimately show ?thesis by auto |
|
13062 | 223 |
qed |
224 |
finally show "?P (l#ls) x" . |
|
225 |
qed |
|
226 |
||
13078 | 227 |
lemma (in lbv) merge_not_top_s: |
228 |
assumes x: "x \<in> A" and ss: "snd`set ss \<subseteq> A" |
|
229 |
assumes m: "merge c pc ss x \<noteq> \<top>" |
|
230 |
shows "merge c pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++_f x)" |
|
13062 | 231 |
proof - |
13078 | 232 |
from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')" |
233 |
by (rule merge_not_top) |
|
234 |
with x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm) |
|
13062 | 235 |
qed |
236 |
||
237 |
section "wtl-inst-list" |
|
10042 | 238 |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
239 |
lemmas [iff] = not_Err_eq |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
240 |
|
13078 | 241 |
lemma (in lbv) wtl_Nil [simp]: "wtl [] c pc s = s" |
242 |
by (simp add: wtl_def) |
|
243 |
||
244 |
lemma (in lbv) wtl_Cons [simp]: |
|
245 |
"wtl (i#is) c pc s = |
|
246 |
(let s' = wtc c pc s in if s' = \<top> \<or> s = \<top> then \<top> else wtl is c (pc+1) s')" |
|
247 |
by (simp add: wtl_def wtc_def) |
|
248 |
||
249 |
lemma (in lbv) wtl_Cons_not_top: |
|
250 |
"wtl (i#is) c pc s \<noteq> \<top> = |
|
251 |
(wtc c pc s \<noteq> \<top> \<and> s \<noteq> T \<and> wtl is c (pc+1) (wtc c pc s) \<noteq> \<top>)" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
252 |
by (auto simp del: split_paired_Ex) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
253 |
|
13078 | 254 |
lemma (in lbv) wtl_top [simp]: "wtl ls c pc \<top> = \<top>" |
255 |
by (cases ls) auto |
|
256 |
||
257 |
lemma (in lbv) wtl_not_top: |
|
258 |
"wtl ls c pc s \<noteq> \<top> \<Longrightarrow> s \<noteq> \<top>" |
|
259 |
by (cases "s=\<top>") auto |
|
9012 | 260 |
|
13078 | 261 |
lemma (in lbv) wtl_append [simp]: |
262 |
"\<And>pc s. wtl (a@b) c pc s = wtl b c (pc+length a) (wtl a c pc s)" |
|
263 |
by (induct a) auto |
|
264 |
||
265 |
lemma (in lbv) wtl_take: |
|
266 |
"wtl is c pc s \<noteq> \<top> \<Longrightarrow> wtl (take pc' is) c pc s \<noteq> \<top>" |
|
267 |
(is "?wtl is \<noteq> _ \<Longrightarrow> _") |
|
9183 | 268 |
proof - |
13078 | 269 |
assume "?wtl is \<noteq> \<top>" |
270 |
hence "?wtl (take pc' is @ drop pc' is) \<noteq> \<top>" by simp |
|
271 |
thus ?thesis by (auto dest!: wtl_not_top simp del: append_take_drop_id) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
272 |
qed |
9012 | 273 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
274 |
lemma take_Suc: |
13078 | 275 |
"\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l") |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
276 |
proof (induct l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
277 |
show "?P []" by simp |
12516 | 278 |
next |
279 |
fix x xs assume IH: "?P xs" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
280 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
281 |
proof (intro strip) |
12516 | 282 |
fix n assume "n < length (x#xs)" |
283 |
with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" |
|
284 |
by (cases n, auto) |
|
9183 | 285 |
qed |
286 |
qed |
|
9012 | 287 |
|
13078 | 288 |
lemma (in lbv) wtl_Suc: |
289 |
assumes suc: "pc+1 < length is" |
|
290 |
assumes wtl: "wtl (take pc is) c 0 s \<noteq> \<top>" |
|
291 |
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)" |
|
9183 | 292 |
proof - |
13062 | 293 |
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc) |
13078 | 294 |
with suc wtl show ?thesis by (simp add: min_def) |
9183 | 295 |
qed |
9012 | 296 |
|
13078 | 297 |
lemma (in lbv) wtl_all: |
298 |
assumes all: "wtl is c 0 s \<noteq> \<top>" (is "?wtl is \<noteq> _") |
|
299 |
assumes pc: "pc < length is" |
|
300 |
shows "wtc c pc (wtl (take pc is) c 0 s) \<noteq> \<top>" |
|
9183 | 301 |
proof - |
13062 | 302 |
from pc have "0 < length (drop pc is)" by simp |
12516 | 303 |
then obtain i r where Cons: "drop pc is = i#r" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
304 |
by (auto simp add: neq_Nil_conv simp del: length_drop) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
305 |
hence "i#r = drop pc is" .. |
13078 | 306 |
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp |
12516 | 307 |
from pc have "is!pc = drop pc is ! 0" by simp |
308 |
with Cons have "is!pc = i" by simp |
|
13078 | 309 |
with take pc show ?thesis by (auto simp add: min_def split: split_if_asm) |
9183 | 310 |
qed |
9012 | 311 |
|
13062 | 312 |
section "preserves-type" |
313 |
||
13078 | 314 |
lemma (in lbv) merge_pres: |
315 |
assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A" |
|
316 |
shows "merge c pc ss x \<in> A" |
|
13062 | 317 |
proof - |
13078 | 318 |
from s0 have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> A" by auto |
319 |
with x have "(map snd [(p', t')\<in>ss . p'=pc+1] ++_f x) \<in> A" |
|
13062 | 320 |
by (auto intro!: plusplus_closed) |
13078 | 321 |
with s0 x show ?thesis by (simp add: merge_def T_A) |
13062 | 322 |
qed |
323 |
||
324 |
||
13078 | 325 |
lemma pres_typeD2: |
326 |
"pres_type step n A \<Longrightarrow> s \<in> A \<Longrightarrow> p < n \<Longrightarrow> snd`set (step p s) \<subseteq> A" |
|
327 |
by auto (drule pres_typeD) |
|
13062 | 328 |
|
13078 | 329 |
|
330 |
lemma (in lbv) wti_pres [intro?]: |
|
331 |
assumes pres: "pres_type step n A" |
|
332 |
assumes cert: "c!(pc+1) \<in> A" |
|
333 |
assumes s_pc: "s \<in> A" "pc < n" |
|
334 |
shows "wti c pc s \<in> A" |
|
13062 | 335 |
proof - |
13078 | 336 |
from pres s_pc have "snd`set (step pc s) \<subseteq> A" by (rule pres_typeD2) |
337 |
with cert show ?thesis by (simp add: wti merge_pres) |
|
13062 | 338 |
qed |
339 |
||
340 |
||
13078 | 341 |
lemma (in lbv) wtc_pres: |
342 |
assumes "pres_type step n A" |
|
343 |
assumes "c!pc \<in> A" and "c!(pc+1) \<in> A" |
|
344 |
assumes "s \<in> A" and "pc < n" |
|
345 |
shows "wtc c pc s \<in> A" |
|
13062 | 346 |
proof - |
13078 | 347 |
have "wti c pc s \<in> A" .. |
348 |
moreover have "wti c pc (c!pc) \<in> A" .. |
|
349 |
ultimately show ?thesis using T_A by (simp add: wtc) |
|
13062 | 350 |
qed |
351 |
||
13078 | 352 |
|
353 |
lemma (in lbv) wtl_pres: |
|
354 |
assumes pres: "pres_type step (length is) A" |
|
355 |
assumes cert: "cert_ok c (length is) \<top> \<bottom> A" |
|
356 |
assumes s: "s \<in> A" |
|
357 |
assumes all: "wtl is c 0 s \<noteq> \<top>" |
|
358 |
shows "pc < length is \<Longrightarrow> wtl (take pc is) c 0 s \<in> A" |
|
359 |
(is "?len pc \<Longrightarrow> ?wtl pc \<in> A") |
|
13062 | 360 |
proof (induct pc) |
13078 | 361 |
from s show "?wtl 0 \<in> A" by simp |
13062 | 362 |
next |
13078 | 363 |
fix n assume "Suc n < length is" |
364 |
then obtain n: "n < length is" by simp |
|
365 |
assume "n < length is \<Longrightarrow> ?wtl n \<in> A" |
|
366 |
hence "?wtl n \<in> A" . |
|
367 |
moreover |
|
368 |
from cert have "c!n \<in> A" by (rule cert_okD1) |
|
13062 | 369 |
moreover |
370 |
have n1: "n+1 < length is" by simp |
|
13078 | 371 |
with cert have "c!(n+1) \<in> A" by (rule cert_okD1) |
13062 | 372 |
ultimately |
13078 | 373 |
have "wtc c n (?wtl n) \<in> A" by - (rule wtc_pres) |
374 |
also |
|
375 |
from all n have "?wtl n \<noteq> \<top>" by - (rule wtl_take) |
|
376 |
with n1 have "wtc c n (?wtl n) = ?wtl (n+1)" by (rule wtl_Suc [symmetric]) |
|
377 |
finally show "?wtl (Suc n) \<in> A" by simp |
|
13062 | 378 |
qed |
379 |
||
10042 | 380 |
|
9183 | 381 |
end |