|
1 (* Title: HOL/MicroJava/BV/BVSpecTypeSafe.ML |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def, |
|
8 correct_frame_def,wt_instr_def]; |
|
9 |
|
10 Goalw [correct_state_def,Let_def,correct_frame_def,split_def] |
|
11 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
12 \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ |
|
13 \ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \ |
|
14 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; |
|
15 by (Asm_full_simp_tac 1); |
|
16 by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1); |
|
17 qed "wt_jvm_prog_impl_wt_instr_cor"; |
|
18 |
|
19 |
|
20 Delsimps [split_paired_All]; |
|
21 |
|
22 |
|
23 (******* LS *******) |
|
24 |
|
25 Goal |
|
26 "\\<lbrakk> wf_prog wt G; \ |
|
27 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
28 \ ins!pc = LS(Load idx); \ |
|
29 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
30 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
31 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
32 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
33 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup, |
|
34 approx_loc_imp_approx_loc_sup] |
|
35 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
36 qed "Load_correct"; |
|
37 |
|
38 |
|
39 Goal |
|
40 "\\<lbrakk> wf_prog wt G; \ |
|
41 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
42 \ ins!pc = LS(Store idx); \ |
|
43 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
44 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
45 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
46 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
47 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
48 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)] |
|
49 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
50 qed "Store_correct"; |
|
51 |
|
52 Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer"; |
|
53 by(Simp_tac 1); |
|
54 qed "conf_Intg_Integer"; |
|
55 AddIffs [conf_Intg_Integer]; |
|
56 |
|
57 Goal |
|
58 "\\<lbrakk> wf_prog wt G; \ |
|
59 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
60 \ ins!pc = LS(Bipush i); \ |
|
61 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
62 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
63 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
64 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
65 by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] |
|
66 addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1); |
|
67 qed "Bipush_correct"; |
|
68 |
|
69 Goal "G \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>C. T = Class C))"; |
|
70 be widen.induct 1; |
|
71 by(Auto_tac); |
|
72 by(rename_tac "R" 1); |
|
73 by(exhaust_tac "R" 1); |
|
74 by(Auto_tac); |
|
75 val lemma = result(); |
|
76 |
|
77 Goal "G \\<turnstile> NT \\<preceq> T = (T=NT | (\\<exists>C. T = Class C))"; |
|
78 by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1); |
|
79 qed "NT_subtype_conv"; |
|
80 |
|
81 Goal |
|
82 "\\<lbrakk> wf_prog wt G; \ |
|
83 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
84 \ ins!pc = LS Aconst_null; \ |
|
85 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
86 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
87 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
88 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
89 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] |
|
90 addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1); |
|
91 qed "Aconst_null_correct"; |
|
92 |
|
93 |
|
94 Goal |
|
95 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
96 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
97 \ ins!pc = LS ls_com; \ |
|
98 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
99 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
100 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
101 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
102 ba 1; |
|
103 ba 1; |
|
104 by(rewtac wt_jvm_prog_def); |
|
105 by (exhaust_tac "ls_com" 1); |
|
106 by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct]))); |
|
107 qed "LS_correct"; |
|
108 |
|
109 |
|
110 (**** CH ****) |
|
111 |
|
112 Goalw [cast_ok_def] |
|
113 "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G (Class C) h v ; G\\<turnstile>(Class C)\\<preceq>T'; is_class G C \\<rbrakk> \ |
|
114 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'"; |
|
115 be disjE 1; |
|
116 by (Clarify_tac 1); |
|
117 by (forward_tac [widen_Class] 1); |
|
118 by (Clarify_tac 1); |
|
119 be disjE 1; |
|
120 by (asm_full_simp_tac (simpset() addsimps [widen.null]) 1); |
|
121 by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1); |
|
122 by (Clarify_tac 1); |
|
123 by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1); |
|
124 by (exhaust_tac "v" 1); |
|
125 by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null])))); |
|
126 qed "Cast_conf2"; |
|
127 |
|
128 Goal |
|
129 "\\<lbrakk> wf_prog wt G; \ |
|
130 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
131 \ ins!pc = CH (Checkcast D); \ |
|
132 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
133 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
134 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
135 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
136 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons, |
|
137 xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
|
138 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
139 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] |
|
140 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1); |
|
141 qed "Checkcast_correct"; |
|
142 |
|
143 |
|
144 Goal |
|
145 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
146 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
147 \ ins!pc = CH ch_com; \ |
|
148 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
149 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
150 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
151 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
152 ba 1; |
|
153 ba 1; |
|
154 by(rewtac wt_jvm_prog_def); |
|
155 by (exhaust_tac "ch_com" 1); |
|
156 by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct]))); |
|
157 qed "CH_correct"; |
|
158 |
|
159 |
|
160 (******* MO *******) |
|
161 Goal |
|
162 "\\<lbrakk> wf_prog wt G; \ |
|
163 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
164 \ ins!pc = MO (Getfield F D); \ |
|
165 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
166 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
167 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
168 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
169 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
|
170 by (Clarify_tac 1); |
|
171 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
|
172 by (Clarify_tac 1); |
|
173 bd approx_stk_Cons_lemma 1; |
|
174 by (Clarify_tac 1); |
|
175 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); |
|
176 |
|
177 by (forward_tac [conf_widen] 1); |
|
178 ba 1; |
|
179 ba 1; |
|
180 bd conf_RefTD 1; |
|
181 by (Clarify_tac 1); |
|
182 by (asm_full_simp_tac (simpset() addsimps []) 1); |
|
183 |
|
184 (* approx_stk *) |
|
185 br conjI 1; |
|
186 by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1); |
|
187 br conjI 1; |
|
188 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup]) 1); |
|
189 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); |
|
190 bd widen_cfs_fields 1; |
|
191 ba 1; |
|
192 ba 1; |
|
193 by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1); |
|
194 |
|
195 (* approx_loc *) |
|
196 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1); |
|
197 qed "Getfield_correct"; |
|
198 |
|
199 |
|
200 Goal |
|
201 "\\<lbrakk> wf_prog wt G; \ |
|
202 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
203 \ ins!pc = MO (Putfield F D); \ |
|
204 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
205 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
206 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
207 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
208 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
|
209 by (Clarify_tac 1); |
|
210 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
|
211 by (Clarify_tac 1); |
|
212 bd approx_stk_Cons_lemma 1; |
|
213 by (Clarify_tac 1); |
|
214 bd approx_stk_Cons_lemma 1; |
|
215 by (Clarify_tac 1); |
|
216 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); |
|
217 |
|
218 by (forward_tac [conf_widen] 1); |
|
219 ba 2; |
|
220 ba 1; |
|
221 by (fast_tac (claset() addDs [conf_RefTD,widen_cfs_fields] |
|
222 addIs [sup_heap_update_value,approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup), |
|
223 approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup), |
|
224 hconf_imp_hconf_field_update, |
|
225 correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1); |
|
226 qed "Putfield_correct"; |
|
227 |
|
228 |
|
229 Goal |
|
230 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
231 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
232 \ ins!pc = MO mo_com; \ |
|
233 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
234 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
235 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
236 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
237 ba 1; |
|
238 ba 1; |
|
239 by(rewtac wt_jvm_prog_def); |
|
240 by (exhaust_tac "mo_com" 1); |
|
241 by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct]))); |
|
242 qed "MO_correct"; |
|
243 |
|
244 |
|
245 (****** CO ******) |
|
246 |
|
247 Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)"; |
|
248 by(Fast_tac 1); |
|
249 qed "collapse_paired_All"; |
|
250 |
|
251 Goal |
|
252 "\\<lbrakk> wf_prog wt G; \ |
|
253 \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ |
|
254 \ ins!pc = CO(New cl_idx); \ |
|
255 \ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \ |
|
256 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \ |
|
257 \ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \ |
|
258 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
259 by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref, |
|
260 approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup), |
|
261 approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup), |
|
262 hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref, |
|
263 rewrite_rule [split_def] correct_init_obj] |
|
264 addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def, |
|
265 fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1 |
|
266 addsplits [option.split])) 1); |
|
267 qed "New_correct"; |
|
268 |
|
269 Goal |
|
270 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
271 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
272 \ ins!pc = CO co_com; \ |
|
273 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
274 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
275 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
276 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
277 ba 1; |
|
278 ba 1; |
|
279 by(rewtac wt_jvm_prog_def); |
|
280 by (exhaust_tac "co_com" 1); |
|
281 by (ALLGOALS (fast_tac (claset() addIs [New_correct]))); |
|
282 qed "CO_correct"; |
|
283 |
|
284 |
|
285 (****** MI ******) |
|
286 |
|
287 Goal |
|
288 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
289 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
290 \ ins ! pc = MI(Invokevirtual mn pTs); \ |
|
291 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
292 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
293 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
294 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
295 by(forward_tac [wt_jvm_progD] 1); |
|
296 by(etac exE 1); |
|
297 by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1 |
|
298 addsplits [option.split]) 1); |
|
299 by (Clarify_tac 1); |
|
300 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
|
301 bd approx_stk_append_lemma 1; |
|
302 by (Clarify_tac 1); |
|
303 bd approx_stk_Cons_lemma 1; |
|
304 by (asm_full_simp_tac (simpset() addsimps []) 1); |
|
305 by (Clarify_tac 1); |
|
306 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1); |
|
307 bd conf_RefTD 1; |
|
308 by (Clarify_tac 1); |
|
309 by(rename_tac "oloc oT ofs T'" 1); |
|
310 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
|
311 bd subtype_widen_methd 1; |
|
312 ba 1; |
|
313 ba 1; |
|
314 be exE 1; |
|
315 by(rename_tac "oT'" 1); |
|
316 by (Clarify_tac 1); |
|
317 by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1); |
|
318 by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2); |
|
319 ba 2; |
|
320 by(Blast_tac 2); |
|
321 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
|
322 by(forward_tac [cmethd_in_md] 1); |
|
323 ba 1; |
|
324 back(); |
|
325 back(); |
|
326 by (Clarify_tac 1); |
|
327 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
|
328 by (forward_tac [wt_jvm_prog_impl_wt_start] 1); |
|
329 ba 1; |
|
330 back(); |
|
331 by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1); |
|
332 by (Clarify_tac 1); |
|
333 |
|
334 (** approx_stk **) |
|
335 br conjI 1; |
|
336 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Nil,approx_stk_Nil]) 1); |
|
337 |
|
338 |
|
339 (** approx_loc **) |
|
340 br conjI 1; |
|
341 br approx_loc_imp_approx_loc_sup 1; |
|
342 ba 1; |
|
343 by (Fast_tac 2); |
|
344 by (asm_full_simp_tac (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def,approx_loc_append]) 1); |
|
345 br conjI 1; |
|
346 br conf_widen 1; |
|
347 ba 1; |
|
348 by (Fast_tac 2); |
|
349 by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1); |
|
350 br conjI 1; |
|
351 by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)] |
|
352 addss (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def])) 1); |
|
353 by (asm_simp_tac (simpset() addsimps [split_def,approx_loc_def,zip_replicate,approx_val_None,set_replicate_conv_if]) 1); |
|
354 |
|
355 br conjI 1; |
|
356 by (asm_simp_tac (simpset() addsimps [min_def]) 1); |
|
357 br exI 1; |
|
358 br exI 1; |
|
359 br conjI 1; |
|
360 by(Blast_tac 1); |
|
361 by (fast_tac (claset() |
|
362 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] |
|
363 addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1); |
|
364 qed "Invokevirtual_correct"; |
|
365 |
|
366 Goal |
|
367 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
368 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
369 \ ins!pc = MI mi_com; \ |
|
370 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
371 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
372 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
373 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
374 ba 1; |
|
375 ba 1; |
|
376 by (exhaust_tac "mi_com" 1); |
|
377 by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct]))); |
|
378 qed "MI_correct"; |
|
379 |
|
380 (****** MR ******) |
|
381 |
|
382 Goal |
|
383 "\\<forall>zs. (xs@ys = zs) = (xs = take (length xs) zs \\<and> ys = drop (length xs) zs)"; |
|
384 by(induct_tac "xs" 1); |
|
385 by(Simp_tac 1); |
|
386 by(Asm_full_simp_tac 1); |
|
387 by(Clarify_tac 1); |
|
388 by(exhaust_tac "zs" 1); |
|
389 by(Auto_tac); |
|
390 qed_spec_mp "append_eq_conv_conj"; |
|
391 |
|
392 |
|
393 |
|
394 Delsimps [map_append]; |
|
395 Goal |
|
396 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
397 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
398 \ ins ! pc = MR; \ |
|
399 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
400 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
401 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
402 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
403 by (asm_full_simp_tac (simpset() addsimps defs1) 1); |
|
404 by (Clarify_tac 1); |
|
405 by (asm_full_simp_tac (simpset() addsimps defs1) 1); |
|
406 by (exhaust_tac "frs" 1); |
|
407 by (asm_full_simp_tac (simpset() addsimps defs1) 1); |
|
408 by (Clarify_tac 1); |
|
409 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1) 1); |
|
410 by (Clarify_tac 1); |
|
411 by (asm_full_simp_tac (simpset() addsimps defs1) 1); |
|
412 by (forward_tac [wt_jvm_prog_impl_wt_instr] 1); |
|
413 by(EVERY1[atac, etac Suc_lessD]); |
|
414 by(rewtac wt_jvm_prog_def); |
|
415 by (fast_tac (claset() |
|
416 addDs [approx_stk_Cons_lemma,subcls_widen_methd] |
|
417 addEs [rotate_prems 1 widen_trans] |
|
418 addIs [conf_widen] |
|
419 addss (simpset() |
|
420 addsimps [approx_val_def,append_eq_conv_conj,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1); |
|
421 qed "Return_correct"; |
|
422 Addsimps [map_append]; |
|
423 |
|
424 Goal |
|
425 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
426 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
427 \ ins!pc = MR; \ |
|
428 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
429 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
430 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
431 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
432 ba 1; |
|
433 ba 1; |
|
434 by (ALLGOALS (fast_tac (claset() addIs [Return_correct]))); |
|
435 qed "MR_correct"; |
|
436 |
|
437 (****** BR ******) |
|
438 Goal |
|
439 "\\<lbrakk> wf_prog wt G; \ |
|
440 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
441 \ ins ! pc = BR(Goto branch); \ |
|
442 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
443 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
444 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
445 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
446 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup] |
|
447 addss (simpset() addsimps defs1)) 1); |
|
448 qed "Goto_correct"; |
|
449 |
|
450 |
|
451 Goal |
|
452 "\\<lbrakk> wf_prog wt G; \ |
|
453 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
454 \ ins!pc = BR(Ifcmpeq branch); \ |
|
455 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
456 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
457 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
458 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
459 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
460 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1); |
|
461 qed "Ifiacmpeq_correct"; |
|
462 |
|
463 |
|
464 Goal |
|
465 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
466 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
467 \ ins!pc = BR br_com; \ |
|
468 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
469 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
470 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
471 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
472 ba 1; |
|
473 ba 1; |
|
474 by(rewtac wt_jvm_prog_def); |
|
475 by (exhaust_tac "br_com" 1); |
|
476 by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct]))); |
|
477 qed "BR_correct"; |
|
478 |
|
479 |
|
480 (****** OS ******) |
|
481 |
|
482 Goal |
|
483 "\\<lbrakk> wf_prog wt G; \ |
|
484 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
485 \ ins ! pc = OS Pop; \ |
|
486 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
487 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
488 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
489 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
490 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
491 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1); |
|
492 qed "Pop_correct"; |
|
493 |
|
494 |
|
495 Goal |
|
496 "\\<lbrakk> wf_prog wt G; \ |
|
497 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
498 \ ins ! pc = OS Dup; \ |
|
499 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
500 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
501 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
502 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
503 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
504 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] |
|
505 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
506 qed "Dup_correct"; |
|
507 |
|
508 |
|
509 Goal |
|
510 "\\<lbrakk> wf_prog wt G; \ |
|
511 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
512 \ ins ! pc = OS Dup_x1; \ |
|
513 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
514 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
515 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
516 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
517 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
518 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] |
|
519 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
520 qed "Dup_x1_correct"; |
|
521 |
|
522 Goal |
|
523 "\\<lbrakk> wf_prog wt G; \ |
|
524 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
525 \ ins ! pc = OS Dup_x2; \ |
|
526 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
527 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
528 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
529 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
530 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
531 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] |
|
532 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
533 qed "Dup_x2_correct"; |
|
534 |
|
535 Goal |
|
536 "\\<lbrakk> wf_prog wt G; \ |
|
537 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
538 \ ins ! pc = OS Swap; \ |
|
539 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
|
540 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
|
541 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
542 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
543 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
|
544 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] |
|
545 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
|
546 qed "Swap_correct"; |
|
547 |
|
548 Goal |
|
549 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
550 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
|
551 \ ins!pc = OS os_com; \ |
|
552 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
|
553 \ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \ |
|
554 \\\<Longrightarrow> correct_state G phi (xp',hp',frs')"; |
|
555 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
|
556 ba 1; |
|
557 ba 1; |
|
558 by(rewtac wt_jvm_prog_def); |
|
559 by (exhaust_tac "os_com" 1); |
|
560 by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct]))); |
|
561 qed "OS_correct"; |
|
562 |
|
563 (** Main **) |
|
564 |
|
565 Goalw [correct_state_def,Let_def] |
|
566 "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \ |
|
567 \ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)"; |
|
568 by(Asm_full_simp_tac 1); |
|
569 by(Blast_tac 1); |
|
570 qed "correct_state_impl_Some_cmethd"; |
|
571 |
|
572 Goal |
|
573 "\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \ |
|
574 \ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'"; |
|
575 by(split_all_tac 1); |
|
576 by(rename_tac "xp hp frs" 1); |
|
577 by (exhaust_tac "xp" 1); |
|
578 by (exhaust_tac "frs" 1); |
|
579 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
|
580 by(split_all_tac 1); |
|
581 by(hyp_subst_tac 1); |
|
582 by(forward_tac [correct_state_impl_Some_cmethd] 1); |
|
583 by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct, |
|
584 BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1); |
|
585 by (exhaust_tac "frs" 1); |
|
586 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
|
587 by (force_tac (claset(), simpset() addsimps exec.rules@[correct_state_def]) 1); |
|
588 qed_spec_mp "BV_correct_1"; |
|
589 |
|
590 |
|
591 (*******) |
|
592 Goal |
|
593 "xp=None \\<longrightarrow> frs\\<noteq>[] \\<longrightarrow> (\\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs'))"; |
|
594 by (fast_tac (claset() addIs [BV_correct_1] |
|
595 addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1); |
|
596 qed_spec_mp "exec_lemma"; |
|
597 |
|
598 Goal |
|
599 "\\<lbrakk> wt_jvm_prog G phi; \ |
|
600 \ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \ |
|
601 \ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')"; |
|
602 by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1); |
|
603 ba 1; |
|
604 by (fast_tac (claset() addIs [BV_correct_1]) 1); |
|
605 qed "L1"; |
|
606 (*******) |
|
607 |
|
608 Goalw [exec_all_def] |
|
609 "\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \ |
|
610 \ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t"; |
|
611 be rtrancl_induct 1; |
|
612 by (Simp_tac 1); |
|
613 by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1); |
|
614 qed_spec_mp "BV_correct"; |
|
615 |
|
616 |
|
617 Goal |
|
618 "\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\<rbrakk> \ |
|
619 \ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) "; |
|
620 bd BV_correct 1; |
|
621 ba 1; |
|
622 ba 1; |
|
623 by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,split_def] |
|
624 addsplits [option.split_asm]) 1); |
|
625 qed_spec_mp "BV_correct_initial"; |