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