author | oheimb |
Thu, 15 May 1997 15:51:47 +0200 | |
changeset 3207 | fe79ad367d77 |
parent 3018 | e65b60b28341 |
child 3240 | cc1d52d47fae |
permissions | -rw-r--r-- |
1300 | 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 |
||
2525 | 11 |
Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD]; |
1300 | 12 |
|
13 |
val has_type_casesE = map(has_type.mk_cases expr.simps) |
|
2525 | 14 |
[" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ]; |
1300 | 15 |
|
16 |
(* the resulting type variable is always greater or equal than the given one *) |
|
17 |
goal thy |
|
2525 | 18 |
"!A n S t m. W e A n = Some (S,t,m) --> n<=m"; |
1300 | 19 |
by (expr.induct_tac "e" 1); |
20 |
(* case Var(n) *) |
|
2525 | 21 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1); |
22 |
by (strip_tac 1); |
|
23 |
by (etac conjE 1); |
|
24 |
by (etac conjE 1); |
|
25 |
by (dtac sym 1); |
|
26 |
by (dtac sym 1); |
|
27 |
by (dtac sym 1); |
|
28 |
by (Asm_full_simp_tac 1); |
|
1300 | 29 |
(* case Abs e *) |
2525 | 30 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
1300 | 31 |
by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
32 |
(* case App e1 e2 *) |
|
2525 | 33 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
1300 | 34 |
by (strip_tac 1); |
2525 | 35 |
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1); |
36 |
by (eres_inst_tac [("x","A")] allE 1); |
|
1300 | 37 |
by (eres_inst_tac [("x","n")] allE 1); |
2525 | 38 |
by (eres_inst_tac [("x","$ S A")] allE 1); |
39 |
by (eres_inst_tac [("x","S")] allE 1); |
|
1300 | 40 |
by (eres_inst_tac [("x","t")] allE 1); |
2525 | 41 |
by (eres_inst_tac [("x","n1")] allE 1); |
42 |
by (eres_inst_tac [("x","n1")] allE 1); |
|
1300 | 43 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
44 |
by (etac conjE 1); |
|
2525 | 45 |
by (eres_inst_tac [("x","S1")] allE 1); |
46 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
47 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
1300 | 48 |
by (etac conjE 1); |
2525 | 49 |
by (res_inst_tac [("j","n1")] le_trans 1); |
1300 | 50 |
by (Asm_simp_tac 1); |
1669 | 51 |
by (Asm_simp_tac 1); |
2525 | 52 |
(* case LET e1 e2 *) |
53 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
|
54 |
by (strip_tac 1); |
|
55 |
by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1); |
|
56 |
by (REPEAT (etac conjE 1)); |
|
57 |
by (REPEAT (etac allE 1)); |
|
58 |
by (mp_tac 1); |
|
59 |
by (mp_tac 1); |
|
60 |
by (best_tac (!claset addEs [le_trans]) 1); |
|
1486 | 61 |
qed_spec_mp "W_var_ge"; |
1300 | 62 |
|
63 |
Addsimps [W_var_ge]; |
|
64 |
||
65 |
goal thy |
|
2525 | 66 |
"!! s. Some (S,t,m) = W e A n ==> n<=m"; |
1300 | 67 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
68 |
qed "W_var_geD"; |
|
69 |
||
2525 | 70 |
goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"; |
71 |
by (dtac W_var_geD 1); |
|
72 |
by (rtac new_scheme_list_le 1); |
|
3018 | 73 |
by (assume_tac 1); |
74 |
by (assume_tac 1); |
|
2525 | 75 |
qed "new_tv_compatible_W"; |
1300 | 76 |
|
2525 | 77 |
goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; |
78 |
by (type_scheme.induct_tac "sch" 1); |
|
79 |
by (Asm_full_simp_tac 1); |
|
80 |
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); |
|
81 |
by (strip_tac 1); |
|
82 |
by (Asm_full_simp_tac 1); |
|
83 |
by (etac conjE 1); |
|
84 |
by (rtac conjI 1); |
|
85 |
by (rtac new_tv_le 1); |
|
86 |
by (mp_tac 2); |
|
87 |
by (mp_tac 2); |
|
3018 | 88 |
by (assume_tac 2); |
2525 | 89 |
by (rtac add_le_mono 1); |
90 |
by (Simp_tac 1); |
|
91 |
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1); |
|
92 |
by (strip_tac 1); |
|
93 |
by (rtac new_tv_le 1); |
|
94 |
by (mp_tac 2); |
|
95 |
by (mp_tac 2); |
|
3018 | 96 |
by (assume_tac 2); |
2525 | 97 |
by (rtac add_le_mono 1); |
98 |
by (Simp_tac 1); |
|
99 |
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1); |
|
100 |
by (strip_tac 1); |
|
101 |
by (dtac not_leE 1); |
|
102 |
by (rtac less_or_eq_imp_le 1); |
|
103 |
by (Fast_tac 1); |
|
104 |
qed_spec_mp "new_tv_bound_typ_inst_sch"; |
|
105 |
||
106 |
Addsimps [new_tv_bound_typ_inst_sch]; |
|
1300 | 107 |
|
108 |
(* resulting type variable is new *) |
|
109 |
goal thy |
|
2525 | 110 |
"!n A S t m. new_tv n A --> W e A n = Some (S,t,m) --> \ |
111 |
\ new_tv m S & new_tv m t"; |
|
1300 | 112 |
by (expr.induct_tac "e" 1); |
113 |
(* case Var n *) |
|
2525 | 114 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1); |
115 |
by (strip_tac 1); |
|
116 |
by (REPEAT (etac conjE 1)); |
|
117 |
by (rtac conjI 1); |
|
118 |
by (dtac sym 1); |
|
119 |
by (Asm_full_simp_tac 1); |
|
120 |
by (dtac sym 1); |
|
121 |
by (dtac sym 1); |
|
122 |
by (dtac sym 1); |
|
123 |
by (dtac new_tv_nth_nat_A 1); |
|
3018 | 124 |
by (assume_tac 1); |
2525 | 125 |
by (Asm_full_simp_tac 1); |
1300 | 126 |
(* case Abs e *) |
127 |
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] |
|
2525 | 128 |
setloop (split_tac [expand_option_bind])) 1); |
1300 | 129 |
by (strip_tac 1); |
130 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
|
2525 | 131 |
by (eres_inst_tac [("x","(FVar n)#A")] allE 1); |
1300 | 132 |
by (fast_tac (HOL_cs addss (!simpset |
1465 | 133 |
addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
1300 | 134 |
(* case App e1 e2 *) |
2525 | 135 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
1300 | 136 |
by (strip_tac 1); |
2525 | 137 |
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1); |
1300 | 138 |
by (eres_inst_tac [("x","n")] allE 1); |
2525 | 139 |
by (eres_inst_tac [("x","A")] allE 1); |
140 |
by (eres_inst_tac [("x","S")] allE 1); |
|
1300 | 141 |
by (eres_inst_tac [("x","t")] allE 1); |
2525 | 142 |
by (eres_inst_tac [("x","n1")] allE 1); |
143 |
by (eres_inst_tac [("x","n1")] allE 1); |
|
144 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1); |
|
145 |
by (eres_inst_tac [("x","$ S A")] allE 1); |
|
146 |
by (eres_inst_tac [("x","S1")] allE 1); |
|
147 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
148 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
3018 | 149 |
by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1); |
1300 | 150 |
by (rtac conjI 1); |
151 |
by (rtac new_tv_subst_comp_2 1); |
|
152 |
by (rtac new_tv_subst_comp_2 1); |
|
2525 | 153 |
by (rtac (lessI RS less_imp_le RS new_tv_le) 1); |
154 |
by (res_inst_tac [("n","n1")] new_tv_subst_le 1); |
|
155 |
by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 1); |
|
1300 | 156 |
by (Asm_simp_tac 1); |
157 |
by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
2525 | 158 |
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le]) |
1300 | 159 |
1); |
1465 | 160 |
by (etac (sym RS mgu_new) 1); |
2525 | 161 |
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le, |
162 |
new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS |
|
163 |
new_tv_subst_le,new_tv_le]) 1); |
|
164 |
by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
165 |
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] |
|
166 |
addss (!simpset)) 1); |
|
1465 | 167 |
by (rtac (lessI RS new_tv_subst_var) 1); |
168 |
by (etac (sym RS mgu_new) 1); |
|
1925 | 169 |
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] |
2525 | 170 |
addDs [W_var_geD] addIs |
171 |
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS |
|
172 |
new_tv_subst_le,new_tv_le] addss !simpset) 1); |
|
173 |
by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
|
174 |
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] |
|
175 |
addss (!simpset)) 1); |
|
176 |
(* case LET e1 e2 *) |
|
177 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
|
178 |
by (strip_tac 1); |
|
179 |
by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1); |
|
180 |
by (REPEAT (etac conjE 1)); |
|
181 |
by (eres_inst_tac [("x","n1")] allE 1); |
|
182 |
by (eres_inst_tac [("x","A")] allE 1); |
|
183 |
by (eres_inst_tac [("x","S1")] allE 1); |
|
184 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
185 |
by (rotate_tac 1 1); |
|
186 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
187 |
by (mp_tac 1); |
|
188 |
by (mp_tac 1); |
|
189 |
by (etac conjE 1); |
|
190 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1); |
|
191 |
by (dtac sym 1); |
|
192 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
193 |
by (eres_inst_tac [("x","gen ($ S1 A) t1 # $ S1 A")] allE 1); |
|
194 |
by (eres_inst_tac [("x","S2")] allE 1); |
|
195 |
by (eres_inst_tac [("x","t2")] allE 1); |
|
196 |
by (eres_inst_tac [("x","m2")] allE 1); |
|
197 |
by (subgoal_tac "new_tv n2 (gen ($ S1 A) t1 # $ S1 A)" 1); |
|
198 |
by (mp_tac 1); |
|
199 |
by (mp_tac 1); |
|
200 |
by (etac conjE 1); |
|
201 |
by (rtac conjI 1); |
|
202 |
by (simp_tac (!simpset addsimps [o_def]) 1); |
|
203 |
by (rtac new_tv_subst_comp_2 1); |
|
204 |
by (res_inst_tac [("n","n2")] new_tv_subst_le 1); |
|
205 |
by (etac W_var_ge 1); |
|
3018 | 206 |
by (assume_tac 1); |
207 |
by (assume_tac 1); |
|
208 |
by (assume_tac 1); |
|
3008 | 209 |
by (rewtac new_tv_def); |
2525 | 210 |
by (Asm_simp_tac 1); |
211 |
by (dtac W_var_ge 1); |
|
212 |
by (rtac allI 1); |
|
213 |
by (rename_tac "p" 1); |
|
214 |
by (strip_tac 1); |
|
3008 | 215 |
by (rewtac free_tv_subst); |
2525 | 216 |
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); |
217 |
fun restrict_prems is tacf = |
|
218 |
METAHYPS(fn prems => |
|
219 |
let val iprems = map (fn i => nth_elem(i,prems)) is |
|
220 |
in cut_facts_tac iprems 1 THEN tacf 1 end); |
|
221 |
by (restrict_prems [0,4,8,9] (best_tac (!claset addEs [less_le_trans])) 1); |
|
1486 | 222 |
qed_spec_mp "new_tv_W"; |
1300 | 223 |
|
2525 | 224 |
goal thy "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)"; |
225 |
by (type_scheme.induct_tac "sch" 1); |
|
226 |
by (Asm_full_simp_tac 1); |
|
227 |
by (Asm_full_simp_tac 1); |
|
228 |
by (strip_tac 1); |
|
229 |
by (rtac exI 1); |
|
230 |
by (rtac refl 1); |
|
231 |
by (Asm_full_simp_tac 1); |
|
232 |
qed_spec_mp "free_tv_bound_typ_inst1"; |
|
233 |
||
234 |
Addsimps [free_tv_bound_typ_inst1]; |
|
1300 | 235 |
|
236 |
goal thy |
|
2525 | 237 |
"!n A S t m v. W e A n = Some (S,t,m) --> \ |
238 |
\ (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A"; |
|
1300 | 239 |
by (expr.induct_tac "e" 1); |
240 |
(* case Var n *) |
|
2525 | 241 |
by (simp_tac (!simpset addsimps |
242 |
[free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1); |
|
243 |
by (strip_tac 1); |
|
244 |
by (REPEAT (etac conjE 1)); |
|
245 |
by (hyp_subst_tac 1); |
|
246 |
by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1); |
|
247 |
by (case_tac "v : free_tv (nth nat A)" 1); |
|
248 |
by (Asm_full_simp_tac 1); |
|
249 |
by (strip_tac 1); |
|
250 |
by (dtac free_tv_bound_typ_inst1 1); |
|
251 |
by (simp_tac (!simpset addsimps [o_def]) 1); |
|
252 |
by (rotate_tac 3 1); |
|
253 |
by (etac exE 1); |
|
254 |
by (rotate_tac 3 1); |
|
255 |
by (Asm_full_simp_tac 1); |
|
256 |
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); |
|
257 |
by (dtac add_lessD1 1); |
|
258 |
by (fast_tac (!claset addIs [less_irrefl]) 1); |
|
1300 | 259 |
(* case Abs e *) |
260 |
by (asm_full_simp_tac (!simpset addsimps |
|
2525 | 261 |
[free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1); |
1300 | 262 |
by (strip_tac 1); |
2525 | 263 |
by (rename_tac "S t n1 S1 t1 m v" 1); |
1300 | 264 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
2525 | 265 |
by (eres_inst_tac [("x","FVar n # A")] allE 1); |
266 |
by (eres_inst_tac [("x","S")] allE 1); |
|
1300 | 267 |
by (eres_inst_tac [("x","t")] allE 1); |
2525 | 268 |
by (eres_inst_tac [("x","n1")] allE 1); |
1300 | 269 |
by (eres_inst_tac [("x","v")] allE 1); |
2525 | 270 |
by (best_tac (HOL_cs addIs [cod_app_subst] |
1669 | 271 |
addss (!simpset addsimps [less_Suc_eq])) 1); |
1300 | 272 |
(* case App e1 e2 *) |
2525 | 273 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1); |
1300 | 274 |
by (strip_tac 1); |
2525 | 275 |
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1); |
1300 | 276 |
by (eres_inst_tac [("x","n")] allE 1); |
2525 | 277 |
by (eres_inst_tac [("x","A")] allE 1); |
278 |
by (eres_inst_tac [("x","S")] allE 1); |
|
1300 | 279 |
by (eres_inst_tac [("x","t")] allE 1); |
2525 | 280 |
by (eres_inst_tac [("x","n1")] allE 1); |
281 |
by (eres_inst_tac [("x","n1")] allE 1); |
|
1300 | 282 |
by (eres_inst_tac [("x","v")] allE 1); |
283 |
(* second case *) |
|
2525 | 284 |
by (eres_inst_tac [("x","$ S A")] allE 1); |
285 |
by (eres_inst_tac [("x","S1")] allE 1); |
|
286 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
287 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
1300 | 288 |
by (eres_inst_tac [("x","v")] allE 1); |
289 |
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); |
|
2525 | 290 |
by (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1); |
1465 | 291 |
by (dtac W_var_geD 1); |
292 |
by (dtac W_var_geD 1); |
|
1300 | 293 |
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
294 |
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, |
|
2525 | 295 |
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, |
1300 | 296 |
less_le_trans,less_not_refl2,subsetD] |
297 |
addEs [UnE] |
|
298 |
addss !simpset) 1); |
|
299 |
by (Asm_full_simp_tac 1); |
|
1465 | 300 |
by (dtac (sym RS W_var_geD) 1); |
301 |
by (dtac (sym RS W_var_geD) 1); |
|
1300 | 302 |
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
303 |
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, |
|
2525 | 304 |
free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, |
305 |
less_le_trans,subsetD] |
|
306 |
addEs [UnE] |
|
307 |
addss !simpset) 1); |
|
308 |
(* LET e1 e2 *) |
|
309 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1); |
|
310 |
by (strip_tac 1); |
|
311 |
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1); |
|
312 |
by (eres_inst_tac [("x","nat")] allE 1); |
|
313 |
by (eres_inst_tac [("x","A")] allE 1); |
|
314 |
by (eres_inst_tac [("x","S1")] allE 1); |
|
315 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
316 |
by (rotate_tac 1 1); |
|
317 |
by (eres_inst_tac [("x","n2")] allE 1); |
|
318 |
by (rotate_tac 4 1); |
|
319 |
by (eres_inst_tac [("x","v")] allE 1); |
|
320 |
by (mp_tac 1); |
|
321 |
by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]); |
|
322 |
by (mp_tac 1); |
|
323 |
by (Asm_full_simp_tac 1); |
|
324 |
by (rtac conjI 1); |
|
325 |
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] |
|
326 |
addDs [less_le_trans]) 1); |
|
327 |
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] |
|
328 |
addDs [less_le_trans]) 1); |
|
1486 | 329 |
qed_spec_mp "free_tv_W"; |
1300 | 330 |
|
2525 | 331 |
goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}"; |
332 |
by (Fast_tac 1); |
|
2625 | 333 |
val weaken_A_Int_B_eq_empty = result(); |
2525 | 334 |
|
335 |
goal thy "!!A. x ~: A | x : B ==> x ~: A - B"; |
|
336 |
by (Fast_tac 1); |
|
2625 | 337 |
val weaken_not_elem_A_minus_B = result(); |
2525 | 338 |
|
339 |
(* correctness of W with respect to has_type *) |
|
340 |
goal W.thy |
|
341 |
"!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t"; |
|
342 |
by (expr.induct_tac "e" 1); |
|
343 |
(* case Var n *) |
|
344 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
345 |
by (strip_tac 1); |
|
346 |
by (rtac has_type.VarI 1); |
|
347 |
by (Simp_tac 1); |
|
348 |
by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1); |
|
349 |
by (rtac exI 1); |
|
350 |
by (rtac refl 1); |
|
351 |
(* case Abs e *) |
|
352 |
by (asm_full_simp_tac (!simpset addsimps [app_subst_list] |
|
353 |
setloop (split_tac [expand_option_bind])) 1); |
|
354 |
by (strip_tac 1); |
|
355 |
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1); |
|
356 |
by (Asm_full_simp_tac 1); |
|
357 |
by (rtac has_type.AbsI 1); |
|
358 |
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1); |
|
3018 | 359 |
by (dtac sym 1); |
2525 | 360 |
by (REPEAT (etac allE 1)); |
361 |
by (etac impE 1); |
|
362 |
by (mp_tac 2); |
|
363 |
by (Asm_simp_tac 1); |
|
3018 | 364 |
by (assume_tac 1); |
2525 | 365 |
(* case App e1 e2 *) |
366 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
|
367 |
by (strip_tac 1); |
|
368 |
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); |
|
369 |
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1); |
|
370 |
by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1); |
|
371 |
by (rtac (app_subst_Fun RS subst) 1); |
|
372 |
by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1); |
|
373 |
by (Asm_full_simp_tac 1); |
|
374 |
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); |
|
375 |
by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1)); |
|
376 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
377 |
by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); |
|
378 |
by (rtac (has_type_cl_sub RS spec) 1); |
|
379 |
by (forward_tac [new_tv_W] 1); |
|
3018 | 380 |
by (assume_tac 1); |
2525 | 381 |
by (dtac conjunct1 1); |
382 |
by (dtac conjunct1 1); |
|
383 |
by (forward_tac [new_tv_subst_scheme_list] 1); |
|
384 |
by (rtac new_scheme_list_le 1); |
|
385 |
by (rtac W_var_ge 1); |
|
3018 | 386 |
by (assume_tac 1); |
387 |
by (assume_tac 1); |
|
2525 | 388 |
by (etac thin_rl 1); |
389 |
by (REPEAT (etac allE 1)); |
|
3018 | 390 |
by (dtac sym 1); |
391 |
by (dtac sym 1); |
|
2525 | 392 |
by (etac thin_rl 1); |
393 |
by (etac thin_rl 1); |
|
394 |
by (mp_tac 1); |
|
395 |
by (mp_tac 1); |
|
3018 | 396 |
by (assume_tac 1); |
2525 | 397 |
(* case Let e1 e2 *) |
398 |
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
|
399 |
by (strip_tac 1); |
|
400 |
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); |
|
401 |
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1); |
|
402 |
by (simp_tac (!simpset addsimps [o_def]) 1); |
|
403 |
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); |
|
404 |
by (rtac (has_type_cl_sub RS spec) 1); |
|
405 |
by (dres_inst_tac [("x","A")] spec 1); |
|
406 |
by (dres_inst_tac [("x","S1")] spec 1); |
|
407 |
by (dres_inst_tac [("x","t1")] spec 1); |
|
408 |
by (dres_inst_tac [("x","m2")] spec 1); |
|
409 |
by (rotate_tac 4 1); |
|
410 |
by (dres_inst_tac [("x","m1")] spec 1); |
|
411 |
by (mp_tac 1); |
|
412 |
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
413 |
by (simp_tac (!simpset addsimps [o_def]) 1); |
|
414 |
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); |
|
415 |
by (rtac (gen_subst_commutes RS sym RS subst) 1); |
|
416 |
by (rtac (app_subst_Cons RS subst) 2); |
|
417 |
by (etac thin_rl 2); |
|
418 |
by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2); |
|
419 |
by (dres_inst_tac [("x","S2")] spec 2); |
|
420 |
by (dres_inst_tac [("x","t")] spec 2); |
|
421 |
by (dres_inst_tac [("x","n2")] spec 2); |
|
422 |
by (dres_inst_tac [("x","m2")] spec 2); |
|
423 |
by (forward_tac [new_tv_W] 2); |
|
3018 | 424 |
by (assume_tac 2); |
2525 | 425 |
by (dtac conjunct1 2); |
426 |
by (dtac conjunct1 2); |
|
427 |
by (forward_tac [new_tv_subst_scheme_list] 2); |
|
428 |
by (rtac new_scheme_list_le 2); |
|
429 |
by (rtac W_var_ge 2); |
|
3018 | 430 |
by (assume_tac 2); |
431 |
by (assume_tac 2); |
|
2525 | 432 |
by (etac impE 2); |
433 |
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2); |
|
434 |
by (Simp_tac 2); |
|
435 |
by (Fast_tac 2); |
|
3018 | 436 |
by (assume_tac 2); |
2525 | 437 |
by (Asm_full_simp_tac 2); |
438 |
by (rtac weaken_A_Int_B_eq_empty 1); |
|
439 |
by (rtac allI 1); |
|
440 |
by (strip_tac 1); |
|
441 |
by (rtac weaken_not_elem_A_minus_B 1); |
|
442 |
by (case_tac "x < m2" 1); |
|
443 |
by (rtac disjI2 1); |
|
444 |
by (rtac (free_tv_gen_cons RS subst) 1); |
|
445 |
by (rtac free_tv_W 1); |
|
3018 | 446 |
by (assume_tac 1); |
2525 | 447 |
by (Asm_full_simp_tac 1); |
3018 | 448 |
by (assume_tac 1); |
2525 | 449 |
by (rtac disjI1 1); |
450 |
by (dtac new_tv_W 1); |
|
3018 | 451 |
by (assume_tac 1); |
2525 | 452 |
by (dtac conjunct2 1); |
453 |
by (dtac conjunct2 1); |
|
454 |
by (rtac new_tv_not_free_tv 1); |
|
455 |
by (rtac new_tv_le 1); |
|
3018 | 456 |
by (assume_tac 2); |
2525 | 457 |
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1); |
458 |
qed_spec_mp "W_correct_lemma"; |
|
459 |
||
460 |
goal Arith.thy "!!n::nat. ~ k+n < n"; |
|
461 |
by (nat_ind_tac "k" 1); |
|
3018 | 462 |
by (ALLGOALS Asm_simp_tac); |
463 |
by (trans_tac 1); |
|
2625 | 464 |
val not_add_less1 = result(); |
2525 | 465 |
Addsimps [not_add_less1]; |
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset
|
466 |
|
1300 | 467 |
(* Completeness of W w.r.t. has_type *) |
468 |
goal thy |
|
2525 | 469 |
"!S' A t' n. $S' A |- e :: t' --> new_tv n A --> \ |
470 |
\ (? S t. (? m. W e A n = Some (S,t,m)) & \ |
|
471 |
\ (? R. $S' A = $R ($S A) & t' = $R t))"; |
|
1300 | 472 |
by (expr.induct_tac "e" 1); |
473 |
(* case Var n *) |
|
474 |
by (strip_tac 1); |
|
475 |
by (simp_tac (!simpset addcongs [conj_cong] |
|
2525 | 476 |
setloop (split_tac [expand_if])) 1); |
1300 | 477 |
by (eresolve_tac has_type_casesE 1); |
2525 | 478 |
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1); |
479 |
by (etac exE 1); |
|
480 |
by (hyp_subst_tac 1); |
|
481 |
by (rename_tac "S" 1); |
|
482 |
by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1); |
|
483 |
by (rtac conjI 1); |
|
1300 | 484 |
by (Asm_simp_tac 1); |
2525 | 485 |
by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] |
486 |
delsimps [bound_typ_inst_composed_subst]) 1); |
|
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
487 |
(** LEVEL 12 **) |
1300 | 488 |
(* case Abs e *) |
489 |
by (strip_tac 1); |
|
490 |
by (eresolve_tac has_type_casesE 1); |
|
2525 | 491 |
by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1); |
492 |
by (eres_inst_tac [("x","(FVar n)#A")] allE 1); |
|
1300 | 493 |
by (eres_inst_tac [("x","t2")] allE 1); |
494 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
|
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
495 |
by (best_tac (HOL_cs addSDs [mk_scheme_injective] |
3207 | 496 |
addss (!simpset addcongs [conj_cong] |
3008 | 497 |
setloop (split_tac [expand_option_bind]))) 1); |
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
498 |
(** LEVEL 19 **) |
1300 | 499 |
|
500 |
(* case App e1 e2 *) |
|
501 |
by (strip_tac 1); |
|
502 |
by (eresolve_tac has_type_casesE 1); |
|
2525 | 503 |
by (eres_inst_tac [("x","S'")] allE 1); |
504 |
by (eres_inst_tac [("x","A")] allE 1); |
|
1400 | 505 |
by (eres_inst_tac [("x","t2 -> t'")] allE 1); |
1300 | 506 |
by (eres_inst_tac [("x","n")] allE 1); |
507 |
by (safe_tac HOL_cs); |
|
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
508 |
(** LEVEL 26 **) |
2525 | 509 |
by (eres_inst_tac [("x","R")] allE 1); |
510 |
by (eres_inst_tac [("x","$ S A")] allE 1); |
|
1300 | 511 |
by (eres_inst_tac [("x","t2")] allE 1); |
512 |
by (eres_inst_tac [("x","m")] allE 1); |
|
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
513 |
by (rotate_tac ~3 1); |
1300 | 514 |
by (Asm_full_simp_tac 1); |
515 |
by (safe_tac HOL_cs); |
|
2779
9c42ae57b5f4
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
paulson
parents:
2749
diff
changeset
|
516 |
by (contr_tac 1); |
1300 | 517 |
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
2525 | 518 |
conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1); |
2779
9c42ae57b5f4
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
paulson
parents:
2749
diff
changeset
|
519 |
(** LEVEL 35 **) |
1300 | 520 |
by (subgoal_tac |
2525 | 521 |
"$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
522 |
\ else Ra x)) ($ Sa t) = \ |
|
523 |
\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
|
524 |
\ else Ra x)) (ta -> (TVar ma))" 1); |
|
1300 | 525 |
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ |
2525 | 526 |
\ (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"), |
527 |
("s","($ Ra ta) -> t'")] ssubst 2); |
|
1300 | 528 |
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2); |
1465 | 529 |
by (rtac eq_free_eq_subst_te 2); |
1300 | 530 |
by (strip_tac 2); |
531 |
by (subgoal_tac "na ~=ma" 2); |
|
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset
|
532 |
by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, |
2525 | 533 |
new_tv_not_free_tv,new_tv_le]) 3); |
534 |
by (case_tac "na:free_tv Sa" 2); |
|
535 |
(* n1 ~: free_tv S1 *) |
|
536 |
by (forward_tac [not_free_impl_id] 3); |
|
537 |
by (asm_simp_tac (!simpset |
|
538 |
setloop (split_tac [expand_if])) 3); |
|
539 |
(* na : free_tv Sa *) |
|
540 |
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); |
|
541 |
by (dtac eq_subst_scheme_list_eq_free 2); |
|
1300 | 542 |
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
543 |
by (Asm_simp_tac 2); |
|
2525 | 544 |
by (case_tac "na:dom Sa" 2); |
545 |
(* na ~: dom Sa *) |
|
1300 | 546 |
by (asm_full_simp_tac (!simpset addsimps [dom_def] |
2525 | 547 |
setloop (split_tac [expand_if])) 3); |
548 |
(* na : dom Sa *) |
|
1465 | 549 |
by (rtac eq_free_eq_subst_te 2); |
1300 | 550 |
by (strip_tac 2); |
551 |
by (subgoal_tac "nb ~= ma" 2); |
|
552 |
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
|
1465 | 553 |
by (etac conjE 3); |
2525 | 554 |
by (dtac new_tv_subst_scheme_list 3); |
555 |
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3); |
|
1300 | 556 |
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss |
2525 | 557 |
(!simpset addsimps [cod_def,free_tv_subst])) 3); |
1300 | 558 |
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] |
2525 | 559 |
setloop (split_tac [expand_if]))) 2); |
1300 | 560 |
by (Simp_tac 2); |
1465 | 561 |
by (rtac eq_free_eq_subst_te 2); |
1300 | 562 |
by (strip_tac 2 ); |
563 |
by (subgoal_tac "na ~= ma" 2); |
|
564 |
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
|
1465 | 565 |
by (etac conjE 3); |
566 |
by (dtac (sym RS W_var_geD) 3); |
|
2525 | 567 |
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3); |
568 |
by (case_tac "na: free_tv t - free_tv Sa" 2); |
|
569 |
(* case na ~: free_tv t - free_tv Sa *) |
|
3018 | 570 |
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
571 |
by (Fast_tac 3); |
2525 | 572 |
(* case na : free_tv t - free_tv Sa *) |
3018 | 573 |
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); |
2525 | 574 |
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); |
575 |
by (dtac eq_subst_scheme_list_eq_free 2); |
|
1300 | 576 |
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
577 |
(** LEVEL 75 **) |
2525 | 578 |
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2); |
579 |
by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); |
|
1300 | 580 |
by (safe_tac HOL_cs ); |
2525 | 581 |
by (dtac mgu_Some 1); |
3018 | 582 |
by ( fast_tac (HOL_cs addss !simpset) 1); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
583 |
(** LEVEL 80 *) |
1300 | 584 |
by ((dtac mgu_mg 1) THEN (atac 1)); |
1465 | 585 |
by (etac exE 1); |
2525 | 586 |
by (res_inst_tac [("x","Rb")] exI 1); |
1465 | 587 |
by (rtac conjI 1); |
1300 | 588 |
by (dres_inst_tac [("x","ma")] fun_cong 2); |
3018 | 589 |
by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2); |
2525 | 590 |
by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1); |
591 |
by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1); |
|
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
592 |
by (res_inst_tac [("A2","($ Sa ($ S A))")] |
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
593 |
((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); |
3018 | 594 |
by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1); |
2525 | 595 |
by (rtac eq_free_eq_subst_scheme_list 1); |
3018 | 596 |
by ( safe_tac HOL_cs ); |
1300 | 597 |
by (subgoal_tac "ma ~= na" 1); |
598 |
by ((forward_tac [new_tv_W] 2) THEN (atac 2)); |
|
1465 | 599 |
by (etac conjE 2); |
2525 | 600 |
by (dtac new_tv_subst_scheme_list 2); |
601 |
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2); |
|
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
602 |
by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2); |
1465 | 603 |
by (etac conjE 2); |
2525 | 604 |
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2779
diff
changeset
|
605 |
by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD, |
1300 | 606 |
new_tv_not_free_tv]) 2); |
2525 | 607 |
by (case_tac "na: free_tv t - free_tv Sa" 1); |
608 |
(* case na ~: free_tv t - free_tv Sa *) |
|
1300 | 609 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); |
2525 | 610 |
(* case na : free_tv t - free_tv Sa *) |
1300 | 611 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
2525 | 612 |
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); |
613 |
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans), |
|
614 |
eq_subst_scheme_list_eq_free] addss ((!simpset addsimps |
|
615 |
[free_tv_subst,dom_def]))) 1); |
|
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset
|
616 |
by (Fast_tac 1); |
2525 | 617 |
(* case Let e1 e2 *) |
618 |
by (eresolve_tac has_type_casesE 1); |
|
619 |
by (eres_inst_tac [("x","S'")] allE 1); |
|
620 |
by (eres_inst_tac [("x","A")] allE 1); |
|
621 |
by (eres_inst_tac [("x","t1")] allE 1); |
|
622 |
by (eres_inst_tac [("x","n")] allE 1); |
|
623 |
by (mp_tac 1); |
|
624 |
by (mp_tac 1); |
|
625 |
by (safe_tac HOL_cs); |
|
626 |
by (Asm_simp_tac 1); |
|
627 |
by (eres_inst_tac [("x","R")] allE 1); |
|
628 |
by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1); |
|
629 |
by (eres_inst_tac [("x","t'")] allE 1); |
|
630 |
by (eres_inst_tac [("x","m")] allE 1); |
|
631 |
by (rotate_tac 4 1); |
|
632 |
by (Asm_full_simp_tac 1); |
|
633 |
by (dtac mp 1); |
|
634 |
by (rtac has_type_le_env 1); |
|
3018 | 635 |
by (assume_tac 1); |
2525 | 636 |
by (Simp_tac 1); |
637 |
by (rtac gen_bound_typ_instance 1); |
|
638 |
by (dtac mp 1); |
|
639 |
by (forward_tac [new_tv_compatible_W] 1); |
|
640 |
by (rtac sym 1); |
|
3018 | 641 |
by (assume_tac 1); |
2525 | 642 |
by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1); |
643 |
by (safe_tac HOL_cs); |
|
644 |
by (Asm_full_simp_tac 1); |
|
645 |
by (res_inst_tac [("x","Ra")] exI 1); |
|
646 |
by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1); |
|
1525 | 647 |
qed_spec_mp "W_complete_lemma"; |
648 |
||
649 |
goal W.thy |
|
2525 | 650 |
"!!e. [] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \ |
651 |
\ (? R. t' = $ R t))"; |
|
3018 | 652 |
by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")] |
1525 | 653 |
W_complete_lemma 1); |
3018 | 654 |
by (ALLGOALS Asm_full_simp_tac); |
1525 | 655 |
qed "W_complete"; |