144 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
144 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
145 by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
145 by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
146 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
146 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
147 qed "new_tv_subst"; |
147 qed "new_tv_subst"; |
148 |
148 |
149 Goal |
149 Goal "new_tv n x = list_all (new_tv n) x"; |
150 "new_tv n = list_all (new_tv n)"; |
|
151 by (rtac ext 1); |
|
152 by (induct_tac "x" 1); |
150 by (induct_tac "x" 1); |
153 by (ALLGOALS Asm_simp_tac); |
151 by (ALLGOALS Asm_simp_tac); |
154 qed "new_tv_list"; |
152 qed "new_tv_list"; |
155 |
153 |
156 (* substitution affects only variables occurring freely *) |
154 (* substitution affects only variables occurring freely *) |
205 Goal |
203 Goal |
206 "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)"; |
204 "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)"; |
207 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
205 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
208 qed "new_tv_subst_var"; |
206 qed "new_tv_subst_var"; |
209 |
207 |
210 Goal |
208 Goal "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)"; |
211 "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)"; |
|
212 by (induct_tac "t" 1); |
209 by (induct_tac "t" 1); |
213 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
210 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
214 qed_spec_mp "new_tv_subst_te"; |
211 qed_spec_mp "new_tv_subst_te"; |
215 Addsimps [new_tv_subst_te]; |
212 Addsimps [new_tv_subst_te]; |
216 |
213 |
217 Goal |
214 Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; |
218 "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; |
|
219 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
215 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
220 by (induct_tac "ts" 1); |
216 by (induct_tac "ts" 1); |
221 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
217 by (Safe_tac); |
|
218 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
222 qed_spec_mp "new_tv_subst_tel"; |
219 qed_spec_mp "new_tv_subst_tel"; |
223 Addsimps [new_tv_subst_tel]; |
220 Addsimps [new_tv_subst_tel]; |
224 |
221 |
225 (* auxilliary lemma *) |
222 (* auxilliary lemma *) |
226 Goal |
223 Goal "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; |
227 "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; |
|
228 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
224 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
229 by (induct_tac "ts" 1); |
|
230 by (ALLGOALS Asm_full_simp_tac); |
|
231 qed "new_tv_Suc_list"; |
225 qed "new_tv_Suc_list"; |
232 |
226 |
233 |
227 |
234 (* composition of substitutions preserves new_tv proposition *) |
228 (* composition of substitutions preserves new_tv proposition *) |
235 Goal |
229 Goal |