8011
|
1 |
(* Title: HOL/MicroJava/BV/Correct.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Cornelia Pusch
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
(** sup_heap **)
|
|
8 |
|
|
9 |
Goalw [hext_def]
|
|
10 |
"hp x = None \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> obj))";
|
|
11 |
by (asm_full_simp_tac (simpset() addsimps []) 1);
|
|
12 |
by (Clarify_tac 1);
|
|
13 |
bd newref_None 1;
|
|
14 |
back();
|
|
15 |
by (asm_full_simp_tac (simpset() addsimps []) 1);
|
|
16 |
qed_spec_mp "sup_heap_newref";
|
|
17 |
|
|
18 |
|
|
19 |
Goalw [hext_def]
|
|
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";
|
|
23 |
|
|
24 |
|
|
25 |
(** approx_val **)
|
|
26 |
|
|
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";
|
|
31 |
|
|
32 |
|
|
33 |
Goalw [approx_val_def]
|
|
34 |
"approx_val G hp Null (Some(RefT x))";
|
|
35 |
by(Simp_tac 1);
|
|
36 |
by (fast_tac (claset() addIs widen.intrs) 1);
|
|
37 |
qed_spec_mp "approx_val_Null";
|
|
38 |
|
|
39 |
|
|
40 |
Goal
|
|
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);
|
|
44 |
by (Asm_simp_tac 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";
|
|
47 |
|
|
48 |
|
|
49 |
Goal
|
|
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";
|
|
55 |
|
|
56 |
Goal
|
|
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";
|
|
62 |
|
|
63 |
|
|
64 |
Goal
|
8023
|
65 |
"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
|
8011
|
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";
|
|
69 |
|
|
70 |
|
|
71 |
Goal
|
8023
|
72 |
"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
|
8011
|
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";
|
|
77 |
|
|
78 |
|
|
79 |
(** approx_loc **)
|
|
80 |
|
|
81 |
Goal
|
|
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";
|
|
86 |
|
|
87 |
|
|
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";
|
|
95 |
|
|
96 |
|
|
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);
|
|
100 |
by (Asm_simp_tac 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";
|
|
104 |
|
|
105 |
|
|
106 |
Goalw [sup_loc_def,approx_loc_def]
|
8023
|
107 |
"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
|
8011
|
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";
|
|
111 |
|
|
112 |
|
|
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";
|
|
119 |
|
|
120 |
|
|
121 |
Goal
|
|
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);
|
|
126 |
br allI 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);
|
|
130 |
by (Clarify_tac 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";
|
|
136 |
|
|
137 |
|
|
138 |
(** approx_stk **)
|
|
139 |
|
|
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";
|
|
144 |
|
|
145 |
Goal
|
|
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";
|
|
149 |
|
|
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";
|
|
154 |
|
|
155 |
|
|
156 |
Goalw [approx_stk_def]
|
8023
|
157 |
"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st) <=l (map Some st') \\<longrightarrow> approx_stk G hp lvars st'";
|
8011
|
158 |
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
|
|
159 |
qed_spec_mp "approx_stk_imp_approx_stk_sup";
|
|
160 |
|
|
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";
|
|
165 |
|
|
166 |
|
|
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";
|
|
171 |
|
|
172 |
Goal
|
|
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";
|
|
179 |
|
|
180 |
Goal
|
|
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);
|
|
186 |
by (Clarify_tac 1);
|
|
187 |
by (asm_full_simp_tac (simpset() addsimps []) 1);
|
|
188 |
bd approx_stk_Cons_lemma 1;
|
|
189 |
by (Clarify_tac 1);
|
|
190 |
by (eres_inst_tac [("x","ST'")] allE 1);
|
|
191 |
by (eres_inst_tac [("x","stk'")] allE 1);
|
|
192 |
by (Clarify_tac 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";
|
|
197 |
|
|
198 |
|
|
199 |
(** oconf **)
|
|
200 |
|
|
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";
|
|
208 |
|
|
209 |
|
|
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";
|
|
216 |
|
|
217 |
|
|
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";
|
|
224 |
|
|
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";
|
|
231 |
|
|
232 |
|
|
233 |
(** hconf **)
|
|
234 |
|
|
235 |
|
8032
|
236 |
Goal "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>";
|
8011
|
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";
|
|
241 |
|
|
242 |
|
|
243 |
Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
|
8032
|
244 |
\ 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>";
|
8011
|
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";
|
|
250 |
|
|
251 |
|
|
252 |
(** correct_frames **)
|
|
253 |
|
|
254 |
Delsimps [fun_upd_apply];
|
|
255 |
Goal
|
|
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";
|
|
267 |
|
|
268 |
|
|
269 |
Goal
|
|
270 |
"\\<forall>rT C ml. hp x = None \\<longrightarrow> correct_frames G hp phi rT C ml frs \\<and> \
|
|
271 |
\ oconf G hp obj \
|
|
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";
|
|
281 |
|