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