src/HOL/MiniML/W.ML
author nipkow
Mon Apr 22 15:42:20 1996 +0200 (1996-04-22)
changeset 1669 e56cdf711729
parent 1525 d127436567d0
child 1818 ffc20ff80190
permissions -rw-r--r--
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
     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 
    12 (* stronger version of Suc_leD *)
    13 goalw Nat.thy [le_def] 
    14         "!!m. Suc m <= n ==> m < n";
    15 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    16 by (cut_facts_tac [less_linear] 1);
    17 by (fast_tac HOL_cs 1);
    18 qed "Suc_le_lessD";
    19 Addsimps [Suc_le_lessD];
    20 
    21 (* correctness of W with respect to has_type *)
    22 goal W.thy
    23         "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
    24 by (expr.induct_tac "e" 1);
    25 (* case Var n *)
    26 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    27 (* case Abs e *)
    28 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
    29                         setloop (split_tac [expand_bind])) 1);
    30 by (strip_tac 1);
    31 by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
    32 by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
    33 (* case App e1 e2 *)
    34 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    35 by (strip_tac 1);
    36 by( rename_tac "sa ta na sb tb nb sc" 1);
    37 by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
    38 by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
    39 by (rtac (app_subst_Fun RS subst) 1);
    40 by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
    41 by (Asm_full_simp_tac 1);
    42 by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
    43 by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
    44 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    45 by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
    46 qed_spec_mp "W_correct";
    47 
    48 val has_type_casesE = map(has_type.mk_cases expr.simps)
    49         [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
    50 
    51 
    52 (* the resulting type variable is always greater or equal than the given one *)
    53 goal thy
    54         "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
    55 by (expr.induct_tac "e" 1);
    56 (* case Var(n) *)
    57 by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
    58 (* case Abs e *)
    59 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    60 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
    61 (* case App e1 e2 *)
    62 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    63 by (strip_tac 1);
    64 by (rename_tac "s t na sa ta nb sb sc tb m" 1);
    65 by (eres_inst_tac [("x","a")] allE 1);
    66 by (eres_inst_tac [("x","n")] allE 1);
    67 by (eres_inst_tac [("x","$ s a")] allE 1);
    68 by (eres_inst_tac [("x","s")] allE 1);
    69 by (eres_inst_tac [("x","t")] allE 1);
    70 by (eres_inst_tac [("x","na")] allE 1);
    71 by (eres_inst_tac [("x","na")] allE 1);
    72 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    73 by (etac conjE 1);
    74 by (eres_inst_tac [("x","sa")] allE 1);
    75 by (eres_inst_tac [("x","ta")] allE 1);
    76 by (eres_inst_tac [("x","nb")] allE 1);
    77 by (etac conjE 1);
    78 by (res_inst_tac [("j","na")] le_trans 1); 
    79 by (Asm_simp_tac 1);
    80 by (Asm_simp_tac 1);
    81 qed_spec_mp "W_var_ge";
    82 
    83 Addsimps [W_var_ge];
    84 
    85 goal thy
    86         "!! s. Ok (s,t,m) = W e a n ==> n<=m";
    87 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    88 qed "W_var_geD";
    89 
    90 
    91 (* auxiliary lemma *)
    92 goal Maybe.thy "(y = Ok x) = (Ok x = y)";
    93 by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    94 qed "rotate_Ok";
    95 
    96 
    97 (* resulting type variable is new *)
    98 goal thy
    99      "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
   100 \                 new_tv m s & new_tv m t";
   101 by (expr.induct_tac "e" 1);
   102 (* case Var n *)
   103 by (fast_tac (HOL_cs addss (!simpset 
   104         addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
   105         setloop (split_tac [expand_if]))) 1);
   106 
   107 (* case Abs e *)
   108 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
   109     setloop (split_tac [expand_bind])) 1);
   110 by (strip_tac 1);
   111 by (eres_inst_tac [("x","Suc n")] allE 1);
   112 by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
   113 by (fast_tac (HOL_cs addss (!simpset
   114               addsimps [new_tv_subst,new_tv_Suc_list])) 1);
   115 
   116 (* case App e1 e2 *)
   117 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   118 by (strip_tac 1);
   119 by (rename_tac "s t na sa ta nb sb sc tb m" 1);
   120 by (eres_inst_tac [("x","n")] allE 1);
   121 by (eres_inst_tac [("x","a")] allE 1);
   122 by (eres_inst_tac [("x","s")] allE 1);
   123 by (eres_inst_tac [("x","t")] allE 1);
   124 by (eres_inst_tac [("x","na")] allE 1);
   125 by (eres_inst_tac [("x","na")] allE 1);
   126 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   127 by (eres_inst_tac [("x","$ s a")] allE 1);
   128 by (eres_inst_tac [("x","sa")] allE 1);
   129 by (eres_inst_tac [("x","ta")] allE 1);
   130 by (eres_inst_tac [("x","nb")] allE 1);
   131 by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
   132 by (rtac conjI 1);
   133 by (rtac new_tv_subst_comp_2 1);
   134 by (rtac new_tv_subst_comp_2 1);
   135 by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
   136 by (res_inst_tac [("n","na")] new_tv_subst_le 1); 
   137 by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
   138 by (Asm_simp_tac 1);
   139 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   140      [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
   141     1);
   142 by (etac (sym RS mgu_new) 1);
   143 by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,
   144    new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
   145    new_tv_subst_le,new_tv_le]) 1);
   146 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   147      [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
   148         addss (!simpset)) 1);
   149 by (rtac (lessI RS new_tv_subst_var) 1);
   150 by (etac (sym RS mgu_new) 1);
   151 by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
   152    addDs [W_var_geD] addIs
   153    [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS
   154    new_tv_subst_le,new_tv_le] addss !simpset) 1);
   155 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
   156      [new_tv_list_le,new_tv_subst_tel,new_tv_le]
   157      addss (!simpset)) 1);
   158 qed_spec_mp "new_tv_W";
   159 
   160 
   161 goal thy
   162      "!n a s t m v. W e a n = Ok (s,t,m) -->            \
   163 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
   164 by (expr.induct_tac "e" 1);
   165 (* case Var n *)
   166 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
   167     addss (!simpset setloop (split_tac [expand_if]))) 1);
   168 
   169 (* case Abs e *)
   170 by (asm_full_simp_tac (!simpset addsimps
   171     [free_tv_subst] setloop (split_tac [expand_bind])) 1);
   172 by (strip_tac 1);
   173 by (rename_tac "s t na sa ta m v" 1);
   174 by (eres_inst_tac [("x","Suc n")] allE 1);
   175 by (eres_inst_tac [("x","TVar n # a")] allE 1);
   176 by (eres_inst_tac [("x","s")] allE 1);
   177 by (eres_inst_tac [("x","t")] allE 1);
   178 by (eres_inst_tac [("x","na")] allE 1);
   179 by (eres_inst_tac [("x","v")] allE 1);
   180 by (fast_tac (HOL_cs addIs [cod_app_subst]
   181                      addss (!simpset addsimps [less_Suc_eq])) 1);
   182 
   183 (* case App e1 e2 *)
   184 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   185 by (strip_tac 1); 
   186 by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
   187 by (eres_inst_tac [("x","n")] allE 1);
   188 by (eres_inst_tac [("x","a")] allE 1);
   189 by (eres_inst_tac [("x","s")] allE 1);
   190 by (eres_inst_tac [("x","t")] allE 1);
   191 by (eres_inst_tac [("x","na")] allE 1);
   192 by (eres_inst_tac [("x","na")] allE 1);
   193 by (eres_inst_tac [("x","v")] allE 1);
   194 (* second case *)
   195 by (eres_inst_tac [("x","$ s a")] allE 1);
   196 by (eres_inst_tac [("x","sa")] allE 1);
   197 by (eres_inst_tac [("x","ta")] allE 1);
   198 by (eres_inst_tac [("x","nb")] allE 1);
   199 by (eres_inst_tac [("x","v")] allE 1);
   200 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
   201 by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
   202 by (dtac W_var_geD 1);
   203 by (dtac W_var_geD 1);
   204 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   205 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
   206     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
   207     less_le_trans,less_not_refl2,subsetD]
   208   addEs [UnE] 
   209   addss !simpset) 1);
   210 by (Asm_full_simp_tac 1); 
   211 by (dtac (sym RS W_var_geD) 1);
   212 by (dtac (sym RS W_var_geD) 1);
   213 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
   214 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
   215     free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
   216     less_le_trans,subsetD]
   217   addEs [UnE]
   218   addss !simpset) 1); 
   219 qed_spec_mp "free_tv_W"; 
   220 
   221 (* Completeness of W w.r.t. has_type *)
   222 goal thy
   223  "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
   224 \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
   225 \                     (? r. $s' a = $r ($s a) & t' = $r t))";
   226 by (expr.induct_tac "e" 1);
   227 (* case Var n *)
   228 by (strip_tac 1);
   229 by (simp_tac (!simpset addcongs [conj_cong] 
   230     setloop (split_tac [expand_if])) 1);
   231 by (eresolve_tac has_type_casesE 1); 
   232 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
   233 by (res_inst_tac [("x","id_subst")] exI 1);
   234 by (res_inst_tac [("x","nth nat a")] exI 1);
   235 by (Simp_tac 1);
   236 by (res_inst_tac [("x","s'")] exI 1);
   237 by (Asm_simp_tac 1);
   238 
   239 (* case Abs e *)
   240 by (strip_tac 1);
   241 by (eresolve_tac has_type_casesE 1);
   242 by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
   243 by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
   244 by (eres_inst_tac [("x","t2")] allE 1);
   245 by (eres_inst_tac [("x","Suc n")] allE 1);
   246 by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
   247     setloop (split_tac [expand_bind]))) 1);
   248 
   249 (* case App e1 e2 *)
   250 by (strip_tac 1);
   251 by (eresolve_tac has_type_casesE 1);
   252 by (eres_inst_tac [("x","s'")] allE 1);
   253 by (eres_inst_tac [("x","a")] allE 1);
   254 by (eres_inst_tac [("x","t2 -> t'")] allE 1);
   255 by (eres_inst_tac [("x","n")] allE 1);
   256 by (safe_tac HOL_cs);
   257 by (eres_inst_tac [("x","r")] allE 1);
   258 by (eres_inst_tac [("x","$ s a")] allE 1);
   259 by (eres_inst_tac [("x","t2")] allE 1);
   260 by (eres_inst_tac [("x","m")] allE 1);
   261 by (dtac asm_rl 1);
   262 by (dtac asm_rl 1);
   263 by (dtac asm_rl 1);
   264 by (Asm_full_simp_tac 1);
   265 by (safe_tac HOL_cs);
   266 by (fast_tac HOL_cs 1);
   267 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
   268         conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
   269 
   270 by (subgoal_tac
   271   "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
   272 \        else ra x)) ($ sa t) = \
   273 \  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
   274 \        else ra x)) (ta -> (TVar ma))" 1);
   275 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
   276 \   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
   277     ("s","($ ra ta) -> t'")] ssubst 2);
   278 by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
   279 by (rtac eq_free_eq_subst_te 2);  
   280 by (strip_tac 2);
   281 by (subgoal_tac "na ~=ma" 2);
   282 by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
   283     new_tv_not_free_tv,new_tv_le]) 3);
   284 by (case_tac "na:free_tv sa" 2);
   285 (* na ~: free_tv sa *)
   286 by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
   287     setloop (split_tac [expand_if])) 3);
   288 (* na : free_tv sa *)
   289 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
   290 by (dtac eq_subst_tel_eq_free 2);
   291 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   292 by (Asm_simp_tac 2); 
   293 by (case_tac "na:dom sa" 2);
   294 (* na ~: dom sa *)
   295 by (asm_full_simp_tac (!simpset addsimps [dom_def] 
   296     setloop (split_tac [expand_if])) 3);
   297 (* na : dom sa *)
   298 by (rtac eq_free_eq_subst_te 2);
   299 by (strip_tac 2);
   300 by (subgoal_tac "nb ~= ma" 2);
   301 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   302 by (etac conjE 3);
   303 by (dtac new_tv_subst_tel 3);
   304 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
   305 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
   306     (!simpset addsimps [cod_def,free_tv_subst])) 3);
   307 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
   308     setloop (split_tac [expand_if]))) 2);
   309 
   310 by (Simp_tac 2);  
   311 by (rtac eq_free_eq_subst_te 2);
   312 by (strip_tac 2 );
   313 by (subgoal_tac "na ~= ma" 2);
   314 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
   315 by (etac conjE 3);
   316 by (dtac (sym RS W_var_geD) 3);
   317 by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
   318 by (case_tac "na: free_tv t - free_tv sa" 2);
   319 (* case na ~: free_tv t - free_tv sa *)
   320 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
   321 (* case na : free_tv t - free_tv sa *)
   322 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
   323 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
   324 by (dtac eq_subst_tel_eq_free 2);
   325 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   326 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
   327 
   328 by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
   329 by (safe_tac HOL_cs );
   330 by (dtac mgu_Ok 1);
   331 by( fast_tac (HOL_cs addss !simpset) 1);
   332 by (REPEAT (resolve_tac [exI,conjI] 1));
   333 by (fast_tac HOL_cs 1);
   334 by (fast_tac HOL_cs 1);
   335 by ((dtac mgu_mg 1) THEN (atac 1));
   336 by (etac exE 1);
   337 by (res_inst_tac [("x","rb")] exI 1);
   338 by (rtac conjI 1);
   339 by (dres_inst_tac [("x","ma")] fun_cong 2);
   340 by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
   341 by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
   342 by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
   343     (2,trans)) 1);
   344 by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
   345 by (rtac eq_free_eq_subst_tel 1);
   346 by( safe_tac HOL_cs );
   347 by (subgoal_tac "ma ~= na" 1);
   348 by ((forward_tac [new_tv_W] 2) THEN (atac 2));
   349 by (etac conjE 2);
   350 by (dtac new_tv_subst_tel 2);
   351 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
   352 by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
   353 by (etac conjE 2);
   354 by (dtac (free_tv_app_subst_tel RS subsetD) 2);
   355 by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
   356     new_tv_not_free_tv]) 2);
   357 by (case_tac "na: free_tv t - free_tv sa" 1);
   358 (* case na ~: free_tv t - free_tv sa *)
   359 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
   360 (* case na : free_tv t - free_tv sa *)
   361 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   362 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
   363 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
   364     eq_subst_tel_eq_free] addss ((!simpset addsimps 
   365     [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
   366 qed_spec_mp "W_complete_lemma";
   367 
   368 goal W.thy
   369  "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
   370 \                                 (? r. t' = $r t))";
   371 by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
   372                 W_complete_lemma 1);
   373 by(ALLGOALS Asm_full_simp_tac);
   374 qed "W_complete";