author | wenzelm |
Sun, 03 Sep 2000 20:01:47 +0200 | |
changeset 9819 | e9fb6d44a490 |
parent 9757 | 1024a2d80ac0 |
child 9906 | 5c027cca6262 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
Proof that the specification of the bytecode verifier only admits type safe |
|
7 |
programs. |
|
8 |
*) |
|
9 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
10 |
header "Type Safety Proof" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
11 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
12 |
theory BVSpecTypeSafe = Correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
13 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
14 |
lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
15 |
lemmas [simp del] = split_paired_All |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
16 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
17 |
lemma wt_jvm_prog_impl_wt_instr_cor: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
18 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
19 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
20 |
==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
21 |
apply (unfold correct_state_def Let_def correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
22 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
23 |
apply (blast intro: wt_jvm_prog_impl_wt_instr) |
9819 | 24 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
25 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
26 |
lemma Load_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
27 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
28 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
29 |
ins!pc = Load idx; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
30 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
31 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
32 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
33 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
34 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
35 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
36 |
apply (rule approx_loc_imp_approx_val_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
37 |
apply simp+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
38 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) |
9819 | 39 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
40 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
41 |
lemma Store_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
42 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
43 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
44 |
ins!pc = Store idx; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
45 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
46 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
47 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
48 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
49 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
50 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
51 |
apply (blast intro: approx_stk_imp_approx_stk_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
52 |
apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup) |
9819 | 53 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
54 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
55 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
56 |
lemma conf_Intg_Integer [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
57 |
"G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
58 |
by (simp add: conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
59 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
60 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
61 |
lemma Bipush_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
62 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
63 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
64 |
ins!pc = Bipush i; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
65 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
66 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
67 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
9819 | 68 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
69 |
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
70 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) |
9819 | 71 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
72 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
73 |
lemma NT_subtype_conv: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
74 |
"G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
75 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
76 |
have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
77 |
apply (erule widen.induct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
78 |
apply auto |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
79 |
apply (case_tac R) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
80 |
apply auto |
9819 | 81 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
82 |
note l = this |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
83 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
84 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
85 |
by (force intro: null dest: l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
86 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
87 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
88 |
lemma Aconst_null_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
89 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
90 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
91 |
ins!pc = Aconst_null; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
92 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
93 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
94 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
9819 | 95 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
96 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
97 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
98 |
apply (force simp add: approx_val_Null NT_subtype_conv) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
99 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) |
9819 | 100 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
101 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
102 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
103 |
lemma Cast_conf2: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
104 |
"\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
105 |
\<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>T" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
106 |
apply (unfold cast_ok_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
107 |
apply (frule widen_Class) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
108 |
apply (elim exE disjE) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
109 |
apply (simp add: null) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
110 |
apply (clarsimp simp add: conf_def obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
111 |
apply (cases v) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
112 |
apply (auto intro: null rtrancl_trans) |
9819 | 113 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
114 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
115 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
116 |
lemma Checkcast_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
117 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
118 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
119 |
ins!pc = Checkcast D; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
120 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
121 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
122 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
123 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
124 |
apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
125 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2) |
9819 | 126 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
127 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
128 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
129 |
lemma Getfield_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
130 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
131 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
132 |
ins!pc = Getfield F D; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
133 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
134 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
135 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
9819 | 136 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
137 |
apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
138 |
apply (frule conf_widen) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
139 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
140 |
apply (drule conf_RefTD) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
141 |
apply (clarsimp simp add: defs1 approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
142 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
143 |
apply (drule widen_cfs_fields) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
144 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
145 |
apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
146 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) |
9819 | 147 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
148 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
149 |
lemma Putfield_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
150 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
151 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
152 |
ins!pc = Putfield F D; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
153 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
154 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
155 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
9819 | 156 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
157 |
apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
158 |
apply (clarsimp simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
159 |
apply (frule conf_widen) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
160 |
prefer 2 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
161 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
162 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
163 |
apply (drule conf_RefTD) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
164 |
apply clarsimp |
9819 | 165 |
apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap |
166 |
approx_stk_imp_approx_stk_sup |
|
167 |
approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup |
|
168 |
hconf_imp_hconf_field_update |
|
169 |
correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields) |
|
170 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
171 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
172 |
lemma collapse_paired_All: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
173 |
"(\<forall>x y. P(x,y)) = (\<forall>z. P z)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
174 |
by fast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
175 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
176 |
lemma New_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
177 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
178 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
179 |
ins!pc = New cl_idx; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
180 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
181 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
182 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
183 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
184 |
apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
185 |
fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
186 |
split: option.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
187 |
apply (force dest!: iffD1 [OF collapse_paired_All] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
188 |
intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
189 |
approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
190 |
hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
191 |
correct_init_obj simp add: NT_subtype_conv approx_val_def conf_def |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
192 |
fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
193 |
split: option.split) |
9819 | 194 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
195 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
196 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
197 |
(****** Method Invocation ******) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
198 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
199 |
lemmas [simp del] = split_paired_Ex |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
200 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
201 |
lemma Invoke_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
202 |
"\<lbrakk> wt_jvm_prog G phi; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
203 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
204 |
ins ! pc = Invoke C' mn pTs; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
205 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
206 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
207 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
208 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
209 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
210 |
assume wtprog: "wt_jvm_prog G phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
211 |
assume method: "method (G,C) sig = Some (C,rT,maxl,ins)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
212 |
assume ins: "ins ! pc = Invoke C' mn pTs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
213 |
assume wti: "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
214 |
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
215 |
assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
216 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
217 |
from wtprog |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
218 |
obtain wfmb where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
219 |
wfprog: "wf_prog wfmb G" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
220 |
by (simp add: wt_jvm_prog_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
221 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
222 |
from ins method approx |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
223 |
obtain s where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
224 |
heap_ok: "G\<turnstile>h hp\<surd>" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
225 |
phi_pc: "phi C sig!pc = Some s" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
226 |
frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
227 |
frames: "correct_frames G hp phi rT sig frs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
228 |
by (clarsimp simp add: correct_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
229 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
230 |
from ins wti phi_pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
231 |
obtain apTs X ST LT D' rT body where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
232 |
s: "s = (rev apTs @ X # ST, LT)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
233 |
l: "length apTs = length pTs" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
234 |
X: "G\<turnstile> X \<preceq> Class C'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
235 |
w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
236 |
mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
237 |
pc: "Suc pc < length ins" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
238 |
step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
239 |
by (simp add: wt_instr_def) (elim exE conjE, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
240 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
241 |
from step |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
242 |
obtain ST' LT' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
243 |
s': "phi C sig ! Suc pc = Some (ST', LT')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
244 |
by (simp add: step_def split_paired_Ex) (elim, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
245 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
246 |
from X |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
247 |
obtain T where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
248 |
X_Ref: "X = RefT T" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
249 |
by - (drule widen_RefT2, erule exE, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
250 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
251 |
from s ins frame |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
252 |
obtain |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
253 |
a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
254 |
a_loc: "approx_loc G hp loc LT" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
255 |
suc_l: "length loc = Suc (length (snd sig) + maxl)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
256 |
by (simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
257 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
258 |
from a_stk |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
259 |
obtain opTs stk' oX where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
260 |
opTs: "approx_stk G hp opTs (rev apTs)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
261 |
oX: "approx_val G hp oX (Ok X)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
262 |
a_stk': "approx_stk G hp stk' ST" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
263 |
stk': "stk = opTs @ oX # stk'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
264 |
l_o: "length opTs = length apTs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
265 |
"length stk' = length ST" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
266 |
by - (drule approx_stk_append_lemma, simp, elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
267 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
268 |
from oX |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
269 |
have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
270 |
by (clarsimp simp add: approx_val_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
271 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
272 |
with X_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
273 |
obtain T' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
274 |
oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
275 |
"G \<turnstile> RefT T' \<preceq> X" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
276 |
apply (elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
277 |
apply (frule widen_RefT2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
278 |
by (elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
279 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
280 |
from stk' l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
281 |
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
282 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
283 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
284 |
with state' method ins |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
285 |
have Null_ok: "oX = Null \<Longrightarrow> ?thesis" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
286 |
by (simp add: correct_state_def raise_xcpt_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
287 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
288 |
{ fix ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
289 |
assume oX_Addr: "oX = Addr ref" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
290 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
291 |
with oX_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
292 |
obtain obj where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
293 |
loc: "hp ref = Some obj" "obj_ty obj = RefT T'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
294 |
by clarsimp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
295 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
296 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
297 |
obtain D where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
298 |
obj_ty: "obj_ty obj = Class D" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
299 |
by (auto simp add: obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
300 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
301 |
with X_Ref oX_Ref loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
302 |
obtain D: "G \<turnstile> Class D \<preceq> X" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
303 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
304 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
305 |
with X_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
306 |
obtain X' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
307 |
X': "X = Class X'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
308 |
by - (drule widen_Class, elim, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
309 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
310 |
with X |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
311 |
have "G \<turnstile> X' \<preceq>C C'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
312 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
313 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
314 |
with mC' wfprog |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
315 |
obtain D0 rT0 maxl0 ins0 where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
316 |
mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
317 |
by (auto dest: subtype_widen_methd) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
318 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
319 |
from X' D |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
320 |
have "G \<turnstile> D \<preceq>C X'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
321 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
322 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
323 |
with wfprog mX |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
324 |
obtain D'' rT' mxl' ins' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
325 |
mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
326 |
"G \<turnstile> rT' \<preceq> rT0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
327 |
by (auto dest: subtype_widen_methd) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
328 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
329 |
from mX mD |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
330 |
have rT': "G \<turnstile> rT' \<preceq> rT" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
331 |
by - (rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
332 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
333 |
from mD wfprog |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
334 |
obtain mD'': |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
335 |
"method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
336 |
"is_class G D''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
337 |
by (auto dest: method_in_md) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
338 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
339 |
from loc obj_ty |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
340 |
have "fst (the (hp ref)) = D" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
341 |
by (simp add: obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
342 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
343 |
with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
344 |
have state'_val: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
345 |
"state' = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
346 |
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
347 |
D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
348 |
(is "state' = Norm (hp, ?f # ?f' # frs)") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
349 |
by (simp add: raise_xcpt_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
350 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
351 |
from wtprog mD'' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
352 |
have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
353 |
by (auto dest: wt_jvm_prog_impl_wt_start) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
354 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
355 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
356 |
obtain LT0 where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
357 |
LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
358 |
by (clarsimp simp add: wt_start_def sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
359 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
360 |
have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
361 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
362 |
from start LT0 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
363 |
have sup_loc: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
364 |
"G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
365 |
(is "G \<turnstile> ?LT <=l LT0") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
366 |
by (simp add: wt_start_def sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
367 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
368 |
have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
369 |
by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
370 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
371 |
from wfprog mD |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
372 |
have "G \<turnstile> Class D \<preceq> Class D''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
373 |
by (auto dest: method_wf_mdecl) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
374 |
with obj_ty loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
375 |
have a: "approx_val G hp (Addr ref) (Ok (Class D''))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
376 |
by (simp add: approx_val_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
377 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
378 |
from w l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
379 |
have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
380 |
by (auto simp add: zip_rev) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
381 |
with wfprog l l_o opTs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
382 |
have "approx_loc G hp opTs (map Ok (rev pTs))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
383 |
by (auto intro: assConv_approx_stk_imp_approx_loc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
384 |
hence "approx_stk G hp opTs (rev pTs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
385 |
by (simp add: approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
386 |
hence "approx_stk G hp (rev opTs) pTs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
387 |
by (simp add: approx_stk_rev) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
388 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
389 |
with r a l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
390 |
have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
391 |
(is "approx_loc G hp ?lt ?LT") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
392 |
by (auto simp add: approx_loc_append approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
393 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
394 |
from wfprog this sup_loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
395 |
have "approx_loc G hp ?lt LT0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
396 |
by (rule approx_loc_imp_approx_loc_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
397 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
398 |
with start l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
399 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
400 |
by (simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
401 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
402 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
403 |
have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
404 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
405 |
from s s' mC' step l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
406 |
have "G \<turnstile> LT <=l LT'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
407 |
by (simp add: step_def sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
408 |
with wfprog a_loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
409 |
have a: "approx_loc G hp loc LT'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
410 |
by (rule approx_loc_imp_approx_loc_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
411 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
412 |
from s s' mC' step l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
413 |
have "G \<turnstile> map Ok ST <=l map Ok (tl ST')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
414 |
by (auto simp add: step_def sup_state_def map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
415 |
with wfprog a_stk' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
416 |
have "approx_stk G hp stk' (tl ST')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
417 |
by (rule approx_stk_imp_approx_stk_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
418 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
419 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
420 |
by (simp add: correct_frame_def suc_l pc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
421 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
422 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
423 |
with state'_val heap_ok mD'' ins method phi_pc s X' l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
424 |
frames s' LT0 c_f c_f' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
425 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
426 |
by (simp add: correct_state_def) (intro exI conjI, force+) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
427 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
428 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
429 |
with Null_ok oX_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
430 |
show "G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
431 |
by - (cases oX, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
432 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
433 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
434 |
lemmas [simp del] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
435 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
436 |
lemma Return_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
437 |
"\<lbrakk> wt_jvm_prog G phi; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
438 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
439 |
ins ! pc = Return; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
440 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
441 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
442 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
443 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
444 |
apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
445 |
apply (frule wt_jvm_prog_impl_wt_instr) |
9819 | 446 |
apply (assumption, erule Suc_lessD) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
447 |
apply (unfold wt_jvm_prog_def) |
9819 | 448 |
apply (fastsimp |
449 |
dest: subcls_widen_methd |
|
450 |
elim: widen_trans [COMP swap_prems_rl] |
|
451 |
intro: conf_widen |
|
452 |
simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) |
|
453 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
454 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
455 |
lemmas [simp] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
456 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
457 |
lemma Goto_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
458 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
459 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
460 |
ins ! pc = Goto branch; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
461 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
462 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
463 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
464 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
465 |
apply (clarsimp simp add: defs1) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
466 |
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) |
9819 | 467 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
468 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
469 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
470 |
lemma Ifcmpeq_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
471 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
472 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
473 |
ins ! pc = Ifcmpeq branch; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
474 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
475 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
476 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
477 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
478 |
apply (clarsimp simp add: defs1) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
479 |
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) |
9819 | 480 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
481 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
482 |
lemma Pop_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
483 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
484 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
485 |
ins ! pc = Pop; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
486 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
487 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
488 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
489 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
490 |
apply (clarsimp simp add: defs1) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
491 |
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) |
9819 | 492 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
493 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
494 |
lemma Dup_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
495 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
496 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
497 |
ins ! pc = Dup; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
498 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
499 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
500 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
501 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
502 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
503 |
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
504 |
simp add: defs1 map_eq_Cons) |
9819 | 505 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
506 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
507 |
lemma Dup_x1_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
508 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
509 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
510 |
ins ! pc = Dup_x1; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
511 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
512 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
513 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
514 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
515 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
516 |
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
517 |
simp add: defs1 map_eq_Cons) |
9819 | 518 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
519 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
520 |
lemma Dup_x2_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
521 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
522 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
523 |
ins ! pc = Dup_x2; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
524 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
525 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
526 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
527 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
528 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
529 |
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
530 |
simp add: defs1 map_eq_Cons) |
9819 | 531 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
532 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
533 |
lemma Swap_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
534 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
535 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
536 |
ins ! pc = Swap; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
537 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
538 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
539 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
540 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
541 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
542 |
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
543 |
simp add: defs1 map_eq_Cons) |
9819 | 544 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
545 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
546 |
lemma IAdd_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
547 |
"\<lbrakk> wf_prog wt G; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
548 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
549 |
ins ! pc = IAdd; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
550 |
wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
551 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
552 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
553 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
554 |
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
555 |
apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup) |
9819 | 556 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
557 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
558 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
559 |
(** instr correct **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
560 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
561 |
lemma instr_correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
562 |
"\<lbrakk> wt_jvm_prog G phi; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
563 |
method (G,C) sig = Some (C,rT,maxl,ins); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
564 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
565 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
566 |
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
567 |
apply (frule wt_jvm_prog_impl_wt_instr_cor) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
568 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
569 |
apply (cases "ins!pc") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
570 |
prefer 9 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
571 |
apply (blast intro: Invoke_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
572 |
prefer 9 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
573 |
apply (blast intro: Return_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
574 |
apply (unfold wt_jvm_prog_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
575 |
apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
576 |
Checkcast_correct Getfield_correct Putfield_correct New_correct |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
577 |
Goto_correct Ifcmpeq_correct Pop_correct Dup_correct |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
578 |
Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+ |
9819 | 579 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
580 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
581 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
582 |
(** Main **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
583 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
584 |
lemma correct_state_impl_Some_method: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
585 |
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
586 |
\<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
587 |
by (auto simp add: correct_state_def Let_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
588 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
589 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
590 |
lemma BV_correct_1 [rulify]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
591 |
"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> |
9819 | 592 |
\<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
593 |
apply (simp only: split_tupled_all) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
594 |
apply (rename_tac xp hp frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
595 |
apply (case_tac xp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
596 |
apply (case_tac frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
597 |
apply simp |
9819 | 598 |
apply (simp only: split_tupled_all) |
599 |
apply hypsubst |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
600 |
apply (frule correct_state_impl_Some_method) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
601 |
apply (force intro: instr_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
602 |
apply (case_tac frs) |
9819 | 603 |
apply simp_all |
604 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
605 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
606 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
607 |
lemma L0: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
608 |
"\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
609 |
by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
610 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
611 |
lemma L1: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
612 |
"\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
613 |
\<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
614 |
apply (drule L0) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
615 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
616 |
apply (fast intro: BV_correct_1) |
9819 | 617 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
618 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
619 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
620 |
theorem BV_correct [rulify]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
621 |
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
622 |
apply (unfold exec_all_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
623 |
apply (erule rtrancl_induct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
624 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
625 |
apply (auto intro: BV_correct_1) |
9819 | 626 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
627 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
628 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
629 |
theorem BV_correct_initial: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
630 |
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
631 |
\<Longrightarrow> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
632 |
apply (drule BV_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
633 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
634 |
apply (simp add: correct_state_def correct_frame_def split_def split: option.splits) |
9819 | 635 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
636 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
637 |
end |