8245
|
1 |
(* Title: HOL/MicroJava/BV/BVLcorrect.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
|
8390
|
8 |
Goal "\\<exists> l. n < length l";
|
8245
|
9 |
by (induct_tac "n" 1);
|
|
10 |
by Auto_tac;
|
|
11 |
by (res_inst_tac [("x","x#l")] exI 1);
|
|
12 |
by (Simp_tac 1);
|
|
13 |
qed "exists_list";
|
|
14 |
|
|
15 |
|
|
16 |
Goal "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc \
|
8390
|
17 |
\ \\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)";
|
8245
|
18 |
by (induct_tac "is" 1);
|
|
19 |
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def, exists_list]) 1);
|
|
20 |
by (Clarify_tac 1);
|
|
21 |
by (Asm_full_simp_tac 1);
|
|
22 |
by (Clarify_tac 1);
|
|
23 |
by (eres_inst_tac [("x","ab")] allE 1);
|
|
24 |
by (eres_inst_tac [("x","ba")] allE 1);
|
|
25 |
by (eres_inst_tac [("x","Suc pc")] allE 1);
|
|
26 |
by (Asm_full_simp_tac 1);
|
|
27 |
by (Clarify_tac 1);
|
8423
|
28 |
by (cases_tac "cert ! pc" 1);
|
8245
|
29 |
by (res_inst_tac [("x","phi[pc:=(aa, b)]")] exI 1);
|
|
30 |
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
|
|
31 |
by (Clarify_tac 1);
|
8423
|
32 |
by (cases_tac "ac" 1);
|
8245
|
33 |
by (Asm_full_simp_tac 1);
|
|
34 |
by (Asm_full_simp_tac 1);
|
|
35 |
by (Clarify_tac 1);
|
|
36 |
by (eres_inst_tac [("x","lista")] allE 1);
|
|
37 |
by (eres_inst_tac [("x","bb")] allE 1);
|
|
38 |
by (eres_inst_tac [("x","i")] allE 1);
|
|
39 |
by (Asm_full_simp_tac 1);
|
|
40 |
by (datac wtl_inst_option_unique 1 1);
|
|
41 |
by (Asm_full_simp_tac 1);
|
|
42 |
by (smp_tac 2 1);
|
|
43 |
be impE 1;
|
|
44 |
by (Force_tac 1);
|
|
45 |
ba 1;
|
|
46 |
by (res_inst_tac [("x","phi[pc:=ac]")] exI 1);
|
|
47 |
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
|
|
48 |
by (Clarify_tac 1);
|
8423
|
49 |
by (cases_tac "ad" 1);
|
8245
|
50 |
by (Asm_full_simp_tac 1);
|
|
51 |
by (Asm_full_simp_tac 1);
|
|
52 |
by (Clarify_tac 1);
|
|
53 |
by (eres_inst_tac [("x","lista")] allE 1);
|
|
54 |
by (eres_inst_tac [("x","bc")] allE 1);
|
|
55 |
by (eres_inst_tac [("x","i")] allE 1);
|
|
56 |
by (Asm_full_simp_tac 1);
|
|
57 |
by (datac wtl_inst_option_unique 1 1);
|
|
58 |
by (Asm_full_simp_tac 1);
|
|
59 |
by (smp_tac 2 1);
|
|
60 |
be impE 1;
|
|
61 |
by (Force_tac 1);
|
|
62 |
ba 1;
|
|
63 |
bind_thm ("exists_phi_partial", result() RS spec RS spec);
|
|
64 |
|
|
65 |
|
8390
|
66 |
Goal "wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi";
|
8245
|
67 |
by (cut_inst_tac [("is","is"),("G","G"),("rT","rT"),("s2.0","s2"),("x","0"),("xa","s0"),("cert","cert")] exists_phi_partial 1);
|
8390
|
68 |
by (asm_full_simp_tac (simpset() addsimps [fits_def]) 1);
|
8245
|
69 |
by (Force_tac 1);
|
|
70 |
qed "exists_phi";
|
|
71 |
|
|
72 |
|
|
73 |
Goal "\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; \
|
8390
|
74 |
\ fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow> \
|
|
75 |
\ \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
|
8245
|
76 |
by (Clarify_tac 1);
|
|
77 |
by (forward_tac [wtl_partial] 1);
|
|
78 |
ba 1;
|
|
79 |
by (Clarify_tac 1);
|
8390
|
80 |
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def ,neq_Nil_conv]) 1);
|
8245
|
81 |
by (Clarify_tac 1);
|
|
82 |
by (eres_inst_tac [("x","aa")] allE 1);
|
|
83 |
by (eres_inst_tac [("x","ys")] allE 1);
|
|
84 |
by (eres_inst_tac [("x","y")] allE 1);
|
|
85 |
by (Asm_full_simp_tac 1);
|
|
86 |
qed "fits_lemma1";
|
|
87 |
|
|
88 |
|
|
89 |
Goal "\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; \
|
|
90 |
\ wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); \
|
|
91 |
\ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a)); \
|
|
92 |
\ fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow> \
|
|
93 |
\ b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
|
|
94 |
by (forward_tac [wtl_append] 1);
|
|
95 |
ba 1;
|
|
96 |
ba 1;
|
8423
|
97 |
by (case_tac "b=[]" 1);
|
8245
|
98 |
by (Asm_full_simp_tac 1);
|
|
99 |
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
|
|
100 |
by (Clarify_tac 1);
|
|
101 |
by (Asm_full_simp_tac 1);
|
|
102 |
by (Clarify_tac 1);
|
8423
|
103 |
by (cases_tac "cert!(Suc (length a))" 1);
|
8390
|
104 |
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
|
8245
|
105 |
by (eres_inst_tac [("x","a@[i]")] allE 1);
|
|
106 |
by (eres_inst_tac [("x","ys")] allE 1);
|
|
107 |
by (eres_inst_tac [("x","y")] allE 1);
|
|
108 |
by (Asm_full_simp_tac 1);
|
|
109 |
by (pair_tac "s2" 1);
|
|
110 |
by (smp_tac 2 1);
|
|
111 |
be impE 1;
|
|
112 |
by (Force_tac 1);
|
|
113 |
by (Asm_full_simp_tac 1);
|
8390
|
114 |
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
|
8245
|
115 |
by (eres_inst_tac [("x","a@[i]")] allE 1);
|
|
116 |
by (eres_inst_tac [("x","ys")] allE 1);
|
|
117 |
by (eres_inst_tac [("x","y")] allE 1);
|
|
118 |
by (Asm_full_simp_tac 1);
|
|
119 |
by (pair_tac "s2" 1);
|
|
120 |
by (smp_tac 2 1);
|
|
121 |
by (Clarify_tac 1);
|
|
122 |
be impE 1;
|
|
123 |
by (Force_tac 1);
|
|
124 |
by (asm_full_simp_tac (simpset() addsimps [wtl_inst_option_def]) 1);
|
|
125 |
qed "wtl_suc_pc";
|
|
126 |
|
|
127 |
|
8390
|
128 |
Goal "\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; \
|
8245
|
129 |
\ wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); \
|
|
130 |
\ fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None; \
|
|
131 |
\ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \
|
|
132 |
\ \\<Longrightarrow> phi!(length a) = s1";
|
8390
|
133 |
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
|
8245
|
134 |
by (eres_inst_tac [("x","a")] allE 1);
|
|
135 |
by (eres_inst_tac [("x","b")] allE 1);
|
|
136 |
by (eres_inst_tac [("x","i")] allE 1);
|
8390
|
137 |
by (Asm_full_simp_tac 1);
|
|
138 |
by (pair_tac "s1" 1);
|
|
139 |
by (eres_inst_tac [("x","x")] allE 1);
|
|
140 |
by (eres_inst_tac [("x","y")] allE 1);
|
8245
|
141 |
by (Asm_full_simp_tac 1);
|
|
142 |
be impE 1;
|
|
143 |
by (pair_tac "s2" 1);
|
|
144 |
by (Force_tac 1);
|
|
145 |
ba 1;
|
|
146 |
qed "fits_lemma2";
|
|
147 |
|
|
148 |
fun ls g1 g2 = if g1 > g2 then ls g2 g1
|
|
149 |
else if g1 = g2 then [g1]
|
|
150 |
else g2::(ls g1 (g2-1))
|
|
151 |
fun GOALS t g1 g2 = EVERY (map t (ls g1 g2));
|
|
152 |
|
|
153 |
Goal "is=(i1@i#i2) \\<longrightarrow> wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length is) 0 \\<longrightarrow> \
|
|
154 |
\ wtl_inst_list i1 G rT s0 s1 cert (length is) 0 \\<longrightarrow> \
|
|
155 |
\ wtl_inst_option i G rT s1 s2 cert (length is) (length i1) \\<longrightarrow> \
|
|
156 |
\ wtl_inst_list i2 G rT s2 s3 cert (length is) (Suc (length i1)) \\<longrightarrow> \
|
|
157 |
\ fits phi (i1@i#i2) G rT s0 s3 cert \\<longrightarrow> \
|
|
158 |
\ wt_instr i G rT phi (length is) (length i1)";
|
|
159 |
by (Clarify_tac 1);
|
|
160 |
by (forward_tac [wtl_suc_pc] 1);
|
|
161 |
by (TRYALL atac);
|
|
162 |
by (forward_tac [fits_lemma1] 1);
|
|
163 |
ba 1;
|
8423
|
164 |
by (cases_tac "cert!(length i1)" 1);
|
8245
|
165 |
by (forward_tac [fits_lemma2] 1);
|
|
166 |
by (TRYALL atac);
|
8423
|
167 |
by (cases_tac "i" 1);
|
|
168 |
by (cases_tac "check_object" 4);
|
|
169 |
by (cases_tac "manipulate_object" 3);
|
|
170 |
by (cases_tac "create_object" 2);
|
|
171 |
by (cases_tac "load_and_store" 1);
|
8245
|
172 |
by (GOALS (force_tac (claset(),
|
|
173 |
simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
|
8423
|
174 |
by (cases_tac "meth_inv" 1);
|
8245
|
175 |
by (thin_tac "\\<forall>pc t.\
|
|
176 |
\ pc < length (i1 @ i # i2) \\<longrightarrow> \
|
|
177 |
\ cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
|
8390
|
178 |
by (pair_tac "s1" 1);
|
|
179 |
by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
|
|
180 |
by (Force_tac 1);
|
8423
|
181 |
by (cases_tac "meth_ret" 1);
|
8245
|
182 |
by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
|
8423
|
183 |
by (cases_tac "branch" 2);
|
|
184 |
by (cases_tac "op_stack" 1);
|
8245
|
185 |
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
|
|
186 |
THEN_MAYBE' Force_tac) 1 7);
|
|
187 |
by (forw_inst_tac [("x","length i1")] spec 1);
|
|
188 |
by (eres_inst_tac [("x","a")] allE 1);
|
8423
|
189 |
by (cases_tac "i" 1);
|
|
190 |
by (cases_tac "check_object" 4);
|
|
191 |
by (cases_tac "manipulate_object" 3);
|
|
192 |
by (cases_tac "create_object" 2);
|
|
193 |
by (cases_tac "load_and_store" 1);
|
8245
|
194 |
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
|
|
195 |
THEN' Force_tac) 1 8);
|
8423
|
196 |
by (cases_tac "meth_inv" 1);
|
8245
|
197 |
by (thin_tac "\\<forall>pc t.\
|
|
198 |
\ pc < length (i1 @ i # i2) \\<longrightarrow> \
|
|
199 |
\ cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
|
|
200 |
by (force_tac (claset(), simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
|
8423
|
201 |
by (cases_tac "branch" 3);
|
|
202 |
by (cases_tac "op_stack" 2);
|
|
203 |
by (cases_tac "meth_ret" 1);
|
8245
|
204 |
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
|
|
205 |
THEN_MAYBE' Force_tac) 1 8);
|
|
206 |
qed "wtl_lemma";
|
|
207 |
|
|
208 |
Goal "\\<lbrakk>wtl_inst_list is G rT s0 s2 cert (length is) 0; \
|
|
209 |
\ fits phi is G rT s0 s2 cert\\<rbrakk> \
|
|
210 |
\ \\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
|
|
211 |
by (Clarify_tac 1);
|
|
212 |
by (forward_tac [wtl_partial] 1);
|
|
213 |
ba 1;
|
|
214 |
by (Clarify_tac 1);
|
|
215 |
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
|
|
216 |
by (Clarify_tac 1);
|
|
217 |
by (Asm_full_simp_tac 1);
|
|
218 |
by (Clarify_tac 1);
|
|
219 |
by (cut_inst_tac [("is","a@y#ys"),("i1.0","a"),("i2.0","ys"),("i","y"),("G","G"),("rT","rT"),("s0.0","s0"),("cert","cert"),("phi","phi"),("s1.0","(aa,ba)"),("s2.0","(ab,b)"),("s3.0","s2")] wtl_lemma 1);
|
|
220 |
by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
|
|
221 |
qed "wtl_fits_wt";
|
|
222 |
|
|
223 |
|
|
224 |
Goal "wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> \
|
|
225 |
\ \\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
|
|
226 |
by (forward_tac [exists_phi] 1);
|
|
227 |
by (Clarify_tac 1);
|
|
228 |
by (forward_tac [wtl_fits_wt] 1);
|
|
229 |
ba 1;
|
|
230 |
by (Force_tac 1);
|
|
231 |
qed "wtl_inst_list_correct";
|
|
232 |
|
8390
|
233 |
Goal "\\<lbrakk>is \\<noteq> []; wtl_inst_list is G rT s0 s2 cert (length is) 0; \
|
|
234 |
\ fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
|
8245
|
235 |
by (forw_inst_tac [("pc'","0")] wtl_partial 1);
|
|
236 |
by (Asm_full_simp_tac 1);
|
8390
|
237 |
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def, neq_Nil_conv]) 1);
|
|
238 |
by (Clarsimp_tac 1);
|
8245
|
239 |
by (eres_inst_tac [("x","[]")] allE 1);
|
|
240 |
by (eres_inst_tac [("x","ys")] allE 1);
|
|
241 |
by (eres_inst_tac [("x","y")] allE 1);
|
|
242 |
by (Asm_full_simp_tac 1);
|
|
243 |
be impE 1;
|
|
244 |
by (Force_tac 1);
|
8423
|
245 |
by (cases_tac "cert ! 0" 1);
|
8245
|
246 |
by (auto_tac (claset(), simpset() addsimps [wtl_inst_option_def]));
|
|
247 |
qed "fits_first";
|
|
248 |
|
|
249 |
|
|
250 |
Goal "wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi";
|
|
251 |
by (asm_full_simp_tac (simpset() addsimps [wtl_method_def, wt_method_def, wt_start_def]) 1);
|
|
252 |
by (Clarify_tac 1);
|
|
253 |
by (forward_tac [exists_phi] 1);
|
|
254 |
by (Clarify_tac 1);
|
|
255 |
by (forward_tac [wtl_fits_wt] 1);
|
|
256 |
ba 1;
|
|
257 |
by (res_inst_tac [("x","phi")] exI 1);
|
|
258 |
by (auto_tac (claset(), simpset() addsimps [fits_first]));
|
|
259 |
qed "wtl_method_correct";
|
|
260 |
|
|
261 |
Goal "(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
|
|
262 |
by (induct_tac "l" 1);
|
|
263 |
by Auto_tac;
|
|
264 |
qed_spec_mp "unique_set";
|
|
265 |
|
|
266 |
Goal "(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
|
|
267 |
by (auto_tac (claset(), simpset() addsimps [unique_set]));
|
|
268 |
qed_spec_mp "unique_epsilon";
|
|
269 |
|
|
270 |
Goalw[wtl_jvm_prog_def,wt_jvm_prog_def] "wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
|
|
271 |
by (asm_full_simp_tac (simpset() addsimps [wf_prog_def, wf_cdecl_def, wf_mdecl_def]) 1);
|
|
272 |
by (res_inst_tac [("x",
|
|
273 |
"\\<lambda> C sig.\
|
|
274 |
\ let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in\
|
|
275 |
\ let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in\
|
|
276 |
\ \\<epsilon> phi. wt_method G C (snd sig) rT maxl b phi")] exI 1);
|
|
277 |
by Safe_tac;
|
|
278 |
by (GOALS Force_tac 1 3);
|
|
279 |
by (GOALS Force_tac 2 3);
|
|
280 |
by (eres_inst_tac [("x","(a, aa, ab, b)")] BallE 1);
|
|
281 |
by (Asm_full_simp_tac 1);
|
|
282 |
by (Clarify_tac 1);
|
|
283 |
by (eres_inst_tac [("x","((ac, ba), ad, ae, bb)")] BallE 1);
|
|
284 |
by (Asm_full_simp_tac 1);
|
|
285 |
by (Clarify_tac 1);
|
|
286 |
bd wtl_method_correct 1;
|
|
287 |
by (Clarify_tac 1);
|
|
288 |
by (asm_full_simp_tac (simpset() addsimps [unique_epsilon]) 1);
|
|
289 |
br selectI 1;
|
|
290 |
ba 1;
|
|
291 |
qed "wtl_correct";
|
|
292 |
|