115 |
115 |
116 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
116 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
117 |
117 |
118 goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
118 goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
119 "new_tv n id_subst"; |
119 "new_tv n id_subst"; |
120 by(Simp_tac 1); |
120 by (Simp_tac 1); |
121 qed "new_tv_id_subst"; |
121 qed "new_tv_id_subst"; |
122 Addsimps[new_tv_id_subst]; |
122 Addsimps[new_tv_id_subst]; |
123 |
123 |
124 goalw thy [new_tv_def] |
124 goalw thy [new_tv_def] |
125 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
125 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
126 \ (! l. l < n --> new_tv n (s l) ))"; |
126 \ (! l. l < n --> new_tv n (s l) ))"; |
127 by( safe_tac HOL_cs ); |
127 by ( safe_tac HOL_cs ); |
128 (* ==> *) |
128 (* ==> *) |
129 by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); |
129 by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); |
130 by( subgoal_tac "m:cod s | s l = TVar l" 1); |
130 by ( subgoal_tac "m:cod s | s l = TVar l" 1); |
131 by( safe_tac HOL_cs ); |
131 by ( safe_tac HOL_cs ); |
132 by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); |
132 by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); |
133 by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
133 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
134 by(Asm_full_simp_tac 1); |
134 by (Asm_full_simp_tac 1); |
135 by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); |
135 by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); |
136 (* <== *) |
136 (* <== *) |
137 by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
137 by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
138 by( safe_tac set_cs ); |
138 by ( safe_tac set_cs ); |
139 by( cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
139 by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
140 by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
140 by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
141 by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
141 by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
142 by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
142 by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
143 qed "new_tv_subst"; |
143 qed "new_tv_subst"; |
144 |
144 |
145 goal thy |
145 goal thy |
146 "new_tv n = list_all (new_tv n)"; |
146 "new_tv n = list_all (new_tv n)"; |
147 by (rtac ext 1); |
147 by (rtac ext 1); |
148 by(list.induct_tac "x" 1); |
148 by (list.induct_tac "x" 1); |
149 by(ALLGOALS Asm_simp_tac); |
149 by (ALLGOALS Asm_simp_tac); |
150 qed "new_tv_list"; |
150 qed "new_tv_list"; |
151 |
151 |
152 (* substitution affects only variables occurring freely *) |
152 (* substitution affects only variables occurring freely *) |
153 goal thy |
153 goal thy |
154 "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t"; |
154 "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t"; |
167 (* all greater variables are also new *) |
167 (* all greater variables are also new *) |
168 goal thy |
168 goal thy |
169 "n<=m --> new_tv n (t::typ) --> new_tv m t"; |
169 "n<=m --> new_tv n (t::typ) --> new_tv m t"; |
170 by (typ.induct_tac "t" 1); |
170 by (typ.induct_tac "t" 1); |
171 (* case TVar n *) |
171 (* case TVar n *) |
172 by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1); |
172 by ( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1); |
173 (* case Fun t1 t2 *) |
173 (* case Fun t1 t2 *) |
174 by (Asm_simp_tac 1); |
174 by (Asm_simp_tac 1); |
175 qed_spec_mp "new_tv_le"; |
175 qed_spec_mp "new_tv_le"; |
176 Addsimps [lessI RS less_imp_le RS new_tv_le]; |
176 Addsimps [lessI RS less_imp_le RS new_tv_le]; |
177 |
177 |
178 goal thy |
178 goal thy |
179 "n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; |
179 "n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; |
180 by( list.induct_tac "ts" 1); |
180 by ( list.induct_tac "ts" 1); |
181 (* case [] *) |
181 (* case [] *) |
182 by(Simp_tac 1); |
182 by (Simp_tac 1); |
183 (* case a#al *) |
183 (* case a#al *) |
184 by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1); |
184 by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1); |
185 qed_spec_mp "new_tv_list_le"; |
185 qed_spec_mp "new_tv_list_le"; |
186 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
186 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
187 |
187 |
210 qed_spec_mp "new_tv_subst_te"; |
210 qed_spec_mp "new_tv_subst_te"; |
211 Addsimps [new_tv_subst_te]; |
211 Addsimps [new_tv_subst_te]; |
212 |
212 |
213 goal thy |
213 goal thy |
214 "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; |
214 "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; |
215 by( simp_tac (!simpset addsimps [new_tv_list]) 1); |
215 by ( simp_tac (!simpset addsimps [new_tv_list]) 1); |
216 by (list.induct_tac "ts" 1); |
216 by (list.induct_tac "ts" 1); |
217 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
217 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
218 qed_spec_mp "new_tv_subst_tel"; |
218 qed_spec_mp "new_tv_subst_tel"; |
219 Addsimps [new_tv_subst_tel]; |
219 Addsimps [new_tv_subst_tel]; |
220 |
220 |
221 (* auxilliary lemma *) |
221 (* auxilliary lemma *) |
222 goal thy |
222 goal thy |
223 "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; |
223 "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; |
224 by( simp_tac (!simpset addsimps [new_tv_list]) 1); |
224 by ( simp_tac (!simpset addsimps [new_tv_list]) 1); |
225 by (list.induct_tac "ts" 1); |
225 by (list.induct_tac "ts" 1); |
226 by (ALLGOALS Asm_full_simp_tac); |
226 by (ALLGOALS Asm_full_simp_tac); |
227 qed "new_tv_Suc_list"; |
227 qed "new_tv_Suc_list"; |
228 |
228 |
229 |
229 |
300 qed_spec_mp "eq_free_eq_subst_tel"; |
300 qed_spec_mp "eq_free_eq_subst_tel"; |
301 |
301 |
302 (* some useful theorems *) |
302 (* some useful theorems *) |
303 goalw thy [free_tv_subst] |
303 goalw thy [free_tv_subst] |
304 "!!v. v : cod s ==> v : free_tv s"; |
304 "!!v. v : cod s ==> v : free_tv s"; |
305 by( fast_tac set_cs 1); |
305 by ( fast_tac set_cs 1); |
306 qed "codD"; |
306 qed "codD"; |
307 |
307 |
308 goalw thy [free_tv_subst,dom_def] |
308 goalw thy [free_tv_subst,dom_def] |
309 "!! x. x ~: free_tv s ==> s x = TVar x"; |
309 "!! x. x ~: free_tv s ==> s x = TVar x"; |
310 by( fast_tac set_cs 1); |
310 by ( fast_tac set_cs 1); |
311 qed "not_free_impl_id"; |
311 qed "not_free_impl_id"; |
312 |
312 |
313 goalw thy [new_tv_def] |
313 goalw thy [new_tv_def] |
314 "!! n. [| new_tv n t; m:free_tv t |] ==> m<n"; |
314 "!! n. [| new_tv n t; m:free_tv t |] ==> m<n"; |
315 by( fast_tac HOL_cs 1 ); |
315 by ( fast_tac HOL_cs 1 ); |
316 qed "free_tv_le_new_tv"; |
316 qed "free_tv_le_new_tv"; |
317 |
317 |
318 goal thy |
318 goal thy |
319 "free_tv (s (v::nat)) <= cod s Un {v}"; |
319 "free_tv (s (v::nat)) <= cod s Un {v}"; |
320 by( cut_inst_tac [("P","v:dom s")] excluded_middle 1); |
320 by ( cut_inst_tac [("P","v:dom s")] excluded_middle 1); |
321 by( safe_tac (HOL_cs addSIs [subsetI]) ); |
321 by ( safe_tac (HOL_cs addSIs [subsetI]) ); |
322 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1); |
322 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1); |
323 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1); |
323 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1); |
324 qed "free_tv_subst_var"; |
324 qed "free_tv_subst_var"; |
325 |
325 |
326 goal thy |
326 goal thy |
327 "free_tv ($ s (t::typ)) <= cod s Un free_tv t"; |
327 "free_tv ($ s (t::typ)) <= cod s Un free_tv t"; |
328 by( typ.induct_tac "t" 1); |
328 by ( typ.induct_tac "t" 1); |
329 (* case TVar n *) |
329 (* case TVar n *) |
330 by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
330 by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
331 (* case Fun t1 t2 *) |
331 (* case Fun t1 t2 *) |
332 by( fast_tac (set_cs addss !simpset) 1); |
332 by ( fast_tac (set_cs addss !simpset) 1); |
333 qed "free_tv_app_subst_te"; |
333 qed "free_tv_app_subst_te"; |
334 |
334 |
335 goal thy |
335 goal thy |
336 "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts"; |
336 "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts"; |
337 by( list.induct_tac "ts" 1); |
337 by ( list.induct_tac "ts" 1); |
338 (* case [] *) |
338 (* case [] *) |
339 by (Simp_tac 1); |
339 by (Simp_tac 1); |
340 (* case a#al *) |
340 (* case a#al *) |
341 by( cut_facts_tac [free_tv_app_subst_te] 1); |
341 by ( cut_facts_tac [free_tv_app_subst_te] 1); |
342 by( fast_tac (set_cs addss !simpset) 1); |
342 by ( fast_tac (set_cs addss !simpset) 1); |
343 qed "free_tv_app_subst_tel"; |
343 qed "free_tv_app_subst_tel"; |
344 |
344 |
345 goalw thy [free_tv_subst,dom_def] |
345 goalw thy [free_tv_subst,dom_def] |
346 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
346 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
347 \ free_tv s1 Un free_tv s2"; |
347 \ free_tv s1 Un free_tv s2"; |
348 by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS |
348 by ( fast_tac (set_cs addSDs [free_tv_app_subst_te RS |
349 subsetD,free_tv_subst_var RS subsetD] addss ( |
349 subsetD,free_tv_subst_var RS subsetD] addss ( |
350 !simpset addsimps [cod_def,dom_def])) 1); |
350 !simpset addsimps [cod_def,dom_def])) 1); |
351 qed "free_tv_comp_subst"; |
351 qed "free_tv_comp_subst"; |
352 |
352 |