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