8011
|
1 |
(* Title: HOL/MicroJava/J/WellForm.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
|
|
8 |
"\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm G (C,c)" (K [
|
|
9 |
Asm_full_simp_tac 1,
|
|
10 |
fast_tac (set_cs addDs [get_in_set]) 1]);
|
|
11 |
|
|
12 |
val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
|
|
13 |
"\\<And>X. wf_prog wtm G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
|
|
14 |
safe_tac set_cs,
|
|
15 |
dtac in_set_get 1,
|
|
16 |
Auto_tac]);
|
|
17 |
Addsimps [class_Object];
|
|
18 |
|
|
19 |
val is_class_Object = prove_goalw thy [is_class_def]
|
|
20 |
"\\<And>X. wf_prog wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
|
|
21 |
Addsimps [is_class_Object];
|
|
22 |
|
|
23 |
Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not> G\\<turnstile>D\\<prec>C C";
|
|
24 |
by( forward_tac [r_into_trancl] 1);
|
|
25 |
by( dtac subcls1D 1);
|
|
26 |
by( strip_tac1 1);
|
|
27 |
by( dtac class_wf 1);
|
|
28 |
by( atac 1);
|
|
29 |
by( rewtac wf_cdecl_def);
|
|
30 |
by( Clarsimp_tac 1);
|
|
31 |
qed "subcls1_wfD";
|
|
32 |
|
|
33 |
val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
|
|
34 |
"\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
|
|
35 |
pair_tac "r" 1,
|
|
36 |
Asm_full_simp_tac 1,
|
|
37 |
strip_tac1 1,
|
|
38 |
option_case_tac 1,
|
|
39 |
Fast_tac 1]);
|
|
40 |
|
|
41 |
local
|
|
42 |
val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [
|
|
43 |
etac trancl_trans_induct 1,
|
|
44 |
atac 2,
|
|
45 |
rewtac subcls1_def,
|
|
46 |
Auto_tac]);
|
|
47 |
in
|
|
48 |
val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [
|
|
49 |
etac (lemma RS mp) 1,
|
|
50 |
Auto_tac]);
|
|
51 |
end;
|
|
52 |
|
|
53 |
Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not> G\\<turnstile>D\\<prec>C C";
|
|
54 |
by(etac tranclE 1);
|
|
55 |
by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
|
|
56 |
qed "subcls_asym";
|
|
57 |
|
|
58 |
val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
|
|
59 |
etac trancl_trans_induct 1,
|
|
60 |
fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
|
|
61 |
fast_tac (HOL_cs addDs [subcls_asym]) 1]);
|
|
62 |
|
|
63 |
val acyclic_subcls1 = prove_goalw thy [acyclic_def]
|
|
64 |
"\\<And>X. wf_prog wt G \\<Longrightarrow> acyclic (subcls1 G)" (K [
|
|
65 |
strip_tac1 1,
|
|
66 |
fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
|
|
67 |
|
|
68 |
val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
|
|
69 |
rtac finite_acyclic_wf 1,
|
|
70 |
stac finite_converse 1,
|
|
71 |
rtac finite_subcls1 1,
|
|
72 |
stac acyclic_converse 1,
|
|
73 |
etac acyclic_subcls1 1]);
|
|
74 |
|
|
75 |
|
|
76 |
val major::prems = goal thy
|
|
77 |
"\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
|
|
78 |
by(cut_facts_tac [major RS wf_subcls1] 1);
|
|
79 |
by(dtac wf_trancl 1);
|
|
80 |
by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
|
|
81 |
by(eres_inst_tac [("a","C")] wf_induct 1);
|
|
82 |
by(resolve_tac prems 1);
|
|
83 |
by(Auto_tac);
|
|
84 |
qed "subcls_induct";
|
|
85 |
|
|
86 |
val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm G; P Object; \
|
|
87 |
\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
|
|
88 |
\ wf_cdecl wtm G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
|
|
89 |
\ \\<rbrakk> \\<Longrightarrow> P C";
|
|
90 |
by( cut_facts_tac prems 1);
|
|
91 |
by( rtac impE 1);
|
|
92 |
by( atac 2);
|
|
93 |
by( atac 2);
|
|
94 |
by( etac thin_rl 1);
|
|
95 |
by( rtac subcls_induct 1);
|
|
96 |
by( atac 1);
|
|
97 |
by( rtac impI 1);
|
|
98 |
by( case_tac "C = Object" 1);
|
|
99 |
by( Fast_tac 1);
|
|
100 |
by( ex_ftac is_classD 1);
|
|
101 |
by( forward_tac [class_wf] 1);
|
|
102 |
by( atac 1);
|
|
103 |
by( forward_tac [wf_cdecl_supD] 1);
|
|
104 |
by( atac 1);
|
|
105 |
by( strip_tac1 1);
|
|
106 |
by( rtac (hd (tl (tl (tl prems)))) 1);
|
|
107 |
by( atac 1);
|
|
108 |
by( atac 1);
|
|
109 |
by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
|
|
110 |
by( fast_tac (HOL_cs addIs [r_into_trancl]) 1);
|
|
111 |
by( etac subcls1I 1);
|
|
112 |
qed "subcls1_induct";
|
|
113 |
|
|
114 |
Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) = \
|
|
115 |
\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
|
|
116 |
\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> cmethd (G,D)) \\<oplus> \
|
|
117 |
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
|
|
118 |
by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1);
|
|
119 |
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
|
|
120 |
addsplits [option.split]) 1);
|
|
121 |
by( case_tac "C = Object" 1);
|
|
122 |
by( Asm_full_simp_tac 1);
|
|
123 |
by( dtac class_wf 1);
|
|
124 |
by( atac 1);
|
|
125 |
by( dtac wf_cdecl_supD 1);
|
|
126 |
by( atac 1);
|
|
127 |
by( Asm_full_simp_tac 1);
|
|
128 |
val cmethd_rec = result();
|
|
129 |
|
|
130 |
Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
|
|
131 |
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
|
|
132 |
\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
|
|
133 |
by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
|
|
134 |
by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
|
|
135 |
by( option_case_tac2 "sc" 1);
|
|
136 |
by( Asm_simp_tac 1);
|
|
137 |
by( case_tac "C = Object" 1);
|
|
138 |
by( rotate_tac 2 1);
|
|
139 |
by( Asm_full_simp_tac 1);
|
|
140 |
by( dtac class_wf 1);
|
|
141 |
by( atac 1);
|
|
142 |
by( dtac wf_cdecl_supD 1);
|
|
143 |
by( atac 1);
|
|
144 |
by( Asm_full_simp_tac 1);
|
|
145 |
val fields_rec = result();
|
|
146 |
|
|
147 |
val cmethd_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> cmethd (G,Object) = empty"
|
|
148 |
(K [stac cmethd_rec 1,Auto_tac]);
|
|
149 |
val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
|
|
150 |
stac fields_rec 1,Auto_tac]);
|
|
151 |
Addsimps [cmethd_Object, fields_Object];
|
|
152 |
val cfield_Object = prove_goalw thy [cfield_def]
|
|
153 |
"\\<And>X. wf_prog wtm G \\<Longrightarrow> cfield (G,Object) = empty" (K [Asm_simp_tac 1]);
|
|
154 |
Addsimps [cfield_Object];
|
|
155 |
|
|
156 |
val subcls_C_Object = prove_goal thy
|
|
157 |
"\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
|
|
158 |
etac subcls1_induct 1,
|
|
159 |
atac 1,
|
|
160 |
Fast_tac 1,
|
|
161 |
safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
|
|
162 |
fast_tac (HOL_cs addIs [r_into_trancl]) 1,
|
|
163 |
rtac trancl_trans 1,
|
|
164 |
atac 2,
|
|
165 |
rtac r_into_trancl 1,
|
|
166 |
rtac subcls1I 1,
|
|
167 |
ALLGOALS Asm_simp_tac]) RS mp;
|
|
168 |
|
|
169 |
val is_type_rTI = prove_goalw thy [wf_mhead_def]
|
|
170 |
"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
|
|
171 |
(K [split_all_tac 1, Auto_tac]);
|
|
172 |
|
|
173 |
val widen_Class_Object = prove_goal thy
|
|
174 |
"\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [
|
|
175 |
cut_facts_tac prems 1,
|
|
176 |
case_tac "C=Object" 1,
|
|
177 |
hyp_subst_tac 1,
|
|
178 |
Asm_simp_tac 1,
|
|
179 |
rtac widen.subcls 1,
|
|
180 |
fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
|
|
181 |
|
|
182 |
val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"
|
|
183 |
(fn prems=> [cut_facts_tac prems 1,
|
|
184 |
fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
|
|
185 |
subcls_Object]) 1]);
|
|
186 |
|
|
187 |
val fields_mono = prove_goal thy
|
|
188 |
"\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
|
|
189 |
\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [
|
|
190 |
etac trancl_trans_induct 1,
|
|
191 |
safe_tac (HOL_cs addSDs [subcls1D]),
|
|
192 |
stac fields_rec 1,
|
|
193 |
Auto_tac]) RS mp;
|
|
194 |
|
|
195 |
Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
|
|
196 |
\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
|
|
197 |
by( etac subcls1_induct 1);
|
|
198 |
by( atac 1);
|
|
199 |
by( Asm_simp_tac 1);
|
|
200 |
by( safe_tac HOL_cs);
|
|
201 |
by( stac fields_rec 1);
|
|
202 |
by( atac 1);
|
|
203 |
by( atac 1);
|
|
204 |
by( Simp_tac 1);
|
|
205 |
by( rtac ballI 1);
|
|
206 |
by( split_all_tac 1);
|
|
207 |
by( Simp_tac 1);
|
|
208 |
by( etac UnE 1);
|
|
209 |
by( dtac split_Pair_eq 1);
|
|
210 |
by( SELECT_GOAL (Auto_tac) 1);
|
|
211 |
by( rtac widen_trans 1);
|
|
212 |
by( atac 1);
|
|
213 |
by( etac (r_into_trancl RS widen.subcls) 1);
|
|
214 |
by( etac BallE 1);
|
|
215 |
by( contr_tac 1);
|
|
216 |
by( Asm_full_simp_tac 1);
|
|
217 |
val widen_fields_defpl' = result();
|
|
218 |
|
|
219 |
Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
|
|
220 |
\ G\\<turnstile>Class C\\<preceq>Class fd";
|
|
221 |
by( dtac widen_fields_defpl' 1);
|
|
222 |
by( atac 1);
|
|
223 |
(*###################*)
|
|
224 |
by( dtac bspec 1);
|
|
225 |
auto();
|
|
226 |
val widen_fields_defpl = result();
|
|
227 |
|
|
228 |
|
|
229 |
Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
|
|
230 |
by( etac subcls1_induct 1);
|
|
231 |
by( atac 1);
|
|
232 |
by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
|
|
233 |
by( Asm_simp_tac 1);
|
|
234 |
by( dtac subcls1_wfD 1);
|
|
235 |
by( atac 1);
|
|
236 |
by( stac fields_rec 1);
|
|
237 |
by Auto_tac;
|
|
238 |
by( rotate_tac ~1 1);
|
|
239 |
by( ex_ftac is_classD 1);
|
|
240 |
by( forward_tac [class_wf] 1);
|
|
241 |
by Auto_tac;
|
|
242 |
by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
|
|
243 |
by( etac unique_append 1);
|
|
244 |
by( rtac unique_map_Pair 1);
|
|
245 |
by( Step_tac 1);
|
|
246 |
by (EVERY1[dtac widen_fields_defpl, atac, atac]);
|
|
247 |
by( Asm_full_simp_tac 1);
|
|
248 |
by( dtac split_Pair_eq 1);
|
|
249 |
by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
|
|
250 |
val unique_fields = result();
|
|
251 |
|
|
252 |
Goal
|
|
253 |
"\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
|
|
254 |
\ map_of (fields (G,C')) f = Some ft";
|
|
255 |
by( dtac widen_Class_Class 1);
|
|
256 |
by( etac disjE 1);
|
|
257 |
by( Asm_simp_tac 1);
|
|
258 |
by( rtac table_mono 1);
|
|
259 |
by( atac 3);
|
|
260 |
by( rtac unique_fields 1);
|
|
261 |
by( etac subcls_is_class 1);
|
|
262 |
by( atac 1);
|
|
263 |
by( fast_tac (HOL_cs addEs [fields_mono]) 1);
|
|
264 |
val widen_fields_mono = result();
|
|
265 |
|
|
266 |
|
|
267 |
val cfs_fields_lemma = prove_goalw thy [cfield_def]
|
|
268 |
"\\<And>X. cfield (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
|
|
269 |
(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
|
|
270 |
|
|
271 |
val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>cfield (G,C) fn = Some (fd, fT);\
|
|
272 |
\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
|
|
273 |
fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
|
|
274 |
|
|
275 |
Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) sig = Some (md,mh,m)\
|
|
276 |
\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
|
|
277 |
by( case_tac "is_class G C" 1);
|
|
278 |
by( forw_inst_tac [("C","C")] cmethd_rec 2);
|
|
279 |
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
|
|
280 |
delsimps [not_None_eq]) 2);
|
|
281 |
by( etac subcls1_induct 1);
|
|
282 |
by( atac 1);
|
|
283 |
by( Force_tac 1);
|
|
284 |
by( forw_inst_tac [("C","C")] cmethd_rec 1);
|
|
285 |
by( strip_tac1 1);
|
|
286 |
by( rotate_tac ~1 1);
|
|
287 |
by( Asm_full_simp_tac 1);
|
|
288 |
by( dtac override_SomeD 1);
|
|
289 |
by( etac disjE 1);
|
|
290 |
by( thin_tac "?P \\<longrightarrow> ?Q" 1);
|
|
291 |
by( Clarify_tac 2);
|
|
292 |
by( rtac widen_trans 2);
|
|
293 |
by( atac 2);
|
|
294 |
by( atac 3);
|
|
295 |
by( rtac widen.subcls 2);
|
|
296 |
by( rtac r_into_trancl 2);
|
|
297 |
by( fast_tac (HOL_cs addIs [subcls1I]) 2);
|
|
298 |
by( forward_tac [table_mapf_SomeD] 1);
|
|
299 |
by( strip_tac1 1);
|
|
300 |
by( Asm_full_simp_tac 1);
|
|
301 |
by( rewtac wf_cdecl_def);
|
|
302 |
by( Asm_full_simp_tac 1);
|
|
303 |
val cmethd_wf_mdecl = result() RS mp;
|
|
304 |
|
|
305 |
Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
|
|
306 |
\ \\<forall>D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
|
|
307 |
\ (\\<exists>D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
|
|
308 |
by( etac trancl_trans_induct 1);
|
|
309 |
by( strip_tac1 2);
|
|
310 |
by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
|
|
311 |
by( fast_tac (HOL_cs addEs [widen_trans]) 2);
|
|
312 |
by( strip_tac1 1);
|
|
313 |
by( dtac subcls1D 1);
|
|
314 |
by( strip_tac1 1);
|
|
315 |
by( stac cmethd_rec 1);
|
|
316 |
by( atac 1);
|
|
317 |
by( rewtac override_def);
|
|
318 |
by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
|
|
319 |
by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
|
|
320 |
by( etac exE 1);
|
|
321 |
by( asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
|
|
322 |
by( ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
|
|
323 |
by( ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
|
|
324 |
by( dtac class_wf 1);
|
|
325 |
by( atac 1);
|
|
326 |
by( split_all_tac 1);
|
|
327 |
by( rewtac wf_cdecl_def);
|
|
328 |
by( dtac table_mapf_Some2 1);
|
|
329 |
by( Clarsimp_tac 1);
|
|
330 |
by( dres_inst_tac [("xys1","ms")] get_in_set 1);
|
|
331 |
by Auto_tac;
|
|
332 |
qed_spec_mp "subcls_widen_methd";
|
|
333 |
|
|
334 |
|
|
335 |
Goal
|
|
336 |
"\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
|
|
337 |
\ cmethd (G,D) sig = Some (md, rT, b) \\<rbrakk> \
|
|
338 |
\ \\<Longrightarrow> \\<exists>mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
|
|
339 |
by(auto_tac (claset() addSDs [widen_Class_Class]
|
|
340 |
addDs [subcls_widen_methd,cmethd_wf_mdecl],
|
|
341 |
simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
|
|
342 |
qed "subtype_widen_methd";
|
|
343 |
|
|
344 |
|
|
345 |
Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. cmethd (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> cmethd (G,D) sig = Some(D,mh,code)";
|
|
346 |
by( case_tac "is_class G C" 1);
|
|
347 |
by( forw_inst_tac [("C","C")] cmethd_rec 2);
|
|
348 |
by( asm_full_simp_tac (simpset() addsimps [is_class_def]
|
|
349 |
delsimps [not_None_eq]) 2);
|
|
350 |
by (etac subcls1_induct 1);
|
|
351 |
ba 1;
|
|
352 |
by (Asm_full_simp_tac 1);
|
|
353 |
by (stac cmethd_rec 1);
|
|
354 |
ba 1;
|
|
355 |
by (Clarify_tac 1);
|
|
356 |
by (eres_inst_tac [("x","Da")] allE 1);
|
|
357 |
by (Clarsimp_tac 1);
|
|
358 |
by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
|
|
359 |
by (Clarify_tac 1);
|
|
360 |
by (stac cmethd_rec 1);
|
|
361 |
ba 1;
|
|
362 |
by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
|
|
363 |
qed_spec_mp "cmethd_in_md";
|
|
364 |
|
|
365 |
writeln"OK";
|
|
366 |
|
|
367 |
Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
|
|
368 |
\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
|
|
369 |
by( etac subcls1_induct 1);
|
|
370 |
by( atac 1);
|
|
371 |
by( Asm_simp_tac 1);
|
|
372 |
by( strip_tac1 1);
|
|
373 |
by( stac fields_rec 1);
|
|
374 |
by( atac 1);
|
|
375 |
by( atac 1);
|
|
376 |
by( Asm_simp_tac 1);
|
|
377 |
by( safe_tac set_cs);
|
|
378 |
by( Fast_tac 2);
|
|
379 |
by( dtac class_wf 1);
|
|
380 |
by( atac 1);
|
|
381 |
by( rewtac wf_cdecl_def);
|
|
382 |
by( Asm_full_simp_tac 1);
|
|
383 |
by( strip_tac1 1);
|
|
384 |
by( EVERY[dtac bspec 1, atac 1]);
|
|
385 |
by( rewtac wf_fdecl_def);
|
|
386 |
by( split_all_tac 1);
|
|
387 |
by( Asm_full_simp_tac 1);
|
|
388 |
val is_type_fields = result() RS bspec;
|