1300
|
1 |
open Type;
|
|
2 |
|
|
3 |
Addsimps [app_subst_TVar,app_subst_Fun];
|
|
4 |
Addsimps [mgu_eq,mgu_mg,mgu_free];
|
|
5 |
Addsimps [free_tv_TVar,free_tv_Fun,free_tv_Nil,free_tv_Cons];
|
|
6 |
|
|
7 |
(* mgu does not introduce new type variables *)
|
|
8 |
goalw thy [new_tv_def]
|
|
9 |
"!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
|
|
10 |
\ new_tv n u";
|
|
11 |
by( fast_tac (set_cs addDs [mgu_free]) 1);
|
|
12 |
qed "mgu_new";
|
|
13 |
|
|
14 |
(* application of id_subst does not change type expression *)
|
|
15 |
goalw thy [id_subst_def]
|
1400
|
16 |
"$ id_subst = (%t::typ.t)";
|
1300
|
17 |
by (rtac ext 1);
|
1400
|
18 |
by (typ.induct_tac "t" 1);
|
1300
|
19 |
by (ALLGOALS Asm_simp_tac);
|
|
20 |
qed "app_subst_id_te";
|
|
21 |
Addsimps [app_subst_id_te];
|
|
22 |
|
|
23 |
(* application of id_subst does not change list of type expressions *)
|
|
24 |
goalw thy [app_subst_list]
|
1400
|
25 |
"$ id_subst = (%ts::typ list.ts)";
|
1300
|
26 |
by (rtac ext 1);
|
1400
|
27 |
by (list.induct_tac "ts" 1);
|
1300
|
28 |
by (ALLGOALS Asm_simp_tac);
|
|
29 |
qed "app_subst_id_tel";
|
|
30 |
Addsimps [app_subst_id_tel];
|
|
31 |
|
|
32 |
goalw thy [dom_def,id_subst_def,empty_def]
|
|
33 |
"dom id_subst = {}";
|
|
34 |
by (Simp_tac 1);
|
|
35 |
qed "dom_id_subst";
|
|
36 |
Addsimps [dom_id_subst];
|
|
37 |
|
|
38 |
goalw thy [cod_def]
|
|
39 |
"cod id_subst = {}";
|
|
40 |
by (Simp_tac 1);
|
|
41 |
qed "cod_id_subst";
|
|
42 |
Addsimps [cod_id_subst];
|
|
43 |
|
|
44 |
goalw thy [free_tv_subst]
|
|
45 |
"free_tv id_subst = {}";
|
|
46 |
by (Simp_tac 1);
|
|
47 |
qed "free_tv_id_subst";
|
|
48 |
Addsimps [free_tv_id_subst];
|
|
49 |
|
|
50 |
goalw thy [dom_def,cod_def,UNION_def,Bex_def]
|
|
51 |
"!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
|
|
52 |
by (Simp_tac 1);
|
|
53 |
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
|
1465
|
54 |
by (assume_tac 2);
|
1300
|
55 |
by (rotate_tac 1 1);
|
|
56 |
by (Asm_full_simp_tac 1);
|
|
57 |
qed "cod_app_subst";
|
|
58 |
Addsimps [cod_app_subst];
|
|
59 |
|
|
60 |
|
|
61 |
(* composition of substitutions *)
|
|
62 |
goal thy
|
1400
|
63 |
"$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
|
|
64 |
by (typ.induct_tac "t" 1);
|
1300
|
65 |
by (ALLGOALS Asm_simp_tac);
|
|
66 |
qed "subst_comp_te";
|
|
67 |
|
|
68 |
goalw thy [app_subst_list]
|
1400
|
69 |
"$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
|
|
70 |
by (list.induct_tac "ts" 1);
|
1300
|
71 |
(* case [] *)
|
|
72 |
by (Simp_tac 1);
|
|
73 |
(* case x#xl *)
|
|
74 |
by (asm_full_simp_tac (!simpset addsimps [subst_comp_te]) 1);
|
|
75 |
qed "subst_comp_tel";
|
|
76 |
|
|
77 |
|
|
78 |
(* constructor laws for app_subst *)
|
|
79 |
goalw thy [app_subst_list]
|
|
80 |
"$ s [] = []";
|
|
81 |
by (Simp_tac 1);
|
|
82 |
qed "app_subst_Nil";
|
|
83 |
|
|
84 |
goalw thy [app_subst_list]
|
1400
|
85 |
"$ s (t#ts) = ($ s t)#($ s ts)";
|
1300
|
86 |
by (Simp_tac 1);
|
|
87 |
qed "app_subst_Cons";
|
|
88 |
|
|
89 |
Addsimps [app_subst_Nil,app_subst_Cons];
|
|
90 |
|
|
91 |
(* constructor laws for new_tv *)
|
|
92 |
goalw thy [new_tv_def]
|
|
93 |
"new_tv n (TVar m) = (m<n)";
|
|
94 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
95 |
qed "new_tv_TVar";
|
|
96 |
|
|
97 |
goalw thy [new_tv_def]
|
1400
|
98 |
"new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
|
1300
|
99 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
100 |
qed "new_tv_Fun";
|
|
101 |
|
|
102 |
goalw thy [new_tv_def]
|
|
103 |
"new_tv n []";
|
|
104 |
by (Simp_tac 1);
|
|
105 |
qed "new_tv_Nil";
|
|
106 |
|
|
107 |
goalw thy [new_tv_def]
|
1400
|
108 |
"new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
|
1300
|
109 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
110 |
qed "new_tv_Cons";
|
|
111 |
|
|
112 |
Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons];
|
|
113 |
|
|
114 |
|
|
115 |
goalw thy [new_tv_def]
|
|
116 |
"new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
|
|
117 |
\ (! l. l < n --> new_tv n (s l) ))";
|
|
118 |
by( safe_tac HOL_cs );
|
|
119 |
(* ==> *)
|
|
120 |
by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
|
|
121 |
by( subgoal_tac "m:cod s | s l = TVar l" 1);
|
|
122 |
by( safe_tac HOL_cs );
|
|
123 |
by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
|
|
124 |
by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
|
|
125 |
by(Asm_full_simp_tac 1);
|
|
126 |
by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
|
|
127 |
(* <== *)
|
|
128 |
by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
|
|
129 |
by( safe_tac set_cs );
|
|
130 |
by( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
|
|
131 |
by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
|
|
132 |
by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
|
|
133 |
by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
|
|
134 |
qed "new_tv_subst";
|
|
135 |
|
|
136 |
goal thy
|
|
137 |
"new_tv n = list_all (new_tv n)";
|
1465
|
138 |
by (rtac ext 1);
|
1300
|
139 |
by(list.induct_tac "x" 1);
|
|
140 |
by(ALLGOALS Asm_simp_tac);
|
|
141 |
qed "new_tv_list";
|
|
142 |
|
|
143 |
(* substitution affects only variables occurring freely *)
|
|
144 |
goal thy
|
1400
|
145 |
"new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
|
|
146 |
by (typ.induct_tac "t" 1);
|
1300
|
147 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
|
148 |
qed "subst_te_new_tv";
|
|
149 |
Addsimps [subst_te_new_tv];
|
|
150 |
|
|
151 |
goal thy
|
1400
|
152 |
"new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
|
|
153 |
by (list.induct_tac "ts" 1);
|
1300
|
154 |
by (ALLGOALS Asm_full_simp_tac);
|
|
155 |
qed "subst_tel_new_tv";
|
|
156 |
Addsimps [subst_tel_new_tv];
|
|
157 |
|
|
158 |
(* all greater variables are also new *)
|
|
159 |
goal thy
|
1400
|
160 |
"n<=m --> new_tv n (t::typ) --> new_tv m t";
|
|
161 |
by (typ.induct_tac "t" 1);
|
1300
|
162 |
(* case TVar n *)
|
|
163 |
by( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
|
|
164 |
(* case Fun t1 t2 *)
|
|
165 |
by (Asm_simp_tac 1);
|
1521
|
166 |
qed_spec_mp "new_tv_le";
|
1300
|
167 |
Addsimps [lessI RS less_imp_le RS new_tv_le];
|
|
168 |
|
|
169 |
goal thy
|
1400
|
170 |
"n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
|
|
171 |
by( list.induct_tac "ts" 1);
|
1300
|
172 |
(* case [] *)
|
|
173 |
by(Simp_tac 1);
|
|
174 |
(* case a#al *)
|
|
175 |
by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1);
|
1521
|
176 |
qed_spec_mp "new_tv_list_le";
|
1300
|
177 |
Addsimps [lessI RS less_imp_le RS new_tv_list_le];
|
|
178 |
|
|
179 |
goal thy
|
|
180 |
"!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
|
|
181 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
|
|
182 |
by (rtac conjI 1);
|
|
183 |
by (slow_tac (HOL_cs addIs [le_trans]) 1);
|
|
184 |
by (safe_tac HOL_cs );
|
|
185 |
by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
|
|
186 |
by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1);
|
|
187 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [new_tv_le])) );
|
|
188 |
qed "new_tv_subst_le";
|
|
189 |
Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
|
|
190 |
|
|
191 |
(* new_tv property remains if a substitution is applied *)
|
|
192 |
goal thy
|
|
193 |
"!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
|
|
194 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
|
|
195 |
qed "new_tv_subst_var";
|
|
196 |
|
|
197 |
goal thy
|
1400
|
198 |
"new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
|
|
199 |
by (typ.induct_tac "t" 1);
|
1300
|
200 |
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
|
1521
|
201 |
qed_spec_mp "new_tv_subst_te";
|
1300
|
202 |
Addsimps [new_tv_subst_te];
|
|
203 |
|
1400
|
204 |
goal thy
|
|
205 |
"new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
|
1300
|
206 |
by( simp_tac (!simpset addsimps [new_tv_list]) 1);
|
1400
|
207 |
by (list.induct_tac "ts" 1);
|
1300
|
208 |
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
|
1521
|
209 |
qed_spec_mp "new_tv_subst_tel";
|
1300
|
210 |
Addsimps [new_tv_subst_tel];
|
|
211 |
|
|
212 |
(* auxilliary lemma *)
|
|
213 |
goal thy
|
1400
|
214 |
"new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
|
1300
|
215 |
by( simp_tac (!simpset addsimps [new_tv_list]) 1);
|
1400
|
216 |
by (list.induct_tac "ts" 1);
|
1300
|
217 |
by (ALLGOALS Asm_full_simp_tac);
|
|
218 |
qed "new_tv_Suc_list";
|
|
219 |
|
|
220 |
|
|
221 |
(* composition of substitutions preserves new_tv proposition *)
|
|
222 |
goal thy
|
|
223 |
"!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
|
|
224 |
\ new_tv n (($ r) o s)";
|
|
225 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
|
|
226 |
qed "new_tv_subst_comp_1";
|
|
227 |
|
|
228 |
goal thy
|
|
229 |
"!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
|
|
230 |
\ new_tv n (%v.$ r (s v))";
|
|
231 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
|
|
232 |
qed "new_tv_subst_comp_2";
|
|
233 |
|
|
234 |
Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
|
|
235 |
|
|
236 |
(* new type variables do not occur freely in a type structure *)
|
|
237 |
goalw thy [new_tv_def]
|
|
238 |
"!!n. new_tv n ts ==> n~:(free_tv ts)";
|
|
239 |
by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
|
|
240 |
qed "new_tv_not_free_tv";
|
|
241 |
Addsimps [new_tv_not_free_tv];
|
|
242 |
|
|
243 |
goal thy
|
1400
|
244 |
"(t::typ) mem ts --> free_tv t <= free_tv ts";
|
|
245 |
by (list.induct_tac "ts" 1);
|
1300
|
246 |
(* case [] *)
|
|
247 |
by (Simp_tac 1);
|
|
248 |
(* case x#xl *)
|
|
249 |
by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
|
1521
|
250 |
qed_spec_mp "ftv_mem_sub_ftv_list";
|
1300
|
251 |
Addsimps [ftv_mem_sub_ftv_list];
|
|
252 |
|
|
253 |
|
|
254 |
(* if two substitutions yield the same result if applied to a type
|
|
255 |
structure the substitutions coincide on the free type variables
|
|
256 |
occurring in the type structure *)
|
|
257 |
goal thy
|
1400
|
258 |
"$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
|
|
259 |
by (typ.induct_tac "t" 1);
|
1300
|
260 |
(* case TVar n *)
|
|
261 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
262 |
(* case Fun t1 t2 *)
|
|
263 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
1521
|
264 |
qed_spec_mp "eq_subst_te_eq_free";
|
1300
|
265 |
|
|
266 |
goal thy
|
1400
|
267 |
"(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
|
|
268 |
by (typ.induct_tac "t" 1);
|
1300
|
269 |
(* case TVar n *)
|
|
270 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
271 |
(* case Fun t1 t2 *)
|
|
272 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
1521
|
273 |
qed_spec_mp "eq_free_eq_subst_te";
|
1300
|
274 |
|
|
275 |
goal thy
|
1400
|
276 |
"$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
|
|
277 |
by (list.induct_tac "ts" 1);
|
1300
|
278 |
(* case [] *)
|
|
279 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
280 |
(* case x#xl *)
|
|
281 |
by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (!simpset)) 1);
|
1521
|
282 |
qed_spec_mp "eq_subst_tel_eq_free";
|
1300
|
283 |
|
|
284 |
goal thy
|
1400
|
285 |
"(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
|
|
286 |
by (list.induct_tac "ts" 1);
|
1300
|
287 |
(* case [] *)
|
|
288 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
289 |
(* case x#xl *)
|
|
290 |
by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (!simpset)) 1);
|
1521
|
291 |
qed_spec_mp "eq_free_eq_subst_tel";
|
1300
|
292 |
|
|
293 |
(* some useful theorems *)
|
|
294 |
goalw thy [free_tv_subst]
|
|
295 |
"!!v. v : cod s ==> v : free_tv s";
|
|
296 |
by( fast_tac set_cs 1);
|
|
297 |
qed "codD";
|
|
298 |
|
|
299 |
goalw thy [free_tv_subst,dom_def]
|
|
300 |
"!! x. x ~: free_tv s ==> s x = TVar x";
|
|
301 |
by( fast_tac set_cs 1);
|
|
302 |
qed "not_free_impl_id";
|
|
303 |
|
|
304 |
goalw thy [new_tv_def]
|
|
305 |
"!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
|
|
306 |
by( fast_tac HOL_cs 1 );
|
|
307 |
qed "free_tv_le_new_tv";
|
|
308 |
|
|
309 |
goal thy
|
|
310 |
"free_tv (s (v::nat)) <= cod s Un {v}";
|
|
311 |
by( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
|
|
312 |
by( safe_tac (HOL_cs addSIs [subsetI]) );
|
|
313 |
by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
|
|
314 |
by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
|
|
315 |
qed "free_tv_subst_var";
|
|
316 |
|
|
317 |
goal thy
|
1400
|
318 |
"free_tv ($ s (t::typ)) <= cod s Un free_tv t";
|
|
319 |
by( typ.induct_tac "t" 1);
|
1300
|
320 |
(* case TVar n *)
|
|
321 |
by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
|
|
322 |
(* case Fun t1 t2 *)
|
|
323 |
by( fast_tac (set_cs addss !simpset) 1);
|
|
324 |
qed "free_tv_app_subst_te";
|
|
325 |
|
|
326 |
goal thy
|
1400
|
327 |
"free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
|
|
328 |
by( list.induct_tac "ts" 1);
|
1300
|
329 |
(* case [] *)
|
|
330 |
by (Simp_tac 1);
|
|
331 |
(* case a#al *)
|
|
332 |
by( cut_facts_tac [free_tv_app_subst_te] 1);
|
|
333 |
by( fast_tac (set_cs addss !simpset) 1);
|
|
334 |
qed "free_tv_app_subst_tel";
|
|
335 |
|
1521
|
336 |
goalw thy [free_tv_subst,dom_def]
|
|
337 |
"free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \
|
|
338 |
\ free_tv s1 Un free_tv s2";
|
|
339 |
by( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
|
|
340 |
subsetD,free_tv_subst_var RS subsetD] addss (
|
|
341 |
!simpset addsimps [cod_def,dom_def])) 1);
|
|
342 |
qed "free_tv_comp_subst";
|
|
343 |
|