|
1 (* Title: HOL/MiniML/W.ML |
|
2 ID: $Id$ |
|
3 Author: Dieter Nazareth and Tobias Nipkow |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 Correctness and completeness of type inference algorithm W |
|
7 *) |
|
8 |
|
9 open W; |
|
10 |
|
11 |
|
12 (* stronger version of Suc_leD *) |
|
13 goalw Nat.thy [le_def] |
|
14 "!!m. Suc m <= n ==> m < n"; |
|
15 by (Asm_full_simp_tac 1); |
|
16 by (cut_facts_tac [less_linear] 1); |
|
17 by (fast_tac HOL_cs 1); |
|
18 qed "Suc_le_lessD"; |
|
19 Addsimps [Suc_le_lessD]; |
|
20 |
|
21 (* correctness of W with respect to has_type *) |
|
22 goal thy |
|
23 "!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)"; |
|
24 by (expr.induct_tac "e" 1); |
|
25 (* case Var n *) |
|
26 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
27 (* case Abs e *) |
|
28 by (asm_full_simp_tac (!simpset addsimps [app_subst_list] |
|
29 setloop (split_tac [expand_bind])) 1); |
|
30 by (strip_tac 1); |
|
31 by (eres_inst_tac [("x","TVar(n) # a")] allE 1); |
|
32 by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1); |
|
33 (* case App e1 e2 *) |
|
34 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
35 by (strip_tac 1); |
|
36 by( rename_tac "sa ta na sb tb nb sc" 1); |
|
37 by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1); |
|
38 by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1); |
|
39 by (rtac (app_subst_Fun RS subst) 1); |
|
40 by (res_inst_tac [("t","$ sc (Fun tb (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1); |
|
41 by (Asm_full_simp_tac 1); |
|
42 by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1); |
|
43 by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1)); |
|
44 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
45 by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1); |
|
46 qed "W_correct"; |
|
47 |
|
48 val has_type_casesE = map(has_type.mk_cases expr.simps) |
|
49 [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"]; |
|
50 |
|
51 |
|
52 (* the resulting type variable is always greater or equal than the given one *) |
|
53 goal thy |
|
54 "!a n s t m. W e a n = Ok (s,t,m) --> n<=m"; |
|
55 by (expr.induct_tac "e" 1); |
|
56 (* case Var(n) *) |
|
57 by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1); |
|
58 (* case Abs e *) |
|
59 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
60 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
|
61 (* case App e1 e2 *) |
|
62 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
63 by (strip_tac 1); |
|
64 by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
|
65 by (eres_inst_tac [("x","a")] allE 1); |
|
66 by (eres_inst_tac [("x","n")] allE 1); |
|
67 by (eres_inst_tac [("x","$ s a")] allE 1); |
|
68 by (eres_inst_tac [("x","s")] allE 1); |
|
69 by (eres_inst_tac [("x","t")] allE 1); |
|
70 by (eres_inst_tac [("x","na")] allE 1); |
|
71 by (eres_inst_tac [("x","na")] allE 1); |
|
72 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
73 by (etac conjE 1); |
|
74 by (eres_inst_tac [("x","sa")] allE 1); |
|
75 by (eres_inst_tac [("x","ta")] allE 1); |
|
76 by (eres_inst_tac [("x","nb")] allE 1); |
|
77 by (etac conjE 1); |
|
78 by (res_inst_tac [("j","na")] le_trans 1); |
|
79 by (Asm_simp_tac 1); |
|
80 by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1); |
|
81 qed "W_var_ge"; |
|
82 |
|
83 Addsimps [W_var_ge]; |
|
84 |
|
85 goal thy |
|
86 "!! s. Ok (s,t,m) = W e a n ==> n<=m"; |
|
87 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
88 qed "W_var_geD"; |
|
89 |
|
90 |
|
91 (* auxiliary lemma *) |
|
92 goal Maybe.thy "(y = Ok x) = (Ok x = y)"; |
|
93 by( simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
94 qed "rotate_Ok"; |
|
95 |
|
96 |
|
97 (* resulting type variable is new *) |
|
98 goal thy |
|
99 "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \ |
|
100 \ (new_tv m s & new_tv m t)"; |
|
101 by (expr.induct_tac "e" 1); |
|
102 (* case Var n *) |
|
103 by (fast_tac (HOL_cs addss (!simpset |
|
104 addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] |
|
105 setloop (split_tac [expand_if]))) 1); |
|
106 |
|
107 (* case Abs e *) |
|
108 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] |
|
109 setloop (split_tac [expand_bind])) 1); |
|
110 by (strip_tac 1); |
|
111 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
112 by (eres_inst_tac [("x","(TVar n)#a")] allE 1); |
|
113 by (fast_tac (HOL_cs addss (!simpset |
|
114 addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
|
115 |
|
116 (* case App e1 e2 *) |
|
117 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
118 by (strip_tac 1); |
|
119 by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
|
120 by (eres_inst_tac [("x","n")] allE 1); |
|
121 by (eres_inst_tac [("x","a")] allE 1); |
|
122 by (eres_inst_tac [("x","s")] allE 1); |
|
123 by (eres_inst_tac [("x","t")] allE 1); |
|
124 by (eres_inst_tac [("x","na")] allE 1); |
|
125 by (eres_inst_tac [("x","na")] allE 1); |
|
126 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
127 by (eres_inst_tac [("x","$ s a")] allE 1); |
|
128 by (eres_inst_tac [("x","sa")] allE 1); |
|
129 by (eres_inst_tac [("x","ta")] allE 1); |
|
130 by (eres_inst_tac [("x","nb")] allE 1); |
|
131 by( asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1); |
|
132 by (rtac conjI 1); |
|
133 by (rtac new_tv_subst_comp_2 1); |
|
134 by (rtac new_tv_subst_comp_2 1); |
|
135 by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1); |
|
136 by (res_inst_tac [("n","na")] new_tv_subst_le 1); |
|
137 by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1); |
|
138 by (Asm_simp_tac 1); |
|
139 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
140 [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le]) |
|
141 1); |
|
142 be (sym RS mgu_new) 1; |
|
143 by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le, |
|
144 new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS |
|
145 new_tv_subst_le,new_tv_le]) 1); |
|
146 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
147 [new_tv_list_le,new_tv_subst_tel,new_tv_le] |
|
148 addss (!simpset)) 1); |
|
149 br (lessI RS new_tv_subst_var) 1; |
|
150 be (sym RS mgu_new) 1; |
|
151 by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] |
|
152 addDs [W_var_geD] addIs |
|
153 [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS |
|
154 new_tv_subst_le,new_tv_le] addss !simpset) 1); |
|
155 by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
156 [new_tv_list_le,new_tv_subst_tel,new_tv_le] |
|
157 addss (!simpset)) 1); |
|
158 bind_thm ("new_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS mp RS mp); |
|
159 |
|
160 |
|
161 goal thy |
|
162 "!n a s t m v. W e a n = Ok (s,t,m) --> \ |
|
163 \ (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a"; |
|
164 by (expr.induct_tac "e" 1); |
|
165 (* case Var n *) |
|
166 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] |
|
167 addss (!simpset setloop (split_tac [expand_if]))) 1); |
|
168 |
|
169 (* case Abs e *) |
|
170 by (asm_full_simp_tac (!simpset addsimps |
|
171 [free_tv_subst] setloop (split_tac [expand_bind])) 1); |
|
172 by (strip_tac 1); |
|
173 by (rename_tac "s t na sa ta m v" 1); |
|
174 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
175 by (eres_inst_tac [("x","TVar n # a")] allE 1); |
|
176 by (eres_inst_tac [("x","s")] allE 1); |
|
177 by (eres_inst_tac [("x","t")] allE 1); |
|
178 by (eres_inst_tac [("x","na")] allE 1); |
|
179 by (eres_inst_tac [("x","v")] allE 1); |
|
180 by (fast_tac (HOL_cs addIs [cod_app_subst] addss !simpset) 1); |
|
181 |
|
182 (* case App e1 e2 *) |
|
183 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
184 by (strip_tac 1); |
|
185 by (rename_tac "s t na sa ta nb sb sc tb m v" 1); |
|
186 by (eres_inst_tac [("x","n")] allE 1); |
|
187 by (eres_inst_tac [("x","a")] allE 1); |
|
188 by (eres_inst_tac [("x","s")] allE 1); |
|
189 by (eres_inst_tac [("x","t")] allE 1); |
|
190 by (eres_inst_tac [("x","na")] allE 1); |
|
191 by (eres_inst_tac [("x","na")] allE 1); |
|
192 by (eres_inst_tac [("x","v")] allE 1); |
|
193 (* second case *) |
|
194 by (eres_inst_tac [("x","$ s a")] allE 1); |
|
195 by (eres_inst_tac [("x","sa")] allE 1); |
|
196 by (eres_inst_tac [("x","ta")] allE 1); |
|
197 by (eres_inst_tac [("x","nb")] allE 1); |
|
198 by (eres_inst_tac [("x","v")] allE 1); |
|
199 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); |
|
200 by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1); |
|
201 bd W_var_geD 1; |
|
202 bd W_var_geD 1; |
|
203 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
|
204 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, |
|
205 codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, |
|
206 less_le_trans,less_not_refl2,subsetD] |
|
207 addEs [UnE] |
|
208 addss !simpset) 1); |
|
209 by (Asm_full_simp_tac 1); |
|
210 bd (sym RS W_var_geD) 1; |
|
211 bd (sym RS W_var_geD) 1; |
|
212 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
|
213 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, |
|
214 free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, |
|
215 less_le_trans,subsetD] |
|
216 addEs [UnE] |
|
217 addss !simpset) 1); |
|
218 bind_thm ("free_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS spec RS mp RS mp RS mp); |
|
219 |
|
220 goal HOL.thy "(~(P | Q)) = (~P & ~Q)"; |
|
221 by( fast_tac HOL_cs 1); |
|
222 qed "not_disj"; |
|
223 |
|
224 (* Completeness of W w.r.t. has_type *) |
|
225 goal thy |
|
226 "!s' a t' n. ($ s' a |- e :: t') --> new_tv n a --> \ |
|
227 \ (? s t. (? m. W e a n = Ok (s,t,m) ) & \ |
|
228 \ (? r. $ s' a = $ r ($ s a) & \ |
|
229 \ t' = $ r t ) )"; |
|
230 by (expr.induct_tac "e" 1); |
|
231 (* case Var n *) |
|
232 by (strip_tac 1); |
|
233 by (simp_tac (!simpset addcongs [conj_cong] |
|
234 setloop (split_tac [expand_if])) 1); |
|
235 by (eresolve_tac has_type_casesE 1); |
|
236 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1); |
|
237 by (res_inst_tac [("x","id_subst")] exI 1); |
|
238 by (res_inst_tac [("x","nth nat a")] exI 1); |
|
239 by (Simp_tac 1); |
|
240 by (res_inst_tac [("x","s'")] exI 1); |
|
241 by (Asm_simp_tac 1); |
|
242 |
|
243 (* case Abs e *) |
|
244 by (strip_tac 1); |
|
245 by (eresolve_tac has_type_casesE 1); |
|
246 by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1); |
|
247 by (eres_inst_tac [("x","(TVar n)#a")] allE 1); |
|
248 by (eres_inst_tac [("x","t2")] allE 1); |
|
249 by (eres_inst_tac [("x","Suc n")] allE 1); |
|
250 by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong] |
|
251 setloop (split_tac [expand_bind]))) 1); |
|
252 |
|
253 (* case App e1 e2 *) |
|
254 by (strip_tac 1); |
|
255 by (eresolve_tac has_type_casesE 1); |
|
256 by (eres_inst_tac [("x","s'")] allE 1); |
|
257 by (eres_inst_tac [("x","a")] allE 1); |
|
258 by (eres_inst_tac [("x","Fun t2 t'")] allE 1); |
|
259 by (eres_inst_tac [("x","n")] allE 1); |
|
260 by (safe_tac HOL_cs); |
|
261 by (eres_inst_tac [("x","r")] allE 1); |
|
262 by (eres_inst_tac [("x","$ s a")] allE 1); |
|
263 by (eres_inst_tac [("x","t2")] allE 1); |
|
264 by (eres_inst_tac [("x","m")] allE 1); |
|
265 bd asm_rl 1; |
|
266 bd asm_rl 1; |
|
267 bd asm_rl 1; |
|
268 by (Asm_full_simp_tac 1); |
|
269 by (safe_tac HOL_cs); |
|
270 by (fast_tac HOL_cs 1); |
|
271 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
|
272 conjunct1,new_tv_list_le,new_tv_subst_tel]) 1); |
|
273 |
|
274 by (subgoal_tac |
|
275 "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \ |
|
276 \ else ra x)) ($ sa t) = \ |
|
277 \ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \ |
|
278 \ else ra x)) (Fun ta (TVar ma))" 1); |
|
279 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ |
|
280 \ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"), |
|
281 ("s","Fun ($ ra ta) t'")] ssubst 2); |
|
282 by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2); |
|
283 br eq_free_eq_subst_te 2; |
|
284 by (strip_tac 2); |
|
285 by (subgoal_tac "na ~=ma" 2); |
|
286 by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, |
|
287 new_tv_not_free_tv,new_tv_le]) 3); |
|
288 by (case_tac "na:free_tv sa" 2); |
|
289 (* na ~: free_tv sa *) |
|
290 by (asm_simp_tac (!simpset addsimps [not_free_impl_id] |
|
291 setloop (split_tac [expand_if])) 3); |
|
292 (* na : free_tv sa *) |
|
293 by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); |
|
294 bd eq_subst_tel_eq_free 2; |
|
295 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
|
296 by (Asm_simp_tac 2); |
|
297 by (case_tac "na:dom sa" 2); |
|
298 (* na ~: dom sa *) |
|
299 by (asm_full_simp_tac (!simpset addsimps [dom_def] |
|
300 setloop (split_tac [expand_if])) 3); |
|
301 (* na : dom sa *) |
|
302 br eq_free_eq_subst_te 2; |
|
303 by (strip_tac 2); |
|
304 by (subgoal_tac "nb ~= ma" 2); |
|
305 by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
|
306 be conjE 3; |
|
307 bd new_tv_subst_tel 3; |
|
308 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3); |
|
309 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss |
|
310 (!simpset addsimps [cod_def,free_tv_subst])) 3); |
|
311 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] |
|
312 setloop (split_tac [expand_if]))) 2); |
|
313 |
|
314 by (Simp_tac 2); |
|
315 br eq_free_eq_subst_te 2; |
|
316 by (strip_tac 2 ); |
|
317 by (subgoal_tac "na ~= ma" 2); |
|
318 by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
|
319 be conjE 3; |
|
320 bd (sym RS W_var_geD) 3; |
|
321 by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3); |
|
322 by (case_tac "na: free_tv t - free_tv sa" 2); |
|
323 (* case na ~: free_tv t - free_tv sa *) |
|
324 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3); |
|
325 (* case na : free_tv t - free_tv sa *) |
|
326 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); |
|
327 by (dres_inst_tac [("l1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); |
|
328 bd eq_subst_tel_eq_free 2; |
|
329 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
|
330 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2); |
|
331 |
|
332 by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
333 by (safe_tac HOL_cs ); |
|
334 bd mgu_Ok 1; |
|
335 by( fast_tac (HOL_cs addss !simpset) 1); |
|
336 by (REPEAT (resolve_tac [exI,conjI] 1)); |
|
337 by (fast_tac HOL_cs 1); |
|
338 by (fast_tac HOL_cs 1); |
|
339 by ((dtac mgu_mg 1) THEN (atac 1)); |
|
340 be exE 1; |
|
341 by (res_inst_tac [("x","rb")] exI 1); |
|
342 br conjI 1; |
|
343 by (dres_inst_tac [("x","ma")] fun_cong 2); |
|
344 by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2); |
|
345 by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1); |
|
346 by (res_inst_tac [("l2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN |
|
347 (2,trans)) 1); |
|
348 by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1); |
|
349 br eq_free_eq_subst_tel 1; |
|
350 by( safe_tac HOL_cs ); |
|
351 by (subgoal_tac "ma ~= na" 1); |
|
352 by ((forward_tac [new_tv_W] 2) THEN (atac 2)); |
|
353 be conjE 2; |
|
354 bd new_tv_subst_tel 2; |
|
355 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2); |
|
356 by (( forw_inst_tac [("xd","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2)); |
|
357 be conjE 2; |
|
358 bd (free_tv_app_subst_tel RS subsetD) 2; |
|
359 by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD, |
|
360 new_tv_not_free_tv]) 2); |
|
361 by (case_tac "na: free_tv t - free_tv sa" 1); |
|
362 (* case na ~: free_tv t - free_tv sa *) |
|
363 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); |
|
364 (* case na : free_tv t - free_tv sa *) |
|
365 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
366 bd (free_tv_app_subst_tel RS subsetD) 1; |
|
367 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), |
|
368 eq_subst_tel_eq_free] addss ((!simpset addsimps |
|
369 [not_disj,free_tv_subst,dom_def]))) 1); |
|
370 qed "W_complete"; |
|
371 |
|
372 |
|
373 |
|
374 |
|
375 |
|
376 |
|
377 |
|
378 |
|
379 |