author  nipkow 
Mon, 03 Nov 1997 09:58:06 +0100  
changeset 4072  d0d32dd77440 
parent 4033  43ec35b5054d 
child 4089  96fba19bcbe2 
permissions  rwrr 
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) *) 

4072  21 
by (simp_tac (!simpset addsplits [split_option_bind,expand_if]) 1); 
1300  22 
(* case Abs e *) 
4072  23 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
1300  24 
by (fast_tac (HOL_cs addDs [Suc_leD]) 1); 
25 
(* case App e1 e2 *) 

4072  26 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
4033  27 
by(blast_tac (!claset addIs [le_SucI,le_trans]) 1); 
2525  28 
(* case LET e1 e2 *) 
4072  29 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
4033  30 
by(blast_tac (!claset addIs [le_trans]) 1); 
1486  31 
qed_spec_mp "W_var_ge"; 
1300  32 

33 
Addsimps [W_var_ge]; 

34 

35 
goal thy 

2525  36 
"!! s. Some (S,t,m) = W e A n ==> n<=m"; 
1300  37 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 
38 
qed "W_var_geD"; 

39 

2525  40 
goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"; 
41 
by (dtac W_var_geD 1); 

42 
by (rtac new_scheme_list_le 1); 

3018  43 
by (assume_tac 1); 
44 
by (assume_tac 1); 

2525  45 
qed "new_tv_compatible_W"; 
1300  46 

2525  47 
goal thy "!!sch. new_tv n sch > new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; 
48 
by (type_scheme.induct_tac "sch" 1); 

49 
by (Asm_full_simp_tac 1); 

50 
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); 

51 
by (strip_tac 1); 

52 
by (Asm_full_simp_tac 1); 

53 
by (etac conjE 1); 

54 
by (rtac conjI 1); 

55 
by (rtac new_tv_le 1); 

56 
by (mp_tac 2); 

57 
by (mp_tac 2); 

3018  58 
by (assume_tac 2); 
2525  59 
by (rtac add_le_mono 1); 
60 
by (Simp_tac 1); 

3919  61 
by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1); 
2525  62 
by (strip_tac 1); 
63 
by (rtac new_tv_le 1); 

64 
by (mp_tac 2); 

65 
by (mp_tac 2); 

3018  66 
by (assume_tac 2); 
2525  67 
by (rtac add_le_mono 1); 
68 
by (Simp_tac 1); 

3919  69 
by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1); 
2525  70 
by (strip_tac 1); 
71 
by (dtac not_leE 1); 

72 
by (rtac less_or_eq_imp_le 1); 

73 
by (Fast_tac 1); 

74 
qed_spec_mp "new_tv_bound_typ_inst_sch"; 

75 

76 
Addsimps [new_tv_bound_typ_inst_sch]; 

1300  77 

78 
(* resulting type variable is new *) 

79 
goal thy 

2525  80 
"!n A S t m. new_tv n A > W e A n = Some (S,t,m) > \ 
81 
\ new_tv m S & new_tv m t"; 

1300  82 
by (expr.induct_tac "e" 1); 
83 
(* case Var n *) 

4072  84 
by (simp_tac (!simpset addsplits [split_option_bind,expand_if]) 1); 
2525  85 
by (strip_tac 1); 
86 
by (dtac new_tv_nth_nat_A 1); 

3018  87 
by (assume_tac 1); 
4033  88 
by (Asm_simp_tac 1); 
1300  89 
(* case Abs e *) 
90 
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 

4072  91 
addsplits [split_option_bind]) 1); 
1300  92 
by (strip_tac 1); 
93 
by (eres_inst_tac [("x","Suc n")] allE 1); 

2525  94 
by (eres_inst_tac [("x","(FVar n)#A")] allE 1); 
1300  95 
by (fast_tac (HOL_cs addss (!simpset 
1465  96 
addsimps [new_tv_subst,new_tv_Suc_list])) 1); 
1300  97 
(* case App e1 e2 *) 
4072  98 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
1300  99 
by (strip_tac 1); 
4033  100 
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); 
1300  101 
by (eres_inst_tac [("x","n")] allE 1); 
2525  102 
by (eres_inst_tac [("x","A")] allE 1); 
4033  103 
by (eres_inst_tac [("x","S1")] allE 1); 
104 
by (eres_inst_tac [("x","t1")] allE 1); 

2525  105 
by (eres_inst_tac [("x","n1")] allE 1); 
106 
by (eres_inst_tac [("x","n1")] allE 1); 

107 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1); 

4033  108 
by (eres_inst_tac [("x","$S1 A")] allE 1); 
109 
by (eres_inst_tac [("x","S2")] allE 1); 

110 
by (eres_inst_tac [("x","t2")] allE 1); 

2525  111 
by (eres_inst_tac [("x","n2")] allE 1); 
3018  112 
by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1); 
1300  113 
by (rtac conjI 1); 
114 
by (rtac new_tv_subst_comp_2 1); 

115 
by (rtac new_tv_subst_comp_2 1); 

2525  116 
by (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
117 
by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 

118 
by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 1); 

1300  119 
by (Asm_simp_tac 1); 
120 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

2525  121 
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le]) 
1300  122 
1); 
1465  123 
by (etac (sym RS mgu_new) 1); 
2525  124 
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le, 
125 
new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 

126 
new_tv_subst_le,new_tv_le]) 1); 

127 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

128 
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 

129 
addss (!simpset)) 1); 

1465  130 
by (rtac (lessI RS new_tv_subst_var) 1); 
131 
by (etac (sym RS mgu_new) 1); 

1925  132 
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] 
2525  133 
addDs [W_var_geD] addIs 
134 
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS 

135 
new_tv_subst_le,new_tv_le] addss !simpset) 1); 

136 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

137 
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 

138 
addss (!simpset)) 1); 

4033  139 
(* 41: case LET e1 e2 *) 
4072  140 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
2525  141 
by (strip_tac 1); 
4033  142 
by(EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]); 
2525  143 
by (etac conjE 1); 
4033  144 
by(EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1, 
145 
etac impE 1, mp_tac 2]); 

146 
by (SELECT_GOAL(rewtac new_tv_def)1); 

147 
by (Asm_simp_tac 1); 

148 
by (REPEAT(dtac W_var_ge 1)); 

149 
by (rtac allI 1); 

150 
by (strip_tac 1); 

151 
by (SELECT_GOAL(rewtac free_tv_subst) 1); 

152 
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); 

153 
by (best_tac (!claset addEs [less_le_trans]) 1); 

2525  154 
by (etac conjE 1); 
155 
by (rtac conjI 1); 

156 
by (rtac new_tv_subst_comp_2 1); 

4033  157 
by (etac (W_var_ge RS new_tv_subst_le) 1); 
3018  158 
by (assume_tac 1); 
159 
by (assume_tac 1); 

160 
by (assume_tac 1); 

1486  161 
qed_spec_mp "new_tv_W"; 
1300  162 

2525  163 
goal thy "!!sch. (v ~: free_tv sch) > (v : free_tv (bound_typ_inst (TVar o S) sch)) > (? x. v = S x)"; 
164 
by (type_scheme.induct_tac "sch" 1); 

165 
by (Asm_full_simp_tac 1); 

166 
by (Asm_full_simp_tac 1); 

167 
by (strip_tac 1); 

168 
by (rtac exI 1); 

169 
by (rtac refl 1); 

170 
by (Asm_full_simp_tac 1); 

171 
qed_spec_mp "free_tv_bound_typ_inst1"; 

172 

173 
Addsimps [free_tv_bound_typ_inst1]; 

1300  174 

175 
goal thy 

2525  176 
"!n A S t m v. W e A n = Some (S,t,m) > \ 
177 
\ (v:free_tv S  v:free_tv t) > v<n > v:free_tv A"; 

1300  178 
by (expr.induct_tac "e" 1); 
179 
(* case Var n *) 

2525  180 
by (simp_tac (!simpset addsimps 
4072  181 
[free_tv_subst] addsplits [split_option_bind,expand_if]) 1); 
2525  182 
by (strip_tac 1); 
183 
by (case_tac "v : free_tv (nth nat A)" 1); 

184 
by (Asm_full_simp_tac 1); 

185 
by (dtac free_tv_bound_typ_inst1 1); 

186 
by (simp_tac (!simpset addsimps [o_def]) 1); 

187 
by (etac exE 1); 

188 
by (rotate_tac 3 1); 

189 
by (Asm_full_simp_tac 1); 

1300  190 
(* case Abs e *) 
191 
by (asm_full_simp_tac (!simpset addsimps 

4072  192 
[free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1); 
1300  193 
by (strip_tac 1); 
2525  194 
by (rename_tac "S t n1 S1 t1 m v" 1); 
1300  195 
by (eres_inst_tac [("x","Suc n")] allE 1); 
2525  196 
by (eres_inst_tac [("x","FVar n # A")] allE 1); 
197 
by (eres_inst_tac [("x","S")] allE 1); 

1300  198 
by (eres_inst_tac [("x","t")] allE 1); 
2525  199 
by (eres_inst_tac [("x","n1")] allE 1); 
1300  200 
by (eres_inst_tac [("x","v")] allE 1); 
2525  201 
by (best_tac (HOL_cs addIs [cod_app_subst] 
1669  202 
addss (!simpset addsimps [less_Suc_eq])) 1); 
1300  203 
(* case App e1 e2 *) 
4072  204 
by (simp_tac (!simpset addsplits [split_option_bind] delsimps all_simps) 1); 
1300  205 
by (strip_tac 1); 
2525  206 
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1); 
1300  207 
by (eres_inst_tac [("x","n")] allE 1); 
2525  208 
by (eres_inst_tac [("x","A")] allE 1); 
209 
by (eres_inst_tac [("x","S")] allE 1); 

1300  210 
by (eres_inst_tac [("x","t")] allE 1); 
2525  211 
by (eres_inst_tac [("x","n1")] allE 1); 
212 
by (eres_inst_tac [("x","n1")] allE 1); 

1300  213 
by (eres_inst_tac [("x","v")] allE 1); 
214 
(* second case *) 

2525  215 
by (eres_inst_tac [("x","$ S A")] allE 1); 
216 
by (eres_inst_tac [("x","S1")] allE 1); 

217 
by (eres_inst_tac [("x","t1")] allE 1); 

218 
by (eres_inst_tac [("x","n2")] allE 1); 

1300  219 
by (eres_inst_tac [("x","v")] allE 1); 
220 
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 

2525  221 
by (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1); 
1465  222 
by (dtac W_var_geD 1); 
223 
by (dtac W_var_geD 1); 

1300  224 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); 
225 
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 

2525  226 
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, 
1300  227 
less_le_trans,less_not_refl2,subsetD] 
228 
addEs [UnE] 

229 
addss !simpset) 1); 

230 
by (Asm_full_simp_tac 1); 

1465  231 
by (dtac (sym RS W_var_geD) 1); 
232 
by (dtac (sym RS W_var_geD) 1); 

1300  233 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); 
234 
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, 

2525  235 
free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, 
236 
less_le_trans,subsetD] 

237 
addEs [UnE] 

238 
addss !simpset) 1); 

239 
(* LET e1 e2 *) 

4072  240 
by (simp_tac (!simpset addsplits [split_option_bind] delsimps all_simps) 1); 
2525  241 
by (strip_tac 1); 
242 
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1); 

243 
by (eres_inst_tac [("x","nat")] allE 1); 

244 
by (eres_inst_tac [("x","A")] allE 1); 

245 
by (eres_inst_tac [("x","S1")] allE 1); 

246 
by (eres_inst_tac [("x","t1")] allE 1); 

247 
by (rotate_tac 1 1); 

248 
by (eres_inst_tac [("x","n2")] allE 1); 

249 
by (rotate_tac 4 1); 

250 
by (eres_inst_tac [("x","v")] allE 1); 

251 
by (mp_tac 1); 

252 
by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]); 

253 
by (mp_tac 1); 

254 
by (Asm_full_simp_tac 1); 

255 
by (rtac conjI 1); 

256 
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 

257 
addDs [less_le_trans]) 1); 

258 
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 

259 
addDs [less_le_trans]) 1); 

1486  260 
qed_spec_mp "free_tv_W"; 
1300  261 

2525  262 
goal thy "!!A. (!x. x : A > x ~: B) ==> A Int B = {}"; 
263 
by (Fast_tac 1); 

2625  264 
val weaken_A_Int_B_eq_empty = result(); 
2525  265 

266 
goal thy "!!A. x ~: A  x : B ==> x ~: A  B"; 

267 
by (Fast_tac 1); 

2625  268 
val weaken_not_elem_A_minus_B = result(); 
2525  269 

270 
(* correctness of W with respect to has_type *) 

271 
goal W.thy 

272 
"!A S t m n . new_tv n A > Some (S,t,m) = W e A n > $S A  e :: t"; 

273 
by (expr.induct_tac "e" 1); 

274 
(* case Var n *) 

3919  275 
by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1); 
2525  276 
by (strip_tac 1); 
277 
by (rtac has_type.VarI 1); 

278 
by (Simp_tac 1); 

279 
by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1); 

280 
by (rtac exI 1); 

281 
by (rtac refl 1); 

282 
(* case Abs e *) 

283 
by (asm_full_simp_tac (!simpset addsimps [app_subst_list] 

4072  284 
addsplits [split_option_bind]) 1); 
2525  285 
by (strip_tac 1); 
286 
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1); 

287 
by (Asm_full_simp_tac 1); 

288 
by (rtac has_type.AbsI 1); 

289 
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1); 

3018  290 
by (dtac sym 1); 
2525  291 
by (REPEAT (etac allE 1)); 
292 
by (etac impE 1); 

293 
by (mp_tac 2); 

294 
by (Asm_simp_tac 1); 

3018  295 
by (assume_tac 1); 
2525  296 
(* case App e1 e2 *) 
4072  297 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
2525  298 
by (strip_tac 1); 
299 
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); 

300 
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1); 

301 
by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1); 

302 
by (rtac (app_subst_Fun RS subst) 1); 

303 
by (res_inst_tac [("t","$S3 (t2 > (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1); 

304 
by (Asm_full_simp_tac 1); 

305 
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); 

306 
by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1)); 

307 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 

308 
by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); 

309 
by (rtac (has_type_cl_sub RS spec) 1); 

310 
by (forward_tac [new_tv_W] 1); 

3018  311 
by (assume_tac 1); 
2525  312 
by (dtac conjunct1 1); 
313 
by (dtac conjunct1 1); 

314 
by (forward_tac [new_tv_subst_scheme_list] 1); 

315 
by (rtac new_scheme_list_le 1); 

316 
by (rtac W_var_ge 1); 

3018  317 
by (assume_tac 1); 
318 
by (assume_tac 1); 

2525  319 
by (etac thin_rl 1); 
320 
by (REPEAT (etac allE 1)); 

3018  321 
by (dtac sym 1); 
322 
by (dtac sym 1); 

2525  323 
by (etac thin_rl 1); 
324 
by (etac thin_rl 1); 

325 
by (mp_tac 1); 

326 
by (mp_tac 1); 

3018  327 
by (assume_tac 1); 
2525  328 
(* case Let e1 e2 *) 
4072  329 
by (simp_tac (!simpset addsplits [split_option_bind]) 1); 
2525  330 
by (strip_tac 1); 
331 
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 

332 
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1); 

333 
by (simp_tac (!simpset addsimps [o_def]) 1); 

334 
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); 

335 
by (rtac (has_type_cl_sub RS spec) 1); 

336 
by (dres_inst_tac [("x","A")] spec 1); 

337 
by (dres_inst_tac [("x","S1")] spec 1); 

338 
by (dres_inst_tac [("x","t1")] spec 1); 

339 
by (dres_inst_tac [("x","m2")] spec 1); 

340 
by (rotate_tac 4 1); 

341 
by (dres_inst_tac [("x","m1")] spec 1); 

342 
by (mp_tac 1); 

343 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 

344 
by (simp_tac (!simpset addsimps [o_def]) 1); 

345 
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); 

346 
by (rtac (gen_subst_commutes RS sym RS subst) 1); 

347 
by (rtac (app_subst_Cons RS subst) 2); 

348 
by (etac thin_rl 2); 

349 
by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2); 

350 
by (dres_inst_tac [("x","S2")] spec 2); 

351 
by (dres_inst_tac [("x","t")] spec 2); 

352 
by (dres_inst_tac [("x","n2")] spec 2); 

353 
by (dres_inst_tac [("x","m2")] spec 2); 

354 
by (forward_tac [new_tv_W] 2); 

3018  355 
by (assume_tac 2); 
2525  356 
by (dtac conjunct1 2); 
357 
by (dtac conjunct1 2); 

358 
by (forward_tac [new_tv_subst_scheme_list] 2); 

359 
by (rtac new_scheme_list_le 2); 

360 
by (rtac W_var_ge 2); 

3018  361 
by (assume_tac 2); 
362 
by (assume_tac 2); 

2525  363 
by (etac impE 2); 
364 
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2); 

365 
by (Simp_tac 2); 

366 
by (Fast_tac 2); 

3018  367 
by (assume_tac 2); 
2525  368 
by (Asm_full_simp_tac 2); 
369 
by (rtac weaken_A_Int_B_eq_empty 1); 

370 
by (rtac allI 1); 

371 
by (strip_tac 1); 

372 
by (rtac weaken_not_elem_A_minus_B 1); 

373 
by (case_tac "x < m2" 1); 

374 
by (rtac disjI2 1); 

375 
by (rtac (free_tv_gen_cons RS subst) 1); 

376 
by (rtac free_tv_W 1); 

3018  377 
by (assume_tac 1); 
2525  378 
by (Asm_full_simp_tac 1); 
3018  379 
by (assume_tac 1); 
2525  380 
by (rtac disjI1 1); 
381 
by (dtac new_tv_W 1); 

3018  382 
by (assume_tac 1); 
2525  383 
by (dtac conjunct2 1); 
384 
by (dtac conjunct2 1); 

385 
by (rtac new_tv_not_free_tv 1); 

386 
by (rtac new_tv_le 1); 

3018  387 
by (assume_tac 2); 
2525  388 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1); 
389 
qed_spec_mp "W_correct_lemma"; 

390 

391 
goal Arith.thy "!!n::nat. ~ k+n < n"; 

392 
by (nat_ind_tac "k" 1); 

3018  393 
by (ALLGOALS Asm_simp_tac); 
394 
by (trans_tac 1); 

2625  395 
val not_add_less1 = result(); 
2525  396 
Addsimps [not_add_less1]; 
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

397 

1300  398 
(* Completeness of W w.r.t. has_type *) 
399 
goal thy 

2525  400 
"!S' A t' n. $S' A  e :: t' > new_tv n A > \ 
401 
\ (? S t. (? m. W e A n = Some (S,t,m)) & \ 

402 
\ (? R. $S' A = $R ($S A) & t' = $R t))"; 

1300  403 
by (expr.induct_tac "e" 1); 
404 
(* case Var n *) 

405 
by (strip_tac 1); 

3919  406 
by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1); 
1300  407 
by (eresolve_tac has_type_casesE 1); 
2525  408 
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1); 
409 
by (etac exE 1); 

410 
by (hyp_subst_tac 1); 

411 
by (rename_tac "S" 1); 

412 
by (res_inst_tac [("x","%x. (if x < n then S' x else S (x  n))")] exI 1); 

413 
by (rtac conjI 1); 

1300  414 
by (Asm_simp_tac 1); 
2525  415 
by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
416 
delsimps [bound_typ_inst_composed_subst]) 1); 

2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

417 
(** LEVEL 12 **) 
1300  418 
(* case Abs e *) 
419 
by (strip_tac 1); 

420 
by (eresolve_tac has_type_casesE 1); 

3842  421 
by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1); 
2525  422 
by (eres_inst_tac [("x","(FVar n)#A")] allE 1); 
1300  423 
by (eres_inst_tac [("x","t2")] allE 1); 
424 
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

425 
by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
3207  426 
addss (!simpset addcongs [conj_cong] 
4072  427 
addsplits [split_option_bind])) 1); 
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

428 
(** LEVEL 19 **) 
1300  429 

430 
(* case App e1 e2 *) 

431 
by (strip_tac 1); 

432 
by (eresolve_tac has_type_casesE 1); 

2525  433 
by (eres_inst_tac [("x","S'")] allE 1); 
434 
by (eres_inst_tac [("x","A")] allE 1); 

1400  435 
by (eres_inst_tac [("x","t2 > t'")] allE 1); 
1300  436 
by (eres_inst_tac [("x","n")] allE 1); 
437 
by (safe_tac HOL_cs); 

2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

438 
(** LEVEL 26 **) 
2525  439 
by (eres_inst_tac [("x","R")] allE 1); 
440 
by (eres_inst_tac [("x","$ S A")] allE 1); 

1300  441 
by (eres_inst_tac [("x","t2")] allE 1); 
442 
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

443 
by (rotate_tac ~3 1); 
1300  444 
by (Asm_full_simp_tac 1); 
445 
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

446 
by (contr_tac 1); 
1300  447 
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS 
2525  448 
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

449 
(** LEVEL 35 **) 
1300  450 
by (subgoal_tac 
3842  451 
"$ (%x. if x=ma then t' else (if x:(free_tv t  free_tv Sa) then R x \ 
2525  452 
\ else Ra x)) ($ Sa t) = \ 
3842  453 
\ $ (%x. if x=ma then t' else (if x:(free_tv t  free_tv Sa) then R x \ 
2525  454 
\ else Ra x)) (ta > (TVar ma))" 1); 
1300  455 
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ 
2525  456 
\ (if x:(free_tv t  free_tv Sa) then R x else Ra x)) ($ Sa t)"), 
457 
("s","($ Ra ta) > t'")] ssubst 2); 

1300  458 
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2); 
1465  459 
by (rtac eq_free_eq_subst_te 2); 
1300  460 
by (strip_tac 2); 
461 
by (subgoal_tac "na ~=ma" 2); 

2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

462 
by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, 
2525  463 
new_tv_not_free_tv,new_tv_le]) 3); 
464 
by (case_tac "na:free_tv Sa" 2); 

465 
(* n1 ~: free_tv S1 *) 

466 
by (forward_tac [not_free_impl_id] 3); 

3919  467 
by (asm_simp_tac (!simpset addsplits [expand_if]) 3); 
2525  468 
(* na : free_tv Sa *) 
469 
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); 

470 
by (dtac eq_subst_scheme_list_eq_free 2); 

1300  471 
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); 
472 
by (Asm_simp_tac 2); 

2525  473 
by (case_tac "na:dom Sa" 2); 
474 
(* na ~: dom Sa *) 

3919  475 
by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3); 
2525  476 
(* na : dom Sa *) 
1465  477 
by (rtac eq_free_eq_subst_te 2); 
1300  478 
by (strip_tac 2); 
479 
by (subgoal_tac "nb ~= ma" 2); 

480 
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); 

1465  481 
by (etac conjE 3); 
2525  482 
by (dtac new_tv_subst_scheme_list 3); 
483 
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3); 

1300  484 
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
2525  485 
(!simpset addsimps [cod_def,free_tv_subst])) 3); 
1300  486 
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
3919  487 
addsplits [expand_if])) 2); 
1300  488 
by (Simp_tac 2); 
1465  489 
by (rtac eq_free_eq_subst_te 2); 
1300  490 
by (strip_tac 2 ); 
491 
by (subgoal_tac "na ~= ma" 2); 

492 
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); 

1465  493 
by (etac conjE 3); 
494 
by (dtac (sym RS W_var_geD) 3); 

2525  495 
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3); 
496 
by (case_tac "na: free_tv t  free_tv Sa" 2); 

497 
(* case na ~: free_tv t  free_tv Sa *) 

3919  498 
by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3); 
2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

499 
by (Fast_tac 3); 
2525  500 
(* case na : free_tv t  free_tv Sa *) 
3919  501 
by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2); 
2525  502 
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); 
503 
by (dtac eq_subst_scheme_list_eq_free 2); 

1300  504 
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 etacontract any longer.
nipkow
parents:
2779
diff
changeset

505 
(** LEVEL 75 **) 
2525  506 
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2); 
4072  507 
by (asm_simp_tac (!simpset addsplits [split_option_bind]) 1); 
1300  508 
by (safe_tac HOL_cs ); 
2525  509 
by (dtac mgu_Some 1); 
3018  510 
by ( fast_tac (HOL_cs addss !simpset) 1); 
2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

511 
(** LEVEL 80 *) 
1300  512 
by ((dtac mgu_mg 1) THEN (atac 1)); 
1465  513 
by (etac exE 1); 
2525  514 
by (res_inst_tac [("x","Rb")] exI 1); 
1465  515 
by (rtac conjI 1); 
1300  516 
by (dres_inst_tac [("x","ma")] fun_cong 2); 
3018  517 
by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2); 
2525  518 
by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1); 
519 
by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1); 

2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

520 
by (res_inst_tac [("A2","($ Sa ($ S A))")] 
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

521 
((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); 
3018  522 
by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1); 
2525  523 
by (rtac eq_free_eq_subst_scheme_list 1); 
3018  524 
by ( safe_tac HOL_cs ); 
1300  525 
by (subgoal_tac "ma ~= na" 1); 
526 
by ((forward_tac [new_tv_W] 2) THEN (atac 2)); 

1465  527 
by (etac conjE 2); 
2525  528 
by (dtac new_tv_subst_scheme_list 2); 
529 
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 etacontract any longer.
nipkow
parents:
2779
diff
changeset

530 
by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2); 
1465  531 
by (etac conjE 2); 
2525  532 
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2); 
2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

533 
by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD, 
1300  534 
new_tv_not_free_tv]) 2); 
2525  535 
by (case_tac "na: free_tv t  free_tv Sa" 1); 
536 
(* case na ~: free_tv t  free_tv Sa *) 

3919  537 
by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2); 
2525  538 
(* case na : free_tv t  free_tv Sa *) 
3919  539 
by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1); 
2525  540 
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); 
541 
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans), 

542 
eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 

543 
[free_tv_subst,dom_def]))) 1); 

2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

544 
by (Fast_tac 1); 
2525  545 
(* case Let e1 e2 *) 
546 
by (eresolve_tac has_type_casesE 1); 

547 
by (eres_inst_tac [("x","S'")] allE 1); 

548 
by (eres_inst_tac [("x","A")] allE 1); 

549 
by (eres_inst_tac [("x","t1")] allE 1); 

550 
by (eres_inst_tac [("x","n")] allE 1); 

551 
by (mp_tac 1); 

552 
by (mp_tac 1); 

553 
by (safe_tac HOL_cs); 

554 
by (Asm_simp_tac 1); 

555 
by (eres_inst_tac [("x","R")] allE 1); 

556 
by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1); 

557 
by (eres_inst_tac [("x","t'")] allE 1); 

558 
by (eres_inst_tac [("x","m")] allE 1); 

559 
by (rotate_tac 4 1); 

560 
by (Asm_full_simp_tac 1); 

561 
by (dtac mp 1); 

562 
by (rtac has_type_le_env 1); 

3018  563 
by (assume_tac 1); 
2525  564 
by (Simp_tac 1); 
565 
by (rtac gen_bound_typ_instance 1); 

566 
by (dtac mp 1); 

567 
by (forward_tac [new_tv_compatible_W] 1); 

568 
by (rtac sym 1); 

3018  569 
by (assume_tac 1); 
2525  570 
by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1); 
571 
by (safe_tac HOL_cs); 

572 
by (Asm_full_simp_tac 1); 

573 
by (res_inst_tac [("x","Ra")] exI 1); 

574 
by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1); 

1525  575 
qed_spec_mp "W_complete_lemma"; 
576 

577 
goal W.thy 

2525  578 
"!!e. []  e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \ 
579 
\ (? R. t' = $ R t))"; 

3018  580 
by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")] 
1525  581 
W_complete_lemma 1); 
3018  582 
by (ALLGOALS Asm_full_simp_tac); 
1525  583 
qed "W_complete"; 