author | nipkow |
Tue, 02 Apr 2002 13:47:01 +0200 | |
changeset 13074 | 96bf406fd3e5 |
parent 13071 | f538a1dba7ee |
child 13078 | 1dd711c6b93c |
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 |
||
11 |
||
12 |
syntax |
|
13 |
"@lesuberropt" :: "'a option err \<Rightarrow> 'a ord \<Rightarrow> 'a option err \<Rightarrow> 'a option err ord" |
|
14 |
("_ \<le>|_ _" [50,50,51] 50) |
|
8245 | 15 |
|
13062 | 16 |
"@superropt" :: "'a option err \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop" |
17 |
("_ +|_ _" [50,50,51] 50) |
|
18 |
||
19 |
"@supsuperropt" :: "'a option err list \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop" |
|
20 |
("_ ++|_ _" [50,50,51] 50) |
|
21 |
||
22 |
translations |
|
23 |
"a \<le>|r b" == "a <=_(Err.le (Opt.le r)) b" |
|
24 |
"a +|f b" == "a +_(Err.lift2 (Opt.sup f)) b" |
|
25 |
"a ++|f b" == "a ++_(Err.lift2 (Opt.sup f)) b" |
|
26 |
||
8245 | 27 |
|
28 |
types |
|
13062 | 29 |
's certificate = "'s option list" |
30 |
's steptype = "'s option err step_type" |
|
8245 | 31 |
|
12516 | 32 |
consts |
13062 | 33 |
merge :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> nat \<Rightarrow> |
34 |
(nat \<times> 's option err) list \<Rightarrow> 's option err \<Rightarrow> 's option err" |
|
12516 | 35 |
primrec |
13062 | 36 |
"merge cert f r pc [] x = x" |
37 |
"merge cert f r pc (s#ss) x = (let (pc',s') = s in |
|
38 |
merge cert f r pc ss (if pc'=pc+1 then (s' +|f x) |
|
39 |
else if s' \<le>|r (OK (cert!pc')) then x |
|
40 |
else Err))" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
41 |
|
13062 | 42 |
constdefs |
43 |
wtl_inst :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> |
|
44 |
's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err" |
|
45 |
"wtl_inst cert f r step pc s \<equiv> merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1)))" |
|
8245 | 46 |
|
13062 | 47 |
wtl_cert :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> |
48 |
's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err" |
|
49 |
"wtl_cert cert f r step pc s \<equiv> |
|
50 |
case cert!pc of |
|
51 |
None \<Rightarrow> wtl_inst cert f r step pc s |
|
52 |
| Some s' \<Rightarrow> if OK s \<le>|r (OK (Some s')) then wtl_inst cert f r step pc (Some s') else Err" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
53 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
54 |
consts |
13062 | 55 |
wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> |
56 |
's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err" |
|
8245 | 57 |
primrec |
13062 | 58 |
"wtl_inst_list [] cert f r step pc s = OK s" |
59 |
"wtl_inst_list (i#ins) cert f r step pc s = |
|
60 |
(let s' = wtl_cert cert f r step pc s in |
|
61 |
strict (wtl_inst_list ins cert f r step (pc+1)) s')" |
|
62 |
||
63 |
||
8245 | 64 |
|
65 |
constdefs |
|
13062 | 66 |
cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" |
13071 | 67 |
"cert_ok cert n A \<equiv> (\<forall>i < n. cert!i \<in> opt A) \<and> (cert!n = None)" |
13062 | 68 |
|
13071 | 69 |
lemma cert_okD1: |
13062 | 70 |
"cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!pc \<in> opt A" |
71 |
by (unfold cert_ok_def) fast |
|
72 |
||
13071 | 73 |
lemma cert_okD2: |
74 |
"cert_ok cert n A \<Longrightarrow> cert!n = None" |
|
75 |
by (simp add: cert_ok_def) |
|
76 |
||
77 |
lemma cert_okD3: |
|
78 |
"cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!Suc pc \<in> opt A" |
|
79 |
by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2) |
|
80 |
||
13062 | 81 |
|
82 |
declare Let_def [simp] |
|
83 |
||
84 |
section "more semilattice lemmas" |
|
85 |
||
86 |
(* |
|
87 |
lemma sup_top [simp]: |
|
88 |
assumes sl: "semilat (A,r,f)" |
|
89 |
assumes set: "x \<in> A" "t \<in> A" |
|
90 |
assumes top: "top r t" |
|
91 |
shows "x +_f t = t" |
|
92 |
proof - |
|
93 |
from sl have "order r" .. |
|
94 |
moreover from top have "x +_f t <=_r t" .. |
|
95 |
moreover from sl set have "t <=_r x +_f t" by simp |
|
96 |
ultimately show ?thesis by (rule order_antisym) |
|
97 |
qed |
|
98 |
||
99 |
lemma plusplussup_top: |
|
100 |
"semilat (A,r,f) \<Longrightarrow> top r Err \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> Err \<in> A \<Longrightarrow> xs ++_f Err = Err" |
|
101 |
by (induct xs) auto |
|
102 |
*) |
|
103 |
||
104 |
lemma err_semilatDorderI [simp, intro]: |
|
105 |
"err_semilat (A,r,f) \<Longrightarrow> order r" |
|
106 |
apply (simp add: Err.sl_def) |
|
107 |
apply (rule order_le_err [THEN iffD1]) |
|
13074 | 108 |
apply (rule semilat.orderI) |
13062 | 109 |
apply assumption |
110 |
done |
|
111 |
||
112 |
lemma err_opt_semilat [simp,elim]: |
|
113 |
"err_semilat (A,r,f) \<Longrightarrow> semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))" |
|
114 |
proof - |
|
115 |
assume "err_semilat (A,r,f)" |
|
116 |
hence "err_semilat (Opt.esl (A,r,f))" .. |
|
117 |
thus ?thesis by (simp add: Err.sl_def Opt.esl_def) |
|
118 |
qed |
|
119 |
||
120 |
lemma plusplus_erropt_Err [simp]: |
|
121 |
"xs ++|f Err = Err" |
|
122 |
by (induct xs) auto |
|
123 |
||
124 |
||
125 |
section "merge" |
|
126 |
||
127 |
lemma merge_Err [simp]: |
|
128 |
"merge cert f r pc ss Err = Err" |
|
129 |
by (induct ss) auto |
|
8245 | 130 |
|
13062 | 131 |
lemma merge_ok: |
132 |
"\<And>x. merge cert f r pc ss x = OK s \<Longrightarrow> |
|
133 |
\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))" |
|
134 |
(is "\<And>x. ?merge ss x \<Longrightarrow> ?P ss") |
|
135 |
proof (induct ss) |
|
136 |
show "?P []" by simp |
|
137 |
next |
|
138 |
fix x l ls assume merge: "?merge (l#ls) x" |
|
139 |
moreover |
|
140 |
obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) |
|
141 |
ultimately |
|
142 |
obtain x' where "?merge ls x'" by simp |
|
143 |
assume "\<And>x. ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" . |
|
144 |
moreover |
|
145 |
from merge |
|
146 |
have "pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by (simp split: split_if_asm) |
|
147 |
ultimately |
|
148 |
show "?P (l#ls)" by simp |
|
149 |
qed |
|
150 |
||
9012 | 151 |
|
13062 | 152 |
lemma merge_def: |
153 |
assumes semi: "err_semilat (A,r,f)" |
|
154 |
shows |
|
155 |
"\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc', s') \<in> set ss. s' \<in> err (opt A) \<Longrightarrow> |
|
156 |
merge cert f r pc ss x = |
|
157 |
(if \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))) then |
|
158 |
map snd [(p',t') \<in> ss. p'=pc+1] ++|f x |
|
159 |
else Err)" |
|
160 |
(is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x") |
|
161 |
proof (induct ss) |
|
162 |
fix x show "?P [] x" by simp |
|
163 |
next |
|
164 |
fix x assume x: "x \<in> err (opt A)" |
|
165 |
fix l::"nat \<times> 'a option err" and ls |
|
166 |
assume "\<forall>(pc', s') \<in> set (l#ls). s' \<in> err (opt A)" |
|
167 |
then obtain l: "snd l \<in> err (opt A)" and ls: "\<forall>(pc', s') \<in> set ls. s' \<in> err (opt A)" by auto |
|
168 |
assume "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc',s') \<in> set ls. s' \<in> err (opt A) \<Longrightarrow> ?P ls x" |
|
169 |
hence IH: "\<And>x. x \<in> err (opt A) \<Longrightarrow> ?P ls x" . |
|
170 |
obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) |
|
171 |
hence "?merge (l#ls) x = ?merge ls |
|
172 |
(if pc'=pc+1 then s' +|f x else if s' \<le>|r (OK (cert!pc')) then x else Err)" |
|
173 |
(is "?merge (l#ls) x = ?merge ls ?if'") |
|
174 |
by simp |
|
175 |
also have "\<dots> = ?if ls ?if'" |
|
176 |
proof - |
|
177 |
from l have "s' \<in> err (opt A)" by simp |
|
13074 | 178 |
with x semi have "(s' +|f x) \<in> err (opt A)" |
179 |
by (fast intro: semilat.closedI closedD) |
|
13062 | 180 |
with x have "?if' \<in> err (opt A)" by auto |
181 |
hence "?P ls ?if'" by (rule IH) thus ?thesis by simp |
|
182 |
qed |
|
183 |
also have "\<dots> = ?if (l#ls) x" |
|
184 |
proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r OK (cert ! pc')") |
|
185 |
case True |
|
186 |
hence "\<forall>(pc', s')\<in>set ls. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert ! pc'))" by auto |
|
187 |
moreover |
|
188 |
from True have |
|
189 |
"map snd [(p',t')\<in>ls . p'=pc+1] ++|f ?if' = |
|
190 |
(map snd [(p',t')\<in>l#ls . p'=pc+1] ++|f x)" |
|
191 |
by simp |
|
192 |
ultimately |
|
193 |
show ?thesis using True by simp |
|
194 |
next |
|
195 |
case False thus ?thesis by auto |
|
196 |
qed |
|
197 |
finally show "?P (l#ls) x" . |
|
198 |
qed |
|
199 |
||
200 |
lemma merge_ok_s: |
|
201 |
assumes sl: "err_semilat (A,r,f)" |
|
202 |
assumes x: "x \<in> err (opt A)" |
|
203 |
assumes ss: "\<forall>(pc', s') \<in> set ss. s' \<in> err (opt A)" |
|
204 |
assumes m: "merge cert f r pc ss x = OK s" |
|
205 |
shows "merge cert f r pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++|f x)" |
|
206 |
proof - |
|
207 |
from m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))" |
|
208 |
by (rule merge_ok) |
|
209 |
with sl x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm) |
|
210 |
qed |
|
211 |
||
212 |
section "wtl-inst-list" |
|
10042 | 213 |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
214 |
lemmas [iff] = not_Err_eq |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
215 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
216 |
lemma wtl_Cons: |
13062 | 217 |
"wtl_inst_list (i#is) cert f r step pc s \<noteq> Err = |
218 |
(\<exists>s'. wtl_cert cert f r step pc s = OK s' \<and> |
|
219 |
wtl_inst_list is cert f r step (pc+1) s' \<noteq> Err)" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10638
diff
changeset
|
220 |
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
|
221 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
222 |
lemma wtl_append: |
13062 | 223 |
"\<forall>s pc. (wtl_inst_list (a@b) cert f r step pc s = OK s') = |
224 |
(\<exists>s''. wtl_inst_list a cert f r step pc s = OK s'' \<and> |
|
225 |
wtl_inst_list b cert f r step (pc+length a) s'' = OK s')" |
|
226 |
(is "\<forall>s pc. ?C s pc a" is "?P a") |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
227 |
proof (induct ?P a) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
228 |
show "?P []" by simp |
12516 | 229 |
next |
230 |
fix x xs assume IH: "?P xs" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
231 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
232 |
proof (intro allI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
233 |
fix s pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
234 |
show "?C s pc (x#xs)" |
13062 | 235 |
proof (cases "wtl_cert cert f r step pc s") |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
236 |
case Err thus ?thesis by simp |
9183 | 237 |
next |
13062 | 238 |
case (OK s0) |
239 |
with IH have "?C s0 (pc+1) xs" by blast |
|
12516 | 240 |
thus ?thesis by (simp!) |
9183 | 241 |
qed |
242 |
qed |
|
243 |
qed |
|
9012 | 244 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
245 |
lemma wtl_take: |
13062 | 246 |
"wtl_inst_list is cert f r step pc s = OK s'' \<Longrightarrow> |
247 |
\<exists>s'. wtl_inst_list (take pc' is) cert f r step pc s = OK s'" |
|
248 |
(is "?wtl is = _ \<Longrightarrow> _") |
|
9183 | 249 |
proof - |
13062 | 250 |
assume "?wtl is = OK s''" |
251 |
hence "?wtl (take pc' is @ drop pc' is) = OK s''" by simp |
|
12516 | 252 |
thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
253 |
qed |
9012 | 254 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
255 |
lemma take_Suc: |
13062 | 256 |
"\<forall>n. n < length l --> 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
|
257 |
proof (induct l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
258 |
show "?P []" by simp |
12516 | 259 |
next |
260 |
fix x xs assume IH: "?P xs" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
261 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
262 |
proof (intro strip) |
12516 | 263 |
fix n assume "n < length (x#xs)" |
264 |
with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" |
|
265 |
by (cases n, auto) |
|
9183 | 266 |
qed |
267 |
qed |
|
9012 | 268 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
269 |
lemma wtl_Suc: |
13062 | 270 |
assumes "wtl_inst_list (take pc is) cert f r step 0 s = OK s'" |
271 |
"wtl_cert cert f r step pc s' = OK s''" and |
|
272 |
suc: "pc+1 < length is" |
|
273 |
shows "wtl_inst_list (take (pc+1) is) cert f r step 0 s = OK s''" |
|
9183 | 274 |
proof - |
13062 | 275 |
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc) |
12516 | 276 |
thus ?thesis by (simp! add: wtl_append min_def) |
9183 | 277 |
qed |
9012 | 278 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
279 |
lemma wtl_all: |
13062 | 280 |
assumes |
281 |
all: "wtl_inst_list is cert f r step 0 s \<noteq> Err" (is "?wtl is \<noteq> _") and |
|
282 |
pc: "pc < length is" |
|
283 |
shows |
|
284 |
"\<exists>s' s''. wtl_inst_list (take pc is) cert f r step 0 s = OK s' \<and> |
|
285 |
wtl_cert cert f r step pc s' = OK s''" |
|
9183 | 286 |
proof - |
13062 | 287 |
from pc have "0 < length (drop pc is)" by simp |
12516 | 288 |
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
|
289 |
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
|
290 |
hence "i#r = drop pc is" .. |
13062 | 291 |
with all have take: "?wtl (take pc is@i#r) \<noteq> Err" by simp |
12516 | 292 |
from pc have "is!pc = drop pc is ! 0" by simp |
293 |
with Cons have "is!pc = i" by simp |
|
294 |
with take pc show ?thesis by (auto simp add: wtl_append min_def) |
|
9183 | 295 |
qed |
9012 | 296 |
|
13062 | 297 |
section "preserves-type" |
298 |
||
299 |
lemma merge_pres: |
|
300 |
assumes semi: "err_semilat (A,r,f)" |
|
301 |
assumes s0_A: "\<forall>(pc', s')\<in>set ss. s' \<in> err (opt A)" |
|
302 |
assumes x_A: "x \<in> err (opt A)" |
|
303 |
assumes merge:"merge cert f r pc ss x = OK s'" |
|
304 |
shows "s' \<in> opt A" |
|
305 |
proof - |
|
306 |
from s0_A |
|
307 |
have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> err (opt A)" by auto |
|
308 |
with semi x_A |
|
309 |
have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) \<in> err (opt A)" |
|
310 |
by (auto intro!: plusplus_closed) |
|
311 |
also { |
|
312 |
note merge |
|
313 |
also from semi x_A s0_A |
|
314 |
have "merge cert f r pc ss x = |
|
315 |
(if \<forall>(pc', s')\<in>set ss. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc')) |
|
316 |
then map snd [(p', t')\<in>ss . p'=pc+1] ++|f x else Err)" |
|
317 |
by (rule merge_def) |
|
318 |
finally have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) = OK s'" |
|
319 |
by (simp split: split_if_asm) |
|
320 |
} |
|
321 |
finally show ?thesis by simp |
|
322 |
qed |
|
323 |
||
324 |
||
325 |
||
326 |
lemma wtl_inst_pres [intro?]: |
|
327 |
assumes semi: "err_semilat (A,r,f)" |
|
328 |
assumes pres: "pres_type step n (err (opt A))" |
|
329 |
assumes cert: "cert!(pc+1) \<in> opt A" |
|
330 |
assumes s_A: "s \<in> opt A" |
|
331 |
assumes pc: "pc < n" |
|
332 |
assumes wtl: "wtl_inst cert f r step pc s = OK s'" |
|
333 |
shows "s' \<in> opt A" |
|
334 |
proof - |
|
335 |
from pres pc s_A |
|
336 |
have "\<forall>(q, s')\<in>set (step pc (OK s)). s' \<in> err (opt A)" |
|
337 |
by (unfold pres_type_def) blast |
|
338 |
moreover |
|
339 |
from cert have "OK (cert!(pc+1)) \<in> err (opt A)" by simp |
|
340 |
moreover |
|
341 |
from wtl |
|
342 |
have "merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1))) = OK s'" |
|
343 |
by (unfold wtl_inst_def) simp |
|
344 |
ultimately |
|
345 |
show "s' \<in> opt A" using semi by - (rule merge_pres) |
|
346 |
qed |
|
347 |
||
348 |
||
349 |
lemma wtl_cert_pres: |
|
350 |
assumes "err_semilat (A,r,f)" |
|
351 |
assumes "pres_type step n (err (opt A))" |
|
352 |
assumes "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A" |
|
353 |
assumes "s \<in> opt A" and "pc < n" |
|
354 |
assumes wtc: "wtl_cert cert f r step pc s = OK s'" |
|
355 |
shows "s' \<in> opt A" |
|
356 |
proof - |
|
357 |
have "wtl_inst cert f r step pc s = OK s' \<Longrightarrow> s' \<in> opt A" .. |
|
358 |
moreover |
|
359 |
have "wtl_inst cert f r step pc (cert!pc) = OK s' \<Longrightarrow> s' \<in> opt A" .. |
|
360 |
ultimately |
|
361 |
show ?thesis using wtc |
|
362 |
by (unfold wtl_cert_def) (simp split: option.splits split_if_asm) |
|
363 |
qed |
|
364 |
||
365 |
lemma wtl_inst_list_pres: |
|
366 |
assumes semi: "err_semilat (A,r,f)" |
|
367 |
assumes pres: "pres_type step (length is) (err (opt A))" |
|
368 |
assumes cert: "cert_ok cert (length is) A" |
|
369 |
assumes s: "s \<in> opt A" |
|
370 |
assumes all: "wtl_inst_list is cert f r step 0 s \<noteq> Err" |
|
371 |
shows "\<And>s'. pc < length is \<Longrightarrow> wtl_inst_list (take pc is) cert f r step 0 s = OK s' |
|
372 |
\<Longrightarrow> s' \<in> opt A" (is "\<And>s'. ?len pc \<Longrightarrow> ?wtl pc s' \<Longrightarrow> ?A s'") |
|
373 |
proof (induct pc) |
|
374 |
from s show "\<And>s'. ?wtl 0 s' \<Longrightarrow> ?A s'" by simp |
|
375 |
next |
|
376 |
fix s' n |
|
377 |
assume "Suc n < length is" |
|
378 |
then obtain "n < length is" by simp |
|
379 |
with all obtain s1 s2 where |
|
380 |
"wtl_inst_list (take n is) cert f r step 0 s = OK s1" |
|
381 |
"wtl_cert cert f r step n s1 = OK s2" |
|
382 |
by - (drule wtl_all, auto) |
|
383 |
||
384 |
assume "?wtl (Suc n) s'" |
|
385 |
moreover |
|
386 |
have n1: "n+1 < length is" by simp |
|
387 |
hence "?wtl (n+1) s2" by - (rule wtl_Suc) |
|
388 |
ultimately |
|
389 |
have [simp]: "s2 = s'" by simp |
|
390 |
||
391 |
assume IH: "\<And>s'. n < length is \<Longrightarrow> ?wtl n s' \<Longrightarrow> s' \<in> opt A" |
|
392 |
hence "s1 \<in> opt A" . |
|
393 |
moreover |
|
13071 | 394 |
from cert have "cert!n \<in> opt A" by (rule cert_okD1) |
13062 | 395 |
moreover |
13071 | 396 |
from cert n1 have "cert!(n+1) \<in> opt A" by (rule cert_okD1) |
13062 | 397 |
ultimately |
398 |
have "s2 \<in> opt A" using semi pres by - (rule wtl_cert_pres) |
|
399 |
thus "s' \<in> opt A" by simp |
|
400 |
qed |
|
401 |
||
10042 | 402 |
|
9183 | 403 |
end |