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