1 (* Title: HOL/MiniML/W.ML |
|
2 ID: $Id$ |
|
3 Author: Dieter Nazareth and Tobias Nipkow |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 Correctness and completeness of type inference algorithm W |
|
7 *) |
|
8 |
|
9 Addsimps [Suc_le_lessD]; Delsimps [less_imp_le]; (*the combination loops*) |
|
10 |
|
11 val has_type_casesE = |
|
12 map has_type.mk_cases |
|
13 [" A |- Var n :: t", |
|
14 " A |- Abs e :: t", |
|
15 "A |- App e1 e2 ::t", |
|
16 "A |- LET e1 e2 ::t" ]; |
|
17 |
|
18 (* the resulting type variable is always greater or equal than the given one *) |
|
19 Goal "!A n S t m. W e A n = Some (S,t,m) --> n<=m"; |
|
20 by (induct_tac "e" 1); |
|
21 (* case Var(n) *) |
|
22 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
23 (* case Abs e *) |
|
24 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
25 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
|
26 (* case App e1 e2 *) |
|
27 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
28 by (blast_tac (claset() addIs [le_SucI,le_trans]) 1); |
|
29 (* case LET e1 e2 *) |
|
30 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
31 by (blast_tac (claset() addIs [le_trans]) 1); |
|
32 qed_spec_mp "W_var_ge"; |
|
33 |
|
34 Addsimps [W_var_ge]; |
|
35 |
|
36 Goal "Some (S,t,m) = W e A n ==> n<=m"; |
|
37 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
38 qed "W_var_geD"; |
|
39 |
|
40 Goal "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"; |
|
41 by (dtac W_var_geD 1); |
|
42 by (rtac new_scheme_list_le 1); |
|
43 by (assume_tac 1); |
|
44 by (assume_tac 1); |
|
45 qed "new_tv_compatible_W"; |
|
46 |
|
47 Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; |
|
48 by (induct_tac "sch" 1); |
|
49 by (Asm_full_simp_tac 1); |
|
50 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); |
|
51 by (strip_tac 1); |
|
52 by (Asm_full_simp_tac 1); |
|
53 by (etac conjE 1); |
|
54 by (rtac conjI 1); |
|
55 by (rtac new_tv_le 1); |
|
56 by (assume_tac 2); |
|
57 by (rtac add_le_mono 1); |
|
58 by (Simp_tac 1); |
|
59 by (simp_tac (simpset() addsimps [max_def]) 1); |
|
60 by (rtac new_tv_le 1); |
|
61 by (assume_tac 2); |
|
62 by (rtac add_le_mono 1); |
|
63 by (Simp_tac 1); |
|
64 by (simp_tac (simpset() addsimps [max_def]) 1); |
|
65 qed_spec_mp "new_tv_bound_typ_inst_sch"; |
|
66 |
|
67 Addsimps [new_tv_bound_typ_inst_sch]; |
|
68 |
|
69 (* resulting type variable is new *) |
|
70 Goal "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) --> \ |
|
71 \ new_tv m S & new_tv m t"; |
|
72 by (induct_tac "e" 1); |
|
73 (* case Var n *) |
|
74 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
75 by (strip_tac 1); |
|
76 by (dtac new_tv_nth_nat_A 1); |
|
77 by (assume_tac 1); |
|
78 by (Asm_simp_tac 1); |
|
79 (* case Abs e *) |
|
80 by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] |
|
81 addsplits [split_option_bind]) 1); |
|
82 by (strip_tac 1); |
|
83 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
84 by (eres_inst_tac [("x","(FVar n)#A")] allE 1); |
|
85 by (fast_tac (HOL_cs addss (simpset() |
|
86 addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
|
87 (* case App e1 e2 *) |
|
88 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
89 by (strip_tac 1); |
|
90 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); |
|
91 by (eres_inst_tac [("x","n")] allE 1); |
|
92 by (eres_inst_tac [("x","A")] allE 1); |
|
93 by (eres_inst_tac [("x","S1")] allE 1); |
|
94 by (eres_inst_tac [("x","t1")] allE 1); |
|
95 by (eres_inst_tac [("x","n1")] allE 1); |
|
96 by (eres_inst_tac [("x","n1")] allE 1); |
|
97 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv] delsimps all_simps) 1); |
|
98 by (eres_inst_tac [("x","$S1 A")] allE 1); |
|
99 by (eres_inst_tac [("x","S2")] allE 1); |
|
100 by (eres_inst_tac [("x","t2")] allE 1); |
|
101 by (eres_inst_tac [("x","n2")] allE 1); |
|
102 by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Some]) 1); |
|
103 by (rtac conjI 1); |
|
104 by (rtac new_tv_subst_comp_2 1); |
|
105 by (rtac new_tv_subst_comp_2 1); |
|
106 by (rtac (lessI RS less_imp_le RS new_tv_le) 1); |
|
107 by (res_inst_tac [("n","n1")] new_tv_subst_le 1); |
|
108 by (asm_full_simp_tac (simpset() addsimps [rotate_Some]) 1); |
|
109 by (Asm_simp_tac 1); |
|
110 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
111 [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le]) |
|
112 1); |
|
113 by (etac (sym RS mgu_new) 1); |
|
114 by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le, |
|
115 new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS |
|
116 new_tv_subst_le,new_tv_le]) 1); |
|
117 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
118 [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] |
|
119 addss (simpset())) 1); |
|
120 by (rtac (lessI RS new_tv_subst_var) 1); |
|
121 by (etac (sym RS mgu_new) 1); |
|
122 by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] |
|
123 addDs [W_var_geD] addIs |
|
124 [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS |
|
125 new_tv_subst_le,new_tv_le] addss simpset()) 1); |
|
126 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
127 [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] |
|
128 addss (simpset())) 1); |
|
129 (* 41: case LET e1 e2 *) |
|
130 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
131 by (strip_tac 1); |
|
132 by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]); |
|
133 by (etac conjE 1); |
|
134 by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1, |
|
135 etac impE 1, mp_tac 2]); |
|
136 by (SELECT_GOAL(rewtac new_tv_def)1); |
|
137 by (Asm_simp_tac 1); |
|
138 by (REPEAT(dtac W_var_ge 1)); |
|
139 by (rtac allI 1); |
|
140 by (strip_tac 1); |
|
141 by (SELECT_GOAL(rewtac free_tv_subst) 1); |
|
142 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); |
|
143 by (best_tac (claset() addEs [less_le_trans]) 1); |
|
144 by (etac conjE 1); |
|
145 by (rtac conjI 1); |
|
146 by (SELECT_GOAL(rewtac o_def)1); |
|
147 by (rtac new_tv_subst_comp_2 1); |
|
148 by (etac (W_var_ge RS new_tv_subst_le) 1); |
|
149 by (assume_tac 1); |
|
150 by (assume_tac 1); |
|
151 by (assume_tac 1); |
|
152 qed_spec_mp "new_tv_W"; |
|
153 |
|
154 Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)"; |
|
155 by (induct_tac "sch" 1); |
|
156 by (Asm_full_simp_tac 1); |
|
157 by (Asm_full_simp_tac 1); |
|
158 by (strip_tac 1); |
|
159 by (rtac exI 1); |
|
160 by (rtac refl 1); |
|
161 by (Asm_full_simp_tac 1); |
|
162 qed_spec_mp "free_tv_bound_typ_inst1"; |
|
163 |
|
164 Addsimps [free_tv_bound_typ_inst1]; |
|
165 |
|
166 Goal "!n A S t m v. W e A n = Some (S,t,m) --> \ |
|
167 \ (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A"; |
|
168 by (induct_tac "e" 1); |
|
169 (* case Var n *) |
|
170 by (simp_tac (simpset() addsimps |
|
171 [free_tv_subst] addsplits [split_option_bind]) 1); |
|
172 by (strip_tac 1); |
|
173 by (case_tac "v : free_tv (A!nat)" 1); |
|
174 by (Asm_full_simp_tac 1); |
|
175 by (dtac free_tv_bound_typ_inst1 1); |
|
176 by (simp_tac (simpset() addsimps [o_def]) 1); |
|
177 by (etac exE 1); |
|
178 by (Asm_full_simp_tac 1); |
|
179 (* case Abs e *) |
|
180 by (asm_full_simp_tac (simpset() addsimps |
|
181 [free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1); |
|
182 by (strip_tac 1); |
|
183 by (rename_tac "S t n1 v" 1); |
|
184 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
185 by (eres_inst_tac [("x","FVar n # A")] allE 1); |
|
186 by (eres_inst_tac [("x","S")] allE 1); |
|
187 by (eres_inst_tac [("x","t")] allE 1); |
|
188 by (eres_inst_tac [("x","n1")] allE 1); |
|
189 by (eres_inst_tac [("x","v")] allE 1); |
|
190 by (best_tac (HOL_cs addIs [cod_app_subst] |
|
191 addss (simpset() addsimps [less_Suc_eq])) 1); |
|
192 (* case App e1 e2 *) |
|
193 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); |
|
194 by (strip_tac 1); |
|
195 by (rename_tac "S t n1 S1 t1 n2 S2 v" 1); |
|
196 by (eres_inst_tac [("x","n")] allE 1); |
|
197 by (eres_inst_tac [("x","A")] allE 1); |
|
198 by (eres_inst_tac [("x","S")] allE 1); |
|
199 by (eres_inst_tac [("x","t")] allE 1); |
|
200 by (eres_inst_tac [("x","n1")] allE 1); |
|
201 by (eres_inst_tac [("x","n1")] allE 1); |
|
202 by (eres_inst_tac [("x","v")] allE 1); |
|
203 (* second case *) |
|
204 by (eres_inst_tac [("x","$ S A")] allE 1); |
|
205 by (eres_inst_tac [("x","S1")] allE 1); |
|
206 by (eres_inst_tac [("x","t1")] allE 1); |
|
207 by (eres_inst_tac [("x","n2")] allE 1); |
|
208 by (eres_inst_tac [("x","v")] allE 1); |
|
209 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); |
|
210 by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1); |
|
211 by (dtac W_var_geD 1); |
|
212 by (dtac W_var_geD 1); |
|
213 by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); |
|
214 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, |
|
215 codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, |
|
216 less_le_trans,less_not_refl2,subsetD] |
|
217 addEs [UnE] |
|
218 addss simpset()) 1); |
|
219 by (Asm_full_simp_tac 1); |
|
220 by (dtac (sym RS W_var_geD) 1); |
|
221 by (dtac (sym RS W_var_geD) 1); |
|
222 by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); |
|
223 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, |
|
224 free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, |
|
225 less_le_trans,subsetD] |
|
226 addEs [UnE] |
|
227 addss (simpset() setSolver unsafe_solver)) 1); |
|
228 (* LET e1 e2 *) |
|
229 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); |
|
230 by (strip_tac 1); |
|
231 by (rename_tac "S1 t1 n2 S2 t2 n3 v" 1); |
|
232 by (eres_inst_tac [("x","n")] allE 1); |
|
233 by (eres_inst_tac [("x","A")] allE 1); |
|
234 by (eres_inst_tac [("x","S1")] allE 1); |
|
235 by (eres_inst_tac [("x","t1")] allE 1); |
|
236 by (rotate_tac ~1 1); |
|
237 by (eres_inst_tac [("x","n2")] allE 1); |
|
238 by (rotate_tac ~1 1); |
|
239 by (eres_inst_tac [("x","v")] allE 1); |
|
240 by (mp_tac 1); |
|
241 by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]); |
|
242 by (mp_tac 1); |
|
243 by (Asm_full_simp_tac 1); |
|
244 by (rtac conjI 1); |
|
245 by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] |
|
246 addDs [less_le_trans]) 1); |
|
247 by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] |
|
248 addDs [less_le_trans]) 1); |
|
249 qed_spec_mp "free_tv_W"; |
|
250 |
|
251 Goal "(!x. x : A --> x ~: B) ==> A Int B = {}"; |
|
252 by (Fast_tac 1); |
|
253 val weaken_A_Int_B_eq_empty = result(); |
|
254 |
|
255 Goal "x ~: A | x : B ==> x ~: A - B"; |
|
256 by (Fast_tac 1); |
|
257 val weaken_not_elem_A_minus_B = result(); |
|
258 |
|
259 (* correctness of W with respect to has_type *) |
|
260 Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t"; |
|
261 by (induct_tac "e" 1); |
|
262 (* case Var n *) |
|
263 by (Asm_full_simp_tac 1); |
|
264 by (strip_tac 1); |
|
265 by (rtac has_type.VarI 1); |
|
266 by (Simp_tac 1); |
|
267 by (simp_tac (simpset() addsimps [is_bound_typ_instance]) 1); |
|
268 by (rtac exI 1); |
|
269 by (rtac refl 1); |
|
270 (* case Abs e *) |
|
271 by (asm_full_simp_tac (simpset() addsimps [app_subst_list] |
|
272 addsplits [split_option_bind]) 1); |
|
273 by (strip_tac 1); |
|
274 by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1); |
|
275 by (Asm_full_simp_tac 1); |
|
276 by (rtac has_type.AbsI 1); |
|
277 by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1); |
|
278 by (dtac sym 1); |
|
279 by (REPEAT (etac allE 1)); |
|
280 by (etac impE 1); |
|
281 by (mp_tac 2); |
|
282 by (Asm_simp_tac 1); |
|
283 by (assume_tac 1); |
|
284 (* case App e1 e2 *) |
|
285 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
286 by (strip_tac 1); |
|
287 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); |
|
288 by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1); |
|
289 by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1); |
|
290 by (rtac (app_subst_Fun RS subst) 1); |
|
291 by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1); |
|
292 by (Asm_full_simp_tac 1); |
|
293 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym,o_def]) 1); |
|
294 by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1)); |
|
295 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
296 by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); |
|
297 by (rtac (has_type_cl_sub RS spec) 1); |
|
298 by (ftac new_tv_W 1); |
|
299 by (assume_tac 1); |
|
300 by (dtac conjunct1 1); |
|
301 by (ftac new_tv_subst_scheme_list 1); |
|
302 by (rtac new_scheme_list_le 1); |
|
303 by (rtac W_var_ge 1); |
|
304 by (assume_tac 1); |
|
305 by (assume_tac 1); |
|
306 by (etac thin_rl 1); |
|
307 by (REPEAT (etac allE 1)); |
|
308 by (dtac sym 1); |
|
309 by (dtac sym 1); |
|
310 by (etac thin_rl 1); |
|
311 by (etac thin_rl 1); |
|
312 by (mp_tac 1); |
|
313 by (mp_tac 1); |
|
314 by (assume_tac 1); |
|
315 (* case Let e1 e2 *) |
|
316 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
317 by (strip_tac 1); |
|
318 (*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *) |
|
319 by (rename_tac "S1 t1 m1 S2" 1); |
|
320 by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1); |
|
321 by (simp_tac (simpset() addsimps [o_def]) 1); |
|
322 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); |
|
323 by (rtac (has_type_cl_sub RS spec) 1); |
|
324 by (dres_inst_tac [("x","A")] spec 1); |
|
325 by (dres_inst_tac [("x","S1")] spec 1); |
|
326 by (dres_inst_tac [("x","t1")] spec 1); |
|
327 by (dres_inst_tac [("x","m1")] spec 1); |
|
328 by (dres_inst_tac [("x","n")] spec 1); |
|
329 by (mp_tac 1); |
|
330 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
331 by (simp_tac (simpset() addsimps [o_def]) 1); |
|
332 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); |
|
333 by (rtac (gen_subst_commutes RS sym RS subst) 1); |
|
334 by (rtac (app_subst_Cons RS subst) 2); |
|
335 by (etac thin_rl 2); |
|
336 by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2); |
|
337 by (dres_inst_tac [("x","S2")] spec 2); |
|
338 by (dres_inst_tac [("x","t")] spec 2); |
|
339 by (dres_inst_tac [("x","m")] spec 2); |
|
340 by (dres_inst_tac [("x","m1")] spec 2); |
|
341 by (ftac new_tv_W 2); |
|
342 by (assume_tac 2); |
|
343 by (dtac conjunct1 2); |
|
344 by (ftac new_tv_subst_scheme_list 2); |
|
345 by (rtac new_scheme_list_le 2); |
|
346 by (rtac W_var_ge 2); |
|
347 by (assume_tac 2); |
|
348 by (assume_tac 2); |
|
349 by (etac impE 2); |
|
350 by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2); |
|
351 by (Simp_tac 2); |
|
352 by (Fast_tac 2); |
|
353 by (assume_tac 2); |
|
354 by (Asm_full_simp_tac 2); |
|
355 by (rtac weaken_A_Int_B_eq_empty 1); |
|
356 by (rtac allI 1); |
|
357 by (strip_tac 1); |
|
358 by (rtac weaken_not_elem_A_minus_B 1); |
|
359 by (case_tac "x < m1" 1); |
|
360 by (rtac disjI2 1); |
|
361 by (rtac (free_tv_gen_cons RS subst) 1); |
|
362 by (rtac free_tv_W 1); |
|
363 by (assume_tac 1); |
|
364 by (Asm_full_simp_tac 1); |
|
365 by (assume_tac 1); |
|
366 by (rtac disjI1 1); |
|
367 by (dtac new_tv_W 1); |
|
368 by (assume_tac 1); |
|
369 by (dtac conjunct2 1); |
|
370 by (rtac new_tv_not_free_tv 1); |
|
371 by (rtac new_tv_le 1); |
|
372 by (assume_tac 2); |
|
373 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1); |
|
374 qed_spec_mp "W_correct_lemma"; |
|
375 |
|
376 (* Completeness of W w.r.t. has_type *) |
|
377 Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A --> \ |
|
378 \ (? S t. (? m. W e A n = Some (S,t,m)) & \ |
|
379 \ (? R. $S' A = $R ($S A) & t' = $R t))"; |
|
380 by (induct_tac "e" 1); |
|
381 (* case Var n *) |
|
382 by (strip_tac 1); |
|
383 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
|
384 by (eresolve_tac has_type_casesE 1); |
|
385 by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1); |
|
386 by (etac exE 1); |
|
387 by (hyp_subst_tac 1); |
|
388 by (rename_tac "S" 1); |
|
389 by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1); |
|
390 by (rtac conjI 1); |
|
391 by (Asm_simp_tac 1); |
|
392 by (asm_simp_tac (simpset() addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] |
|
393 delsimps [bound_typ_inst_composed_subst]) 1); |
|
394 (** LEVEL 12 **) |
|
395 (* case Abs e *) |
|
396 by (strip_tac 1); |
|
397 by (eresolve_tac has_type_casesE 1); |
|
398 by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1); |
|
399 by (eres_inst_tac [("x","(FVar n)#A")] allE 1); |
|
400 by (eres_inst_tac [("x","t2")] allE 1); |
|
401 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
402 by (best_tac (HOL_cs addSDs [mk_scheme_injective] |
|
403 addss (simpset() addcongs [conj_cong] |
|
404 addsplits [split_option_bind])) 1); |
|
405 (** LEVEL 19 **) |
|
406 |
|
407 (* case App e1 e2 *) |
|
408 by (strip_tac 1); |
|
409 by (eresolve_tac has_type_casesE 1); |
|
410 by (eres_inst_tac [("x","S'")] allE 1); |
|
411 by (eres_inst_tac [("x","A")] allE 1); |
|
412 by (eres_inst_tac [("x","t2 -> t'")] allE 1); |
|
413 by (eres_inst_tac [("x","n")] allE 1); |
|
414 by (safe_tac HOL_cs); |
|
415 (** LEVEL 26 **) |
|
416 by (eres_inst_tac [("x","R")] allE 1); |
|
417 by (eres_inst_tac [("x","$ S A")] allE 1); |
|
418 by (eres_inst_tac [("x","t2")] allE 1); |
|
419 by (eres_inst_tac [("x","m")] allE 1); |
|
420 by (Asm_full_simp_tac 1); |
|
421 by (safe_tac HOL_cs); |
|
422 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
|
423 conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1); |
|
424 (** LEVEL 33 **) |
|
425 by (subgoal_tac |
|
426 "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
|
427 \ else Ra x)) ($ Sa t) = \ |
|
428 \ $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
|
429 \ else Ra x)) (ta -> (TVar ma))" 1); |
|
430 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ |
|
431 \ (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"), |
|
432 ("s","($ Ra ta) -> t'")] ssubst 2); |
|
433 by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2); |
|
434 by (rtac eq_free_eq_subst_te 2); |
|
435 by (strip_tac 2); |
|
436 by (subgoal_tac "na ~=ma" 2); |
|
437 by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, |
|
438 new_tv_not_free_tv,new_tv_le]) 3); |
|
439 by (case_tac "na:free_tv Sa" 2); |
|
440 (* n1 ~: free_tv S1 *) |
|
441 by (ftac not_free_impl_id 3); |
|
442 by (Asm_simp_tac 3); |
|
443 (* na : free_tv Sa *) |
|
444 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); |
|
445 by (dtac eq_subst_scheme_list_eq_free 2); |
|
446 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
|
447 by (Asm_simp_tac 2); |
|
448 by (case_tac "na:dom Sa" 2); |
|
449 (* na ~: dom Sa *) |
|
450 by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3); |
|
451 (* na : dom Sa *) |
|
452 by (rtac eq_free_eq_subst_te 2); |
|
453 by (strip_tac 2); |
|
454 by (subgoal_tac "nb ~= ma" 2); |
|
455 by ((ftac new_tv_W 3) THEN (atac 3)); |
|
456 by (etac conjE 3); |
|
457 by (dtac new_tv_subst_scheme_list 3); |
|
458 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3); |
|
459 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss |
|
460 (simpset() addsimps [cod_def,free_tv_subst])) 3); |
|
461 by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2); |
|
462 by (Simp_tac 2); |
|
463 by (rtac eq_free_eq_subst_te 2); |
|
464 by (strip_tac 2 ); |
|
465 by (subgoal_tac "na ~= ma" 2); |
|
466 by ((ftac new_tv_W 3) THEN (atac 3)); |
|
467 by (etac conjE 3); |
|
468 by (dtac (sym RS W_var_geD) 3); |
|
469 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3); |
|
470 by (case_tac "na: free_tv t - free_tv Sa" 2); |
|
471 (* case na ~: free_tv t - free_tv Sa *) |
|
472 by (Asm_full_simp_tac 3); |
|
473 by (Fast_tac 3); |
|
474 (* case na : free_tv t - free_tv Sa *) |
|
475 by (Asm_full_simp_tac 2); |
|
476 by (dres_inst_tac [("A1", "$ S A"), ("r", "$ R ($ S A)")] (subst_comp_scheme_list RSN (2,trans)) 2); |
|
477 by (dtac eq_subst_scheme_list_eq_free 2); |
|
478 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
|
479 (** LEVEL 73 **) |
|
480 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2); |
|
481 by (asm_simp_tac (simpset() addsplits [split_option_bind]) 1); |
|
482 by (safe_tac HOL_cs ); |
|
483 by (dtac mgu_Some 1); |
|
484 by ( fast_tac (HOL_cs addss simpset()) 1); |
|
485 (** LEVEL 78 *) |
|
486 by ((dtac mgu_mg 1) THEN (atac 1)); |
|
487 by (etac exE 1); |
|
488 by (res_inst_tac [("x","Rb")] exI 1); |
|
489 by (rtac conjI 1); |
|
490 by (dres_inst_tac [("x","ma")] fun_cong 2); |
|
491 by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2); |
|
492 by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1); |
|
493 by (simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym]) 1); |
|
494 by (res_inst_tac [("A2","($ Sa ($ S A))")] |
|
495 ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); |
|
496 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1); |
|
497 by (dres_inst_tac [("s","Some ?X")] sym 1); |
|
498 by (rtac eq_free_eq_subst_scheme_list 1); |
|
499 by ( safe_tac HOL_cs ); |
|
500 by (subgoal_tac "ma ~= na" 1); |
|
501 by ((ftac new_tv_W 2) THEN (atac 2)); |
|
502 by (etac conjE 2); |
|
503 by (dtac new_tv_subst_scheme_list 2); |
|
504 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2); |
|
505 by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2); |
|
506 by (etac conjE 2); |
|
507 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2); |
|
508 by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD, |
|
509 new_tv_not_free_tv]) 2); |
|
510 by (case_tac "na: free_tv t - free_tv Sa" 1); |
|
511 (* case na ~: free_tv t - free_tv Sa *) |
|
512 by (Asm_full_simp_tac 2); |
|
513 (* case na : free_tv t - free_tv Sa *) |
|
514 by (Asm_full_simp_tac 1); |
|
515 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); |
|
516 by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans), |
|
517 eq_subst_scheme_list_eq_free] addss ((simpset() addsimps |
|
518 [free_tv_subst,dom_def]))) 1); |
|
519 by (Fast_tac 1); |
|
520 (* case Let e1 e2 *) |
|
521 by (eresolve_tac has_type_casesE 1); |
|
522 by (eres_inst_tac [("x","S'")] allE 1); |
|
523 by (eres_inst_tac [("x","A")] allE 1); |
|
524 by (eres_inst_tac [("x","t1")] allE 1); |
|
525 by (eres_inst_tac [("x","n")] allE 1); |
|
526 by (mp_tac 1); |
|
527 by (mp_tac 1); |
|
528 by (safe_tac HOL_cs); |
|
529 by (Asm_simp_tac 1); |
|
530 by (eres_inst_tac [("x","R")] allE 1); |
|
531 by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1); |
|
532 by (eres_inst_tac [("x","t'")] allE 1); |
|
533 by (eres_inst_tac [("x","m")] allE 1); |
|
534 by (Asm_full_simp_tac 1); |
|
535 by (dtac mp 1); |
|
536 by (rtac has_type_le_env 1); |
|
537 by (assume_tac 1); |
|
538 by (Simp_tac 1); |
|
539 by (rtac gen_bound_typ_instance 1); |
|
540 by (dtac mp 1); |
|
541 by (ftac new_tv_compatible_W 1); |
|
542 by (rtac sym 1); |
|
543 by (assume_tac 1); |
|
544 by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1); |
|
545 by (safe_tac HOL_cs); |
|
546 by (Asm_full_simp_tac 1); |
|
547 by (res_inst_tac [("x","Ra")] exI 1); |
|
548 by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1); |
|
549 qed_spec_mp "W_complete_lemma"; |
|
550 |
|
551 Goal "[] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \ |
|
552 \ (? R. t' = $ R t))"; |
|
553 by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")] |
|
554 W_complete_lemma 1); |
|
555 by (ALLGOALS Asm_full_simp_tac); |
|
556 qed "W_complete"; |
|