author  berghofe 
Fri, 24 Jul 1998 13:19:38 +0200  
changeset 5184  9b8547a9496a 
parent 5118  6b995dad8a9d 
child 5348  5f6416d64a94 
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 *) 

5069  17 
Goal 
2525  18 
"!A n S t m. W e A n = Some (S,t,m) > n<=m"; 
5184  19 
by (induct_tac "e" 1); 
1300  20 
(* case Var(n) *) 
4686  21 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
1300  22 
(* case Abs e *) 
4089  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 *) 

4089  26 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
4423  27 
by (blast_tac (claset() addIs [le_SucI,le_trans]) 1); 
2525  28 
(* case LET e1 e2 *) 
4089  29 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
4423  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 

5069  35 
Goal 
5118  36 
"Some (S,t,m) = W e A n ==> n<=m"; 
4089  37 
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); 
1300  38 
qed "W_var_geD"; 
39 

5118  40 
Goal "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"; 
2525  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 

5118  47 
Goal "new_tv n sch > new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; 
5184  48 
by (induct_tac "sch" 1); 
4727  49 
by (Asm_full_simp_tac 1); 
50 
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); 

2525  51 
by (strip_tac 1); 
52 
by (Asm_full_simp_tac 1); 

53 
by (etac conjE 1); 

54 
by (rtac conjI 1); 

4727  55 
by (rtac new_tv_le 1); 
56 
by (assume_tac 2); 

57 
by (rtac add_le_mono 1); 

58 
by (Simp_tac 1); 

59 
by (simp_tac (simpset() addsimps [max_def]) 1); 

2525  60 
by (rtac new_tv_le 1); 
4727  61 
by (assume_tac 2); 
2525  62 
by (rtac add_le_mono 1); 
4727  63 
by (Simp_tac 1); 
4686  64 
by (simp_tac (simpset() addsimps [max_def]) 1); 
2525  65 
by (strip_tac 1); 
66 
by (dtac not_leE 1); 

67 
by (rtac less_or_eq_imp_le 1); 

68 
by (Fast_tac 1); 

69 
qed_spec_mp "new_tv_bound_typ_inst_sch"; 

70 

71 
Addsimps [new_tv_bound_typ_inst_sch]; 

1300  72 

73 
(* resulting type variable is new *) 

5069  74 
Goal 
2525  75 
"!n A S t m. new_tv n A > W e A n = Some (S,t,m) > \ 
76 
\ new_tv m S & new_tv m t"; 

5184  77 
by (induct_tac "e" 1); 
1300  78 
(* case Var n *) 
4686  79 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
2525  80 
by (strip_tac 1); 
81 
by (dtac new_tv_nth_nat_A 1); 

3018  82 
by (assume_tac 1); 
4033  83 
by (Asm_simp_tac 1); 
1300  84 
(* case Abs e *) 
4089  85 
by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
4072  86 
addsplits [split_option_bind]) 1); 
1300  87 
by (strip_tac 1); 
88 
by (eres_inst_tac [("x","Suc n")] allE 1); 

2525  89 
by (eres_inst_tac [("x","(FVar n)#A")] allE 1); 
4089  90 
by (fast_tac (HOL_cs addss (simpset() 
1465  91 
addsimps [new_tv_subst,new_tv_Suc_list])) 1); 
1300  92 
(* case App e1 e2 *) 
4089  93 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
1300  94 
by (strip_tac 1); 
4033  95 
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); 
1300  96 
by (eres_inst_tac [("x","n")] allE 1); 
2525  97 
by (eres_inst_tac [("x","A")] allE 1); 
4033  98 
by (eres_inst_tac [("x","S1")] allE 1); 
99 
by (eres_inst_tac [("x","t1")] allE 1); 

2525  100 
by (eres_inst_tac [("x","n1")] allE 1); 
101 
by (eres_inst_tac [("x","n1")] allE 1); 

4089  102 
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv] delsimps all_simps) 1); 
4033  103 
by (eres_inst_tac [("x","$S1 A")] allE 1); 
104 
by (eres_inst_tac [("x","S2")] allE 1); 

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

2525  106 
by (eres_inst_tac [("x","n2")] allE 1); 
4089  107 
by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Some]) 1); 
1300  108 
by (rtac conjI 1); 
109 
by (rtac new_tv_subst_comp_2 1); 

110 
by (rtac new_tv_subst_comp_2 1); 

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

4089  113 
by (asm_full_simp_tac (simpset() addsimps [rotate_Some]) 1); 
1300  114 
by (Asm_simp_tac 1); 
115 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

2525  116 
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le]) 
1300  117 
1); 
1465  118 
by (etac (sym RS mgu_new) 1); 
2525  119 
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le, 
120 
new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 

121 
new_tv_subst_le,new_tv_le]) 1); 

122 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

123 
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 

4089  124 
addss (simpset())) 1); 
1465  125 
by (rtac (lessI RS new_tv_subst_var) 1); 
126 
by (etac (sym RS mgu_new) 1); 

1925  127 
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] 
2525  128 
addDs [W_var_geD] addIs 
129 
[new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS 

4089  130 
new_tv_subst_le,new_tv_le] addss simpset()) 1); 
2525  131 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 
132 
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 

4089  133 
addss (simpset())) 1); 
4033  134 
(* 41: case LET e1 e2 *) 
4089  135 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
2525  136 
by (strip_tac 1); 
4423  137 
by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]); 
2525  138 
by (etac conjE 1); 
4423  139 
by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1, 
4033  140 
etac impE 1, mp_tac 2]); 
141 
by (SELECT_GOAL(rewtac new_tv_def)1); 

142 
by (Asm_simp_tac 1); 

143 
by (REPEAT(dtac W_var_ge 1)); 

144 
by (rtac allI 1); 

145 
by (strip_tac 1); 

146 
by (SELECT_GOAL(rewtac free_tv_subst) 1); 

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

4089  148 
by (best_tac (claset() addEs [less_le_trans]) 1); 
2525  149 
by (etac conjE 1); 
150 
by (rtac conjI 1); 

151 
by (rtac new_tv_subst_comp_2 1); 

4033  152 
by (etac (W_var_ge RS new_tv_subst_le) 1); 
3018  153 
by (assume_tac 1); 
154 
by (assume_tac 1); 

155 
by (assume_tac 1); 

1486  156 
qed_spec_mp "new_tv_W"; 
1300  157 

5118  158 
Goal "(v ~: free_tv sch) > (v : free_tv (bound_typ_inst (TVar o S) sch)) > (? x. v = S x)"; 
5184  159 
by (induct_tac "sch" 1); 
2525  160 
by (Asm_full_simp_tac 1); 
161 
by (Asm_full_simp_tac 1); 

162 
by (strip_tac 1); 

163 
by (rtac exI 1); 

164 
by (rtac refl 1); 

165 
by (Asm_full_simp_tac 1); 

166 
qed_spec_mp "free_tv_bound_typ_inst1"; 

167 

168 
Addsimps [free_tv_bound_typ_inst1]; 

1300  169 

5069  170 
Goal 
2525  171 
"!n A S t m v. W e A n = Some (S,t,m) > \ 
172 
\ (v:free_tv S  v:free_tv t) > v<n > v:free_tv A"; 

5184  173 
by (induct_tac "e" 1); 
1300  174 
(* case Var n *) 
4089  175 
by (simp_tac (simpset() addsimps 
4686  176 
[free_tv_subst] addsplits [split_option_bind]) 1); 
2525  177 
by (strip_tac 1); 
4502  178 
by (case_tac "v : free_tv (A!nat)" 1); 
2525  179 
by (Asm_full_simp_tac 1); 
180 
by (dtac free_tv_bound_typ_inst1 1); 

4089  181 
by (simp_tac (simpset() addsimps [o_def]) 1); 
2525  182 
by (etac exE 1); 
183 
by (rotate_tac 3 1); 

184 
by (Asm_full_simp_tac 1); 

1300  185 
(* case Abs e *) 
4089  186 
by (asm_full_simp_tac (simpset() addsimps 
4072  187 
[free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1); 
1300  188 
by (strip_tac 1); 
2525  189 
by (rename_tac "S t n1 S1 t1 m v" 1); 
1300  190 
by (eres_inst_tac [("x","Suc n")] allE 1); 
2525  191 
by (eres_inst_tac [("x","FVar n # A")] allE 1); 
192 
by (eres_inst_tac [("x","S")] allE 1); 

1300  193 
by (eres_inst_tac [("x","t")] allE 1); 
2525  194 
by (eres_inst_tac [("x","n1")] allE 1); 
1300  195 
by (eres_inst_tac [("x","v")] allE 1); 
2525  196 
by (best_tac (HOL_cs addIs [cod_app_subst] 
4089  197 
addss (simpset() addsimps [less_Suc_eq])) 1); 
1300  198 
(* case App e1 e2 *) 
4089  199 
by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); 
1300  200 
by (strip_tac 1); 
2525  201 
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1); 
1300  202 
by (eres_inst_tac [("x","n")] allE 1); 
2525  203 
by (eres_inst_tac [("x","A")] allE 1); 
204 
by (eres_inst_tac [("x","S")] allE 1); 

1300  205 
by (eres_inst_tac [("x","t")] allE 1); 
2525  206 
by (eres_inst_tac [("x","n1")] allE 1); 
207 
by (eres_inst_tac [("x","n1")] allE 1); 

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

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

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

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

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

4089  216 
by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1); 
1465  217 
by (dtac W_var_geD 1); 
218 
by (dtac W_var_geD 1); 

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

2525  221 
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, 
1300  222 
less_le_trans,less_not_refl2,subsetD] 
223 
addEs [UnE] 

4089  224 
addss simpset()) 1); 
1300  225 
by (Asm_full_simp_tac 1); 
1465  226 
by (dtac (sym RS W_var_geD) 1); 
227 
by (dtac (sym RS W_var_geD) 1); 

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

2525  230 
free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, 
231 
less_le_trans,subsetD] 

232 
addEs [UnE] 

4089  233 
addss simpset()) 1); 
2525  234 
(* LET e1 e2 *) 
4089  235 
by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); 
2525  236 
by (strip_tac 1); 
237 
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1); 

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

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

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

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

242 
by (rotate_tac 1 1); 

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

244 
by (rotate_tac 4 1); 

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

246 
by (mp_tac 1); 

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

248 
by (mp_tac 1); 

249 
by (Asm_full_simp_tac 1); 

250 
by (rtac conjI 1); 

4089  251 
by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
2525  252 
addDs [less_le_trans]) 1); 
4089  253 
by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
2525  254 
addDs [less_le_trans]) 1); 
1486  255 
qed_spec_mp "free_tv_W"; 
1300  256 

5118  257 
Goal "(!x. x : A > x ~: B) ==> A Int B = {}"; 
2525  258 
by (Fast_tac 1); 
2625  259 
val weaken_A_Int_B_eq_empty = result(); 
2525  260 

5118  261 
Goal "x ~: A  x : B ==> x ~: A  B"; 
2525  262 
by (Fast_tac 1); 
2625  263 
val weaken_not_elem_A_minus_B = result(); 
2525  264 

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

5069  266 
Goal 
2525  267 
"!A S t m n . new_tv n A > Some (S,t,m) = W e A n > $S A  e :: t"; 
5184  268 
by (induct_tac "e" 1); 
2525  269 
(* case Var n *) 
4686  270 
by (Asm_full_simp_tac 1); 
2525  271 
by (strip_tac 1); 
272 
by (rtac has_type.VarI 1); 

273 
by (Simp_tac 1); 

4089  274 
by (simp_tac (simpset() addsimps [is_bound_typ_instance]) 1); 
2525  275 
by (rtac exI 1); 
276 
by (rtac refl 1); 

277 
(* case Abs e *) 

4089  278 
by (asm_full_simp_tac (simpset() addsimps [app_subst_list] 
4072  279 
addsplits [split_option_bind]) 1); 
2525  280 
by (strip_tac 1); 
281 
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1); 

282 
by (Asm_full_simp_tac 1); 

283 
by (rtac has_type.AbsI 1); 

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

3018  285 
by (dtac sym 1); 
2525  286 
by (REPEAT (etac allE 1)); 
287 
by (etac impE 1); 

288 
by (mp_tac 2); 

289 
by (Asm_simp_tac 1); 

3018  290 
by (assume_tac 1); 
2525  291 
(* case App e1 e2 *) 
4089  292 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
2525  293 
by (strip_tac 1); 
294 
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); 

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

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

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

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

299 
by (Asm_full_simp_tac 1); 

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

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

4089  302 
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); 
303 
by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); 

2525  304 
by (rtac (has_type_cl_sub RS spec) 1); 
305 
by (forward_tac [new_tv_W] 1); 

3018  306 
by (assume_tac 1); 
2525  307 
by (dtac conjunct1 1); 
308 
by (dtac conjunct1 1); 

309 
by (forward_tac [new_tv_subst_scheme_list] 1); 

310 
by (rtac new_scheme_list_le 1); 

311 
by (rtac W_var_ge 1); 

3018  312 
by (assume_tac 1); 
313 
by (assume_tac 1); 

2525  314 
by (etac thin_rl 1); 
315 
by (REPEAT (etac allE 1)); 

3018  316 
by (dtac sym 1); 
317 
by (dtac sym 1); 

2525  318 
by (etac thin_rl 1); 
319 
by (etac thin_rl 1); 

320 
by (mp_tac 1); 

321 
by (mp_tac 1); 

3018  322 
by (assume_tac 1); 
2525  323 
(* case Let e1 e2 *) 
4089  324 
by (simp_tac (simpset() addsplits [split_option_bind]) 1); 
2525  325 
by (strip_tac 1); 
326 
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 

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

4089  328 
by (simp_tac (simpset() addsimps [o_def]) 1); 
2525  329 
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); 
330 
by (rtac (has_type_cl_sub RS spec) 1); 

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

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

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

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

335 
by (rotate_tac 4 1); 

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

337 
by (mp_tac 1); 

4089  338 
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); 
339 
by (simp_tac (simpset() addsimps [o_def]) 1); 

2525  340 
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1); 
341 
by (rtac (gen_subst_commutes RS sym RS subst) 1); 

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

343 
by (etac thin_rl 2); 

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

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

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

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

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

349 
by (forward_tac [new_tv_W] 2); 

3018  350 
by (assume_tac 2); 
2525  351 
by (dtac conjunct1 2); 
352 
by (dtac conjunct1 2); 

353 
by (forward_tac [new_tv_subst_scheme_list] 2); 

354 
by (rtac new_scheme_list_le 2); 

355 
by (rtac W_var_ge 2); 

3018  356 
by (assume_tac 2); 
357 
by (assume_tac 2); 

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

360 
by (Simp_tac 2); 

361 
by (Fast_tac 2); 

3018  362 
by (assume_tac 2); 
2525  363 
by (Asm_full_simp_tac 2); 
364 
by (rtac weaken_A_Int_B_eq_empty 1); 

365 
by (rtac allI 1); 

366 
by (strip_tac 1); 

367 
by (rtac weaken_not_elem_A_minus_B 1); 

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

369 
by (rtac disjI2 1); 

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

371 
by (rtac free_tv_W 1); 

3018  372 
by (assume_tac 1); 
2525  373 
by (Asm_full_simp_tac 1); 
3018  374 
by (assume_tac 1); 
2525  375 
by (rtac disjI1 1); 
376 
by (dtac new_tv_W 1); 

3018  377 
by (assume_tac 1); 
2525  378 
by (dtac conjunct2 1); 
379 
by (dtac conjunct2 1); 

380 
by (rtac new_tv_not_free_tv 1); 

381 
by (rtac new_tv_le 1); 

3018  382 
by (assume_tac 2); 
4089  383 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1); 
2525  384 
qed_spec_mp "W_correct_lemma"; 
385 

1300  386 
(* Completeness of W w.r.t. has_type *) 
5069  387 
Goal 
2525  388 
"!S' A t' n. $S' A  e :: t' > new_tv n A > \ 
389 
\ (? S t. (? m. W e A n = Some (S,t,m)) & \ 

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

5184  391 
by (induct_tac "e" 1); 
1300  392 
(* case Var n *) 
393 
by (strip_tac 1); 

4686  394 
by (simp_tac (simpset() addcongs [conj_cong]) 1); 
1300  395 
by (eresolve_tac has_type_casesE 1); 
4089  396 
by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1); 
2525  397 
by (etac exE 1); 
398 
by (hyp_subst_tac 1); 

399 
by (rename_tac "S" 1); 

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

401 
by (rtac conjI 1); 

1300  402 
by (Asm_simp_tac 1); 
4089  403 
by (asm_simp_tac (simpset() addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
2525  404 
delsimps [bound_typ_inst_composed_subst]) 1); 
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

405 
(** LEVEL 12 **) 
1300  406 
(* case Abs e *) 
407 
by (strip_tac 1); 

408 
by (eresolve_tac has_type_casesE 1); 

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

413 
by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
4089  414 
addss (simpset() addcongs [conj_cong] 
4072  415 
addsplits [split_option_bind])) 1); 
2749
2f477a0e690d
Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents:
2637
diff
changeset

416 
(** LEVEL 19 **) 
1300  417 

418 
(* case App e1 e2 *) 

419 
by (strip_tac 1); 

420 
by (eresolve_tac has_type_casesE 1); 

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

1400  423 
by (eres_inst_tac [("x","t2 > t'")] allE 1); 
1300  424 
by (eres_inst_tac [("x","n")] allE 1); 
425 
by (safe_tac HOL_cs); 

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

426 
(** LEVEL 26 **) 
2525  427 
by (eres_inst_tac [("x","R")] allE 1); 
428 
by (eres_inst_tac [("x","$ S A")] allE 1); 

1300  429 
by (eres_inst_tac [("x","t2")] allE 1); 
430 
by (eres_inst_tac [("x","m")] allE 1); 

431 
by (Asm_full_simp_tac 1); 

432 
by (safe_tac HOL_cs); 

433 
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS 

2525  434 
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

435 
(** LEVEL 35 **) 
1300  436 
by (subgoal_tac 
3842  437 
"$ (%x. if x=ma then t' else (if x:(free_tv t  free_tv Sa) then R x \ 
2525  438 
\ else Ra x)) ($ Sa t) = \ 
3842  439 
\ $ (%x. if x=ma then t' else (if x:(free_tv t  free_tv Sa) then R x \ 
2525  440 
\ else Ra x)) (ta > (TVar ma))" 1); 
1300  441 
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ 
2525  442 
\ (if x:(free_tv t  free_tv Sa) then R x else Ra x)) ($ Sa t)"), 
443 
("s","($ Ra ta) > t'")] ssubst 2); 

4089  444 
by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2); 
1465  445 
by (rtac eq_free_eq_subst_te 2); 
1300  446 
by (strip_tac 2); 
447 
by (subgoal_tac "na ~=ma" 2); 

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

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

451 
(* n1 ~: free_tv S1 *) 

452 
by (forward_tac [not_free_impl_id] 3); 

4686  453 
by (Asm_simp_tac 3); 
2525  454 
(* na : free_tv Sa *) 
455 
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); 

456 
by (dtac eq_subst_scheme_list_eq_free 2); 

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

2525  459 
by (case_tac "na:dom Sa" 2); 
460 
(* na ~: dom Sa *) 

4686  461 
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3); 
2525  462 
(* na : dom Sa *) 
1465  463 
by (rtac eq_free_eq_subst_te 2); 
1300  464 
by (strip_tac 2); 
465 
by (subgoal_tac "nb ~= ma" 2); 

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

1465  467 
by (etac conjE 3); 
2525  468 
by (dtac new_tv_subst_scheme_list 3); 
469 
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3); 

1300  470 
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
4089  471 
(simpset() addsimps [cod_def,free_tv_subst])) 3); 
4686  472 
by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2); 
1300  473 
by (Simp_tac 2); 
1465  474 
by (rtac eq_free_eq_subst_te 2); 
1300  475 
by (strip_tac 2 ); 
476 
by (subgoal_tac "na ~= ma" 2); 

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

1465  478 
by (etac conjE 3); 
479 
by (dtac (sym RS W_var_geD) 3); 

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

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

4686  483 
by (Asm_full_simp_tac 3); 
2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

484 
by (Fast_tac 3); 
2525  485 
(* case na : free_tv t  free_tv Sa *) 
4686  486 
by (Asm_full_simp_tac 2); 
2525  487 
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); 
488 
by (dtac eq_subst_scheme_list_eq_free 2); 

1300  489 
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

490 
(** LEVEL 75 **) 
4089  491 
by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2); 
492 
by (asm_simp_tac (simpset() addsplits [split_option_bind]) 1); 

1300  493 
by (safe_tac HOL_cs ); 
2525  494 
by (dtac mgu_Some 1); 
4089  495 
by ( fast_tac (HOL_cs addss simpset()) 1); 
2793
b30c41754c86
Modified proofs because simplifier does not etacontract any longer.
nipkow
parents:
2779
diff
changeset

496 
(** LEVEL 80 *) 
1300  497 
by ((dtac mgu_mg 1) THEN (atac 1)); 
1465  498 
by (etac exE 1); 
2525  499 
by (res_inst_tac [("x","Rb")] exI 1); 
1465  500 
by (rtac conjI 1); 
1300  501 
by (dres_inst_tac [("x","ma")] fun_cong 2); 
4089  502 
by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2); 
503 
by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1); 

504 
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

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

506 
((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); 
4089  507 
by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1); 
2525  508 
by (rtac eq_free_eq_subst_scheme_list 1); 
3018  509 
by ( safe_tac HOL_cs ); 
1300  510 
by (subgoal_tac "ma ~= na" 1); 
511 
by ((forward_tac [new_tv_W] 2) THEN (atac 2)); 

1465  512 
by (etac conjE 2); 
2525  513 
by (dtac new_tv_subst_scheme_list 2); 
514 
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

515 
by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2); 
1465  516 
by (etac conjE 2); 
2525  517 
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

518 
by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD, 
1300  519 
new_tv_not_free_tv]) 2); 
2525  520 
by (case_tac "na: free_tv t  free_tv Sa" 1); 
521 
(* case na ~: free_tv t  free_tv Sa *) 

4686  522 
by (Asm_full_simp_tac 2); 
2525  523 
(* case na : free_tv t  free_tv Sa *) 
4686  524 
by (Asm_full_simp_tac 1); 
2525  525 
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); 
526 
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans), 

4089  527 
eq_subst_scheme_list_eq_free] addss ((simpset() addsimps 
2525  528 
[free_tv_subst,dom_def]))) 1); 
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

529 
by (Fast_tac 1); 
2525  530 
(* case Let e1 e2 *) 
531 
by (eresolve_tac has_type_casesE 1); 

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

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

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

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

536 
by (mp_tac 1); 

537 
by (mp_tac 1); 

538 
by (safe_tac HOL_cs); 

539 
by (Asm_simp_tac 1); 

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

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

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

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

544 
by (Asm_full_simp_tac 1); 

545 
by (dtac mp 1); 

546 
by (rtac has_type_le_env 1); 

3018  547 
by (assume_tac 1); 
2525  548 
by (Simp_tac 1); 
549 
by (rtac gen_bound_typ_instance 1); 

550 
by (dtac mp 1); 

551 
by (forward_tac [new_tv_compatible_W] 1); 

552 
by (rtac sym 1); 

3018  553 
by (assume_tac 1); 
4089  554 
by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1); 
2525  555 
by (safe_tac HOL_cs); 
556 
by (Asm_full_simp_tac 1); 

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

4089  558 
by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1); 
1525  559 
qed_spec_mp "W_complete_lemma"; 
560 

5069  561 
Goal 
5118  562 
"[]  e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \ 
2525  563 
\ (? R. t' = $ R t))"; 
3018  564 
by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")] 
1525  565 
W_complete_lemma 1); 
3018  566 
by (ALLGOALS Asm_full_simp_tac); 
1525  567 
qed "W_complete"; 