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