97 Addsimps [app_subst_Nil,app_subst_Cons]; |
97 Addsimps [app_subst_Nil,app_subst_Cons]; |
98 |
98 |
99 (* constructor laws for new_tv *) |
99 (* constructor laws for new_tv *) |
100 goalw thy [new_tv_def] |
100 goalw thy [new_tv_def] |
101 "new_tv n (TVar m) = (m<n)"; |
101 "new_tv n (TVar m) = (m<n)"; |
102 by (fast_tac (HOL_cs addss !simpset) 1); |
102 by (fast_tac (HOL_cs addss simpset()) 1); |
103 qed "new_tv_TVar"; |
103 qed "new_tv_TVar"; |
104 |
104 |
105 goalw thy [new_tv_def] |
105 goalw thy [new_tv_def] |
106 "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
106 "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
107 by (fast_tac (HOL_cs addss !simpset) 1); |
107 by (fast_tac (HOL_cs addss simpset()) 1); |
108 qed "new_tv_Fun"; |
108 qed "new_tv_Fun"; |
109 |
109 |
110 goalw thy [new_tv_def] |
110 goalw thy [new_tv_def] |
111 "new_tv n []"; |
111 "new_tv n []"; |
112 by (Simp_tac 1); |
112 by (Simp_tac 1); |
113 qed "new_tv_Nil"; |
113 qed "new_tv_Nil"; |
114 |
114 |
115 goalw thy [new_tv_def] |
115 goalw thy [new_tv_def] |
116 "new_tv n (t#ts) = (new_tv n t & new_tv n ts)"; |
116 "new_tv n (t#ts) = (new_tv n t & new_tv n ts)"; |
117 by (fast_tac (HOL_cs addss !simpset) 1); |
117 by (fast_tac (HOL_cs addss simpset()) 1); |
118 qed "new_tv_Cons"; |
118 qed "new_tv_Cons"; |
119 |
119 |
120 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
120 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
121 |
121 |
122 goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
122 goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
128 goalw thy [new_tv_def] |
128 goalw thy [new_tv_def] |
129 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
129 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
130 \ (! l. l < n --> new_tv n (s l) ))"; |
130 \ (! l. l < n --> new_tv n (s l) ))"; |
131 by (safe_tac HOL_cs ); |
131 by (safe_tac HOL_cs ); |
132 (* ==> *) |
132 (* ==> *) |
133 by (fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); |
133 by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1); |
134 by (subgoal_tac "m:cod s | s l = TVar l" 1); |
134 by (subgoal_tac "m:cod s | s l = TVar l" 1); |
135 by (safe_tac HOL_cs ); |
135 by (safe_tac HOL_cs ); |
136 by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); |
136 by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1); |
137 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
137 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
138 by (Asm_full_simp_tac 1); |
138 by (Asm_full_simp_tac 1); |
139 by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); |
139 by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1); |
140 (* <== *) |
140 (* <== *) |
141 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
141 by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
142 by (safe_tac set_cs ); |
142 by (safe_tac set_cs ); |
143 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
143 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
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); |
183 "n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; |
183 "n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; |
184 by (list.induct_tac "ts" 1); |
184 by (list.induct_tac "ts" 1); |
185 (* case [] *) |
185 (* case [] *) |
186 by (Simp_tac 1); |
186 by (Simp_tac 1); |
187 (* case a#al *) |
187 (* case a#al *) |
188 by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1); |
188 by (fast_tac (HOL_cs addIs [new_tv_le] addss simpset()) 1); |
189 qed_spec_mp "new_tv_list_le"; |
189 qed_spec_mp "new_tv_list_le"; |
190 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
190 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
191 |
191 |
192 goal thy |
192 goal thy |
193 "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s"; |
193 "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s"; |
194 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
194 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
195 by (rtac conjI 1); |
195 by (rtac conjI 1); |
196 by (slow_tac (HOL_cs addIs [le_trans]) 1); |
196 by (slow_tac (HOL_cs addIs [le_trans]) 1); |
197 by (safe_tac HOL_cs ); |
197 by (safe_tac HOL_cs ); |
198 by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1); |
198 by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1); |
199 by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1); |
199 by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1); |
200 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [new_tv_le])) ); |
200 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) ); |
201 qed "new_tv_subst_le"; |
201 qed "new_tv_subst_le"; |
202 Addsimps [lessI RS less_imp_le RS new_tv_subst_le]; |
202 Addsimps [lessI RS less_imp_le RS new_tv_subst_le]; |
203 |
203 |
204 (* new_tv property remains if a substitution is applied *) |
204 (* new_tv property remains if a substitution is applied *) |
205 goal thy |
205 goal thy |
206 "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)"; |
206 "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)"; |
207 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
207 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
208 qed "new_tv_subst_var"; |
208 qed "new_tv_subst_var"; |
209 |
209 |
210 goal thy |
210 goal thy |
211 "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 (typ.induct_tac "t" 1); |
212 by (typ.induct_tac "t" 1); |
213 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
213 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
214 qed_spec_mp "new_tv_subst_te"; |
214 qed_spec_mp "new_tv_subst_te"; |
215 Addsimps [new_tv_subst_te]; |
215 Addsimps [new_tv_subst_te]; |
216 |
216 |
217 goal thy |
217 goal thy |
218 "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); |
219 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
220 by (list.induct_tac "ts" 1); |
220 by (list.induct_tac "ts" 1); |
221 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
221 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])))); |
222 qed_spec_mp "new_tv_subst_tel"; |
222 qed_spec_mp "new_tv_subst_tel"; |
223 Addsimps [new_tv_subst_tel]; |
223 Addsimps [new_tv_subst_tel]; |
224 |
224 |
225 (* auxilliary lemma *) |
225 (* auxilliary lemma *) |
226 goal thy |
226 goal thy |
227 "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); |
228 by (simp_tac (simpset() addsimps [new_tv_list]) 1); |
229 by (list.induct_tac "ts" 1); |
229 by (list.induct_tac "ts" 1); |
230 by (ALLGOALS Asm_full_simp_tac); |
230 by (ALLGOALS Asm_full_simp_tac); |
231 qed "new_tv_Suc_list"; |
231 qed "new_tv_Suc_list"; |
232 |
232 |
233 |
233 |
234 (* composition of substitutions preserves new_tv proposition *) |
234 (* composition of substitutions preserves new_tv proposition *) |
235 goal thy |
235 goal thy |
236 "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
236 "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
237 \ new_tv n (($ r) o s)"; |
237 \ new_tv n (($ r) o s)"; |
238 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
238 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
239 qed "new_tv_subst_comp_1"; |
239 qed "new_tv_subst_comp_1"; |
240 |
240 |
241 goal thy |
241 goal thy |
242 "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
242 "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
243 \ new_tv n (%v.$ r (s v))"; |
243 \ new_tv n (%v.$ r (s v))"; |
244 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
244 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
245 qed "new_tv_subst_comp_2"; |
245 qed "new_tv_subst_comp_2"; |
246 |
246 |
247 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
247 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
248 |
248 |
249 (* new type variables do not occur freely in a type structure *) |
249 (* new type variables do not occur freely in a type structure *) |
269 occurring in the type structure *) |
269 occurring in the type structure *) |
270 goal thy |
270 goal thy |
271 "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n"; |
271 "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n"; |
272 by (typ.induct_tac "t" 1); |
272 by (typ.induct_tac "t" 1); |
273 (* case TVar n *) |
273 (* case TVar n *) |
274 by (fast_tac (HOL_cs addss !simpset) 1); |
274 by (fast_tac (HOL_cs addss simpset()) 1); |
275 (* case Fun t1 t2 *) |
275 (* case Fun t1 t2 *) |
276 by (fast_tac (HOL_cs addss !simpset) 1); |
276 by (fast_tac (HOL_cs addss simpset()) 1); |
277 qed_spec_mp "eq_subst_te_eq_free"; |
277 qed_spec_mp "eq_subst_te_eq_free"; |
278 |
278 |
279 goal thy |
279 goal thy |
280 "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t"; |
280 "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t"; |
281 by (typ.induct_tac "t" 1); |
281 by (typ.induct_tac "t" 1); |
282 (* case TVar n *) |
282 (* case TVar n *) |
283 by (fast_tac (HOL_cs addss !simpset) 1); |
283 by (fast_tac (HOL_cs addss simpset()) 1); |
284 (* case Fun t1 t2 *) |
284 (* case Fun t1 t2 *) |
285 by (fast_tac (HOL_cs addss !simpset) 1); |
285 by (fast_tac (HOL_cs addss simpset()) 1); |
286 qed_spec_mp "eq_free_eq_subst_te"; |
286 qed_spec_mp "eq_free_eq_subst_te"; |
287 |
287 |
288 goal thy |
288 goal thy |
289 "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n"; |
289 "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n"; |
290 by (list.induct_tac "ts" 1); |
290 by (list.induct_tac "ts" 1); |
291 (* case [] *) |
291 (* case [] *) |
292 by (fast_tac (HOL_cs addss !simpset) 1); |
292 by (fast_tac (HOL_cs addss simpset()) 1); |
293 (* case x#xl *) |
293 (* case x#xl *) |
294 by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (!simpset)) 1); |
294 by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1); |
295 qed_spec_mp "eq_subst_tel_eq_free"; |
295 qed_spec_mp "eq_subst_tel_eq_free"; |
296 |
296 |
297 goal thy |
297 goal thy |
298 "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts"; |
298 "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts"; |
299 by (list.induct_tac "ts" 1); |
299 by (list.induct_tac "ts" 1); |
300 (* case [] *) |
300 (* case [] *) |
301 by (fast_tac (HOL_cs addss !simpset) 1); |
301 by (fast_tac (HOL_cs addss simpset()) 1); |
302 (* case x#xl *) |
302 (* case x#xl *) |
303 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (!simpset)) 1); |
303 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (simpset())) 1); |
304 qed_spec_mp "eq_free_eq_subst_tel"; |
304 qed_spec_mp "eq_free_eq_subst_tel"; |
305 |
305 |
306 (* some useful theorems *) |
306 (* some useful theorems *) |
307 goalw thy [free_tv_subst] |
307 goalw thy [free_tv_subst] |
308 "!!v. v : cod s ==> v : free_tv s"; |
308 "!!v. v : cod s ==> v : free_tv s"; |
320 qed "free_tv_le_new_tv"; |
320 qed "free_tv_le_new_tv"; |
321 |
321 |
322 goal thy |
322 goal thy |
323 "free_tv (s (v::nat)) <= insert v (cod s)"; |
323 "free_tv (s (v::nat)) <= insert v (cod s)"; |
324 by (expand_case_tac "v:dom s" 1); |
324 by (expand_case_tac "v:dom s" 1); |
325 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1); |
325 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1); |
326 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1); |
326 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1); |
327 qed "free_tv_subst_var"; |
327 qed "free_tv_subst_var"; |
328 |
328 |
329 goal thy |
329 goal thy |
330 "free_tv ($ s (t::typ)) <= cod s Un free_tv t"; |
330 "free_tv ($ s (t::typ)) <= cod s Un free_tv t"; |
331 by (typ.induct_tac "t" 1); |
331 by (typ.induct_tac "t" 1); |
332 (* case TVar n *) |
332 (* case TVar n *) |
333 by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
333 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); |
334 (* case Fun t1 t2 *) |
334 (* case Fun t1 t2 *) |
335 by (fast_tac (set_cs addss !simpset) 1); |
335 by (fast_tac (set_cs addss simpset()) 1); |
336 qed "free_tv_app_subst_te"; |
336 qed "free_tv_app_subst_te"; |
337 |
337 |
338 goal thy |
338 goal thy |
339 "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts"; |
339 "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts"; |
340 by (list.induct_tac "ts" 1); |
340 by (list.induct_tac "ts" 1); |
341 (* case [] *) |
341 (* case [] *) |
342 by (Simp_tac 1); |
342 by (Simp_tac 1); |
343 (* case a#al *) |
343 (* case a#al *) |
344 by (cut_facts_tac [free_tv_app_subst_te] 1); |
344 by (cut_facts_tac [free_tv_app_subst_te] 1); |
345 by (fast_tac (set_cs addss !simpset) 1); |
345 by (fast_tac (set_cs addss simpset()) 1); |
346 qed "free_tv_app_subst_tel"; |
346 qed "free_tv_app_subst_tel"; |
347 |
347 |
348 goalw thy [free_tv_subst,dom_def] |
348 goalw thy [free_tv_subst,dom_def] |
349 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
349 "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
350 \ free_tv s1 Un free_tv s2"; |
350 \ free_tv s1 Un free_tv s2"; |
351 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
351 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
352 free_tv_subst_var RS subsetD] |
352 free_tv_subst_var RS subsetD] |
353 addss (!simpset delsimps bex_simps |
353 addss (simpset() delsimps bex_simps |
354 addsimps [cod_def,dom_def])) 1); |
354 addsimps [cod_def,dom_def])) 1); |
355 qed "free_tv_comp_subst"; |
355 qed "free_tv_comp_subst"; |