author | kleing |
Fri, 09 Feb 2001 16:01:58 +0100 | |
changeset 11085 | b830bf10bf71 |
parent 10920 | 9b74eceea2d2 |
child 11252 | 71c00cb091d2 |
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 |
||
10056 | 10 |
header "BV Type Safety Proof" |
9757
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 |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
14 |
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def |
10056 | 15 |
wt_instr_def step_def |
16 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
17 |
lemmas [simp del] = split_paired_All |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
18 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
19 |
lemma wt_jvm_prog_impl_wt_instr_cor: |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
20 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
21 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
10592 | 22 |
==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
23 |
apply (unfold correct_state_def Let_def correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
24 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
25 |
apply (blast intro: wt_jvm_prog_impl_wt_instr) |
9819 | 26 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
27 |
|
11085 | 28 |
section {* Single Instructions *} |
29 |
||
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
30 |
lemmas [iff] = not_Err_eq |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
31 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
32 |
lemma Load_correct: |
10042 | 33 |
"[| wf_prog wt G; |
10592 | 34 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
10056 | 35 |
ins!pc = Load idx; |
10592 | 36 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
10056 | 37 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
38 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
39 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
40 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
41 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
42 |
apply (rule approx_loc_imp_approx_val_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
43 |
apply simp+ |
10056 | 44 |
apply (blast intro: approx_stk_imp_approx_stk_sup |
45 |
approx_loc_imp_approx_loc_sup) |
|
9819 | 46 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
47 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
48 |
lemma Store_correct: |
10042 | 49 |
"[| wf_prog wt G; |
10592 | 50 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
51 |
ins!pc = Store idx; |
10592 | 52 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
53 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
54 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
55 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
56 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
57 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
58 |
apply (blast intro: approx_stk_imp_approx_stk_sup) |
10056 | 59 |
apply (blast intro: approx_loc_imp_approx_loc_subst |
60 |
approx_loc_imp_approx_loc_sup) |
|
9819 | 61 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
62 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
63 |
|
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
64 |
lemma LitPush_correct: |
10042 | 65 |
"[| wf_prog wt G; |
10592 | 66 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
67 |
ins!pc = LitPush v; |
10592 | 68 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
10056 | 69 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
70 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
71 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
72 |
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
73 |
apply (blast dest: conf_litval intro: conf_widen approx_stk_imp_approx_stk_sup |
10056 | 74 |
approx_loc_imp_approx_loc_sup) |
9819 | 75 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
76 |
|
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
77 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
78 |
lemma Cast_conf2: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
79 |
"[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
80 |
G\<turnstile>Class C\<preceq>T; is_class G C|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
81 |
==> G,h\<turnstile>v::\<preceq>T" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
82 |
apply (unfold cast_ok_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
83 |
apply (frule widen_Class) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
84 |
apply (elim exE disjE) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
85 |
apply (simp add: null) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
86 |
apply (clarsimp simp add: conf_def obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
87 |
apply (cases v) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
88 |
apply (auto intro: rtrancl_trans) |
9819 | 89 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
90 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
91 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
92 |
lemma Checkcast_correct: |
10042 | 93 |
"[| wf_prog wt G; |
10592 | 94 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
10056 | 95 |
ins!pc = Checkcast D; |
10592 | 96 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
10056 | 97 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
98 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
99 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
100 |
apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def) |
10056 | 101 |
apply (blast intro: approx_stk_imp_approx_stk_sup |
102 |
approx_loc_imp_approx_loc_sup Cast_conf2) |
|
9819 | 103 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
104 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
105 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
106 |
lemma Getfield_correct: |
10042 | 107 |
"[| wf_prog wt G; |
10592 | 108 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
109 |
ins!pc = Getfield F D; |
10592 | 110 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
111 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
112 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
113 |
==> G,phi \<turnstile>JVM state'\<surd>" |
10056 | 114 |
apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def |
115 |
split: option.split) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
116 |
apply (frule conf_widen) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
117 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
118 |
apply (drule conf_RefTD) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
119 |
apply (clarsimp simp add: defs1 approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
120 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
121 |
apply (drule widen_cfs_fields) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
122 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
123 |
apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def) |
10056 | 124 |
apply (blast intro: approx_stk_imp_approx_stk_sup |
125 |
approx_loc_imp_approx_loc_sup) |
|
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 |
lemma Putfield_correct: |
10042 | 129 |
"[| wf_prog wt G; |
10592 | 130 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
131 |
ins!pc = Putfield F D; |
10592 | 132 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
133 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
134 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
135 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
136 |
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
|
137 |
apply (clarsimp simp add: approx_val_def) |
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 |
prefer 2 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
140 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
141 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
142 |
apply (drule conf_RefTD) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
143 |
apply clarsimp |
10056 | 144 |
apply (blast |
145 |
intro: |
|
11085 | 146 |
hext_upd_obj approx_stk_imp_approx_stk_sup_heap |
10056 | 147 |
approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup_heap |
148 |
approx_loc_imp_approx_loc_sup hconf_imp_hconf_field_update |
|
149 |
correct_frames_imp_correct_frames_field_update conf_widen |
|
150 |
dest: |
|
151 |
widen_cfs_fields) |
|
9819 | 152 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
153 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
154 |
lemma New_correct: |
10042 | 155 |
"[| wf_prog wt G; |
10592 | 156 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
10920 | 157 |
ins!pc = New X; |
10592 | 158 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
159 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
160 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
161 |
==> G,phi \<turnstile>JVM state'\<surd>" |
10920 | 162 |
proof - |
163 |
assume wf: "wf_prog wt G" |
|
164 |
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" |
|
165 |
assume ins: "ins!pc = New X" |
|
166 |
assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
|
167 |
assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
|
168 |
assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
|
169 |
||
170 |
from ins conf meth |
|
171 |
obtain ST LT where |
|
172 |
heap_ok: "G\<turnstile>h hp\<surd>" and |
|
173 |
phi_pc: "phi C sig!pc = Some (ST,LT)" and |
|
174 |
is_class_C: "is_class G C" and |
|
175 |
frame: "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and |
|
176 |
frames: "correct_frames G hp phi rT sig frs" |
|
177 |
by (auto simp add: correct_state_def iff del: not_None_eq) |
|
178 |
from phi_pc ins wt |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
179 |
|
10920 | 180 |
obtain ST' LT' where |
181 |
is_class_X: "is_class G X" and |
|
182 |
maxs: "maxs < length ST" and |
|
183 |
suc_pc: "Suc pc < length ins" and |
|
184 |
phi_suc: "phi C sig ! Suc pc = Some (ST', LT')" and |
|
185 |
less: "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')" |
|
186 |
by (unfold wt_instr_def step_def) auto |
|
187 |
||
188 |
obtain oref xp' where |
|
189 |
new_Addr: "(oref,xp') = new_Addr hp" |
|
190 |
by (cases "new_Addr hp") auto |
|
191 |
hence cases: |
|
192 |
"hp oref = None \<and> xp' = None \<or> xp' = Some OutOfMemory" |
|
193 |
by (blast dest: new_AddrD) |
|
194 |
moreover |
|
195 |
{ assume "xp' = Some OutOfMemory" |
|
196 |
with exec ins meth new_Addr [symmetric] |
|
197 |
have "state' = (Some OutOfMemory, hp, (stk, loc, C, sig, Suc pc) # frs)" |
|
198 |
by simp |
|
199 |
hence ?thesis |
|
200 |
by (simp add: correct_state_def) |
|
201 |
} |
|
202 |
moreover |
|
203 |
{ assume hp: "hp oref = None" and "xp' = None" |
|
204 |
with exec ins meth new_Addr [symmetric] |
|
205 |
have state': |
|
206 |
"state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))), |
|
207 |
(Addr oref # stk, loc, C, sig, Suc pc) # frs)" |
|
208 |
(is "state' = Norm (?hp', ?f # frs)") |
|
209 |
by simp |
|
210 |
moreover |
|
211 |
from wf hp heap_ok is_class_X |
|
212 |
have hp': "G \<turnstile>h ?hp' \<surd>" |
|
213 |
by - (rule hconf_imp_hconf_newref, |
|
214 |
auto simp add: oconf_def dest: fields_is_type) |
|
215 |
moreover |
|
216 |
from hp |
|
11085 | 217 |
have sup: "hp \<le>| ?hp'" by (rule hext_new) |
10920 | 218 |
from hp frame less suc_pc wf |
219 |
have "correct_frame G ?hp' (ST', LT') maxl ins ?f" |
|
220 |
apply (unfold correct_frame_def sup_state_conv) |
|
221 |
apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def) |
|
222 |
apply (blast intro: approx_stk_imp_approx_stk_sup_heap |
|
223 |
approx_stk_imp_approx_stk_sup |
|
224 |
approx_loc_imp_approx_loc_sup_heap |
|
225 |
approx_loc_imp_approx_loc_sup sup) |
|
226 |
done |
|
227 |
moreover |
|
228 |
from hp frames wf heap_ok is_class_X |
|
229 |
have "correct_frames G ?hp' phi rT sig frs" |
|
230 |
by - (rule correct_frames_imp_correct_frames_newref, |
|
231 |
auto simp add: oconf_def dest: fields_is_type) |
|
232 |
ultimately |
|
233 |
have ?thesis |
|
234 |
by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq) |
|
235 |
} |
|
236 |
ultimately |
|
237 |
show ?thesis by auto |
|
238 |
qed |
|
11085 | 239 |
|
9757
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 |
lemmas [simp del] = split_paired_Ex |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
242 |
|
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
243 |
lemma Invoke_correct: |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
244 |
"[| wt_jvm_prog G phi; |
10592 | 245 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
246 |
ins ! pc = Invoke C' mn pTs; |
10592 | 247 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
248 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
249 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
250 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
251 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
252 |
assume wtprog: "wt_jvm_prog G phi" |
10592 | 253 |
assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
254 |
assume ins: "ins ! pc = Invoke C' mn pTs" |
10592 | 255 |
assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
256 |
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
257 |
assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
258 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
259 |
from wtprog |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
260 |
obtain wfmb where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
261 |
wfprog: "wf_prog wfmb G" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
262 |
by (simp add: wt_jvm_prog_def) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
263 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
264 |
from ins method approx |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
265 |
obtain s where |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
266 |
heap_ok: "G\<turnstile>h hp\<surd>" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
267 |
phi_pc: "phi C sig!pc = Some s" and |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
268 |
is_class_C: "is_class G C" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
269 |
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
|
270 |
frames: "correct_frames G hp phi rT sig frs" |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
271 |
by (clarsimp simp add: correct_state_def iff del: not_None_eq) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
272 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
273 |
from ins wti phi_pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
274 |
obtain apTs X ST LT D' rT body where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
275 |
s: "s = (rev apTs @ X # ST, LT)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
276 |
l: "length apTs = length pTs" and |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
277 |
is_class: "is_class G C'" and |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
278 |
X: "G\<turnstile> X \<preceq> Class C'" and |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
279 |
w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
280 |
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
|
281 |
pc: "Suc pc < length ins" and |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
282 |
step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
283 |
by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
284 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
285 |
from step |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
286 |
obtain ST' LT' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
287 |
s': "phi C sig ! Suc pc = Some (ST', LT')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
288 |
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
|
289 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
290 |
from X |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
291 |
obtain T where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
292 |
X_Ref: "X = RefT T" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
293 |
by - (drule widen_RefT2, erule exE, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
294 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
295 |
from s ins frame |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
296 |
obtain |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
297 |
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
|
298 |
a_loc: "approx_loc G hp loc LT" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
299 |
suc_l: "length loc = Suc (length (snd sig) + maxl)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
300 |
by (simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
301 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
302 |
from a_stk |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
303 |
obtain opTs stk' oX where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
304 |
opTs: "approx_stk G hp opTs (rev apTs)" and |
10496 | 305 |
oX: "approx_val G hp oX (OK X)" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
306 |
a_stk': "approx_stk G hp stk' ST" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
307 |
stk': "stk = opTs @ oX # stk'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
308 |
l_o: "length opTs = length apTs" |
10592 | 309 |
"length stk' = length ST" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
310 |
by - (drule approx_stk_append_lemma, simp, elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
311 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
312 |
from oX |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
313 |
have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
314 |
by (clarsimp simp add: approx_val_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
315 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
316 |
with X_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
317 |
obtain T' where |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
318 |
oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
319 |
"G \<turnstile> RefT T' \<preceq> X" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
320 |
apply (elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
321 |
apply (frule widen_RefT2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
322 |
by (elim, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
323 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
324 |
from stk' l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
325 |
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
326 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
327 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
328 |
with state' method ins |
10042 | 329 |
have Null_ok: "oX = Null ==> ?thesis" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
330 |
by (simp add: correct_state_def raise_xcpt_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
331 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
332 |
{ fix ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
333 |
assume oX_Addr: "oX = Addr ref" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
334 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
335 |
with oX_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
336 |
obtain obj where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
337 |
loc: "hp ref = Some obj" "obj_ty obj = RefT T'" |
10387 | 338 |
by auto |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
339 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
340 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
341 |
obtain D where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
342 |
obj_ty: "obj_ty obj = Class D" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
343 |
by (auto simp add: obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
344 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
345 |
with X_Ref oX_Ref loc |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
346 |
obtain D: "G \<turnstile> Class D \<preceq> X" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
347 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
348 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
349 |
with X_Ref |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
350 |
obtain X' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
351 |
X': "X = Class X'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
352 |
by - (drule widen_Class, elim, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
353 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
354 |
with X |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
355 |
have X'_subcls: "G \<turnstile> X' \<preceq>C C'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
356 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
357 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
358 |
with mC' wfprog |
10592 | 359 |
obtain D0 rT0 maxs0 maxl0 ins0 where |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
360 |
mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT" |
10387 | 361 |
by (auto dest: subtype_widen_methd intro: that) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
362 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
363 |
from X' D |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
364 |
have D_subcls: "G \<turnstile> D \<preceq>C X'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
365 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
366 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
367 |
with wfprog mX |
10592 | 368 |
obtain D'' rT' mxs' mxl' ins' where |
369 |
mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
370 |
"G \<turnstile> rT' \<preceq> rT0" |
10387 | 371 |
by (auto dest: subtype_widen_methd intro: that) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
372 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
373 |
from mX mD |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
374 |
have rT': "G \<turnstile> rT' \<preceq> rT" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
375 |
by - (rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
376 |
|
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
377 |
from is_class X'_subcls D_subcls |
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
378 |
have is_class_D: "is_class G D" |
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
379 |
by (auto dest: subcls_is_class2) |
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
380 |
|
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
381 |
with mD wfprog |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
382 |
obtain mD'': |
10592 | 383 |
"method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" |
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
384 |
"is_class G D''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
385 |
by (auto dest: method_in_md) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
386 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
387 |
from loc obj_ty |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
388 |
have "fst (the (hp ref)) = D" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
389 |
by (simp add: obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
390 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
391 |
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
|
392 |
have state'_val: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
393 |
"state' = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
394 |
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
395 |
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
|
396 |
(is "state' = Norm (hp, ?f # ?f' # frs)") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
397 |
by (simp add: raise_xcpt_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
398 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
399 |
from wtprog mD'' |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
400 |
have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
401 |
by (auto dest: wt_jvm_prog_impl_wt_start) |
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 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
404 |
obtain LT0 where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
405 |
LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
406 |
by (clarsimp simp add: wt_start_def sup_state_conv) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
407 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
408 |
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
|
409 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
410 |
from start LT0 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
411 |
have sup_loc: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
412 |
"G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
413 |
(is "G \<turnstile> ?LT <=l LT0") |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
414 |
by (simp add: wt_start_def sup_state_conv) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
415 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
416 |
have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" |
10056 | 417 |
by (simp add: approx_loc_def approx_val_Err |
418 |
list_all2_def set_replicate_conv_if) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
419 |
|
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
420 |
from wfprog mD is_class_D |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
421 |
have "G \<turnstile> Class D \<preceq> Class D''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
422 |
by (auto dest: method_wf_mdecl) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
423 |
with obj_ty loc |
10496 | 424 |
have a: "approx_val G hp (Addr ref) (OK (Class D''))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
425 |
by (simp add: approx_val_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
426 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
427 |
from w l |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
428 |
have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
429 |
by (auto simp add: zip_rev) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
430 |
with wfprog l l_o opTs |
10496 | 431 |
have "approx_loc G hp opTs (map OK (rev pTs))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
432 |
by (auto intro: assConv_approx_stk_imp_approx_loc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
433 |
hence "approx_stk G hp opTs (rev pTs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
434 |
by (simp add: approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
435 |
hence "approx_stk G hp (rev opTs) pTs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
436 |
by (simp add: approx_stk_rev) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
437 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
438 |
with r a l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
439 |
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
|
440 |
(is "approx_loc G hp ?lt ?LT") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
441 |
by (auto simp add: approx_loc_append approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
442 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
443 |
from wfprog this sup_loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
444 |
have "approx_loc G hp ?lt LT0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
445 |
by (rule approx_loc_imp_approx_loc_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
446 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
447 |
with start l_o l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
448 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
449 |
by (simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
450 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
451 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
452 |
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
|
453 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
454 |
from s s' mC' step l |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
455 |
have "G \<turnstile> LT <=l LT'" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
456 |
by (simp add: step_def sup_state_conv) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
457 |
with wfprog a_loc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
458 |
have a: "approx_loc G hp loc LT'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
459 |
by (rule approx_loc_imp_approx_loc_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
460 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
461 |
from s s' mC' step l |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
462 |
have "G \<turnstile> map OK ST <=l map OK (tl ST')" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
463 |
by (auto simp add: step_def sup_state_conv map_eq_Cons) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
464 |
with wfprog a_stk' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
465 |
have "approx_stk G hp stk' (tl ST')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
466 |
by (rule approx_stk_imp_approx_stk_sup) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
467 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
468 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
469 |
by (simp add: correct_frame_def suc_l pc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
470 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
471 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
472 |
with state'_val heap_ok mD'' ins method phi_pc s X' l |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
473 |
frames s' LT0 c_f c_f' is_class_C |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
474 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
475 |
by (simp add: correct_state_def) (intro exI conjI, force+) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
476 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
477 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
478 |
with Null_ok oX_Ref |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
479 |
show "G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
480 |
by - (cases oX, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
481 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
482 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
483 |
lemmas [simp del] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
484 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
485 |
lemma Return_correct: |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
486 |
"[| wt_jvm_prog G phi; |
10592 | 487 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
488 |
ins ! pc = Return; |
10592 | 489 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
490 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
491 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
492 |
==> G,phi \<turnstile>JVM state'\<surd>" |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
493 |
apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
494 |
apply (frule wt_jvm_prog_impl_wt_instr) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
495 |
apply (assumption, assumption, erule Suc_lessD) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
496 |
apply (unfold wt_jvm_prog_def) |
9819 | 497 |
apply (fastsimp |
498 |
dest: subcls_widen_methd |
|
499 |
elim: widen_trans [COMP swap_prems_rl] |
|
500 |
intro: conf_widen |
|
501 |
simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) |
|
502 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
503 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
504 |
lemmas [simp] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
505 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
506 |
lemma Goto_correct: |
10042 | 507 |
"[| wf_prog wt G; |
10592 | 508 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
509 |
ins ! pc = Goto branch; |
10592 | 510 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
511 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
512 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
513 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
514 |
apply (clarsimp simp add: defs1) |
10056 | 515 |
apply (fast intro: approx_loc_imp_approx_loc_sup |
516 |
approx_stk_imp_approx_stk_sup) |
|
9819 | 517 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
518 |
|
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 Ifcmpeq_correct: |
10042 | 521 |
"[| wf_prog wt G; |
10592 | 522 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
523 |
ins ! pc = Ifcmpeq branch; |
10592 | 524 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
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) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
526 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
527 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
528 |
apply (clarsimp simp add: defs1) |
10056 | 529 |
apply (fast intro: approx_loc_imp_approx_loc_sup |
530 |
approx_stk_imp_approx_stk_sup) |
|
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 Pop_correct: |
10042 | 534 |
"[| wf_prog wt G; |
10592 | 535 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
536 |
ins ! pc = Pop; |
10592 | 537 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
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) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
539 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
540 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
541 |
apply (clarsimp simp add: defs1) |
10056 | 542 |
apply (fast intro: approx_loc_imp_approx_loc_sup |
543 |
approx_stk_imp_approx_stk_sup) |
|
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 Dup_correct: |
10042 | 547 |
"[| wf_prog wt G; |
10592 | 548 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
549 |
ins ! pc = Dup; |
10592 | 550 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
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) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
552 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
553 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
554 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
10056 | 555 |
apply (force intro: approx_stk_imp_approx_stk_sup |
556 |
approx_val_imp_approx_val_sup |
|
557 |
approx_loc_imp_approx_loc_sup |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
558 |
simp add: defs1 map_eq_Cons) |
9819 | 559 |
done |
9757
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 Dup_x1_correct: |
10042 | 562 |
"[| wf_prog wt G; |
10592 | 563 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
564 |
ins ! pc = Dup_x1; |
10592 | 565 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
566 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
567 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
568 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
569 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
10056 | 570 |
apply (force intro: approx_stk_imp_approx_stk_sup |
571 |
approx_val_imp_approx_val_sup |
|
572 |
approx_loc_imp_approx_loc_sup |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
573 |
simp add: defs1 map_eq_Cons) |
9819 | 574 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
575 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
576 |
lemma Dup_x2_correct: |
10042 | 577 |
"[| wf_prog wt G; |
10592 | 578 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
579 |
ins ! pc = Dup_x2; |
10592 | 580 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
581 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
582 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
583 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
584 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
10056 | 585 |
apply (force intro: approx_stk_imp_approx_stk_sup |
586 |
approx_val_imp_approx_val_sup |
|
587 |
approx_loc_imp_approx_loc_sup |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
588 |
simp add: defs1 map_eq_Cons) |
9819 | 589 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
590 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
591 |
lemma Swap_correct: |
10042 | 592 |
"[| wf_prog wt G; |
10592 | 593 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
594 |
ins ! pc = Swap; |
10592 | 595 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
596 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
597 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
598 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
599 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
10056 | 600 |
apply (force intro: approx_stk_imp_approx_stk_sup |
601 |
approx_val_imp_approx_val_sup |
|
602 |
approx_loc_imp_approx_loc_sup |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
603 |
simp add: defs1 map_eq_Cons) |
9819 | 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 |
lemma IAdd_correct: |
10042 | 607 |
"[| wf_prog wt G; |
10592 | 608 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
609 |
ins ! pc = IAdd; |
10592 | 610 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
611 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
612 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
613 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
614 |
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) |
10056 | 615 |
apply (blast intro: approx_stk_imp_approx_stk_sup |
616 |
approx_val_imp_approx_val_sup |
|
617 |
approx_loc_imp_approx_loc_sup) |
|
9819 | 618 |
done |
9757
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 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
621 |
lemma instr_correct: |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
622 |
"[| wt_jvm_prog G phi; |
10592 | 623 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
624 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
625 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
626 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
627 |
apply (frule wt_jvm_prog_impl_wt_instr_cor) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
628 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
629 |
apply (cases "ins!pc") |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
630 |
prefer 8 |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
631 |
apply (rule Invoke_correct, assumption+) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
632 |
prefer 8 |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
633 |
apply (rule Return_correct, assumption+) |
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
634 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
635 |
apply (unfold wt_jvm_prog_def) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
636 |
apply (rule Load_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
637 |
apply (rule Store_correct, assumption+) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
638 |
apply (rule LitPush_correct, assumption+) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
639 |
apply (rule New_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
640 |
apply (rule Getfield_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
641 |
apply (rule Putfield_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
642 |
apply (rule Checkcast_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
643 |
apply (rule Pop_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
644 |
apply (rule Dup_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
645 |
apply (rule Dup_x1_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
646 |
apply (rule Dup_x2_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
647 |
apply (rule Swap_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
648 |
apply (rule IAdd_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
649 |
apply (rule Goto_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
650 |
apply (rule Ifcmpeq_correct, assumption+) |
9819 | 651 |
done |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
652 |
|
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
653 |
|
11085 | 654 |
section {* Main *} |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
655 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
656 |
lemma correct_state_impl_Some_method: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
657 |
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
658 |
==> \<exists>meth. method (G,C) sig = Some(C,meth)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
659 |
by (auto simp add: correct_state_def Let_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
660 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
661 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
662 |
lemma BV_correct_1 [rule_format]: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
663 |
"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
664 |
==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>" |
9819 | 665 |
apply (simp only: split_tupled_all) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
666 |
apply (rename_tac xp hp frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
667 |
apply (case_tac xp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
668 |
apply (case_tac frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
669 |
apply simp |
9819 | 670 |
apply (simp only: split_tupled_all) |
671 |
apply hypsubst |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
672 |
apply (frule correct_state_impl_Some_method) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
673 |
apply (force intro: instr_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
674 |
apply (case_tac frs) |
9819 | 675 |
apply simp_all |
676 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
677 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
678 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
679 |
lemma L0: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
680 |
"[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
681 |
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
|
682 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
683 |
lemma L1: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
684 |
"[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
685 |
==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
686 |
apply (drule L0) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
687 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
688 |
apply (fast intro: BV_correct_1) |
9819 | 689 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
690 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
691 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
692 |
theorem BV_correct [rule_format]: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
693 |
"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
694 |
apply (unfold exec_all_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
695 |
apply (erule rtrancl_induct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
696 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
697 |
apply (auto intro: BV_correct_1) |
9819 | 698 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
699 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
700 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
701 |
theorem BV_correct_initial: |
10056 | 702 |
"[| wt_jvm_prog G phi; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
703 |
G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
704 |
==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and> |
10056 | 705 |
approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
706 |
apply (drule BV_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
707 |
apply assumption+ |
10056 | 708 |
apply (simp add: correct_state_def correct_frame_def split_def |
709 |
split: option.splits) |
|
9819 | 710 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
711 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
712 |
end |