7 val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def, |
7 val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def, |
8 correct_frame_def,wt_instr_def]; |
8 correct_frame_def,wt_instr_def]; |
9 |
9 |
10 Goalw [correct_state_def,Let_def,correct_frame_def,split_def] |
10 Goalw [correct_state_def,Let_def,correct_frame_def,split_def] |
11 "\\<lbrakk> wt_jvm_prog G phi; \ |
11 "\\<lbrakk> wt_jvm_prog G phi; \ |
12 \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ |
12 \ method (G,C) sig = Some (C,rT,maxl,ins); \ |
13 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \ |
13 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \ |
14 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; |
14 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; |
15 by (Asm_full_simp_tac 1); |
15 by (Asm_full_simp_tac 1); |
16 by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1); |
16 by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1); |
17 qed "wt_jvm_prog_impl_wt_instr_cor"; |
17 qed "wt_jvm_prog_impl_wt_instr_cor"; |
22 |
22 |
23 (******* LS *******) |
23 (******* LS *******) |
24 |
24 |
25 Goal |
25 Goal |
26 "\\<lbrakk> wf_prog wt G; \ |
26 "\\<lbrakk> wf_prog wt G; \ |
27 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
27 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
28 \ ins!pc = LS(Load idx); \ |
28 \ ins!pc = LS(Load idx); \ |
29 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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); \ |
30 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
31 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
31 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
32 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
32 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
36 qed "Load_correct"; |
36 qed "Load_correct"; |
37 |
37 |
38 |
38 |
39 Goal |
39 Goal |
40 "\\<lbrakk> wf_prog wt G; \ |
40 "\\<lbrakk> wf_prog wt G; \ |
41 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
41 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
42 \ ins!pc = LS(Store idx); \ |
42 \ ins!pc = LS(Store idx); \ |
43 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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) ; \ |
44 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
45 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
45 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
46 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
46 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
54 qed "conf_Intg_Integer"; |
54 qed "conf_Intg_Integer"; |
55 AddIffs [conf_Intg_Integer]; |
55 AddIffs [conf_Intg_Integer]; |
56 |
56 |
57 Goal |
57 Goal |
58 "\\<lbrakk> wf_prog wt G; \ |
58 "\\<lbrakk> wf_prog wt G; \ |
59 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
59 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
60 \ ins!pc = LS(Bipush i); \ |
60 \ ins!pc = LS(Bipush i); \ |
61 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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) ; \ |
62 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
63 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
63 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
64 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
64 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
78 by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1); |
78 by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1); |
79 qed "NT_subtype_conv"; |
79 qed "NT_subtype_conv"; |
80 |
80 |
81 Goal |
81 Goal |
82 "\\<lbrakk> wf_prog wt G; \ |
82 "\\<lbrakk> wf_prog wt G; \ |
83 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
83 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
84 \ ins!pc = LS Aconst_null; \ |
84 \ ins!pc = LS Aconst_null; \ |
85 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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) ; \ |
86 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
87 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
87 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
88 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
88 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
91 qed "Aconst_null_correct"; |
91 qed "Aconst_null_correct"; |
92 |
92 |
93 |
93 |
94 Goal |
94 Goal |
95 "\\<lbrakk> wt_jvm_prog G phi; \ |
95 "\\<lbrakk> wt_jvm_prog G phi; \ |
96 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
96 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
97 \ ins!pc = LS ls_com; \ |
97 \ ins!pc = LS ls_com; \ |
98 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
98 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
99 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
99 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
100 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
100 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
101 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
101 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
125 by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null])))); |
125 by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null])))); |
126 qed "Cast_conf2"; |
126 qed "Cast_conf2"; |
127 |
127 |
128 Goal |
128 Goal |
129 "\\<lbrakk> wf_prog wt G; \ |
129 "\\<lbrakk> wf_prog wt G; \ |
130 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
130 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
131 \ ins!pc = CH (Checkcast D); \ |
131 \ ins!pc = CH (Checkcast D); \ |
132 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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); \ |
133 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
134 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
134 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
135 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
135 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
136 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons, |
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); |
137 raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
138 by (fast_tac (claset() addDs [approx_stk_Cons_lemma] |
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] |
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); |
140 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1); |
141 qed "Checkcast_correct"; |
141 qed "Checkcast_correct"; |
142 |
142 |
143 |
143 |
144 Goal |
144 Goal |
145 "\\<lbrakk> wt_jvm_prog G phi; \ |
145 "\\<lbrakk> wt_jvm_prog G phi; \ |
146 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
146 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
147 \ ins!pc = CH ch_com; \ |
147 \ ins!pc = CH ch_com; \ |
148 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
148 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
149 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
149 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
150 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
150 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
151 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
151 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
158 |
158 |
159 |
159 |
160 (******* MO *******) |
160 (******* MO *******) |
161 Goal |
161 Goal |
162 "\\<lbrakk> wf_prog wt G; \ |
162 "\\<lbrakk> wf_prog wt G; \ |
163 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
163 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
164 \ ins!pc = MO (Getfield F D); \ |
164 \ ins!pc = MO (Getfield F D); \ |
165 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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); \ |
166 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
167 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
167 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
168 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
168 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
169 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
169 by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
170 by (Clarify_tac 1); |
170 by (Clarify_tac 1); |
171 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
171 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
172 by (Clarify_tac 1); |
172 by (Clarify_tac 1); |
173 bd approx_stk_Cons_lemma 1; |
173 bd approx_stk_Cons_lemma 1; |
174 by (Clarify_tac 1); |
174 by (Clarify_tac 1); |
197 qed "Getfield_correct"; |
197 qed "Getfield_correct"; |
198 |
198 |
199 |
199 |
200 Goal |
200 Goal |
201 "\\<lbrakk> wf_prog wt G; \ |
201 "\\<lbrakk> wf_prog wt G; \ |
202 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
202 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
203 \ ins!pc = MO (Putfield F D); \ |
203 \ ins!pc = MO (Putfield F D); \ |
204 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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); \ |
205 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
206 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
206 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
207 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
207 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
208 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
208 by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1); |
209 by (Clarify_tac 1); |
209 by (Clarify_tac 1); |
210 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
210 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); |
211 by (Clarify_tac 1); |
211 by (Clarify_tac 1); |
212 bd approx_stk_Cons_lemma 1; |
212 bd approx_stk_Cons_lemma 1; |
213 by (Clarify_tac 1); |
213 by (Clarify_tac 1); |
226 qed "Putfield_correct"; |
226 qed "Putfield_correct"; |
227 |
227 |
228 |
228 |
229 Goal |
229 Goal |
230 "\\<lbrakk> wt_jvm_prog G phi; \ |
230 "\\<lbrakk> wt_jvm_prog G phi; \ |
231 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
231 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
232 \ ins!pc = MO mo_com; \ |
232 \ ins!pc = MO mo_com; \ |
233 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
233 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
234 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
234 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
235 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
235 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
236 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
236 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
248 by(Fast_tac 1); |
248 by(Fast_tac 1); |
249 qed "collapse_paired_All"; |
249 qed "collapse_paired_All"; |
250 |
250 |
251 Goal |
251 Goal |
252 "\\<lbrakk> wf_prog wt G; \ |
252 "\\<lbrakk> wf_prog wt G; \ |
253 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
253 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
254 \ ins!pc = CO(New cl_idx); \ |
254 \ ins!pc = CO(New cl_idx); \ |
255 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
255 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
256 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
256 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
257 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
257 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
258 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
258 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
260 approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup), |
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), |
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, |
262 hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref, |
263 rewrite_rule [split_def] correct_init_obj] |
263 rewrite_rule [split_def] correct_init_obj] |
264 addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def, |
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 |
265 fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 |
266 addsplits [option.split])) 1); |
266 addsplits [option.split])) 1); |
267 qed "New_correct"; |
267 qed "New_correct"; |
268 |
268 |
269 Goal |
269 Goal |
270 "\\<lbrakk> wt_jvm_prog G phi; \ |
270 "\\<lbrakk> wt_jvm_prog G phi; \ |
271 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
271 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
272 \ ins!pc = CO co_com; \ |
272 \ ins!pc = CO co_com; \ |
273 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
273 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
274 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
274 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
275 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
275 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
276 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
276 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
284 |
284 |
285 (****** MI ******) |
285 (****** MI ******) |
286 |
286 |
287 Goal |
287 Goal |
288 "\\<lbrakk> wt_jvm_prog G phi; \ |
288 "\\<lbrakk> wt_jvm_prog G phi; \ |
289 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
289 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
290 \ ins ! pc = MI(Invoke mn pTs); \ |
290 \ ins ! pc = MI(Invoke mn pTs); \ |
291 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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) ; \ |
292 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
293 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
293 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
294 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
294 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
295 by(forward_tac [wt_jvm_progD] 1); |
295 by(forward_tac [wt_jvm_progD] 1); |
296 by(etac exE 1); |
296 by(etac exE 1); |
297 by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1 |
297 by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 |
298 addsplits [option.split]) 1); |
298 addsplits [option.split]) 1); |
299 by (Clarify_tac 1); |
299 by (Clarify_tac 1); |
300 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
300 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); |
301 bd approx_stk_append_lemma 1; |
301 bd approx_stk_append_lemma 1; |
302 by (Clarify_tac 1); |
302 by (Clarify_tac 1); |
363 addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1); |
363 addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1); |
364 qed "Invoke_correct"; |
364 qed "Invoke_correct"; |
365 |
365 |
366 Goal |
366 Goal |
367 "\\<lbrakk> wt_jvm_prog G phi; \ |
367 "\\<lbrakk> wt_jvm_prog G phi; \ |
368 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
368 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
369 \ ins!pc = MI mi_com; \ |
369 \ ins!pc = MI mi_com; \ |
370 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
370 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
371 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
371 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
372 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
372 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
373 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
373 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
392 |
392 |
393 |
393 |
394 Delsimps [map_append]; |
394 Delsimps [map_append]; |
395 Goal |
395 Goal |
396 "\\<lbrakk> wt_jvm_prog G phi; \ |
396 "\\<lbrakk> wt_jvm_prog G phi; \ |
397 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
397 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
398 \ ins ! pc = MR Return; \ |
398 \ ins ! pc = MR Return; \ |
399 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
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) ; \ |
400 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
401 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
401 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
402 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
402 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
421 qed "Return_correct"; |
421 qed "Return_correct"; |
422 Addsimps [map_append]; |
422 Addsimps [map_append]; |
423 |
423 |
424 Goal |
424 Goal |
425 "\\<lbrakk> wt_jvm_prog G phi; \ |
425 "\\<lbrakk> wt_jvm_prog G phi; \ |
426 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
426 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
427 \ ins!pc = MR mr; \ |
427 \ ins!pc = MR mr; \ |
428 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
428 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
429 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
429 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
430 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
430 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
431 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
431 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
436 qed "MR_correct"; |
436 qed "MR_correct"; |
437 |
437 |
438 (****** BR ******) |
438 (****** BR ******) |
439 Goal |
439 Goal |
440 "\\<lbrakk> wf_prog wt G; \ |
440 "\\<lbrakk> wf_prog wt G; \ |
441 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
441 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
442 \ ins ! pc = BR(Goto branch); \ |
442 \ ins ! pc = BR(Goto branch); \ |
443 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
443 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
444 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
444 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
445 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
445 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
446 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
446 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
449 qed "Goto_correct"; |
449 qed "Goto_correct"; |
450 |
450 |
451 |
451 |
452 Goal |
452 Goal |
453 "\\<lbrakk> wf_prog wt G; \ |
453 "\\<lbrakk> wf_prog wt G; \ |
454 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
454 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
455 \ ins!pc = BR(Ifcmpeq branch); \ |
455 \ ins!pc = BR(Ifcmpeq branch); \ |
456 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
456 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
457 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
457 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
458 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
458 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
459 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
459 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
462 qed "Ifiacmpeq_correct"; |
462 qed "Ifiacmpeq_correct"; |
463 |
463 |
464 |
464 |
465 Goal |
465 Goal |
466 "\\<lbrakk> wt_jvm_prog G phi; \ |
466 "\\<lbrakk> wt_jvm_prog G phi; \ |
467 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
467 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
468 \ ins!pc = BR br_com; \ |
468 \ ins!pc = BR br_com; \ |
469 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
469 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
470 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
470 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
471 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
471 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
472 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
472 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
480 |
480 |
481 (****** OS ******) |
481 (****** OS ******) |
482 |
482 |
483 Goal |
483 Goal |
484 "\\<lbrakk> wf_prog wt G; \ |
484 "\\<lbrakk> wf_prog wt G; \ |
485 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
485 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
486 \ ins ! pc = OS Pop; \ |
486 \ ins ! pc = OS Pop; \ |
487 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
487 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
488 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
488 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
489 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
489 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
490 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
490 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
493 qed "Pop_correct"; |
493 qed "Pop_correct"; |
494 |
494 |
495 |
495 |
496 Goal |
496 Goal |
497 "\\<lbrakk> wf_prog wt G; \ |
497 "\\<lbrakk> wf_prog wt G; \ |
498 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
498 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
499 \ ins ! pc = OS Dup; \ |
499 \ ins ! pc = OS Dup; \ |
500 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
500 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
501 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
501 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
502 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
502 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
503 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
503 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
507 qed "Dup_correct"; |
507 qed "Dup_correct"; |
508 |
508 |
509 |
509 |
510 Goal |
510 Goal |
511 "\\<lbrakk> wf_prog wt G; \ |
511 "\\<lbrakk> wf_prog wt G; \ |
512 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
512 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
513 \ ins ! pc = OS Dup_x1; \ |
513 \ ins ! pc = OS Dup_x1; \ |
514 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
514 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
515 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
515 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
516 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
516 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
517 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
517 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
520 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
520 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
521 qed "Dup_x1_correct"; |
521 qed "Dup_x1_correct"; |
522 |
522 |
523 Goal |
523 Goal |
524 "\\<lbrakk> wf_prog wt G; \ |
524 "\\<lbrakk> wf_prog wt G; \ |
525 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
525 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
526 \ ins ! pc = OS Dup_x2; \ |
526 \ ins ! pc = OS Dup_x2; \ |
527 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
527 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
528 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
528 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
529 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
529 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
530 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
530 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
533 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
533 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
534 qed "Dup_x2_correct"; |
534 qed "Dup_x2_correct"; |
535 |
535 |
536 Goal |
536 Goal |
537 "\\<lbrakk> wf_prog wt G; \ |
537 "\\<lbrakk> wf_prog wt G; \ |
538 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
538 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
539 \ ins ! pc = OS Swap; \ |
539 \ ins ! pc = OS Swap; \ |
540 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
540 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ |
541 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
541 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ |
542 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
542 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
543 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
543 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
546 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
546 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1); |
547 qed "Swap_correct"; |
547 qed "Swap_correct"; |
548 |
548 |
549 Goal |
549 Goal |
550 "\\<lbrakk> wt_jvm_prog G phi; \ |
550 "\\<lbrakk> wt_jvm_prog G phi; \ |
551 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ |
551 \ method (G,C) ml = Some (C,rT,maxl,ins); \ |
552 \ ins!pc = OS os_com; \ |
552 \ ins!pc = OS os_com; \ |
553 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
553 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ |
554 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
554 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \ |
555 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
555 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>"; |
556 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
556 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1); |
563 |
563 |
564 (** Main **) |
564 (** Main **) |
565 |
565 |
566 Goalw [correct_state_def,Let_def] |
566 Goalw [correct_state_def,Let_def] |
567 "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \ |
567 "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \ |
568 \ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)"; |
568 \ \\<Longrightarrow> \\<exists>meth. method (G,C) ml = Some(C,meth)"; |
569 by(Asm_full_simp_tac 1); |
569 by(Asm_full_simp_tac 1); |
570 by(Blast_tac 1); |
570 by(Blast_tac 1); |
571 qed "correct_state_impl_Some_cmethd"; |
571 qed "correct_state_impl_Some_method"; |
572 |
572 |
573 Goal |
573 Goal |
574 "\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \ |
574 "\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \ |
575 \ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>"; |
575 \ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>"; |
576 by(split_all_tac 1); |
576 by(split_all_tac 1); |
578 by (exhaust_tac "xp" 1); |
578 by (exhaust_tac "xp" 1); |
579 by (exhaust_tac "frs" 1); |
579 by (exhaust_tac "frs" 1); |
580 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
580 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
581 by(split_all_tac 1); |
581 by(split_all_tac 1); |
582 by(hyp_subst_tac 1); |
582 by(hyp_subst_tac 1); |
583 by(forward_tac [correct_state_impl_Some_cmethd] 1); |
583 by(forward_tac [correct_state_impl_Some_method] 1); |
584 by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct, |
584 by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct, |
585 BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1); |
585 BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1); |
586 by (exhaust_tac "frs" 1); |
586 by (exhaust_tac "frs" 1); |
587 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
587 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); |
588 by (force_tac (claset(), simpset() addsimps exec.rules@[correct_state_def]) 1); |
588 by (force_tac (claset(), simpset() addsimps exec.rules@[correct_state_def]) 1); |