|
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; |