1 (* Title: HOL/MicroJava/BV/Correct.ML
4 Copyright 1999 Technische Universitaet Muenchen
10 "hp x = None \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> obj))";
11 by (asm_full_simp_tac (simpset() addsimps []) 1);
15 by (asm_full_simp_tac (simpset() addsimps []) 1);
16 qed_spec_mp "sup_heap_newref";
20 "hp a = Some (cn,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (cn,od)))";
21 by (asm_full_simp_tac (simpset() addsimps []) 1);
22 qed_spec_mp "sup_heap_update_value";
27 Goalw [approx_val_def]
28 "approx_val G hp x None";
29 by (Asm_full_simp_tac 1);
30 qed_spec_mp "approx_val_None";
33 Goalw [approx_val_def]
34 "approx_val G hp Null (Some(RefT x))";
36 by (fast_tac (claset() addIs widen.intrs) 1);
37 qed_spec_mp "approx_val_Null";
41 "\\<lbrakk> wf_prog wt G \\<rbrakk> \
42 \\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
43 by (exhaust_tac "T" 1);
45 by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
46 qed_spec_mp "approx_val_imp_approx_val_assConvertible";
50 "approx_val G hp val at \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_val G hp' val at";
51 by (asm_full_simp_tac (simpset() setloop (split_tac [option.split])
52 addsimps [approx_val_def]) 1);
53 by(blast_tac (claset() addIs [conf_hext]) 1);
54 qed_spec_mp "approx_val_imp_approx_val_sup_heap";
57 "\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
58 \\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
59 by (exhaust_tac "v" 1);
60 by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
61 qed_spec_mp "approx_val_imp_approx_val_heap_update";
65 "wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
66 by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
67 by(blast_tac (claset() addIs [conf_widen]) 1);
68 qed_spec_mp "approx_val_imp_approx_val_sup";
72 "\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
73 \\\<Longrightarrow> approx_val G hp val at";
74 by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
75 [split_def,approx_loc_def,all_set_conv_all_nth])) 1);
76 qed "approx_loc_imp_approx_val_sup";
82 "approx_loc G hp (s#xs) (l#ls) = \
83 \ ((length xs = length ls) \\<and> (approx_val G hp s l) \\<and> (approx_loc G hp xs ls))";
84 by (fast_tac (claset() addss (simpset() addsimps [approx_loc_def])) 1);
85 qed "approx_loc_Cons";
88 Goalw [approx_stk_def,approx_loc_def]
89 "\\<lbrakk> wf_prog wt G \\<rbrakk> \
90 \\\<Longrightarrow> (\\<forall>tt'\\<in>set (zip tys_n ts). tt' \\<in> widen G) \\<longrightarrow> \
91 \ length tys_n = length ts \\<longrightarrow> approx_stk G hp s tys_n \\<longrightarrow> approx_loc G hp s (map Some ts)";
92 by (force_tac (claset() addIs [approx_val_imp_approx_val_assConvertible], simpset()
93 addsimps [all_set_conv_all_nth,split_def]) 1);
94 qed_spec_mp "assConv_approx_stk_imp_approx_loc";
97 Goalw [approx_loc_def]
98 "\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
99 by (exhaust_tac "lt" 1);
101 by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
102 simpset() addsimps [neq_Nil_conv]) 1);
103 qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
106 Goalw [sup_loc_def,approx_loc_def]
107 "wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
108 by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
109 by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
110 qed_spec_mp "approx_loc_imp_approx_loc_sup";
113 Goalw [approx_loc_def]
114 "\\<forall>loc idx x X. (approx_loc G hp loc LT) \\<longrightarrow> (approx_val G hp x X) \
115 \ \\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))";
116 by (fast_tac (claset() addDs [set_update_subset RS subsetD]
117 addss (simpset() addsimps [zip_update])) 1);
118 qed_spec_mp "approx_loc_imp_approx_loc_subst";
122 "\\<forall>L1 l2 L2. length l1=length L1 \
123 \ \\<longrightarrow> approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\<and> approx_loc G hp l2 L2)";
124 by (induct_tac "l1" 1);
125 by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_loc_def])) 1);
127 by (exhaust_tac "L1" 1);
128 by (asm_full_simp_tac (simpset() addsimps []) 1);
129 by (asm_full_simp_tac (simpset() addsimps []) 1);
131 by (asm_full_simp_tac (simpset() addsimps [approx_loc_Cons]) 1);
132 by (case_tac "length l2 = length L2" 1);
133 by (asm_full_simp_tac (simpset() addsimps []) 1);
134 by (asm_full_simp_tac (simpset() addsimps [approx_loc_def]) 1);
135 qed_spec_mp "approx_loc_append";
140 Goalw [approx_stk_def,approx_loc_def]
141 "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t";
142 by (fast_tac (claset() addss (simpset() addsimps [zip_rev,rev_map RS sym])) 1);
143 qed_spec_mp "approx_stk_rev_lem";
146 "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)";
147 by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset())) 1);
148 qed_spec_mp "approx_stk_rev";
150 Goalw [approx_stk_def]
151 "\\<forall> lvars. approx_stk G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_stk G hp' lvars lt";
152 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap]) 1);
153 qed_spec_mp "approx_stk_imp_approx_stk_sup_heap";
156 Goalw [approx_stk_def]
157 "wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st') >>= (map Some st) \\<longrightarrow> approx_stk G hp lvars st'";
158 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
159 qed_spec_mp "approx_stk_imp_approx_stk_sup";
161 Goalw [approx_stk_def,approx_loc_def]
162 "approx_stk G hp [] []";
163 by (asm_full_simp_tac (simpset() addsimps []) 1);
164 qed "approx_stk_Nil";
167 Goalw [approx_stk_def,approx_loc_def]
168 "approx_stk G hp (x # stk) (S#ST) = (approx_stk G hp stk ST \\<and> approx_val G hp x (Some S))";
169 by (fast_tac (claset() addss (simpset())) 1);
170 qed "approx_stk_Cons";
173 "\\<lbrakk> approx_stk G hp stk (S#ST') \\<rbrakk> \
174 \ \\<Longrightarrow> \\<exists>s stk'. stk = s#stk' \\<and> approx_stk G hp stk' ST' \\<and> approx_val G hp s (Some S)";
175 by (exhaust_tac "stk" 1);
176 by (fast_tac (claset() addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
177 by (fast_tac (claset() addss (simpset() addsimps [approx_stk_Cons])) 1);
178 qed "approx_stk_Cons_lemma";
181 "\\<forall>ST' stk. approx_stk G hp stk (S@ST') \
182 \ \\<longrightarrow> (\\<exists>s stk'. stk = s@stk' \\<and> length s = length S \\<and> length stk' = length ST' \\<and> \
183 \ approx_stk G hp s S \\<and> approx_stk G hp stk' ST')";
184 by (induct_tac "S" 1);
185 by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
187 by (asm_full_simp_tac (simpset() addsimps []) 1);
188 bd approx_stk_Cons_lemma 1;
190 by (eres_inst_tac [("x","ST'")] allE 1);
191 by (eres_inst_tac [("x","stk'")] allE 1);
193 by (res_inst_tac [("x","s#sa")] exI 1);
194 by (res_inst_tac [("x","stk'a")] exI 1);
195 by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
196 qed_spec_mp "approx_stk_append_lemma";
201 Goalw [oconf_def,lconf_def]
202 "\\<lbrakk> is_class G C; wf_prog wt G \\<rbrakk> \\<Longrightarrow> \
203 \G,h\\<turnstile> (C, map_of (map (\\<lambda>(f,fT).(f,default_val fT)) (fields(G,C))))\\<surd>";
204 by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
205 by (force_tac (claset() addIs [defval_conf]
206 addDs [map_of_SomeD,is_type_fields],simpset()) 1);
207 qed "correct_init_obj";
210 Goalw [oconf_def,lconf_def]
211 "\\<lbrakk> map_of (fields (G, oT)) FD = Some T ; G,hp\\<turnstile>v\\<Colon>\\<preceq>T ; \
212 \ G,hp\\<turnstile>(oT,fs)\\<surd> \\<rbrakk> \
213 \\\<Longrightarrow> G,hp\\<turnstile>(oT, fs(FD\\<mapsto>v))\\<surd>";
214 by (asm_full_simp_tac (simpset() addsplits [ty.split]) 1);
215 qed_spec_mp "oconf_imp_oconf_field_update";
218 Goalw [oconf_def,lconf_def]
219 "hp x = None \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj'\\<surd> \
220 \ \\<longrightarrow> G,(hp(newref hp\\<mapsto>obj'))\\<turnstile>obj\\<surd>";
221 by (Asm_full_simp_tac 1);
222 by (fast_tac (claset() addIs [conf_hext,sup_heap_newref]) 1);
223 qed_spec_mp "oconf_imp_oconf_heap_newref";
225 Goalw [oconf_def,lconf_def]
226 "hp a = Some obj' \\<longrightarrow> obj_ty obj' = obj_ty obj'' \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \
227 \ \\<longrightarrow> G,hp(a\\<mapsto>obj'')\\<turnstile>obj\\<surd>";
228 by (Asm_full_simp_tac 1);
229 by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1);
230 qed_spec_mp "oconf_imp_oconf_heap_update";
236 Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
237 by (asm_full_simp_tac (simpset() addsplits [split_split]
238 addsimps [hconf_def]) 1);
239 by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
240 qed_spec_mp "hconf_imp_hconf_newref";
243 Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
244 \ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>";
245 by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
246 by (fast_tac (claset() addIs
247 [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
248 addss (simpset() addsimps [obj_ty_def])) 1);
249 qed_spec_mp "hconf_imp_hconf_field_update";
252 (** correct_frames **)
254 Delsimps [fun_upd_apply];
256 "\\<forall>rT C ml. correct_frames G hp phi rT C ml frs \\<longrightarrow> \
257 \ hp a = Some (cn,od) \\<longrightarrow> map_of (fields (G, cn)) fl = Some fd \\<longrightarrow> \
258 \ G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
259 \ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT C ml frs";
260 by (induct_tac "frs" 1);
261 by (Asm_full_simp_tac 1);
262 by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
263 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
264 approx_loc_imp_approx_loc_sup_heap,
265 sup_heap_update_value] addss (simpset())) 1);
266 qed_spec_mp "correct_frames_imp_correct_frames_field_update";
270 "\\<forall>rT C ml. hp x = None \\<longrightarrow> correct_frames G hp phi rT C ml frs \\<and> \
272 \ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT C ml frs";
273 by (induct_tac "frs" 1);
274 by (asm_full_simp_tac (simpset() addsimps []) 1);
275 by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
276 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
277 approx_loc_imp_approx_loc_sup_heap,
278 hconf_imp_hconf_newref,
279 sup_heap_newref] addss (simpset())) 1);
280 qed_spec_mp "correct_frames_imp_correct_frames_newref";