8245
|
1 |
(* Title: HOL/MicroJava/BV/BVLightSpec.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
9054
|
5 |
*)
|
8245
|
6 |
|
9054
|
7 |
header {* Specification of the LBV *}
|
|
8 |
|
8245
|
9 |
|
9183
|
10 |
theory LBVSpec = BVSpec:
|
8245
|
11 |
|
|
12 |
types
|
|
13 |
certificate = "state_type option list"
|
|
14 |
class_certificate = "sig \\<Rightarrow> certificate"
|
9183
|
15 |
prog_certificate = "cname \\<Rightarrow> class_certificate"
|
8245
|
16 |
|
9376
|
17 |
|
8245
|
18 |
consts
|
9376
|
19 |
wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
20 |
|
8245
|
21 |
primrec
|
9376
|
22 |
"wtl_inst (Load idx) G rT s s' cert max_pc pc =
|
8245
|
23 |
(let (ST,LT) = s
|
|
24 |
in
|
|
25 |
pc+1 < max_pc \\<and>
|
|
26 |
idx < length LT \\<and>
|
|
27 |
(\\<exists>ts. (LT ! idx) = Some ts \\<and>
|
|
28 |
(ts # ST , LT) = s'))"
|
|
29 |
|
9376
|
30 |
"wtl_inst (Store idx) G rT s s' cert max_pc pc =
|
8245
|
31 |
(let (ST,LT) = s
|
|
32 |
in
|
|
33 |
pc+1 < max_pc \\<and>
|
|
34 |
idx < length LT \\<and>
|
|
35 |
(\\<exists>ts ST'. ST = ts # ST' \\<and>
|
|
36 |
(ST' , LT[idx:=Some ts]) = s'))"
|
|
37 |
|
9376
|
38 |
"wtl_inst (Bipush i) G rT s s' cert max_pc pc =
|
8245
|
39 |
(let (ST,LT) = s
|
|
40 |
in
|
|
41 |
pc+1 < max_pc \\<and>
|
|
42 |
((PrimT Integer) # ST , LT) = s')"
|
|
43 |
|
9376
|
44 |
"wtl_inst (Aconst_null) G rT s s' cert max_pc pc =
|
8245
|
45 |
(let (ST,LT) = s
|
|
46 |
in
|
|
47 |
pc+1 < max_pc \\<and>
|
9183
|
48 |
(NT # ST , LT) = s')"
|
8245
|
49 |
|
9376
|
50 |
"wtl_inst (Getfield F C) G rT s s' cert max_pc pc =
|
8245
|
51 |
(let (ST,LT) = s
|
|
52 |
in
|
|
53 |
pc+1 < max_pc \\<and>
|
|
54 |
is_class G C \\<and>
|
|
55 |
(\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
|
8390
|
56 |
ST = oT # ST' \\<and>
|
|
57 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
|
|
58 |
(T # ST' , LT) = s'))"
|
8245
|
59 |
|
9376
|
60 |
"wtl_inst (Putfield F C) G rT s s' cert max_pc pc =
|
8245
|
61 |
(let (ST,LT) = s
|
|
62 |
in
|
|
63 |
pc+1 < max_pc \\<and>
|
|
64 |
is_class G C \\<and>
|
|
65 |
(\\<exists>T vT oT ST'.
|
|
66 |
field (G,C) F = Some(C,T) \\<and>
|
|
67 |
ST = vT # oT # ST' \\<and>
|
|
68 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
|
8390
|
69 |
G \\<turnstile> vT \\<preceq> T \\<and>
|
9183
|
70 |
(ST' , LT) = s'))"
|
8245
|
71 |
|
9376
|
72 |
"wtl_inst (New C) G rT s s' cert max_pc pc =
|
8245
|
73 |
(let (ST,LT) = s
|
|
74 |
in
|
|
75 |
pc+1 < max_pc \\<and>
|
|
76 |
is_class G C \\<and>
|
9183
|
77 |
((Class C) # ST , LT) = s')"
|
8245
|
78 |
|
9376
|
79 |
"wtl_inst (Checkcast C) G rT s s' cert max_pc pc =
|
9054
|
80 |
(let (ST,LT) = s
|
8245
|
81 |
in
|
|
82 |
pc+1 < max_pc \\<and>
|
|
83 |
is_class G C \\<and>
|
|
84 |
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
|
9183
|
85 |
(Class C # ST' , LT) = s'))"
|
8245
|
86 |
|
9376
|
87 |
"wtl_inst Pop G rT s s' cert max_pc pc =
|
8245
|
88 |
(let (ST,LT) = s
|
|
89 |
in
|
|
90 |
\\<exists>ts ST'. pc+1 < max_pc \\<and>
|
|
91 |
ST = ts # ST' \\<and>
|
|
92 |
(ST' , LT) = s')"
|
|
93 |
|
9376
|
94 |
"wtl_inst Dup G rT s s' cert max_pc pc =
|
8245
|
95 |
(let (ST,LT) = s
|
|
96 |
in
|
|
97 |
pc+1 < max_pc \\<and>
|
|
98 |
(\\<exists>ts ST'. ST = ts # ST' \\<and>
|
|
99 |
(ts # ts # ST' , LT) = s'))"
|
|
100 |
|
9376
|
101 |
"wtl_inst Dup_x1 G rT s s' cert max_pc pc =
|
8245
|
102 |
(let (ST,LT) = s
|
|
103 |
in
|
|
104 |
pc+1 < max_pc \\<and>
|
|
105 |
(\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
|
|
106 |
(ts1 # ts2 # ts1 # ST' , LT) = s'))"
|
|
107 |
|
9376
|
108 |
"wtl_inst Dup_x2 G rT s s' cert max_pc pc =
|
8245
|
109 |
(let (ST,LT) = s
|
|
110 |
in
|
|
111 |
pc+1 < max_pc \\<and>
|
|
112 |
(\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
|
|
113 |
(ts1 # ts2 # ts3 # ts1 # ST' , LT) = s'))"
|
|
114 |
|
9376
|
115 |
"wtl_inst Swap G rT s s' cert max_pc pc =
|
8245
|
116 |
(let (ST,LT) = s
|
|
117 |
in
|
|
118 |
pc+1 < max_pc \\<and>
|
|
119 |
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
|
9183
|
120 |
(ts # ts' # ST' , LT) = s'))"
|
8245
|
121 |
|
9376
|
122 |
"wtl_inst IAdd G rT s s' cert max_pc pc =
|
9260
|
123 |
(let (ST,LT) = s
|
|
124 |
in
|
|
125 |
pc+1 < max_pc \\<and>
|
|
126 |
(\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
|
|
127 |
((PrimT Integer) # ST' , LT) = s'))"
|
9376
|
128 |
|
|
129 |
|
|
130 |
"wtl_inst (Ifcmpeq branch) G rT s s' cert max_pc pc =
|
8245
|
131 |
(let (ST,LT) = s
|
|
132 |
in
|
|
133 |
pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
|
8390
|
134 |
(\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>
|
|
135 |
((\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or>
|
|
136 |
(\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and>
|
8245
|
137 |
((ST' , LT) = s') \\<and>
|
|
138 |
cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
|
9376
|
139 |
G \\<turnstile> (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))"
|
8245
|
140 |
|
9376
|
141 |
"wtl_inst (Goto branch) G rT s s' cert max_pc pc =
|
8245
|
142 |
((let (ST,LT) = s
|
|
143 |
in
|
|
144 |
(nat(int pc+branch)) < max_pc \\<and> cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
|
|
145 |
G \\<turnstile> (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\<and>
|
9183
|
146 |
(cert ! (pc+1) = Some s'))"
|
9376
|
147 |
|
|
148 |
"wtl_inst (Invoke mn fpTs) G rT s s' cert max_pc pc =
|
8245
|
149 |
(let (ST,LT) = s
|
|
150 |
in
|
|
151 |
pc+1 < max_pc \\<and>
|
8390
|
152 |
(\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and>
|
8245
|
153 |
length apTs = length fpTs \\<and>
|
8390
|
154 |
(\\<exists>s''. cert ! (pc+1) = Some s'' \\<and>
|
|
155 |
((s'' = s' \\<and> X = NT) \\<or>
|
|
156 |
((G \\<turnstile> s' <=s s'') \\<and> (\\<exists>C. X = Class C \\<and>
|
|
157 |
(\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
|
|
158 |
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
|
9183
|
159 |
(rT # ST' , LT) = s')))))))"
|
8245
|
160 |
|
9376
|
161 |
"wtl_inst Return G rT s s' cert max_pc pc =
|
8245
|
162 |
((let (ST,LT) = s
|
|
163 |
in
|
|
164 |
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
|
9183
|
165 |
(cert ! (pc+1) = Some s'))"
|
8245
|
166 |
|
|
167 |
|
|
168 |
constdefs
|
|
169 |
wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
170 |
"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
|
|
171 |
(case cert!pc of
|
|
172 |
None \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
|
|
173 |
| Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
|
9183
|
174 |
wtl_inst i G rT s0' s1 cert max_pc pc)"
|
8245
|
175 |
|
|
176 |
consts
|
9183
|
177 |
wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
8245
|
178 |
primrec
|
|
179 |
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
|
|
180 |
|
|
181 |
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
|
|
182 |
(\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and>
|
9183
|
183 |
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"
|
8245
|
184 |
|
|
185 |
constdefs
|
|
186 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool"
|
|
187 |
"wtl_method G C pTs rT mxl ins cert \\<equiv>
|
|
188 |
let max_pc = length ins
|
|
189 |
in
|
|
190 |
0 < max_pc \\<and>
|
|
191 |
(\\<exists>s2. wtl_inst_list ins G rT
|
|
192 |
([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
|
|
193 |
s2 cert max_pc 0)"
|
|
194 |
|
9012
|
195 |
wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
|
8245
|
196 |
"wtl_jvm_prog G cert \\<equiv>
|
|
197 |
wf_prog (\\<lambda>G C (sig,rT,maxl,b).
|
9183
|
198 |
wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
|
9012
|
199 |
|
9054
|
200 |
text {* \medskip *}
|
|
201 |
|
9183
|
202 |
lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z"
|
|
203 |
by auto
|
9012
|
204 |
|
|
205 |
lemma wtl_inst_unique:
|
|
206 |
"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
|
9183
|
207 |
wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
|
|
208 |
proof (induct i)
|
9376
|
209 |
case Invoke
|
9183
|
210 |
have "\\<exists>x y. s0 = (x,y)" by (simp)
|
9376
|
211 |
thus "wtl_inst (Invoke mname list) G rT s0 s1 cert max_pc pc \\<longrightarrow>
|
|
212 |
wtl_inst (Invoke mname list) G rT s0 s1' cert max_pc pc \\<longrightarrow>
|
9183
|
213 |
s1 = s1'"
|
|
214 |
proof elim
|
|
215 |
apply_end(clarsimp_tac, drule rev_eq, assumption+)
|
|
216 |
qed auto
|
9376
|
217 |
qed auto
|
|
218 |
|
9012
|
219 |
|
|
220 |
lemma wtl_inst_option_unique:
|
|
221 |
"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
|
9183
|
222 |
wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'"
|
|
223 |
by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
|
9012
|
224 |
|
|
225 |
|
|
226 |
lemma wtl_inst_list_unique:
|
|
227 |
"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow>
|
9183
|
228 |
wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
|
|
229 |
proof (induct "?P" "is")
|
|
230 |
case Nil
|
|
231 |
show "?P []" by simp
|
8245
|
232 |
|
9183
|
233 |
case Cons
|
|
234 |
show "?P (a # list)"
|
|
235 |
proof intro
|
|
236 |
fix s0 fix pc
|
|
237 |
let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc"
|
|
238 |
let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc"
|
|
239 |
assume a: "?l (a#list) s0 s1 pc"
|
|
240 |
assume b: "?l (a#list) s0 s1' pc"
|
|
241 |
with a
|
|
242 |
show "s1 = s1'"
|
9012
|
243 |
obtain s s' where "?o s0 s" "?o s0 s'"
|
|
244 |
and l: "?l list s s1 (Suc pc)"
|
9183
|
245 |
and l': "?l list s' s1' (Suc pc)" by auto
|
|
246 |
have "s=s'" by(rule wtl_inst_option_unique)
|
|
247 |
with l l' Cons
|
|
248 |
show ?thesis by blast
|
|
249 |
qed
|
|
250 |
qed
|
|
251 |
qed
|
9012
|
252 |
|
|
253 |
lemma wtl_partial:
|
|
254 |
"\\<forall> pc' pc s.
|
|
255 |
wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
|
|
256 |
pc' < length is \\<longrightarrow> \
|
|
257 |
(\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
|
|
258 |
wtl_inst_list a G rT s s1 cert mpc pc \\<and> \
|
9183
|
259 |
wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is")
|
|
260 |
proof (induct "?P" "is")
|
|
261 |
case Nil
|
|
262 |
show "?P []" by auto
|
9012
|
263 |
|
9183
|
264 |
case Cons
|
|
265 |
show "?P (a#list)"
|
|
266 |
proof (intro allI impI)
|
|
267 |
fix pc' pc s
|
|
268 |
assume length: "pc' < length (a # list)"
|
|
269 |
assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc"
|
9012
|
270 |
show "\\<exists> a' b s1.
|
|
271 |
a' @ b = a#list \\<and> length a' = pc' \\<and> \
|
|
272 |
wtl_inst_list a' G rT s s1 cert mpc pc \\<and> \
|
|
273 |
wtl_inst_list b G rT s1 s' cert mpc (pc+length a')"
|
9183
|
274 |
(is "\\<exists> a b s1. ?E a b s1")
|
|
275 |
proof (cases "pc'")
|
|
276 |
case 0
|
|
277 |
with wtl
|
|
278 |
have "?E [] (a#list) s" by simp
|
|
279 |
thus ?thesis by blast
|
|
280 |
next
|
|
281 |
case Suc
|
|
282 |
with wtl
|
|
283 |
show ?thesis
|
9012
|
284 |
obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"
|
9183
|
285 |
and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto
|
|
286 |
from Cons
|
|
287 |
show ?thesis
|
9012
|
288 |
obtain a' b s1'
|
|
289 |
where "a' @ b = list" "length a' = nat"
|
|
290 |
and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)"
|
9183
|
291 |
and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')"
|
|
292 |
proof (elim allE impE)
|
|
293 |
from length Suc show "nat < length list" by simp
|
|
294 |
from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" .
|
|
295 |
qed (elim exE conjE, auto)
|
|
296 |
with Suc wtlOpt
|
|
297 |
have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex)
|
|
298 |
thus ?thesis by blast
|
|
299 |
qed
|
|
300 |
qed
|
|
301 |
qed
|
|
302 |
qed
|
|
303 |
qed
|
9012
|
304 |
|
|
305 |
lemma "wtl_append1":
|
|
306 |
"\\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0;
|
|
307 |
wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\\<rbrakk> \\<Longrightarrow>
|
9183
|
308 |
wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0"
|
|
309 |
proof -
|
9012
|
310 |
assume w:
|
|
311 |
"wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0"
|
9183
|
312 |
"wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)"
|
9012
|
313 |
|
|
314 |
have
|
|
315 |
"\\<forall> pc s0.
|
|
316 |
wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow>
|
|
317 |
wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
|
9183
|
318 |
wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
|
|
319 |
proof (induct "?P" "x")
|
|
320 |
case Nil
|
|
321 |
show "?P []" by simp
|
|
322 |
next
|
|
323 |
case Cons
|
|
324 |
show "?P (a#list)"
|
|
325 |
proof intro
|
|
326 |
fix pc s0
|
9012
|
327 |
assume y:
|
9183
|
328 |
"wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))"
|
9012
|
329 |
assume al:
|
9183
|
330 |
"wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc"
|
|
331 |
thus "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
|
9012
|
332 |
obtain s' where
|
|
333 |
a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and
|
9183
|
334 |
l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto
|
|
335 |
with y Cons
|
|
336 |
have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)"
|
|
337 |
by (elim allE impE) (assumption, simp+)
|
|
338 |
with a
|
|
339 |
show ?thesis by (auto simp del: split_paired_Ex)
|
|
340 |
qed
|
|
341 |
qed
|
|
342 |
qed
|
9012
|
343 |
|
9183
|
344 |
with w
|
|
345 |
show ?thesis
|
|
346 |
proof (elim allE impE)
|
|
347 |
from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp
|
|
348 |
qed simp+
|
|
349 |
qed
|
9012
|
350 |
|
|
351 |
lemma wtl_cons_appendl:
|
|
352 |
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
|
|
353 |
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
|
|
354 |
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow>
|
9183
|
355 |
wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0"
|
|
356 |
proof -
|
|
357 |
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
|
9012
|
358 |
|
|
359 |
assume "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
|
9183
|
360 |
"wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
|
9012
|
361 |
|
9183
|
362 |
hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)"
|
|
363 |
by (auto simp del: split_paired_Ex)
|
9012
|
364 |
|
9183
|
365 |
with a
|
|
366 |
show ?thesis by (rule wtl_append1)
|
|
367 |
qed
|
9012
|
368 |
|
|
369 |
lemma "wtl_append":
|
|
370 |
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
|
|
371 |
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
|
|
372 |
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow>
|
9183
|
373 |
wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"
|
|
374 |
proof -
|
|
375 |
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
|
|
376 |
assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
|
|
377 |
assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
|
9012
|
378 |
|
|
379 |
have "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow>
|
|
380 |
wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow>
|
|
381 |
wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \\<longrightarrow>
|
9183
|
382 |
wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a")
|
|
383 |
proof (induct "?P" "a")
|
|
384 |
case Nil
|
|
385 |
show "?P []" by (simp del: split_paired_Ex)
|
|
386 |
case Cons
|
|
387 |
show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc")
|
|
388 |
proof intro
|
|
389 |
fix s0 pc
|
|
390 |
assume y: "?y s0 pc"
|
|
391 |
assume z: "?z s0 pc"
|
|
392 |
assume "?x s0 pc"
|
|
393 |
thus "?p s0 pc"
|
9012
|
394 |
obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc"
|
9183
|
395 |
and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"
|
|
396 |
by (auto simp del: split_paired_Ex)
|
|
397 |
with y z Cons
|
|
398 |
have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)"
|
|
399 |
proof (elim allE impE)
|
|
400 |
from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" .
|
|
401 |
qed auto
|
|
402 |
with opt
|
|
403 |
show ?thesis by (auto simp del: split_paired_Ex)
|
|
404 |
qed
|
|
405 |
qed
|
|
406 |
qed
|
|
407 |
with a i b
|
|
408 |
show ?thesis
|
|
409 |
proof (elim allE impE)
|
|
410 |
from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp
|
|
411 |
qed auto
|
|
412 |
qed
|
9012
|
413 |
|
9183
|
414 |
end
|