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