|
1 (* Title: HOL/MicroJava/Comp/CorrComp.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Strecker |
|
4 Copyright GPL 2002 |
|
5 *) |
|
6 |
|
7 (* Compiler correctness statement and proof *) |
|
8 |
|
9 theory CorrComp = JTypeSafe + LemmasComp: |
|
10 |
|
11 |
|
12 |
|
13 (* If no exception is present after evaluation/execution, |
|
14 none can have been present before *) |
|
15 lemma eval_evals_exec_xcpt: |
|
16 "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
|
17 ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
|
18 ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)" |
|
19 by (induct rule: eval_evals_exec.induct, auto) |
|
20 |
|
21 |
|
22 (* instance of eval_evals_exec_xcpt for eval *) |
|
23 lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
|
24 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T") |
|
25 proof- |
|
26 assume h1: ?H1 |
|
27 assume h2: ?H2 |
|
28 from h1 h2 eval_evals_exec_xcpt show "?T" by simp |
|
29 qed |
|
30 |
|
31 (* instance of eval_evals_exec_xcpt for evals *) |
|
32 lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
|
33 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T") |
|
34 proof- |
|
35 assume h1: ?H1 |
|
36 assume h2: ?H2 |
|
37 from h1 h2 eval_evals_exec_xcpt show "?T" by simp |
|
38 qed |
|
39 |
|
40 (* instance of eval_evals_exec_xcpt for exec *) |
|
41 lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
|
42 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T") |
|
43 proof- |
|
44 assume h1: ?H1 |
|
45 assume h2: ?H2 |
|
46 from h1 h2 eval_evals_exec_xcpt show "?T" by simp |
|
47 qed |
|
48 |
|
49 (**********************************************************************) |
|
50 |
|
51 theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)" |
|
52 apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans) |
|
53 done |
|
54 |
|
55 theorem exec_all_refl: "exec_all G s s" |
|
56 by (simp only: exec_all_def, rule rtrancl_refl) |
|
57 |
|
58 |
|
59 theorem exec_instr_in_exec_all: |
|
60 "\<lbrakk> exec_instr i G hp stk lvars C S pc frs = (None, hp', frs'); |
|
61 gis (gmb G C S) ! pc = i\<rbrakk> \<Longrightarrow> |
|
62 G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) -jvm\<rightarrow> (None, hp', frs')" |
|
63 apply (simp only: exec_all_def) |
|
64 apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
|
65 apply (simp add: gis_def gmb_def) |
|
66 apply (case_tac frs', simp+) |
|
67 done |
|
68 |
|
69 theorem exec_all_one_step: " |
|
70 \<lbrakk> gis (gmb G C S) = pre @ (i # post); pc0 = length pre; |
|
71 (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) = |
|
72 (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk> |
|
73 \<Longrightarrow> |
|
74 G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) -jvm\<rightarrow> |
|
75 (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)" |
|
76 apply (unfold exec_all_def) |
|
77 apply (rule r_into_rtrancl) |
|
78 apply (simp add: gis_def gmb_def split_beta) |
|
79 done |
|
80 |
|
81 |
|
82 (***********************************************************************) |
|
83 |
|
84 constdefs |
|
85 progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> |
|
86 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> |
|
87 bytecode \<Rightarrow> |
|
88 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> |
|
89 bool" |
|
90 ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60) |
|
91 "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} == |
|
92 \<forall> pre post frs. |
|
93 (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow> |
|
94 G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow> |
|
95 (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)" |
|
96 |
|
97 |
|
98 |
|
99 lemma progression_call: |
|
100 "\<lbrakk> \<forall> pc frs. |
|
101 exec_instr instr G hp0 os0 lvars0 C S pc frs = |
|
102 (None, hp', (os', lvars', C', S', 0) # (fr pc) # frs) \<and> |
|
103 gis (gmb G C' S') = instrs' @ [Return] \<and> |
|
104 {G, C', S'} \<turnstile> {hp', os', lvars'} >- instrs' \<rightarrow> {hp'', os'', lvars''} \<and> |
|
105 exec_instr Return G hp'' os'' lvars'' C' S' (length instrs') |
|
106 ((fr pc) # frs) = |
|
107 (None, hp2, (os2, lvars2, C, S, Suc pc) # frs) \<rbrakk> \<Longrightarrow> |
|
108 {G, C, S} \<turnstile> {hp0, os0, lvars0} >-[instr]\<rightarrow> {hp2,os2,lvars2}" |
|
109 apply (simp only: progression_def) |
|
110 apply (intro strip) |
|
111 apply (drule_tac x="length pre" in spec) |
|
112 apply (drule_tac x="frs" in spec) |
|
113 apply clarify |
|
114 apply (rule exec_all_trans) |
|
115 apply (rule exec_instr_in_exec_all) apply simp |
|
116 apply simp |
|
117 apply (rule exec_all_trans) |
|
118 apply (simp only: append_Nil) |
|
119 apply (drule_tac x="[]" in spec) |
|
120 apply (simp only: list.simps) |
|
121 apply blast |
|
122 apply (rule exec_instr_in_exec_all) |
|
123 apply auto |
|
124 done |
|
125 |
|
126 |
|
127 lemma progression_transitive: |
|
128 "\<lbrakk> instrs_comb = instrs0 @ instrs1; |
|
129 {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs0 \<rightarrow> {hp1, os1, lvars1}; |
|
130 {G, C, S} \<turnstile> {hp1, os1, lvars1} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> |
|
131 \<Longrightarrow> |
|
132 {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}" |
|
133 apply (simp only: progression_def) |
|
134 apply (intro strip) |
|
135 apply (rule_tac "s1.0" = "Norm (hp1, (os1, lvars1, C, S, |
|
136 length pre + length instrs0) # frs)" |
|
137 in exec_all_trans) |
|
138 apply (simp only: append_assoc) |
|
139 apply (erule thin_rl, erule thin_rl) |
|
140 apply (drule_tac x="pre @ instrs0" in spec) |
|
141 apply (simp add: add_assoc) |
|
142 done |
|
143 |
|
144 lemma progression_refl: |
|
145 "{G, C, S} \<turnstile> {hp0, os0, lvars0} >- [] \<rightarrow> {hp0, os0, lvars0}" |
|
146 apply (simp add: progression_def) |
|
147 apply (intro strip) |
|
148 apply (rule exec_all_refl) |
|
149 done |
|
150 |
|
151 lemma progression_one_step: " |
|
152 \<forall> pc frs. |
|
153 (exec_instr i G hp0 os0 lvars0 C S pc frs) = |
|
154 (None, hp1, (os1,lvars1,C,S, Suc pc)#frs) |
|
155 \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- [i] \<rightarrow> {hp1, os1, lvars1}" |
|
156 apply (unfold progression_def) |
|
157 apply (intro strip) |
|
158 apply simp |
|
159 apply (rule exec_all_one_step) |
|
160 apply auto |
|
161 done |
|
162 |
|
163 (*****) |
|
164 constdefs |
|
165 jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> |
|
166 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> |
|
167 instr \<Rightarrow> bytecode \<Rightarrow> bool" |
|
168 "jump_fwd G C S hp lvars os0 os1 instr instrs == |
|
169 \<forall> pre post frs. |
|
170 (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow> |
|
171 exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs) |
|
172 (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)" |
|
173 |
|
174 |
|
175 lemma jump_fwd_one_step: |
|
176 "\<forall> pc frs. |
|
177 exec_instr instr G hp os0 lvars C S pc frs = |
|
178 (None, hp, (os1, lvars, C, S, pc + (length instrs) + 1)#frs) |
|
179 \<Longrightarrow> jump_fwd G C S hp lvars os0 os1 instr instrs" |
|
180 apply (unfold jump_fwd_def) |
|
181 apply (intro strip) |
|
182 apply (rule exec_instr_in_exec_all) |
|
183 apply auto |
|
184 done |
|
185 |
|
186 |
|
187 lemma jump_fwd_progression_aux: |
|
188 "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; |
|
189 jump_fwd G C S hp lvars os0 os1 instr instrs0; |
|
190 {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> |
|
191 \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}" |
|
192 apply (simp only: progression_def jump_fwd_def) |
|
193 apply (intro strip) |
|
194 apply (rule_tac "s1.0" = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans) |
|
195 apply (simp only: append_assoc) |
|
196 apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)") |
|
197 apply blast |
|
198 apply simp |
|
199 apply (erule thin_rl, erule thin_rl) |
|
200 apply (drule_tac x="pre @ instr # instrs0" in spec) |
|
201 apply (simp add: add_assoc) |
|
202 done |
|
203 |
|
204 |
|
205 lemma jump_fwd_progression: |
|
206 "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; |
|
207 \<forall> pc frs. |
|
208 exec_instr instr G hp os0 lvars C S pc frs = |
|
209 (None, hp, (os1, lvars, C, S, pc + (length instrs0) + 1)#frs); |
|
210 {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> |
|
211 \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}" |
|
212 apply (rule jump_fwd_progression_aux) |
|
213 apply assumption |
|
214 apply (rule jump_fwd_one_step) apply assumption+ |
|
215 done |
|
216 |
|
217 |
|
218 (* note: instrs and instr reversed wrt. jump_fwd *) |
|
219 constdefs |
|
220 jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> |
|
221 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> |
|
222 bytecode \<Rightarrow> instr \<Rightarrow> bool" |
|
223 "jump_bwd G C S hp lvars os0 os1 instrs instr == |
|
224 \<forall> pre post frs. |
|
225 (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow> |
|
226 exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs) |
|
227 (None,hp,(os1,lvars,C,S, (length pre))#frs)" |
|
228 |
|
229 |
|
230 lemma jump_bwd_one_step: |
|
231 "\<forall> pc frs. |
|
232 exec_instr instr G hp os0 lvars C S (pc + (length instrs)) frs = |
|
233 (None, hp, (os1, lvars, C, S, pc)#frs) |
|
234 \<Longrightarrow> |
|
235 jump_bwd G C S hp lvars os0 os1 instrs instr" |
|
236 apply (unfold jump_bwd_def) |
|
237 apply (intro strip) |
|
238 apply (rule exec_instr_in_exec_all) |
|
239 apply auto |
|
240 done |
|
241 |
|
242 lemma jump_bwd_progression: |
|
243 "\<lbrakk> instrs_comb = instrs @ [instr]; |
|
244 {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1}; |
|
245 jump_bwd G C S hp1 lvars1 os1 os2 instrs instr; |
|
246 {G, C, S} \<turnstile> {hp1, os2, lvars1} >- instrs_comb \<rightarrow> {hp3, os3, lvars3} \<rbrakk> |
|
247 \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp3, os3, lvars3}" |
|
248 apply (simp only: progression_def jump_bwd_def) |
|
249 apply (intro strip) |
|
250 apply (rule exec_all_trans, force) |
|
251 apply (rule exec_all_trans, force) |
|
252 apply (rule exec_all_trans, force) |
|
253 apply simp |
|
254 apply (rule exec_all_refl) |
|
255 done |
|
256 |
|
257 |
|
258 (**********************************************************************) |
|
259 |
|
260 (* class C with signature S is defined in program G *) |
|
261 constdefs class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool" |
|
262 "class_sig_defined G C S == |
|
263 is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))" |
|
264 |
|
265 |
|
266 (* The environment of a java method body |
|
267 (characterized by class and signature) *) |
|
268 constdefs env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env" |
|
269 "env_of_jmb G C S == |
|
270 (let (mn,pTs) = S; |
|
271 (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in |
|
272 (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))" |
|
273 |
|
274 lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G" |
|
275 by (simp add: env_of_jmb_def split_beta) |
|
276 |
|
277 |
|
278 (**********************************************************************) |
|
279 |
|
280 |
|
281 (* ### to be moved to one of the J/* files *) |
|
282 |
|
283 lemma method_preserves [rule_format (no_asm)]: |
|
284 "\<lbrakk> wf_prog wf_mb G; is_class G C; |
|
285 \<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb) \<longrightarrow> (P cn S (rT,mb))\<rbrakk> |
|
286 \<Longrightarrow> \<forall> D. |
|
287 method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))" |
|
288 |
|
289 apply (frule WellForm.wf_subcls1) |
|
290 apply (rule subcls1_induct, assumption, assumption) |
|
291 |
|
292 apply (intro strip) |
|
293 apply ((drule spec)+, drule_tac x="Object" in bspec) |
|
294 apply (simp add: wf_prog_def wf_syscls_def) |
|
295 apply (subgoal_tac "D=Object") apply simp |
|
296 apply (drule mp) |
|
297 apply (frule_tac C=Object in method_wf_mdecl) |
|
298 apply simp apply assumption apply simp apply assumption apply simp |
|
299 |
|
300 apply (subst method_rec) apply simp |
|
301 apply force |
|
302 apply assumption |
|
303 apply (simp only: override_def) |
|
304 apply (split option.split) |
|
305 apply (rule conjI) |
|
306 apply force |
|
307 apply (intro strip) |
|
308 apply (frule_tac |
|
309 "P1.0" = "wf_mdecl wf_mb G Ca" and |
|
310 "P2.0" = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop) |
|
311 apply (force simp: wf_cdecl_def) |
|
312 |
|
313 apply clarify |
|
314 |
|
315 apply (simp only: class_def) |
|
316 apply (drule map_of_SomeD)+ |
|
317 apply (frule_tac A="set G" and f=fst in imageI, simp) |
|
318 apply blast |
|
319 apply simp |
|
320 done |
|
321 |
|
322 |
|
323 lemma method_preserves_length: |
|
324 "\<lbrakk> wf_java_prog G; is_class G C; |
|
325 method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk> |
|
326 \<Longrightarrow> length pns = length pTs" |
|
327 apply (frule_tac |
|
328 P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs" |
|
329 in method_preserves) |
|
330 apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
331 done |
|
332 |
|
333 (**********************************************************************) |
|
334 |
|
335 (* required for lemma wtpd_expr_call *) |
|
336 lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)" |
|
337 apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)") |
|
338 apply blast |
|
339 apply (rule ty_expr_ty_exprs_wt_stmt.induct) |
|
340 apply auto |
|
341 done |
|
342 |
|
343 constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool" |
|
344 "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)" |
|
345 wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool" |
|
346 "wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)" |
|
347 wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" |
|
348 "wtpd_stmt E c == (E\<turnstile>c \<surd>)" |
|
349 |
|
350 lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C" |
|
351 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
352 |
|
353 lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \<Longrightarrow> (wtpd_expr E e)" |
|
354 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
355 |
|
356 lemma wtpd_expr_lacc: "\<lbrakk> wtpd_expr (env_of_jmb G C S) (LAcc vn); |
|
357 class_sig_defined G C S \<rbrakk> |
|
358 \<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This" |
|
359 apply (simp only: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs) |
|
360 apply clarify |
|
361 apply (case_tac S) |
|
362 apply simp |
|
363 apply (erule ty_expr.cases) |
|
364 apply (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
|
365 apply (drule map_upds_SomeD) |
|
366 apply (erule disjE) |
|
367 apply assumption |
|
368 apply (drule map_of_SomeD) apply (auto dest: fst_in_set_lemma) |
|
369 done |
|
370 |
|
371 lemma wtpd_expr_lass: "wtpd_expr E (vn::=e) |
|
372 \<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)" |
|
373 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
374 |
|
375 lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn) |
|
376 \<Longrightarrow> (wtpd_expr E a)" |
|
377 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
378 |
|
379 lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v) |
|
380 \<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)" |
|
381 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
382 |
|
383 |
|
384 lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2) |
|
385 \<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)" |
|
386 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
387 |
|
388 lemma wtpd_exprs_cons: "wtpd_exprs E (e # es) |
|
389 \<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)" |
|
390 by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto) |
|
391 |
|
392 lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \<Longrightarrow> (wtpd_expr E e)" |
|
393 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
394 |
|
395 lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \<Longrightarrow> |
|
396 (wtpd_stmt E s1) & (wtpd_stmt E s2)" |
|
397 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
398 |
|
399 lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \<Longrightarrow> |
|
400 (wtpd_expr E e) & (wtpd_stmt E s1) & (wtpd_stmt E s2) |
|
401 & (E\<turnstile>e::PrimT Boolean)" |
|
402 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
403 |
|
404 lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \<Longrightarrow> |
|
405 (wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)" |
|
406 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
407 |
|
408 lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps)) |
|
409 \<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps) |
|
410 & (length ps = length pTs') & (E\<turnstile>a::Class C) |
|
411 & (\<exists> pTs md rT. |
|
412 E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})" |
|
413 apply (simp only: wtpd_expr_def wtpd_exprs_def) |
|
414 apply (erule exE) |
|
415 apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T") |
|
416 apply (auto simp: max_spec_preserves_length) |
|
417 done |
|
418 |
|
419 lemma wtpd_blk: |
|
420 "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); |
|
421 wf_prog wf_java_mdecl G; is_class G D \<rbrakk> |
|
422 \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk" |
|
423 apply (simp add: wtpd_stmt_def env_of_jmb_def) |
|
424 apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves) |
|
425 apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
426 done |
|
427 |
|
428 lemma wtpd_res: |
|
429 "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); |
|
430 wf_prog wf_java_mdecl G; is_class G D \<rbrakk> |
|
431 \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res" |
|
432 apply (simp add: wtpd_expr_def env_of_jmb_def) |
|
433 apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves) |
|
434 apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
435 done |
|
436 |
|
437 |
|
438 (**********************************************************************) |
|
439 |
|
440 |
|
441 (* Is there a more elegant proof? *) |
|
442 lemma evals_preserves_length: |
|
443 "G\<turnstile> xs -es[\<succ>]vs-> (None, s) \<Longrightarrow> length es = length vs" |
|
444 apply (subgoal_tac |
|
445 "\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & |
|
446 (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow> (\<exists> s. (xs' = (None, s))) \<longrightarrow> |
|
447 length es = length vs) & |
|
448 ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)") |
|
449 apply blast |
|
450 apply (rule allI) |
|
451 apply (rule Eval.eval_evals_exec.induct) |
|
452 apply auto |
|
453 done |
|
454 |
|
455 (***********************************************************************) |
|
456 |
|
457 (* required for translation of BinOp *) |
|
458 |
|
459 |
|
460 lemma progression_Eq : "{G, C, S} \<turnstile> |
|
461 {hp, (v2 # v1 # os), lvars} |
|
462 >- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow> |
|
463 {hp, (Bool (v1 = v2) # os), lvars}" |
|
464 apply (case_tac "v1 = v2") |
|
465 |
|
466 (* case v1 = v2 *) |
|
467 apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression) |
|
468 apply (auto simp: NatBin.nat_add_distrib) |
|
469 apply (rule progression_one_step) apply simp |
|
470 |
|
471 (* case v1 \<noteq> v2 *) |
|
472 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
|
473 apply auto |
|
474 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
|
475 apply auto |
|
476 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
|
477 apply (auto simp: NatBin.nat_add_distrib intro: progression_refl) |
|
478 done |
|
479 |
|
480 |
|
481 (**********************************************************************) |
|
482 |
|
483 |
|
484 (* to avoid automatic pair splits *) |
|
485 |
|
486 declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
487 ML_setup {* |
|
488 simpset_ref() := simpset() delloop "split_all_tac" |
|
489 *} |
|
490 |
|
491 lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; |
|
492 method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
493 distinct (gjmb_plns (gmb G C S))" |
|
494 apply (frule method_wf_mdecl [THEN conjunct2], assumption, assumption) |
|
495 apply (case_tac S) |
|
496 apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append) |
|
497 apply (simp add: unique_def map_of_in_set) |
|
498 apply blast |
|
499 done |
|
500 |
|
501 lemma distinct_method_if_class_sig_defined : |
|
502 "\<lbrakk> wf_java_prog G; class_sig_defined G C S \<rbrakk> \<Longrightarrow> |
|
503 distinct (gjmb_plns (gmb G C S))" |
|
504 by (auto intro: distinct_method simp: class_sig_defined_def) |
|
505 |
|
506 |
|
507 lemma method_yields_wf_java_mdecl: "\<lbrakk> wf_java_prog G; is_class G C; |
|
508 method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
509 wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))" |
|
510 apply (frule method_wf_mdecl) |
|
511 apply (auto simp: wf_mdecl_def) |
|
512 done |
|
513 |
|
514 (**********************************************************************) |
|
515 |
|
516 |
|
517 lemma progression_lvar_init_aux [rule_format (no_asm)]: " |
|
518 \<forall> zs prfx lvals lvars0. |
|
519 lvars0 = (zs @ lvars) \<longrightarrow> |
|
520 (disjoint_varnames pns lvars0 \<longrightarrow> |
|
521 (length lvars = length lvals) \<longrightarrow> |
|
522 (Suc(length pns + length zs) = length prfx) \<longrightarrow> |
|
523 ({cG, D, S} \<turnstile> |
|
524 {h, os, (prfx @ lvals)} |
|
525 >- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow> |
|
526 {h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))" |
|
527 apply simp |
|
528 apply (induct lvars) |
|
529 apply (clarsimp, rule progression_refl) |
|
530 apply (intro strip) |
|
531 apply (case_tac lvals) apply simp |
|
532 apply (simp (no_asm_simp) ) |
|
533 |
|
534 apply (rule_tac "lvars1.0" = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl) |
|
535 apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def) |
|
536 apply (rule_tac "instrs0.0" = "[load_default_val b]" in progression_transitive, simp) |
|
537 apply (rule progression_one_step) |
|
538 apply (simp (no_asm_simp) add: load_default_val_def) |
|
539 apply (rule conjI, simp)+ apply (rule HOL.refl) |
|
540 |
|
541 apply (rule progression_one_step) |
|
542 apply (simp (no_asm_simp)) |
|
543 apply (rule conjI, simp)+ |
|
544 apply (simp add: index_of_var2) |
|
545 apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *) |
|
546 apply (drule mp, simp) |
|
547 apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *) |
|
548 apply auto |
|
549 done |
|
550 |
|
551 lemma progression_lvar_init [rule_format (no_asm)]: |
|
552 "\<lbrakk> wf_java_prog G; is_class G C; |
|
553 method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
554 length pns = length pvs \<longrightarrow> |
|
555 (\<forall> lvals. |
|
556 length lvars = length lvals \<longrightarrow> |
|
557 {cG, D, S} \<turnstile> |
|
558 {h, os, (a' # pvs @ lvals)} |
|
559 >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow> |
|
560 {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})" |
|
561 apply (simp only: compInitLvars_def) |
|
562 apply (frule method_yields_wf_java_mdecl, assumption, assumption) |
|
563 |
|
564 apply (simp only: wf_java_mdecl_def) |
|
565 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))") |
|
566 apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd) |
|
567 apply (intro strip) |
|
568 apply (simp (no_asm_simp) only: append_Cons [THEN sym]) |
|
569 apply (rule progression_lvar_init_aux) |
|
570 apply (auto simp: unique_def map_of_in_set disjoint_varnames_def) |
|
571 done |
|
572 |
|
573 |
|
574 |
|
575 |
|
576 |
|
577 |
|
578 |
|
579 |
|
580 |
|
581 (**********************************************************************) |
|
582 |
|
583 constdefs |
|
584 state_ok :: "java_mb env \<Rightarrow> xstate \<Rightarrow> bool" |
|
585 "state_ok E xs == xs::\<preceq>E" |
|
586 |
|
587 |
|
588 lemma state_ok_eval: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_expr E e; |
|
589 (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow> state_ok E xs'" |
|
590 apply (simp only: state_ok_def wtpd_expr_def) |
|
591 apply (erule exE) |
|
592 apply (case_tac xs', case_tac xs, simp only:) |
|
593 apply (rule eval_type_sound [THEN conjunct1]) |
|
594 apply (rule HOL.refl) |
|
595 apply assumption |
|
596 apply (subgoal_tac "fst E \<turnstile> (gx xs, gs xs) -e\<succ>v-> (gx xs', gs xs')") |
|
597 apply assumption |
|
598 apply (auto simp: gx_def gs_def) |
|
599 done |
|
600 |
|
601 (* to be moved into JTypeSafe.thy *) |
|
602 lemma evals_type_sound: "!!E s s'. |
|
603 [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |] |
|
604 ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)" |
|
605 apply( simp (no_asm_simp) only: split_tupled_all) |
|
606 apply (drule eval_evals_exec_type_sound |
|
607 [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
|
608 apply auto |
|
609 done |
|
610 |
|
611 lemma state_ok_evals: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_exprs E es; |
|
612 (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> state_ok E xs'" |
|
613 apply (simp only: state_ok_def wtpd_exprs_def) |
|
614 apply (erule exE) |
|
615 apply (case_tac xs) apply (case_tac xs') apply (simp only:) |
|
616 apply (rule evals_type_sound [THEN conjunct1]) |
|
617 apply (auto simp: gx_def gs_def) |
|
618 done |
|
619 |
|
620 lemma state_ok_exec: "\<lbrakk>state_ok E xs; wf_java_prog (prg E); wtpd_stmt E st; |
|
621 (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow> state_ok E xs'" |
|
622 apply (simp only: state_ok_def wtpd_stmt_def) |
|
623 apply (case_tac xs', case_tac xs, simp only:) |
|
624 apply (rule exec_type_sound) |
|
625 apply (rule HOL.refl) |
|
626 apply assumption |
|
627 apply (subgoal_tac "((gx xs, gs xs), st, (gx xs', gs xs')) \<in> Eval.exec (fst E)") |
|
628 apply assumption |
|
629 apply (auto simp: gx_def gs_def) |
|
630 done |
|
631 |
|
632 |
|
633 lemma state_ok_init: |
|
634 "\<lbrakk> wf_java_prog G; state_ok (env_of_jmb G C S) (x, h, l); |
|
635 is_class G dynT; |
|
636 method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res); |
|
637 list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk> |
|
638 \<Longrightarrow> |
|
639 state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" |
|
640 apply (frule method_in_md [THEN conjunct2], assumption+) |
|
641 apply (frule method_yields_wf_java_mdecl, assumption, assumption) |
|
642 apply (simp add: state_ok_def env_of_jmb_def gs_def conforms_def split_beta) |
|
643 apply (simp add: wf_java_mdecl_def) |
|
644 apply (rule conjI) |
|
645 apply (rule lconf_ext) |
|
646 apply (rule lconf_ext_list) |
|
647 apply (rule lconf_init_vars) |
|
648 apply (auto dest: Ball_set_table) |
|
649 apply (simp add: np_def xconf_raise_if) |
|
650 done |
|
651 |
|
652 |
|
653 lemma ty_exprs_list_all2 [rule_format (no_asm)]: |
|
654 "(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)" |
|
655 apply (rule list.induct) |
|
656 apply simp |
|
657 apply (rule allI) |
|
658 apply (rule iffI) |
|
659 apply (ind_cases "E \<turnstile> [] [::] Ts", assumption) |
|
660 apply simp apply (rule WellType.Nil) |
|
661 apply (simp add: list_all2_Cons1) |
|
662 apply (rule allI) |
|
663 apply (rule iffI) |
|
664 apply (rename_tac a exs Ts) |
|
665 apply (ind_cases "E \<turnstile> a # exs [::] Ts") apply blast |
|
666 apply (auto intro: WellType.Cons) |
|
667 done |
|
668 |
|
669 |
|
670 lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b" |
|
671 apply (simp add: conf_def) |
|
672 apply (erule exE) |
|
673 apply (case_tac v) |
|
674 apply (auto elim: widen.cases) |
|
675 done |
|
676 |
|
677 |
|
678 lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; wf_prog wf_mb (prg E)\<rbrakk> |
|
679 \<Longrightarrow> is_class (prg E) C" |
|
680 by (case_tac E, auto dest: ty_expr_is_type) |
|
681 |
|
682 |
|
683 lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> |
|
684 list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'" |
|
685 by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD) |
|
686 |
|
687 |
|
688 lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; state_ok E s; |
|
689 E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> |
|
690 \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T" |
|
691 apply (simp add: gh_def) |
|
692 apply (rule_tac x2="fst s" and "s2"="snd s"and "x'2"="fst s'" |
|
693 in eval_type_sound [THEN conjunct2 [THEN mp], simplified]) |
|
694 apply (rule sym) apply assumption |
|
695 apply assumption |
|
696 apply (simp (no_asm_use) add: surjective_pairing [THEN sym]) |
|
697 apply (simp only: state_ok_def gs_def) |
|
698 apply (case_tac s, simp) |
|
699 apply assumption |
|
700 apply (simp add: gx_def) |
|
701 done |
|
702 |
|
703 lemma evals_preserves_conf: |
|
704 "\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts; |
|
705 wf_java_prog G; state_ok E s; |
|
706 prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T" |
|
707 apply (subgoal_tac "gh s\<le>| gh s'") |
|
708 apply (frule conf_hext, assumption, assumption) |
|
709 apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) |
|
710 apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))") |
|
711 apply assumption |
|
712 apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym]) |
|
713 apply (case_tac E) |
|
714 apply (simp add: gx_def gs_def gh_def gl_def state_ok_def |
|
715 surjective_pairing [THEN sym]) |
|
716 done |
|
717 |
|
718 lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; |
|
719 wf_java_prog G; state_ok E s; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk> |
|
720 \<Longrightarrow> (\<exists> lc. a' = Addr lc)" |
|
721 apply (case_tac s, case_tac s', simp) |
|
722 apply (frule eval_type_sound, (simp add: state_ok_def gs_def)+) |
|
723 apply (case_tac a') |
|
724 apply (auto simp: conf_def) |
|
725 done |
|
726 |
|
727 |
|
728 lemma dynT_subcls: |
|
729 "\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a'))); |
|
730 is_class G dynT; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C" |
|
731 apply (case_tac "C = Object") |
|
732 apply (simp, rule subcls_C_Object, assumption+) |
|
733 apply (frule non_np_objD, auto) |
|
734 done |
|
735 |
|
736 |
|
737 lemma method_defined: "\<lbrakk> |
|
738 m = the (method (G, dynT) (mn, pTs)); |
|
739 dynT = fst (the (h a)); is_class G dynT; wf_java_prog G; |
|
740 a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; a = the_Addr a'; |
|
741 \<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk> |
|
742 \<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m" |
|
743 apply (erule exE)+ |
|
744 apply (drule singleton_in_set, drule max_spec2appl_meths) |
|
745 apply (simp add: appl_methds_def) |
|
746 apply ((erule exE)+, (erule conjE)+, (erule exE)+) |
|
747 apply (drule widen_methd) |
|
748 apply assumption |
|
749 apply (rule dynT_subcls, assumption+, simp, assumption+) |
|
750 apply (erule exE)+ apply simp |
|
751 done |
|
752 |
|
753 |
|
754 |
|
755 (**********************************************************************) |
|
756 |
|
757 |
|
758 (* 1. any difference between locvars_xstate \<dots> and L ??? *) |
|
759 (* 2. possibly skip env_of_jmb ??? *) |
|
760 theorem compiler_correctness: |
|
761 "wf_java_prog G \<Longrightarrow> |
|
762 ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> |
|
763 gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
|
764 (\<forall> os CL S. |
|
765 (class_sig_defined G CL S) \<longrightarrow> |
|
766 (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow> |
|
767 (state_ok (env_of_jmb G CL S) xs) \<longrightarrow> |
|
768 ( {TranslComp.comp G, CL, S} \<turnstile> |
|
769 {gh xs, os, (locvars_xstate G CL S xs)} |
|
770 >- (compExpr (gmb G CL S) ex) \<rightarrow> |
|
771 {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> |
|
772 |
|
773 ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> |
|
774 gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
|
775 (\<forall> os CL S. |
|
776 (class_sig_defined G CL S) \<longrightarrow> |
|
777 (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow> |
|
778 (state_ok (env_of_jmb G CL S) xs) \<longrightarrow> |
|
779 ( {TranslComp.comp G, CL, S} \<turnstile> |
|
780 {gh xs, os, (locvars_xstate G CL S xs)} |
|
781 >- (compExprs (gmb G CL S) exs) \<rightarrow> |
|
782 {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> |
|
783 |
|
784 ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> |
|
785 gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
|
786 (\<forall> os CL S. |
|
787 (class_sig_defined G CL S) \<longrightarrow> |
|
788 (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow> |
|
789 (state_ok (env_of_jmb G CL S) xs) \<longrightarrow> |
|
790 ( {TranslComp.comp G, CL, S} \<turnstile> |
|
791 {gh xs, os, (locvars_xstate G CL S xs)} |
|
792 >- (compStmt (gmb G CL S) st) \<rightarrow> |
|
793 {gh xs', os, (locvars_xstate G CL S xs')})))" |
|
794 apply (rule Eval.eval_evals_exec.induct) |
|
795 |
|
796 (* case XcptE *) |
|
797 apply simp |
|
798 |
|
799 (* case NewC *) |
|
800 apply clarify |
|
801 apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *) |
|
802 apply (simp add: c_hupd_hp_invariant) |
|
803 apply (rule progression_one_step) |
|
804 apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *) |
|
805 apply (simp add: locvars_xstate_def locvars_locals_def comp_fields) |
|
806 |
|
807 |
|
808 (* case Cast *) |
|
809 apply (intro allI impI) |
|
810 apply simp |
|
811 apply (frule raise_if_NoneD) |
|
812 apply (frule wtpd_expr_cast) |
|
813 apply simp |
|
814 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, simp) |
|
815 apply blast |
|
816 apply (rule progression_one_step) |
|
817 apply (simp add: raise_system_xcpt_def gh_def comp_cast_ok) |
|
818 |
|
819 |
|
820 (* case Lit *) |
|
821 apply simp |
|
822 apply (intro strip) |
|
823 apply (rule progression_one_step) |
|
824 apply simp |
|
825 |
|
826 |
|
827 (* case BinOp *) |
|
828 apply (intro allI impI) |
|
829 apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *) |
|
830 apply (frule wtpd_expr_binop) |
|
831 (* establish (state_ok \<dots> s1) *) |
|
832 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
833 |
|
834 |
|
835 apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
836 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast |
|
837 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast |
|
838 apply (case_tac bop) |
|
839 (*subcase bop = Eq *) apply simp apply (rule progression_Eq) |
|
840 (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp |
|
841 |
|
842 |
|
843 (* case LAcc *) |
|
844 apply simp |
|
845 apply (intro strip) |
|
846 apply (rule progression_one_step) |
|
847 apply (simp add: locvars_xstate_def locvars_locals_def) |
|
848 apply (frule wtpd_expr_lacc) |
|
849 apply assumption |
|
850 apply (simp add: gl_def) |
|
851 apply (erule select_at_index) |
|
852 |
|
853 |
|
854 (* case LAss *) |
|
855 apply (intro allI impI) |
|
856 apply (frule wtpd_expr_lass, erule conjE, erule conjE) |
|
857 apply (simp add: compExpr_compExprs.simps) |
|
858 |
|
859 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
|
860 apply blast |
|
861 |
|
862 apply (rule_tac "instrs0.0" = "[Dup]" in progression_transitive, simp) |
|
863 apply (rule progression_one_step) |
|
864 apply (simp add: gh_def) |
|
865 apply (rule conjI, simp)+ apply simp |
|
866 apply (rule progression_one_step) |
|
867 apply (simp add: gh_def) |
|
868 (* the following falls out of the general scheme *) |
|
869 apply (frule wtpd_expr_lacc) apply assumption |
|
870 apply (rule update_at_index) |
|
871 apply (rule distinct_method_if_class_sig_defined) apply assumption |
|
872 apply assumption apply simp apply assumption |
|
873 |
|
874 |
|
875 (* case FAcc *) |
|
876 apply (intro allI impI) |
|
877 (* establish x1 = None \<and> a' \<noteq> Null *) |
|
878 apply (simp (no_asm_use) only: gx_conv, frule np_NoneD) |
|
879 apply (frule wtpd_expr_facc) |
|
880 |
|
881 apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
882 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
|
883 apply blast |
|
884 apply (rule progression_one_step) |
|
885 apply (simp add: gh_def) |
|
886 apply (case_tac "(the (fst s1 (the_Addr a')))") |
|
887 apply (simp add: raise_system_xcpt_def) |
|
888 |
|
889 |
|
890 (* case FAss *) |
|
891 apply (intro allI impI) |
|
892 apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc) |
|
893 apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *) |
|
894 (* establish x1 = None and a' \<noteq> Null *) |
|
895 apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt) |
|
896 apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE) |
|
897 |
|
898 |
|
899 (* establish (state_ok \<dots> (Norm s1)) *) |
|
900 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
901 |
|
902 apply (simp only: compExpr_compExprs.simps) |
|
903 |
|
904 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl) |
|
905 apply fast (* blast does not seem to work - why? *) |
|
906 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl) |
|
907 apply fast |
|
908 apply (rule_tac "instrs0.0" = "[Dup_x1]" and "instrs1.0" = "[Putfield fn T]" in progression_transitive, simp) |
|
909 |
|
910 (* Dup_x1 *) |
|
911 apply (rule progression_one_step) |
|
912 apply (simp add: gh_def) |
|
913 apply (rule conjI, simp)+ apply simp |
|
914 |
|
915 |
|
916 (* Putfield \<longrightarrow> still looks nasty*) |
|
917 apply (rule progression_one_step) |
|
918 apply simp |
|
919 apply (case_tac "(the (fst s2 (the_Addr a')))") |
|
920 apply (simp add: c_hupd_hp_invariant) |
|
921 apply (case_tac s2) |
|
922 apply (simp add: c_hupd_conv raise_system_xcpt_def) |
|
923 apply (rule locvars_xstate_par_dep, rule HOL.refl) |
|
924 |
|
925 defer (* method call *) |
|
926 |
|
927 (* case XcptEs *) |
|
928 apply simp |
|
929 |
|
930 (* case Nil *) |
|
931 apply (simp add: compExpr_compExprs.simps) |
|
932 apply (intro strip) |
|
933 apply (rule progression_refl) |
|
934 |
|
935 (* case Cons *) |
|
936 apply (intro allI impI) |
|
937 apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *) |
|
938 apply (frule wtpd_exprs_cons) |
|
939 (* establish (state_ok \<dots> (Norm s0)) *) |
|
940 apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
941 |
|
942 apply simp |
|
943 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
|
944 apply fast |
|
945 apply fast |
|
946 |
|
947 |
|
948 (* case Statement: exception *) |
|
949 apply simp |
|
950 |
|
951 (* case Skip *) |
|
952 apply (intro allI impI) |
|
953 apply simp |
|
954 apply (rule progression_refl) |
|
955 |
|
956 (* case Expr *) |
|
957 apply (intro allI impI) |
|
958 apply (frule wtpd_stmt_expr) |
|
959 apply simp |
|
960 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
|
961 apply fast |
|
962 apply (rule progression_one_step) |
|
963 apply simp |
|
964 |
|
965 (* case Comp *) |
|
966 apply (intro allI impI) |
|
967 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
968 apply (frule wtpd_stmt_comp) |
|
969 |
|
970 (* establish (state_ok \<dots> s1) *) |
|
971 apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
972 |
|
973 apply simp |
|
974 apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl) |
|
975 apply fast |
|
976 apply fast |
|
977 |
|
978 |
|
979 (* case Cond *) |
|
980 apply (intro allI impI) |
|
981 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
982 apply (frule wtpd_stmt_cond, (erule conjE)+) |
|
983 (* establish (state_ok \<dots> s1) *) |
|
984 apply (frule_tac e=e in state_ok_eval) |
|
985 apply (simp (no_asm_simp) only: env_of_jmb_fst) |
|
986 apply assumption |
|
987 apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
988 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
989 apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
990 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
991 apply (erule exE) |
|
992 |
|
993 apply simp |
|
994 apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
|
995 apply (rule progression_one_step, simp) |
|
996 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
997 |
|
998 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
|
999 apply fast |
|
1000 |
|
1001 apply (case_tac b) |
|
1002 (* case b= True *) |
|
1003 apply simp |
|
1004 apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp) |
|
1005 apply (rule progression_one_step) apply simp |
|
1006 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
1007 apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp) |
|
1008 apply fast |
|
1009 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
|
1010 apply (simp, rule conjI, (rule HOL.refl)+) |
|
1011 apply simp apply (rule conjI, simp) apply (simp add: NatBin.nat_add_distrib) |
|
1012 apply (rule progression_refl) |
|
1013 |
|
1014 (* case b= False *) |
|
1015 apply simp |
|
1016 apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression) |
|
1017 apply (simp, rule conjI, (rule HOL.refl)+) |
|
1018 apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib) |
|
1019 apply fast |
|
1020 |
|
1021 (* case exit Loop *) |
|
1022 apply (intro allI impI) |
|
1023 apply (frule wtpd_stmt_loop, (erule conjE)+) |
|
1024 |
|
1025 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
1026 apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
1027 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
1028 apply (erule exE) |
|
1029 apply (case_tac b) |
|
1030 |
|
1031 (* case b= True \<longrightarrow> contradiction *) |
|
1032 apply simp |
|
1033 |
|
1034 (* case b= False *) |
|
1035 apply simp |
|
1036 |
|
1037 apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
|
1038 apply (rule progression_one_step) |
|
1039 apply simp |
|
1040 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
1041 |
|
1042 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
|
1043 apply fast |
|
1044 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
|
1045 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl) |
|
1046 apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib) |
|
1047 apply (rule progression_refl) |
|
1048 |
|
1049 |
|
1050 (* case continue Loop *) |
|
1051 apply (intro allI impI) |
|
1052 apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *) |
|
1053 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
1054 apply (frule wtpd_stmt_loop, (erule conjE)+) |
|
1055 |
|
1056 (* establish (state_ok \<dots> s1) *) |
|
1057 apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
1058 (* establish (state_ok \<dots> s2) *) |
|
1059 apply (frule_tac xs=s1 and st=c in state_ok_exec) |
|
1060 apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
1061 |
|
1062 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
1063 apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
1064 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
1065 apply (erule exE) |
|
1066 |
|
1067 apply simp |
|
1068 apply (rule jump_bwd_progression) |
|
1069 apply simp |
|
1070 apply (rule conjI, (rule HOL.refl)+) |
|
1071 |
|
1072 apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
|
1073 apply (rule progression_one_step) |
|
1074 apply simp |
|
1075 apply (rule conjI, simp)+ apply simp |
|
1076 |
|
1077 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
|
1078 apply fast |
|
1079 |
|
1080 apply (case_tac b) |
|
1081 (* case b= True *) |
|
1082 apply simp |
|
1083 |
|
1084 apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp) |
|
1085 apply (rule progression_one_step) apply simp |
|
1086 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
1087 apply fast |
|
1088 |
|
1089 (* case b= False \<longrightarrow> contradiction*) |
|
1090 apply simp |
|
1091 |
|
1092 apply (rule jump_bwd_one_step) |
|
1093 apply simp |
|
1094 apply blast |
|
1095 |
|
1096 (*****) |
|
1097 (* case method call *) defer (* !!! NEWC *) |
|
1098 |
|
1099 apply (intro allI impI) |
|
1100 |
|
1101 apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *) |
|
1102 apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *) |
|
1103 apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *) |
|
1104 |
|
1105 apply (frule wtpd_expr_call, (erule conjE)+) |
|
1106 |
|
1107 |
|
1108 (* assumptions about state_ok and is_class *) |
|
1109 |
|
1110 (* establish state_ok (env_of_jmb G CL S) s1 *) |
|
1111 apply (frule_tac xs="Norm s0" and e=e in state_ok_eval) |
|
1112 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst) |
|
1113 |
|
1114 (* establish state_ok (env_of_jmb G CL S) (x, h, l) *) |
|
1115 apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals) |
|
1116 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst) |
|
1117 |
|
1118 (* establish \<exists> lc. a' = Addr lc *) |
|
1119 apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym]) |
|
1120 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C") |
|
1121 apply (subgoal_tac "is_class G dynT") |
|
1122 |
|
1123 (* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *) |
|
1124 apply (drule method_defined, assumption+) |
|
1125 apply (simp only: env_of_jmb_fst) |
|
1126 apply ((erule exE)+, erule conjE, (rule exI)+, assumption) |
|
1127 |
|
1128 apply (subgoal_tac "is_class G md") |
|
1129 apply (subgoal_tac "G\<turnstile>Class dynT \<preceq> Class md") |
|
1130 apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)") |
|
1131 apply (subgoal_tac "list_all2 (conf G h) pvs pTs") |
|
1132 |
|
1133 (* establish state_ok (env_of_jmb G md (mn, pTs)) (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a')) *) |
|
1134 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT") |
|
1135 apply (frule (2) conf_widen) |
|
1136 apply (frule state_ok_init, assumption+) |
|
1137 |
|
1138 apply (subgoal_tac "class_sig_defined G md (mn, pTs)") |
|
1139 apply (frule wtpd_blk, assumption, assumption) |
|
1140 apply (frule wtpd_res, assumption, assumption) |
|
1141 apply (subgoal_tac "state_ok (env_of_jmb G md (mn, pTs)) s3") |
|
1142 |
|
1143 (* establish method (TranslComp.comp G, md) (mn, pTs) = |
|
1144 Some (md, rT, compMethod (pns, lvars, blk, res)) *) |
|
1145 apply (frule_tac C=md and D=md in comp_method, assumption, assumption) |
|
1146 |
|
1147 (* establish |
|
1148 method (TranslComp.comp G, dynT) (mn, pTs) = |
|
1149 Some (md, rT, compMethod (pns, lvars, blk, res)) *) |
|
1150 apply (frule_tac C=dynT and D=md in comp_method, assumption, assumption) |
|
1151 apply (simp only: fst_conv snd_conv) |
|
1152 |
|
1153 (* establish length pns = length pTs *) |
|
1154 apply (frule method_preserves_length, assumption, assumption) |
|
1155 (* establish length pvs = length ps *) |
|
1156 apply (frule evals_preserves_length [THEN sym]) |
|
1157 |
|
1158 (** start evaluating subexpressions **) |
|
1159 apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
1160 |
|
1161 (* evaluate e *) |
|
1162 apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
|
1163 apply fast |
|
1164 |
|
1165 (* evaluate parameters *) |
|
1166 apply (rule_tac "instrs0.0" = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl) |
|
1167 apply fast |
|
1168 |
|
1169 (* invokation *) |
|
1170 apply (rule progression_call) |
|
1171 apply (intro allI impI conjI) |
|
1172 (* execute Invoke statement *) |
|
1173 apply (simp (no_asm_use) only: exec_instr.simps) |
|
1174 apply (erule thin_rl, erule thin_rl, erule thin_rl) |
|
1175 apply (simp add: compMethod_def raise_system_xcpt_def) |
|
1176 apply (rule conjI, simp)+ apply (rule HOL.refl) |
|
1177 |
|
1178 (* get instructions of invoked method *) |
|
1179 apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def) |
|
1180 |
|
1181 (* var. initialization *) |
|
1182 apply (rule_tac "instrs0.0" = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl) |
|
1183 apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption) |
|
1184 apply (simp (no_asm_simp)) (* length pns = length pvs *) |
|
1185 apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *) |
|
1186 |
|
1187 |
|
1188 (* body statement *) |
|
1189 apply (rule_tac "instrs0.0" = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl) |
|
1190 apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)") |
|
1191 apply (simp (no_asm_simp)) |
|
1192 apply (simp only: gh_conv) |
|
1193 apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption) |
|
1194 apply (simp (no_asm_use)) |
|
1195 apply (simp (no_asm_simp) add: gmb_def) |
|
1196 |
|
1197 (* return expression *) |
|
1198 apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)") |
|
1199 apply (simp (no_asm_simp)) |
|
1200 apply (simp only: gh_conv) |
|
1201 apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption) |
|
1202 apply (simp (no_asm_use)) |
|
1203 apply (simp (no_asm_simp) add: gmb_def) |
|
1204 |
|
1205 (* execute return statement *) |
|
1206 apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append) |
|
1207 apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os") |
|
1208 apply (simp only: drop_append) |
|
1209 apply (simp (no_asm_simp)) |
|
1210 apply (simp (no_asm_simp)) |
|
1211 |
|
1212 (* show state_ok \<dots> s3 *) |
|
1213 apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec) |
|
1214 apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) |
|
1215 apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
1216 |
|
1217 (* show class_sig_defined G md (mn, pTs) *) |
|
1218 apply (simp (no_asm_simp) add: class_sig_defined_def) |
|
1219 |
|
1220 (* show G,h \<turnstile> a' ::\<preceq> Class dynT *) |
|
1221 apply (frule non_npD) apply assumption |
|
1222 apply (erule exE)+ apply simp |
|
1223 apply (rule conf_obj_AddrI) apply simp |
|
1224 apply (rule conjI, (rule HOL.refl)+) |
|
1225 apply (rule widen_Class_Class [THEN iffD1], rule widen.refl) |
|
1226 |
|
1227 |
|
1228 (* show list_all2 (conf G h) pvs pTs *) |
|
1229 apply (erule exE)+ apply (erule conjE)+ |
|
1230 apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption |
|
1231 apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G") |
|
1232 apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound) |
|
1233 apply (simp only: env_of_jmb_fst) |
|
1234 apply assumption apply (simp only: state_ok_def) |
|
1235 apply (simp add: conforms_def xconf_def gs_def) |
|
1236 apply simp |
|
1237 apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym]) |
|
1238 apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp |
|
1239 apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym]) |
|
1240 (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *) |
|
1241 apply (rule max_spec_widen, simp only: env_of_jmb_fst) |
|
1242 |
|
1243 |
|
1244 (* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *) |
|
1245 apply (frule method_in_md [THEN conjunct2], assumption+) |
|
1246 |
|
1247 (* show G\<turnstile>Class dynT \<preceq> Class md *) |
|
1248 apply (simp (no_asm_use) only: widen_Class_Class) |
|
1249 apply (rule method_wf_mdecl [THEN conjunct1], assumption+) |
|
1250 |
|
1251 (* is_class G md *) |
|
1252 apply (rule method_in_md [THEN conjunct1], assumption+) |
|
1253 |
|
1254 (* show is_class G dynT *) |
|
1255 apply (frule non_npD) apply assumption |
|
1256 apply (erule exE)+ apply (erule conjE)+ |
|
1257 apply simp |
|
1258 apply (rule subcls_is_class2) apply assumption |
|
1259 apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst) |
|
1260 apply (simp only: env_of_jmb_fst) |
|
1261 |
|
1262 (* show G,h \<turnstile> a' ::\<preceq> Class C *) |
|
1263 apply (simp only: wtpd_exprs_def, erule exE) |
|
1264 apply (frule evals_preserves_conf) |
|
1265 apply (rule eval_conf, assumption+) |
|
1266 apply (rule env_of_jmb_fst, assumption+) |
|
1267 apply (rule env_of_jmb_fst) |
|
1268 apply (simp only: gh_conv) |
|
1269 done |
|
1270 |
|
1271 |
|
1272 theorem compiler_correctness_eval: " |
|
1273 \<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc'); |
|
1274 wf_java_prog G; |
|
1275 class_sig_defined G C S; |
|
1276 wtpd_expr (env_of_jmb G C S) ex; |
|
1277 (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow> |
|
1278 {(TranslComp.comp G), C, S} \<turnstile> |
|
1279 {hp, os, (locvars_locals G C S loc)} |
|
1280 >- (compExpr (gmb G C S) ex) \<rightarrow> |
|
1281 {hp', val#os, (locvars_locals G C S loc')}" |
|
1282 apply (frule compiler_correctness [THEN conjunct1]) |
|
1283 apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def) |
|
1284 done |
|
1285 |
|
1286 theorem compiler_correctness_exec: " |
|
1287 \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G; |
|
1288 wf_java_prog G; |
|
1289 class_sig_defined G C S; |
|
1290 wtpd_stmt (env_of_jmb G C S) st; |
|
1291 (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow> |
|
1292 {(TranslComp.comp G), C, S} \<turnstile> |
|
1293 {hp, os, (locvars_locals G C S loc)} |
|
1294 >- (compStmt (gmb G C S) st) \<rightarrow> |
|
1295 {hp', os, (locvars_locals G C S loc')}" |
|
1296 apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]]) |
|
1297 apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def state_ok_def) |
|
1298 done |
|
1299 |
|
1300 (**********************************************************************) |
|
1301 |
|
1302 |
|
1303 (* reinstall pair splits *) |
|
1304 declare split_paired_All [simp] split_paired_Ex [simp] |
|
1305 ML_setup {* |
|
1306 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
|
1307 *} |
|
1308 |
|
1309 end |