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