src/HOL/MiniML/W.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6141 a6922171b396
child 6540 eaf90f6806df
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
    10 
    11 val has_type_casesE = 
    12     map has_type.mk_cases
    13 	[" A |- Var n :: t",
    14 	 " A |- Abs e :: t",
    15 	 "A |- App e1 e2 ::t",
    16 	 "A |- LET e1 e2 ::t" ];
    17 
    18 (* the resulting type variable is always greater or equal than the given one *)
    19 Goal "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
    20 by (induct_tac "e" 1);
    21 (* case Var(n) *)
    22 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    23 (* case Abs e *)
    24 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    25 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
    26 (* case App e1 e2 *)
    27 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    28 by (blast_tac (claset() addIs [le_SucI,le_trans]) 1);
    29 (* case LET e1 e2 *)
    30 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    31 by (blast_tac (claset() addIs [le_trans]) 1);
    32 qed_spec_mp "W_var_ge";
    33 
    34 Addsimps [W_var_ge];
    35 
    36 Goal "Some (S,t,m) = W e A n ==> n<=m";
    37 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    38 qed "W_var_geD";
    39 
    40 Goal "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);
    43 by (assume_tac 1);
    44 by (assume_tac 1);
    45 qed "new_tv_compatible_W";
    46 
    47 Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
    48 by (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 (assume_tac 2);
    57  by (rtac add_le_mono 1);
    58   by (Simp_tac 1);
    59  by (simp_tac (simpset() addsimps [max_def]) 1);
    60 by (rtac new_tv_le 1);
    61  by (assume_tac 2);
    62 by (rtac add_le_mono 1);
    63  by (Simp_tac 1);
    64 by (simp_tac (simpset() addsimps [max_def]) 1);
    65 qed_spec_mp "new_tv_bound_typ_inst_sch";
    66 
    67 Addsimps [new_tv_bound_typ_inst_sch];
    68 
    69 (* resulting type variable is new *)
    70 Goal "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
    71 \                 new_tv m S & new_tv m t";
    72 by (induct_tac "e" 1);
    73 (* case Var n *)
    74 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    75 by (strip_tac 1);
    76 by (dtac new_tv_nth_nat_A 1);
    77 by (assume_tac 1);
    78 by (Asm_simp_tac 1);
    79 (* case Abs e *)
    80 by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
    81     addsplits [split_option_bind]) 1);
    82 by (strip_tac 1);
    83 by (eres_inst_tac [("x","Suc n")] allE 1);
    84 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
    85 by (fast_tac (HOL_cs addss (simpset()
    86               addsimps [new_tv_subst,new_tv_Suc_list])) 1);
    87 (* case App e1 e2 *)
    88 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    89 by (strip_tac 1);
    90 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
    91 by (eres_inst_tac [("x","n")] allE 1);
    92 by (eres_inst_tac [("x","A")] allE 1);
    93 by (eres_inst_tac [("x","S1")] allE 1);
    94 by (eres_inst_tac [("x","t1")] allE 1);
    95 by (eres_inst_tac [("x","n1")] allE 1);
    96 by (eres_inst_tac [("x","n1")] allE 1);
    97 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv] delsimps all_simps) 1);
    98 by (eres_inst_tac [("x","$S1 A")] allE 1);
    99 by (eres_inst_tac [("x","S2")] allE 1);
   100 by (eres_inst_tac [("x","t2")] allE 1);
   101 by (eres_inst_tac [("x","n2")] allE 1);
   102 by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Some]) 1);
   103 by (rtac conjI 1);
   104 by (rtac new_tv_subst_comp_2 1);
   105 by (rtac new_tv_subst_comp_2 1);
   106 by (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
   107 by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 
   108 by (asm_full_simp_tac (simpset() addsimps [rotate_Some]) 1);
   109 by (Asm_simp_tac 1);
   110 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   111      [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le])
   112     1);
   113 by (etac (sym RS mgu_new) 1);
   114 by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
   115    new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
   116    new_tv_subst_le,new_tv_le]) 1);
   117 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   118      [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 
   119         addss (simpset())) 1);
   120 by (rtac (lessI RS new_tv_subst_var) 1);
   121 by (etac (sym RS mgu_new) 1);
   122 by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
   123    addDs [W_var_geD] addIs
   124    [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS
   125    new_tv_subst_le,new_tv_le] addss simpset()) 1);
   126 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   127      [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
   128      addss (simpset())) 1);
   129 (* 41: case LET e1 e2 *)
   130 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   131 by (strip_tac 1);
   132 by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
   133 by (etac conjE 1);
   134 by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
   135          etac impE 1, mp_tac 2]);
   136 by (SELECT_GOAL(rewtac new_tv_def)1);
   137 by (Asm_simp_tac 1);
   138 by (REPEAT(dtac W_var_ge 1));
   139 by (rtac allI 1);
   140 by (strip_tac 1);
   141 by (SELECT_GOAL(rewtac free_tv_subst) 1);
   142 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
   143 by (best_tac (claset() addEs [less_le_trans]) 1);
   144 by (etac conjE 1);
   145 by (rtac conjI 1);
   146 by (rtac new_tv_subst_comp_2 1);
   147 by (etac (W_var_ge RS new_tv_subst_le) 1);
   148 by (assume_tac 1);
   149 by (assume_tac 1);
   150 by (assume_tac 1);
   151 qed_spec_mp "new_tv_W";
   152 
   153 Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
   154 by (induct_tac "sch" 1);
   155 by (Asm_full_simp_tac 1);
   156 by (Asm_full_simp_tac 1);
   157 by (strip_tac 1);
   158 by (rtac exI 1);
   159 by (rtac refl 1);
   160 by (Asm_full_simp_tac 1);
   161 qed_spec_mp "free_tv_bound_typ_inst1";
   162 
   163 Addsimps [free_tv_bound_typ_inst1];
   164 
   165 Goal "!n A S t m v. W e A n = Some (S,t,m) -->            \
   166 \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
   167 by (induct_tac "e" 1);
   168 (* case Var n *)
   169 by (simp_tac (simpset() addsimps
   170     [free_tv_subst] addsplits [split_option_bind]) 1);
   171 by (strip_tac 1);
   172 by (case_tac "v : free_tv (A!nat)" 1);
   173 by (Asm_full_simp_tac 1);
   174 by (dtac free_tv_bound_typ_inst1 1);
   175 by (simp_tac (simpset() addsimps [o_def]) 1);
   176 by (etac exE 1);
   177 by (rotate_tac 3 1);
   178 by (Asm_full_simp_tac 1);
   179 (* case Abs e *)
   180 by (asm_full_simp_tac (simpset() addsimps
   181     [free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1);
   182 by (strip_tac 1);
   183 by (rename_tac "S t n1 S1 t1 m v" 1);
   184 by (eres_inst_tac [("x","Suc n")] allE 1);
   185 by (eres_inst_tac [("x","FVar n # A")] allE 1);
   186 by (eres_inst_tac [("x","S")] allE 1);
   187 by (eres_inst_tac [("x","t")] allE 1);
   188 by (eres_inst_tac [("x","n1")] allE 1);
   189 by (eres_inst_tac [("x","v")] allE 1);
   190 by (best_tac (HOL_cs addIs [cod_app_subst]
   191                      addss (simpset() addsimps [less_Suc_eq])) 1);
   192 (* case App e1 e2 *)
   193 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
   194 by (strip_tac 1); 
   195 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
   196 by (eres_inst_tac [("x","n")] allE 1);
   197 by (eres_inst_tac [("x","A")] allE 1);
   198 by (eres_inst_tac [("x","S")] allE 1);
   199 by (eres_inst_tac [("x","t")] allE 1);
   200 by (eres_inst_tac [("x","n1")] allE 1);
   201 by (eres_inst_tac [("x","n1")] allE 1);
   202 by (eres_inst_tac [("x","v")] allE 1);
   203 (* second case *)
   204 by (eres_inst_tac [("x","$ S A")] allE 1);
   205 by (eres_inst_tac [("x","S1")] allE 1);
   206 by (eres_inst_tac [("x","t1")] allE 1);
   207 by (eres_inst_tac [("x","n2")] allE 1);
   208 by (eres_inst_tac [("x","v")] allE 1);
   209 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
   210 by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
   211 by (dtac W_var_geD 1);
   212 by (dtac W_var_geD 1);
   213 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   214 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
   215     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
   216     less_le_trans,less_not_refl2,subsetD]
   217   addEs [UnE] 
   218   addss simpset()) 1);
   219 by (Asm_full_simp_tac 1); 
   220 by (dtac (sym RS W_var_geD) 1);
   221 by (dtac (sym RS W_var_geD) 1);
   222 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   223 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
   224     free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
   225     less_le_trans,subsetD]
   226   addEs [UnE]
   227   addss (simpset() setSolver unsafe_solver)) 1);
   228 (* LET e1 e2 *)
   229 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
   230 by (strip_tac 1); 
   231 by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
   232 by (eres_inst_tac [("x","nat")] allE 1);
   233 by (eres_inst_tac [("x","A")] allE 1);
   234 by (eres_inst_tac [("x","S1")] allE 1);
   235 by (eres_inst_tac [("x","t1")] allE 1);
   236 by (rotate_tac 1 1);
   237 by (eres_inst_tac [("x","n2")] allE 1);
   238 by (rotate_tac 4 1);
   239 by (eres_inst_tac [("x","v")] allE 1);
   240 by (mp_tac 1);
   241 by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
   242 by (mp_tac 1);
   243 by (Asm_full_simp_tac 1);
   244 by (rtac conjI 1);
   245 by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
   246               addDs [less_le_trans]) 1);
   247 by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
   248               addDs [less_le_trans]) 1);
   249 qed_spec_mp "free_tv_W"; 
   250 
   251 Goal "(!x. x : A --> x ~: B) ==> A Int B = {}";
   252 by (Fast_tac 1);
   253 val weaken_A_Int_B_eq_empty = result();
   254 
   255 Goal "x ~: A | x : B ==> x ~: A - B";
   256 by (Fast_tac 1);
   257 val weaken_not_elem_A_minus_B = result();
   258 
   259 (* correctness of W with respect to has_type *)
   260 Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
   261 by (induct_tac "e" 1);
   262 (* case Var n *)
   263 by (Asm_full_simp_tac 1);
   264 by (strip_tac 1);
   265 by (rtac has_type.VarI 1);
   266 by (Simp_tac 1);
   267 by (simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
   268 by (rtac exI 1);
   269 by (rtac refl 1);
   270 (* case Abs e *)
   271 by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
   272                         addsplits [split_option_bind]) 1);
   273 by (strip_tac 1);
   274 by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
   275 by (Asm_full_simp_tac 1);
   276 by (rtac has_type.AbsI 1);
   277 by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
   278 by (dtac sym 1);
   279 by (REPEAT (etac allE 1));
   280 by (etac impE 1);
   281 by (mp_tac 2);
   282 by (Asm_simp_tac 1);
   283 by (assume_tac 1);
   284 (* case App e1 e2 *)
   285 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   286 by (strip_tac 1);
   287 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
   288 by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
   289 by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
   290 by (rtac (app_subst_Fun RS subst) 1);
   291 by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
   292 by (Asm_full_simp_tac 1);
   293 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
   294 by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
   295 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   296 by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
   297 by (rtac (has_type_cl_sub RS spec) 1);
   298 by (forward_tac [new_tv_W] 1);
   299 by (assume_tac 1);
   300 by (dtac conjunct1 1);
   301 by (dtac conjunct1 1);
   302 by (forward_tac [new_tv_subst_scheme_list] 1);
   303 by (rtac new_scheme_list_le 1);
   304 by (rtac W_var_ge 1);
   305 by (assume_tac 1);
   306 by (assume_tac 1);
   307 by (etac thin_rl 1);
   308 by (REPEAT (etac allE 1));
   309 by (dtac sym 1);
   310 by (dtac sym 1);
   311 by (etac thin_rl 1);
   312 by (etac thin_rl 1);
   313 by (mp_tac 1);
   314 by (mp_tac 1);
   315 by (assume_tac 1);
   316 (* case Let e1 e2 *)
   317 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   318 by (strip_tac 1);
   319 by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
   320 by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
   321 by (simp_tac (simpset() addsimps [o_def]) 1);
   322 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
   323 by (rtac (has_type_cl_sub RS spec) 1);
   324 by (dres_inst_tac [("x","A")] spec 1);
   325 by (dres_inst_tac [("x","S1")] spec 1);
   326 by (dres_inst_tac [("x","t1")] spec 1);
   327 by (dres_inst_tac [("x","m2")] spec 1);
   328 by (rotate_tac 4 1);
   329 by (dres_inst_tac [("x","m1")] spec 1);
   330 by (mp_tac 1);
   331 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   332 by (simp_tac (simpset() addsimps [o_def]) 1);
   333 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
   334 by (rtac (gen_subst_commutes RS sym RS subst) 1);
   335 by (rtac (app_subst_Cons RS subst) 2);
   336 by (etac thin_rl 2);
   337 by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
   338 by (dres_inst_tac [("x","S2")] spec 2);
   339 by (dres_inst_tac [("x","t")] spec 2);
   340 by (dres_inst_tac [("x","n2")] spec 2);
   341 by (dres_inst_tac [("x","m2")] spec 2);
   342 by (forward_tac [new_tv_W] 2);
   343 by (assume_tac 2);
   344 by (dtac conjunct1 2);
   345 by (dtac conjunct1 2);
   346 by (forward_tac [new_tv_subst_scheme_list] 2);
   347 by (rtac new_scheme_list_le 2);
   348 by (rtac W_var_ge 2);
   349 by (assume_tac 2);
   350 by (assume_tac 2);
   351 by (etac impE 2);
   352 by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
   353 by (Simp_tac 2);
   354 by (Fast_tac 2);
   355 by (assume_tac 2);
   356 by (Asm_full_simp_tac 2);
   357 by (rtac weaken_A_Int_B_eq_empty 1);
   358 by (rtac allI 1);
   359 by (strip_tac 1);
   360 by (rtac weaken_not_elem_A_minus_B 1);
   361 by (case_tac "x < m2" 1);
   362 by (rtac disjI2 1);
   363 by (rtac (free_tv_gen_cons RS subst) 1);
   364 by (rtac free_tv_W 1);
   365 by (assume_tac 1);
   366 by (Asm_full_simp_tac 1);
   367 by (assume_tac 1);
   368 by (rtac disjI1 1);
   369 by (dtac new_tv_W 1);
   370 by (assume_tac 1);
   371 by (dtac conjunct2 1);
   372 by (dtac conjunct2 1);
   373 by (rtac new_tv_not_free_tv 1);
   374 by (rtac new_tv_le 1);
   375 by (assume_tac 2);
   376 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
   377 qed_spec_mp "W_correct_lemma";
   378 
   379 (* Completeness of W w.r.t. has_type *)
   380 Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
   381 \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
   382 \                     (? R. $S' A = $R ($S A) & t' = $R t))";
   383 by (induct_tac "e" 1);
   384 (* case Var n *)
   385 by (strip_tac 1);
   386 by (simp_tac (simpset() addcongs [conj_cong]) 1);
   387 by (eresolve_tac has_type_casesE 1); 
   388 by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
   389 by (etac exE 1);
   390 by (hyp_subst_tac 1);
   391 by (rename_tac "S" 1);
   392 by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
   393 by (rtac conjI 1);
   394 by (Asm_simp_tac 1);
   395 by (asm_simp_tac (simpset() addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
   396                            delsimps [bound_typ_inst_composed_subst]) 1);
   397 (** LEVEL 12 **)
   398 (* case Abs e *)
   399 by (strip_tac 1);
   400 by (eresolve_tac has_type_casesE 1);
   401 by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1);
   402 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
   403 by (eres_inst_tac [("x","t2")] allE 1);
   404 by (eres_inst_tac [("x","Suc n")] allE 1);
   405 by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
   406                   addss (simpset() addcongs [conj_cong] 
   407                                 addsplits [split_option_bind])) 1);
   408 (** LEVEL 19 **)
   409 
   410 (* case App e1 e2 *)
   411 by (strip_tac 1);
   412 by (eresolve_tac has_type_casesE 1);
   413 by (eres_inst_tac [("x","S'")] allE 1);
   414 by (eres_inst_tac [("x","A")] allE 1);
   415 by (eres_inst_tac [("x","t2 -> t'")] allE 1);
   416 by (eres_inst_tac [("x","n")] allE 1);
   417 by (safe_tac HOL_cs);
   418 (** LEVEL 26 **)
   419 by (eres_inst_tac [("x","R")] allE 1);
   420 by (eres_inst_tac [("x","$ S A")] allE 1);
   421 by (eres_inst_tac [("x","t2")] allE 1);
   422 by (eres_inst_tac [("x","m")] allE 1);
   423 by (Asm_full_simp_tac 1);
   424 by (safe_tac HOL_cs);
   425 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
   426         conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
   427 (** LEVEL 35 **)
   428 by (subgoal_tac
   429   "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
   430 \        else Ra x)) ($ Sa t) = \
   431 \  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
   432 \        else Ra x)) (ta -> (TVar ma))" 1);
   433 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
   434 \   (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
   435     ("s","($ Ra ta) -> t'")] ssubst 2);
   436 by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2);
   437 by (rtac eq_free_eq_subst_te 2);  
   438 by (strip_tac 2);
   439 by (subgoal_tac "na ~=ma" 2);
   440 by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
   441     new_tv_not_free_tv,new_tv_le]) 3);
   442 by (case_tac "na:free_tv Sa" 2);
   443 (* n1 ~: free_tv S1 *)
   444 by (forward_tac [not_free_impl_id] 3);
   445 by (Asm_simp_tac 3);
   446 (* na : free_tv Sa *)
   447 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
   448 by (dtac eq_subst_scheme_list_eq_free 2);
   449 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   450 by (Asm_simp_tac 2); 
   451 by (case_tac "na:dom Sa" 2);
   452 (* na ~: dom Sa *)
   453 by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
   454 (* na : dom Sa *)
   455 by (rtac eq_free_eq_subst_te 2);
   456 by (strip_tac 2);
   457 by (subgoal_tac "nb ~= ma" 2);
   458 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   459 by (etac conjE 3);
   460 by (dtac new_tv_subst_scheme_list 3);
   461 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
   462 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
   463     (simpset() addsimps [cod_def,free_tv_subst])) 3);
   464 by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
   465 by (Simp_tac 2);  
   466 by (rtac eq_free_eq_subst_te 2);
   467 by (strip_tac 2 );
   468 by (subgoal_tac "na ~= ma" 2);
   469 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   470 by (etac conjE 3);
   471 by (dtac (sym RS W_var_geD) 3);
   472 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
   473 by (case_tac "na: free_tv t - free_tv Sa" 2);
   474 (* case na ~: free_tv t - free_tv Sa *)
   475 by (Asm_full_simp_tac 3);
   476 by (Fast_tac 3);
   477 (* case na : free_tv t - free_tv Sa *)
   478 by (Asm_full_simp_tac 2);
   479 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
   480 by (dtac eq_subst_scheme_list_eq_free 2);
   481 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   482 (** LEVEL 75 **)
   483 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2);
   484 by (asm_simp_tac (simpset() addsplits [split_option_bind]) 1); 
   485 by (safe_tac HOL_cs );
   486 by (dtac mgu_Some 1);
   487 by ( fast_tac (HOL_cs addss simpset()) 1);
   488 (** LEVEL 80 *)
   489 by ((dtac mgu_mg 1) THEN (atac 1));
   490 by (etac exE 1);
   491 by (res_inst_tac [("x","Rb")] exI 1);
   492 by (rtac conjI 1);
   493 by (dres_inst_tac [("x","ma")] fun_cong 2);
   494 by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2);
   495 by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1);
   496 by (simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym]) 1);
   497 by (res_inst_tac [("A2","($ Sa ($ S A))")]
   498        ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
   499 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
   500 by (rtac eq_free_eq_subst_scheme_list 1);
   501 by ( safe_tac HOL_cs );
   502 by (subgoal_tac "ma ~= na" 1);
   503 by ((forward_tac [new_tv_W] 2) THEN (atac 2));
   504 by (etac conjE 2);
   505 by (dtac new_tv_subst_scheme_list 2);
   506 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
   507 by (forw_inst_tac [("n","m")] new_tv_W 2  THEN  atac 2);
   508 by (etac conjE 2);
   509 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
   510 by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD,
   511     new_tv_not_free_tv]) 2);
   512 by (case_tac "na: free_tv t - free_tv Sa" 1);
   513 (* case na ~: free_tv t - free_tv Sa *)
   514 by (Asm_full_simp_tac 2);
   515 (* case na : free_tv t - free_tv Sa *)
   516 by (Asm_full_simp_tac 1);
   517 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
   518 by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
   519     eq_subst_scheme_list_eq_free] addss ((simpset() addsimps 
   520     [free_tv_subst,dom_def]))) 1);
   521 by (Fast_tac 1);
   522 (* case Let e1 e2 *)
   523 by (eresolve_tac has_type_casesE 1);
   524 by (eres_inst_tac [("x","S'")] allE 1);
   525 by (eres_inst_tac [("x","A")] allE 1);
   526 by (eres_inst_tac [("x","t1")] allE 1);
   527 by (eres_inst_tac [("x","n")] allE 1);
   528 by (mp_tac 1);
   529 by (mp_tac 1);
   530 by (safe_tac HOL_cs);
   531 by (Asm_simp_tac 1); 
   532 by (eres_inst_tac [("x","R")] allE 1);
   533 by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
   534 by (eres_inst_tac [("x","t'")] allE 1);
   535 by (eres_inst_tac [("x","m")] allE 1);
   536 by (Asm_full_simp_tac 1);
   537 by (dtac mp 1);
   538 by (rtac has_type_le_env 1);
   539 by (assume_tac 1);
   540 by (Simp_tac 1);
   541 by (rtac gen_bound_typ_instance 1);
   542 by (dtac mp 1);
   543 by (forward_tac [new_tv_compatible_W] 1);
   544 by (rtac sym 1);
   545 by (assume_tac 1);
   546 by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
   547 by (safe_tac HOL_cs);
   548 by (Asm_full_simp_tac 1);
   549 by (res_inst_tac [("x","Ra")] exI 1);
   550 by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
   551 qed_spec_mp "W_complete_lemma";
   552 
   553 Goal "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
   554 \                                 (? R. t' = $ R t))";
   555 by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
   556                 W_complete_lemma 1);
   557 by (ALLGOALS Asm_full_simp_tac);
   558 qed "W_complete";