60 |
60 |
61 (* constructor laws for new_tv *) |
61 (* constructor laws for new_tv *) |
62 |
62 |
63 goalw thy [new_tv_def] |
63 goalw thy [new_tv_def] |
64 "new_tv n (TVar m) = (m<n)"; |
64 "new_tv n (TVar m) = (m<n)"; |
65 by (fast_tac (HOL_cs addss !simpset) 1); |
65 by (fast_tac (HOL_cs addss simpset()) 1); |
66 qed "new_tv_TVar"; |
66 qed "new_tv_TVar"; |
67 |
67 |
68 goalw thy [new_tv_def] |
68 goalw thy [new_tv_def] |
69 "new_tv n (FVar m) = (m<n)"; |
69 "new_tv n (FVar m) = (m<n)"; |
70 by (fast_tac (HOL_cs addss !simpset) 1); |
70 by (fast_tac (HOL_cs addss simpset()) 1); |
71 qed "new_tv_FVar"; |
71 qed "new_tv_FVar"; |
72 |
72 |
73 goalw thy [new_tv_def] |
73 goalw thy [new_tv_def] |
74 "new_tv n (BVar m) = True"; |
74 "new_tv n (BVar m) = True"; |
75 by (Simp_tac 1); |
75 by (Simp_tac 1); |
76 qed "new_tv_BVar"; |
76 qed "new_tv_BVar"; |
77 |
77 |
78 goalw thy [new_tv_def] |
78 goalw thy [new_tv_def] |
79 "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
79 "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
80 by (fast_tac (HOL_cs addss !simpset) 1); |
80 by (fast_tac (HOL_cs addss simpset()) 1); |
81 qed "new_tv_Fun"; |
81 qed "new_tv_Fun"; |
82 |
82 |
83 goalw thy [new_tv_def] |
83 goalw thy [new_tv_def] |
84 "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)"; |
84 "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)"; |
85 by (fast_tac (HOL_cs addss !simpset) 1); |
85 by (fast_tac (HOL_cs addss simpset()) 1); |
86 qed "new_tv_Fun2"; |
86 qed "new_tv_Fun2"; |
87 |
87 |
88 goalw thy [new_tv_def] |
88 goalw thy [new_tv_def] |
89 "new_tv n []"; |
89 "new_tv n []"; |
90 by (Simp_tac 1); |
90 by (Simp_tac 1); |
91 qed "new_tv_Nil"; |
91 qed "new_tv_Nil"; |
92 |
92 |
93 goalw thy [new_tv_def] |
93 goalw thy [new_tv_def] |
94 "new_tv n (x#l) = (new_tv n x & new_tv n l)"; |
94 "new_tv n (x#l) = (new_tv n x & new_tv n l)"; |
95 by (fast_tac (HOL_cs addss !simpset) 1); |
95 by (fast_tac (HOL_cs addss simpset()) 1); |
96 qed "new_tv_Cons"; |
96 qed "new_tv_Cons"; |
97 |
97 |
98 goalw thy [new_tv_def] "!!n. new_tv n TVar"; |
98 goalw thy [new_tv_def] "!!n. new_tv n TVar"; |
99 by (strip_tac 1); |
99 by (strip_tac 1); |
100 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1); |
100 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1); |
101 qed "new_tv_TVar_subst"; |
101 qed "new_tv_TVar_subst"; |
102 |
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]; |
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 |
104 |
105 goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
105 goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
179 qed_spec_mp "typ_substitutions_only_on_free_variables"; |
179 qed_spec_mp "typ_substitutions_only_on_free_variables"; |
180 |
180 |
181 goal thy |
181 goal thy |
182 "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t"; |
182 "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t"; |
183 by (rtac typ_substitutions_only_on_free_variables 1); |
183 by (rtac typ_substitutions_only_on_free_variables 1); |
184 by (simp_tac (!simpset addsimps [Ball_def]) 1); |
184 by (simp_tac (simpset() addsimps [Ball_def]) 1); |
185 qed "eq_free_eq_subst_te"; |
185 qed "eq_free_eq_subst_te"; |
186 |
186 |
187 goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch"; |
187 goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch"; |
188 by (type_scheme.induct_tac "sch" 1); |
188 by (type_scheme.induct_tac "sch" 1); |
189 by (Simp_tac 1); |
189 by (Simp_tac 1); |
192 qed_spec_mp "scheme_substitutions_only_on_free_variables"; |
192 qed_spec_mp "scheme_substitutions_only_on_free_variables"; |
193 |
193 |
194 goal thy |
194 goal thy |
195 "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch"; |
195 "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch"; |
196 by (rtac scheme_substitutions_only_on_free_variables 1); |
196 by (rtac scheme_substitutions_only_on_free_variables 1); |
197 by (simp_tac (!simpset addsimps [Ball_def]) 1); |
197 by (simp_tac (simpset() addsimps [Ball_def]) 1); |
198 qed "eq_free_eq_subst_type_scheme"; |
198 qed "eq_free_eq_subst_type_scheme"; |
199 |
199 |
200 goal thy |
200 goal thy |
201 "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"; |
201 "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"; |
202 by (list.induct_tac "A" 1); |
202 by (list.induct_tac "A" 1); |
203 (* case [] *) |
203 (* case [] *) |
204 by (fast_tac (HOL_cs addss !simpset) 1); |
204 by (fast_tac (HOL_cs addss simpset()) 1); |
205 (* case x#xl *) |
205 (* case x#xl *) |
206 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (!simpset)) 1); |
206 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1); |
207 qed_spec_mp "eq_free_eq_subst_scheme_list"; |
207 qed_spec_mp "eq_free_eq_subst_scheme_list"; |
208 |
208 |
209 goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"; |
209 goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"; |
210 by (Fast_tac 1); |
210 by (Fast_tac 1); |
211 val weaken_asm_Un = result (); |
211 val weaken_asm_Un = result (); |
221 |
221 |
222 goal thy |
222 goal thy |
223 "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"; |
223 "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"; |
224 by (typ.induct_tac "t" 1); |
224 by (typ.induct_tac "t" 1); |
225 (* case TVar n *) |
225 (* case TVar n *) |
226 by (fast_tac (HOL_cs addss !simpset) 1); |
226 by (fast_tac (HOL_cs addss simpset()) 1); |
227 (* case Fun t1 t2 *) |
227 (* case Fun t1 t2 *) |
228 by (fast_tac (HOL_cs addss !simpset) 1); |
228 by (fast_tac (HOL_cs addss simpset()) 1); |
229 qed_spec_mp "eq_subst_te_eq_free"; |
229 qed_spec_mp "eq_subst_te_eq_free"; |
230 |
230 |
231 goal thy |
231 goal thy |
232 "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"; |
232 "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"; |
233 by (type_scheme.induct_tac "sch" 1); |
233 by (type_scheme.induct_tac "sch" 1); |
243 |
243 |
244 goal thy |
244 goal thy |
245 "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"; |
245 "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"; |
246 by (list.induct_tac "A" 1); |
246 by (list.induct_tac "A" 1); |
247 (* case [] *) |
247 (* case [] *) |
248 by (fast_tac (HOL_cs addss !simpset) 1); |
248 by (fast_tac (HOL_cs addss simpset()) 1); |
249 (* case x#xl *) |
249 (* case x#xl *) |
250 by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (!simpset)) 1); |
250 by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (simpset())) 1); |
251 qed_spec_mp "eq_subst_scheme_list_eq_free"; |
251 qed_spec_mp "eq_subst_scheme_list_eq_free"; |
252 |
252 |
253 goalw thy [free_tv_subst] |
253 goalw thy [free_tv_subst] |
254 "!!v. v : cod S ==> v : free_tv S"; |
254 "!!v. v : cod S ==> v : free_tv S"; |
255 by (fast_tac set_cs 1); |
255 by (fast_tac set_cs 1); |
276 Addsimps [cod_app_subst]; |
276 Addsimps [cod_app_subst]; |
277 |
277 |
278 goal thy |
278 goal thy |
279 "free_tv (S (v::nat)) <= insert v (cod S)"; |
279 "free_tv (S (v::nat)) <= insert v (cod S)"; |
280 by (expand_case_tac "v:dom S" 1); |
280 by (expand_case_tac "v:dom S" 1); |
281 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1); |
281 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1); |
282 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1); |
282 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1); |
283 qed "free_tv_subst_var"; |
283 qed "free_tv_subst_var"; |
284 |
284 |
285 goal thy |
285 goal thy |
286 "free_tv ($ S (t::typ)) <= cod S Un free_tv t"; |
286 "free_tv ($ S (t::typ)) <= cod S Un free_tv t"; |
287 by (typ.induct_tac "t" 1); |
287 by (typ.induct_tac "t" 1); |
288 (* case TVar n *) |
288 (* case TVar n *) |
289 by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
289 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); |
290 (* case Fun t1 t2 *) |
290 (* case Fun t1 t2 *) |
291 by (fast_tac (set_cs addss !simpset) 1); |
291 by (fast_tac (set_cs addss simpset()) 1); |
292 qed "free_tv_app_subst_te"; |
292 qed "free_tv_app_subst_te"; |
293 |
293 |
294 goal thy |
294 goal thy |
295 "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"; |
295 "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"; |
296 by (type_scheme.induct_tac "sch" 1); |
296 by (type_scheme.induct_tac "sch" 1); |
297 (* case FVar n *) |
297 (* case FVar n *) |
298 by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
298 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); |
299 (* case BVar n *) |
299 (* case BVar n *) |
300 by (Simp_tac 1); |
300 by (Simp_tac 1); |
301 (* case Fun t1 t2 *) |
301 (* case Fun t1 t2 *) |
302 by (fast_tac (set_cs addss !simpset) 1); |
302 by (fast_tac (set_cs addss simpset()) 1); |
303 qed "free_tv_app_subst_type_scheme"; |
303 qed "free_tv_app_subst_type_scheme"; |
304 |
304 |
305 goal thy |
305 goal thy |
306 "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"; |
306 "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"; |
307 by (list.induct_tac "A" 1); |
307 by (list.induct_tac "A" 1); |
308 (* case [] *) |
308 (* case [] *) |
309 by (Simp_tac 1); |
309 by (Simp_tac 1); |
310 (* case a#al *) |
310 (* case a#al *) |
311 by (cut_facts_tac [free_tv_app_subst_type_scheme] 1); |
311 by (cut_facts_tac [free_tv_app_subst_type_scheme] 1); |
312 by (fast_tac (set_cs addss !simpset) 1); |
312 by (fast_tac (set_cs addss simpset()) 1); |
313 qed "free_tv_app_subst_scheme_list"; |
313 qed "free_tv_app_subst_scheme_list"; |
314 |
314 |
315 goalw thy [free_tv_subst,dom_def] |
315 goalw thy [free_tv_subst,dom_def] |
316 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
316 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
317 \ free_tv s1 Un free_tv s2"; |
317 \ free_tv s1 Un free_tv s2"; |
318 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
318 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
319 free_tv_subst_var RS subsetD] |
319 free_tv_subst_var RS subsetD] |
320 addss (!simpset delsimps bex_simps |
320 addss (simpset() delsimps bex_simps |
321 addsimps [cod_def,dom_def])) 1); |
321 addsimps [cod_def,dom_def])) 1); |
322 qed "free_tv_comp_subst"; |
322 qed "free_tv_comp_subst"; |
323 |
323 |
324 goalw thy [o_def] |
324 goalw thy [o_def] |
325 "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)"; |
325 "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)"; |
343 |
343 |
344 goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)"; |
344 goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)"; |
345 by (list.induct_tac "A" 1); |
345 by (list.induct_tac "A" 1); |
346 by (Simp_tac 1); |
346 by (Simp_tac 1); |
347 by (Simp_tac 1); |
347 by (Simp_tac 1); |
348 by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_schemes]) 1); |
348 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1); |
349 qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists"; |
349 qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists"; |
350 |
350 |
351 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists]; |
351 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists]; |
352 |
352 |
353 goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)"; |
353 goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)"; |
354 by (type_scheme.induct_tac "sch" 1); |
354 by (type_scheme.induct_tac "sch" 1); |
355 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]))); |
355 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
356 by (strip_tac 1); |
356 by (strip_tac 1); |
357 by (Fast_tac 1); |
357 by (Fast_tac 1); |
358 qed "free_tv_ML_scheme"; |
358 qed "free_tv_ML_scheme"; |
359 |
359 |
360 goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)"; |
360 goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)"; |
361 by (list.induct_tac "A" 1); |
361 by (list.induct_tac "A" 1); |
362 by (Simp_tac 1); |
362 by (Simp_tac 1); |
363 by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme]) 1); |
363 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1); |
364 qed "free_tv_ML_scheme_list"; |
364 qed "free_tv_ML_scheme_list"; |
365 |
365 |
366 |
366 |
367 (* lemmata for bound_tv *) |
367 (* lemmata for bound_tv *) |
368 |
368 |
394 goalw thy [new_tv_def] |
394 goalw thy [new_tv_def] |
395 "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \ |
395 "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \ |
396 \ (! l. l < n --> new_tv n (S l) ))"; |
396 \ (! l. l < n --> new_tv n (S l) ))"; |
397 by (safe_tac HOL_cs ); |
397 by (safe_tac HOL_cs ); |
398 (* ==> *) |
398 (* ==> *) |
399 by (fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); |
399 by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1); |
400 by (subgoal_tac "m:cod S | S l = TVar l" 1); |
400 by (subgoal_tac "m:cod S | S l = TVar l" 1); |
401 by (safe_tac HOL_cs ); |
401 by (safe_tac HOL_cs ); |
402 by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); |
402 by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1); |
403 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
403 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
404 by (Asm_full_simp_tac 1); |
404 by (Asm_full_simp_tac 1); |
405 by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); |
405 by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1); |
406 (* <== *) |
406 (* <== *) |
407 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
407 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
408 by (safe_tac set_cs ); |
408 by (safe_tac set_cs ); |
409 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
409 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
410 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
410 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
421 |
421 |
422 (* substitution affects only variables occurring freely *) |
422 (* substitution affects only variables occurring freely *) |
423 goal thy |
423 goal thy |
424 "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"; |
424 "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"; |
425 by (typ.induct_tac "t" 1); |
425 by (typ.induct_tac "t" 1); |
426 by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]))); |
426 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
427 qed "subst_te_new_tv"; |
427 qed "subst_te_new_tv"; |
428 Addsimps [subst_te_new_tv]; |
428 Addsimps [subst_te_new_tv]; |
429 |
429 |
430 goal thy |
430 goal thy |
431 "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"; |
431 "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"; |
432 by (type_scheme.induct_tac "sch" 1); |
432 by (type_scheme.induct_tac "sch" 1); |
433 by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]))); |
433 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
434 qed_spec_mp "subst_te_new_type_scheme"; |
434 qed_spec_mp "subst_te_new_type_scheme"; |
435 Addsimps [subst_te_new_type_scheme]; |
435 Addsimps [subst_te_new_type_scheme]; |
436 |
436 |
437 goal thy |
437 goal thy |
438 "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"; |
438 "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"; |
442 Addsimps [subst_tel_new_scheme_list]; |
442 Addsimps [subst_tel_new_scheme_list]; |
443 |
443 |
444 (* all greater variables are also new *) |
444 (* all greater variables are also new *) |
445 goalw thy [new_tv_def] |
445 goalw thy [new_tv_def] |
446 "!!n m. n<=m ==> new_tv n t ==> new_tv m t"; |
446 "!!n m. n<=m ==> new_tv n t ==> new_tv m t"; |
447 by (safe_tac (!claset)); |
447 by (safe_tac (claset())); |
448 by (dtac spec 1); |
448 by (dtac spec 1); |
449 by (mp_tac 1); |
449 by (mp_tac 1); |
450 by (trans_tac 1); |
450 by (trans_tac 1); |
451 qed "new_tv_le"; |
451 qed "new_tv_le"; |
452 Addsimps [lessI RS less_imp_le RS new_tv_le]; |
452 Addsimps [lessI RS less_imp_le RS new_tv_le]; |
453 |
453 |
454 goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t"; |
454 goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t"; |
455 by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1); |
455 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
456 qed "new_tv_typ_le"; |
456 qed "new_tv_typ_le"; |
457 |
457 |
458 goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A"; |
458 goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A"; |
459 by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1); |
459 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
460 qed "new_scheme_list_le"; |
460 qed "new_scheme_list_le"; |
461 |
461 |
462 goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S"; |
462 goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S"; |
463 by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1); |
463 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1); |
464 qed "new_tv_subst_le"; |
464 qed "new_tv_subst_le"; |
465 |
465 |
466 (* new_tv property remains if a substitution is applied *) |
466 (* new_tv property remains if a substitution is applied *) |
467 goal thy |
467 goal thy |
468 "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"; |
468 "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"; |
469 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
469 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
470 qed "new_tv_subst_var"; |
470 qed "new_tv_subst_var"; |
471 |
471 |
472 goal thy |
472 goal thy |
473 "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"; |
473 "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"; |
474 by (typ.induct_tac "t" 1); |
474 by (typ.induct_tac "t" 1); |
475 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
475 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
476 qed_spec_mp "new_tv_subst_te"; |
476 qed_spec_mp "new_tv_subst_te"; |
477 Addsimps [new_tv_subst_te]; |
477 Addsimps [new_tv_subst_te]; |
478 |
478 |
479 goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)"; |
479 goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)"; |
480 by (type_scheme.induct_tac "sch" 1); |
480 by (type_scheme.induct_tac "sch" 1); |
481 by (ALLGOALS (Asm_full_simp_tac)); |
481 by (ALLGOALS (Asm_full_simp_tac)); |
482 by (rewtac new_tv_def); |
482 by (rewtac new_tv_def); |
483 by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1); |
483 by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1); |
484 by (strip_tac 1); |
484 by (strip_tac 1); |
485 by (case_tac "S nat = TVar nat" 1); |
485 by (case_tac "S nat = TVar nat" 1); |
486 by (rotate_tac 3 1); |
486 by (rotate_tac 3 1); |
487 by (Asm_full_simp_tac 1); |
487 by (Asm_full_simp_tac 1); |
488 by (dres_inst_tac [("x","m")] spec 1); |
488 by (dres_inst_tac [("x","m")] spec 1); |
491 Addsimps [new_tv_subst_type_scheme]; |
491 Addsimps [new_tv_subst_type_scheme]; |
492 |
492 |
493 goal thy |
493 goal thy |
494 "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"; |
494 "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"; |
495 by (list.induct_tac "A" 1); |
495 by (list.induct_tac "A" 1); |
496 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset)))); |
496 by (ALLGOALS(fast_tac (HOL_cs addss (simpset())))); |
497 qed_spec_mp "new_tv_subst_scheme_list"; |
497 qed_spec_mp "new_tv_subst_scheme_list"; |
498 Addsimps [new_tv_subst_scheme_list]; |
498 Addsimps [new_tv_subst_scheme_list]; |
499 |
499 |
500 goal thy |
500 goal thy |
501 "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"; |
501 "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"; |
502 by (simp_tac (!simpset addsimps [new_tv_list]) 1); |
502 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
503 by (list.induct_tac "A" 1); |
503 by (list.induct_tac "A" 1); |
504 by (ALLGOALS Asm_full_simp_tac); |
504 by (ALLGOALS Asm_full_simp_tac); |
505 qed "new_tv_Suc_list"; |
505 qed "new_tv_Suc_list"; |
506 |
506 |
507 goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')"; |
507 goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')"; |
525 |
525 |
526 (* composition of substitutions preserves new_tv proposition *) |
526 (* composition of substitutions preserves new_tv proposition *) |
527 goal thy |
527 goal thy |
528 "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \ |
528 "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \ |
529 \ new_tv n (($ R) o S)"; |
529 \ new_tv n (($ R) o S)"; |
530 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
530 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
531 qed "new_tv_subst_comp_1"; |
531 qed "new_tv_subst_comp_1"; |
532 |
532 |
533 goal thy |
533 goal thy |
534 "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \ |
534 "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \ |
535 \ new_tv n (%v.$ R (S v))"; |
535 \ new_tv n (%v.$ R (S v))"; |
536 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
536 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
537 qed "new_tv_subst_comp_2"; |
537 qed "new_tv_subst_comp_2"; |
538 |
538 |
539 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
539 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
540 |
540 |
541 (* new type variables do not occur freely in a type structure *) |
541 (* new type variables do not occur freely in a type structure *) |
544 by (fast_tac (HOL_cs addEs [less_irrefl]) 1); |
544 by (fast_tac (HOL_cs addEs [less_irrefl]) 1); |
545 qed "new_tv_not_free_tv"; |
545 qed "new_tv_not_free_tv"; |
546 Addsimps [new_tv_not_free_tv]; |
546 Addsimps [new_tv_not_free_tv]; |
547 |
547 |
548 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'"; |
548 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'"; |
549 by (simp_tac (!simpset addsplits [expand_if]) 1); |
549 by (simp_tac (simpset() addsplits [expand_if]) 1); |
550 by (safe_tac (!claset)); |
550 by (safe_tac (claset())); |
551 by (trans_tac 1); |
551 by (trans_tac 1); |
552 qed "less_maxL"; |
552 qed "less_maxL"; |
553 |
553 |
554 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'"; |
554 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'"; |
555 by (simp_tac (!simpset addsplits [expand_if]) 1); |
555 by (simp_tac (simpset() addsplits [expand_if]) 1); |
556 by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1); |
556 by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1); |
557 val less_maxR = result(); |
557 val less_maxR = result(); |
558 |
558 |
559 goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)"; |
559 goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)"; |
560 by (typ.induct_tac "t" 1); |
560 by (typ.induct_tac "t" 1); |
561 by (res_inst_tac [("x","Suc nat")] exI 1); |
561 by (res_inst_tac [("x","Suc nat")] exI 1); |
562 by (Asm_simp_tac 1); |
562 by (Asm_simp_tac 1); |
563 by (REPEAT (etac exE 1)); |
563 by (REPEAT (etac exE 1)); |
564 by (rename_tac "n'" 1); |
564 by (rename_tac "n'" 1); |
565 by (res_inst_tac [("x","max n n'")] exI 1); |
565 by (res_inst_tac [("x","max n n'")] exI 1); |
566 by (Simp_tac 1); |
566 by (Simp_tac 1); |
567 by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1); |
567 by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1); |
568 qed "fresh_variable_types"; |
568 qed "fresh_variable_types"; |
569 |
569 |
570 Addsimps [fresh_variable_types]; |
570 Addsimps [fresh_variable_types]; |
571 |
571 |
572 goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)"; |
572 goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)"; |
577 by (Simp_tac 1); |
577 by (Simp_tac 1); |
578 by (REPEAT (etac exE 1)); |
578 by (REPEAT (etac exE 1)); |
579 by (rename_tac "n'" 1); |
579 by (rename_tac "n'" 1); |
580 by (res_inst_tac [("x","max n n'")] exI 1); |
580 by (res_inst_tac [("x","max n n'")] exI 1); |
581 by (Simp_tac 1); |
581 by (Simp_tac 1); |
582 by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1); |
582 by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1); |
583 qed "fresh_variable_type_schemes"; |
583 qed "fresh_variable_type_schemes"; |
584 |
584 |
585 Addsimps [fresh_variable_type_schemes]; |
585 Addsimps [fresh_variable_type_schemes]; |
586 |
586 |
587 goalw thy [max_def] "!!n::nat. n <= (max n n')"; |
587 goalw thy [max_def] "!!n::nat. n <= (max n n')"; |
588 by (simp_tac (!simpset addsplits [expand_if]) 1); |
588 by (simp_tac (simpset() addsplits [expand_if]) 1); |
589 val le_maxL = result(); |
589 val le_maxL = result(); |
590 |
590 |
591 goalw thy [max_def] "!!n'::nat. n' <= (max n n')"; |
591 goalw thy [max_def] "!!n'::nat. n' <= (max n n')"; |
592 by (simp_tac (!simpset addsplits [expand_if]) 1); |
592 by (simp_tac (simpset() addsplits [expand_if]) 1); |
593 by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1); |
593 by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1); |
594 val le_maxR = result(); |
594 val le_maxR = result(); |
595 |
595 |
596 goal thy "!!A::type_scheme list. ? n. (new_tv n A)"; |
596 goal thy "!!A::type_scheme list. ? n. (new_tv n A)"; |
597 by (list.induct_tac "A" 1); |
597 by (list.induct_tac "A" 1); |
598 by (Simp_tac 1); |
598 by (Simp_tac 1); |
602 by (etac exE 1); |
602 by (etac exE 1); |
603 by (rename_tac "n'" 1); |
603 by (rename_tac "n'" 1); |
604 by (res_inst_tac [("x","(max n n')")] exI 1); |
604 by (res_inst_tac [("x","(max n n')")] exI 1); |
605 by (subgoal_tac "n <= (max n n')" 1); |
605 by (subgoal_tac "n <= (max n n')" 1); |
606 by (subgoal_tac "n' <= (max n n')" 1); |
606 by (subgoal_tac "n' <= (max n n')" 1); |
607 by (fast_tac (!claset addDs [new_tv_le]) 1); |
607 by (fast_tac (claset() addDs [new_tv_le]) 1); |
608 by (ALLGOALS (simp_tac (!simpset addsimps [le_maxR,le_maxL]))); |
608 by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL]))); |
609 qed "fresh_variable_type_scheme_lists"; |
609 qed "fresh_variable_type_scheme_lists"; |
610 |
610 |
611 Addsimps [fresh_variable_type_scheme_lists]; |
611 Addsimps [fresh_variable_type_scheme_lists]; |
612 |
612 |
613 goal thy "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)"; |
613 goal thy "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)"; |
614 by (REPEAT (etac exE 1)); |
614 by (REPEAT (etac exE 1)); |
615 by (rename_tac "n1 n2" 1); |
615 by (rename_tac "n1 n2" 1); |
616 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
616 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
617 by (subgoal_tac "n1 <= max n1 n2" 1); |
617 by (subgoal_tac "n1 <= max n1 n2" 1); |
618 by (subgoal_tac "n2 <= max n1 n2" 1); |
618 by (subgoal_tac "n2 <= max n1 n2" 1); |
619 by (fast_tac (!claset addDs [new_tv_le]) 1); |
619 by (fast_tac (claset() addDs [new_tv_le]) 1); |
620 by (ALLGOALS (simp_tac (!simpset addsimps [le_maxL,le_maxR]))); |
620 by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR]))); |
621 qed "make_one_new_out_of_two"; |
621 qed "make_one_new_out_of_two"; |
622 |
622 |
623 goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \ |
623 goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \ |
624 \ ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ; |
624 \ ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ; |
625 by (cut_inst_tac [("t","t")] fresh_variable_types 1); |
625 by (cut_inst_tac [("t","t")] fresh_variable_types 1); |
635 by (thin_tac "? n. new_tv n A'" 1); |
635 by (thin_tac "? n. new_tv n A'" 1); |
636 by (REPEAT (etac exE 1)); |
636 by (REPEAT (etac exE 1)); |
637 by (rename_tac "n2 n1" 1); |
637 by (rename_tac "n2 n1" 1); |
638 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
638 by (res_inst_tac [("x","(max n1 n2)")] exI 1); |
639 by (rewtac new_tv_def); |
639 by (rewtac new_tv_def); |
640 by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1); |
640 by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1); |
641 qed "ex_fresh_variable"; |
641 qed "ex_fresh_variable"; |
642 |
642 |
643 (* mgu does not introduce new type variables *) |
643 (* mgu does not introduce new type variables *) |
644 goalw thy [new_tv_def] |
644 goalw thy [new_tv_def] |
645 "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \ |
645 "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \ |
663 |
663 |
664 Addsimps [subst_TVar_scheme]; |
664 Addsimps [subst_TVar_scheme]; |
665 |
665 |
666 goal thy "!!A::type_scheme list. $ TVar A = A"; |
666 goal thy "!!A::type_scheme list. $ TVar A = A"; |
667 by (rtac list.induct 1); |
667 by (rtac list.induct 1); |
668 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [app_subst_list]))); |
668 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list]))); |
669 qed "subst_TVar_scheme_list"; |
669 qed "subst_TVar_scheme_list"; |
670 |
670 |
671 Addsimps [subst_TVar_scheme_list]; |
671 Addsimps [subst_TVar_scheme_list]; |
672 |
672 |
673 (* application of id_subst does not change type expression *) |
673 (* application of id_subst does not change type expression *) |
696 qed "app_subst_id_tel"; |
696 qed "app_subst_id_tel"; |
697 Addsimps [app_subst_id_tel]; |
697 Addsimps [app_subst_id_tel]; |
698 |
698 |
699 goal thy "!!sch::type_scheme. $ id_subst sch = sch"; |
699 goal thy "!!sch::type_scheme. $ id_subst sch = sch"; |
700 by (type_scheme.induct_tac "sch" 1); |
700 by (type_scheme.induct_tac "sch" 1); |
701 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [id_subst_def]))); |
701 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def]))); |
702 qed "id_subst_sch"; |
702 qed "id_subst_sch"; |
703 |
703 |
704 Addsimps [id_subst_sch]; |
704 Addsimps [id_subst_sch]; |
705 |
705 |
706 goal thy "!!A::type_scheme list. $ id_subst A = A"; |
706 goal thy "!!A::type_scheme list. $ id_subst A = A"; |
734 "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"; |
734 "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"; |
735 by (list.induct_tac "A" 1); |
735 by (list.induct_tac "A" 1); |
736 (* case [] *) |
736 (* case [] *) |
737 by (Simp_tac 1); |
737 by (Simp_tac 1); |
738 (* case x#xl *) |
738 (* case x#xl *) |
739 by (asm_full_simp_tac (!simpset addsimps [subst_comp_type_scheme]) 1); |
739 by (asm_full_simp_tac (simpset() addsimps [subst_comp_type_scheme]) 1); |
740 qed "subst_comp_scheme_list"; |
740 qed "subst_comp_scheme_list"; |
741 |
741 |
742 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A"; |
742 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A"; |
743 by (rtac scheme_list_substitutions_only_on_free_variables 1); |
743 by (rtac scheme_list_substitutions_only_on_free_variables 1); |
744 by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1); |
744 by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1); |
745 qed "subst_id_on_type_scheme_list'"; |
745 qed "subst_id_on_type_scheme_list'"; |
746 |
746 |
747 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"; |
747 goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"; |
748 by (stac subst_id_on_type_scheme_list' 1); |
748 by (stac subst_id_on_type_scheme_list' 1); |
749 by (assume_tac 1); |
749 by (assume_tac 1); |