9 header "Type Safety Invariant" |
9 header "Type Safety Invariant" |
10 |
10 |
11 theory Correct = BVSpec: |
11 theory Correct = BVSpec: |
12 |
12 |
13 constdefs |
13 constdefs |
14 approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool" |
14 approx_val :: "[jvm_prog,aheap,val,ty err] => bool" |
15 "approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T" |
15 "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T" |
16 |
16 |
17 approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool" |
17 approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool" |
18 "approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT" |
18 "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT" |
19 |
19 |
20 approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool" |
20 approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool" |
21 "approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)" |
21 "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)" |
22 |
22 |
23 correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool" |
23 correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool" |
24 "correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
24 "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
25 approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> |
25 approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> |
26 pc < length ins \<and> length loc=length(snd sig)+maxl+1" |
26 pc < length ins \<and> length loc=length(snd sig)+maxl+1" |
27 |
27 |
28 correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool" |
28 correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool" |
29 "correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t" |
29 "correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t" |
30 |
30 |
31 |
31 |
32 consts |
32 consts |
33 correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool" |
33 correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool" |
34 primrec |
34 primrec |
35 "correct_frames G hp phi rT0 sig0 [] = True" |
35 "correct_frames G hp phi rT0 sig0 [] = True" |
36 |
36 |
37 "correct_frames G hp phi rT0 sig0 (f#frs) = |
37 "correct_frames G hp phi rT0 sig0 (f#frs) = |
38 (let (stk,loc,C,sig,pc) = f in |
38 (let (stk,loc,C,sig,pc) = f in |
50 correct_frame G hp (tl ST, LT) maxl ins f \<and> |
50 correct_frame G hp (tl ST, LT) maxl ins f \<and> |
51 correct_frames G hp phi rT sig frs))))" |
51 correct_frames G hp phi rT sig frs))))" |
52 |
52 |
53 |
53 |
54 constdefs |
54 constdefs |
55 correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool" |
55 correct_state :: "[jvm_prog,prog_type,jvm_state] => bool" |
56 ("_,_\<turnstile>JVM _\<surd>" [51,51] 50) |
56 ("_,_\<turnstile>JVM _\<surd>" [51,51] 50) |
57 "correct_state G phi \<equiv> \<lambda>(xp,hp,frs). |
57 "correct_state G phi == \<lambda>(xp,hp,frs). |
58 case xp of |
58 case xp of |
59 None \<Rightarrow> (case frs of |
59 None => (case frs of |
60 [] \<Rightarrow> True |
60 [] => True |
61 | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> |
61 | (f#fs) => G\<turnstile>h hp\<surd> \<and> |
62 (let (stk,loc,C,sig,pc) = f |
62 (let (stk,loc,C,sig,pc) = f |
63 in |
63 in |
64 \<exists>rT maxl ins s. |
64 \<exists>rT maxl ins s. |
65 method (G,C) sig = Some(C,rT,(maxl,ins)) \<and> |
65 method (G,C) sig = Some(C,rT,(maxl,ins)) \<and> |
66 phi C sig ! pc = Some s \<and> |
66 phi C sig ! pc = Some s \<and> |
67 correct_frame G hp s maxl ins f \<and> |
67 correct_frame G hp s maxl ins f \<and> |
68 correct_frames G hp phi rT sig fs)) |
68 correct_frames G hp phi rT sig fs)) |
69 | Some x \<Rightarrow> True" |
69 | Some x => True" |
70 |
70 |
71 |
71 |
72 lemma sup_heap_newref: |
72 lemma sup_heap_newref: |
73 "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)" |
73 "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)" |
74 apply (unfold hext_def) |
74 apply (unfold hext_def) |
75 apply clarsimp |
75 apply clarsimp |
76 apply (drule newref_None 1) back |
76 apply (drule newref_None 1) back |
77 apply simp |
77 apply simp |
78 . |
78 . |
79 |
79 |
80 lemma sup_heap_update_value: |
80 lemma sup_heap_update_value: |
81 "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))" |
81 "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))" |
82 by (simp add: hext_def) |
82 by (simp add: hext_def) |
83 |
83 |
84 |
84 |
85 (** approx_val **) |
85 (** approx_val **) |
86 |
86 |
91 lemma approx_val_Null: |
91 lemma approx_val_Null: |
92 "approx_val G hp Null (Ok (RefT x))" |
92 "approx_val G hp Null (Ok (RefT x))" |
93 by (auto intro: null simp add: approx_val_def) |
93 by (auto intro: null simp add: approx_val_def) |
94 |
94 |
95 lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
95 lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
96 "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')" |
96 "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')" |
97 by (cases T) (auto intro: conf_widen simp add: approx_val_def) |
97 by (cases T) (auto intro: conf_widen simp add: approx_val_def) |
98 |
98 |
99 lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
99 lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
100 "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at" |
100 "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at" |
101 apply (simp add: approx_val_def split: err.split) |
101 apply (simp add: approx_val_def split: err.split) |
102 apply (blast intro: conf_hext) |
102 apply (blast intro: conf_hext) |
103 . |
103 . |
104 |
104 |
105 lemma approx_val_imp_approx_val_heap_update: |
105 lemma approx_val_imp_approx_val_heap_update: |
106 "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> |
106 "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] |
107 \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T" |
107 ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
108 by (cases v, auto simp add: obj_ty_def conf_def) |
108 by (cases v, auto simp add: obj_ty_def conf_def) |
109 |
109 |
110 lemma approx_val_imp_approx_val_sup [rule_format]: |
110 lemma approx_val_imp_approx_val_sup [rule_format]: |
111 "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')" |
111 "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')" |
112 apply (simp add: sup_PTS_eq approx_val_def split: err.split) |
112 apply (simp add: sup_PTS_eq approx_val_def split: err.split) |
113 apply (blast intro: conf_widen) |
113 apply (blast intro: conf_widen) |
114 . |
114 . |
115 |
115 |
116 lemma approx_loc_imp_approx_val_sup: |
116 lemma approx_loc_imp_approx_val_sup: |
117 "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk> |
117 "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|] |
118 \<Longrightarrow> approx_val G hp v at" |
118 ==> approx_val G hp v at" |
119 apply (unfold approx_loc_def) |
119 apply (unfold approx_loc_def) |
120 apply (unfold list_all2_def) |
120 apply (unfold list_all2_def) |
121 apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth) |
121 apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth) |
122 . |
122 . |
123 |
123 |
127 lemma approx_loc_Cons [iff]: |
127 lemma approx_loc_Cons [iff]: |
128 "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)" |
128 "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)" |
129 by (simp add: approx_loc_def) |
129 by (simp add: approx_loc_def) |
130 |
130 |
131 lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
131 lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
132 "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
132 "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
133 \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> |
133 --> length tys_n = length ts --> approx_stk G hp s tys_n --> |
134 approx_loc G hp s (map Ok ts)" |
134 approx_loc G hp s (map Ok ts)" |
135 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
135 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
136 apply (clarsimp simp add: all_set_conv_all_nth) |
136 apply (clarsimp simp add: all_set_conv_all_nth) |
137 apply (rule approx_val_imp_approx_val_assConvertible) |
137 apply (rule approx_val_imp_approx_val_assConvertible) |
138 apply auto |
138 apply auto |
139 . |
139 . |
140 |
140 |
141 |
141 |
142 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
142 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
143 "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt" |
143 "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt" |
144 apply (unfold approx_loc_def list_all2_def) |
144 apply (unfold approx_loc_def list_all2_def) |
145 apply (cases lt) |
145 apply (cases lt) |
146 apply simp |
146 apply simp |
147 apply clarsimp |
147 apply clarsimp |
148 apply (rule approx_val_imp_approx_val_sup_heap) |
148 apply (rule approx_val_imp_approx_val_sup_heap) |
149 apply auto |
149 apply auto |
150 . |
150 . |
151 |
151 |
152 lemma approx_loc_imp_approx_loc_sup [rule_format]: |
152 lemma approx_loc_imp_approx_loc_sup [rule_format]: |
153 "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'" |
153 "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'" |
154 apply (unfold sup_loc_def approx_loc_def list_all2_def) |
154 apply (unfold sup_loc_def approx_loc_def list_all2_def) |
155 apply (auto simp add: all_set_conv_all_nth) |
155 apply (auto simp add: all_set_conv_all_nth) |
156 apply (auto elim: approx_val_imp_approx_val_sup) |
156 apply (auto elim: approx_val_imp_approx_val_sup) |
157 . |
157 . |
158 |
158 |
159 |
159 |
160 lemma approx_loc_imp_approx_loc_subst [rule_format]: |
160 lemma approx_loc_imp_approx_loc_subst [rule_format]: |
161 "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) |
161 "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) |
162 \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" |
162 --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" |
163 apply (unfold approx_loc_def list_all2_def) |
163 apply (unfold approx_loc_def list_all2_def) |
164 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
164 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
165 . |
165 . |
166 |
166 |
167 |
167 |
168 lemmas [cong] = conj_cong |
168 lemmas [cong] = conj_cong |
169 |
169 |
170 lemma approx_loc_append [rule_format]: |
170 lemma approx_loc_append [rule_format]: |
171 "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> |
171 "\<forall>L1 l2 L2. length l1=length L1 --> |
172 approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" |
172 approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" |
173 apply (unfold approx_loc_def list_all2_def) |
173 apply (unfold approx_loc_def list_all2_def) |
174 apply simp |
174 apply simp |
175 apply blast |
175 apply blast |
176 . |
176 . |
190 "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" |
190 "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" |
191 by (auto intro: subst [OF approx_stk_rev_lem]) |
191 by (auto intro: subst [OF approx_stk_rev_lem]) |
192 |
192 |
193 |
193 |
194 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
194 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
195 "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt" |
195 "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt" |
196 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) |
196 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) |
197 |
197 |
198 lemma approx_stk_imp_approx_stk_sup [rule_format]: |
198 lemma approx_stk_imp_approx_stk_sup [rule_format]: |
199 "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) |
199 "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) |
200 \<longrightarrow> approx_stk G hp lvars st'" |
200 --> approx_stk G hp lvars st'" |
201 by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def) |
201 by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def) |
202 |
202 |
203 lemma approx_stk_Nil [iff]: |
203 lemma approx_stk_Nil [iff]: |
204 "approx_stk G hp [] []" |
204 "approx_stk G hp [] []" |
205 by (simp add: approx_stk_def approx_loc_def) |
205 by (simp add: approx_stk_def approx_loc_def) |
213 "approx_stk G hp stk (S#ST') = |
213 "approx_stk G hp stk (S#ST') = |
214 (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')" |
214 (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')" |
215 by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def) |
215 by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def) |
216 |
216 |
217 lemma approx_stk_append_lemma: |
217 lemma approx_stk_append_lemma: |
218 "approx_stk G hp stk (S@ST') \<Longrightarrow> |
218 "approx_stk G hp stk (S@ST') ==> |
219 (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> |
219 (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> |
220 approx_stk G hp s S \<and> approx_stk G hp stk' ST')" |
220 approx_stk G hp s S \<and> approx_stk G hp stk' ST')" |
221 by (simp add: list_all2_append2 approx_stk_def approx_loc_def) |
221 by (simp add: list_all2_append2 approx_stk_def approx_loc_def) |
222 |
222 |
223 |
223 |
224 (** oconf **) |
224 (** oconf **) |
225 |
225 |
226 lemma correct_init_obj: |
226 lemma correct_init_obj: |
227 "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow> |
227 "[|is_class G C; wf_prog wt G|] ==> |
228 G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>" |
228 G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>" |
229 apply (unfold oconf_def lconf_def) |
229 apply (unfold oconf_def lconf_def) |
230 apply (simp add: map_of_map) |
230 apply (simp add: map_of_map) |
231 apply (force intro: defval_conf dest: map_of_SomeD is_type_fields) |
231 apply (force intro: defval_conf dest: map_of_SomeD is_type_fields) |
232 . |
232 . |
233 |
233 |
234 |
234 |
235 lemma oconf_imp_oconf_field_update [rule_format]: |
235 lemma oconf_imp_oconf_field_update [rule_format]: |
236 "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk> |
236 "[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |] |
237 \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>" |
237 ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>" |
238 by (simp add: oconf_def lconf_def) |
238 by (simp add: oconf_def lconf_def) |
239 |
239 |
240 |
240 |
241 lemma oconf_imp_oconf_heap_newref [rule_format]: |
241 lemma oconf_imp_oconf_heap_newref [rule_format]: |
242 "hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>" |
242 "hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>" |
243 apply (unfold oconf_def lconf_def) |
243 apply (unfold oconf_def lconf_def) |
244 apply simp |
244 apply simp |
245 apply (fast intro: conf_hext sup_heap_newref) |
245 apply (fast intro: conf_hext sup_heap_newref) |
246 . |
246 . |
247 |
247 |
248 |
248 |
249 lemma oconf_imp_oconf_heap_update [rule_format]: |
249 lemma oconf_imp_oconf_heap_update [rule_format]: |
250 "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> |
250 "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> |
251 \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" |
251 --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" |
252 apply (unfold oconf_def lconf_def) |
252 apply (unfold oconf_def lconf_def) |
253 apply simp |
253 apply simp |
254 apply (force intro: approx_val_imp_approx_val_heap_update) |
254 apply (force intro: approx_val_imp_approx_val_heap_update) |
255 . |
255 . |
256 |
256 |
257 |
257 |
258 (** hconf **) |
258 (** hconf **) |
259 |
259 |
260 |
260 |
261 lemma hconf_imp_hconf_newref [rule_format]: |
261 lemma hconf_imp_hconf_newref [rule_format]: |
262 "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>" |
262 "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>" |
263 apply (simp add: hconf_def) |
263 apply (simp add: hconf_def) |
264 apply (fast intro: oconf_imp_oconf_heap_newref) |
264 apply (fast intro: oconf_imp_oconf_heap_newref) |
265 . |
265 . |
266 |
266 |
267 lemma hconf_imp_hconf_field_update [rule_format]: |
267 lemma hconf_imp_hconf_field_update [rule_format]: |
268 "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
268 "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
269 G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>" |
269 G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>" |
270 apply (simp add: hconf_def) |
270 apply (simp add: hconf_def) |
271 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update |
271 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update |
272 simp add: obj_ty_def) |
272 simp add: obj_ty_def) |
273 . |
273 . |
274 |
274 |
275 (** correct_frames **) |
275 (** correct_frames **) |
276 |
276 |
277 lemmas [simp del] = fun_upd_apply |
277 lemmas [simp del] = fun_upd_apply |
278 |
278 |
279 lemma correct_frames_imp_correct_frames_field_update [rule_format]: |
279 lemma correct_frames_imp_correct_frames_field_update [rule_format]: |
280 "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> |
280 "\<forall>rT C sig. correct_frames G hp phi rT sig frs --> |
281 hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> |
281 hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd --> |
282 G,hp\<turnstile>v\<Colon>\<preceq>fd |
282 G,hp\<turnstile>v::\<preceq>fd |
283 \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs"; |
283 --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs"; |
284 apply (induct frs) |
284 apply (induct frs) |
285 apply simp |
285 apply simp |
286 apply (clarsimp simp add: correct_frame_def) (*takes long*) |
286 apply (clarsimp simp add: correct_frame_def) (*takes long*) |
287 apply (intro exI conjI) |
287 apply (intro exI conjI) |
288 apply simp |
288 apply simp |