author | haftmann |
Tue, 24 Nov 2009 14:37:23 +0100 | |
changeset 33954 | 1bc3b688548c |
parent 33639 | 603320b93668 |
child 35416 | d8d7d1b785af |
permissions | -rwxr-xr-x |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/CorrComp.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
5 |
(* Compiler correctness statement and proof *) |
|
6 |
||
15860 | 7 |
theory CorrComp |
15866 | 8 |
imports "../J/JTypeSafe" "LemmasComp" |
15860 | 9 |
begin |
13673 | 10 |
|
14045 | 11 |
declare wf_prog_ws_prog [simp add] |
13673 | 12 |
|
13 |
(* If no exception is present after evaluation/execution, |
|
14 |
none can have been present before *) |
|
15 |
lemma eval_evals_exec_xcpt: |
|
22271 | 16 |
"(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
17 |
(G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and> |
|
18 |
(G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)" |
|
13673 | 19 |
by (induct rule: eval_evals_exec.induct, auto) |
20 |
||
21 |
||
22 |
(* instance of eval_evals_exec_xcpt for eval *) |
|
22271 | 23 |
lemma eval_xcpt: "G \<turnstile> xs -ex\<succ>val-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
13673 | 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 *) |
|
22271 | 32 |
lemma evals_xcpt: "G \<turnstile> xs -exs[\<succ>]vals-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
13673 | 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 *) |
|
22271 | 41 |
lemma exec_xcpt: "G \<turnstile> xs -st-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None" |
13673 | 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" |
|
15097
b807858b97bd
Modifications for trancl_tac (new solver in simplifier).
ballarin
parents:
15076
diff
changeset
|
56 |
by (simp only: exec_all_def) |
13673 | 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) |
|
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24074
diff
changeset
|
120 |
apply (simp only: list.simps list.size) |
13673 | 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) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
135 |
apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S, |
13673 | 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) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
194 |
apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans) |
13673 | 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 |
lemma method_preserves [rule_format (no_asm)]: |
|
282 |
"\<lbrakk> wf_prog wf_mb G; is_class G C; |
|
283 |
\<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> |
|
284 |
\<Longrightarrow> \<forall> D. |
|
285 |
method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))" |
|
286 |
||
14045 | 287 |
apply (frule wf_prog_ws_prog [THEN wf_subcls1]) |
13673 | 288 |
apply (rule subcls1_induct, assumption, assumption) |
289 |
||
290 |
apply (intro strip) |
|
291 |
apply ((drule spec)+, drule_tac x="Object" in bspec) |
|
14045 | 292 |
apply (simp add: wf_prog_def ws_prog_def wf_syscls_def) |
13673 | 293 |
apply (subgoal_tac "D=Object") apply simp |
294 |
apply (drule mp) |
|
295 |
apply (frule_tac C=Object in method_wf_mdecl) |
|
14045 | 296 |
apply simp |
297 |
apply assumption apply simp apply assumption apply simp |
|
13673 | 298 |
|
15481 | 299 |
apply (simplesubst method_rec) apply simp |
13673 | 300 |
apply force |
14045 | 301 |
apply simp |
14025 | 302 |
apply (simp only: map_add_def) |
13673 | 303 |
apply (split option.split) |
304 |
apply (rule conjI) |
|
305 |
apply force |
|
306 |
apply (intro strip) |
|
307 |
apply (frule_tac |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
308 |
?P1.0 = "wf_mdecl wf_mb G Ca" and |
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
309 |
?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop) |
13673 | 310 |
apply (force simp: wf_cdecl_def) |
311 |
||
312 |
apply clarify |
|
313 |
||
314 |
apply (simp only: class_def) |
|
315 |
apply (drule map_of_SomeD)+ |
|
316 |
apply (frule_tac A="set G" and f=fst in imageI, simp) |
|
317 |
apply blast |
|
318 |
apply simp |
|
319 |
done |
|
320 |
||
321 |
||
322 |
lemma method_preserves_length: |
|
323 |
"\<lbrakk> wf_java_prog G; is_class G C; |
|
324 |
method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk> |
|
325 |
\<Longrightarrow> length pns = length pTs" |
|
326 |
apply (frule_tac |
|
327 |
P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs" |
|
328 |
in method_preserves) |
|
329 |
apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
330 |
done |
|
331 |
||
332 |
(**********************************************************************) |
|
333 |
||
334 |
constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool" |
|
335 |
"wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)" |
|
336 |
wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool" |
|
337 |
"wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)" |
|
338 |
wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" |
|
339 |
"wtpd_stmt E c == (E\<turnstile>c \<surd>)" |
|
340 |
||
341 |
lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C" |
|
342 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
343 |
||
344 |
lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \<Longrightarrow> (wtpd_expr E e)" |
|
345 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
346 |
||
347 |
lemma wtpd_expr_lacc: "\<lbrakk> wtpd_expr (env_of_jmb G C S) (LAcc vn); |
|
348 |
class_sig_defined G C S \<rbrakk> |
|
349 |
\<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This" |
|
350 |
apply (simp only: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs) |
|
351 |
apply clarify |
|
352 |
apply (case_tac S) |
|
353 |
apply simp |
|
354 |
apply (erule ty_expr.cases) |
|
355 |
apply (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
|
356 |
apply (drule map_upds_SomeD) |
|
357 |
apply (erule disjE) |
|
358 |
apply assumption |
|
359 |
apply (drule map_of_SomeD) apply (auto dest: fst_in_set_lemma) |
|
360 |
done |
|
361 |
||
362 |
lemma wtpd_expr_lass: "wtpd_expr E (vn::=e) |
|
363 |
\<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)" |
|
364 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
365 |
||
366 |
lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn) |
|
367 |
\<Longrightarrow> (wtpd_expr E a)" |
|
368 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
369 |
||
370 |
lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v) |
|
371 |
\<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)" |
|
372 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
373 |
||
374 |
||
375 |
lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2) |
|
376 |
\<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)" |
|
377 |
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto) |
|
378 |
||
379 |
lemma wtpd_exprs_cons: "wtpd_exprs E (e # es) |
|
380 |
\<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)" |
|
381 |
by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto) |
|
382 |
||
383 |
lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \<Longrightarrow> (wtpd_expr E e)" |
|
384 |
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
385 |
||
386 |
lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \<Longrightarrow> |
|
387 |
(wtpd_stmt E s1) & (wtpd_stmt E s2)" |
|
388 |
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
389 |
||
390 |
lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \<Longrightarrow> |
|
391 |
(wtpd_expr E e) & (wtpd_stmt E s1) & (wtpd_stmt E s2) |
|
392 |
& (E\<turnstile>e::PrimT Boolean)" |
|
393 |
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
394 |
||
395 |
lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \<Longrightarrow> |
|
396 |
(wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)" |
|
397 |
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto) |
|
398 |
||
399 |
lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps)) |
|
400 |
\<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps) |
|
401 |
& (length ps = length pTs') & (E\<turnstile>a::Class C) |
|
402 |
& (\<exists> pTs md rT. |
|
403 |
E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})" |
|
404 |
apply (simp only: wtpd_expr_def wtpd_exprs_def) |
|
405 |
apply (erule exE) |
|
23757 | 406 |
apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T) |
13673 | 407 |
apply (auto simp: max_spec_preserves_length) |
408 |
done |
|
409 |
||
410 |
lemma wtpd_blk: |
|
411 |
"\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); |
|
412 |
wf_prog wf_java_mdecl G; is_class G D \<rbrakk> |
|
413 |
\<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk" |
|
414 |
apply (simp add: wtpd_stmt_def env_of_jmb_def) |
|
415 |
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) |
|
416 |
apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
417 |
done |
|
418 |
||
419 |
lemma wtpd_res: |
|
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_expr (env_of_jmb G D (md, pTs)) res" |
|
423 |
apply (simp add: wtpd_expr_def env_of_jmb_def) |
|
424 |
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) |
|
425 |
apply (auto simp: wf_mdecl_def wf_java_mdecl_def) |
|
426 |
done |
|
427 |
||
428 |
||
429 |
(**********************************************************************) |
|
430 |
||
431 |
||
432 |
(* Is there a more elegant proof? *) |
|
433 |
lemma evals_preserves_length: |
|
434 |
"G\<turnstile> xs -es[\<succ>]vs-> (None, s) \<Longrightarrow> length es = length vs" |
|
435 |
apply (subgoal_tac |
|
436 |
"\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & |
|
437 |
(G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow> (\<exists> s. (xs' = (None, s))) \<longrightarrow> |
|
438 |
length es = length vs) & |
|
22271 | 439 |
(G \<turnstile> xc -xb-> xa \<longrightarrow> True)") |
13673 | 440 |
apply blast |
441 |
apply (rule allI) |
|
442 |
apply (rule Eval.eval_evals_exec.induct) |
|
443 |
apply auto |
|
444 |
done |
|
445 |
||
446 |
(***********************************************************************) |
|
447 |
||
448 |
(* required for translation of BinOp *) |
|
449 |
||
450 |
||
451 |
lemma progression_Eq : "{G, C, S} \<turnstile> |
|
452 |
{hp, (v2 # v1 # os), lvars} |
|
453 |
>- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow> |
|
454 |
{hp, (Bool (v1 = v2) # os), lvars}" |
|
455 |
apply (case_tac "v1 = v2") |
|
456 |
||
457 |
(* case v1 = v2 *) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
458 |
apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13673
diff
changeset
|
459 |
apply (auto simp: nat_add_distrib) |
13673 | 460 |
apply (rule progression_one_step) apply simp |
461 |
||
462 |
(* case v1 \<noteq> v2 *) |
|
463 |
apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
|
464 |
apply auto |
|
465 |
apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
|
466 |
apply auto |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
467 |
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression) |
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13673
diff
changeset
|
468 |
apply (auto simp: nat_add_distrib intro: progression_refl) |
13673 | 469 |
done |
470 |
||
471 |
||
472 |
(**********************************************************************) |
|
473 |
||
474 |
||
475 |
(* to avoid automatic pair splits *) |
|
476 |
||
477 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
24074 | 478 |
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} |
13673 | 479 |
|
480 |
lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; |
|
481 |
method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
482 |
distinct (gjmb_plns (gmb G C S))" |
|
483 |
apply (frule method_wf_mdecl [THEN conjunct2], assumption, assumption) |
|
484 |
apply (case_tac S) |
|
485 |
apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append) |
|
486 |
apply (simp add: unique_def map_of_in_set) |
|
487 |
apply blast |
|
488 |
done |
|
489 |
||
490 |
lemma distinct_method_if_class_sig_defined : |
|
491 |
"\<lbrakk> wf_java_prog G; class_sig_defined G C S \<rbrakk> \<Longrightarrow> |
|
492 |
distinct (gjmb_plns (gmb G C S))" |
|
493 |
by (auto intro: distinct_method simp: class_sig_defined_def) |
|
494 |
||
495 |
||
496 |
lemma method_yields_wf_java_mdecl: "\<lbrakk> wf_java_prog G; is_class G C; |
|
497 |
method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
498 |
wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))" |
|
499 |
apply (frule method_wf_mdecl) |
|
500 |
apply (auto simp: wf_mdecl_def) |
|
501 |
done |
|
502 |
||
503 |
(**********************************************************************) |
|
504 |
||
505 |
||
506 |
lemma progression_lvar_init_aux [rule_format (no_asm)]: " |
|
507 |
\<forall> zs prfx lvals lvars0. |
|
508 |
lvars0 = (zs @ lvars) \<longrightarrow> |
|
509 |
(disjoint_varnames pns lvars0 \<longrightarrow> |
|
510 |
(length lvars = length lvals) \<longrightarrow> |
|
511 |
(Suc(length pns + length zs) = length prfx) \<longrightarrow> |
|
512 |
({cG, D, S} \<turnstile> |
|
513 |
{h, os, (prfx @ lvals)} |
|
514 |
>- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow> |
|
515 |
{h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))" |
|
516 |
apply simp |
|
517 |
apply (induct lvars) |
|
518 |
apply (clarsimp, rule progression_refl) |
|
519 |
apply (intro strip) |
|
520 |
apply (case_tac lvals) apply simp |
|
521 |
apply (simp (no_asm_simp) ) |
|
522 |
||
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15097
diff
changeset
|
523 |
apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl) |
13673 | 524 |
apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
525 |
apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp) |
13673 | 526 |
apply (rule progression_one_step) |
527 |
apply (simp (no_asm_simp) add: load_default_val_def) |
|
528 |
apply (rule conjI, simp)+ apply (rule HOL.refl) |
|
529 |
||
530 |
apply (rule progression_one_step) |
|
531 |
apply (simp (no_asm_simp)) |
|
532 |
apply (rule conjI, simp)+ |
|
533 |
apply (simp add: index_of_var2) |
|
534 |
apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *) |
|
535 |
apply (drule mp, simp) |
|
536 |
apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *) |
|
537 |
apply auto |
|
538 |
done |
|
539 |
||
540 |
lemma progression_lvar_init [rule_format (no_asm)]: |
|
541 |
"\<lbrakk> wf_java_prog G; is_class G C; |
|
542 |
method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> |
|
543 |
length pns = length pvs \<longrightarrow> |
|
544 |
(\<forall> lvals. |
|
545 |
length lvars = length lvals \<longrightarrow> |
|
546 |
{cG, D, S} \<turnstile> |
|
547 |
{h, os, (a' # pvs @ lvals)} |
|
548 |
>- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow> |
|
549 |
{h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})" |
|
550 |
apply (simp only: compInitLvars_def) |
|
551 |
apply (frule method_yields_wf_java_mdecl, assumption, assumption) |
|
552 |
||
553 |
apply (simp only: wf_java_mdecl_def) |
|
554 |
apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))") |
|
33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
32960
diff
changeset
|
555 |
apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map) |
13673 | 556 |
apply (intro strip) |
557 |
apply (simp (no_asm_simp) only: append_Cons [THEN sym]) |
|
558 |
apply (rule progression_lvar_init_aux) |
|
559 |
apply (auto simp: unique_def map_of_in_set disjoint_varnames_def) |
|
560 |
done |
|
561 |
||
562 |
||
563 |
||
564 |
||
565 |
(**********************************************************************) |
|
566 |
||
14045 | 567 |
lemma state_ok_eval: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_expr E e; |
568 |
(prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E" |
|
569 |
apply (simp only: wtpd_expr_def) |
|
13673 | 570 |
apply (erule exE) |
14045 | 571 |
apply (case_tac xs', case_tac xs) |
572 |
apply (auto intro: eval_type_sound [THEN conjunct1]) |
|
13673 | 573 |
done |
574 |
||
14045 | 575 |
lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es; |
22271 | 576 |
prg E \<turnstile> xs -es[\<succ>]vs-> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E" |
14045 | 577 |
apply (simp only: wtpd_exprs_def) |
578 |
apply (erule exE) |
|
579 |
apply (case_tac xs) apply (case_tac xs') |
|
580 |
apply (auto intro: evals_type_sound [THEN conjunct1]) |
|
13673 | 581 |
done |
582 |
||
14045 | 583 |
lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st; |
22271 | 584 |
prg E \<turnstile> xs -st-> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E" |
14045 | 585 |
apply (simp only: wtpd_stmt_def) |
586 |
apply (case_tac xs', case_tac xs) |
|
14143 | 587 |
apply (auto dest: exec_type_sound) |
13673 | 588 |
done |
589 |
||
590 |
||
591 |
lemma state_ok_init: |
|
14045 | 592 |
"\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S); |
13673 | 593 |
is_class G dynT; |
594 |
method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res); |
|
595 |
list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk> |
|
596 |
\<Longrightarrow> |
|
14045 | 597 |
(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))" |
598 |
apply (frule wf_prog_ws_prog) |
|
13673 | 599 |
apply (frule method_in_md [THEN conjunct2], assumption+) |
600 |
apply (frule method_yields_wf_java_mdecl, assumption, assumption) |
|
14045 | 601 |
apply (simp add: env_of_jmb_def gs_def conforms_def split_beta) |
13673 | 602 |
apply (simp add: wf_java_mdecl_def) |
603 |
apply (rule conjI) |
|
604 |
apply (rule lconf_ext) |
|
605 |
apply (rule lconf_ext_list) |
|
606 |
apply (rule lconf_init_vars) |
|
607 |
apply (auto dest: Ball_set_table) |
|
608 |
apply (simp add: np_def xconf_raise_if) |
|
609 |
done |
|
610 |
||
611 |
||
612 |
lemma ty_exprs_list_all2 [rule_format (no_asm)]: |
|
613 |
"(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)" |
|
614 |
apply (rule list.induct) |
|
615 |
apply simp |
|
616 |
apply (rule allI) |
|
617 |
apply (rule iffI) |
|
23757 | 618 |
apply (ind_cases "E \<turnstile> [] [::] Ts" for Ts, assumption) |
13673 | 619 |
apply simp apply (rule WellType.Nil) |
620 |
apply (simp add: list_all2_Cons1) |
|
621 |
apply (rule allI) |
|
622 |
apply (rule iffI) |
|
623 |
apply (rename_tac a exs Ts) |
|
23757 | 624 |
apply (ind_cases "E \<turnstile> a # exs [::] Ts" for a exs Ts) apply blast |
13673 | 625 |
apply (auto intro: WellType.Cons) |
626 |
done |
|
627 |
||
628 |
||
629 |
lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b" |
|
630 |
apply (simp add: conf_def) |
|
631 |
apply (erule exE) |
|
632 |
apply (case_tac v) |
|
633 |
apply (auto elim: widen.cases) |
|
634 |
done |
|
635 |
||
636 |
||
14045 | 637 |
lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; ws_prog (prg E)\<rbrakk> |
13673 | 638 |
\<Longrightarrow> is_class (prg E) C" |
639 |
by (case_tac E, auto dest: ty_expr_is_type) |
|
640 |
||
641 |
||
642 |
lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> |
|
643 |
list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'" |
|
644 |
by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD) |
|
645 |
||
646 |
||
14045 | 647 |
lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; s::\<preceq>E; |
13673 | 648 |
E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> |
649 |
\<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T" |
|
650 |
apply (simp add: gh_def) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
651 |
apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'" |
14143 | 652 |
in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified]) |
653 |
apply assumption+ |
|
13673 | 654 |
apply (simp (no_asm_use) add: surjective_pairing [THEN sym]) |
14045 | 655 |
apply (simp only: surjective_pairing [THEN sym]) |
656 |
apply (auto simp add: gs_def gx_def) |
|
13673 | 657 |
done |
658 |
||
659 |
lemma evals_preserves_conf: |
|
660 |
"\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts; |
|
14045 | 661 |
wf_java_prog G; s::\<preceq>E; |
13673 | 662 |
prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T" |
663 |
apply (subgoal_tac "gh s\<le>| gh s'") |
|
664 |
apply (frule conf_hext, assumption, assumption) |
|
665 |
apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) |
|
666 |
apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))") |
|
667 |
apply assumption |
|
668 |
apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym]) |
|
669 |
apply (case_tac E) |
|
14045 | 670 |
apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym]) |
13673 | 671 |
done |
672 |
||
673 |
lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; |
|
14045 | 674 |
wf_java_prog G; s::\<preceq>E; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk> |
13673 | 675 |
\<Longrightarrow> (\<exists> lc. a' = Addr lc)" |
676 |
apply (case_tac s, case_tac s', simp) |
|
14045 | 677 |
apply (frule eval_type_sound, (simp add: gs_def)+) |
13673 | 678 |
apply (case_tac a') |
679 |
apply (auto simp: conf_def) |
|
680 |
done |
|
681 |
||
682 |
||
683 |
lemma dynT_subcls: |
|
684 |
"\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a'))); |
|
14045 | 685 |
is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C" |
13673 | 686 |
apply (case_tac "C = Object") |
687 |
apply (simp, rule subcls_C_Object, assumption+) |
|
14045 | 688 |
apply simp |
13673 | 689 |
apply (frule non_np_objD, auto) |
690 |
done |
|
691 |
||
692 |
||
693 |
lemma method_defined: "\<lbrakk> |
|
694 |
m = the (method (G, dynT) (mn, pTs)); |
|
695 |
dynT = fst (the (h a)); is_class G dynT; wf_java_prog G; |
|
696 |
a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; a = the_Addr a'; |
|
697 |
\<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk> |
|
698 |
\<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m" |
|
699 |
apply (erule exE)+ |
|
700 |
apply (drule singleton_in_set, drule max_spec2appl_meths) |
|
701 |
apply (simp add: appl_methds_def) |
|
702 |
apply ((erule exE)+, (erule conjE)+, (erule exE)+) |
|
703 |
apply (drule widen_methd) |
|
704 |
apply assumption |
|
14045 | 705 |
apply (rule dynT_subcls) apply assumption+ apply simp apply simp |
13673 | 706 |
apply (erule exE)+ apply simp |
707 |
done |
|
708 |
||
709 |
||
710 |
||
711 |
(**********************************************************************) |
|
712 |
||
713 |
||
714 |
(* 1. any difference between locvars_xstate \<dots> and L ??? *) |
|
715 |
(* 2. possibly skip env_of_jmb ??? *) |
|
716 |
theorem compiler_correctness: |
|
717 |
"wf_java_prog G \<Longrightarrow> |
|
22271 | 718 |
(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> |
13673 | 719 |
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
720 |
(\<forall> os CL S. |
|
721 |
(class_sig_defined G CL S) \<longrightarrow> |
|
722 |
(wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow> |
|
14045 | 723 |
(xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow> |
13673 | 724 |
( {TranslComp.comp G, CL, S} \<turnstile> |
725 |
{gh xs, os, (locvars_xstate G CL S xs)} |
|
726 |
>- (compExpr (gmb G CL S) ex) \<rightarrow> |
|
727 |
{gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> |
|
728 |
||
22271 | 729 |
(G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> |
13673 | 730 |
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
731 |
(\<forall> os CL S. |
|
732 |
(class_sig_defined G CL S) \<longrightarrow> |
|
733 |
(wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow> |
|
14045 | 734 |
(xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow> |
13673 | 735 |
( {TranslComp.comp G, CL, S} \<turnstile> |
736 |
{gh xs, os, (locvars_xstate G CL S xs)} |
|
737 |
>- (compExprs (gmb G CL S) exs) \<rightarrow> |
|
738 |
{gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> |
|
739 |
||
22271 | 740 |
(G \<turnstile> xs -st-> xs' \<longrightarrow> |
13673 | 741 |
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow> |
742 |
(\<forall> os CL S. |
|
743 |
(class_sig_defined G CL S) \<longrightarrow> |
|
744 |
(wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow> |
|
14045 | 745 |
(xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow> |
13673 | 746 |
( {TranslComp.comp G, CL, S} \<turnstile> |
747 |
{gh xs, os, (locvars_xstate G CL S xs)} |
|
748 |
>- (compStmt (gmb G CL S) st) \<rightarrow> |
|
749 |
{gh xs', os, (locvars_xstate G CL S xs')})))" |
|
750 |
apply (rule Eval.eval_evals_exec.induct) |
|
751 |
||
752 |
(* case XcptE *) |
|
753 |
apply simp |
|
754 |
||
755 |
(* case NewC *) |
|
14045 | 756 |
apply clarify |
757 |
apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish wf ((subcls1 G)^-1) *) |
|
13673 | 758 |
apply (simp add: c_hupd_hp_invariant) |
759 |
apply (rule progression_one_step) |
|
760 |
apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *) |
|
761 |
apply (simp add: locvars_xstate_def locvars_locals_def comp_fields) |
|
762 |
||
763 |
||
764 |
(* case Cast *) |
|
765 |
apply (intro allI impI) |
|
766 |
apply simp |
|
767 |
apply (frule raise_if_NoneD) |
|
768 |
apply (frule wtpd_expr_cast) |
|
769 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
770 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp) |
13673 | 771 |
apply blast |
772 |
apply (rule progression_one_step) |
|
773 |
apply (simp add: raise_system_xcpt_def gh_def comp_cast_ok) |
|
774 |
||
775 |
||
776 |
(* case Lit *) |
|
777 |
apply simp |
|
778 |
apply (intro strip) |
|
779 |
apply (rule progression_one_step) |
|
780 |
apply simp |
|
781 |
||
782 |
||
783 |
(* case BinOp *) |
|
784 |
apply (intro allI impI) |
|
785 |
apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *) |
|
786 |
apply (frule wtpd_expr_binop) |
|
14045 | 787 |
(* establish (s1::\<preceq> \<dots>) *) |
13673 | 788 |
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) |
789 |
||
790 |
||
791 |
apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
792 |
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast |
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
793 |
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast |
13673 | 794 |
apply (case_tac bop) |
795 |
(*subcase bop = Eq *) apply simp apply (rule progression_Eq) |
|
796 |
(*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp |
|
797 |
||
798 |
||
799 |
(* case LAcc *) |
|
800 |
apply simp |
|
801 |
apply (intro strip) |
|
802 |
apply (rule progression_one_step) |
|
803 |
apply (simp add: locvars_xstate_def locvars_locals_def) |
|
804 |
apply (frule wtpd_expr_lacc) |
|
805 |
apply assumption |
|
806 |
apply (simp add: gl_def) |
|
807 |
apply (erule select_at_index) |
|
808 |
||
809 |
||
810 |
(* case LAss *) |
|
811 |
apply (intro allI impI) |
|
812 |
apply (frule wtpd_expr_lass, erule conjE, erule conjE) |
|
813 |
apply (simp add: compExpr_compExprs.simps) |
|
814 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
815 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
13673 | 816 |
apply blast |
817 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
818 |
apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp) |
13673 | 819 |
apply (rule progression_one_step) |
820 |
apply (simp add: gh_def) |
|
821 |
apply (rule conjI, simp)+ apply simp |
|
822 |
apply (rule progression_one_step) |
|
823 |
apply (simp add: gh_def) |
|
824 |
(* the following falls out of the general scheme *) |
|
825 |
apply (frule wtpd_expr_lacc) apply assumption |
|
826 |
apply (rule update_at_index) |
|
827 |
apply (rule distinct_method_if_class_sig_defined) apply assumption |
|
828 |
apply assumption apply simp apply assumption |
|
829 |
||
830 |
||
831 |
(* case FAcc *) |
|
832 |
apply (intro allI impI) |
|
833 |
(* establish x1 = None \<and> a' \<noteq> Null *) |
|
834 |
apply (simp (no_asm_use) only: gx_conv, frule np_NoneD) |
|
835 |
apply (frule wtpd_expr_facc) |
|
836 |
||
837 |
apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
838 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
13673 | 839 |
apply blast |
840 |
apply (rule progression_one_step) |
|
841 |
apply (simp add: gh_def) |
|
842 |
apply (case_tac "(the (fst s1 (the_Addr a')))") |
|
843 |
apply (simp add: raise_system_xcpt_def) |
|
844 |
||
845 |
||
846 |
(* case FAss *) |
|
847 |
apply (intro allI impI) |
|
848 |
apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc) |
|
849 |
apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *) |
|
850 |
(* establish x1 = None and a' \<noteq> Null *) |
|
851 |
apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt) |
|
852 |
apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE) |
|
853 |
||
854 |
||
14045 | 855 |
(* establish ((Norm s1)::\<preceq> \<dots>) *) |
856 |
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) |
|
857 |
apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
13673 | 858 |
|
859 |
apply (simp only: compExpr_compExprs.simps) |
|
860 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
861 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl) |
13673 | 862 |
apply fast (* blast does not seem to work - why? *) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
863 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl) |
13673 | 864 |
apply fast |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
865 |
apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp) |
13673 | 866 |
|
867 |
(* Dup_x1 *) |
|
868 |
apply (rule progression_one_step) |
|
869 |
apply (simp add: gh_def) |
|
870 |
apply (rule conjI, simp)+ apply simp |
|
871 |
||
872 |
||
873 |
(* Putfield \<longrightarrow> still looks nasty*) |
|
874 |
apply (rule progression_one_step) |
|
875 |
apply simp |
|
876 |
apply (case_tac "(the (fst s2 (the_Addr a')))") |
|
877 |
apply (simp add: c_hupd_hp_invariant) |
|
878 |
apply (case_tac s2) |
|
879 |
apply (simp add: c_hupd_conv raise_system_xcpt_def) |
|
880 |
apply (rule locvars_xstate_par_dep, rule HOL.refl) |
|
881 |
||
882 |
defer (* method call *) |
|
883 |
||
884 |
(* case XcptEs *) |
|
885 |
apply simp |
|
886 |
||
887 |
(* case Nil *) |
|
888 |
apply (simp add: compExpr_compExprs.simps) |
|
889 |
apply (intro strip) |
|
890 |
apply (rule progression_refl) |
|
891 |
||
892 |
(* case Cons *) |
|
893 |
apply (intro allI impI) |
|
894 |
apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *) |
|
895 |
apply (frule wtpd_exprs_cons) |
|
14045 | 896 |
(* establish ((Norm s0)::\<preceq> \<dots>) *) |
13673 | 897 |
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) |
898 |
||
899 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
900 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
13673 | 901 |
apply fast |
902 |
apply fast |
|
903 |
||
904 |
||
905 |
(* case Statement: exception *) |
|
906 |
apply simp |
|
907 |
||
908 |
(* case Skip *) |
|
909 |
apply (intro allI impI) |
|
910 |
apply simp |
|
911 |
apply (rule progression_refl) |
|
912 |
||
913 |
(* case Expr *) |
|
914 |
apply (intro allI impI) |
|
915 |
apply (frule wtpd_stmt_expr) |
|
916 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
917 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
13673 | 918 |
apply fast |
919 |
apply (rule progression_one_step) |
|
920 |
apply simp |
|
921 |
||
922 |
(* case Comp *) |
|
923 |
apply (intro allI impI) |
|
924 |
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
925 |
apply (frule wtpd_stmt_comp) |
|
926 |
||
14045 | 927 |
(* establish (s1::\<preceq> \<dots>) *) |
13673 | 928 |
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) |
929 |
||
930 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
931 |
apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl) |
13673 | 932 |
apply fast |
933 |
apply fast |
|
934 |
||
935 |
||
936 |
(* case Cond *) |
|
937 |
apply (intro allI impI) |
|
938 |
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
939 |
apply (frule wtpd_stmt_cond, (erule conjE)+) |
|
14045 | 940 |
(* establish (s1::\<preceq> \<dots>) *) |
13673 | 941 |
apply (frule_tac e=e in state_ok_eval) |
942 |
apply (simp (no_asm_simp) only: env_of_jmb_fst) |
|
943 |
apply assumption |
|
944 |
apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
945 |
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
946 |
apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
947 |
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
948 |
apply (erule exE) |
|
949 |
||
950 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
951 |
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
13673 | 952 |
apply (rule progression_one_step, simp) |
953 |
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
954 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
955 |
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
13673 | 956 |
apply fast |
957 |
||
958 |
apply (case_tac b) |
|
959 |
(* case b= True *) |
|
960 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
961 |
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp) |
13673 | 962 |
apply (rule progression_one_step) apply simp |
963 |
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
964 |
apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp) |
13673 | 965 |
apply fast |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
966 |
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression) |
13673 | 967 |
apply (simp, rule conjI, (rule HOL.refl)+) |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset
|
968 |
apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib) |
13673 | 969 |
apply (rule progression_refl) |
970 |
||
971 |
(* case b= False *) |
|
972 |
apply simp |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
973 |
apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression) |
13673 | 974 |
apply (simp, rule conjI, (rule HOL.refl)+) |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset
|
975 |
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib) |
13673 | 976 |
apply fast |
977 |
||
978 |
(* case exit Loop *) |
|
979 |
apply (intro allI impI) |
|
980 |
apply (frule wtpd_stmt_loop, (erule conjE)+) |
|
981 |
||
982 |
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
983 |
apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
984 |
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
985 |
apply (erule exE) |
|
986 |
apply (case_tac b) |
|
987 |
||
988 |
(* case b= True \<longrightarrow> contradiction *) |
|
989 |
apply simp |
|
990 |
||
991 |
(* case b= False *) |
|
992 |
apply simp |
|
993 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
994 |
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
13673 | 995 |
apply (rule progression_one_step) |
996 |
apply simp |
|
997 |
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
998 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
999 |
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
13673 | 1000 |
apply fast |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1001 |
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression) |
13673 | 1002 |
apply (simp, rule conjI, rule HOL.refl, rule HOL.refl) |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset
|
1003 |
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib) |
13673 | 1004 |
apply (rule progression_refl) |
1005 |
||
1006 |
||
1007 |
(* case continue Loop *) |
|
1008 |
apply (intro allI impI) |
|
1009 |
apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *) |
|
1010 |
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *) |
|
1011 |
apply (frule wtpd_stmt_loop, (erule conjE)+) |
|
1012 |
||
14045 | 1013 |
(* establish (s1::\<preceq> \<dots>) *) |
13673 | 1014 |
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) |
14045 | 1015 |
(* establish (s2::\<preceq> \<dots>) *) |
13673 | 1016 |
apply (frule_tac xs=s1 and st=c in state_ok_exec) |
1017 |
apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
1018 |
||
1019 |
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *) |
|
1020 |
apply (frule eval_conf, assumption+, rule env_of_jmb_fst) |
|
1021 |
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *) |
|
1022 |
apply (erule exE) |
|
1023 |
||
1024 |
apply simp |
|
1025 |
apply (rule jump_bwd_progression) |
|
1026 |
apply simp |
|
1027 |
apply (rule conjI, (rule HOL.refl)+) |
|
1028 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1029 |
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp)) |
13673 | 1030 |
apply (rule progression_one_step) |
1031 |
apply simp |
|
1032 |
apply (rule conjI, simp)+ apply simp |
|
1033 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1034 |
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
13673 | 1035 |
apply fast |
1036 |
||
1037 |
apply (case_tac b) |
|
1038 |
(* case b= True *) |
|
1039 |
apply simp |
|
1040 |
||
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1041 |
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp) |
13673 | 1042 |
apply (rule progression_one_step) apply simp |
1043 |
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
|
1044 |
apply fast |
|
1045 |
||
1046 |
(* case b= False \<longrightarrow> contradiction*) |
|
1047 |
apply simp |
|
1048 |
||
1049 |
apply (rule jump_bwd_one_step) |
|
1050 |
apply simp |
|
1051 |
apply blast |
|
1052 |
||
1053 |
(*****) |
|
14045 | 1054 |
(* case method call *) |
13673 | 1055 |
|
1056 |
apply (intro allI impI) |
|
1057 |
||
1058 |
apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *) |
|
1059 |
apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *) |
|
1060 |
apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *) |
|
1061 |
||
1062 |
apply (frule wtpd_expr_call, (erule conjE)+) |
|
1063 |
||
1064 |
||
1065 |
(* assumptions about state_ok and is_class *) |
|
1066 |
||
14045 | 1067 |
(* establish s1::\<preceq> (env_of_jmb G CL S) *) |
13673 | 1068 |
apply (frule_tac xs="Norm s0" and e=e in state_ok_eval) |
1069 |
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst) |
|
1070 |
||
14045 | 1071 |
(* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *) |
13673 | 1072 |
apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals) |
1073 |
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst) |
|
1074 |
||
1075 |
(* establish \<exists> lc. a' = Addr lc *) |
|
1076 |
apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym]) |
|
1077 |
apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C") |
|
1078 |
apply (subgoal_tac "is_class G dynT") |
|
1079 |
||
1080 |
(* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *) |
|
1081 |
apply (drule method_defined, assumption+) |
|
1082 |
apply (simp only: env_of_jmb_fst) |
|
1083 |
apply ((erule exE)+, erule conjE, (rule exI)+, assumption) |
|
1084 |
||
1085 |
apply (subgoal_tac "is_class G md") |
|
1086 |
apply (subgoal_tac "G\<turnstile>Class dynT \<preceq> Class md") |
|
1087 |
apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)") |
|
1088 |
apply (subgoal_tac "list_all2 (conf G h) pvs pTs") |
|
1089 |
||
14045 | 1090 |
(* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *) |
13673 | 1091 |
apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT") |
1092 |
apply (frule (2) conf_widen) |
|
1093 |
apply (frule state_ok_init, assumption+) |
|
1094 |
||
1095 |
apply (subgoal_tac "class_sig_defined G md (mn, pTs)") |
|
1096 |
apply (frule wtpd_blk, assumption, assumption) |
|
1097 |
apply (frule wtpd_res, assumption, assumption) |
|
14045 | 1098 |
apply (subgoal_tac "s3::\<preceq>(env_of_jmb G md (mn, pTs))") |
13673 | 1099 |
|
14045 | 1100 |
apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) = |
1101 |
Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))") |
|
1102 |
prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method]) |
|
1103 |
apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) = |
|
1104 |
Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))") |
|
1105 |
prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method]) |
|
13673 | 1106 |
apply (simp only: fst_conv snd_conv) |
1107 |
||
1108 |
(* establish length pns = length pTs *) |
|
1109 |
apply (frule method_preserves_length, assumption, assumption) |
|
1110 |
(* establish length pvs = length ps *) |
|
1111 |
apply (frule evals_preserves_length [THEN sym]) |
|
1112 |
||
1113 |
(** start evaluating subexpressions **) |
|
1114 |
apply (simp (no_asm_use) only: compExpr_compExprs.simps) |
|
1115 |
||
1116 |
(* evaluate e *) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1117 |
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl) |
13673 | 1118 |
apply fast |
1119 |
||
1120 |
(* evaluate parameters *) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1121 |
apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl) |
13673 | 1122 |
apply fast |
1123 |
||
1124 |
(* invokation *) |
|
1125 |
apply (rule progression_call) |
|
1126 |
apply (intro allI impI conjI) |
|
1127 |
(* execute Invoke statement *) |
|
1128 |
apply (simp (no_asm_use) only: exec_instr.simps) |
|
1129 |
apply (erule thin_rl, erule thin_rl, erule thin_rl) |
|
1130 |
apply (simp add: compMethod_def raise_system_xcpt_def) |
|
1131 |
apply (rule conjI, simp)+ apply (rule HOL.refl) |
|
1132 |
||
1133 |
(* get instructions of invoked method *) |
|
1134 |
apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def) |
|
1135 |
||
1136 |
(* var. initialization *) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1137 |
apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl) |
13673 | 1138 |
apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption) |
1139 |
apply (simp (no_asm_simp)) (* length pns = length pvs *) |
|
28524 | 1140 |
apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) undefined) *) |
13673 | 1141 |
|
1142 |
||
1143 |
(* body statement *) |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14143
diff
changeset
|
1144 |
apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl) |
13673 | 1145 |
apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)") |
1146 |
apply (simp (no_asm_simp)) |
|
15866 | 1147 |
apply (simp only: gh_conv) |
1148 |
apply (drule mp [OF _ TrueI])+ |
|
1149 |
apply (erule allE, erule allE, erule allE, erule impE, assumption)+ |
|
1150 |
apply ((erule impE, assumption)+, assumption) |
|
15860 | 1151 |
|
13673 | 1152 |
apply (simp (no_asm_use)) |
1153 |
apply (simp (no_asm_simp) add: gmb_def) |
|
1154 |
||
1155 |
(* return expression *) |
|
1156 |
apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)") |
|
1157 |
apply (simp (no_asm_simp)) |
|
1158 |
apply (simp only: gh_conv) |
|
1159 |
apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption) |
|
1160 |
apply (simp (no_asm_use)) |
|
1161 |
apply (simp (no_asm_simp) add: gmb_def) |
|
1162 |
||
1163 |
(* execute return statement *) |
|
1164 |
apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append) |
|
1165 |
apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os") |
|
1166 |
apply (simp only: drop_append) |
|
1167 |
apply (simp (no_asm_simp)) |
|
1168 |
apply (simp (no_asm_simp)) |
|
1169 |
||
14045 | 1170 |
(* show s3::\<preceq>\<dots> *) |
13673 | 1171 |
apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec) |
1172 |
apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) |
|
1173 |
apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) |
|
1174 |
||
1175 |
(* show class_sig_defined G md (mn, pTs) *) |
|
1176 |
apply (simp (no_asm_simp) add: class_sig_defined_def) |
|
1177 |
||
1178 |
(* show G,h \<turnstile> a' ::\<preceq> Class dynT *) |
|
1179 |
apply (frule non_npD) apply assumption |
|
1180 |
apply (erule exE)+ apply simp |
|
1181 |
apply (rule conf_obj_AddrI) apply simp |
|
1182 |
apply (rule conjI, (rule HOL.refl)+) |
|
1183 |
apply (rule widen_Class_Class [THEN iffD1], rule widen.refl) |
|
1184 |
||
1185 |
||
1186 |
(* show list_all2 (conf G h) pvs pTs *) |
|
1187 |
apply (erule exE)+ apply (erule conjE)+ |
|
1188 |
apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption |
|
22271 | 1189 |
apply (subgoal_tac "G \<turnstile> (gx s1, gs s1) -ps[\<succ>]pvs-> (x, h, l)") |
13673 | 1190 |
apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound) |
14143 | 1191 |
apply assumption+ |
13673 | 1192 |
apply (simp only: env_of_jmb_fst) |
1193 |
apply (simp add: conforms_def xconf_def gs_def) |
|
1194 |
apply simp |
|
1195 |
apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym]) |
|
1196 |
apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp |
|
14143 | 1197 |
apply simp |
13673 | 1198 |
apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym]) |
1199 |
(* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *) |
|
1200 |
apply (rule max_spec_widen, simp only: env_of_jmb_fst) |
|
1201 |
||
1202 |
||
1203 |
(* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *) |
|
14045 | 1204 |
apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+) |
13673 | 1205 |
|
1206 |
(* show G\<turnstile>Class dynT \<preceq> Class md *) |
|
1207 |
apply (simp (no_asm_use) only: widen_Class_Class) |
|
1208 |
apply (rule method_wf_mdecl [THEN conjunct1], assumption+) |
|
1209 |
||
1210 |
(* is_class G md *) |
|
14045 | 1211 |
apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+) |
13673 | 1212 |
|
1213 |
(* show is_class G dynT *) |
|
1214 |
apply (frule non_npD) apply assumption |
|
1215 |
apply (erule exE)+ apply (erule conjE)+ |
|
1216 |
apply simp |
|
1217 |
apply (rule subcls_is_class2) apply assumption |
|
1218 |
apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst) |
|
14045 | 1219 |
apply (rule wf_prog_ws_prog, assumption) |
13673 | 1220 |
apply (simp only: env_of_jmb_fst) |
1221 |
||
1222 |
(* show G,h \<turnstile> a' ::\<preceq> Class C *) |
|
1223 |
apply (simp only: wtpd_exprs_def, erule exE) |
|
1224 |
apply (frule evals_preserves_conf) |
|
1225 |
apply (rule eval_conf, assumption+) |
|
1226 |
apply (rule env_of_jmb_fst, assumption+) |
|
1227 |
apply (rule env_of_jmb_fst) |
|
1228 |
apply (simp only: gh_conv) |
|
1229 |
done |
|
1230 |
||
1231 |
||
1232 |
theorem compiler_correctness_eval: " |
|
1233 |
\<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc'); |
|
1234 |
wf_java_prog G; |
|
1235 |
class_sig_defined G C S; |
|
1236 |
wtpd_expr (env_of_jmb G C S) ex; |
|
1237 |
(None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow> |
|
1238 |
{(TranslComp.comp G), C, S} \<turnstile> |
|
1239 |
{hp, os, (locvars_locals G C S loc)} |
|
1240 |
>- (compExpr (gmb G C S) ex) \<rightarrow> |
|
1241 |
{hp', val#os, (locvars_locals G C S loc')}" |
|
1242 |
apply (frule compiler_correctness [THEN conjunct1]) |
|
14045 | 1243 |
apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def) |
13673 | 1244 |
done |
1245 |
||
1246 |
theorem compiler_correctness_exec: " |
|
22271 | 1247 |
\<lbrakk> G \<turnstile> Norm (hp, loc) -st-> Norm (hp', loc'); |
13673 | 1248 |
wf_java_prog G; |
1249 |
class_sig_defined G C S; |
|
1250 |
wtpd_stmt (env_of_jmb G C S) st; |
|
1251 |
(None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow> |
|
1252 |
{(TranslComp.comp G), C, S} \<turnstile> |
|
1253 |
{hp, os, (locvars_locals G C S loc)} |
|
1254 |
>- (compStmt (gmb G C S) st) \<rightarrow> |
|
1255 |
{hp', os, (locvars_locals G C S loc')}" |
|
1256 |
apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]]) |
|
14045 | 1257 |
apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def) |
13673 | 1258 |
done |
1259 |
||
1260 |
(**********************************************************************) |
|
1261 |
||
1262 |
||
1263 |
(* reinstall pair splits *) |
|
1264 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
24074 | 1265 |
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
13673 | 1266 |
|
14045 | 1267 |
declare wf_prog_ws_prog [simp del] |
1268 |
||
13673 | 1269 |
end |