1 (* Title: HOL/MicroJava/J/WellForm.ML
3 Author: David von Oheimb
4 Copyright 1999 Technische Universitaet Muenchen
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 wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
10 fast_tac (set_cs addDs [get_in_set]) 1]);
12 val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
13 "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
17 Addsimps [class_Object];
19 val is_class_Object = prove_goalw thy [is_class_def]
20 "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
21 Addsimps [is_class_Object];
23 Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
24 by( forward_tac [r_into_trancl] 1);
27 by( datac class_wf 1 1);
28 by( rewtac wf_cdecl_def);
29 by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
30 delsimps [reflcl_trancl]) 1);
33 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
34 "\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
36 asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
38 Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
40 by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
43 val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
44 etac trancl_trans_induct 1,
45 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
46 fast_tac (HOL_cs addDs [subcls_asym]) 1]);
48 val acyclic_subcls1 = prove_goalw thy [acyclic_def]
49 "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
51 fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
53 val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
54 rtac finite_acyclic_wf 1,
55 stac finite_converse 1,
56 rtac finite_subcls1 1,
57 stac acyclic_converse 1,
58 etac acyclic_subcls1 1]);
60 val major::prems = goal thy
61 "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
62 by(cut_facts_tac [major RS wf_subcls1] 1);
64 by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
65 by(eres_inst_tac [("a","C")] wf_induct 1);
66 by(resolve_tac prems 1);
70 val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
71 \\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
72 \ wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
73 \ \\<rbrakk> \\<Longrightarrow> P C";
74 by( cut_facts_tac prems 1);
79 by( rtac subcls_induct 1);
82 by( case_tac "C = Object" 1);
84 by( ex_ftac is_classD 1);
85 by( forward_tac [class_wf] 1);
87 by( forward_tac [wf_cdecl_supD] 1);
90 by( rtac (hd (tl (tl (tl prems)))) 1);
93 by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
94 by( fast_tac (HOL_cs addIs [r_into_trancl]) 1);
98 Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
99 \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
100 \ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
101 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
102 by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1);
103 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
104 addsplits [option.split]) 1);
105 by( case_tac "C = Object" 1);
106 by( Asm_full_simp_tac 1);
107 by( dtac class_wf 1);
109 by( dtac wf_cdecl_supD 1);
111 by( Asm_full_simp_tac 1);
114 Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
115 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
116 \ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
117 by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
118 by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
119 by( option_case_tac2 "sc" 1);
121 by( case_tac "C = Object" 1);
123 by( Asm_full_simp_tac 1);
124 by( dtac class_wf 1);
126 by( dtac wf_cdecl_supD 1);
128 by( Asm_full_simp_tac 1);
131 val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
132 (K [stac method_rec 1,Auto_tac]);
133 val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
134 stac fields_rec 1,Auto_tac]);
135 Addsimps [method_Object, fields_Object];
136 val field_Object = prove_goalw thy [field_def]
137 "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
138 Addsimps [field_Object];
140 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
141 by(etac subcls1_induct 1);
144 by(auto_tac (HOL_cs addSDs [wf_cdecl_supD], simpset()));
145 by(eatac rtrancl_into_rtrancl2 1 1);
146 qed "subcls_C_Object";
148 val is_type_rTI = prove_goalw thy [wf_mhead_def]
149 "\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
150 (K [split_all_tac 1, Auto_tac]);
152 Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
153 \ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
154 by(etac trancl_trans_induct 1);
155 by( safe_tac (HOL_cs addSDs [subcls1D]));
156 by(stac fields_rec 1);
158 qed_spec_mp "fields_mono";
160 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
161 \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
162 by( etac subcls1_induct 1);
165 by( safe_tac HOL_cs);
166 by( stac fields_rec 1);
171 by( split_all_tac 1);
174 by( dtac split_Pair_eq 1);
175 by( SELECT_GOAL (Auto_tac) 1);
176 by( etac (r_into_rtrancl RS rtrancl_trans) 1);
179 by( Asm_full_simp_tac 1);
180 qed "widen_fields_defpl'";
182 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
183 \ G\\<turnstile>C\\<preceq>C fd";
184 by( datac widen_fields_defpl' 1 1);
185 (*###################*)
188 qed "widen_fields_defpl";
191 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
192 by( etac subcls1_induct 1);
194 by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
196 by( dtac subcls1_wfD 1);
198 by( stac fields_rec 1);
200 by( rotate_tac ~1 1);
201 by( ex_ftac is_classD 1);
202 by( forward_tac [class_wf] 1);
204 by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
205 by( etac unique_append 1);
206 by( rtac unique_map_Pair 1);
208 by (EVERY1[dtac widen_fields_defpl, atac, atac]);
209 by( Asm_full_simp_tac 1);
210 by( dtac split_Pair_eq 1);
211 by( Asm_full_simp_tac 1);
215 Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
216 by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
217 delsimps [reflcl_trancl]) 1);
221 "\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
222 \ map_of (fields (G,C')) f = Some ft";
223 by( dtac rtranclD 1);
225 by( rtac table_mono 1);
227 by( rtac unique_fields 1);
228 by( etac subcls_is_class 1);
230 by( fast_tac (HOL_cs addEs [fields_mono]) 1);
231 qed "widen_fields_mono";
234 val cfs_fields_lemma = prove_goalw thy [field_def]
235 "\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
236 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
238 val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
239 \ G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
240 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
242 Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
243 \ \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
244 by( case_tac "is_class G C" 1);
245 by( forw_inst_tac [("C","C")] method_rec 2);
246 by( asm_full_simp_tac (simpset() addsimps [is_class_def]
247 delsimps [not_None_eq]) 2);
248 by( etac subcls1_induct 1);
251 by( forw_inst_tac [("C","C")] method_rec 1);
253 by( rotate_tac ~1 1);
254 by( Asm_full_simp_tac 1);
255 by( dtac override_SomeD 1);
257 by( thin_tac "?P \\<longrightarrow> ?Q" 1);
259 by( rtac rtrancl_trans 2);
261 by( rtac r_into_rtrancl 2);
262 by( fast_tac (HOL_cs addIs [subcls1I]) 2);
263 by( forward_tac [table_mapf_SomeD] 1);
265 by( Asm_full_simp_tac 1);
266 by( rewtac wf_cdecl_def);
267 by( Asm_full_simp_tac 1);
268 qed_spec_mp "method_wf_mdecl";
270 Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
271 \ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
272 \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
273 by( dtac rtranclD 1);
277 by( etac trancl_trans_induct 1);
279 by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
280 by( fast_tac (HOL_cs addEs [widen_trans]) 2);
282 by( dtac subcls1D 1);
284 by( stac method_rec 1);
286 by( rewtac override_def);
287 by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
288 by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
290 by( asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
291 by( ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
292 by( ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
293 by( dtac class_wf 1);
295 by( split_all_tac 1);
296 by( rewtac wf_cdecl_def);
297 by( dtac table_mapf_Some2 1);
299 by( dres_inst_tac [("xys1","ms")] get_in_set 1);
301 qed_spec_mp "subcls_widen_methd";
305 "\\<lbrakk> G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
306 \ method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
307 \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
308 by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
309 simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
310 qed "subtype_widen_methd";
313 Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
314 by( case_tac "is_class G C" 1);
315 by( forw_inst_tac [("C","C")] method_rec 2);
316 by( asm_full_simp_tac (simpset() addsimps [is_class_def]
317 delsimps [not_None_eq]) 2);
318 by (etac subcls1_induct 1);
320 by (Asm_full_simp_tac 1);
321 by (stac method_rec 1);
324 by (eres_inst_tac [("x","Da")] allE 1);
326 by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
328 by (stac method_rec 1);
330 by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
331 qed_spec_mp "method_in_md";
334 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
335 \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
336 by( etac subcls1_induct 1);
340 by( stac fields_rec 1);
344 by( safe_tac set_cs);
346 by( dtac class_wf 1);
348 by( rewtac wf_cdecl_def);
349 by( Asm_full_simp_tac 1);
351 by( EVERY[dtac bspec 1, atac 1]);
352 by( rewtac wf_fdecl_def);
353 by( split_all_tac 1);
354 by( Asm_full_simp_tac 1);
355 bind_thm ("is_type_fields", result() RS bspec);