# HG changeset patch
# User wenzelm
# Date 1014679144 -3600
# Node ID fa6a3ddec27f42747c166639683dfc553bef732f
# Parent  1db24da0537bac9bb0dc3a0617efdb9ecc35cb49
converted;

diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(* Title:     HOL/W0/I.ML
-   ID:        $Id$
-   Author:    Thomas Stauner
-   Copyright  1995 TU Muenchen
-
-Equivalence of W and I.
-*)
-
-open I;
-
-Goal "! a m s s' t n.  \
-\    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
-\    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
-by (induct_tac "e" 1);
-
-  (* case Var n *)
-  by (simp_tac (simpset() addsimps [app_subst_list]
-      setloop (split_inside_tac [split_if])) 1);
-
- (* case Abs e *)
- by (asm_full_simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
- by (strip_tac 1);
- by (rtac conjI 1);
-  by (strip_tac 1);
-  by (REPEAT (etac allE 1));
-  by (etac impE 1);
-   by (fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])) 2);
-  by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
-                              less_imp_le,lessI]) 1); 
-(** LEVEL 10 **)
- by (strip_tac 1);
- by (REPEAT (etac allE 1));
- by (etac impE 1);
-  by (fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])) 2);
- by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
-                             less_imp_le,lessI]) 1);
-(** LEVEL 15 **)
-(* case App e1 e2 *)
-by (simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
-by (strip_tac 1);
-by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
-by (rtac conjI 1);
- by (fast_tac (HOL_cs addss simpset()) 1);
-by (strip_tac 1);
-by (rename_tac "s1 t1' n1'" 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","m")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","s1'")] allE 1);
-by (eres_inst_tac [("x","t1")] allE 1);
-by (eres_inst_tac [("x","n1")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","n1")] allE 1);
-by (eres_inst_tac [("x","s1'")] allE 1);
-by (eres_inst_tac [("x","s2'")] allE 1);
-by (eres_inst_tac [("x","t2")] allE 1);
-by (eres_inst_tac [("x","n2")] allE 1);
-(** LEVEL 34 **)
-by (rtac conjI 1);
- by (strip_tac 1);
- by (rtac notI 1);
- by (Asm_full_simp_tac 1);
-(* by (mp_tac 1);
- by (mp_tac 1);
- by (etac exE 1);
- by (etac conjE 1);*)
- by (etac impE 1);
-  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
-  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-                       addss simpset()) 1);
- by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel])) 1);
-(** LEVEL 45 **)
-by (strip_tac 1);
-by (rename_tac "s2 t2' n2'" 1);
-by (rtac conjI 1);
- by (strip_tac 1);
- by (rtac notI 1);
- by (Asm_full_simp_tac 1);
-(*
- by (mp_tac 1);
- by (mp_tac 1);
- by (etac exE 1);
- by (etac conjE 1);*)
- by (etac impE 1);
-  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
-  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-                       addss simpset()) 1);
- by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel,subst_comp_te])) 1);
-by (strip_tac 1);
-by (mp_tac 1);
-(** LEVEL 60 **)
-by (mp_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (etac impE 1);
- by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
- by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
- by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-                      addss simpset()) 1);
-by (mp_tac 1);
-by (REPEAT (eresolve_tac [exE,conjE] 1));
-by (REPEAT(EVERY1
-     [asm_full_simp_tac (simpset() addsimps [subst_comp_tel,subst_comp_te,o_def]),
-      REPEAT o etac conjE, hyp_subst_tac]));
-(** LEVEL 70 **)
-by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
- by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-by ((ftac new_tv_subst_tel 1) THEN (atac 1));
-by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
-by (safe_tac HOL_cs);
-  by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-                       addss simpset()) 1);
- by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
-                      addss simpset()) 1);
-(** LEVEL 77 **)
-by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
-by ((dtac new_tv_subst_tel 1) THEN (atac 1));
-by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
-by ((dtac new_tv_subst_tel 1) THEN (atac 1));
-by (best_tac (HOL_cs addDs [new_tv_W] 
-                     addss (simpset() addsimps [subst_comp_tel])) 1);
-(** LEVEL 82 **)
-qed_spec_mp "I_correct_wrt_W";
-
-(***
-We actually want the corollary
-
-Goal "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
-by (cut_facts_tac [(read_instantiate[("x","id_subst")]
- (read_instantiate[("x","[]")](thm RS spec)
-  RS spec RS spec))] 1);
-by (Full_simp_tac 1);
-by (fast_tac HOL_cs 1);
-qed;
-
-assuming that thm is the undischarged version of I_correct_wrt_W.
-
-Wait until simplification of thms is possible.
-***)
-
-val lemma = I_correct_wrt_W COMP swap_prems_rl;
-
-Addsimps [split_paired_Ex];
-
-Goal "!a m s. \
-\  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
-by (induct_tac "e" 1);
-  by (simp_tac (simpset() addsimps [app_subst_list]) 1);
- by (Simp_tac 1);
- by (strip_tac 1);
- by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
-  by (asm_simp_tac (HOL_ss addsimps
-        [new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);
- by (etac conjE 1);
- by (dtac (new_tv_not_free_tv RS not_free_impl_id) 1);
- by (Asm_simp_tac 1);
-(** LEVEL 9 **)
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (REPEAT(etac exE 1));
-by (REPEAT(etac conjE 1));
-by (dtac lemma 1);
- by (fast_tac HOL_cs 1);
-(** LEVEL 15 **)
-by (etac exE 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-by (Asm_simp_tac 1);
-by (REPEAT(resolve_tac [exI,conjI,refl] 1));
-by (etac disjE 1);
- by (rtac disjI1 1);
-(** LEVEL 22 **)
- by (full_simp_tac (simpset() addsimps [o_def,subst_comp_tel]) 1);
- by (EVERY[etac allE 1, etac allE 1, etac allE 1,
-          etac impE 1, etac impE 2, atac 2, atac 2]);
- by (rtac conjI 1);
-  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
- by (rtac new_tv_subst_comp_2 1);
-  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
- by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
-by (rtac disjI2 1);
-by (REPEAT(etac exE 1));
-by (etac conjE 1);
-(** LEVEL 32 **)
-by (dtac lemma 1);
- by (rtac conjI 1);
-  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
- by (rtac new_tv_subst_comp_1 1);
-  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
- by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
-by (etac exE 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-(** LEVEL 41 **)
-by (asm_full_simp_tac (simpset() addsimps
-     [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
-qed_spec_mp "I_complete_wrt_W";
-
-(***
-We actually want the corollary
-
-  "I e [] m id_subst = Fail ==> W e [] m = Fail";
-
-Wait until simplification of thms is possible.
-***)
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/I.thy
--- a/src/HOL/W0/I.thy	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title:     HOL/W0/I.thy
-   ID:        $Id$
-   Author:    Thomas Stauner
-   Copyright  1995 TU Muenchen
-
-   Recursive definition of type inference algorithm I for Mini_ML.
-*)
-
-I = W +
-
-consts
-        I :: [expr, typ list, nat, subst] => result_W
-
-primrec
-        "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
-                                    else Fail)"
-        "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
-                                     Ok(s, TVar n -> t, m) )"
-        "I (App e1 e2) a n s =
-                   ( (s1,t1,m1) := I e1 a n s;
-                     (s2,t2,m2) := I e2 a m1 s1;
-                     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
-                     Ok($u o s2, TVar m2, Suc m2) )"
-end
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/Maybe.ML
--- a/src/HOL/W0/Maybe.ML	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title:     HOL/W0/Maybe.ML
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-*)
-
-
-(* constructor laws for bind *)
-Goalw [bind_def] "(Ok s) bind f = (f s)";
-by (Simp_tac 1);
-qed "bind_Ok";
-
-Goalw [bind_def] "Fail bind f = Fail";
-by (Simp_tac 1);
-qed "bind_Fail";
-
-Addsimps [bind_Ok,bind_Fail];
-
-(* case splitting of bind *)
-Goal
-  "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
-by (induct_tac "res" 1);
-by (fast_tac (HOL_cs addss simpset()) 1);
-by (Asm_simp_tac 1);
-qed "split_bind";
-
-Goal
-  "P(res bind f) = (~ (res = Fail & ~ P Fail | (? s. res = Ok s & ~ P(f s))))";
- by (simp_tac (simpset() addsplits [split_bind]) 1);
-qed "split_bind_asm";
-
-bind_thms ("bind_splits", [split_bind, split_bind_asm]);
-
-Goal
-  "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-qed "bind_eq_Fail";
-
-Addsimps [bind_eq_Fail];
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/Maybe.thy
--- a/src/HOL/W0/Maybe.thy	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title:     HOL/W0/Maybe.thy
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-
-Universal error monad.
-*)
-
-Maybe = List +
-
-datatype 'a maybe =  Ok 'a | Fail
-
-constdefs
-  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
-  "m bind f == case m of Ok r => f r | Fail => Fail"
-
-syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "E bind (%P. F)"
-
-end
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/MiniML.ML
--- a/src/HOL/W0/MiniML.ML	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title:     HOL/W0/MiniML.ML
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-*)
-
-open MiniML;
-
-Addsimps has_type.intrs;
-Addsimps [Un_upper1,Un_upper2];
-
-
-(* has_type is closed w.r.t. substitution *)
-Goal "a |- e :: t ==> $s a |- e :: $s t";
-by (etac has_type.induct 1);
-(* case VarI *)
-by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
-by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
-by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (simpset() delsimps [nth_map])) 1);
-(* case AbsI *)
-by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
-(* case AppI *)
-by (Asm_full_simp_tac 1);
-qed "has_type_cl_sub";
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/MiniML.thy
--- a/src/HOL/W0/MiniML.thy	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title:     HOL/W0/MiniML.thy
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-
-Mini_ML with type inference rules.
-*)
-
-MiniML = Type + 
-
-(* expressions *)
-datatype
-        expr = Var nat | Abs expr | App expr expr
-
-(* type inference rules *)
-consts
-        has_type :: "(typ list * expr * typ)set"
-syntax
-        "@has_type" :: [typ list, expr, typ] => bool
-                       ("((_) |-/ (_) :: (_))" [60,0,60] 60)
-translations 
-        "a |- e :: t" == "(a,e,t):has_type"
-
-inductive has_type
-intrs
-        VarI "[| n < length a |] ==> a |- Var n :: a!n"
-        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
-        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
-              ==> a |- App e1 e2 :: t1"
-
-end
-
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML	Mon Feb 25 20:51:48 2002 +0100
+++ b/src/HOL/W0/ROOT.ML	Tue Feb 26 00:19:04 2002 +0100
@@ -1,13 +1,2 @@
-(*  Title:      HOL/W0/ROOT.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TUM
 
-Type inference for let-free MiniML
-*)
-
-Unify.trace_bound := 20;
-
-AddSEs [less_SucE];
-
-time_use_thy "I";
+use_thy "W0";
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,341 +0,0 @@
-(* Title:     HOL/W0/Type.ML
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-*)
-
-Addsimps [mgu_eq,mgu_mg,mgu_free];
-
-(* mgu does not introduce new type variables *)
-Goalw [new_tv_def] 
-      "[|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
-\            new_tv n u";
-by (fast_tac (set_cs addDs [mgu_free]) 1);
-qed "mgu_new";
-
-(* application of id_subst does not change type expression *)
-Goalw [id_subst_def]
-  "$ id_subst = (%t::typ. t)";
-by (rtac ext 1);
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_te";
-Addsimps [app_subst_id_te];
-
-(* application of id_subst does not change list of type expressions *)
-Goalw [app_subst_list]
-  "$ id_subst = (%ts::typ list. ts)";
-by (rtac ext 1); 
-by (induct_tac "ts" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_tel";
-Addsimps [app_subst_id_tel];
-
-Goalw [id_subst_def,o_def] "$s o id_subst = s";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "o_id_subst";
-Addsimps[o_id_subst];
-
-Goalw [dom_def,id_subst_def,empty_def]
-  "dom id_subst = {}";
-by (Simp_tac 1);
-qed "dom_id_subst";
-Addsimps [dom_id_subst];
-
-Goalw [cod_def]
-  "cod id_subst = {}";
-by (Simp_tac 1);
-qed "cod_id_subst";
-Addsimps [cod_id_subst];
-
-Goalw [free_tv_subst]
-  "free_tv id_subst = {}";
-by (Simp_tac 1);
-qed "free_tv_id_subst";
-Addsimps [free_tv_id_subst];
-
-Goalw [dom_def,cod_def,UNION_def,Bex_def]
-  "[| v : free_tv(s n); v~=n |] ==> v : cod s";
-by (Simp_tac 1);
-by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
-by (assume_tac 2);
-by (rotate_tac 1 1);
-by (Asm_full_simp_tac 1);
-qed "cod_app_subst";
-Addsimps [cod_app_subst];
-
-
-(* composition of substitutions *)
-Goal
-  "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "subst_comp_te";
-
-Goalw [app_subst_list]
-  "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
-by (induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (asm_full_simp_tac (simpset() addsimps [subst_comp_te]) 1);
-qed "subst_comp_tel";
-
-
-(* constructor laws for app_subst *)
-Goalw [app_subst_list]
-  "$ s [] = []";
-by (Simp_tac 1);
-qed "app_subst_Nil";
-
-Goalw [app_subst_list]
-  "$ s (t#ts) = ($ s t)#($ s ts)";
-by (Simp_tac 1);
-qed "app_subst_Cons";
-
-Addsimps [app_subst_Nil,app_subst_Cons];
-
-(* constructor laws for new_tv *)
-Goalw [new_tv_def]
-  "new_tv n (TVar m) = (m<n)";
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "new_tv_TVar";
-
-Goalw [new_tv_def]
-  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "new_tv_Fun";
-
-Goalw [new_tv_def]
-  "new_tv n []";
-by (Simp_tac 1);
-qed "new_tv_Nil";
-
-Goalw [new_tv_def]
-  "new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "new_tv_Cons";
-
-Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons];
-
-Goalw [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
-  "new_tv n id_subst";
-by (Simp_tac 1);
-qed "new_tv_id_subst";
-Addsimps[new_tv_id_subst];
-
-Goalw [new_tv_def]
-  "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
-\                (! l. l < n --> new_tv n (s l) ))";
-by (safe_tac HOL_cs );
-(* ==> *)
-by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1);
-by (subgoal_tac "m:cod s | s l = TVar l" 1);
-by (safe_tac HOL_cs );
-by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1);
-by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
-by (Asm_full_simp_tac 1);
-by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1);
-(* <== *)
-by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
-by (safe_tac set_cs );
-by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
-by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-qed "new_tv_subst";
-
-Goal "new_tv n x = (!y:set x. new_tv n y)";
-by (induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "new_tv_list";
-
-(* substitution affects only variables occurring freely *)
-Goal
-  "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "subst_te_new_tv";
-Addsimps [subst_te_new_tv];
-
-Goal
-  "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
-by (induct_tac "ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst_tel_new_tv";
-Addsimps [subst_tel_new_tv];
-
-(* all greater variables are also new *)
-Goal
-  "n<=m --> new_tv n (t::typ) --> new_tv m t";
-by (induct_tac "t" 1);
-(* case TVar n *)
-by (fast_tac (HOL_cs addIs [less_le_trans] addss simpset()) 1);
-(* case Fun t1 t2 *)
-by (Asm_simp_tac 1);
-qed_spec_mp "new_tv_le";
-Addsimps [lessI RS less_imp_le RS new_tv_le];
-
-Goal 
-  "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by (induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case a#al *)
-by (fast_tac (HOL_cs addIs [new_tv_le] addss simpset()) 1);
-qed_spec_mp "new_tv_list_le";
-Addsimps [lessI RS less_imp_le RS new_tv_list_le];
-
-Goal
-  "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
-by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
-by (Clarify_tac 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) );
-qed "new_tv_subst_le";
-Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
-
-(* new_tv property remains if a substitution is applied *)
-Goal
-  "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
-by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_var";
-
-Goal "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
-by (induct_tac "t" 1);
-by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
-qed_spec_mp "new_tv_subst_te";
-Addsimps [new_tv_subst_te];
-
-Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
-by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (induct_tac "ts" 1);
-by Safe_tac;
-by    (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
-qed_spec_mp "new_tv_subst_tel";
-Addsimps [new_tv_subst_tel];
-
-(* auxilliary lemma *)
-Goal "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
-by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-qed "new_tv_Suc_list";
-
-
-(* composition of substitutions preserves new_tv proposition *)
-Goal 
-     "[| new_tv n (s::subst); new_tv n r |] ==> \
-\           new_tv n (($ r) o s)";
-by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_comp_1";
-
-Goal
-     "[| new_tv n (s::subst); new_tv n r |] ==>  \ 
-\     new_tv n (%v.$ r (s v))";
-by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_comp_2";
-
-Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
-
-(* new type variables do not occur freely in a type structure *)
-Goalw [new_tv_def] 
-      "new_tv n ts ==> n~:(free_tv ts)";
-by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
-qed "new_tv_not_free_tv";
-Addsimps [new_tv_not_free_tv];
-
-Goal
-  "(t::typ): set ts --> free_tv t <= free_tv ts";
-by (induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (fast_tac (set_cs addss simpset()) 1);
-qed_spec_mp "ftv_mem_sub_ftv_list";
-Addsimps [ftv_mem_sub_ftv_list];
-
-
-(* if two substitutions yield the same result if applied to a type
-   structure the substitutions coincide on the free type variables
-   occurring in the type structure *)
-Goal
-  "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (induct_tac "t" 1);
-(* case TVar n *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-(* case Fun t1 t2 *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed_spec_mp "eq_subst_te_eq_free";
-
-Goal
-  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
-by (induct_tac "t" 1);
-(* case TVar n *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-(* case Fun t1 t2 *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed_spec_mp "eq_free_eq_subst_te";
-
-Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
-by (induct_tac "ts" 1);
-(* case [] *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-(* case x#xl *)
-by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1);
-qed_spec_mp "eq_subst_tel_eq_free";
-
-Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
-by (induct_tac "ts" 1); 
-(* case [] *)
-by (fast_tac (HOL_cs addss simpset()) 1);
-(* case x#xl *)
-by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (simpset())) 1);
-qed_spec_mp "eq_free_eq_subst_tel";
-
-(* some useful theorems *)
-Goalw [free_tv_subst] 
-      "v : cod s ==> v : free_tv s";
-by (fast_tac set_cs 1);
-qed "codD";
- 
-Goalw [free_tv_subst,dom_def] 
-      "x ~: free_tv s ==> s x = TVar x";
-by (fast_tac set_cs 1);
-qed "not_free_impl_id";
-
-Goalw [new_tv_def] "[| new_tv n t; m:free_tv t |] ==> m<n";
-by (fast_tac HOL_cs 1 );
-qed "free_tv_le_new_tv";
-
-Goal "free_tv (s (v::nat)) <= insert v (cod s)";
-by (expand_case_tac "v:dom s" 1);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
-by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
-qed "free_tv_subst_var";
-
-Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by (induct_tac "t" 1);
-(* case TVar n *)
-by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
-(* case Fun t1 t2 *)
-by (fast_tac (set_cs addss simpset()) 1);
-qed "free_tv_app_subst_te";     
-
-Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by (induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case a#al *)
-by (cut_facts_tac [free_tv_app_subst_te] 1);
-by (fast_tac (set_cs addss simpset()) 1);
-qed "free_tv_app_subst_tel";
-
-Goalw [free_tv_subst,dom_def]
-     "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
-\     free_tv s1 Un free_tv s2";
-by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
-			     free_tv_subst_var RS subsetD] 
-	             addss (simpset() delsimps bex_simps
-				     addsimps [cod_def,dom_def])) 1);
-qed "free_tv_comp_subst";
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/Type.thy
--- a/src/HOL/W0/Type.thy	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-(* Title:     HOL/W0/Type.thy
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-
-MiniML-types and type substitutions.
-*)
-
-Type = Maybe + 
-
-(* new class for structures containing type variables *)
-classes
-        type_struct < type
-
-(* type expressions *)
-datatype
-        typ = TVar nat | "->" typ typ (infixr 70)
-
-(* type variable substitution *)
-types
-        subst = nat => typ
-
-arities
-        typ::type_struct
-        list::(type_struct)type_struct
-        fun::(type,type_struct)type_struct
-
-(* substitutions *)
-
-(* identity *)
-constdefs
-        id_subst :: subst
-        "id_subst == (%n. TVar n)"
-
-(* extension of substitution to type structures *)
-consts
-        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
-
-primrec
-  app_subst_TVar  "$ s (TVar n) = s n" 
-  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
-
-defs
-        app_subst_list  "$ s == map ($ s)"
-  
-(* free_tv s: the type variables occuring freely in the type structure s *)
-consts
-        free_tv :: ['a::type_struct] => nat set
-
-primrec
-  "free_tv (TVar m) = {m}"
-  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-
-primrec
-  "free_tv [] = {}"
-  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
-
-(* domain of a substitution *)
-constdefs
-        dom :: subst => nat set
-        "dom s == {n. s n ~= TVar n}" 
-
-(* codomain of a substitutions: the introduced variables *)
-constdefs
-        cod :: subst => nat set
-        "cod s == (UN m:dom s. free_tv (s m))"
-
-defs
-        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
-
-(* new_tv s n computes whether n is a new type variable w.r.t. a type 
-   structure s, i.e. whether n is greater than any type variable 
-   occuring in the type structure *)
-constdefs
-        new_tv :: [nat,'a::type_struct] => bool
-        "new_tv n ts == ! m. m:free_tv ts --> m<n"
-
-(* unification algorithm mgu *)
-consts
-        mgu :: [typ,typ] => subst maybe
-rules
-        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
-        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
-                  ? r. s = $r o u"
-        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
-        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
-
-end
-
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title:     HOL/W0/W.ML
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-
-Correctness and completeness of type inference algorithm W
-*)
-
-Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
-
-Delsimps (ex_simps @ all_simps);
-
-(* correctness of W with respect to has_type *)
-Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
-by (induct_tac "e" 1);
-(* case Var n *)
-by (Asm_simp_tac 1);
-(* case Abs e *)
-by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
-                        addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (dtac sym 1);
-by (fast_tac (HOL_cs addss simpset()) 1);
-(* case App e1 e2 *)
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (strip_tac 1);
-by ( rename_tac "sa ta na sb tb nb sc" 1);
-by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
-by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
-by (rtac (app_subst_Fun RS subst) 1);
-by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
-by (Asm_full_simp_tac 1);
-by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym,o_def]) 1);
-by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (asm_full_simp_tac (simpset() addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
-qed_spec_mp "W_correct";
-
-val has_type_casesE = map has_type.mk_cases
-        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
-
-(* the resulting type variable is always greater or equal than the given one *)
-Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
-by (induct_tac "e" 1);
-(* case Var(n) *)
-by (Clarsimp_tac 1);
-(* case Abs e *)
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
-(* case App e1 e2 *)
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb" 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "W_var_ge";
-
-Addsimps [W_var_ge];
-
-Goal "Ok (s,t,m) = W e a n ==> n<=m";
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-qed "W_var_geD";
-
-
-(* auxiliary lemma *)
-goal Maybe.thy "(y = Ok x) = (Ok x = y)";
-by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-qed "rotate_Ok";
-
-
-(* resulting type variable is new *)
-Goal "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
-\                 new_tv m s & new_tv m t";
-by (induct_tac "e" 1);
-(* case Var n *)
-  by (Clarsimp_tac 1);
-  by (force_tac (claset() addEs [list_ball_nth],
-		simpset() addsimps [id_subst_def,new_tv_list,new_tv_subst])1);
-(* case Abs e *)
- by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
-    addsplits [split_bind]) 1);
- by (strip_tac 1);
- by (eres_inst_tac [("x","Suc n")] allE 1);
- by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
- by (fast_tac (HOL_cs addss (simpset()
-              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
-
-(* case App e1 e2 *)
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb" 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
-by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Ok]) 1);
-by (rtac conjI 1);
-by (rtac new_tv_subst_comp_2 1);
-by (rtac new_tv_subst_comp_2 1);
-by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
-by (res_inst_tac [("n","na")] new_tv_subst_le 1); 
-by (asm_full_simp_tac (simpset() addsimps [rotate_Ok]) 1);
-by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] addIs
-     [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
-    1);
-by (etac (sym RS mgu_new) 1);
-by (best_tac (HOL_cs addDs [W_var_geD] 
-                     addIs [new_tv_subst_te,new_tv_list_le,
-                            new_tv_subst_tel,
-                            lessI RS less_imp_le RS new_tv_le,
-                            lessI RS less_imp_le RS new_tv_subst_le,
-                            new_tv_le]) 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] 
-                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
-                     addss (simpset())) 1);
-by (rtac (lessI RS new_tv_subst_var) 1);
-by (etac (sym RS mgu_new) 1);
-by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
-                     addDs [W_var_geD]
-                     addIs [new_tv_list_le,
-                            new_tv_subst_tel,
-                            lessI RS less_imp_le RS new_tv_subst_le,
-                            new_tv_le] 
-                     addss simpset()) 1);
-by (fast_tac (HOL_cs addDs [W_var_geD] 
-                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
-                     addss (simpset())) 1);
-qed_spec_mp "new_tv_W";
-
-
-Goal "!n a s t m v. W e a n = Ok (s,t,m) -->            \
-\         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
-by (induct_tac "e" 1);
-(* case Var n *)
-by (Clarsimp_tac 1);
-by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list])1);
-
-(* case Abs e *)
-by (asm_full_simp_tac (simpset() addsimps
-    [free_tv_subst] addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (rename_tac "s t n1 v" 1);
-by (eres_inst_tac [("x","Suc n")] allE 1);
-by (eres_inst_tac [("x","TVar n # a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","n1")] allE 1);
-by (eres_inst_tac [("x","v")] allE 1);
-by (force_tac (claset() addSEs [allE] addIs [cod_app_subst], simpset()) 1);
-(** LEVEL 13 **)
-(* case App e1 e2 *)
-by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (rename_tac "s t n1 s1 t1 n2 s3 v" 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
-by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","n1")] allE 1);
-by (eres_inst_tac [("x","n1")] allE 1);
-by (eres_inst_tac [("x","v")] allE 1);
-(** LEVEL 23 **)
-(* second case *)
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","s1")] allE 1);
-by (eres_inst_tac [("x","t1")] allE 1);
-by (eres_inst_tac [("x","n2")] allE 1);
-by (eres_inst_tac [("x","v")] allE 1);
-by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
- by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1);
- by (dtac W_var_geD 1);
- by (dtac W_var_geD 1);
- by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
-(** LEVEL 33 **)
- by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
-    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
-    subsetD]
-  addEs [UnE] 
-  addss simpset()) 1);
-by (Asm_full_simp_tac 1); 
-by (dtac (sym RS W_var_geD) 1);
-by (dtac (sym RS W_var_geD) 1);
-by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
-by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
-                            free_tv_app_subst_te RS subsetD,
-                            free_tv_app_subst_tel RS subsetD,
-                            less_le_trans,subsetD]
-                     addSEs [UnE]
-                     addss (simpset() setSolver unsafe_solver)) 1);
-(* builtin arithmetic in simpset messes things up *)
-qed_spec_mp "free_tv_W"; 
-
-(* Completeness of W w.r.t. has_type *)
-Goal "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
-\             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
-\                     (? r. $s' a = $r ($s a) & t' = $r t))";
-by (induct_tac "e" 1);
-(* case Var n *)
-by (strip_tac 1);
-by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (eresolve_tac has_type_casesE 1); 
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1);
-by (res_inst_tac [("x","s'")] exI 1);
-by (Asm_simp_tac 1);
-
-(** LEVEL 7 **)
-(* case Abs e *)
-by (strip_tac 1);
-by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x. if x=n then t1 else (s' x)")] allE 1);
-by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
-by (eres_inst_tac [("x","t2")] allE 1);
-by (eres_inst_tac [("x","Suc n")] allE 1);
-by (fast_tac (HOL_cs addss (simpset() addcongs [conj_cong]
-                            addsplits [split_bind])) 1);
-
-(** LEVEL 14 **)
-(* case App e1 e2 *)
-by (strip_tac 1);
-by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","s'")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","t2 -> t'")] allE 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (safe_tac HOL_cs);
-by (eres_inst_tac [("x","r")] allE 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","t2")] allE 1);
-by (eres_inst_tac [("x","m")] allE 1);
-by (Asm_full_simp_tac 1);
-by (safe_tac HOL_cs);
-by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
-                            conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
-
-(** LEVEL 28 **)
-by (subgoal_tac
-  "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\        else ra x)) ($ sa t) = \
-\  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\        else ra x)) (ta -> (TVar ma))" 1);
-by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
-\   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
-    ("s","($ ra ta) -> t'")] ssubst 2);
-by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2);
-by (rtac eq_free_eq_subst_te 2);  
-by (strip_tac 2);
-by (subgoal_tac "na ~=ma" 2);
-by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
-                            new_tv_not_free_tv,new_tv_le]) 3);
-(** LEVEL 35 **)
-by (case_tac "na:free_tv sa" 2);
-(* na ~: free_tv sa *)
-by (ftac not_free_impl_id 3);
-by (Asm_simp_tac 3);
-(* na : free_tv sa *)
-by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
-by (dtac eq_subst_tel_eq_free 2);
-by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
-by (Asm_simp_tac 2); 
-by (case_tac "na:dom sa" 2);
-(* na ~: dom sa *)
-(** LEVEL 43 **)
-by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
-(* na : dom sa *)
-by (rtac eq_free_eq_subst_te 2);
-by (strip_tac 2);
-by (subgoal_tac "nb ~= ma" 2);
-by ((ftac new_tv_W 3) THEN (atac 3));
-by (etac conjE 3);
-by (dtac new_tv_subst_tel 3);
-by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
-by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
-              (simpset() addsimps [cod_def,free_tv_subst])) 3);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
-
-(** LEVEL 53 **)
-by (Simp_tac 2);  
-by (rtac eq_free_eq_subst_te 2);
-by (strip_tac 2 );
-by (subgoal_tac "na ~= ma" 2);
-by ((ftac new_tv_W 3) THEN (atac 3));
-by (etac conjE 3);
-by (dtac (sym RS W_var_geD) 3);
-by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
-by (case_tac "na: free_tv t - free_tv sa" 2);
-(** LEVEL 62 **)
-(* case na ~: free_tv t - free_tv sa *)
-by (Asm_full_simp_tac 3);
-(* case na : free_tv t - free_tv sa *)
-by (Asm_full_simp_tac 2);
-by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
-by (dtac eq_subst_tel_eq_free 2);
-by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
-by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2);
-by (Fast_tac 2);
-(** LEVEL 69 **)
-by (asm_simp_tac (simpset() addsplits [split_bind]) 1);
-by (safe_tac HOL_cs);
-by (dtac mgu_Ok 1);
-by ( fast_tac (HOL_cs addss simpset()) 1);
-by ((dtac mgu_mg 1) THEN (atac 1));
-by (etac exE 1);
-by (res_inst_tac [("x","rb")] exI 1);
-by (rtac conjI 1);
-by (dres_inst_tac [("x","ma")] fun_cong 2);
-by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2);
-by (simp_tac (simpset() addsimps [o_def,subst_comp_tel RS sym]) 1);
-(** LEVEL 80 **)
-by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
-by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
-by (dres_inst_tac [("s","Ok ?X")] sym 1);
-by (rtac eq_free_eq_subst_tel 1);
-by ( safe_tac HOL_cs );
-by (subgoal_tac "ma ~= na" 1);
-by ((ftac new_tv_W 2) THEN (atac 2));
-by (etac conjE 2);
-by (dtac new_tv_subst_tel 2);
-by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
-by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2);
-(** LEVEL 100 **)
-by (etac conjE 2);
-by (dtac (free_tv_app_subst_tel RS subsetD) 2);
-by (fast_tac (set_cs addDs [sym RS W_var_geD,new_tv_list_le,codD,
-    new_tv_not_free_tv]) 2);
-by (case_tac "na: free_tv t - free_tv sa" 1);
-(* case na ~: free_tv t - free_tv sa *)
-by (Asm_full_simp_tac 2);
-(* case na : free_tv t - free_tv sa *)
-by (Asm_full_simp_tac 1);
-by (dtac (free_tv_app_subst_tel RS subsetD) 1);
-by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
-                            eq_subst_tel_eq_free] 
-       addss ((simpset() addsimps [free_tv_subst,dom_def]))) 1);
-(** LEVEL 106 **)
-by (Fast_tac 1);
-qed_spec_mp "W_complete_lemma";
-
-Goal "[] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
-\                                 (? r. t' = $r t))";
-by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
-                W_complete_lemma 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "W_complete";
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/W.thy
--- a/src/HOL/W0/W.thy	Mon Feb 25 20:51:48 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title:     HOL/MiniML/W.thy
-   ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
-
-Type inference algorithm W
-*)
-
-W = MiniML + 
-
-types 
-        result_W = "(subst * typ * nat)maybe"
-
-(* type inference algorithm W *)
-consts
-        W :: [expr, typ list, nat] => result_W
-
-primrec
-  "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
-                    else Fail)"
-  "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
-                     Ok(s, (s n) -> t, m) )"
-  "W (App e1 e2) a n =
-                 ( (s1,t1,m1) := W e1 a n;
-                   (s2,t2,m2) := W e2 ($s1 a) m1;
-                   u := mgu ($s2 t1) (t2 -> (TVar m2));
-                   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
-end
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/W0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/W0.thy	Tue Feb 26 00:19:04 2002 +0100
@@ -0,0 +1,947 @@
+(*  Title:      HOL/W0/W0.thy
+    ID:         $Id$
+    Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, and Markus Wenzel
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+theory W0 = Main:
+
+section {* Universal error monad *}
+
+datatype 'a maybe = Ok 'a | Fail
+
+constdefs
+  bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60)
+  "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
+
+syntax
+  "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
+translations
+  "P := E; F" == "E \<bind> (\<lambda>P. F)"
+
+lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)"
+  by (simp add: bind_def)
+
+lemma bind_Fail [simp]: "Fail \<bind> f = Fail"
+  by (simp add: bind_def)
+
+lemma split_bind:
+    "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))"
+  by (induct res) simp_all
+
+lemma split_bind_asm:
+  "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))"
+  by (simp split: split_bind)
+
+lemmas bind_splits = split_bind split_bind_asm
+
+lemma bind_eq_Fail [simp]:
+  "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> f p = Fail))"
+  by (simp split: split_bind)
+
+lemma rotate_Ok: "(y = Ok x) = (Ok x = y)"
+  by (rule eq_sym_conv)
+
+
+section {* MiniML-types and type substitutions *}
+
+axclass type_struct \<subseteq> type
+  -- {* new class for structures containing type variables *}
+
+datatype "typ" = TVar nat | TFun "typ" "typ"    (infixr "->" 70)
+  -- {* type expressions *}
+
+types subst = "nat => typ"
+  -- {* type variable substitution *}
+
+instance "typ" :: type_struct ..
+instance list :: (type_struct) type_struct ..
+instance fun :: (type, type_struct) type_struct ..
+
+
+subsection {* Substitutions *}
+
+consts
+  app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
+  -- {* extension of substitution to type structures *}
+primrec
+  app_subst_TVar: "$s (TVar n) = s n"
+  app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
+
+defs (overloaded)
+  app_subst_list: "$s \<equiv> map ($s)"
+
+consts
+  free_tv :: "'a::type_struct \<Rightarrow> nat set"
+  -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
+
+primrec
+  "free_tv (TVar m) = {m}"
+  "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
+
+primrec
+  "free_tv [] = {}"
+  "free_tv (x # xs) = free_tv x \<union> free_tv xs"
+
+constdefs
+  dom :: "subst \<Rightarrow> nat set"
+  "dom s \<equiv> {n. s n \<noteq> TVar n}"
+  -- {* domain of a substitution *}
+
+  cod :: "subst \<Rightarrow> nat set"
+  "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
+  -- {* codomain of a substitutions: the introduced variables *}
+
+defs
+  free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
+
+text {*
+  @{text "new_tv s n"} checks whether @{text n} is a new type variable
+  wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
+  than any type variable occuring in the type structure.
+*}
+
+constdefs
+  new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
+  "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
+
+
+subsubsection {* Identity substitution *}
+
+constdefs
+  id_subst :: subst
+  "id_subst \<equiv> \<lambda>n. TVar n"
+
+lemma app_subst_id_te [simp]:
+  "$id_subst = (\<lambda>t::typ. t)"
+  -- {* application of @{text id_subst} does not change type expression *}
+proof
+  fix t :: "typ"
+  show "$id_subst t = t"
+    by (induct t) (simp_all add: id_subst_def)
+qed
+
+lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)"
+  -- {* application of @{text id_subst} does not change list of type expressions *}
+proof
+  fix ts :: "typ list"
+  show "$id_subst ts = ts"
+    by (induct ts) (simp_all add: app_subst_list)
+qed
+
+lemma o_id_subst [simp]: "$s o id_subst = s"
+  by (rule ext) (simp add: id_subst_def)
+
+lemma dom_id_subst [simp]: "dom id_subst = {}"
+  by (simp add: dom_def id_subst_def empty_def)
+
+lemma cod_id_subst [simp]: "cod id_subst = {}"
+  by (simp add: cod_def)
+
+lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
+  by (simp add: free_tv_subst)
+
+
+lemma cod_app_subst [simp]:
+  assumes free: "v \<in> free_tv (s n)"
+    and neq: "v \<noteq> n"
+  shows "v \<in> cod s"
+proof -
+  have "s n \<noteq> TVar n"
+  proof
+    assume "s n = TVar n"
+    with free have "v = n" by simp
+    with neq show False ..
+  qed
+  with free show ?thesis
+    by (auto simp add: dom_def cod_def)
+qed
+
+lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t"
+  -- {* composition of substitutions *}
+  by (induct t) simp_all
+
+lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts"
+  by (induct ts) (simp_all add: app_subst_list subst_comp_te)
+
+
+lemma app_subst_Nil [simp]: "$s [] = []"
+  by (simp add: app_subst_list)
+
+lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
+  by (simp add: app_subst_list)
+
+lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
+  by (simp add: new_tv_def)
+
+lemma new_tv_Fun [simp]:
+  "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
+  by (auto simp add: new_tv_def)
+
+lemma new_tv_Nil [simp]: "new_tv n []"
+  by (simp add: new_tv_def)
+
+lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)"
+  by (auto simp add: new_tv_def)
+
+lemma new_tv_id_subst [simp]: "new_tv n id_subst"
+  by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
+
+lemma new_tv_subst:
+  "new_tv n s =
+    ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
+     (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
+  apply (unfold new_tv_def)
+  apply (tactic "safe_tac HOL_cs")
+  -- {* @{text \<Longrightarrow>} *}
+    apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
+      addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
+   apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
+    apply (tactic "safe_tac HOL_cs")
+     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
+       addsimps [thm "free_tv_subst"])) 1 *})
+    apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
+    apply simp
+   apply (tactic {* fast_tac (set_cs addss (simpset()
+     addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
+  -- {* @{text \<Longleftarrow>} *}
+  apply (unfold free_tv_subst cod_def dom_def)
+  apply (tactic "safe_tac set_cs")
+   apply (cut_tac m = m and n = n in less_linear)
+   apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
+  apply (cut_tac m = ma and n = n in less_linear)
+  apply (fast intro!: less_or_eq_imp_le)
+  done
+
+lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
+  by (induct x) simp_all
+
+lemma subst_te_new_tv [simp]:
+  "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
+  -- {* substitution affects only variables occurring freely *}
+  by (induct t) simp_all
+
+lemma subst_tel_new_tv [simp]:
+  "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
+  by (induct ts) simp_all
+
+lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
+  -- {* all greater variables are also new *}
+proof (induct t)
+  case (TVar n)
+  thus ?case by (auto intro: less_le_trans)
+next
+  case TFun
+  thus ?case by simp
+qed
+
+lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
+  by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
+
+lemma new_tv_list_le:
+  "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
+proof (induct ts)
+  case Nil
+  thus ?case by simp
+next
+  case Cons
+  thus ?case by (auto intro: new_tv_le)
+qed
+
+lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
+  by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
+
+lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
+  apply (simp add: new_tv_subst)
+  apply clarify
+  apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
+    apply clarify
+    apply (simp_all add: new_tv_le)
+  done
+
+lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
+  by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
+
+lemma new_tv_subst_var:
+    "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
+  -- {* @{text new_tv} property remains if a substitution is applied *}
+  by (simp add: new_tv_subst)
+
+lemma new_tv_subst_te [simp]:
+    "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
+  by (induct t) (auto simp add: new_tv_subst)
+
+lemma new_tv_subst_tel [simp]:
+    "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
+  by (induct ts) (fastsimp simp add: new_tv_subst)+
+
+lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
+  -- {* auxilliary lemma *}
+  by (simp add: new_tv_list)
+
+lemma new_tv_subst_comp_1 [simp]:
+    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
+  -- {* composition of substitutions preserves @{text new_tv} proposition *}
+  by (simp add: new_tv_subst)
+
+lemma new_tv_subst_comp_2 [simp]:
+    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
+  by (simp add: new_tv_subst)
+
+lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
+  -- {* new type variables do not occur freely in a type structure *}
+  by (auto simp add: new_tv_def)
+
+lemma ftv_mem_sub_ftv_list [simp]:
+    "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
+  by (induct ts) auto
+
+text {*
+  If two substitutions yield the same result if applied to a type
+  structure the substitutions coincide on the free type variables
+  occurring in the type structure.
+*}
+
+lemma eq_subst_te_eq_free:
+    "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
+  by (induct t) auto
+
+lemma eq_free_eq_subst_te:
+    "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
+  by (induct t) auto
+
+lemma eq_subst_tel_eq_free:
+    "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
+  by (induct ts) (auto intro: eq_subst_te_eq_free)
+
+lemma eq_free_eq_subst_tel:
+    "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
+  by (induct ts) (auto intro: eq_free_eq_subst_te)
+
+text {*
+  \medskip Some useful lemmas.
+*}
+
+lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
+  by (simp add: free_tv_subst)
+
+lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
+  by (simp add: free_tv_subst dom_def)
+
+lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
+  by (unfold new_tv_def) fast
+
+lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
+  by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
+
+lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
+  by (induct t) (auto simp add: free_tv_subst_var)
+
+lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
+  apply (induct ts)
+   apply simp
+  apply (cut_tac free_tv_app_subst_te)
+  apply fastsimp
+  done
+
+lemma free_tv_comp_subst:
+    "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
+  apply (unfold free_tv_subst dom_def)
+  apply (tactic {*
+    fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
+    thm "free_tv_subst_var" RS subsetD]
+    addss (simpset() delsimps bex_simps
+    addsimps [thm "cod_def", thm "dom_def"])) 1 *})
+  done
+
+
+subsection {* Most general unifiers *}
+
+consts
+  mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
+axioms
+  mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
+  mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
+  mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
+  mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
+
+lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
+  -- {* @{text mgu} does not introduce new type variables *}
+  by (unfold new_tv_def) (blast dest: mgu_free)
+
+
+section {* Mini-ML with type inference rules *}
+
+datatype
+  expr = Var nat | Abs expr | App expr expr
+
+
+text {* Type inference rules. *}
+
+consts
+  has_type :: "(typ list \<times> expr \<times> typ) set"
+
+syntax
+  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
+    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
+translations
+  "a |- e :: t" == "(a, e, t) \<in> has_type"
+
+inductive has_type
+  intros
+    Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
+    Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
+    App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
+      \<Longrightarrow> a |- App e1 e2 :: t1"
+
+
+text {* Type assigment is closed wrt.\ substitution. *}
+
+lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
+proof -
+  assume "a |- e :: t"
+  thus ?thesis (is "?P a e t")
+  proof induct
+    case (Var a n)
+    hence "n < length (map ($ s) a)" by simp
+    hence "map ($ s) a |- Var n :: map ($ s) a ! n"
+      by (rule has_type.Var)
+    also have "map ($ s) a ! n = $ s (a ! n)"
+      by (rule nth_map)
+    also have "map ($ s) a = $ s a"
+      by (simp only: app_subst_list)
+    finally show "?P a (Var n) (a ! n)" .
+  next
+    case (Abs a e t1 t2)
+    hence "$ s t1 # map ($ s) a |- e :: $ s t2"
+      by (simp add: app_subst_list)
+    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
+      by (rule has_type.Abs)
+    thus "?P a (Abs e) (t1 -> t2)"
+      by (simp add: app_subst_list)
+  next
+    case App
+    thus ?case by (simp add: has_type.App)
+  qed
+qed
+
+
+section {* Correctness and completeness of the type inference algorithm @{text \<W>} *}
+
+consts
+  W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
+
+primrec
+  "\<W> (Var i) a n =
+    (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
+  "\<W> (Abs e) a n =
+    ((s, t, m) := \<W> e (TVar n # a) (Suc n);
+     Ok (s, (s n) -> t, m))"
+  "\<W> (App e1 e2) a n =
+    ((s1, t1, m1) := \<W> e1 a n;
+     (s2, t2, m2) := \<W> e2 ($s1 a) m1;
+     u := mgu ($ s2 t1) (t2 -> TVar m2);
+     Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
+
+theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
+  (is "PROP ?P e")
+proof (induct e)
+  fix a s t m n
+  {
+    fix i
+    assume "Ok (s, t, m) = \<W> (Var i) a n"
+    thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
+  next
+    fix e assume hyp: "PROP ?P e"
+    assume "Ok (s, t, m) = \<W> (Abs e) a n"
+    then obtain t' where "t = s n -> t'"
+        and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
+      by (auto split: bind_splits)
+    with hyp show "$s a |- Abs e :: t"
+      by (force intro: has_type.Abs)
+  next
+    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
+    assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
+    then obtain s1 t1 n1 s2 t2 n2 u where
+          s: "s = $u o $s2 o s1"
+        and t: "t = u n2"
+        and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
+        and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
+        and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
+      by (auto split: bind_splits simp: that)
+    show "$s a |- App e1 e2 :: t"
+    proof (rule has_type.App)
+      from s have s': "$u ($s2 ($s1 a)) = $s a"
+        by (simp add: subst_comp_tel o_def)
+      show "$s a |- e1 :: $u t2 -> t"
+      proof -
+        from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
+        hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
+          by (intro has_type_subst_closed)
+        with s' t mgu_ok show ?thesis by simp
+      qed
+      show "$s a |- e2 :: $u t2"
+      proof -
+        from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
+        hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
+          by (rule has_type_subst_closed)
+        with s' show ?thesis by simp
+      qed
+    qed
+  }
+qed
+
+
+inductive_cases has_type_casesE:
+  "s |- Var n :: t"
+  "s |- Abs e :: t"
+  "s |- App e1 e2 ::t"
+
+
+lemmas [simp] = Suc_le_lessD
+  and [simp del] = less_imp_le ex_simps all_simps
+
+lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
+  -- {* the resulting type variable is always greater or equal than the given one *}
+  apply (atomize (full))
+  apply (induct e)
+    txt {* case @{text "Var n"} *}
+    apply clarsimp
+   txt {* case @{text "Abs e"} *}
+   apply (simp split add: split_bind)
+   apply (fast dest: Suc_leD)
+  txt {* case @{text "App e1 e2"} *}
+  apply (simp (no_asm) split add: split_bind)
+  apply (intro strip)
+  apply (rename_tac s t na sa ta nb sb)
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = n in allE)
+  apply (erule_tac x = "$s a" in allE)
+  apply (erule_tac x = s in allE)
+  apply (erule_tac x = t in allE)
+  apply (erule_tac x = na in allE)
+  apply (erule_tac x = na in allE)
+  apply (simp add: eq_sym_conv)
+  done
+
+lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
+  by (simp add: eq_sym_conv)
+
+lemma new_tv_W: "!!n a s t m.
+  new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
+  -- {* resulting type variable is new *}
+  apply (atomize (full))
+  apply (induct e)
+    txt {* case @{text "Var n"} *}
+    apply clarsimp
+    apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
+   txt {* case @{text "Abs e"} *}
+   apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
+   apply (intro strip)
+   apply (erule_tac x = "Suc n" in allE)
+   apply (erule_tac x = "TVar n # a" in allE)
+   apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
+  txt {* case @{text "App e1 e2"} *}
+  apply (simp (no_asm) split add: split_bind)
+  apply (intro strip)
+  apply (rename_tac s t na sa ta nb sb)
+  apply (erule_tac x = n in allE)
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = s in allE)
+  apply (erule_tac x = t in allE)
+  apply (erule_tac x = na in allE)
+  apply (erule_tac x = na in allE)
+  apply (simp add: eq_sym_conv)
+  apply (erule_tac x = "$s a" in allE)
+  apply (erule_tac x = sa in allE)
+  apply (erule_tac x = ta in allE)
+  apply (erule_tac x = nb in allE)
+  apply (simp add: o_def rotate_Ok)
+  apply (rule conjI)
+   apply (rule new_tv_subst_comp_2)
+    apply (rule new_tv_subst_comp_2)
+     apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
+     apply (rule_tac n = na in new_tv_subst_le)
+      apply (simp add: rotate_Ok)
+     apply (simp (no_asm_simp))
+    apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
+      lessI [THEN less_imp_le, THEN new_tv_subst_le])
+   apply (erule sym [THEN mgu_new])
+    apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
+      lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
+      new_tv_le)
+   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
+     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
+     addss (simpset())) 1 *})
+  apply (rule lessI [THEN new_tv_subst_var])
+  apply (erule sym [THEN mgu_new])
+    apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
+      dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
+        lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
+  apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
+    addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
+    addss (simpset())) 1 *})
+  done
+
+lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
+    (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
+  apply (atomize (full))
+  apply (induct e)
+    txt {* case @{text "Var n"} *}
+    apply clarsimp
+    apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
+   txt {* case @{text "Abs e"} *}
+   apply (simp add: free_tv_subst split add: split_bind)
+   apply (intro strip)
+   apply (rename_tac s t n1 v)
+   apply (erule_tac x = "Suc n" in allE)
+   apply (erule_tac x = "TVar n # a" in allE)
+   apply (erule_tac x = s in allE)
+   apply (erule_tac x = t in allE)
+   apply (erule_tac x = n1 in allE)
+   apply (erule_tac x = v in allE)
+   apply (force elim!: allE intro: cod_app_subst)
+  txt {* case @{text "App e1 e2"} *}
+  apply (simp (no_asm) split add: split_bind)
+  apply (intro strip)
+  apply (rename_tac s t n1 s1 t1 n2 s3 v)
+  apply (erule_tac x = n in allE)
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = s in allE)
+  apply (erule_tac x = t in allE)
+  apply (erule_tac x = n1 in allE)
+  apply (erule_tac x = n1 in allE)
+  apply (erule_tac x = v in allE)
+  txt {* second case *}
+  apply (erule_tac x = "$ s a" in allE)
+  apply (erule_tac x = s1 in allE)
+  apply (erule_tac x = t1 in allE)
+  apply (erule_tac x = n2 in allE)
+  apply (erule_tac x = v in allE)
+  apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
+   apply (simp add: rotate_Ok o_def)
+   apply (drule W_var_geD)
+   apply (drule W_var_geD)
+   apply (frule less_le_trans, assumption)
+   apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
+     free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
+  apply simp
+  apply (drule sym [THEN W_var_geD])
+  apply (drule sym [THEN W_var_geD])
+  apply (frule less_le_trans, assumption)
+  apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
+    thm "free_tv_subst_var" RS subsetD,
+    thm "free_tv_app_subst_te" RS subsetD,
+    thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
+    addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
+      -- {* builtin arithmetic in simpset messes things up *}
+  done
+
+text {*
+  \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
+*}
+
+lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
+    (\<exists>s t. (\<exists>m. \<W> e a n = Ok (s, t, m)) \<and> (\<exists>r. $s' a = $r ($s a) \<and> t' = $r t))"
+  apply (atomize (full))
+  apply (induct e)
+    txt {* case @{text "Var n"} *}
+    apply (intro strip)
+    apply (simp (no_asm) cong add: conj_cong)
+    apply (erule has_type_casesE)
+    apply (simp add: eq_sym_conv app_subst_list)
+    apply (rule_tac x = s' in exI)
+    apply simp
+   txt {* case @{text "Abs e"} *}
+   apply (intro strip)
+   apply (erule has_type_casesE)
+   apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
+   apply (erule_tac x = "TVar n # a" in allE)
+   apply (erule_tac x = t2 in allE)
+   apply (erule_tac x = "Suc n" in allE)
+   apply (fastsimp cong add: conj_cong split add: split_bind)
+  txt {* case @{text "App e1 e2"} *}
+  apply (intro strip)
+  apply (erule has_type_casesE)
+  apply (erule_tac x = s' in allE)
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = "t2 -> t'" in allE)
+  apply (erule_tac x = n in allE)
+  apply (tactic "safe_tac HOL_cs")
+  apply (erule_tac x = r in allE)
+  apply (erule_tac x = "$s a" in allE)
+  apply (erule_tac x = t2 in allE)
+  apply (erule_tac x = m in allE)
+  apply simp
+  apply (tactic "safe_tac HOL_cs")
+   apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
+     thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
+  apply (subgoal_tac
+    "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
+      else ra x)) ($ sa t) =
+    $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
+      else ra x)) (ta -> (TVar ma))")
+   apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
+     else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
+     s = "($ ra ta) -> t'" in ssubst)
+    prefer 2
+    apply (simp add: subst_comp_te)
+    apply (rule eq_free_eq_subst_te)
+    apply (intro strip)
+    apply (subgoal_tac "na \<noteq> ma")
+     prefer 2
+     apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
+    apply (case_tac "na \<in> free_tv sa")
+     txt {* @{text "na \<notin> free_tv sa"} *}
+     prefer 2
+     apply (frule not_free_impl_id)
+     apply simp
+    txt {* @{text "na \<in> free_tv sa"} *}
+    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
+    apply (drule_tac eq_subst_tel_eq_free)
+     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
+    apply simp
+    apply (case_tac "na \<in> dom sa")
+     prefer 2
+     txt {* @{text "na \<noteq> dom sa"} *}
+     apply (simp add: dom_def)
+    txt {* @{text "na \<in> dom sa"} *}
+    apply (rule eq_free_eq_subst_te)
+    apply (intro strip)
+    apply (subgoal_tac "nb \<noteq> ma")
+     prefer 2
+     apply (frule new_tv_W, assumption)
+     apply (erule conjE)
+     apply (drule new_tv_subst_tel)
+      apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
+     apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
+    apply (fastsimp simp add: cod_def free_tv_subst)
+   prefer 2
+   apply (simp (no_asm))
+   apply (rule eq_free_eq_subst_te)
+   apply (intro strip)
+   apply (subgoal_tac "na \<noteq> ma")
+    prefer 2
+    apply (frule new_tv_W, assumption)
+    apply (erule conjE)
+    apply (drule sym [THEN W_var_geD])
+    apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
+   apply (case_tac "na \<in> free_tv t - free_tv sa")
+    prefer 2
+    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
+    apply simp
+    defer
+    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
+    apply simp
+    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
+    apply (drule eq_subst_tel_eq_free)
+     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
+    apply (simp add: free_tv_subst dom_def)
+   prefer 2 apply fast
+  apply (simp (no_asm_simp) split add: split_bind)
+  apply (tactic "safe_tac HOL_cs")
+   apply (drule mgu_Ok)
+   apply fastsimp
+  apply (drule mgu_mg, assumption)
+  apply (erule exE)
+  apply (rule_tac x = rb in exI)
+  apply (rule conjI)
+   prefer 2
+   apply (drule_tac x = ma in fun_cong)
+   apply (simp add: eq_sym_conv)
+  apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
+  apply (rule subst_comp_tel [symmetric, THEN [2] trans])
+  apply (simp add: o_def eq_sym_conv)
+  apply (rule eq_free_eq_subst_tel)
+  apply (tactic "safe_tac HOL_cs")
+  apply (subgoal_tac "ma \<noteq> na")
+   prefer 2
+   apply (frule new_tv_W, assumption)
+   apply (erule conjE)
+   apply (drule new_tv_subst_tel)
+    apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
+   apply (frule_tac n = m in new_tv_W, assumption)
+   apply (erule conjE)
+   apply (drule free_tv_app_subst_tel [THEN subsetD])
+   apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
+     thm "codD", thm "new_tv_not_free_tv"]) 1 *})
+  apply (case_tac "na \<in> free_tv t - free_tv sa")
+   prefer 2
+   txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
+   apply simp
+   defer
+   txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
+   apply simp
+   apply (drule free_tv_app_subst_tel [THEN subsetD])
+   apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
+     eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
+  apply fast
+  done
+
+lemma W_complete: "[] |- e :: t' ==>
+    \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
+  apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
+    apply simp_all
+  done
+
+
+section {* Equivalence of @{text \<W>} and @{text \<I>} *}
+
+text {*
+  Recursive definition of type inference algorithm @{text \<I>} for
+  Mini-ML.
+*}
+
+consts
+  I :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<I>")
+primrec
+  "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
+  "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
+    Ok (s, TVar n -> t, m))"
+  "\<I> (App e1 e2) a n s =
+    ((s1, t1, m1) := \<I> e1 a n s;
+    (s2, t2, m2) := \<I> e2 a m1 s1;
+    u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+    Ok($u o s2, TVar m2, Suc m2))"
+
+text {* \medskip Correctness. *}
+
+lemma I_correct_wrt_W: "!!a m s s' t n.
+    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
+    \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
+  apply (atomize (full))
+  apply (induct e)
+    txt {* case @{text "Var n"} *}
+    apply (simp add: app_subst_list split: split_if)
+   txt {* case @{text "Abs e"} *}
+   apply (tactic {* asm_full_simp_tac
+     (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
+   apply (intro strip)
+   apply (rule conjI)
+    apply (intro strip)
+    apply (erule allE)+
+    apply (erule impE)
+     prefer 2 apply (fastsimp simp add: new_tv_subst)
+    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
+      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
+   apply (intro strip)
+   apply (erule allE)+
+   apply (erule impE)
+    prefer 2 apply (fastsimp simp add: new_tv_subst)
+   apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
+     thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
+  txt {* case @{text "App e1 e2"} *}
+  apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
+  apply (intro strip)
+  apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
+  apply (rule conjI)
+   apply fastsimp
+  apply (intro strip)
+  apply (rename_tac s1 t1' n1')
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = m in allE)
+  apply (erule_tac x = s in allE)
+  apply (erule_tac x = s1' in allE)
+  apply (erule_tac x = t1 in allE)
+  apply (erule_tac x = n1 in allE)
+  apply (erule_tac x = a in allE)
+  apply (erule_tac x = n1 in allE)
+  apply (erule_tac x = s1' in allE)
+  apply (erule_tac x = s2' in allE)
+  apply (erule_tac x = t2 in allE)
+  apply (erule_tac x = n2 in allE)
+  apply (rule conjI)
+   apply (intro strip)
+   apply (rule notI)
+   apply simp
+   apply (erule impE)
+    apply (frule new_tv_subst_tel, assumption)
+    apply (drule_tac a = "$s a" in new_tv_W, assumption)
+    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
+   apply (fastsimp simp add: subst_comp_tel)
+  apply (intro strip)
+  apply (rename_tac s2 t2' n2')
+  apply (rule conjI)
+   apply (intro strip)
+   apply (rule notI)
+   apply simp
+   apply (erule impE)
+   apply (frule new_tv_subst_tel, assumption)
+   apply (drule_tac a = "$s a" in new_tv_W, assumption)
+    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
+   apply (fastsimp simp add: subst_comp_tel subst_comp_te)
+  apply (intro strip)
+  apply (erule (1) notE impE)
+  apply (erule (1) notE impE)
+  apply (erule exE)
+  apply (erule conjE)
+  apply (erule impE)
+   apply (frule new_tv_subst_tel, assumption)
+   apply (drule_tac a = "$s a" in new_tv_W, assumption)
+   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
+  apply (erule (1) notE impE)
+  apply (erule exE conjE)+
+  apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
+  apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
+   apply (simp add: new_tv_subst)
+  apply (frule new_tv_subst_tel, assumption)
+  apply (drule_tac a = "$s a" in new_tv_W, assumption)
+  apply (tactic "safe_tac HOL_cs")
+    apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
+   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
+  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
+  apply (drule new_tv_subst_tel, assumption)
+  apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
+  apply (drule new_tv_subst_tel, assumption)
+  apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
+  done
+
+lemma I_complete_wrt_W: "!!a m s.
+    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
+  apply (atomize (full))
+  apply (induct e)
+    apply (simp add: app_subst_list)
+   apply (simp (no_asm))
+   apply (intro strip)
+   apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
+    apply (tactic {* asm_simp_tac (HOL_ss addsimps
+      [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
+    apply (erule conjE)
+    apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
+    apply (simp (no_asm_simp))
+  apply (simp (no_asm_simp))
+  apply (intro strip)
+  apply (erule exE)+
+  apply (erule conjE)+
+  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
+   apply fast
+  apply (erule exE)
+  apply (erule conjE)
+  apply hypsubst
+  apply (simp (no_asm_simp))
+  apply (erule disjE)
+   apply (rule disjI1)
+   apply (simp (no_asm_use) add: o_def subst_comp_tel)
+   apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
+     erule_tac [2] asm_rl, erule_tac [2] asm_rl)
+   apply (rule conjI)
+    apply (fast intro: W_var_ge [THEN new_tv_list_le])
+   apply (rule new_tv_subst_comp_2)
+    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
+   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
+  apply (rule disjI2)
+  apply (erule exE)+
+  apply (erule conjE)
+  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
+   apply (rule conjI)
+   apply (fast intro: W_var_ge [THEN new_tv_list_le])
+   apply (rule new_tv_subst_comp_1)
+   apply (fast intro: W_var_ge [THEN new_tv_subst_le])
+   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
+  apply (erule exE)
+  apply (erule conjE)
+  apply hypsubst
+  apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
+  done
+
+end
diff -r 1db24da0537b -r fa6a3ddec27f src/HOL/W0/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/document/root.tex	Tue Feb 26 00:19:04 2002 +0100
@@ -0,0 +1,25 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+\newcommand{\isasymbind}{\textsf{bind}}
+
+\begin{document}
+
+\title{Type inference for let-free MiniML}
+\author{Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel}
+\maketitle
+
+\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}