1 (* Title: HOL/MiniML/Type.thy |
|
2 ID: $Id$ |
|
3 Author: Wolfgang Naraschewski and Tobias Nipkow |
|
4 Copyright 1996 TU Muenchen |
|
5 *) |
|
6 |
|
7 Addsimps [mgu_eq,mgu_mg,mgu_free]; |
|
8 |
|
9 |
|
10 (* lemmata for make scheme *) |
|
11 |
|
12 Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)"; |
|
13 by (induct_tac "t" 1); |
|
14 by (Simp_tac 1); |
|
15 by (Asm_full_simp_tac 1); |
|
16 by (Fast_tac 1); |
|
17 qed_spec_mp "mk_scheme_Fun"; |
|
18 |
|
19 Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'"; |
|
20 by (induct_tac "t" 1); |
|
21 by (rtac allI 1); |
|
22 by (induct_tac "t'" 1); |
|
23 by (Simp_tac 1); |
|
24 by (Asm_full_simp_tac 1); |
|
25 by (rtac allI 1); |
|
26 by (induct_tac "t'" 1); |
|
27 by (Simp_tac 1); |
|
28 by (Asm_full_simp_tac 1); |
|
29 qed_spec_mp "mk_scheme_injective"; |
|
30 |
|
31 Goal "free_tv (mk_scheme t) = free_tv t"; |
|
32 by (induct_tac "t" 1); |
|
33 by (ALLGOALS Asm_simp_tac); |
|
34 qed "free_tv_mk_scheme"; |
|
35 |
|
36 Addsimps [free_tv_mk_scheme]; |
|
37 |
|
38 Goal "$ S (mk_scheme t) = mk_scheme ($ S t)"; |
|
39 by (induct_tac "t" 1); |
|
40 by (ALLGOALS Asm_simp_tac); |
|
41 qed "subst_mk_scheme"; |
|
42 |
|
43 Addsimps [subst_mk_scheme]; |
|
44 |
|
45 |
|
46 (* constructor laws for app_subst *) |
|
47 |
|
48 Goalw [app_subst_list] |
|
49 "$ S [] = []"; |
|
50 by (Simp_tac 1); |
|
51 qed "app_subst_Nil"; |
|
52 |
|
53 Goalw [app_subst_list] |
|
54 "$ S (x#l) = ($ S x)#($ S l)"; |
|
55 by (Simp_tac 1); |
|
56 qed "app_subst_Cons"; |
|
57 |
|
58 Addsimps [app_subst_Nil,app_subst_Cons]; |
|
59 |
|
60 |
|
61 (* constructor laws for new_tv *) |
|
62 |
|
63 Goalw [new_tv_def] |
|
64 "new_tv n (TVar m) = (m<n)"; |
|
65 by (fast_tac (HOL_cs addss simpset()) 1); |
|
66 qed "new_tv_TVar"; |
|
67 |
|
68 Goalw [new_tv_def] |
|
69 "new_tv n (FVar m) = (m<n)"; |
|
70 by (fast_tac (HOL_cs addss simpset()) 1); |
|
71 qed "new_tv_FVar"; |
|
72 |
|
73 Goalw [new_tv_def] |
|
74 "new_tv n (BVar m) = True"; |
|
75 by (Simp_tac 1); |
|
76 qed "new_tv_BVar"; |
|
77 |
|
78 Goalw [new_tv_def] |
|
79 "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
|
80 by (fast_tac (HOL_cs addss simpset()) 1); |
|
81 qed "new_tv_Fun"; |
|
82 |
|
83 Goalw [new_tv_def] |
|
84 "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)"; |
|
85 by (fast_tac (HOL_cs addss simpset()) 1); |
|
86 qed "new_tv_Fun2"; |
|
87 |
|
88 Goalw [new_tv_def] |
|
89 "new_tv n []"; |
|
90 by (Simp_tac 1); |
|
91 qed "new_tv_Nil"; |
|
92 |
|
93 Goalw [new_tv_def] |
|
94 "new_tv n (x#l) = (new_tv n x & new_tv n l)"; |
|
95 by (fast_tac (HOL_cs addss simpset()) 1); |
|
96 qed "new_tv_Cons"; |
|
97 |
|
98 Goalw [new_tv_def] "new_tv n TVar"; |
|
99 by (strip_tac 1); |
|
100 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1); |
|
101 qed "new_tv_TVar_subst"; |
|
102 |
|
103 Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst]; |
|
104 |
|
105 Goalw [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
|
106 "new_tv n id_subst"; |
|
107 by (Simp_tac 1); |
|
108 qed "new_tv_id_subst"; |
|
109 Addsimps[new_tv_id_subst]; |
|
110 |
|
111 Goal "new_tv n (sch::type_scheme) --> \ |
|
112 \ $(%k. if k<n then S k else S' k) sch = $S sch"; |
|
113 by (induct_tac "sch" 1); |
|
114 by (ALLGOALS Asm_simp_tac); |
|
115 qed "new_if_subst_type_scheme"; |
|
116 Addsimps [new_if_subst_type_scheme]; |
|
117 |
|
118 Goal "new_tv n (A::type_scheme list) --> \ |
|
119 \ $(%k. if k<n then S k else S' k) A = $S A"; |
|
120 by (induct_tac "A" 1); |
|
121 by (ALLGOALS Asm_simp_tac); |
|
122 qed "new_if_subst_type_scheme_list"; |
|
123 Addsimps [new_if_subst_type_scheme_list]; |
|
124 |
|
125 |
|
126 (* constructor laws for dom and cod *) |
|
127 |
|
128 Goalw [dom_def,id_subst_def,empty_def] |
|
129 "dom id_subst = {}"; |
|
130 by (Simp_tac 1); |
|
131 qed "dom_id_subst"; |
|
132 Addsimps [dom_id_subst]; |
|
133 |
|
134 Goalw [cod_def] |
|
135 "cod id_subst = {}"; |
|
136 by (Simp_tac 1); |
|
137 qed "cod_id_subst"; |
|
138 Addsimps [cod_id_subst]; |
|
139 |
|
140 |
|
141 (* lemmata for free_tv *) |
|
142 |
|
143 Goalw [free_tv_subst] |
|
144 "free_tv id_subst = {}"; |
|
145 by (Simp_tac 1); |
|
146 qed "free_tv_id_subst"; |
|
147 Addsimps [free_tv_id_subst]; |
|
148 |
|
149 Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A"; |
|
150 by (induct_tac "A" 1); |
|
151 by (Asm_full_simp_tac 1); |
|
152 by (rtac allI 1); |
|
153 by (induct_thm_tac nat_induct "n" 1); |
|
154 by (Asm_full_simp_tac 1); |
|
155 by (Asm_full_simp_tac 1); |
|
156 qed_spec_mp "free_tv_nth_A_impl_free_tv_A"; |
|
157 |
|
158 Addsimps [free_tv_nth_A_impl_free_tv_A]; |
|
159 |
|
160 Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A"; |
|
161 by (induct_tac "A" 1); |
|
162 by (Asm_full_simp_tac 1); |
|
163 by (rtac allI 1); |
|
164 by (induct_thm_tac nat_induct "nat" 1); |
|
165 by (strip_tac 1); |
|
166 by (Asm_full_simp_tac 1); |
|
167 by (Simp_tac 1); |
|
168 qed_spec_mp "free_tv_nth_nat_A"; |
|
169 |
|
170 |
|
171 (* if two substitutions yield the same result if applied to a type |
|
172 structure the substitutions coincide on the free type variables |
|
173 occurring in the type structure *) |
|
174 |
|
175 Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t"; |
|
176 by (induct_tac "t" 1); |
|
177 by (Simp_tac 1); |
|
178 by (Asm_full_simp_tac 1); |
|
179 qed_spec_mp "typ_substitutions_only_on_free_variables"; |
|
180 |
|
181 Goal "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t"; |
|
182 by (rtac typ_substitutions_only_on_free_variables 1); |
|
183 by (simp_tac (simpset() addsimps [Ball_def]) 1); |
|
184 qed "eq_free_eq_subst_te"; |
|
185 |
|
186 Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch"; |
|
187 by (induct_tac "sch" 1); |
|
188 by (Simp_tac 1); |
|
189 by (Simp_tac 1); |
|
190 by (Asm_full_simp_tac 1); |
|
191 qed_spec_mp "scheme_substitutions_only_on_free_variables"; |
|
192 |
|
193 Goal |
|
194 "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch"; |
|
195 by (rtac scheme_substitutions_only_on_free_variables 1); |
|
196 by (simp_tac (simpset() addsimps [Ball_def]) 1); |
|
197 qed "eq_free_eq_subst_type_scheme"; |
|
198 |
|
199 Goal |
|
200 "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"; |
|
201 by (induct_tac "A" 1); |
|
202 (* case [] *) |
|
203 by (fast_tac (HOL_cs addss simpset()) 1); |
|
204 (* case x#xl *) |
|
205 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1); |
|
206 qed_spec_mp "eq_free_eq_subst_scheme_list"; |
|
207 |
|
208 Goal "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"; |
|
209 by (Fast_tac 1); |
|
210 val weaken_asm_Un = result (); |
|
211 |
|
212 Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A"; |
|
213 by (induct_tac "A" 1); |
|
214 by (Simp_tac 1); |
|
215 by (Asm_full_simp_tac 1); |
|
216 by (rtac weaken_asm_Un 1); |
|
217 by (strip_tac 1); |
|
218 by (etac scheme_substitutions_only_on_free_variables 1); |
|
219 qed_spec_mp "scheme_list_substitutions_only_on_free_variables"; |
|
220 |
|
221 Goal |
|
222 "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"; |
|
223 by (induct_tac "t" 1); |
|
224 (* case TVar n *) |
|
225 by (fast_tac (HOL_cs addss simpset()) 1); |
|
226 (* case Fun t1 t2 *) |
|
227 by (fast_tac (HOL_cs addss simpset()) 1); |
|
228 qed_spec_mp "eq_subst_te_eq_free"; |
|
229 |
|
230 Goal |
|
231 "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"; |
|
232 by (induct_tac "sch" 1); |
|
233 (* case TVar n *) |
|
234 by (Asm_simp_tac 1); |
|
235 (* case BVar n *) |
|
236 by (strip_tac 1); |
|
237 by (etac mk_scheme_injective 1); |
|
238 by (Asm_simp_tac 1); |
|
239 (* case Fun t1 t2 *) |
|
240 by (Asm_full_simp_tac 1); |
|
241 qed_spec_mp "eq_subst_type_scheme_eq_free"; |
|
242 |
|
243 Goal |
|
244 "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"; |
|
245 by (induct_tac "A" 1); |
|
246 (* case [] *) |
|
247 by (fast_tac (HOL_cs addss simpset()) 1); |
|
248 (* case x#xl *) |
|
249 by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (simpset())) 1); |
|
250 qed_spec_mp "eq_subst_scheme_list_eq_free"; |
|
251 |
|
252 Goalw [free_tv_subst] |
|
253 "v : cod S ==> v : free_tv S"; |
|
254 by (fast_tac set_cs 1); |
|
255 qed "codD"; |
|
256 |
|
257 Goalw [free_tv_subst,dom_def] |
|
258 "x ~: free_tv S ==> S x = TVar x"; |
|
259 by (fast_tac set_cs 1); |
|
260 qed "not_free_impl_id"; |
|
261 |
|
262 Goalw [new_tv_def] |
|
263 "[| new_tv n t; m:free_tv t |] ==> m<n"; |
|
264 by (fast_tac HOL_cs 1 ); |
|
265 qed "free_tv_le_new_tv"; |
|
266 |
|
267 Goalw [dom_def,cod_def,UNION_def,Bex_def] |
|
268 "[| v : free_tv(S n); v~=n |] ==> v : cod S"; |
|
269 by (Simp_tac 1); |
|
270 by (safe_tac (empty_cs addSIs [exI,conjI,notI])); |
|
271 by (assume_tac 2); |
|
272 by (Asm_full_simp_tac 1); |
|
273 qed "cod_app_subst"; |
|
274 Addsimps [cod_app_subst]; |
|
275 |
|
276 Goal "free_tv (S (v::nat)) <= insert v (cod S)"; |
|
277 by (expand_case_tac "v:dom S" 1); |
|
278 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1); |
|
279 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1); |
|
280 qed "free_tv_subst_var"; |
|
281 |
|
282 Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t"; |
|
283 by (induct_tac "t" 1); |
|
284 (* case TVar n *) |
|
285 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); |
|
286 (* case Fun t1 t2 *) |
|
287 by (fast_tac (set_cs addss simpset()) 1); |
|
288 qed "free_tv_app_subst_te"; |
|
289 |
|
290 Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"; |
|
291 by (induct_tac "sch" 1); |
|
292 (* case FVar n *) |
|
293 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); |
|
294 (* case BVar n *) |
|
295 by (Simp_tac 1); |
|
296 (* case Fun t1 t2 *) |
|
297 by (fast_tac (set_cs addss simpset()) 1); |
|
298 qed "free_tv_app_subst_type_scheme"; |
|
299 |
|
300 Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"; |
|
301 by (induct_tac "A" 1); |
|
302 (* case [] *) |
|
303 by (Simp_tac 1); |
|
304 (* case a#al *) |
|
305 by (cut_facts_tac [free_tv_app_subst_type_scheme] 1); |
|
306 by (fast_tac (set_cs addss simpset()) 1); |
|
307 qed "free_tv_app_subst_scheme_list"; |
|
308 |
|
309 Goalw [free_tv_subst,dom_def] |
|
310 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
|
311 \ free_tv s1 Un free_tv s2"; |
|
312 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
|
313 free_tv_subst_var RS subsetD] |
|
314 addss (simpset() delsimps bex_simps |
|
315 addsimps [cod_def,dom_def])) 1); |
|
316 qed "free_tv_comp_subst"; |
|
317 |
|
318 Goalw [o_def] |
|
319 "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)"; |
|
320 by (rtac free_tv_comp_subst 1); |
|
321 qed "free_tv_o_subst"; |
|
322 |
|
323 Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)"; |
|
324 by (induct_tac "t" 1); |
|
325 by (Simp_tac 1); |
|
326 by (Simp_tac 1); |
|
327 by (Fast_tac 1); |
|
328 qed_spec_mp "free_tv_of_substitutions_extend_to_types"; |
|
329 |
|
330 Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)"; |
|
331 by (induct_tac "sch" 1); |
|
332 by (Simp_tac 1); |
|
333 by (Simp_tac 1); |
|
334 by (Simp_tac 1); |
|
335 by (Fast_tac 1); |
|
336 qed_spec_mp "free_tv_of_substitutions_extend_to_schemes"; |
|
337 |
|
338 Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)"; |
|
339 by (induct_tac "A" 1); |
|
340 by (Simp_tac 1); |
|
341 by (Simp_tac 1); |
|
342 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1); |
|
343 qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists"; |
|
344 |
|
345 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists]; |
|
346 |
|
347 Goal "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))"; |
|
348 by (induct_tac "sch" 1); |
|
349 by (ALLGOALS Asm_simp_tac); |
|
350 qed "free_tv_ML_scheme"; |
|
351 |
|
352 Goal "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))"; |
|
353 by (induct_tac "A" 1); |
|
354 by (Simp_tac 1); |
|
355 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1); |
|
356 qed "free_tv_ML_scheme_list"; |
|
357 |
|
358 |
|
359 (* lemmata for bound_tv *) |
|
360 |
|
361 Goal "bound_tv (mk_scheme t) = {}"; |
|
362 by (induct_tac "t" 1); |
|
363 by (ALLGOALS Asm_simp_tac); |
|
364 qed "bound_tv_mk_scheme"; |
|
365 |
|
366 Addsimps [bound_tv_mk_scheme]; |
|
367 |
|
368 Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch"; |
|
369 by (induct_tac "sch" 1); |
|
370 by (ALLGOALS Asm_simp_tac); |
|
371 qed "bound_tv_subst_scheme"; |
|
372 |
|
373 Addsimps [bound_tv_subst_scheme]; |
|
374 |
|
375 Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A"; |
|
376 by (rtac (thm"list.induct") 1); |
|
377 by (Simp_tac 1); |
|
378 by (Asm_simp_tac 1); |
|
379 qed "bound_tv_subst_scheme_list"; |
|
380 |
|
381 Addsimps [bound_tv_subst_scheme_list]; |
|
382 |
|
383 |
|
384 (* lemmata for new_tv *) |
|
385 |
|
386 Goalw [new_tv_def] |
|
387 "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \ |
|
388 \ (! l. l < n --> new_tv n (S l) ))"; |
|
389 by (safe_tac HOL_cs ); |
|
390 (* ==> *) |
|
391 by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1); |
|
392 by (subgoal_tac "m:cod S | S l = TVar l" 1); |
|
393 by (safe_tac HOL_cs ); |
|
394 by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1); |
|
395 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
|
396 by (Asm_full_simp_tac 1); |
|
397 by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1); |
|
398 (* <== *) |
|
399 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
|
400 by (safe_tac set_cs ); |
|
401 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
|
402 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
|
403 by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
|
404 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
|
405 qed "new_tv_subst"; |
|
406 |
|
407 Goal "new_tv n x = (!y:set x. new_tv n y)"; |
|
408 by (induct_tac "x" 1); |
|
409 by (ALLGOALS Asm_simp_tac); |
|
410 qed "new_tv_list"; |
|
411 |
|
412 (* substitution affects only variables occurring freely *) |
|
413 Goal |
|
414 "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"; |
|
415 by (induct_tac "t" 1); |
|
416 by (ALLGOALS Asm_simp_tac); |
|
417 qed "subst_te_new_tv"; |
|
418 Addsimps [subst_te_new_tv]; |
|
419 |
|
420 Goal |
|
421 "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"; |
|
422 by (induct_tac "sch" 1); |
|
423 by (ALLGOALS Asm_simp_tac); |
|
424 qed_spec_mp "subst_te_new_type_scheme"; |
|
425 Addsimps [subst_te_new_type_scheme]; |
|
426 |
|
427 Goal |
|
428 "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"; |
|
429 by (induct_tac "A" 1); |
|
430 by (ALLGOALS Asm_full_simp_tac); |
|
431 qed_spec_mp "subst_tel_new_scheme_list"; |
|
432 Addsimps [subst_tel_new_scheme_list]; |
|
433 |
|
434 (* all greater variables are also new *) |
|
435 Goalw [new_tv_def] |
|
436 "n<=m ==> new_tv n t ==> new_tv m t"; |
|
437 by Safe_tac; |
|
438 by (dtac spec 1); |
|
439 by (mp_tac 1); |
|
440 by (Simp_tac 1); |
|
441 qed "new_tv_le"; |
|
442 Addsimps [lessI RS less_imp_le RS new_tv_le]; |
|
443 |
|
444 Goal "n<=m ==> new_tv n (t::typ) ==> new_tv m t"; |
|
445 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
|
446 qed "new_tv_typ_le"; |
|
447 |
|
448 Goal "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A"; |
|
449 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
|
450 qed "new_scheme_list_le"; |
|
451 |
|
452 Goal "n<=m ==> new_tv n (S::subst) ==> new_tv m S"; |
|
453 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
|
454 qed "new_tv_subst_le"; |
|
455 |
|
456 (* new_tv property remains if a substitution is applied *) |
|
457 Goal |
|
458 "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"; |
|
459 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
|
460 qed "new_tv_subst_var"; |
|
461 |
|
462 Goal |
|
463 "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"; |
|
464 by (induct_tac "t" 1); |
|
465 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
|
466 qed_spec_mp "new_tv_subst_te"; |
|
467 Addsimps [new_tv_subst_te]; |
|
468 |
|
469 Goal "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)"; |
|
470 by (induct_tac "sch" 1); |
|
471 by (ALLGOALS (Asm_full_simp_tac)); |
|
472 by (rewtac new_tv_def); |
|
473 by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1); |
|
474 by (strip_tac 1); |
|
475 by (case_tac "S nat = TVar nat" 1); |
|
476 by (Asm_full_simp_tac 1); |
|
477 by (dres_inst_tac [("x","m")] spec 1); |
|
478 by (Fast_tac 1); |
|
479 qed_spec_mp "new_tv_subst_type_scheme"; |
|
480 Addsimps [new_tv_subst_type_scheme]; |
|
481 |
|
482 Goal |
|
483 "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"; |
|
484 by (induct_tac "A" 1); |
|
485 by (ALLGOALS(fast_tac (HOL_cs addss (simpset())))); |
|
486 qed_spec_mp "new_tv_subst_scheme_list"; |
|
487 Addsimps [new_tv_subst_scheme_list]; |
|
488 |
|
489 Goal "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"; |
|
490 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
|
491 qed "new_tv_Suc_list"; |
|
492 |
|
493 Goalw [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')"; |
|
494 by (Asm_simp_tac 1); |
|
495 qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme"; |
|
496 |
|
497 Goalw [new_tv_def] "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')"; |
|
498 by (Asm_simp_tac 1); |
|
499 qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list"; |
|
500 |
|
501 Goalw [new_tv_def] |
|
502 "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))"; |
|
503 by (induct_tac "A" 1); |
|
504 by (Asm_full_simp_tac 1); |
|
505 by (rtac allI 1); |
|
506 by (induct_thm_tac nat_induct "nat" 1); |
|
507 by (strip_tac 1); |
|
508 by (Asm_full_simp_tac 1); |
|
509 by (Simp_tac 1); |
|
510 qed_spec_mp "new_tv_nth_nat_A"; |
|
511 |
|
512 |
|
513 (* composition of substitutions preserves new_tv proposition *) |
|
514 Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)"; |
|
515 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
|
516 qed "new_tv_subst_comp_1"; |
|
517 |
|
518 Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))"; |
|
519 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
|
520 qed "new_tv_subst_comp_2"; |
|
521 |
|
522 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
|
523 |
|
524 (* new type variables do not occur freely in a type structure *) |
|
525 Goalw [new_tv_def] |
|
526 "new_tv n A ==> n~:(free_tv A)"; |
|
527 by (fast_tac (HOL_cs addEs [less_irrefl]) 1); |
|
528 qed "new_tv_not_free_tv"; |
|
529 Addsimps [new_tv_not_free_tv]; |
|
530 |
|
531 Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)"; |
|
532 by (induct_tac "t" 1); |
|
533 by (res_inst_tac [("x","Suc nat")] exI 1); |
|
534 by (Asm_simp_tac 1); |
|
535 by (REPEAT (etac exE 1)); |
|
536 by (rename_tac "n'" 1); |
|
537 by (res_inst_tac [("x","max n n'")] exI 1); |
|
538 by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1); |
|
539 by (Blast_tac 1); |
|
540 qed "fresh_variable_types"; |
|
541 |
|
542 Addsimps [fresh_variable_types]; |
|
543 |
|
544 Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)"; |
|
545 by (induct_tac "sch" 1); |
|
546 by (res_inst_tac [("x","Suc nat")] exI 1); |
|
547 by (Simp_tac 1); |
|
548 by (res_inst_tac [("x","Suc nat")] exI 1); |
|
549 by (Simp_tac 1); |
|
550 by (REPEAT (etac exE 1)); |
|
551 by (rename_tac "n'" 1); |
|
552 by (res_inst_tac [("x","max n n'")] exI 1); |
|
553 by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1); |
|
554 by (Blast_tac 1); |
|
555 qed "fresh_variable_type_schemes"; |
|
556 |
|
557 Addsimps [fresh_variable_type_schemes]; |
|
558 |
|
559 Goal "!!A::type_scheme list. ? n. (new_tv n A)"; |
|
560 by (induct_tac "A" 1); |
|
561 by (Simp_tac 1); |
|
562 by (Simp_tac 1); |
|
563 by (etac exE 1); |
|
564 by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1); |
|
565 by (etac exE 1); |
|
566 by (rename_tac "n'" 1); |
|
567 by (res_inst_tac [("x","(max n n')")] exI 1); |
|
568 by (subgoal_tac "n <= (max n n')" 1); |
|
569 by (subgoal_tac "n' <= (max n n')" 1); |
|
570 by (fast_tac (claset() addDs [new_tv_le]) 1); |
|
571 by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj]))); |
|
572 qed "fresh_variable_type_scheme_lists"; |
|
573 |
|
574 Addsimps [fresh_variable_type_scheme_lists]; |
|
575 |
|
576 Goal "[| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)"; |
|
577 by (REPEAT (etac exE 1)); |
|
578 by (rename_tac "n1 n2" 1); |
|
579 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
|
580 by (subgoal_tac "n1 <= max n1 n2" 1); |
|
581 by (subgoal_tac "n2 <= max n1 n2" 1); |
|
582 by (fast_tac (claset() addDs [new_tv_le]) 1); |
|
583 by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj]))); |
|
584 qed "make_one_new_out_of_two"; |
|
585 |
|
586 Goal "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \ |
|
587 \ ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ; |
|
588 by (cut_inst_tac [("t","t")] fresh_variable_types 1); |
|
589 by (cut_inst_tac [("t","t'")] fresh_variable_types 1); |
|
590 by (dtac make_one_new_out_of_two 1); |
|
591 by (assume_tac 1); |
|
592 by (thin_tac "? n. new_tv n t'" 1); |
|
593 by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1); |
|
594 by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1); |
|
595 by (rotate_tac 1 1); |
|
596 by (dtac make_one_new_out_of_two 1); |
|
597 by (assume_tac 1); |
|
598 by (thin_tac "? n. new_tv n A'" 1); |
|
599 by (REPEAT (etac exE 1)); |
|
600 by (rename_tac "n2 n1" 1); |
|
601 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
|
602 by (rewtac new_tv_def); |
|
603 by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1); |
|
604 by (Blast_tac 1); |
|
605 qed "ex_fresh_variable"; |
|
606 |
|
607 (* mgu does not introduce new type variables *) |
|
608 Goalw [new_tv_def] |
|
609 "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"; |
|
610 by (fast_tac (set_cs addDs [mgu_free]) 1); |
|
611 qed "mgu_new"; |
|
612 |
|
613 |
|
614 (* lemmata for substitutions *) |
|
615 |
|
616 Goalw [app_subst_list] |
|
617 "!!A:: ('a::type_struct) list. length ($ S A) = length A"; |
|
618 by (Simp_tac 1); |
|
619 qed "length_app_subst_list"; |
|
620 Addsimps [length_app_subst_list]; |
|
621 |
|
622 Goal "!!sch::type_scheme. $ TVar sch = sch"; |
|
623 by (induct_tac "sch" 1); |
|
624 by (ALLGOALS Asm_simp_tac); |
|
625 qed "subst_TVar_scheme"; |
|
626 |
|
627 Addsimps [subst_TVar_scheme]; |
|
628 |
|
629 Goal "!!A::type_scheme list. $ TVar A = A"; |
|
630 by (rtac (thm"list.induct") 1); |
|
631 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list]))); |
|
632 qed "subst_TVar_scheme_list"; |
|
633 |
|
634 Addsimps [subst_TVar_scheme_list]; |
|
635 |
|
636 (* application of id_subst does not change type expression *) |
|
637 Goalw [id_subst_def] |
|
638 "$ id_subst = (%t::typ. t)"; |
|
639 by (rtac ext 1); |
|
640 by (induct_tac "t" 1); |
|
641 by (ALLGOALS Asm_simp_tac); |
|
642 qed "app_subst_id_te"; |
|
643 Addsimps [app_subst_id_te]; |
|
644 |
|
645 Goalw [id_subst_def] |
|
646 "$ id_subst = (%sch::type_scheme. sch)"; |
|
647 by (rtac ext 1); |
|
648 by (induct_tac "sch" 1); |
|
649 by (ALLGOALS Asm_simp_tac); |
|
650 qed "app_subst_id_type_scheme"; |
|
651 Addsimps [app_subst_id_type_scheme]; |
|
652 |
|
653 (* application of id_subst does not change list of type expressions *) |
|
654 Goalw [app_subst_list] |
|
655 "$ id_subst = (%A::type_scheme list. A)"; |
|
656 by (rtac ext 1); |
|
657 by (induct_tac "A" 1); |
|
658 by (ALLGOALS Asm_simp_tac); |
|
659 qed "app_subst_id_tel"; |
|
660 Addsimps [app_subst_id_tel]; |
|
661 |
|
662 Goal "!!sch::type_scheme. $ id_subst sch = sch"; |
|
663 by (induct_tac "sch" 1); |
|
664 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def]))); |
|
665 qed "id_subst_sch"; |
|
666 |
|
667 Addsimps [id_subst_sch]; |
|
668 |
|
669 Goal "!!A::type_scheme list. $ id_subst A = A"; |
|
670 by (induct_tac "A" 1); |
|
671 by (Asm_full_simp_tac 1); |
|
672 by (Asm_full_simp_tac 1); |
|
673 qed "id_subst_A"; |
|
674 |
|
675 Addsimps [id_subst_A]; |
|
676 |
|
677 (* composition of substitutions *) |
|
678 Goalw [id_subst_def,o_def] "$S o id_subst = S"; |
|
679 by (rtac ext 1); |
|
680 by (Simp_tac 1); |
|
681 qed "o_id_subst"; |
|
682 Addsimps[o_id_subst]; |
|
683 |
|
684 Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t"; |
|
685 by (induct_tac "t" 1); |
|
686 by (ALLGOALS Asm_simp_tac); |
|
687 qed "subst_comp_te"; |
|
688 |
|
689 Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch"; |
|
690 by (induct_tac "sch" 1); |
|
691 by (ALLGOALS Asm_full_simp_tac); |
|
692 qed "subst_comp_type_scheme"; |
|
693 |
|
694 Goalw [app_subst_list] |
|
695 "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"; |
|
696 by (induct_tac "A" 1); |
|
697 (* case [] *) |
|
698 by (Simp_tac 1); |
|
699 (* case x#xl *) |
|
700 by (asm_full_simp_tac (simpset() addsimps [subst_comp_type_scheme]) 1); |
|
701 qed "subst_comp_scheme_list"; |
|
702 |
|
703 Goal "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A"; |
|
704 by (rtac scheme_list_substitutions_only_on_free_variables 1); |
|
705 by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1); |
|
706 qed "subst_id_on_type_scheme_list'"; |
|
707 |
|
708 Goal "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"; |
|
709 by (stac subst_id_on_type_scheme_list' 1); |
|
710 by (assume_tac 1); |
|
711 by (Simp_tac 1); |
|
712 qed "subst_id_on_type_scheme_list"; |
|
713 |
|
714 Goal "!n. n < length A --> ($ S A)!n = $S (A!n)"; |
|
715 by (induct_tac "A" 1); |
|
716 by (Asm_full_simp_tac 1); |
|
717 by (rtac allI 1); |
|
718 by (rename_tac "n1" 1); |
|
719 by (induct_thm_tac nat_induct "n1" 1); |
|
720 by (Asm_full_simp_tac 1); |
|
721 by (Asm_full_simp_tac 1); |
|
722 qed_spec_mp "nth_subst"; |
|