8011
|
1 |
(* Title: HOL/MicroJava/J/Conform.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
section "hext";
|
|
8 |
|
|
9 |
val hextI = prove_goalw thy [hext_def] "\\<And>h. \
|
|
10 |
\ \\<forall>a C fs . h a = Some (C,fs) \\<longrightarrow> \
|
|
11 |
\ (\\<exists>fs'. h' a = Some (C,fs')) \\<Longrightarrow> h\\<le>|h'" (K [Auto_tac ]);
|
|
12 |
|
|
13 |
val hext_objD = prove_goalw thy [hext_def]
|
|
14 |
"\\<And>h. \\<lbrakk>h\\<le>|h'; h a = Some (C,fs) \\<rbrakk> \\<Longrightarrow> \\<exists>fs'. h' a = Some (C,fs')"
|
|
15 |
(K [Force_tac 1]);
|
|
16 |
|
|
17 |
val hext_refl = prove_goal thy "h\\<le>|h" (K [
|
|
18 |
rtac hextI 1,
|
|
19 |
Fast_tac 1]);
|
|
20 |
|
|
21 |
val hext_new = prove_goal thy "\\<And>h. h a = None \\<Longrightarrow> h\\<le>|h(a\\<mapsto>x)" (K [
|
|
22 |
rtac hextI 1,
|
|
23 |
safe_tac HOL_cs,
|
|
24 |
ALLGOALS (case_tac "aa = a"),
|
|
25 |
Auto_tac]);
|
|
26 |
|
|
27 |
val hext_trans = prove_goal thy "\\<And>h. \\<lbrakk>h\\<le>|h'; h'\\<le>|h''\\<rbrakk> \\<Longrightarrow> h\\<le>|h''" (K [
|
|
28 |
rtac hextI 1,
|
|
29 |
safe_tac HOL_cs,
|
|
30 |
fast_tac (HOL_cs addDs [hext_objD]) 1]);
|
|
31 |
|
|
32 |
Addsimps [hext_refl, hext_new];
|
|
33 |
|
|
34 |
val hext_upd_obj = prove_goal thy
|
|
35 |
"\\<And>h. h a = Some (C,fs) \\<Longrightarrow> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
|
|
36 |
rtac hextI 1,
|
|
37 |
safe_tac HOL_cs,
|
|
38 |
ALLGOALS (case_tac "aa = a"),
|
|
39 |
Auto_tac]);
|
|
40 |
|
|
41 |
|
|
42 |
section "conf";
|
|
43 |
|
|
44 |
val conf_Null = prove_goalw thy [conf_def]
|
|
45 |
"G,h\\<turnstile>Null\\<Colon>\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
|
|
46 |
Addsimps [conf_Null];
|
|
47 |
|
|
48 |
val conf_litval = prove_goalw thy [conf_def]
|
|
49 |
"typeof (\\<lambda>v. None) v = Some T \\<longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" (K [
|
|
50 |
rtac val_.induct 1,
|
|
51 |
Auto_tac]) RS mp;
|
|
52 |
|
|
53 |
val conf_AddrI = prove_goalw thy [conf_def]
|
|
54 |
"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
|
|
55 |
(K [Asm_full_simp_tac 1]);
|
|
56 |
|
|
57 |
val conf_obj_AddrI = prove_goalw thy [conf_def]
|
|
58 |
"\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>Class C\\<preceq>Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>Class D"
|
|
59 |
(K [Asm_full_simp_tac 1]);
|
|
60 |
|
|
61 |
Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
|
|
62 |
by (Simp_tac 1);
|
|
63 |
by (res_inst_tac [("y","T")] ty.exhaust 1);
|
|
64 |
by (etac ssubst 1);
|
|
65 |
by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
|
|
66 |
by (auto_tac (claset(), simpset() addsimps [widen.null]));
|
|
67 |
qed_spec_mp "defval_conf";
|
|
68 |
|
|
69 |
val conf_upd_obj = prove_goalw thy [conf_def]
|
|
70 |
"h a = Some (C,fs) \\<longrightarrow> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x\\<Colon>\\<preceq>T) = (G,h\\<turnstile>x\\<Colon>\\<preceq>T)" (fn _ => [
|
|
71 |
rtac impI 1,
|
|
72 |
rtac val_.induct 1,
|
|
73 |
ALLGOALS Simp_tac,
|
|
74 |
case_tac "loc = a" 1,
|
|
75 |
ALLGOALS Asm_simp_tac]) RS mp;
|
|
76 |
|
|
77 |
val conf_widen = prove_goalw thy [conf_def]
|
8082
|
78 |
"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
|
8011
|
79 |
rtac val_.induct 1,
|
|
80 |
ALLGOALS Simp_tac,
|
|
81 |
ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
|
|
82 |
|
|
83 |
val conf_hext' = prove_goalw thy [conf_def]
|
|
84 |
"\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
|
|
85 |
REPEAT (rtac allI 1),
|
|
86 |
rtac val_.induct 1,
|
|
87 |
ALLGOALS Simp_tac,
|
|
88 |
safe_tac (HOL_cs addSDs [option_map_SomeD]),
|
|
89 |
rewtac option_map_def,
|
|
90 |
dtac hext_objD 1,
|
|
91 |
Auto_tac]);
|
|
92 |
val conf_hext = conf_hext' RS spec RS spec RS mp;
|
|
93 |
|
|
94 |
val new_locD = prove_goalw thy [conf_def]
|
|
95 |
"\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
|
|
96 |
cut_facts_tac prems 1,
|
|
97 |
Full_simp_tac 1,
|
|
98 |
safe_tac HOL_cs,
|
|
99 |
Asm_full_simp_tac 1]);
|
|
100 |
|
|
101 |
val conf_RefTD = prove_goalw thy [conf_def] "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null | \
|
|
102 |
\ (\\<exists>a obj T'. a' = Addr a \\<and> h a = Some obj \\<and> obj_ty obj = T' \\<and> G\\<turnstile>T'\\<preceq>RefT T)" (K [
|
|
103 |
induct_tac "a'" 1,
|
|
104 |
Auto_tac,
|
|
105 |
REPEAT (etac widen_PrimT_RefT 1)]) RS mp;
|
|
106 |
|
|
107 |
val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
|
|
108 |
dtac conf_RefTD 1,
|
|
109 |
Step_tac 1,
|
|
110 |
Auto_tac,
|
|
111 |
etac widen_Class_NullT 1]);
|
|
112 |
|
|
113 |
val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
|
|
114 |
\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t" (K [
|
|
115 |
dtac conf_RefTD 1,
|
|
116 |
Step_tac 1,
|
|
117 |
Auto_tac]);
|
|
118 |
|
|
119 |
val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
|
|
120 |
\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>Class C'\\<preceq>Class C)"
|
|
121 |
(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
|
|
122 |
|
8082
|
123 |
Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
|
8011
|
124 |
\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
|
|
125 |
\ (\\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t)";
|
|
126 |
by (rtac impI 1);
|
|
127 |
by (rtac impI 1);
|
|
128 |
by (res_inst_tac [("y","t")] ref_ty.exhaust 1);
|
|
129 |
by (safe_tac HOL_cs);
|
|
130 |
by (dtac conf_NullTD 1);
|
|
131 |
by (contr_tac 1);
|
|
132 |
by (etac non_np_objD 1);
|
|
133 |
by (atac 1);
|
|
134 |
by (Fast_tac 1);
|
|
135 |
qed_spec_mp "non_np_objD'";
|
|
136 |
|
8082
|
137 |
Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow> list_all2 (conf G h) vs Ts'";
|
8011
|
138 |
by( induct_tac "vs" 1);
|
|
139 |
by( ALLGOALS Clarsimp_tac);
|
|
140 |
by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
|
|
141 |
by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
|
|
142 |
by( Safe_tac);
|
|
143 |
by( rotate_tac ~1 1);
|
|
144 |
by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
|
|
145 |
by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
|
|
146 |
by( ALLGOALS Clarify_tac);
|
|
147 |
by( fast_tac (claset() addEs [conf_widen]) 1);
|
|
148 |
qed_spec_mp "conf_list_gext_widen";
|
|
149 |
|
|
150 |
|
|
151 |
section "lconf";
|
|
152 |
|
|
153 |
val lconfD = prove_goalw thy [lconf_def]
|
|
154 |
"\\<And>X. \\<lbrakk> G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts; Ts n = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>(the (vs n))\\<Colon>\\<preceq>T"
|
|
155 |
(K [Force_tac 1]);
|
|
156 |
|
|
157 |
val lconf_hext = prove_goalw thy [lconf_def]
|
|
158 |
"\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]L; h\\<le>|h' \\<rbrakk> \\<Longrightarrow> G,h'\\<turnstile>l[\\<Colon>\\<preceq>]L" (K [
|
|
159 |
fast_tac (claset() addEs [conf_hext]) 1]);
|
|
160 |
AddEs [lconf_hext];
|
|
161 |
|
|
162 |
Goalw [lconf_def] "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT; \
|
|
163 |
\ G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>l(va\\<mapsto>v)[\\<Colon>\\<preceq>]lT";
|
|
164 |
by( Clarify_tac 1);
|
|
165 |
by( case_tac "n = va" 1);
|
|
166 |
by Auto_tac;
|
|
167 |
qed "lconf_upd";
|
|
168 |
|
|
169 |
Goal "\\<forall>x. P x \\<longrightarrow> R (dv x) x \\<Longrightarrow> (\\<forall>x. map_of fs f = Some x \\<longrightarrow> P x) \\<longrightarrow> \
|
|
170 |
\ (\\<forall>T. map_of fs f = Some T \\<longrightarrow> \
|
|
171 |
\ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and> R v T))";
|
|
172 |
by( induct_tac "fs" 1);
|
|
173 |
by Auto_tac;
|
|
174 |
qed_spec_mp "lconf_init_vars_lemma";
|
|
175 |
|
|
176 |
Goalw [lconf_def, init_vars_def]
|
|
177 |
"\\<forall>n. \\<forall>T. map_of fs n = Some T \\<longrightarrow> is_type G T \\<Longrightarrow> G,h\\<turnstile>init_vars fs[\\<Colon>\\<preceq>]map_of fs";
|
|
178 |
by Auto_tac;
|
|
179 |
by( rtac lconf_init_vars_lemma 1);
|
|
180 |
by( atac 3);
|
|
181 |
by( strip_tac 1);
|
|
182 |
by( etac defval_conf 1);
|
|
183 |
by Auto_tac;
|
|
184 |
qed "lconf_init_vars";
|
|
185 |
AddSIs [lconf_init_vars];
|
|
186 |
|
|
187 |
val lconf_ext = prove_goalw thy [lconf_def]
|
|
188 |
"\\<And>X. \\<lbrakk>G,s\\<turnstile>l[\\<Colon>\\<preceq>]L; G,s\\<turnstile>v\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,s\\<turnstile>l(vn\\<mapsto>v)[\\<Colon>\\<preceq>]L(vn\\<mapsto>T)"
|
|
189 |
(K [Auto_tac]);
|
|
190 |
|
|
191 |
Goalw [lconf_def] "G,h\\<turnstile>l[\\<Colon>\\<preceq>]L \\<Longrightarrow> \\<forall>vs Ts. nodups vns \\<longrightarrow> length Ts = length vns \\<longrightarrow> list_all2 (\\<lambda>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts \\<longrightarrow> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[\\<Colon>\\<preceq>]L(vns[\\<mapsto>]Ts)";
|
|
192 |
by( induct_tac "vns" 1);
|
|
193 |
by( ALLGOALS Clarsimp_tac);
|
|
194 |
by( forward_tac [list_all2_lengthD] 1);
|
|
195 |
by( auto_tac (claset(), simpset() addsimps [length_Suc_conv]));
|
|
196 |
qed_spec_mp "lconf_ext_list";
|
|
197 |
|
|
198 |
|
|
199 |
section "oconf";
|
|
200 |
|
|
201 |
val oconf_hext = prove_goalw thy [oconf_def]
|
|
202 |
"\\<And>X. G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> h\\<le>|h' \\<Longrightarrow> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
|
|
203 |
|
|
204 |
val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
|
|
205 |
\ (\\<forall>T f. map_of(fields (G,C)) f = Some T \\<longrightarrow> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T))"(K [
|
|
206 |
Auto_tac]);
|
|
207 |
|
|
208 |
val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
|
|
209 |
|
|
210 |
|
|
211 |
section "hconf";
|
|
212 |
|
8032
|
213 |
Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
|
8011
|
214 |
by (Fast_tac 1);
|
|
215 |
qed "hconfD";
|
|
216 |
|
8032
|
217 |
Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
|
8011
|
218 |
by (Fast_tac 1);
|
|
219 |
qed "hconfI";
|
|
220 |
|
|
221 |
|
|
222 |
section "conforms";
|
|
223 |
|
|
224 |
val conforms_heapD = prove_goalw thy [conforms_def]
|
8032
|
225 |
"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
|
8011
|
226 |
(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
|
|
227 |
|
|
228 |
val conforms_localD = prove_goalw thy [conforms_def]
|
|
229 |
"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT" (fn prems => [
|
|
230 |
cut_facts_tac prems 1, Asm_full_simp_tac 1]);
|
|
231 |
|
|
232 |
val conformsI = prove_goalw thy [conforms_def]
|
8032
|
233 |
"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
|
8011
|
234 |
cut_facts_tac prems 1,
|
|
235 |
Simp_tac 1,
|
|
236 |
Auto_tac]);
|
|
237 |
|
8032
|
238 |
Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
|
8011
|
239 |
by( fast_tac (HOL_cs addDs [conforms_localD]
|
|
240 |
addSEs [conformsI, lconf_hext]) 1);
|
|
241 |
qed "conforms_hext";
|
|
242 |
|
|
243 |
Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)\\<rbrakk> \\<Longrightarrow> (h(a\\<mapsto>obj),l)\\<Colon>\\<preceq>(G, lT)";
|
|
244 |
by( rtac conforms_hext 1);
|
|
245 |
by Auto_tac;
|
|
246 |
by( rtac hconfI 1);
|
|
247 |
by( dtac conforms_heapD 1);
|
|
248 |
by( (auto_tac (HOL_cs addEs [oconf_hext] addDs [hconfD],
|
|
249 |
simpset()delsimps[split_paired_All])));
|
|
250 |
qed "conforms_upd_obj";
|
|
251 |
|
|
252 |
Goalw [conforms_def]
|
|
253 |
"\\<lbrakk>(h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T\\<rbrakk> \\<Longrightarrow> \
|
|
254 |
\ (h, l(va\\<mapsto>v))\\<Colon>\\<preceq>(G, lT)";
|
|
255 |
by( auto_tac (claset() addEs [lconf_upd], simpset()));
|
|
256 |
qed "conforms_upd_local";
|