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