|
1 (* Title: HOL/MicroJava/Comp/CorrCompTp.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Strecker |
|
4 Copyright GPL 2002 |
|
5 *) |
|
6 |
|
7 theory CorrCompTp = LemmasComp + JVM + TypeInf + NatCanonify + Altern: |
|
8 |
|
9 |
|
10 declare split_paired_All [simp del] |
|
11 declare split_paired_Ex [simp del] |
|
12 |
|
13 |
|
14 (**********************************************************************) |
|
15 |
|
16 constdefs |
|
17 inited_LT :: "[cname, ty list, (vname \<times> ty) list] \<Rightarrow> locvars_type" |
|
18 "inited_LT C pTs lvars == (OK (Class C))#((map OK pTs))@(map (Fun.comp OK snd) lvars)" |
|
19 is_inited_LT :: "[cname, ty list, (vname \<times> ty) list, locvars_type] \<Rightarrow> bool" |
|
20 "is_inited_LT C pTs lvars LT == (LT = (inited_LT C pTs lvars))" |
|
21 |
|
22 local_env :: "[java_mb prog, cname, sig, vname list,(vname \<times> ty) list] \<Rightarrow> java_mb env" |
|
23 "local_env G C S pns lvars == |
|
24 let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))" |
|
25 |
|
26 lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G" |
|
27 by (simp add: local_env_def split_beta) |
|
28 |
|
29 |
|
30 lemma wt_class_expr_is_class: "\<lbrakk> wf_prog wf_mb G; E \<turnstile> expr :: Class cname; |
|
31 E = local_env G C (mn, pTs) pns lvars\<rbrakk> |
|
32 \<Longrightarrow> is_class G cname " |
|
33 apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname") |
|
34 apply (frule ty_expr_is_type) apply simp |
|
35 apply simp apply (simp (no_asm_use)) |
|
36 done |
|
37 |
|
38 |
|
39 |
|
40 (********************************************************************************) |
|
41 (**** Stuff about index ****) |
|
42 |
|
43 lemma local_env_snd: " |
|
44 snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)" |
|
45 by (simp add: local_env_def) |
|
46 |
|
47 |
|
48 |
|
49 lemma index_in_bounds: " length pns = length pTs \<Longrightarrow> |
|
50 snd (local_env G C (mn, pTs) pns lvars) vname = Some T |
|
51 \<Longrightarrow> index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)" |
|
52 apply (simp add: local_env_snd index_def split_beta) |
|
53 apply (case_tac "vname = This") |
|
54 apply (simp add: inited_LT_def) |
|
55 apply simp |
|
56 apply (drule map_of_upds_SomeD) |
|
57 apply (drule length_takeWhile) |
|
58 apply (simp add: inited_LT_def) |
|
59 done |
|
60 |
|
61 |
|
62 lemma map_upds_append [rule_format (no_asm)]: |
|
63 "\<forall> x1s m. (length k1s = length x1s |
|
64 \<longrightarrow> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s)))" |
|
65 apply (induct k1s) |
|
66 apply simp |
|
67 apply (intro strip) |
|
68 apply (subgoal_tac "\<exists> x xr. x1s = x # xr") |
|
69 apply clarify |
|
70 apply simp |
|
71 (* subgoal *) |
|
72 apply (case_tac x1s) |
|
73 apply auto |
|
74 done |
|
75 |
|
76 |
|
77 lemma map_of_append [rule_format]: |
|
78 "\<forall> ys. (map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [\<mapsto>] (map snd xs)))" |
|
79 apply (induct xs) |
|
80 apply simp |
|
81 apply (rule allI) |
|
82 apply (drule_tac x="a # ys" in spec) |
|
83 apply (simp only: rev.simps append_assoc append_Cons append_Nil |
|
84 map.simps map_of.simps map_upds.simps hd.simps tl.simps) |
|
85 done |
|
86 |
|
87 lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))" |
|
88 by (rule map_of_append [of _ "[]", simplified]) |
|
89 |
|
90 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs" |
|
91 apply (induct xs) |
|
92 apply simp |
|
93 apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]) |
|
94 done |
|
95 |
|
96 lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs |
|
97 \<longrightarrow> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))" |
|
98 apply (induct ks) |
|
99 apply simp |
|
100 apply (intro strip) |
|
101 apply (subgoal_tac "\<exists> x xr. xs = x # xr") |
|
102 apply clarify |
|
103 apply (drule_tac x=xr in spec) |
|
104 apply (simp add: map_upds_append [THEN sym]) |
|
105 (* subgoal *) |
|
106 apply (case_tac xs) |
|
107 apply auto |
|
108 done |
|
109 |
|
110 lemma map_upds_takeWhile [rule_format]: |
|
111 "\<forall> ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow> |
|
112 xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x" |
|
113 apply (induct xs) |
|
114 apply simp |
|
115 apply (intro strip) |
|
116 apply (subgoal_tac "\<exists> k' kr. ks = k' # kr") |
|
117 apply (clarify) |
|
118 apply (drule_tac x=kr in spec) |
|
119 apply (simp only: rev.simps) |
|
120 apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])") |
|
121 apply (simp only:) |
|
122 apply (case_tac "k' = k") |
|
123 apply simp |
|
124 apply simp |
|
125 apply (case_tac "k = k'") |
|
126 apply simp |
|
127 apply (simp add: empty_def) |
|
128 apply (simp add: map_upds_append [THEN sym]) |
|
129 apply (case_tac ks) |
|
130 apply auto |
|
131 done |
|
132 |
|
133 |
|
134 lemma local_env_inited_LT: "\<lbrakk> snd (local_env G C (mn, pTs) pns lvars) vname = Some T; |
|
135 length pns = length pTs; distinct pns; unique lvars \<rbrakk> |
|
136 \<Longrightarrow> (inited_LT C pTs lvars ! index (pns, lvars, blk, res) vname) = OK T" |
|
137 apply (simp add: local_env_snd index_def) |
|
138 apply (case_tac "vname = This") |
|
139 apply (simp add: inited_LT_def) |
|
140 apply (simp add: inited_LT_def) |
|
141 apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym]) |
|
142 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)") |
|
143 apply (simp (no_asm_simp) only: List.nth_map ok_val.simps) |
|
144 apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)") |
|
145 apply (simp only:) |
|
146 apply (subgoal_tac "distinct (map fst lvars)") |
|
147 apply (frule_tac g=snd in AuxLemmas.map_of_map_as_map_upd) |
|
148 apply (simp only:) |
|
149 apply (simp add: map_upds_append) |
|
150 apply (frule map_upds_SomeD) |
|
151 apply (rule map_upds_takeWhile) |
|
152 apply (simp (no_asm_simp)) |
|
153 apply (simp add: map_upds_append [THEN sym]) |
|
154 apply (simp add: map_upds_rev) |
|
155 |
|
156 (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *) |
|
157 apply simp |
|
158 |
|
159 (* show distinct (map fst lvars) *) |
|
160 apply (simp only: unique_def Fun.comp_def) |
|
161 |
|
162 (* show map_of lvars = map_of (map (\<lambda>p. (fst p, snd p)) lvars) *) |
|
163 apply simp |
|
164 |
|
165 (* show length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *) |
|
166 apply (drule map_of_upds_SomeD) |
|
167 apply (drule length_takeWhile) |
|
168 apply simp |
|
169 done |
|
170 |
|
171 |
|
172 lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars) |
|
173 \<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err" |
|
174 apply (simp only: inited_LT_def) |
|
175 apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map) |
|
176 apply (simp only: nth_map) |
|
177 apply simp |
|
178 done |
|
179 |
|
180 |
|
181 lemma sup_loc_update_index: " |
|
182 \<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars; |
|
183 snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \<rbrakk> |
|
184 \<Longrightarrow> |
|
185 comp G \<turnstile> |
|
186 inited_LT C pTs lvars [index (pns, lvars, blk, res) vname := OK T] <=l |
|
187 inited_LT C pTs lvars" |
|
188 apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)") |
|
189 apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+) |
|
190 apply (rule sup_loc_trans) |
|
191 apply (rule_tac b="OK T'" in sup_loc_update) |
|
192 apply (simp add: comp_widen) |
|
193 apply assumption |
|
194 apply (rule sup_loc_refl) |
|
195 apply (simp add: list_update_same_conv [THEN iffD2]) |
|
196 (* subgoal *) |
|
197 apply (rule index_in_bounds) |
|
198 apply simp+ |
|
199 done |
|
200 |
|
201 |
|
202 (********************************************************************************) |
|
203 |
|
204 (* Preservation of ST and LT by compTpExpr / compTpStmt *) |
|
205 |
|
206 lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp" |
|
207 by (simp add: comb_nil_def) |
|
208 |
|
209 lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []" |
|
210 by (simp add: comb_nil_def) |
|
211 |
|
212 |
|
213 lemma sttp_of_comb [simp]: "sttp_of ((f1 \<box> f2) sttp) = sttp_of (f2 (sttp_of (f1 sttp)))" |
|
214 apply (case_tac "f1 sttp") |
|
215 apply (case_tac "(f2 (sttp_of (f1 sttp)))") |
|
216 apply (simp add: comb_def) |
|
217 done |
|
218 |
|
219 lemma mt_of_comb: "(mt_of ((f1 \<box> f2) sttp)) = |
|
220 (mt_of (f1 sttp)) @ (mt_of (f2 (sttp_of (f1 sttp))))" |
|
221 by (simp add: comb_def split_beta) |
|
222 |
|
223 |
|
224 lemma mt_of_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk> |
|
225 \<Longrightarrow> (mt_of ((f1 \<box> f2) sttp) ! n) = (mt_of (f2 (sttp_of (f1 sttp))) ! (n - n1))" |
|
226 by (simp add: comb_def nth_append split_beta) |
|
227 |
|
228 |
|
229 lemma compTpExpr_Exprs_LT_ST: " |
|
230 \<lbrakk>jmb = (pns, lvars, blk, res); |
|
231 wf_prog wf_java_mdecl G; |
|
232 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
233 E = local_env G C (mn, pTs) pns lvars \<rbrakk> |
|
234 \<Longrightarrow> |
|
235 (\<forall> ST LT T. |
|
236 E \<turnstile> ex :: T \<longrightarrow> |
|
237 is_inited_LT C pTs lvars LT \<longrightarrow> |
|
238 sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT)) |
|
239 \<and> |
|
240 (\<forall> ST LT Ts. |
|
241 E \<turnstile> exs [::] Ts \<longrightarrow> |
|
242 is_inited_LT C pTs lvars LT \<longrightarrow> |
|
243 sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))" |
|
244 |
|
245 apply (rule expr.induct) |
|
246 |
|
247 (* expresssions *) |
|
248 |
|
249 (* NewC *) |
|
250 apply (intro strip) |
|
251 apply (drule NewC_invers) |
|
252 apply (simp add: pushST_def) |
|
253 |
|
254 (* Cast *) |
|
255 apply (intro strip) |
|
256 apply (drule Cast_invers, clarify) |
|
257 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+) |
|
258 apply (simp add: replST_def split_beta) |
|
259 |
|
260 (* Lit *) |
|
261 apply (intro strip) |
|
262 apply (drule Lit_invers) |
|
263 apply (simp add: pushST_def) |
|
264 |
|
265 (* BinOp *) |
|
266 apply (intro strip) |
|
267 apply (drule BinOp_invers, clarify) |
|
268 apply (drule_tac x=ST in spec) |
|
269 apply (drule_tac x="Ta # ST" in spec) |
|
270 apply ((drule spec)+, (drule mp, assumption)+) |
|
271 apply (case_tac binop) |
|
272 apply (simp (no_asm_simp)) |
|
273 apply (simp (no_asm_simp) add: popST_def pushST_def) |
|
274 apply (simp) |
|
275 apply (simp (no_asm_simp) add: replST_def) |
|
276 |
|
277 |
|
278 (* LAcc *) |
|
279 apply (intro strip) |
|
280 apply (drule LAcc_invers) |
|
281 apply (simp add: pushST_def is_inited_LT_def) |
|
282 apply (simp add: wf_prog_def) |
|
283 apply (frule wf_java_mdecl_disjoint_varnames) |
|
284 apply (simp add: disjoint_varnames_def) |
|
285 apply (frule wf_java_mdecl_length_pTs_pns) |
|
286 apply (erule conjE)+ |
|
287 apply (simp (no_asm_simp) add: local_env_inited_LT) |
|
288 |
|
289 (* LAss *) |
|
290 apply (intro strip) |
|
291 apply (drule LAss_invers, clarify) |
|
292 apply (drule LAcc_invers) |
|
293 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+) |
|
294 apply (simp add: popST_def dupST_def) |
|
295 |
|
296 (* FAcc *) |
|
297 apply (intro strip) |
|
298 apply (drule FAcc_invers, clarify) |
|
299 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+) |
|
300 apply (simp add: replST_def) |
|
301 |
|
302 (* show snd (the (field (G, cname) vname)) = T *) |
|
303 apply (subgoal_tac "is_class G Ca") |
|
304 apply (subgoal_tac "is_class G cname \<and> field (G, cname) vname = Some (cname, T)") |
|
305 apply simp |
|
306 |
|
307 (* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *) |
|
308 apply (rule field_in_fd) apply assumption+ |
|
309 (* show is_class G Ca *) |
|
310 apply (rule wt_class_expr_is_class, assumption+, rule HOL.refl) |
|
311 |
|
312 (* FAss *) |
|
313 apply (intro strip) |
|
314 apply (drule FAss_invers, clarify) |
|
315 apply (drule FAcc_invers, clarify) |
|
316 apply (drule_tac x=ST in spec) |
|
317 apply (drule_tac x="Class Ca # ST" in spec) |
|
318 apply ((drule spec)+, (drule mp, assumption)+) |
|
319 apply (simp add: popST_def dup_x1ST_def) |
|
320 |
|
321 |
|
322 (* Call *) |
|
323 apply (intro strip) |
|
324 apply (drule Call_invers, clarify) |
|
325 apply (drule_tac x=ST in spec) |
|
326 apply (drule_tac x="Class cname # ST" in spec) |
|
327 apply ((drule spec)+, (drule mp, assumption)+) |
|
328 apply (simp add: replST_def) |
|
329 |
|
330 |
|
331 (* expression lists *) |
|
332 (* nil *) |
|
333 |
|
334 apply (intro strip) |
|
335 apply (drule Nil_invers) |
|
336 apply (simp add: comb_nil_def) |
|
337 |
|
338 (* cons *) |
|
339 |
|
340 apply (intro strip) |
|
341 apply (drule Cons_invers, clarify) |
|
342 apply (drule_tac x=ST in spec) |
|
343 apply (drule_tac x="T # ST" in spec) |
|
344 apply ((drule spec)+, (drule mp, assumption)+) |
|
345 apply simp |
|
346 |
|
347 done |
|
348 |
|
349 |
|
350 |
|
351 lemmas compTpExpr_LT_ST [rule_format (no_asm)] = |
|
352 compTpExpr_Exprs_LT_ST [THEN conjunct1] |
|
353 |
|
354 lemmas compTpExprs_LT_ST [rule_format (no_asm)] = |
|
355 compTpExpr_Exprs_LT_ST [THEN conjunct2] |
|
356 |
|
357 lemma compTpStmt_LT_ST [rule_format (no_asm)]: " |
|
358 \<lbrakk> jmb = (pns,lvars,blk,res); |
|
359 wf_prog wf_java_mdecl G; |
|
360 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
361 E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> |
|
362 \<Longrightarrow> (\<forall> ST LT. |
|
363 E \<turnstile> s\<surd> \<longrightarrow> |
|
364 (is_inited_LT C pTs lvars LT) |
|
365 \<longrightarrow> sttp_of (compTpStmt jmb G s (ST, LT)) = (ST, LT))" |
|
366 |
|
367 apply (rule stmt.induct) |
|
368 |
|
369 (* Skip *) |
|
370 apply (intro strip) |
|
371 apply simp |
|
372 |
|
373 (* Expr *) |
|
374 apply (intro strip) |
|
375 apply (drule Expr_invers, erule exE) |
|
376 apply (simp (no_asm_simp) add: compTpExpr_LT_ST) |
|
377 apply (frule_tac ST=ST in compTpExpr_LT_ST, assumption+) |
|
378 apply (simp add: popST_def) |
|
379 |
|
380 (* Comp *) |
|
381 apply (intro strip) |
|
382 apply (drule Comp_invers, clarify) |
|
383 apply (simp (no_asm_use)) |
|
384 apply simp |
|
385 |
|
386 (* Cond *) |
|
387 apply (intro strip) |
|
388 apply (drule Cond_invers) |
|
389 apply (erule conjE)+ |
|
390 apply (drule_tac x=ST in spec) |
|
391 apply (drule_tac x=ST in spec) |
|
392 apply (drule spec)+ apply (drule mp, assumption)+ |
|
393 apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+) |
|
394 apply (simp add: popST_def pushST_def nochangeST_def) |
|
395 |
|
396 (* Loop *) |
|
397 apply (intro strip) |
|
398 apply (drule Loop_invers) |
|
399 apply (erule conjE)+ |
|
400 apply (drule_tac x=ST in spec) |
|
401 apply (drule spec)+ apply (drule mp, assumption)+ |
|
402 apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+) |
|
403 apply (simp add: popST_def pushST_def nochangeST_def) |
|
404 done |
|
405 |
|
406 |
|
407 |
|
408 lemma compTpInit_LT_ST: " |
|
409 sttp_of (compTpInit jmb (vn,ty) (ST, LT)) = (ST, LT[(index jmb vn):= OK ty])" |
|
410 by (simp add: compTpInit_def storeST_def pushST_def) |
|
411 |
|
412 |
|
413 lemma compTpInitLvars_LT_ST_aux [rule_format (no_asm)]: |
|
414 "\<forall> pre lvars_pre lvars0. |
|
415 jmb = (pns,lvars0,blk,res) \<and> |
|
416 lvars0 = (lvars_pre @ lvars) \<and> |
|
417 (length pns) + (length lvars_pre) + 1 = length pre \<and> |
|
418 disjoint_varnames pns (lvars_pre @ lvars) |
|
419 \<longrightarrow> |
|
420 sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err)) |
|
421 = (ST, pre @ map (Fun.comp OK snd) lvars)" |
|
422 apply (induct lvars) |
|
423 apply simp |
|
424 |
|
425 apply (intro strip) |
|
426 apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)") |
|
427 prefer 2 apply (simp (no_asm_simp)) |
|
428 apply ((erule exE)+, simp (no_asm_simp)) |
|
429 |
|
430 apply (drule_tac x="pre @ [OK ty]" in spec) |
|
431 apply (drule_tac x="lvars_pre @ [a]" in spec) |
|
432 apply (drule_tac x="lvars0" in spec) |
|
433 apply (simp add: compTpInit_LT_ST index_of_var2) |
|
434 done |
|
435 |
|
436 lemma compTpInitLvars_LT_ST: |
|
437 "\<lbrakk> jmb = (pns, lvars, blk, res); wf_java_mdecl G C ((mn, pTs), rT, jmb) \<rbrakk> |
|
438 \<Longrightarrow>(sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars)))) |
|
439 = (ST, inited_LT C pTs lvars)" |
|
440 apply (simp add: start_LT_def inited_LT_def) |
|
441 apply (simp only: append_Cons [THEN sym]) |
|
442 apply (rule compTpInitLvars_LT_ST_aux) |
|
443 apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames) |
|
444 done |
|
445 |
|
446 |
|
447 |
|
448 (********************************************************************************) |
|
449 |
|
450 lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)" |
|
451 by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def) |
|
452 |
|
453 lemma max_of_list_sublist: "set xs \<subseteq> set ys |
|
454 \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)" |
|
455 by (induct xs, auto dest: max_of_list_elem simp: max_of_list_def) |
|
456 |
|
457 lemma max_of_list_append [simp]: |
|
458 "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" |
|
459 apply (simp add: max_of_list_def) |
|
460 apply (induct xs) |
|
461 apply simp |
|
462 apply simp |
|
463 apply arith |
|
464 done |
|
465 |
|
466 |
|
467 lemma app_mono_mxs: "\<lbrakk> app i G mxs rT pc et s; mxs \<le> mxs' \<rbrakk> |
|
468 \<Longrightarrow> app i G mxs' rT pc et s" |
|
469 apply (case_tac s) |
|
470 apply (simp add: app_def) |
|
471 apply (case_tac i) |
|
472 apply (auto intro: less_trans) |
|
473 done |
|
474 |
|
475 |
|
476 |
|
477 lemma err_mono [simp]: "A \<subseteq> B \<Longrightarrow> err A \<subseteq> err B" |
|
478 by (auto simp: err_def) |
|
479 |
|
480 lemma opt_mono [simp]: "A \<subseteq> B \<Longrightarrow> opt A \<subseteq> opt B" |
|
481 by (auto simp: opt_def) |
|
482 |
|
483 |
|
484 lemma states_mono: "\<lbrakk> mxs \<le> mxs' \<rbrakk> |
|
485 \<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr" |
|
486 apply (simp add: states_def JVMType.sl_def) |
|
487 apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def |
|
488 JType.esl_def) |
|
489 apply (simp add: Err.esl_def Err.le_def Listn.le_def) |
|
490 apply (simp add: Product.le_def Product.sup_def Err.sup_def) |
|
491 apply (simp add: Opt.esl_def Listn.sup_def) |
|
492 apply (rule err_mono) |
|
493 apply (rule opt_mono) |
|
494 apply (rule Sigma_mono) |
|
495 apply (rule Union_mono) |
|
496 apply auto |
|
497 done |
|
498 |
|
499 |
|
500 lemma check_type_mono: "\<lbrakk> check_type G mxs mxr s; mxs \<le> mxs' \<rbrakk> |
|
501 \<Longrightarrow> check_type G mxs' mxr s" |
|
502 apply (simp add: check_type_def) |
|
503 apply (frule_tac G=G and mxr=mxr in states_mono) |
|
504 apply auto |
|
505 done |
|
506 |
|
507 |
|
508 (* wt is preserved when adding instructions/state-types at the end *) |
|
509 lemma wt_instr_prefix: " |
|
510 \<lbrakk> wt_instr_altern (bc ! pc) cG rT mt mxs mxr max_pc et pc; |
|
511 bc' = bc @ bc_post; mt' = mt @ mt_post; |
|
512 mxs \<le> mxs'; max_pc \<le> max_pc'; |
|
513 pc < length bc; pc < length mt; |
|
514 max_pc = (length mt)\<rbrakk> |
|
515 \<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' et pc" |
|
516 apply (simp add: wt_instr_altern_def nth_append) |
|
517 apply (auto intro: app_mono_mxs check_type_mono) |
|
518 done |
|
519 |
|
520 |
|
521 (************************************************************************) |
|
522 |
|
523 |
|
524 |
|
525 lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n)) |
|
526 \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))" |
|
527 apply (induct i) |
|
528 apply simp+ |
|
529 (* case Goto *) |
|
530 apply (simp only: nat_canonify) |
|
531 apply simp |
|
532 (* case Ifcmpeq *) |
|
533 apply simp |
|
534 apply (erule disjE) |
|
535 apply simp |
|
536 apply (simp only: nat_canonify) |
|
537 apply simp |
|
538 (* case Throw *) |
|
539 apply simp |
|
540 done |
|
541 |
|
542 |
|
543 lemma pc_succs_le: "\<lbrakk> pc' \<in> set (succs i (pc'' + n)); |
|
544 \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> |
|
545 \<Longrightarrow> n \<le> pc'" |
|
546 apply (induct i) |
|
547 apply simp+ |
|
548 (* case Goto *) |
|
549 apply (simp only: nat_canonify) |
|
550 apply simp |
|
551 (* case Ifcmpeq *) |
|
552 apply simp |
|
553 apply (erule disjE) |
|
554 apply simp |
|
555 apply (simp only: nat_canonify) |
|
556 apply simp |
|
557 (* case Throw *) |
|
558 apply simp |
|
559 done |
|
560 |
|
561 |
|
562 (**********************************************************************) |
|
563 |
|
564 constdefs |
|
565 offset_xcentry :: "[nat, exception_entry] \<Rightarrow> exception_entry" |
|
566 "offset_xcentry == |
|
567 \<lambda> n (start_pc, end_pc, handler_pc, catch_type). |
|
568 (start_pc + n, end_pc + n, handler_pc + n, catch_type)" |
|
569 |
|
570 offset_xctable :: "[nat, exception_table] \<Rightarrow> exception_table" |
|
571 "offset_xctable n == (map (offset_xcentry n))" |
|
572 |
|
573 lemma match_xcentry_offset [simp]: " |
|
574 match_exception_entry G cn (pc + n) (offset_xcentry n ee) = |
|
575 match_exception_entry G cn pc ee" |
|
576 by (simp add: match_exception_entry_def offset_xcentry_def split_beta) |
|
577 |
|
578 lemma match_xctable_offset: " |
|
579 (match_exception_table G cn (pc + n) (offset_xctable n et)) = |
|
580 (option_map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))" |
|
581 apply (induct et) |
|
582 apply (simp add: offset_xctable_def)+ |
|
583 apply (case_tac "match_exception_entry G cn pc a") |
|
584 apply (simp add: offset_xcentry_def split_beta)+ |
|
585 done |
|
586 |
|
587 |
|
588 lemma match_offset [simp]: " |
|
589 match G cn (pc + n) (offset_xctable n et) = match G cn pc et" |
|
590 apply (induct et) |
|
591 apply (simp add: offset_xctable_def)+ |
|
592 done |
|
593 |
|
594 lemma match_any_offset [simp]: " |
|
595 match_any G (pc + n) (offset_xctable n et) = match_any G pc et" |
|
596 apply (induct et) |
|
597 apply (simp add: offset_xctable_def offset_xcentry_def split_beta)+ |
|
598 done |
|
599 |
|
600 lemma app_mono_pc: "\<lbrakk> app i G mxs rT pc et s; pc'= pc + n \<rbrakk> |
|
601 \<Longrightarrow> app i G mxs rT pc' (offset_xctable n et) s" |
|
602 apply (case_tac s) |
|
603 apply (simp add: app_def) |
|
604 apply (case_tac i) |
|
605 apply (auto) |
|
606 done |
|
607 |
|
608 (**********************************************************************) |
|
609 |
|
610 (* Currently: empty exception_table *) |
|
611 |
|
612 syntax |
|
613 empty_et :: exception_table |
|
614 translations |
|
615 "empty_et" => "[]" |
|
616 |
|
617 |
|
618 |
|
619 (* move into Effect.thy *) |
|
620 lemma xcpt_names_Nil [simp]: "(xcpt_names (i, G, pc, [])) = []" |
|
621 by (induct i, simp_all) |
|
622 |
|
623 lemma xcpt_eff_Nil [simp]: "(xcpt_eff i G pc s []) = []" |
|
624 by (simp add: xcpt_eff_def) |
|
625 |
|
626 |
|
627 lemma app_jumps_lem: "\<lbrakk> app i cG mxs rT pc empty_et s; s=(Some st) \<rbrakk> |
|
628 \<Longrightarrow> \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc + b))" |
|
629 apply (simp only:) |
|
630 apply (induct i) |
|
631 apply auto |
|
632 done |
|
633 |
|
634 |
|
635 (* wt is preserved when adding instructions/state-types to the front *) |
|
636 lemma wt_instr_offset: " |
|
637 \<lbrakk> \<forall> pc'' < length mt. |
|
638 wt_instr_altern ((bc@bc_post) ! pc'') cG rT (mt@mt_post) mxs mxr max_pc empty_et pc''; |
|
639 bc' = bc_pre @ bc @ bc_post; mt' = mt_pre @ mt @ mt_post; |
|
640 length bc_pre = length mt_pre; length bc = length mt; |
|
641 length mt_pre \<le> pc; pc < length (mt_pre @ mt); |
|
642 mxs \<le> mxs'; max_pc + length mt_pre \<le> max_pc' \<rbrakk> |
|
643 \<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' empty_et pc" |
|
644 |
|
645 apply (simp add: wt_instr_altern_def) |
|
646 apply (subgoal_tac "\<exists> pc''. pc = pc'' + length mt_pre", erule exE) |
|
647 prefer 2 apply (rule_tac x="pc - length mt_pre" in exI, arith) |
|
648 |
|
649 apply (drule_tac x=pc'' in spec) |
|
650 apply (drule mp) apply arith (* show pc'' < length mt *) |
|
651 apply clarify |
|
652 |
|
653 apply (rule conjI) |
|
654 (* app *) |
|
655 apply (simp add: nth_append) |
|
656 apply (rule app_mono_mxs) |
|
657 apply (frule app_mono_pc) apply (rule HOL.refl) apply (simp add: offset_xctable_def) |
|
658 apply assumption+ |
|
659 |
|
660 (* check_type *) |
|
661 apply (rule conjI) |
|
662 apply (simp add: nth_append) |
|
663 apply (rule check_type_mono) apply assumption+ |
|
664 |
|
665 (* ..eff.. *) |
|
666 apply (intro ballI) |
|
667 apply (subgoal_tac "\<exists> pc' s'. x = (pc', s')", (erule exE)+, simp) |
|
668 |
|
669 apply (case_tac s') |
|
670 (* s' = None *) |
|
671 apply (simp add: eff_def nth_append norm_eff_def) |
|
672 apply (frule_tac x="(pc', None)" and f=fst and b=pc' in rev_image_eqI) |
|
673 apply (simp (no_asm_simp)) |
|
674 apply (simp only: fst_conv image_compose [THEN sym] Fun.comp_def) |
|
675 apply simp |
|
676 apply (frule pc_succs_shift) |
|
677 apply (drule bspec, assumption) |
|
678 apply arith |
|
679 |
|
680 (* s' = Some a *) |
|
681 apply (drule_tac x="(pc' - length mt_pre, s')" in bspec) |
|
682 |
|
683 (* show (pc' - length mt_pre, s') \<in> set (eff \<dots>) *) |
|
684 apply (simp add: eff_def) |
|
685 (* norm_eff *) |
|
686 apply (clarsimp simp: nth_append pc_succs_shift) |
|
687 |
|
688 (* show P x of bspec *) |
|
689 apply simp |
|
690 apply (subgoal_tac "length mt_pre \<le> pc'") |
|
691 apply (simp add: nth_append) apply arith |
|
692 |
|
693 (* subgoals *) |
|
694 apply (simp add: eff_def xcpt_eff_def) |
|
695 apply (clarsimp) |
|
696 apply (rule pc_succs_le) apply assumption+ |
|
697 apply (subgoal_tac "\<exists> st. mt ! pc'' = Some st", erule exE) |
|
698 apply (rule_tac s="Some st" and st=st and cG=cG and mxs=mxs and rT=rT |
|
699 in app_jumps_lem) |
|
700 apply (simp add: nth_append)+ |
|
701 (* subgoal \<exists> st. mt ! pc'' = Some st *) |
|
702 apply (simp add: norm_eff_def option_map_def nth_append) |
|
703 apply (case_tac "mt ! pc''") |
|
704 apply simp+ |
|
705 done |
|
706 |
|
707 |
|
708 (**********************************************************************) |
|
709 |
|
710 |
|
711 constdefs |
|
712 start_sttp_resp_cons :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool" |
|
713 "start_sttp_resp_cons f == |
|
714 (\<forall> sttp. let (mt', sttp') = (f sttp) in (\<exists>mt'_rest. mt' = Some sttp # mt'_rest))" |
|
715 |
|
716 start_sttp_resp :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool" |
|
717 "start_sttp_resp f == (f = comb_nil) \<or> (start_sttp_resp_cons f)" |
|
718 |
|
719 lemma start_sttp_resp_comb_nil [simp]: "start_sttp_resp comb_nil" |
|
720 by (simp add: start_sttp_resp_def) |
|
721 |
|
722 lemma start_sttp_resp_cons_comb_cons [simp]: "start_sttp_resp_cons f |
|
723 \<Longrightarrow> start_sttp_resp_cons (f \<box> f')" |
|
724 apply (simp add: start_sttp_resp_cons_def comb_def split_beta) |
|
725 apply (rule allI) |
|
726 apply (drule_tac x=sttp in spec) |
|
727 apply auto |
|
728 done |
|
729 |
|
730 lemma start_sttp_resp_cons_comb_cons_r: "\<lbrakk> start_sttp_resp f; start_sttp_resp_cons f'\<rbrakk> |
|
731 \<Longrightarrow> start_sttp_resp_cons (f \<box> f')" |
|
732 apply (simp add: start_sttp_resp_def) |
|
733 apply (erule disjE) |
|
734 apply simp+ |
|
735 done |
|
736 |
|
737 lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f |
|
738 \<Longrightarrow> start_sttp_resp (f \<box> f')" |
|
739 by (simp add: start_sttp_resp_def) |
|
740 |
|
741 lemma start_sttp_resp_comb: "\<lbrakk> start_sttp_resp f; start_sttp_resp f' \<rbrakk> |
|
742 \<Longrightarrow> start_sttp_resp (f \<box> f')" |
|
743 apply (simp add: start_sttp_resp_def) |
|
744 apply (erule disjE) |
|
745 apply simp |
|
746 apply (erule disjE) |
|
747 apply simp+ |
|
748 done |
|
749 |
|
750 lemma start_sttp_resp_cons_nochangeST [simp]: "start_sttp_resp_cons nochangeST" |
|
751 by (simp add: start_sttp_resp_cons_def nochangeST_def) |
|
752 |
|
753 lemma start_sttp_resp_cons_pushST [simp]: "start_sttp_resp_cons (pushST Ts)" |
|
754 by (simp add: start_sttp_resp_cons_def pushST_def split_beta) |
|
755 |
|
756 lemma start_sttp_resp_cons_dupST [simp]: "start_sttp_resp_cons dupST" |
|
757 by (simp add: start_sttp_resp_cons_def dupST_def split_beta) |
|
758 |
|
759 lemma start_sttp_resp_cons_dup_x1ST [simp]: "start_sttp_resp_cons dup_x1ST" |
|
760 by (simp add: start_sttp_resp_cons_def dup_x1ST_def split_beta) |
|
761 |
|
762 lemma start_sttp_resp_cons_popST [simp]: "start_sttp_resp_cons (popST n)" |
|
763 by (simp add: start_sttp_resp_cons_def popST_def split_beta) |
|
764 |
|
765 lemma start_sttp_resp_cons_replST [simp]: "start_sttp_resp_cons (replST n tp)" |
|
766 by (simp add: start_sttp_resp_cons_def replST_def split_beta) |
|
767 |
|
768 lemma start_sttp_resp_cons_storeST [simp]: "start_sttp_resp_cons (storeST i tp)" |
|
769 by (simp add: start_sttp_resp_cons_def storeST_def split_beta) |
|
770 |
|
771 lemma start_sttp_resp_cons_compTpExpr [simp]: "start_sttp_resp_cons (compTpExpr jmb G ex)" |
|
772 apply (induct ex) |
|
773 apply simp+ |
|
774 apply (simp add: start_sttp_resp_cons_def comb_def pushST_def split_beta) (* LAcc *) |
|
775 apply simp+ |
|
776 done |
|
777 |
|
778 lemma start_sttp_resp_cons_compTpInit [simp]: "start_sttp_resp_cons (compTpInit jmb lv)" |
|
779 by (simp add: compTpInit_def split_beta) |
|
780 |
|
781 |
|
782 lemma start_sttp_resp_nochangeST [simp]: "start_sttp_resp nochangeST" |
|
783 by (simp add: start_sttp_resp_def) |
|
784 |
|
785 lemma start_sttp_resp_pushST [simp]: "start_sttp_resp (pushST Ts)" |
|
786 by (simp add: start_sttp_resp_def) |
|
787 |
|
788 lemma start_sttp_resp_dupST [simp]: "start_sttp_resp dupST" |
|
789 by (simp add: start_sttp_resp_def) |
|
790 |
|
791 lemma start_sttp_resp_dup_x1ST [simp]: "start_sttp_resp dup_x1ST" |
|
792 by (simp add: start_sttp_resp_def) |
|
793 |
|
794 lemma start_sttp_resp_popST [simp]: "start_sttp_resp (popST n)" |
|
795 by (simp add: start_sttp_resp_def) |
|
796 |
|
797 lemma start_sttp_resp_replST [simp]: "start_sttp_resp (replST n tp)" |
|
798 by (simp add: start_sttp_resp_def) |
|
799 |
|
800 lemma start_sttp_resp_storeST [simp]: "start_sttp_resp (storeST i tp)" |
|
801 by (simp add: start_sttp_resp_def) |
|
802 |
|
803 lemma start_sttp_resp_compTpExpr [simp]: "start_sttp_resp (compTpExpr jmb G ex)" |
|
804 by (simp add: start_sttp_resp_def) |
|
805 |
|
806 lemma start_sttp_resp_compTpExprs [simp]: "start_sttp_resp (compTpExprs jmb G exs)" |
|
807 by (induct exs, (simp add: start_sttp_resp_comb)+) |
|
808 |
|
809 lemma start_sttp_resp_compTpStmt [simp]: "start_sttp_resp (compTpStmt jmb G s)" |
|
810 by (induct s, (simp add: start_sttp_resp_comb)+) |
|
811 |
|
812 lemma start_sttp_resp_compTpInitLvars [simp]: "start_sttp_resp (compTpInitLvars jmb lvars)" |
|
813 by (induct lvars, simp+) |
|
814 |
|
815 |
|
816 |
|
817 |
|
818 (* ********************************************************************** *) |
|
819 (* length of compExpr/ compTpExprs *) |
|
820 (* ********************************************************************** *) |
|
821 |
|
822 lemma length_comb [simp]: "length (mt_of ((f1 \<box> f2) sttp)) = |
|
823 length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))" |
|
824 by (simp add: comb_def split_beta) |
|
825 |
|
826 |
|
827 lemma length_comb_nil [simp]: "length (mt_of (comb_nil sttp)) = 0" |
|
828 by (simp add: comb_nil_def) |
|
829 |
|
830 lemma length_nochangeST [simp]: "length (mt_of (nochangeST sttp)) = 1" |
|
831 by (simp add: nochangeST_def) |
|
832 |
|
833 lemma length_pushST [simp]: "length (mt_of (pushST Ts sttp)) = 1" |
|
834 by (simp add: pushST_def split_beta) |
|
835 |
|
836 lemma length_dupST [simp]: "length (mt_of (dupST sttp)) = 1" |
|
837 by (simp add: dupST_def split_beta) |
|
838 |
|
839 lemma length_dup_x1ST [simp]: "length (mt_of (dup_x1ST sttp)) = 1" |
|
840 by (simp add: dup_x1ST_def split_beta) |
|
841 |
|
842 lemma length_popST [simp]: "length (mt_of (popST n sttp)) = 1" |
|
843 by (simp add: popST_def split_beta) |
|
844 |
|
845 lemma length_replST [simp]: "length (mt_of (replST n tp sttp)) = 1" |
|
846 by (simp add: replST_def split_beta) |
|
847 |
|
848 lemma length_storeST [simp]: "length (mt_of (storeST i tp sttp)) = 1" |
|
849 by (simp add: storeST_def split_beta) |
|
850 |
|
851 |
|
852 lemma length_compTpExpr_Exprs [rule_format]: " |
|
853 (\<forall> sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex))) |
|
854 \<and> (\<forall> sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))" |
|
855 apply (rule expr.induct) |
|
856 apply simp+ |
|
857 apply (case_tac binop) |
|
858 apply simp+ |
|
859 apply (simp add: pushST_def split_beta) |
|
860 apply simp+ |
|
861 done |
|
862 |
|
863 lemma length_compTpExpr: "length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)" |
|
864 by (rule length_compTpExpr_Exprs [THEN conjunct1 [THEN spec]]) |
|
865 |
|
866 lemma length_compTpExprs: "length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)" |
|
867 by (rule length_compTpExpr_Exprs [THEN conjunct2 [THEN spec]]) |
|
868 |
|
869 lemma length_compTpStmt [rule_format]: " |
|
870 (\<forall> sttp. (length (mt_of (compTpStmt jmb G s sttp)) = length (compStmt jmb s)))" |
|
871 apply (rule stmt.induct) |
|
872 apply (simp add: length_compTpExpr)+ |
|
873 done |
|
874 |
|
875 |
|
876 lemma length_compTpInit: "length (mt_of (compTpInit jmb lv sttp)) = length (compInit jmb lv)" |
|
877 by (simp add: compTpInit_def compInit_def split_beta) |
|
878 |
|
879 lemma length_compTpInitLvars [rule_format]: |
|
880 "\<forall> sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)" |
|
881 by (induct lvars, (simp add: compInitLvars_def length_compTpInit split_beta)+) |
|
882 |
|
883 |
|
884 (* ********************************************************************** *) |
|
885 (* Correspondence bytecode - method types *) |
|
886 (* ********************************************************************** *) |
|
887 |
|
888 syntax |
|
889 ST_of :: "state_type \<Rightarrow> opstack_type" |
|
890 LT_of :: "state_type \<Rightarrow> locvars_type" |
|
891 translations |
|
892 "ST_of" => "fst" |
|
893 "LT_of" => "snd" |
|
894 |
|
895 lemma states_lower: |
|
896 "\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk> |
|
897 \<Longrightarrow> OK (Some (ST, LT)) \<in> states cG (length ST) mxr" |
|
898 apply (simp add: states_def JVMType.sl_def) |
|
899 apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def |
|
900 JType.esl_def) |
|
901 apply (simp add: Err.esl_def Err.le_def Listn.le_def) |
|
902 apply (simp add: Product.le_def Product.sup_def Err.sup_def) |
|
903 apply (simp add: Opt.esl_def Listn.sup_def) |
|
904 apply clarify |
|
905 apply auto |
|
906 done |
|
907 |
|
908 lemma check_type_lower: |
|
909 "\<lbrakk> check_type cG mxs mxr (OK (Some (ST, LT))); length ST \<le> mxs\<rbrakk> |
|
910 \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))" |
|
911 by (simp add: check_type_def states_lower) |
|
912 |
|
913 lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y" |
|
914 by (simp del: max_assoc add: max_assoc [THEN sym]) |
|
915 |
|
916 (* ******************************************************************* *) |
|
917 |
|
918 constdefs |
|
919 bc_mt_corresp :: " |
|
920 [bytecode, state_type \<Rightarrow> method_type \<times> state_type, state_type, jvm_prog, ty, nat, p_count] |
|
921 \<Rightarrow> bool" |
|
922 |
|
923 "bc_mt_corresp bc f sttp0 cG rT mxr idx == |
|
924 let (mt, sttp) = f sttp0 in |
|
925 (length bc = length mt \<and> |
|
926 ((check_type cG (length (ST_of sttp0)) mxr (OK (Some sttp0))) \<longrightarrow> |
|
927 (\<forall> mxs. |
|
928 mxs = max_ssize (mt@[Some sttp]) \<longrightarrow> |
|
929 (\<forall> pc. pc < idx \<longrightarrow> |
|
930 wt_instr_altern (bc ! pc) cG rT (mt@[Some sttp]) mxs mxr (length mt + 1) empty_et pc) |
|
931 \<and> |
|
932 check_type cG mxs mxr (OK ((mt@[Some sttp]) ! idx)))))" |
|
933 |
|
934 |
|
935 lemma bc_mt_corresp_comb: " |
|
936 \<lbrakk> bc' = (bc1@bc2); l' = (length bc'); |
|
937 bc_mt_corresp bc1 f1 sttp0 cG rT mxr (length bc1); |
|
938 bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2); |
|
939 start_sttp_resp f2\<rbrakk> |
|
940 \<Longrightarrow> bc_mt_corresp bc' (f1 \<box> f2) sttp0 cG rT mxr l'" |
|
941 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+) |
|
942 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+) |
|
943 |
|
944 (* unfold start_sttp_resp and make case distinction *) |
|
945 apply (simp only: start_sttp_resp_def) |
|
946 apply (erule disjE) |
|
947 (* case f2 = comb_nil *) |
|
948 apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def) |
|
949 apply (erule conjE)+ |
|
950 apply (intro strip) |
|
951 apply simp |
|
952 |
|
953 (* case start_sttp_resp_cons f2 *) |
|
954 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def del: all_simps) |
|
955 apply (intro strip) |
|
956 apply (erule conjE)+ |
|
957 apply (drule mp, assumption) |
|
958 apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))") |
|
959 apply (erule conjE)+ |
|
960 apply (drule mp, assumption) |
|
961 apply (erule conjE)+ |
|
962 |
|
963 apply (rule conjI) |
|
964 (* show wt_instr \<dots> *) |
|
965 |
|
966 apply (drule_tac x=sttp1 in spec, simp) |
|
967 apply (erule exE) |
|
968 apply (intro strip) |
|
969 apply (case_tac "pc < length mt1") |
|
970 |
|
971 (* case pc < length mt1 *) |
|
972 apply (drule spec, drule mp, simp) |
|
973 apply simp |
|
974 apply (rule_tac mt="mt1 @ [Some sttp1]" in wt_instr_prefix) |
|
975 apply assumption+ apply (rule HOL.refl) |
|
976 apply (simp (no_asm_simp)) |
|
977 apply (simp (no_asm_simp) add: max_ssize_def) |
|
978 apply (simp add: max_of_list_def max_ac) |
|
979 apply arith |
|
980 apply (simp (no_asm_simp))+ |
|
981 |
|
982 (* case pc \<ge> length mt1 *) |
|
983 apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]" |
|
984 and mxr=mxr |
|
985 in wt_instr_offset) |
|
986 apply simp |
|
987 apply (simp (no_asm_simp))+ |
|
988 apply simp |
|
989 apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def) |
|
990 apply (simp (no_asm_simp))+ |
|
991 |
|
992 (* show check_type \<dots> *) |
|
993 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2") |
|
994 apply (simp only:) |
|
995 apply (rule check_type_mono) apply assumption |
|
996 apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append max_ac) |
|
997 apply arith |
|
998 apply (simp add: nth_append) |
|
999 |
|
1000 apply (erule conjE)+ |
|
1001 apply (case_tac sttp1) |
|
1002 apply (simp add: check_type_def) |
|
1003 apply (rule states_lower, assumption) |
|
1004 apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append) |
|
1005 apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def) |
|
1006 apply (simp (no_asm_simp))+ |
|
1007 done |
|
1008 |
|
1009 |
|
1010 lemma bc_mt_corresp_zero [simp]: "\<lbrakk> length (mt_of (f sttp)) = length bc; start_sttp_resp f\<rbrakk> |
|
1011 \<Longrightarrow> bc_mt_corresp bc f sttp cG rT mxr 0" |
|
1012 apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta) |
|
1013 apply (erule disjE) |
|
1014 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split_beta) |
|
1015 apply (intro strip) |
|
1016 apply (simp add: start_sttp_resp_cons_def split_beta) |
|
1017 apply (drule_tac x=sttp in spec, erule exE) |
|
1018 apply simp |
|
1019 apply (rule check_type_mono, assumption) |
|
1020 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split_beta) |
|
1021 done |
|
1022 |
|
1023 (* ********************************************************************** *) |
|
1024 |
|
1025 |
|
1026 constdefs |
|
1027 mt_sttp_flatten :: "method_type \<times> state_type \<Rightarrow> method_type" |
|
1028 "mt_sttp_flatten mt_sttp == (mt_of mt_sttp) @ [Some (sttp_of mt_sttp)]" |
|
1029 |
|
1030 |
|
1031 lemma mt_sttp_flatten_length [simp]: "n = (length (mt_of (f sttp))) |
|
1032 \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! n = Some (sttp_of (f sttp))" |
|
1033 by (simp add: mt_sttp_flatten_def) |
|
1034 |
|
1035 lemma mt_sttp_flatten_comb: "(mt_sttp_flatten ((f1 \<box> f2) sttp)) = |
|
1036 (mt_of (f1 sttp)) @ (mt_sttp_flatten (f2 (sttp_of (f1 sttp))))" |
|
1037 by (simp add: mt_sttp_flatten_def comb_def split_beta) |
|
1038 |
|
1039 lemma mt_sttp_flatten_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk> |
|
1040 \<Longrightarrow> (mt_sttp_flatten ((f1 \<box> f2) sttp) ! n) = (mt_sttp_flatten (f2 (sttp_of (f1 sttp))) ! (n - n1))" |
|
1041 by (simp add: mt_sttp_flatten_comb nth_append) |
|
1042 |
|
1043 lemma mt_sttp_flatten_comb_zero [simp]: "start_sttp_resp f |
|
1044 \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! 0 = Some sttp" |
|
1045 apply (simp only: start_sttp_resp_def) |
|
1046 apply (erule disjE) |
|
1047 apply (simp add: comb_nil_def mt_sttp_flatten_def) |
|
1048 apply (simp add: start_sttp_resp_cons_def mt_sttp_flatten_def split_beta) |
|
1049 apply (drule_tac x=sttp in spec) |
|
1050 apply (erule exE) |
|
1051 apply simp |
|
1052 done |
|
1053 |
|
1054 |
|
1055 (* move into prelude -- compare with nat_int_length *) |
|
1056 lemma int_outside_right: "0 \<le> (m::int) \<Longrightarrow> m + (int n) = int ((nat m) + n)" |
|
1057 by simp |
|
1058 |
|
1059 lemma int_outside_left: "0 \<le> (m::int) \<Longrightarrow> (int n) + m = int (n + (nat m))" |
|
1060 by simp |
|
1061 |
|
1062 |
|
1063 |
|
1064 |
|
1065 (* ********************************************************************** *) |
|
1066 (* bc_mt_corresp for individual instructions *) |
|
1067 (* ---------------------------------------------------------------------- *) |
|
1068 |
|
1069 lemma less_Suc [simp] : "n \<le> k \<Longrightarrow> (k < Suc n) = (k = n)" |
|
1070 by arith |
|
1071 |
|
1072 lemmas check_type_simps = check_type_def states_def JVMType.sl_def |
|
1073 Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def |
|
1074 JType.esl_def Err.esl_def Err.le_def Listn.le_def Product.le_def Product.sup_def Err.sup_def |
|
1075 Opt.esl_def Listn.sup_def |
|
1076 |
|
1077 |
|
1078 lemma check_type_push: "\<lbrakk> |
|
1079 is_class cG cname; check_type cG (length ST) mxr (OK (Some (ST, LT))) \<rbrakk> |
|
1080 \<Longrightarrow> check_type cG (Suc (length ST)) mxr (OK (Some (Class cname # ST, LT)))" |
|
1081 apply (simp add: check_type_simps) |
|
1082 apply clarify |
|
1083 apply (rule_tac x="Suc (length ST)" in exI) |
|
1084 apply simp+ |
|
1085 done |
|
1086 |
|
1087 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk> |
|
1088 \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)" |
|
1089 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
|
1090 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1091 eff_def norm_eff_def) |
|
1092 apply (intro strip) |
|
1093 apply (rule conjI) |
|
1094 apply (rule check_type_mono, assumption, simp) |
|
1095 apply (simp add: check_type_push) |
|
1096 done |
|
1097 |
|
1098 lemma bc_mt_corresp_Pop: " |
|
1099 bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)" |
|
1100 apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1101 apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) |
|
1102 apply (simp add: max_def) |
|
1103 apply (simp add: check_type_simps) |
|
1104 apply clarify |
|
1105 apply (rule_tac x="(length ST)" in exI) |
|
1106 apply simp+ |
|
1107 done |
|
1108 |
|
1109 lemma bc_mt_corresp_Checkcast: "\<lbrakk> is_class cG cname; sttp = (ST, LT); |
|
1110 (\<exists>rT STo. ST = RefT rT # STo) \<rbrakk> |
|
1111 \<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)" |
|
1112 apply (erule exE)+ |
|
1113 apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1114 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def) |
|
1115 apply (simp add: check_type_simps) |
|
1116 apply clarify |
|
1117 apply (rule_tac x="Suc (length STo)" in exI) |
|
1118 apply simp+ |
|
1119 done |
|
1120 |
|
1121 |
|
1122 lemma bc_mt_corresp_LitPush: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<rbrakk> |
|
1123 \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)" |
|
1124 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+) |
|
1125 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
|
1126 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1127 eff_def norm_eff_def) |
|
1128 apply (intro strip) |
|
1129 apply (rule conjI) |
|
1130 apply (rule check_type_mono, assumption, simp) |
|
1131 apply (simp add: check_type_simps) |
|
1132 apply clarify |
|
1133 apply (rule_tac x="Suc (length ST)" in exI) |
|
1134 apply simp |
|
1135 apply (drule sym) |
|
1136 apply (case_tac val) |
|
1137 apply simp+ |
|
1138 done |
|
1139 |
|
1140 |
|
1141 lemma bc_mt_corresp_LitPush_CT: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<and> cG \<turnstile> T \<preceq> T'; |
|
1142 is_type cG T' \<rbrakk> |
|
1143 \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)" |
|
1144 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+) |
|
1145 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
|
1146 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1147 eff_def norm_eff_def) |
|
1148 apply (intro strip) |
|
1149 apply (rule conjI) |
|
1150 apply (rule check_type_mono, assumption, simp) |
|
1151 apply (simp add: check_type_simps) |
|
1152 apply (simp add: sup_state_Cons) |
|
1153 apply clarify |
|
1154 apply (rule_tac x="Suc (length ST)" in exI) |
|
1155 apply simp |
|
1156 apply simp+ |
|
1157 done |
|
1158 |
|
1159 lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk> |
|
1160 \<Longrightarrow> bc_mt_corresp [Load i] |
|
1161 (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)" |
|
1162 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
|
1163 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1164 eff_def norm_eff_def) |
|
1165 apply (intro strip) |
|
1166 apply (rule conjI) |
|
1167 apply (rule check_type_mono, assumption, simp) |
|
1168 apply (simp add: check_type_simps) |
|
1169 apply clarify |
|
1170 apply (rule_tac x="Suc (length ST)" in exI) |
|
1171 apply (simp (no_asm_simp)) |
|
1172 apply (simp only: err_def) |
|
1173 apply (frule listE_nth_in) apply assumption |
|
1174 apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}") |
|
1175 apply (drule CollectD) apply (erule bexE) |
|
1176 apply (simp (no_asm_simp) ) |
|
1177 apply blast |
|
1178 apply blast |
|
1179 done |
|
1180 |
|
1181 |
|
1182 lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk> |
|
1183 \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)" |
|
1184 apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1185 apply (simp add: max_ssize_def max_of_list_def ) |
|
1186 apply (simp add: ssize_sto_def) apply (simp add: max_def) |
|
1187 apply (intro strip) |
|
1188 apply (simp add: check_type_simps) |
|
1189 apply clarify |
|
1190 apply (rule conjI) |
|
1191 apply (rule_tac x="(length ST)" in exI) |
|
1192 apply simp+ |
|
1193 done |
|
1194 |
|
1195 |
|
1196 |
|
1197 lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG \<turnstile> LT[i := OK T] <=l LT \<rbrakk> |
|
1198 \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)" |
|
1199 apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1200 apply (simp add: sup_state_conv) |
|
1201 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def) |
|
1202 apply (simp add: max_def) |
|
1203 apply (intro strip) |
|
1204 apply (simp add: check_type_simps) |
|
1205 apply clarify |
|
1206 apply (rule_tac x="(length ST)" in exI) |
|
1207 apply simp+ |
|
1208 done |
|
1209 |
|
1210 |
|
1211 lemma bc_mt_corresp_Dup: " |
|
1212 bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)" |
|
1213 apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def |
|
1214 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1215 eff_def norm_eff_def) |
|
1216 apply (intro strip) |
|
1217 apply (rule conjI) |
|
1218 apply (rule check_type_mono, assumption, simp) |
|
1219 apply (simp add: check_type_simps) |
|
1220 apply clarify |
|
1221 apply (rule_tac x="Suc (Suc (length ST))" in exI) |
|
1222 apply simp+ |
|
1223 done |
|
1224 |
|
1225 lemma bc_mt_corresp_Dup_x1: " |
|
1226 bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)" |
|
1227 apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def |
|
1228 max_ssize_def max_of_list_def ssize_sto_def max_def |
|
1229 eff_def norm_eff_def) |
|
1230 apply (intro strip) |
|
1231 apply (rule conjI) |
|
1232 apply (rule check_type_mono, assumption, simp) |
|
1233 apply (simp add: check_type_simps) |
|
1234 apply clarify |
|
1235 apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI) |
|
1236 apply simp+ |
|
1237 done |
|
1238 |
|
1239 |
|
1240 |
|
1241 lemma bc_mt_corresp_IAdd: " |
|
1242 bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) |
|
1243 (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)" |
|
1244 apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1245 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def) |
|
1246 apply (simp add: check_type_simps) |
|
1247 apply clarify |
|
1248 apply (rule_tac x="Suc (length ST)" in exI) |
|
1249 apply simp+ |
|
1250 done |
|
1251 |
|
1252 lemma bc_mt_corresp_Getfield: "\<lbrakk> wf_prog wf_mb G; |
|
1253 field (G, C) vname = Some (cname, T); is_class G C \<rbrakk> |
|
1254 \<Longrightarrow> bc_mt_corresp [Getfield vname cname] |
|
1255 (replST (Suc 0) (snd (the (field (G, cname) vname)))) |
|
1256 (Class C # ST, LT) (comp G) rT mxr (Suc 0)" |
|
1257 apply (frule wf_subcls1) |
|
1258 apply (frule field_in_fd, assumption+) |
|
1259 apply (frule widen_field, assumption+) |
|
1260 apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1261 apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym]) |
|
1262 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def) |
|
1263 apply (intro strip) |
|
1264 apply (simp add: check_type_simps) |
|
1265 apply clarify |
|
1266 apply (rule_tac x="Suc (length ST)" in exI) |
|
1267 apply simp+ |
|
1268 apply (simp only: comp_is_type [THEN sym]) |
|
1269 apply (rule_tac C=cname in fields_is_type) |
|
1270 apply (simp add: field_def) |
|
1271 apply (drule JBasis.table_of_remap_SomeD)+ |
|
1272 apply assumption+ |
|
1273 done |
|
1274 |
|
1275 lemma bc_mt_corresp_Putfield: "\<lbrakk> wf_prog wf_mb G; |
|
1276 field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk> |
|
1277 \<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT) |
|
1278 (comp G) rT mxr (Suc 0)" |
|
1279 apply (frule wf_subcls1) |
|
1280 apply (frule field_in_fd, assumption+) |
|
1281 apply (frule widen_field, assumption+) |
|
1282 apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def) |
|
1283 apply (simp add: comp_field [THEN sym] comp_subcls1 [THEN sym] comp_widen [THEN sym] comp_is_class [THEN sym]) |
|
1284 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def) |
|
1285 |
|
1286 apply (intro strip) |
|
1287 apply (simp add: check_type_simps) |
|
1288 apply clarify |
|
1289 apply (rule_tac x="Suc (length ST)" in exI) |
|
1290 apply simp+ |
|
1291 done |
|
1292 |
|
1293 |
|
1294 |
|
1295 lemma Call_app: "\<lbrakk> wf_prog wf_mb G; is_class G cname; |
|
1296 STs = rev pTsa @ Class cname # ST; |
|
1297 max_spec G cname (mname, pTsa) = {((md, T), pTs')} \<rbrakk> |
|
1298 \<Longrightarrow> app (Invoke cname mname pTs') (comp G) (length (T # ST)) rT 0 empty_et (Some (STs, LTs))" |
|
1299 apply (subgoal_tac "(\<exists>mD' rT' comp_b. |
|
1300 method (comp G, cname) (mname, pTs') = Some (mD', rT', comp_b))") |
|
1301 apply (simp add: comp_is_class) |
|
1302 apply (rule_tac x=pTsa in exI) |
|
1303 apply (rule_tac x="Class cname" in exI) |
|
1304 apply (simp add: max_spec_preserves_length comp_is_class [THEN sym]) |
|
1305 apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) |
|
1306 apply (simp add: comp_widen list_all2_def) |
|
1307 apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) |
|
1308 apply (rule exI)+ |
|
1309 apply (rule comp_method) |
|
1310 apply assumption+ |
|
1311 done |
|
1312 |
|
1313 |
|
1314 lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; |
|
1315 max_spec G cname (mname, pTsa) = {((md, T), fpTs)}; |
|
1316 is_class G cname \<rbrakk> |
|
1317 \<Longrightarrow> bc_mt_corresp [Invoke cname mname fpTs] (replST (Suc (length pTsa)) T) |
|
1318 (rev pTsa @ Class cname # ST, LT) (comp G) rT mxr (Suc 0)" |
|
1319 apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def) |
|
1320 apply (simp add: replST_def del: appInvoke) |
|
1321 apply (intro strip) |
|
1322 apply (rule conjI) |
|
1323 |
|
1324 -- "app" |
|
1325 apply (rule Call_app [THEN app_mono_mxs]) apply assumption+ |
|
1326 apply (rule HOL.refl) apply assumption |
|
1327 apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def) |
|
1328 |
|
1329 -- "<=s" |
|
1330 apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+) |
|
1331 apply (frule comp_method, assumption+) |
|
1332 apply (simp add: max_spec_preserves_length [THEN sym]) |
|
1333 |
|
1334 -- "check_type" |
|
1335 apply (simp add: max_ssize_def ssize_sto_def max_def) |
|
1336 apply (simp add: max_of_list_def) |
|
1337 apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)") |
|
1338 apply simp |
|
1339 apply (simp add: check_type_simps) |
|
1340 apply clarify |
|
1341 apply (rule_tac x="Suc (length ST)" in exI) |
|
1342 apply simp+ |
|
1343 apply (simp only: comp_is_type [THEN sym]) |
|
1344 apply (frule method_wf_mdecl) apply assumption apply assumption |
|
1345 apply (simp add: wf_mdecl_def wf_mhead_def) |
|
1346 apply (simp add: max_def) |
|
1347 done |
|
1348 |
|
1349 |
|
1350 lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; |
|
1351 0 \<le> (int pc + i); nat (int pc + i) < max_pc; |
|
1352 (mt_sttp_flatten f ! pc = Some (ts#ts'#ST,LT)) \<and> |
|
1353 ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> (\<exists>r r'. ts = RefT r \<and> ts' = RefT r')); |
|
1354 mt_sttp_flatten f ! Suc pc = Some (ST,LT); |
|
1355 mt_sttp_flatten f ! nat (int pc + i) = Some (ST,LT); |
|
1356 check_type (TranslComp.comp G) mxs mxr (OK (Some (ts # ts' # ST, LT))) \<rbrakk> |
|
1357 \<Longrightarrow> wt_instr_altern (Ifcmpeq i) (comp G) rT (mt_sttp_flatten f) mxs mxr max_pc empty_et pc" |
|
1358 by (simp add: wt_instr_altern_def eff_def norm_eff_def) |
|
1359 |
|
1360 |
|
1361 lemma wt_instr_Goto: "\<lbrakk> 0 \<le> (int pc + i); nat (int pc + i) < max_pc; |
|
1362 mt_sttp_flatten f ! nat (int pc + i) = (mt_sttp_flatten f ! pc); |
|
1363 check_type (TranslComp.comp G) mxs mxr (OK (mt_sttp_flatten f ! pc)) \<rbrakk> |
|
1364 \<Longrightarrow> wt_instr_altern (Goto i) (comp G) rT (mt_sttp_flatten f) mxs mxr max_pc empty_et pc" |
|
1365 apply (case_tac "(mt_sttp_flatten f ! pc)") |
|
1366 apply (simp add: wt_instr_altern_def eff_def norm_eff_def app_def xcpt_app_def)+ |
|
1367 done |
|
1368 |
|
1369 |
|
1370 |
|
1371 |
|
1372 (* ********************************************************************** *) |
|
1373 |
|
1374 |
|
1375 |
|
1376 lemma bc_mt_corresp_comb_inside: " |
|
1377 \<lbrakk> |
|
1378 bc_mt_corresp bc' f' sttp0 cG rT mxr l1; |
|
1379 bc' = (bc1@bc2@bc3); f'= (f1 \<box> f2 \<box> f3); |
|
1380 l1 = (length bc1); l12 = (length (bc1@bc2)); |
|
1381 bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2); |
|
1382 length bc1 = length (mt_of (f1 sttp0)); |
|
1383 start_sttp_resp f2; start_sttp_resp f3\<rbrakk> |
|
1384 \<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr l12" |
|
1385 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+) |
|
1386 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+) |
|
1387 apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+) |
|
1388 |
|
1389 (* unfold start_sttp_resp and make case distinction *) |
|
1390 apply (simp only: start_sttp_resp_def) |
|
1391 apply (erule_tac Q="start_sttp_resp_cons f2" in disjE) |
|
1392 (* case f2 = comb_nil *) |
|
1393 apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def) |
|
1394 |
|
1395 (* case start_sttp_resp_cons f2 *) |
|
1396 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def) |
|
1397 apply (drule_tac x=sttp1 in spec, simp, erule exE) |
|
1398 apply (intro strip, (erule conjE)+) |
|
1399 |
|
1400 |
|
1401 (* get rid of all check_type info *) |
|
1402 apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))") |
|
1403 apply (subgoal_tac "check_type cG (max_ssize (mt2 @ [Some sttp2])) mxr (OK (Some sttp2))") |
|
1404 apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr |
|
1405 (OK ((mt2 @ mt3 @ [Some sttp3]) ! length mt2))") |
|
1406 apply simp |
|
1407 |
|
1408 |
|
1409 |
|
1410 apply (intro strip, (erule conjE)+) |
|
1411 apply (case_tac "pc < length mt1") |
|
1412 |
|
1413 (* case pc < length mt1 *) |
|
1414 apply (drule spec, drule mp, assumption) |
|
1415 apply assumption |
|
1416 |
|
1417 (* case pc \<ge> length mt1 *) |
|
1418 (* case distinction on start_sttp_resp f3 *) |
|
1419 apply (erule_tac P="f3 = comb_nil" in disjE) |
|
1420 |
|
1421 (* case f3 = comb_nil *) |
|
1422 apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3") apply (erule conjE)+ |
|
1423 apply (subgoal_tac "bc3=[]") |
|
1424 |
|
1425 apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3 |
|
1426 and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" |
|
1427 and mxs="(max_ssize (mt2 @ [(Some sttp2)]))" |
|
1428 and max_pc="(Suc (length mt2))" |
|
1429 in wt_instr_offset) |
|
1430 apply simp |
|
1431 apply (rule HOL.refl)+ |
|
1432 apply (simp (no_asm_simp))+ |
|
1433 |
|
1434 apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append) |
|
1435 apply (rule max_of_list_sublist) |
|
1436 apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast |
|
1437 apply (simp (no_asm_simp)) |
|
1438 apply simp (* subgoal bc3 = [] *) |
|
1439 apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *) |
|
1440 |
|
1441 (* case start_sttp_resp_cons f3 *) |
|
1442 apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE) |
|
1443 apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3 |
|
1444 and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" |
|
1445 and mxs="(max_ssize (mt2 @ [Some sttp2]))" |
|
1446 and max_pc="(Suc (length mt2))" |
|
1447 in wt_instr_offset) |
|
1448 apply (intro strip) |
|
1449 apply (rule_tac bc=bc2 and mt="(mt2 @ [Some sttp2])" |
|
1450 and mxs="(max_ssize (mt2 @ [Some sttp2]))" |
|
1451 and max_pc="(Suc (length mt2))" |
|
1452 in wt_instr_prefix) |
|
1453 |
|
1454 |
|
1455 (* preconditions of wt_instr_prefix *) |
|
1456 apply simp |
|
1457 apply (rule HOL.refl) |
|
1458 apply (simp (no_asm_simp))+ |
|
1459 apply simp+ |
|
1460 (* (some) preconditions of wt_instr_offset *) |
|
1461 apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append) |
|
1462 apply (rule max_of_list_sublist) |
|
1463 apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast |
|
1464 apply (simp (no_asm_simp)) |
|
1465 |
|
1466 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *) |
|
1467 |
|
1468 (* subgoals check_type*) |
|
1469 (* \<dots> ! length mt2 *) |
|
1470 apply simp |
|
1471 |
|
1472 apply (erule_tac P="f3 = comb_nil" in disjE) |
|
1473 |
|
1474 (* -- case f3 = comb_nil *) |
|
1475 apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3") apply (erule conjE)+ |
|
1476 apply simp |
|
1477 apply (rule check_type_mono, assumption) |
|
1478 apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp)) |
|
1479 apply blast |
|
1480 apply simp (* subgoal bc3 = [] *) |
|
1481 apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *) |
|
1482 |
|
1483 |
|
1484 (* -- case start_sttp_resp_cons f3 *) |
|
1485 apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE) |
|
1486 apply (simp (no_asm_simp) add: nth_append) |
|
1487 apply (erule conjE)+ |
|
1488 apply (rule check_type_mono, assumption) |
|
1489 apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp)) |
|
1490 apply blast |
|
1491 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *) |
|
1492 |
|
1493 |
|
1494 (* subgoal check_type \<dots> Some sttp2 *) |
|
1495 apply (simp add: nth_append) |
|
1496 |
|
1497 (* subgoal check_type \<dots> Some sttp1 *) |
|
1498 apply (simp add: nth_append) |
|
1499 apply (erule conjE)+ |
|
1500 apply (case_tac "sttp1", simp) |
|
1501 apply (rule check_type_lower) apply assumption |
|
1502 apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def) |
|
1503 apply (simp (no_asm_simp) add: max_of_list_def max_def) |
|
1504 |
|
1505 (* subgoals \<exists> ... *) |
|
1506 apply (rule surj_pair)+ |
|
1507 done |
|
1508 |
|
1509 |
|
1510 (* ******************** *) |
|
1511 constdefs |
|
1512 contracting :: "(state_type \<Rightarrow> method_type \<times> state_type) \<Rightarrow> bool" |
|
1513 "contracting f == (\<forall> ST LT. |
|
1514 let (ST', LT') = sttp_of (f (ST, LT)) |
|
1515 in (length ST' \<le> length ST \<and> set ST' \<subseteq> set ST \<and> |
|
1516 length LT' = length LT \<and> set LT' \<subseteq> set LT))" |
|
1517 |
|
1518 |
|
1519 (* ### possibly move into HOL *) |
|
1520 lemma set_drop_Suc [rule_format]: "\<forall> xs. set (drop (Suc n) xs) \<subseteq> set (drop n xs)" |
|
1521 apply (induct n) |
|
1522 apply simp |
|
1523 apply (intro strip) |
|
1524 apply (rule list.induct) |
|
1525 apply simp |
|
1526 apply simp apply blast |
|
1527 apply (intro strip) |
|
1528 apply (rule_tac |
|
1529 P="\<lambda> xs. set (drop (Suc (Suc n)) xs) \<subseteq> set (drop (Suc n) xs)" in list.induct) |
|
1530 apply simp+ |
|
1531 done |
|
1532 |
|
1533 lemma set_drop_le [rule_format,simp]: "\<forall> n xs. n \<le> m \<longrightarrow> set (drop m xs) \<subseteq> set (drop n xs)" |
|
1534 apply (induct m) |
|
1535 apply simp |
|
1536 apply (intro strip) |
|
1537 apply (subgoal_tac "na \<le> n \<or> na = Suc n") |
|
1538 apply (erule disjE) |
|
1539 apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption) |
|
1540 apply (rule set_drop_Suc [THEN subset_trans], assumption) |
|
1541 apply auto |
|
1542 done |
|
1543 |
|
1544 lemma set_drop [simp] : "set (drop m xs) \<subseteq> set xs" |
|
1545 apply (rule_tac B="set (drop 0 xs)" in subset_trans) |
|
1546 apply (rule set_drop_le) |
|
1547 apply simp+ |
|
1548 done |
|
1549 |
|
1550 |
|
1551 |
|
1552 lemma contracting_popST [simp]: "contracting (popST n)" |
|
1553 by (simp add: contracting_def popST_def) |
|
1554 |
|
1555 lemma contracting_nochangeST [simp]: "contracting nochangeST" |
|
1556 by (simp add: contracting_def nochangeST_def) |
|
1557 |
|
1558 |
|
1559 lemma check_type_contracting: "\<lbrakk> check_type cG mxs mxr (OK (Some sttp)); contracting f\<rbrakk> |
|
1560 \<Longrightarrow> check_type cG mxs mxr (OK (Some (sttp_of (f sttp))))" |
|
1561 apply (subgoal_tac "\<exists> ST LT. sttp = (ST, LT)", (erule exE)+) |
|
1562 apply (simp add: check_type_simps contracting_def) |
|
1563 apply clarify |
|
1564 apply (drule_tac x=ST in spec, drule_tac x=LT in spec) |
|
1565 apply (case_tac "(sttp_of (f (ST, LT)))") |
|
1566 apply simp |
|
1567 apply (erule conjE)+ |
|
1568 |
|
1569 apply (drule listE_set)+ |
|
1570 apply (rule conjI) |
|
1571 apply (rule_tac x="length a" in exI) apply simp |
|
1572 apply (rule listI) apply simp apply blast |
|
1573 apply (rule listI) apply simp apply blast |
|
1574 apply auto |
|
1575 done |
|
1576 |
|
1577 (* ******************** *) |
|
1578 |
|
1579 |
|
1580 lemma bc_mt_corresp_comb_wt_instr: " |
|
1581 \<lbrakk> bc_mt_corresp bc' f' sttp0 cG rT mxr l1; |
|
1582 bc' = (bc1@[inst]@bc3); f'= (f1 \<box> f2 \<box> f3); |
|
1583 l1 = (length bc1); |
|
1584 length bc1 = length (mt_of (f1 sttp0)); |
|
1585 length (mt_of (f2 (sttp_of (f1 sttp0)))) = 1; |
|
1586 start_sttp_resp_cons f1; start_sttp_resp_cons f2; start_sttp_resp f3; |
|
1587 |
|
1588 check_type cG (max_ssize (mt_sttp_flatten (f' sttp0))) mxr |
|
1589 (OK ((mt_sttp_flatten (f' sttp0)) ! (length bc1))) |
|
1590 \<longrightarrow> |
|
1591 wt_instr_altern inst cG rT |
|
1592 (mt_sttp_flatten (f' sttp0)) |
|
1593 (max_ssize (mt_sttp_flatten (f' sttp0))) |
|
1594 mxr |
|
1595 (Suc (length bc')) |
|
1596 empty_et |
|
1597 (length bc1); |
|
1598 contracting f2 |
|
1599 \<rbrakk> |
|
1600 \<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr (length (bc1@[inst]))" |
|
1601 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+) |
|
1602 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+) |
|
1603 apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+) |
|
1604 |
|
1605 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def |
|
1606 mt_sttp_flatten_def) |
|
1607 |
|
1608 apply (intro strip, (erule conjE)+) |
|
1609 apply (drule mp, assumption)+ apply (erule conjE)+ |
|
1610 apply (drule mp, assumption) |
|
1611 apply (rule conjI) |
|
1612 |
|
1613 (* wt_instr \<dots> *) |
|
1614 apply (intro strip) |
|
1615 apply (case_tac "pc < length mt1") |
|
1616 |
|
1617 (* case pc < length mt1 *) |
|
1618 apply (drule spec, drule mp, assumption) |
|
1619 apply assumption |
|
1620 |
|
1621 (* case pc \<ge> length mt1 *) |
|
1622 apply (subgoal_tac "pc = length mt1") prefer 2 apply arith |
|
1623 apply (simp only:) |
|
1624 apply (simp add: nth_append mt_sttp_flatten_def) |
|
1625 |
|
1626 |
|
1627 (* check_type \<dots> *) |
|
1628 apply (simp add: start_sttp_resp_def) |
|
1629 apply (drule_tac x="sttp0" in spec, simp, erule exE) |
|
1630 apply (drule_tac x="sttp1" in spec, simp, erule exE) |
|
1631 |
|
1632 apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr |
|
1633 (OK (Some (sttp_of (f2 sttp1))))") |
|
1634 |
|
1635 apply (simp only:) |
|
1636 |
|
1637 apply (erule disjE) |
|
1638 (* case f3 = comb_nil *) |
|
1639 apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! Suc (length mt1)) = (Some (snd (f2 sttp1)))")apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3") apply (erule conjE)+ |
|
1640 apply (simp add: nth_append) |
|
1641 apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *) |
|
1642 apply (simp add: nth_append comb_nil_def) (* subgoal \<dots> ! Suc (length mt1) *) |
|
1643 |
|
1644 (* case start_sttp_resp_cons f3 *) |
|
1645 apply (simp add: start_sttp_resp_cons_def) |
|
1646 apply (drule_tac x="sttp2" in spec, simp, erule exE) |
|
1647 apply (simp add: nth_append) |
|
1648 |
|
1649 (* subgoal check_type *) |
|
1650 apply (rule check_type_contracting) |
|
1651 apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! length mt1) = (Some sttp1)") |
|
1652 apply (simp add: nth_append) |
|
1653 apply (simp add: nth_append) |
|
1654 |
|
1655 apply assumption |
|
1656 |
|
1657 (* subgoals *) |
|
1658 apply (rule surj_pair)+ |
|
1659 done |
|
1660 |
|
1661 |
|
1662 lemma compTpExpr_LT_ST_rewr [simp]: "\<lbrakk> |
|
1663 wf_java_prog G; |
|
1664 wf_java_mdecl G C ((mn, pTs), rT, (pns, lvars, blk, res)); |
|
1665 local_env G C (mn, pTs) pns lvars \<turnstile> ex :: T; |
|
1666 is_inited_LT C pTs lvars LT\<rbrakk> |
|
1667 \<Longrightarrow> sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)" |
|
1668 apply (rule compTpExpr_LT_ST) |
|
1669 apply auto |
|
1670 done |
|
1671 |
|
1672 |
|
1673 |
|
1674 |
|
1675 lemma wt_method_compTpExpr_Exprs_corresp: " |
|
1676 \<lbrakk> jmb = (pns,lvars,blk,res); |
|
1677 wf_prog wf_java_mdecl G; |
|
1678 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
1679 E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> |
|
1680 \<Longrightarrow> |
|
1681 (\<forall> ST LT T bc' f'. |
|
1682 E \<turnstile> ex :: T \<longrightarrow> |
|
1683 (is_inited_LT C pTs lvars LT) \<longrightarrow> |
|
1684 bc' = (compExpr jmb ex) \<longrightarrow> |
|
1685 f' = (compTpExpr jmb G ex) |
|
1686 \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc')) |
|
1687 \<and> |
|
1688 (\<forall> ST LT Ts. |
|
1689 E \<turnstile> exs [::] Ts \<longrightarrow> |
|
1690 (is_inited_LT C pTs lvars LT) |
|
1691 \<longrightarrow> bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))" |
|
1692 |
|
1693 apply (rule expr.induct) |
|
1694 |
|
1695 |
|
1696 (* expresssions *) |
|
1697 |
|
1698 (* NewC *) |
|
1699 apply (intro allI impI) |
|
1700 apply (simp only:) |
|
1701 apply (drule NewC_invers) |
|
1702 apply (simp (no_asm_use)) |
|
1703 apply (rule bc_mt_corresp_New) |
|
1704 apply (simp add: comp_is_class) |
|
1705 |
|
1706 (* Cast *) |
|
1707 apply (intro allI impI) |
|
1708 apply (simp only:) |
|
1709 apply (drule Cast_invers) |
|
1710 apply clarify |
|
1711 apply (simp (no_asm_use)) |
|
1712 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) |
|
1713 apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast) |
|
1714 apply (simp add: comp_is_class) |
|
1715 apply (simp only: compTpExpr_LT_ST) |
|
1716 apply blast |
|
1717 apply (simp add: start_sttp_resp_def) |
|
1718 |
|
1719 (* Lit *) |
|
1720 apply (intro allI impI) |
|
1721 apply (simp only:) |
|
1722 apply (drule Lit_invers) |
|
1723 (* apply (simp (no_asm_use)) *) |
|
1724 apply simp |
|
1725 apply (rule bc_mt_corresp_LitPush) |
|
1726 apply assumption |
|
1727 |
|
1728 |
|
1729 (* BinOp *) |
|
1730 |
|
1731 apply (intro allI impI) |
|
1732 apply (simp (no_asm_simp) only:) |
|
1733 apply (drule BinOp_invers, erule exE, (erule conjE)+) |
|
1734 apply (case_tac binop) |
|
1735 apply (simp (no_asm_simp)) |
|
1736 |
|
1737 (* case Eq *) |
|
1738 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0") |
|
1739 prefer 2 |
|
1740 apply (rule bc_mt_corresp_zero) apply (simp add: length_compTpExpr) |
|
1741 apply (simp (no_asm_simp)) |
|
1742 |
|
1743 apply (drule_tac "bc1.0"="[]" and "bc2.0" = "compExpr jmb expr1" |
|
1744 and "f1.0"=comb_nil and "f2.0" = "compTpExpr jmb G expr1" |
|
1745 in bc_mt_corresp_comb_inside) |
|
1746 apply (simp (no_asm_simp))+ |
|
1747 apply blast |
|
1748 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
1749 |
|
1750 apply (drule_tac "bc2.0" = "compExpr jmb expr2" and "f2.0" = "compTpExpr jmb G expr2" |
|
1751 in bc_mt_corresp_comb_inside) |
|
1752 apply (simp (no_asm_simp))+ |
|
1753 apply (simp only: compTpExpr_LT_ST) |
|
1754 apply (simp (no_asm_simp) add: length_compTpExpr) |
|
1755 apply (simp (no_asm_simp)) |
|
1756 apply (simp (no_asm_simp)) |
|
1757 |
|
1758 apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2" |
|
1759 and inst = "Ifcmpeq 3" and "bc3.0" = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]" |
|
1760 and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2" |
|
1761 and "f2.0"="popST 2" and "f3.0"="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]" |
|
1762 in bc_mt_corresp_comb_wt_instr) |
|
1763 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
1764 |
|
1765 (* wt_instr *) |
|
1766 apply (intro strip) |
|
1767 apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr eff_def) |
|
1768 apply (simp (no_asm_simp) add: norm_eff_def) |
|
1769 apply (simp (no_asm_simp) only: int_outside_left nat_int) |
|
1770 apply (simp (no_asm_simp) add: length_compTpExpr) |
|
1771 apply (simp only: compTpExpr_LT_ST)+ |
|
1772 apply (simp add: eff_def norm_eff_def popST_def pushST_def mt_sttp_flatten_def) |
|
1773 apply (case_tac Ta) apply (simp (no_asm_simp)) apply (simp (no_asm_simp)) |
|
1774 apply (rule contracting_popST) (* contracting (popST 2) *) |
|
1775 |
|
1776 apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]" |
|
1777 and "bc2.0" = "[LitPush (Bool False)]" |
|
1778 and "bc3.0" = "[Goto 2, LitPush (Bool True)]" |
|
1779 and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2" |
|
1780 and "f2.0" = "pushST [PrimT Boolean]" |
|
1781 and "f3.0" = "popST (Suc 0) \<box> pushST [PrimT Boolean]" |
|
1782 in bc_mt_corresp_comb_inside) |
|
1783 apply (simp (no_asm_simp))+ |
|
1784 apply (simp add: compTpExpr_LT_ST_rewr popST_def) |
|
1785 apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp)) |
|
1786 apply (simp (no_asm_simp) add: length_compTpExpr) |
|
1787 apply (simp (no_asm_simp)) |
|
1788 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1789 |
|
1790 |
|
1791 apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]" |
|
1792 and inst = "Goto 2" and "bc3.0" = "[LitPush (Bool True)]" |
|
1793 and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]" |
|
1794 and "f2.0"="popST 1" and "f3.0"="pushST [PrimT Boolean]" |
|
1795 in bc_mt_corresp_comb_wt_instr) |
|
1796 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
1797 |
|
1798 (* wt_instr *) |
|
1799 apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr) |
|
1800 apply (simp (no_asm_simp) add: eff_def norm_eff_def) |
|
1801 apply (simp (no_asm_simp) only: int_outside_right nat_int) |
|
1802 apply (simp (no_asm_simp) add: length_compTpExpr) |
|
1803 apply (simp only: compTpExpr_LT_ST)+ |
|
1804 apply (simp add: eff_def norm_eff_def popST_def pushST_def) |
|
1805 apply (rule contracting_popST) (* contracting (popST 1) *) |
|
1806 |
|
1807 apply (drule_tac |
|
1808 "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]" |
|
1809 and "bc2.0" = "[LitPush (Bool True)]" |
|
1810 and "bc3.0" = "[]" |
|
1811 and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> |
|
1812 pushST [PrimT Boolean] \<box> popST (Suc 0)" |
|
1813 and "f2.0" = "pushST [PrimT Boolean]" |
|
1814 and "f3.0" = "comb_nil" |
|
1815 in bc_mt_corresp_comb_inside) |
|
1816 apply (simp (no_asm_simp))+ |
|
1817 apply (simp add: compTpExpr_LT_ST_rewr popST_def) |
|
1818 apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp)) |
|
1819 apply (simp (no_asm_simp) add: length_compTpExpr) |
|
1820 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1821 apply (simp (no_asm_simp)) |
|
1822 |
|
1823 apply simp |
|
1824 |
|
1825 (* case Add *) |
|
1826 apply simp |
|
1827 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast |
|
1828 apply (rule bc_mt_corresp_comb, rule HOL.refl) |
|
1829 apply (simp only: compTpExpr_LT_ST) |
|
1830 apply (simp only: compTpExpr_LT_ST) apply blast |
|
1831 |
|
1832 apply (simp only: compTpExpr_LT_ST) |
|
1833 apply simp |
|
1834 apply (rule bc_mt_corresp_IAdd) |
|
1835 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1836 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1837 |
|
1838 |
|
1839 (* LAcc *) |
|
1840 apply (intro allI impI) |
|
1841 apply (simp only:) |
|
1842 apply (drule LAcc_invers) |
|
1843 apply (frule wf_java_mdecl_length_pTs_pns) |
|
1844 apply clarify |
|
1845 apply (simp add: is_inited_LT_def) |
|
1846 apply (rule bc_mt_corresp_Load) |
|
1847 apply (rule index_in_bounds) apply simp apply assumption |
|
1848 apply (rule inited_LT_at_index_no_err) |
|
1849 apply (rule index_in_bounds) apply simp apply assumption |
|
1850 apply (rule HOL.refl) |
|
1851 |
|
1852 |
|
1853 (* LAss *) |
|
1854 apply (intro allI impI) |
|
1855 apply (simp only:) |
|
1856 apply (drule LAss_invers, erule exE, (erule conjE)+) |
|
1857 apply (drule LAcc_invers) |
|
1858 apply (frule wf_java_mdecl_disjoint_varnames, simp add: disjoint_varnames_def) |
|
1859 apply (frule wf_java_mdecl_length_pTs_pns) |
|
1860 apply clarify |
|
1861 apply (simp (no_asm_use)) |
|
1862 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) |
|
1863 apply (rule_tac "bc1.0"="[Dup]" and "bc2.0"="[Store (index (pns, lvars, blk, res) vname)]" |
|
1864 and "f1.0"="dupST" and "f2.0"="popST (Suc 0)" |
|
1865 in bc_mt_corresp_comb) |
|
1866 apply (simp (no_asm_simp))+ |
|
1867 apply (rule bc_mt_corresp_Dup) |
|
1868 apply (simp only: compTpExpr_LT_ST) |
|
1869 apply (simp add: dupST_def is_inited_LT_def) |
|
1870 apply (rule bc_mt_corresp_Store) |
|
1871 apply (rule index_in_bounds) |
|
1872 apply simp apply assumption |
|
1873 apply (rule sup_loc_update_index, assumption+) |
|
1874 apply simp apply assumption+ |
|
1875 apply (simp add: start_sttp_resp_def) |
|
1876 apply (simp add: start_sttp_resp_def) |
|
1877 |
|
1878 (* FAcc *) |
|
1879 apply (intro allI impI) |
|
1880 apply (simp only:) |
|
1881 apply (drule FAcc_invers) |
|
1882 apply clarify |
|
1883 apply (simp (no_asm_use)) |
|
1884 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) |
|
1885 apply (simp (no_asm_simp)) |
|
1886 apply (rule bc_mt_corresp_Getfield) apply assumption+ |
|
1887 apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) |
|
1888 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1889 |
|
1890 |
|
1891 (* FAss *) |
|
1892 apply (intro allI impI) |
|
1893 apply (simp only:) |
|
1894 apply (drule FAss_invers, erule exE, (erule conjE)+) |
|
1895 apply (drule FAcc_invers) |
|
1896 apply clarify |
|
1897 apply (simp (no_asm_use)) |
|
1898 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast |
|
1899 apply (simp only: compTpExpr_LT_ST) |
|
1900 apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast |
|
1901 apply (simp only: compTpExpr_LT_ST) |
|
1902 apply (rule_tac "bc1.0"="[Dup_x1]" and "bc2.0"="[Putfield vname cname]" in bc_mt_corresp_comb) |
|
1903 apply (simp (no_asm_simp))+ |
|
1904 apply (rule bc_mt_corresp_Dup_x1) |
|
1905 apply (simp (no_asm_simp) add: dup_x1ST_def) |
|
1906 apply (rule bc_mt_corresp_Putfield) apply assumption+ |
|
1907 apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) |
|
1908 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1909 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1910 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1911 |
|
1912 (* Call *) |
|
1913 apply (intro allI impI) |
|
1914 apply (simp only:) |
|
1915 apply (drule Call_invers) |
|
1916 apply clarify |
|
1917 apply (simp (no_asm_use)) |
|
1918 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast |
|
1919 apply (simp only: compTpExpr_LT_ST) |
|
1920 apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast |
|
1921 apply (simp only: compTpExprs_LT_ST) |
|
1922 apply (simp (no_asm_simp)) |
|
1923 apply (rule bc_mt_corresp_Invoke) apply assumption+ |
|
1924 apply (rule wt_class_expr_is_class, assumption+) apply (rule HOL.refl) |
|
1925 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1926 apply (rule start_sttp_resp_comb) |
|
1927 apply (simp (no_asm_simp)) |
|
1928 apply (simp (no_asm_simp) add: start_sttp_resp_def) |
|
1929 |
|
1930 |
|
1931 (* expression lists *) |
|
1932 (* nil *) |
|
1933 |
|
1934 apply (intro allI impI) |
|
1935 apply (drule Nil_invers) |
|
1936 apply simp |
|
1937 |
|
1938 (* cons *) |
|
1939 |
|
1940 apply (intro allI impI) |
|
1941 apply (drule Cons_invers, (erule exE)+, (erule conjE)+) |
|
1942 apply clarify |
|
1943 apply (simp (no_asm_use)) |
|
1944 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast |
|
1945 apply (simp only: compTpExpr_LT_ST) |
|
1946 apply blast |
|
1947 apply simp |
|
1948 |
|
1949 done |
|
1950 |
|
1951 |
|
1952 lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = |
|
1953 wt_method_compTpExpr_Exprs_corresp [THEN conjunct1] |
|
1954 |
|
1955 |
|
1956 (* ********************************************************************** *) |
|
1957 |
|
1958 |
|
1959 |
|
1960 |
|
1961 lemma wt_method_compTpStmt_corresp [rule_format (no_asm)]: " |
|
1962 \<lbrakk> jmb = (pns,lvars,blk,res); |
|
1963 wf_prog wf_java_mdecl G; |
|
1964 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
1965 E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> |
|
1966 \<Longrightarrow> |
|
1967 (\<forall> ST LT T bc' f'. |
|
1968 E \<turnstile> s\<surd> \<longrightarrow> |
|
1969 (is_inited_LT C pTs lvars LT) \<longrightarrow> |
|
1970 bc' = (compStmt jmb s) \<longrightarrow> |
|
1971 f' = (compTpStmt jmb G s) |
|
1972 \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))" |
|
1973 |
|
1974 apply (rule stmt.induct) |
|
1975 |
|
1976 (* Skip *) |
|
1977 apply (intro allI impI) |
|
1978 apply simp |
|
1979 |
|
1980 |
|
1981 (* Expr *) |
|
1982 apply (intro allI impI) |
|
1983 apply (drule Expr_invers, erule exE) |
|
1984 apply (simp (no_asm_simp)) |
|
1985 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp)) |
|
1986 apply (rule wt_method_compTpExpr_corresp) apply assumption+ |
|
1987 apply (simp add: compTpExpr_LT_ST [of _ pns lvars blk res])+ |
|
1988 apply (rule bc_mt_corresp_Pop) |
|
1989 apply (simp add: start_sttp_resp_def) |
|
1990 |
|
1991 |
|
1992 (* Comp *) |
|
1993 apply (intro allI impI) |
|
1994 apply (drule Comp_invers) |
|
1995 apply clarify |
|
1996 apply (simp (no_asm_use)) |
|
1997 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) |
|
1998 apply (simp (no_asm_simp)) apply blast |
|
1999 apply (simp only: compTpStmt_LT_ST) |
|
2000 apply (simp (no_asm_simp)) |
|
2001 |
|
2002 (* Cond *) |
|
2003 apply (intro allI impI) |
|
2004 apply (simp (no_asm_simp) only:) |
|
2005 apply (drule Cond_invers, (erule conjE)+) |
|
2006 apply (simp (no_asm_simp)) |
|
2007 |
|
2008 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0") |
|
2009 prefer 2 |
|
2010 apply (rule bc_mt_corresp_zero) |
|
2011 apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr) |
|
2012 apply (simp (no_asm_simp)) |
|
2013 |
|
2014 apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" |
|
2015 and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) # |
|
2016 compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) # |
|
2017 compStmt jmb stmt2" |
|
2018 and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" |
|
2019 and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box> |
|
2020 nochangeST \<box> compTpStmt jmb G stmt2" |
|
2021 in bc_mt_corresp_comb_inside) |
|
2022 apply (simp (no_asm_simp))+ |
|
2023 apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) |
|
2024 apply (simp (no_asm_simp) add: start_sttp_resp_def)+ |
|
2025 |
|
2026 apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr" |
|
2027 and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) # |
|
2028 compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) # |
|
2029 compStmt jmb stmt2" |
|
2030 and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr" |
|
2031 and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt1 \<box> |
|
2032 nochangeST \<box> compTpStmt jmb G stmt2" |
|
2033 in bc_mt_corresp_comb_inside) |
|
2034 apply (simp (no_asm_simp))+ |
|
2035 apply (simp (no_asm_simp) add: pushST_def) |
|
2036 apply (rule wt_method_compTpExpr_corresp) apply assumption+ |
|
2037 apply (simp (no_asm_simp))+ |
|
2038 |
|
2039 |
|
2040 apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" |
|
2041 and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))" |
|
2042 and "bc3.0" = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) # |
|
2043 compStmt jmb stmt2" |
|
2044 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2" |
|
2045 and "f3.0"="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2" |
|
2046 in bc_mt_corresp_comb_wt_instr) |
|
2047 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
2048 apply (simp (no_asm_simp) add: start_sttp_resp_comb) |
|
2049 |
|
2050 (* wt_instr *) |
|
2051 apply (intro strip) |
|
2052 apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" |
|
2053 and ST=ST and LT=LT |
|
2054 in wt_instr_Ifcmpeq) |
|
2055 apply (simp (no_asm_simp)) |
|
2056 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2057 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2058 (* current pc *) |
|
2059 apply (simp add: length_compTpExpr pushST_def) |
|
2060 apply (simp only: compTpExpr_LT_ST) |
|
2061 (* Suc pc *) |
|
2062 apply (simp add: length_compTpExpr pushST_def) |
|
2063 apply (simp add: popST_def start_sttp_resp_comb) |
|
2064 (* jump goal *) |
|
2065 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2066 apply (simp add: length_compTpExpr pushST_def) |
|
2067 apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt) |
|
2068 apply (simp only: compTpStmt_LT_ST) |
|
2069 apply (simp add: nochangeST_def) |
|
2070 (* check_type *) |
|
2071 apply (subgoal_tac " |
|
2072 (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = |
|
2073 (Some (PrimT Boolean # PrimT Boolean # ST, LT))") |
|
2074 apply (simp only:) |
|
2075 apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) |
|
2076 apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr) |
|
2077 apply (simp (no_asm_simp) add: length_compTpExpr pushST_def) |
|
2078 apply (simp only: compTpExpr_LT_ST_rewr) |
|
2079 (* contracting\<dots> *) |
|
2080 apply (rule contracting_popST) |
|
2081 |
|
2082 apply (drule_tac |
|
2083 "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ |
|
2084 [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] " |
|
2085 and "bc2.0" = "compStmt jmb stmt1" |
|
2086 and "bc3.0"="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2" |
|
2087 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" |
|
2088 and "f2.0" = "compTpStmt jmb G stmt1" |
|
2089 and "f3.0"="nochangeST \<box> compTpStmt jmb G stmt2" |
|
2090 in bc_mt_corresp_comb_inside) |
|
2091 apply (simp (no_asm_simp))+ |
|
2092 apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST) |
|
2093 apply (simp only: compTpExpr_LT_ST) |
|
2094 apply (simp (no_asm_simp)) |
|
2095 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
2096 |
|
2097 |
|
2098 apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1" |
|
2099 and inst = "Goto (1 + int (length (compStmt jmb stmt2)))" |
|
2100 and "bc3.0" = "compStmt jmb stmt2" |
|
2101 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> |
|
2102 compTpStmt jmb G stmt1" |
|
2103 and "f2.0" = "nochangeST" |
|
2104 and "f3.0"="compTpStmt jmb G stmt2" |
|
2105 in bc_mt_corresp_comb_wt_instr) |
|
2106 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ |
|
2107 apply (intro strip) |
|
2108 apply (rule wt_instr_Goto) |
|
2109 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2110 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2111 (* \<dots> ! nat (int pc + i) = \<dots> ! pc *) |
|
2112 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2113 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) |
|
2114 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) |
|
2115 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2116 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) |
|
2117 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2118 apply (simp only:) |
|
2119 apply (simp add: length_compTpExpr length_compTpStmt) |
|
2120 apply (rule contracting_nochangeST) |
|
2121 |
|
2122 |
|
2123 apply (drule_tac |
|
2124 "bc1.0"= "[LitPush (Bool False)] @ compExpr jmb expr @ |
|
2125 [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ |
|
2126 compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]" |
|
2127 and "bc2.0" = "compStmt jmb stmt2" |
|
2128 and "bc3.0"="[]" |
|
2129 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> |
|
2130 compTpStmt jmb G stmt1 \<box> nochangeST" |
|
2131 and "f2.0" = "compTpStmt jmb G stmt2" |
|
2132 and "f3.0"="comb_nil" |
|
2133 in bc_mt_corresp_comb_inside) |
|
2134 apply (simp (no_asm_simp))+ |
|
2135 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST) |
|
2136 apply (simp only: compTpExpr_LT_ST) |
|
2137 apply (simp (no_asm_simp)) |
|
2138 apply (simp only: compTpStmt_LT_ST) |
|
2139 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ |
|
2140 |
|
2141 apply simp |
|
2142 |
|
2143 |
|
2144 (* Loop *) |
|
2145 apply (intro allI impI) |
|
2146 apply (simp (no_asm_simp) only:) |
|
2147 apply (drule Loop_invers, (erule conjE)+) |
|
2148 apply (simp (no_asm_simp)) |
|
2149 |
|
2150 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0") |
|
2151 prefer 2 |
|
2152 apply (rule bc_mt_corresp_zero) |
|
2153 apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr) |
|
2154 apply (simp (no_asm_simp)) |
|
2155 |
|
2156 apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" |
|
2157 and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) # |
|
2158 compStmt jmb stmt @ |
|
2159 [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" |
|
2160 and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" |
|
2161 and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST" |
|
2162 in bc_mt_corresp_comb_inside) |
|
2163 apply (simp (no_asm_simp))+ |
|
2164 apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) |
|
2165 apply (simp (no_asm_simp) add: start_sttp_resp_def)+ |
|
2166 |
|
2167 apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr" |
|
2168 and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt))) # |
|
2169 compStmt jmb stmt @ |
|
2170 [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" |
|
2171 and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr" |
|
2172 and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST" |
|
2173 in bc_mt_corresp_comb_inside) |
|
2174 apply (simp (no_asm_simp))+ |
|
2175 apply (simp (no_asm_simp) add: pushST_def) |
|
2176 apply (rule wt_method_compTpExpr_corresp) apply assumption+ |
|
2177 apply (simp (no_asm_simp))+ |
|
2178 |
|
2179 |
|
2180 apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" |
|
2181 and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))" |
|
2182 and "bc3.0" = "compStmt jmb stmt @ |
|
2183 [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" |
|
2184 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2" |
|
2185 and "f3.0"="compTpStmt jmb G stmt \<box> nochangeST" |
|
2186 in bc_mt_corresp_comb_wt_instr) |
|
2187 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
2188 apply (simp (no_asm_simp) add: start_sttp_resp_comb) |
|
2189 |
|
2190 (* wt_instr *) |
|
2191 apply (intro strip) |
|
2192 apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" |
|
2193 and ST=ST and LT=LT |
|
2194 in wt_instr_Ifcmpeq) |
|
2195 apply (simp (no_asm_simp)) |
|
2196 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2197 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2198 (* current pc *) |
|
2199 apply (simp add: length_compTpExpr pushST_def) |
|
2200 apply (simp only: compTpExpr_LT_ST) |
|
2201 (* Suc pc *) |
|
2202 apply (simp add: length_compTpExpr pushST_def) |
|
2203 apply (simp add: popST_def start_sttp_resp_comb) |
|
2204 (* jump goal *) |
|
2205 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp)) |
|
2206 apply (simp add: length_compTpExpr pushST_def) |
|
2207 apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt) |
|
2208 apply (simp only: compTpStmt_LT_ST) |
|
2209 apply (simp add: nochangeST_def) |
|
2210 (* check_type *) |
|
2211 apply (subgoal_tac " |
|
2212 (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = |
|
2213 (Some (PrimT Boolean # PrimT Boolean # ST, LT))") |
|
2214 apply (simp only:) |
|
2215 apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) |
|
2216 apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr) |
|
2217 apply (simp (no_asm_simp) add: length_compTpExpr pushST_def) |
|
2218 apply (simp only: compTpExpr_LT_ST_rewr) |
|
2219 (* contracting\<dots> *) |
|
2220 apply (rule contracting_popST) |
|
2221 |
|
2222 apply (drule_tac |
|
2223 "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ |
|
2224 [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] " |
|
2225 and "bc2.0" = "compStmt jmb stmt" |
|
2226 and "bc3.0"="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" |
|
2227 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" |
|
2228 and "f2.0" = "compTpStmt jmb G stmt" |
|
2229 and "f3.0"="nochangeST" |
|
2230 in bc_mt_corresp_comb_inside) |
|
2231 apply (simp (no_asm_simp))+ |
|
2232 apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST) |
|
2233 apply (simp only: compTpExpr_LT_ST) |
|
2234 apply (simp (no_asm_simp)) |
|
2235 apply (simp (no_asm_simp) add: length_compTpExpr)+ |
|
2236 |
|
2237 |
|
2238 apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt" |
|
2239 and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))" |
|
2240 and "bc3.0" = "[]" |
|
2241 and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> |
|
2242 compTpStmt jmb G stmt" |
|
2243 and "f2.0" = "nochangeST" |
|
2244 and "f3.0"="comb_nil" |
|
2245 in bc_mt_corresp_comb_wt_instr) |
|
2246 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ |
|
2247 apply (intro strip) |
|
2248 apply (rule wt_instr_Goto) |
|
2249 apply (simp (no_asm_simp) add: nat_canonify) |
|
2250 apply (simp (no_asm_simp) add: nat_canonify) |
|
2251 (* \<dots> ! nat (int pc + i) = \<dots> ! pc *) |
|
2252 apply (simp (no_asm_simp) add: nat_canonify) |
|
2253 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) |
|
2254 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) |
|
2255 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2256 apply (simp (no_asm_simp) only: int_outside_right nat_int) |
|
2257 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) |
|
2258 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2259 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def) |
|
2260 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt) |
|
2261 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2262 |
|
2263 apply (simp add: length_compTpExpr length_compTpStmt) (* check_type *) |
|
2264 apply (simp add: pushST_def popST_def compTpExpr_LT_ST compTpStmt_LT_ST) |
|
2265 apply (rule contracting_nochangeST) |
|
2266 apply simp |
|
2267 |
|
2268 done |
|
2269 |
|
2270 |
|
2271 (**********************************************************************************) |
|
2272 |
|
2273 |
|
2274 |
|
2275 lemma wt_method_compTpInit_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); |
|
2276 wf_java_mdecl G C ((mn, pTs), rT, jmb); mxr = length LT; |
|
2277 length LT = (length pns) + (length lvars) + 1; vn \<in> set (map fst lvars); |
|
2278 bc = (compInit jmb (vn,ty)); f = (compTpInit jmb (vn,ty)); |
|
2279 is_type G ty \<rbrakk> |
|
2280 \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)" |
|
2281 apply (simp add: compInit_def compTpInit_def split_beta) |
|
2282 apply (rule_tac "bc1.0"="[load_default_val ty]" and "bc2.0"="[Store (index jmb vn)]" |
|
2283 in bc_mt_corresp_comb) |
|
2284 apply simp+ |
|
2285 apply (simp add: load_default_val_def) |
|
2286 apply (rule typeof_default_val [THEN exE]) |
|
2287 |
|
2288 apply (rule bc_mt_corresp_LitPush_CT) apply assumption |
|
2289 apply (simp add: comp_is_type) |
|
2290 apply (simp add: pushST_def) |
|
2291 apply (rule bc_mt_corresp_Store_init) |
|
2292 apply simp |
|
2293 apply (rule index_length_lvars [THEN conjunct2]) |
|
2294 apply auto |
|
2295 done |
|
2296 |
|
2297 |
|
2298 lemma wt_method_compTpInitLvars_corresp_aux [rule_format (no_asm)]: " |
|
2299 \<forall> lvars_pre lvars0 ST LT. |
|
2300 jmb = (pns,lvars0,blk,res) \<and> |
|
2301 lvars0 = (lvars_pre @ lvars) \<and> |
|
2302 length LT = (length pns) + (length lvars0) + 1 \<and> |
|
2303 wf_java_mdecl G C ((mn, pTs), rT, jmb) |
|
2304 \<longrightarrow> bc_mt_corresp (compInitLvars jmb lvars) (compTpInitLvars jmb lvars) (ST, LT) (comp G) rT |
|
2305 (length LT) (length (compInitLvars jmb lvars))" |
|
2306 apply (induct lvars) |
|
2307 apply (simp add: compInitLvars_def) |
|
2308 |
|
2309 apply (intro strip, (erule conjE)+) |
|
2310 apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)") |
|
2311 prefer 2 apply (simp (no_asm_simp)) |
|
2312 apply ((erule exE)+, simp (no_asm_simp)) |
|
2313 apply (drule_tac x="lvars_pre @ [a]" in spec) |
|
2314 apply (drule_tac x="lvars0" in spec) |
|
2315 apply (simp (no_asm_simp) add: compInitLvars_def) |
|
2316 apply (rule_tac "bc1.0"="compInit jmb a" and "bc2.0"="compInitLvars jmb list" |
|
2317 in bc_mt_corresp_comb) |
|
2318 apply (simp (no_asm_simp) add: compInitLvars_def)+ |
|
2319 |
|
2320 apply (rule_tac vn=vn and ty=ty in wt_method_compTpInit_corresp) |
|
2321 apply assumption+ |
|
2322 apply (simp (no_asm_simp))+ |
|
2323 apply (simp add: wf_java_mdecl_def) (* is_type G ty *) |
|
2324 apply (simp add: compTpInit_def storeST_def pushST_def) |
|
2325 apply simp |
|
2326 done |
|
2327 |
|
2328 |
|
2329 lemma wt_method_compTpInitLvars_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); |
|
2330 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
2331 length LT = (length pns) + (length lvars) + 1; mxr = (length LT); |
|
2332 bc = (compInitLvars jmb lvars); f= (compTpInitLvars jmb lvars) \<rbrakk> |
|
2333 \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)" |
|
2334 apply (simp only:) |
|
2335 apply (subgoal_tac "bc_mt_corresp (compInitLvars (pns, lvars, blk, res) lvars) |
|
2336 (compTpInitLvars (pns, lvars, blk, res) lvars) (ST, LT) (TranslComp.comp G) rT |
|
2337 (length LT) (length (compInitLvars (pns, lvars, blk, res) lvars))") |
|
2338 apply simp |
|
2339 apply (rule_tac lvars_pre="[]" in wt_method_compTpInitLvars_corresp_aux) |
|
2340 apply auto |
|
2341 done |
|
2342 |
|
2343 |
|
2344 (**********************************************************************************) |
|
2345 |
|
2346 |
|
2347 |
|
2348 lemma wt_method_comp_wo_return: "\<lbrakk> wf_prog wf_java_mdecl G; |
|
2349 wf_java_mdecl G C ((mn, pTs), rT, jmb); |
|
2350 bc = compInitLvars jmb lvars @ compStmt jmb blk @ compExpr jmb res; |
|
2351 jmb = (pns,lvars,blk,res); |
|
2352 f = (compTpInitLvars jmb lvars \<box> compTpStmt jmb G blk \<box> compTpExpr jmb G res); |
|
2353 sttp = (start_ST, start_LT C pTs (length lvars)); |
|
2354 li = (length (inited_LT C pTs lvars)) |
|
2355 \<rbrakk> |
|
2356 \<Longrightarrow> bc_mt_corresp bc f sttp (comp G) rT li (length bc)" |
|
2357 apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> |
|
2358 (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))") |
|
2359 apply (erule exE, (erule conjE)+)+ |
|
2360 apply (simp only:) |
|
2361 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+ |
|
2362 |
|
2363 (* InitLvars *) |
|
2364 apply (rule wt_method_compTpInitLvars_corresp) |
|
2365 apply assumption+ |
|
2366 apply (simp only:) |
|
2367 apply (simp (no_asm_simp) add: start_LT_def) |
|
2368 apply (rule wf_java_mdecl_length_pTs_pns, assumption) |
|
2369 apply (simp (no_asm_simp) only: start_LT_def) |
|
2370 apply (simp (no_asm_simp) add: inited_LT_def)+ |
|
2371 |
|
2372 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+ |
|
2373 apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST) |
|
2374 |
|
2375 (* stmt *) |
|
2376 apply (simp only: compTpInitLvars_LT_ST) |
|
2377 apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))") |
|
2378 prefer 2 apply (simp (no_asm_simp) add: inited_LT_def) |
|
2379 apply (simp only:) |
|
2380 apply (rule_tac s=blk in wt_method_compTpStmt_corresp) |
|
2381 apply assumption+ |
|
2382 apply (simp only:)+ |
|
2383 apply (simp (no_asm_simp) add: is_inited_LT_def) |
|
2384 apply (simp only:)+ |
|
2385 |
|
2386 (* expr *) |
|
2387 apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST is_inited_LT_def) |
|
2388 apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))") |
|
2389 prefer 2 apply (simp (no_asm_simp) add: inited_LT_def) |
|
2390 apply (simp only:) |
|
2391 apply (rule_tac ex=res in wt_method_compTpExpr_corresp) |
|
2392 apply assumption+ |
|
2393 apply (simp only:)+ |
|
2394 apply (simp (no_asm_simp) add: is_inited_LT_def) |
|
2395 apply (simp only:)+ |
|
2396 |
|
2397 (* start_sttp_resp *) |
|
2398 apply (simp add: start_sttp_resp_comb)+ |
|
2399 |
|
2400 (* subgoal *) |
|
2401 apply (simp add: wf_java_mdecl_def local_env_def) |
|
2402 done |
|
2403 |
|
2404 |
|
2405 (**********************************************************************************) |
|
2406 |
|
2407 |
|
2408 |
|
2409 lemma check_type_start: "\<lbrakk> wf_mhead cG (mn, pTs) rT; is_class cG C\<rbrakk> |
|
2410 \<Longrightarrow> check_type cG (length start_ST) (Suc (length pTs + mxl)) |
|
2411 (OK (Some (start_ST, start_LT C pTs mxl)))" |
|
2412 apply (simp add: check_type_def wf_mhead_def start_ST_def start_LT_def) |
|
2413 apply (simp add: check_type_simps) |
|
2414 apply (simp only: list_def) |
|
2415 apply (auto simp: err_def) |
|
2416 apply (subgoal_tac "set (replicate mxl Err) \<subseteq> {Err}") |
|
2417 apply blast |
|
2418 apply (rule subset_replicate) |
|
2419 done |
|
2420 |
|
2421 |
|
2422 lemma wt_method_comp_aux: "\<lbrakk> bc' = bc @ [Return]; f' = (f \<box> nochangeST); |
|
2423 bc_mt_corresp bc f sttp0 cG rT (1+length pTs+mxl) (length bc); |
|
2424 start_sttp_resp_cons f'; |
|
2425 sttp0 = (start_ST, start_LT C pTs mxl); |
|
2426 mxs = max_ssize (mt_of (f' sttp0)); |
|
2427 wf_mhead cG (mn, pTs) rT; is_class cG C; |
|
2428 sttp_of (f sttp0) = (T # ST, LT); |
|
2429 |
|
2430 check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT))) \<longrightarrow> |
|
2431 wt_instr_altern Return cG rT (mt_of (f' sttp0)) mxs (1+length pTs+mxl) |
|
2432 (Suc (length bc)) empty_et (length bc) |
|
2433 \<rbrakk> |
|
2434 \<Longrightarrow> wt_method_altern cG C pTs rT mxs mxl bc' empty_et (mt_of (f' sttp0))" |
|
2435 apply (subgoal_tac "check_type cG (length start_ST) (Suc (length pTs + mxl)) |
|
2436 (OK (Some (start_ST, start_LT C pTs mxl)))") |
|
2437 apply (subgoal_tac "check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT)))") |
|
2438 |
|
2439 apply (simp add: wt_method_altern_def) |
|
2440 |
|
2441 (* length (.. f ..) = length bc *) |
|
2442 apply (rule conjI) |
|
2443 apply (simp add: bc_mt_corresp_def split_beta) |
|
2444 |
|
2445 (* check_bounded *) |
|
2446 apply (rule conjI) |
|
2447 apply (simp add: bc_mt_corresp_def split_beta check_bounded_def) |
|
2448 apply (erule conjE)+ |
|
2449 apply (intro strip) |
|
2450 apply (subgoal_tac "pc < (length bc) \<or> pc = length bc") |
|
2451 apply (erule disjE) |
|
2452 (* case pc < length bc *) |
|
2453 apply (subgoal_tac "(bc' ! pc) = (bc ! pc)") |
|
2454 apply (simp add: wt_instr_altern_def eff_def) |
|
2455 (* subgoal *) |
|
2456 apply (simp add: nth_append) |
|
2457 (* case pc = length bc *) |
|
2458 apply (subgoal_tac "(bc' ! pc) = Return") |
|
2459 apply (simp add: wt_instr_altern_def) |
|
2460 (* subgoal *) |
|
2461 apply (simp add: nth_append) |
|
2462 |
|
2463 (* subgoal pc < length bc \<or> pc = length bc *) |
|
2464 apply arith |
|
2465 |
|
2466 (* wt_start *) |
|
2467 apply (rule conjI) |
|
2468 apply (simp add: wt_start_def start_sttp_resp_cons_def split_beta) |
|
2469 apply (drule_tac x=sttp0 in spec) apply (erule exE) |
|
2470 apply (simp add: mt_sttp_flatten_def start_ST_def start_LT_def) |
|
2471 |
|
2472 (* wt_instr *) |
|
2473 apply (intro strip) |
|
2474 apply (subgoal_tac "pc < (length bc) \<or> pc = length bc") |
|
2475 apply (erule disjE) |
|
2476 |
|
2477 (* pc < (length bc) *) |
|
2478 apply (simp (no_asm_use) add: bc_mt_corresp_def mt_sttp_flatten_def split_beta) |
|
2479 apply (erule conjE)+ |
|
2480 apply (drule mp, assumption)+ |
|
2481 apply (erule conjE)+ |
|
2482 apply (drule spec, drule mp, assumption) |
|
2483 apply (simp add: nth_append) |
|
2484 apply (simp (no_asm_simp) add: comb_def split_beta nochangeST_def) |
|
2485 |
|
2486 (* pc = length bc *) |
|
2487 apply (simp add: nth_append) |
|
2488 |
|
2489 (* subgoal pc < (length bc) \<or> pc = length bc *) |
|
2490 apply arith |
|
2491 |
|
2492 (* subgoals *) |
|
2493 apply (simp (no_asm_use) add: bc_mt_corresp_def split_beta) |
|
2494 apply (subgoal_tac "check_type cG (length (fst sttp0)) (Suc (length pTs + mxl)) |
|
2495 (OK (Some sttp0))") |
|
2496 apply ((erule conjE)+, drule mp, assumption) |
|
2497 apply (simp add: nth_append) |
|
2498 apply (simp (no_asm_simp) add: comb_def nochangeST_def split_beta) |
|
2499 apply (simp (no_asm_simp)) |
|
2500 |
|
2501 apply (rule check_type_start, assumption+) |
|
2502 done |
|
2503 |
|
2504 |
|
2505 lemma wt_instr_Return: "\<lbrakk>fst f ! pc = Some (T # ST, LT); (G \<turnstile> T \<preceq> rT); pc < max_pc; |
|
2506 check_type (TranslComp.comp G) mxs mxr (OK (Some (T # ST, LT))) |
|
2507 \<rbrakk> |
|
2508 \<Longrightarrow> wt_instr_altern Return (comp G) rT (mt_of f) mxs mxr max_pc empty_et pc" |
|
2509 apply (case_tac "(mt_of f ! pc)") |
|
2510 apply (simp add: wt_instr_altern_def eff_def norm_eff_def app_def)+ |
|
2511 apply (drule sym) |
|
2512 apply (simp add: comp_widen xcpt_app_def) |
|
2513 done |
|
2514 |
|
2515 |
|
2516 theorem wt_method_comp: " |
|
2517 \<lbrakk> wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths; |
|
2518 jmdcl = ((mn,pTs), rT, jmb); |
|
2519 mt = (compTpMethod G C jmdcl); |
|
2520 (mxs, mxl, bc, et) = mtd_mb (compMethod G C jmdcl) \<rbrakk> |
|
2521 \<Longrightarrow> wt_method (comp G) C pTs rT mxs mxl bc et mt" |
|
2522 |
|
2523 (* show statement for wt_method_altern *) |
|
2524 apply (rule wt_method_altern_wt_method) |
|
2525 |
|
2526 apply (subgoal_tac "wf_java_mdecl G C jmdcl") |
|
2527 apply (subgoal_tac "wf_mhead G (mn, pTs) rT") |
|
2528 apply (subgoal_tac "is_class G C") |
|
2529 apply (subgoal_tac "\<forall> jmb. \<exists> pns lvars blk res. jmb = (pns, lvars, blk, res)") |
|
2530 apply (drule_tac x=jmb in spec, (erule exE)+) |
|
2531 apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> |
|
2532 (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))") |
|
2533 apply (erule exE, (erule conjE)+)+ |
|
2534 apply (simp add: compMethod_def compTpMethod_def split_beta) |
|
2535 apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux) |
|
2536 |
|
2537 (* bc *) |
|
2538 apply (simp only: append_assoc [THEN sym]) |
|
2539 |
|
2540 (* comb *) |
|
2541 apply (simp only: comb_assoc [THEN sym]) |
|
2542 |
|
2543 (* bc_corresp *) |
|
2544 apply (rule wt_method_comp_wo_return) |
|
2545 apply assumption+ |
|
2546 apply (simp (no_asm_use) only: append_assoc) |
|
2547 apply (rule HOL.refl) |
|
2548 apply (simp (no_asm_simp))+ |
|
2549 apply (simp (no_asm_simp) add: inited_LT_def) |
|
2550 |
|
2551 (* start_sttp_resp *) |
|
2552 apply (simp add: start_sttp_resp_cons_comb_cons_r)+ |
|
2553 |
|
2554 (* wf_mhead / is_class *) |
|
2555 apply (simp add: wf_mhead_def comp_is_type) |
|
2556 apply (simp add: comp_is_class) |
|
2557 |
|
2558 (* sttp_of .. = (T # ST, LT) *) |
|
2559 apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST compTpExpr_LT_ST compTpStmt_LT_ST is_inited_LT_def) |
|
2560 apply (subgoal_tac "(snd (compTpInitLvars (pns, lvars, blk, res) lvars |
|
2561 (start_ST, start_LT C pTs (length lvars)))) |
|
2562 = (start_ST, inited_LT C pTs lvars)") |
|
2563 prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption |
|
2564 apply (simp only:) |
|
2565 apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk |
|
2566 (start_ST, inited_LT C pTs lvars))) |
|
2567 = (start_ST, inited_LT C pTs lvars)") |
|
2568 prefer 2 apply (erule conjE)+ |
|
2569 apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+ |
|
2570 apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def) |
|
2571 apply (simp only:) |
|
2572 apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+ |
|
2573 apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def) |
|
2574 |
|
2575 |
|
2576 (* Return *) |
|
2577 apply (intro strip) |
|
2578 apply (rule_tac T=T and ST=start_ST and LT="inited_LT C pTs lvars" in wt_instr_Return) |
|
2579 apply (simp (no_asm_simp) add: nth_append |
|
2580 length_compTpInitLvars length_compTpStmt length_compTpExpr) |
|
2581 apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST compTpExpr_LT_ST |
|
2582 nochangeST_def) |
|
2583 apply (simp only: is_inited_LT_def compTpStmt_LT_ST compTpExpr_LT_ST) |
|
2584 apply (simp (no_asm_simp))+ |
|
2585 apply simp |
|
2586 |
|
2587 (* subgoal \<exists> E. \<dots> *) |
|
2588 apply (simp add: wf_java_mdecl_def local_env_def) |
|
2589 |
|
2590 (* subgoal jmb = (\<dots>) *) |
|
2591 apply (simp only: split_paired_All, simp) |
|
2592 |
|
2593 (* subgoal is_class / wf_mhead / wf_java_mdecl *) |
|
2594 apply (rule methd [THEN conjunct2]) apply assumption+ apply (simp only:) |
|
2595 apply (rule wf_prog_wf_mhead, assumption+) apply (simp only:) |
|
2596 apply (rule wf_java_prog_wf_java_mdecl, assumption+) |
|
2597 |
|
2598 done |
|
2599 |
|
2600 |
|
2601 (**********************************************************************************) |
|
2602 |
|
2603 |
|
2604 |
|
2605 lemma comp_set_ms: "(C, D, fs, cms)\<in>set (comp G) |
|
2606 \<Longrightarrow> \<exists> ms. (C, D, fs, ms) \<in>set G \<and> cms = map (compMethod G C) ms" |
|
2607 by (auto simp: comp_def compClass_def) |
|
2608 |
|
2609 lemma method_body_source: "\<lbrakk> wf_prog wf_mb G; is_class G C; method (comp G, C) sig = Some (D, rT, cmb) \<rbrakk> |
|
2610 \<Longrightarrow> (\<exists> mb. method (G, C) sig = Some (D, rT, mb))" |
|
2611 apply (simp add: comp_method_eq comp_method_result_def) |
|
2612 apply (case_tac "method (G, C) sig") |
|
2613 apply auto |
|
2614 done |
|
2615 |
|
2616 |
|
2617 (* MAIN THEOREM: |
|
2618 Methodtype computed by comp is correct for bytecode generated by compTp *) |
|
2619 theorem wt_prog_comp: "wf_java_prog G \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)" |
|
2620 apply (simp add: wf_prog_def) |
|
2621 apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def) |
|
2622 apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def) |
|
2623 apply (simp add: comp_unique comp_wf_syscls wf_cdecl_def) |
|
2624 apply clarify |
|
2625 apply (frule comp_set_ms) |
|
2626 apply clarify |
|
2627 apply (drule bspec, assumption) |
|
2628 apply (simp add: comp_wf_fdecl) |
|
2629 apply (simp add: wf_mdecl_def) |
|
2630 |
|
2631 apply (rule conjI) |
|
2632 apply (rule ballI) |
|
2633 apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") prefer 2 apply (case_tac x, simp) |
|
2634 apply (erule exE)+ |
|
2635 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
|
2636 apply (erule conjE)+ |
|
2637 apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp |
|
2638 apply (rule conjI) |
|
2639 apply (simp add: comp_wf_mhead) |
|
2640 apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp) |
|
2641 apply assumption+ |
|
2642 apply simp |
|
2643 apply (simp (no_asm_simp) add: compTp_def) |
|
2644 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
|
2645 apply (frule WellForm.methd) apply assumption+ |
|
2646 apply simp |
|
2647 apply simp |
|
2648 apply (simp add: compMethod_def split_beta) |
|
2649 |
|
2650 apply (rule conjI) |
|
2651 apply (rule unique_map_fst [THEN iffD1]) |
|
2652 apply (simp (no_asm_simp) add: compMethod_def split_beta) apply simp |
|
2653 |
|
2654 apply clarify |
|
2655 apply (rule conjI) apply (simp add: comp_is_class) |
|
2656 apply (rule conjI) apply (simp add: comp_subcls) |
|
2657 apply (simp add: compMethod_def split_beta) |
|
2658 apply (intro strip) |
|
2659 apply (drule_tac x=x in bspec, assumption, drule_tac x="D'" in spec, drule_tac x="rT'" in spec) |
|
2660 apply (erule exE) |
|
2661 |
|
2662 apply (frule method_body_source) apply assumption+ |
|
2663 apply (drule mp, assumption) |
|
2664 apply (simp add: comp_widen) |
|
2665 done |
|
2666 |
|
2667 |
|
2668 |
|
2669 |
|
2670 (**********************************************************************************) |
|
2671 |
|
2672 declare split_paired_All [simp add] |
|
2673 declare split_paired_Ex [simp add] |
|
2674 |
|
2675 |
|
2676 end |