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