# HG changeset patch
# User nipkow
# Date 853523404 -3600
# Node ID 477c055862862ea1b0f4e32679d7283c9c978ee2
# Parent  dd0f298b024cabf852eb0d4ea92bb0d05db087e4
The new version of MiniML including "let".

diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Generalize.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/Generalize.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -0,0 +1,138 @@
+(* Title:     HOL/MiniML/Generalize.ML
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+*)
+
+AddSEs [equalityE];
+
+goal thy "!!A B. free_tv A = free_tv B ==> gen A t = gen B t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "gen_eq_on_free_tv";
+
+goal thy "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
+by (typ.induct_tac "t" 1);
+by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "gen_without_effect";
+
+Addsimps [gen_without_effect];
+
+goal thy "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (case_tac "nat : free_tv ($ S A)" 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
+qed "free_tv_gen";
+
+Addsimps [free_tv_gen];
+
+goal thy "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "free_tv_gen_cons";
+
+Addsimps [free_tv_gen_cons];
+
+goal thy "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
+by (typ.induct_tac "t1" 1);
+by (Simp_tac 1);
+by (case_tac "nat : free_tv A" 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (Fast_tac 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
+qed "bound_tv_gen";
+
+Addsimps [bound_tv_gen];
+
+goal thy "!!A. new_tv n t --> new_tv n (gen A t)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (case_tac "nat : free_tv A" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "new_tv_compatible_gen";
+
+goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
+by (typ.induct_tac "t" 1);
+by (simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
+by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
+qed "gen_eq_gen_ML";
+
+goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
+\          --> gen ($ S A) ($ S t) = $ S (gen A t)";
+by (typ.induct_tac "t" 1);
+by (strip_tac 1);
+by (case_tac "nat:(free_tv A)" 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "nat ~: free_tv S" 1);
+by (Fast_tac 2);
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
+by (split_tac [expand_if] 1);
+by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
+by (Fast_tac 1);
+by (Asm_simp_tac 1);
+by (Best_tac 1);
+qed_spec_mp "gen_subst_commutes";
+
+goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
+by(typ.induct_tac "t" 1);
+by(ALLGOALS Asm_simp_tac);
+by(Fast_tac 1);
+qed_spec_mp "bound_typ_inst_gen";
+Addsimps [bound_typ_inst_gen];
+
+goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
+  "gen ($ S A) ($ S t) <= $ S (gen A t)";
+by(safe_tac (!claset));
+by(rename_tac "R" 1);
+by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
+by(typ.induct_tac "t" 1);
+ by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by(Asm_simp_tac 1);
+qed "gen_bound_typ_instance";
+
+goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
+  "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
+by(safe_tac (!claset));
+by(rename_tac "S" 1);
+by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
+by (typ.induct_tac "t" 1);
+ by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+ by(Fast_tac 1);
+by(Asm_simp_tac 1);
+qed "free_tv_subset_gen_le";
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] 
+      "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
+by (strip_tac 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (case_tac "nat : free_tv A" 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (subgoal_tac "n <= n + nat" 1);
+by (forw_inst_tac [("t","A")] new_tv_le 1);
+ba 1;
+by (dtac new_tv_not_free_tv 1);
+by (dtac new_tv_not_free_tv 1);
+by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
+by (simp_tac (!simpset addsimps [le_add1]) 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "gen_t_le_gen_alpha_t";
+
+Addsimps [gen_t_le_gen_alpha_t];
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Generalize.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/Generalize.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -0,0 +1,38 @@
+(* Title:     HOL/MiniML/Generalize.thy
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+
+Generalizing type schemes with respect to a context
+*)
+
+Generalize = Instance +
+
+
+(* gen: binding (generalising) the variables which are not free in the type scheme *)
+
+types ctxt = type_scheme list
+    
+consts
+  gen :: [ctxt, typ] => type_scheme
+
+primrec gen typ
+  "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
+  "gen A (t1 -> t2) = ((gen A t1) =-> (gen A t2))"
+
+(* executable version of gen: Implementation with free_tv_ML *)
+
+consts
+  gen_ML_aux :: [nat list, typ] => type_scheme
+
+primrec gen_ML_aux typ
+  "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
+  "gen_ML_aux A (t1 -> t2) = ((gen_ML_aux A t1) =-> (gen_ML_aux A t2))"
+
+consts
+  gen_ML :: [ctxt, typ] => type_scheme
+
+defs
+  gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
+
+end
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Instance.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/Instance.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -0,0 +1,289 @@
+(* Title:     HOL/MiniML/Instance.ML
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+*)
+
+(* lemmatas for instatiation *)
+
+
+(* lemmatas for bound_typ_inst *)
+
+goal thy "bound_typ_inst S (mk_scheme t) = t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "bound_typ_inst_mk_scheme";
+
+Addsimps [bound_typ_inst_mk_scheme];
+goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "bound_typ_inst_composed_subst";
+
+Addsimps [bound_typ_inst_composed_subst];
+
+goal thy "!!S. S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'";
+by (Asm_full_simp_tac 1);
+qed "bound_typ_inst_eq";
+
+
+(* lemmatas for bound_scheme_inst *)
+
+goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "bound_scheme_inst_mk_scheme";
+
+Addsimps [bound_scheme_inst_mk_scheme];
+
+goal thy "!!S. $S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "substitution_lemma";
+
+goal thy "!t. mk_scheme t = bound_scheme_inst B sch --> \
+\         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (safe_tac (!claset));
+by (rtac exI 1);
+by (rtac ballI 1);
+by (rtac sym 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (dtac mk_scheme_Fun 1);
+by (REPEAT (etac exE 1));
+by (etac conjE 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
+by (safe_tac (!claset));
+by (rename_tac "S1 S2" 1);
+by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
+by (safe_tac (!claset));
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (strip_tac 1);
+by (dres_inst_tac [("x","x")] bspec 1);
+ba 1;
+by (dres_inst_tac [("x","x")] bspec 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "bound_scheme_inst_type";
+
+
+(* lemmatas for subst_to_scheme *)
+
+goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
+\                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
+by (type_scheme.induct_tac "sch" 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "subst_to_scheme_inverse";
+
+goal thy "!!t t'. t = t' ==> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \
+\                            subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'";
+by (Fast_tac 1);
+val aux = result ();
+
+goal thy "new_tv n sch --> \
+\        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
+\                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
+by (Asm_simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
+val aux2 = result () RS mp;
+
+
+(* lemmata for <= *)
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance]
+      "!!(sch::type_scheme) sch'. (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
+by (rtac iffI 1);
+by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
+by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
+by (dtac make_one_new_out_of_two 1);
+ba 1;
+by (thin_tac "? n. new_tv n sch'" 1); 
+by (etac exE 1);
+by (etac allE 1);
+by (dtac mp 1);
+by (res_inst_tac [("x","(%k. TVar (k + n))")] exI 1);
+by (rtac refl 1);
+by (etac exE 1);
+by (REPEAT (etac conjE 1));
+by (dres_inst_tac [("n","n")] aux 1);
+by (asm_full_simp_tac (!simpset addsimps [subst_to_scheme_inverse]) 1);
+by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
+by (asm_simp_tac (!simpset addsimps [aux2]) 1);
+by (safe_tac (!claset));
+by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "le_type_scheme_def2";
+
+goalw thy [is_bound_typ_instance] "(mk_scheme t) <= sch = t <| sch";
+by (simp_tac (!simpset addsimps [le_type_scheme_def2]) 1); 
+by (rtac iffI 1); 
+by (etac exE 1); 
+by (forward_tac [bound_scheme_inst_type] 1);
+by (etac exE 1);
+by (rtac exI 1);
+by (rtac mk_scheme_injective 1); 
+by (Asm_full_simp_tac 1);
+by (rotate_tac 1 1);
+by (rtac mp 1);
+ba 2;
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac exE 1);
+by (Asm_full_simp_tac 1);
+by (rtac exI 1);
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "le_type_eq_is_bound_typ_instance";
+
+goalw thy [le_env_def]
+  "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
+by(Simp_tac 1);
+br iffI 1;
+ by(SELECT_GOAL(safe_tac (!claset))1);
+  by(eres_inst_tac [("x","0")] allE 1);
+  by(Asm_full_simp_tac 1);
+ by(eres_inst_tac [("x","Suc i")] allE 1);
+ by(Asm_full_simp_tac 1);
+br conjI 1;
+ by(Fast_tac 1);
+br allI 1;
+by(nat_ind_tac "i" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "le_env_Cons";
+AddIffs [le_env_Cons];
+
+goalw thy [is_bound_typ_instance]"!!t. t <| sch ==> $S t <| $S sch";
+by (etac exE 1);
+by (rename_tac "SA" 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("x","$S o SA")] exI 1);
+by (Simp_tac 1);
+qed "is_bound_typ_instance_closed_subst";
+
+goal thy "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch";
+by (asm_full_simp_tac (!simpset addsimps [le_type_scheme_def2]) 1);
+by (etac exE 1);
+by (asm_full_simp_tac (!simpset addsimps [substitution_lemma]) 1);
+by (Fast_tac 1);
+qed "S_compatible_le_scheme";
+
+goalw thy [le_env_def,app_subst_list] "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
+by (simp_tac (!simpset addcongs [conj_cong]) 1);
+by (fast_tac (!claset addSIs [S_compatible_le_scheme]) 1);
+qed "S_compatible_le_scheme_lists";
+
+goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
+by(Fast_tac 1);
+qed "bound_typ_instance_trans";
+
+goalw thy [le_type_scheme_def] "sch <= (sch::type_scheme)";
+by(Fast_tac 1);
+qed "le_type_scheme_refl";
+AddIffs [le_type_scheme_refl];
+
+goalw thy [le_env_def] "A <= (A::type_scheme list)";
+by(Fast_tac 1);
+qed "le_env_refl";
+AddIffs [le_env_refl];
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
+by(strip_tac 1);
+by(res_inst_tac [("x","%a.t")]exI 1);
+by(Simp_tac 1);
+qed "bound_typ_instance_BVar";
+AddIffs [bound_typ_instance_BVar];
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
+by(type_scheme.induct_tac "sch" 1);
+  by(Simp_tac 1);
+ by(Simp_tac 1);
+ by(SELECT_GOAL(safe_tac(!claset))1);
+ by(eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
+ by(Asm_full_simp_tac 1);
+ by(Fast_tac 1);
+by(Asm_full_simp_tac 1);
+br iffI 1;
+ by(eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
+ by(Asm_full_simp_tac 1);
+ by(Fast_tac 1);
+by(Fast_tac 1);
+qed "le_FVar";
+Addsimps [le_FVar];
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
+by(Simp_tac 1);
+qed "not_FVar_le_Fun";
+AddIffs [not_FVar_le_Fun];
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
+by(Simp_tac 1);
+by(res_inst_tac [("x","TVar n")] exI 1);
+by(Simp_tac 1);
+by(Fast_tac 1);
+qed "not_BVar_le_Fun";
+AddIffs [not_BVar_le_Fun];
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance]
+  "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
+by(fast_tac (!claset addss !simpset) 1);
+qed "Fun_le_FunD";
+
+goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
+by (type_scheme.induct_tac "sch'" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "scheme_le_Fun";
+
+goal thy "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
+by(type_scheme.induct_tac "sch" 1);
+  br allI 1;
+  by(type_scheme.induct_tac "sch'" 1);
+    by(Simp_tac 1);
+   by(Simp_tac 1);
+  by(Simp_tac 1);
+ br allI 1;
+ by(type_scheme.induct_tac "sch'" 1);
+   by(Simp_tac 1);
+  by(Simp_tac 1);
+ by(Simp_tac 1);
+br allI 1;
+by(type_scheme.induct_tac "sch'" 1);
+  by(Simp_tac 1);
+ by(Simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(strip_tac 1);
+bd Fun_le_FunD 1;
+by(Fast_tac 1);
+qed_spec_mp "le_type_scheme_free_tv";
+
+goal thy "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
+by(list.induct_tac "B" 1);
+ by(Simp_tac 1);
+br allI 1;
+by(list.induct_tac "A" 1);
+ by(simp_tac (!simpset addsimps [le_env_def]) 1);
+by(Simp_tac 1);
+by(fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
+qed_spec_mp "le_env_free_tv";
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Instance.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MiniML/Instance.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -0,0 +1,49 @@
+(* Title:     HOL/MiniML/Instance.thy
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+
+Instances of type schemes
+*)
+
+Instance = Type + 
+
+  
+(* generic instances of a type scheme *)
+
+consts
+  bound_typ_inst :: [subst, type_scheme] => typ
+
+primrec bound_typ_inst type_scheme
+  "bound_typ_inst S (FVar n) = (TVar n)"
+  "bound_typ_inst S (BVar n) = (S n)"
+  "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
+
+consts
+  bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
+
+primrec bound_scheme_inst type_scheme
+  "bound_scheme_inst S (FVar n) = (FVar n)"
+  "bound_scheme_inst S (BVar n) = (S n)"
+  "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
+  
+consts
+  "<|" :: [typ, type_scheme] => bool (infixr 70)
+defs
+  is_bound_typ_instance "t <| sch == ? S. t = (bound_typ_inst S sch)" 
+
+instance type_scheme :: ord
+defs le_type_scheme_def "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
+
+consts
+  subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
+
+primrec subst_to_scheme typ
+  "subst_to_scheme B (TVar n) = (B n)"
+  "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
+  
+instance list :: (ord)ord
+defs le_env_def
+  "A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)"
+
+end
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Maybe.ML
--- a/src/HOL/MiniML/Maybe.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Maybe.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -1,27 +1,31 @@
-open Maybe;
+(* Title:     HOL/MiniML/Maybe.ML
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+*)
 
-(* constructor laws for bind *)
-goalw thy [bind_def] "(Ok s) bind f = (f s)";
-by (Simp_tac 1);
-qed "bind_Ok";
-
-goalw thy [bind_def] "Fail bind f = Fail";
+(* constructor laws for option_bind *)
+goalw thy [option_bind_def] "option_bind (Some s) f = (f s)";
 by (Simp_tac 1);
-qed "bind_Fail";
+qed "option_bind_Some";
 
-Addsimps [bind_Ok,bind_Fail];
+goalw thy [option_bind_def] "option_bind None f = None";
+by (Simp_tac 1);
+qed "option_bind_None";
 
-(* expansion of bind *)
+Addsimps [option_bind_Some,option_bind_None];
+
+(* expansion of option_bind *)
 goal thy
-  "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
-by (maybe.induct_tac "res" 1);
+  "P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
+by (option.induct_tac "res" 1);
 by (fast_tac (HOL_cs addss !simpset) 1);
 by (Asm_simp_tac 1);
-qed "expand_bind";
+qed "expand_option_bind";
 
 goal Maybe.thy
-  "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
-qed "bind_eq_Fail";
+  "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
+by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+qed "option_bind_eq_None";
 
-Addsimps [bind_eq_Fail];
+Addsimps [option_bind_eq_None];
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Maybe.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -1,20 +1,18 @@
 (* Title:     HOL/MiniML/Maybe.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 Universal error monad.
 *)
 
-Maybe = List +
-
-datatype 'a maybe =  Ok 'a | Fail
+Maybe = Option + List +
 
 constdefs
-  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
-  "m bind f == case m of Ok r => f r | Fail => Fail"
+  option_bind :: ['a option, 'a => 'b option] => 'b option
+  "option_bind m f == case m of None => None | Some r => f r"
 
-syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "E bind (%P.F)"
+syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
+translations "P := E; F" == "option_bind E (%P.F)"
 
 end
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/MiniML.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -4,21 +4,246 @@
    Copyright  1995 TU Muenchen
 *)
 
-open MiniML;
-
 Addsimps has_type.intrs;
 Addsimps [Un_upper1,Un_upper2];
 
+Addsimps [is_bound_typ_instance_closed_subst];
+
+
+goal thy "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t";
+by (rtac typ_substitutions_only_on_free_variables 1);
+by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "s'_t_equals_s_t";
+
+Addsimps [s'_t_equals_s_t];
+
+goal thy "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A";
+by (rtac scheme_list_substitutions_only_on_free_variables 1);
+by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "s'_a_equals_s_a";
+
+Addsimps [s'_a_equals_s_a];
+
+goal thy "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ 
+\              $ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t) ==> \
+\             $S A |- e :: $S t";
+
+by (res_inst_tac [("P","%A. A |- e :: $S t")] ssubst 1);
+by (rtac (s'_a_equals_s_a RS sym) 1);
+by (res_inst_tac [("P","%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t")] ssubst 1);
+by (rtac (s'_t_equals_s_t RS sym) 1);
+by (Asm_full_simp_tac 1);
+qed "replace_s_by_s'";
+
+goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A";
+by (rtac scheme_list_substitutions_only_on_free_variables 1);
+by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1);
+qed "alpha_A'";
+
+goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A";
+by (rtac (alpha_A' RS ssubst) 1);
+by (Asm_full_simp_tac 1);
+qed "alpha_A";
+
+goal thy "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+qed "S_o_alpha_typ";
+
+goal thy "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+val S_o_alpha_typ' = result ();
+
+goal thy "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+qed "S_o_alpha_type_scheme";
+
+goal thy "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
+by (list.induct_tac "A" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
+qed "S_o_alpha_type_scheme_list";
+
+goal thy "!!A::type_scheme list. \
+\              ($ (%n. if n : free_tv A Un free_tv t \
+\                      then S n else TVar n) \
+\                 A) = \
+\              ($ ((%x. if x : free_tv A Un free_tv t then S x \
+\                       else TVar x) o \
+\                  (%x. if x : free_tv A \
+\                       then x else n + x)) A)";
+by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1);
+by (rtac (alpha_A RS ssubst) 1);
+by (rtac refl 1);
+qed "S'_A_eq_S'_alpha_A";
+
+goalw thy [free_tv_subst,dom_def]
+          "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\               free_tv A Un free_tv t";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (Fast_tac 1);
+qed "dom_S'";
+
+goalw thy [free_tv_subst,cod_def,subset_def]
+          "!!(A::type_scheme list) (t::typ). \ 
+\              cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\              free_tv ($ S A) Un free_tv ($ S t)";
+by (rtac ballI 1);
+by (etac UN_E 1);
+by (dtac (dom_S' RS subsetD) 1);
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
+                      addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
+qed "cod_S'";
+
+goalw thy [free_tv_subst]
+          "!!(A::type_scheme list) (t::typ). \
+\               free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\               free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
+by (fast_tac (!claset addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
+qed "free_tv_S'";
+
+goal thy "!!t1::typ. \
+\         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
+\         {x. ? y. x = n + y}";
+by (typ.induct_tac "t1" 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (Fast_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "free_tv_alpha";
+
+goal thy "!!(k::nat). n <= n + k";
+by (res_inst_tac [("n","k")] nat_induct 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+val aux_plus = result();
+
+Addsimps [aux_plus];
+
+goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
+by (step_tac (!claset) 1);
+by (cut_facts_tac [aux_plus] 1);
+by (dtac new_tv_le 1);
+ba 1;
+by (rotate_tac 1 1);
+by (dtac new_tv_not_free_tv 1);
+by (Fast_tac 1);
+val new_tv_Int_free_tv_empty_type = result ();
+
+goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
+by (step_tac (!claset) 1);
+by (cut_facts_tac [aux_plus] 1);
+by (dtac new_tv_le 1);
+ba 1;
+by (rotate_tac 1 1);
+by (dtac new_tv_not_free_tv 1);
+by (Fast_tac 1);
+val new_tv_Int_free_tv_empty_scheme = result ();
+
+goal thy "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
+by (rtac allI 1);
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
+val new_tv_Int_free_tv_empty_scheme_list = result ();
+
+goalw thy [le_type_scheme_def,is_bound_typ_instance] 
+      "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
+by (strip_tac 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (case_tac "nat : free_tv A" 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "n <= n + nat" 1);
+by (dtac new_tv_le 1);
+ba 1;
+by (dtac new_tv_not_free_tv 1);
+by (dtac new_tv_not_free_tv 1);
+by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "gen_t_le_gen_alpha_t";
+
+AddSIs has_type.intrs;
+
+goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
+by(etac has_type.induct 1);
+   by(simp_tac (!simpset addsimps [le_env_def]) 1);
+   by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
+  by(Asm_full_simp_tac 1);
+ by(Fast_tac 1);
+by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
+qed_spec_mp "has_type_le_env";
 
 (* has_type is closed w.r.t. substitution *)
-goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+goal thy "!!a. A |- e :: t ==> !S. $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);
+   by (rtac allI 1);
+   by (rtac has_type.VarI 1);
+    by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
+   by (asm_simp_tac (!simpset addsimps [app_subst_list]) 1);
+  (* case AbsI *)
+  by (rtac allI 1);
+  by (Simp_tac 1);  
+  by (rtac has_type.AbsI 1);
+  by (Asm_full_simp_tac 1);
+ (* case AppI *)
+ by (rtac allI 1);
+ by (rtac has_type.AppI 1);
+  by (Asm_full_simp_tac 1);
+  by (etac spec 1);
+ by (etac spec 1);
+(* case LetI *)
+by (rtac allI 1);
+by (rtac replace_s_by_s' 1);
+by (cut_inst_tac [("A","$ S A"), 
+                  ("A'","A"),
+                  ("t","t"),
+                  ("t'","$ S t")] 
+                 ex_fresh_variable 1);
+by (etac exE 1);
+by (REPEAT (etac conjE 1));
+by (res_inst_tac [("t1.0","$((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
+\                            (%x. if x : free_tv A then x else n + x)) t1")] 
+                 has_type.LETI 1);
+ by (dres_inst_tac [("x","(%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
+\                         (%x. if x : free_tv A then x else n + x)")] spec 1);
+ val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
+ (fn _ => [rtac refl 1]);
+ by (stac (S'_A_eq_S'_alpha_A) 1);
+ ba 1;
+by (stac S_o_alpha_typ 1);
+by (stac gen_subst_commutes 1);
+ by (rtac subset_antisym 1);
+  by (rtac subsetI 1);
+  by (etac IntE 1);
+  by (dtac (free_tv_S' RS subsetD) 1);
+  by (dtac (free_tv_alpha RS subsetD) 1);
+  by (Asm_full_simp_tac 1);
+  by (etac exE 1);
+  by (hyp_subst_tac 1);
+  by (subgoal_tac "new_tv (n + y) ($ S A)" 1);
+   by (subgoal_tac "new_tv (n + y) ($ S t)" 1);
+    by (subgoal_tac "new_tv (n + y) A" 1);
+     by (subgoal_tac "new_tv (n + y) t" 1);
+      by (REPEAT (dtac new_tv_not_free_tv 1));
+      by (Fast_tac 1);
+     by (REPEAT ((rtac new_tv_le 1) THEN (assume_tac 2) THEN (Simp_tac 1)));
+ by (Fast_tac 1);
+by (rtac has_type_le_env 1);
+ by (dtac spec 1);
+ by (dtac spec 1);
+ ba 1;
+by (rtac (app_subst_Cons RS subst) 1);
+by (rtac S_compatible_le_scheme_lists 1);
+by (Asm_simp_tac 1);
 qed "has_type_cl_sub";
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -1,32 +1,32 @@
 (* Title:     HOL/MiniML/MiniML.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 Mini_ML with type inference rules.
 *)
 
-MiniML = Type + 
+MiniML = Generalize + 
 
 (* expressions *)
 datatype
-        expr = Var nat | Abs expr | App expr expr
+        expr = Var nat | Abs expr | App expr expr | LET expr expr
 
 (* type inference rules *)
 consts
-        has_type :: "(typ list * expr * typ)set"
+        has_type :: "(ctxt * expr * typ)set"
 syntax
-        "@has_type" :: [typ list, expr, typ] => bool
+        "@has_type" :: [ctxt, expr, typ] => bool
                        ("((_) |-/ (_) :: (_))" [60,0,60] 60)
 translations 
-        "a |- e :: t" == "(a,e,t):has_type"
+        "A |- e :: t" == "(A,e,t):has_type"
 
 inductive has_type
 intrs
-        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
-        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
-        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
-              ==> a |- App e1 e2 :: t1"
+        VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t"
+        AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
+        AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
+              ==> A |- App e1 e2 :: t1"
+        LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
 
 end
-
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/ROOT.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -1,16 +1,13 @@
 (*  Title:      HOL/MiniML/ROOT.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Wolfgang Naraschewski and Tobias Nipkow
     Copyright   1995 TUM
 
-Type inference for let-free MiniML
+Type inference for MiniML
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/MiniML";
-Unify.trace_bound := 20;
 
-AddSEs [less_SucE];
-
-time_use_thy "I";
+time_use_thy "W";
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -1,37 +1,116 @@
-open Type;
+(* Title:     HOL/MiniML/Type.thy
+   ID:        $Id$
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
+*)
 
 Addsimps [mgu_eq,mgu_mg,mgu_free];
 
-(* mgu does not introduce new type variables *)
-goalw thy [new_tv_def] 
-      "!! n. [|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";
+
+(* lemmata for make scheme *)
+
+goal thy "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "mk_scheme_Fun";
 
-(* application of id_subst does not change type expression *)
-goalw thy [id_subst_def]
-  "$ id_subst = (%t::typ.t)";
-by (rtac ext 1);
+goal Type.thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
+by (typ.induct_tac "t" 1);
+ br allI 1;
+ by (typ.induct_tac "t'" 1);
+  by(Simp_tac 1);
+ by(Asm_full_simp_tac 1);
+br allI 1;
+by (typ.induct_tac "t'" 1);
+ by(Simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(Fast_tac 1);
+qed_spec_mp "mk_scheme_injective";
+
+goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "free_tv_mk_scheme";
+
+Addsimps [free_tv_mk_scheme];
+
+goal thy "!!t. $ S (mk_scheme t) = mk_scheme ($ S t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_te";
-Addsimps [app_subst_id_te];
+qed "subst_mk_scheme";
+
+Addsimps [subst_mk_scheme];
+
 
-(* application of id_subst does not change list of type expressions *)
+(* constructor laws for app_subst *)
+
+goalw thy [app_subst_list]
+  "$ S [] = []";
+by (Simp_tac 1);
+qed "app_subst_Nil";
+
 goalw thy [app_subst_list]
-  "$ id_subst = (%ts::typ list.ts)";
-by (rtac ext 1); 
-by (list.induct_tac "ts" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_tel";
-Addsimps [app_subst_id_tel];
+  "$ S (x#l) = ($ S x)#($ S l)";
+by (Simp_tac 1);
+qed "app_subst_Cons";
+
+Addsimps [app_subst_Nil,app_subst_Cons];
+
+
+(* constructor laws for new_tv *)
+
+goalw thy [new_tv_def]
+  "new_tv n (TVar m) = (m<n)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_TVar";
+
+goalw thy [new_tv_def]
+  "new_tv n (FVar m) = (m<n)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_FVar";
+
+goalw thy [new_tv_def]
+  "new_tv n (BVar m) = True";
+by (Simp_tac 1);
+qed "new_tv_BVar";
+
+goalw thy [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 Type.thy [id_subst_def,o_def] "$s o id_subst = s";
-by (rtac ext 1);
+goalw thy [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_Fun2";
+
+goalw thy [new_tv_def]
+  "new_tv n []";
 by (Simp_tac 1);
-qed "o_id_subst";
-Addsimps[o_id_subst];
+qed "new_tv_Nil";
+
+goalw thy [new_tv_def]
+  "new_tv n (x#l) = (new_tv n x & new_tv n l)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_Cons";
+
+goalw Type.thy [new_tv_def] "!!n. new_tv n TVar";
+by (strip_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
+qed "new_tv_TVar_subst";
+
+Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst];
+
+goalw Type.thy [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];
+
+
+(* constructor laws for dom and cod *)
 
 goalw thy [dom_def,id_subst_def,empty_def]
   "dom id_subst = {}";
@@ -45,14 +124,136 @@
 qed "cod_id_subst";
 Addsimps [cod_id_subst];
 
+
+(* lemmata for free_tv *)
+
 goalw thy [free_tv_subst]
   "free_tv id_subst = {}";
 by (Simp_tac 1);
 qed "free_tv_id_subst";
 Addsimps [free_tv_id_subst];
 
+goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","n")] nat_induct 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
+
+Addsimps [free_tv_nth_A_impl_free_tv_A];
+
+goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","nat")] nat_induct 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+qed_spec_mp "free_tv_nth_nat_A";
+
+
+(* 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 thy "!!S S'. (!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "typ_substitutions_only_on_free_variables";
+
+goal thy
+  "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
+by (rtac typ_substitutions_only_on_free_variables 1);
+by (simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "eq_free_eq_subst_te";
+
+goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "scheme_substitutions_only_on_free_variables";
+
+goal thy
+  "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
+by (rtac scheme_substitutions_only_on_free_variables 1);
+by (simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "eq_free_eq_subst_type_scheme";
+
+goal thy
+  "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
+by (list.induct_tac "A" 1); 
+(* case [] *)
+by (fast_tac (HOL_cs addss !simpset) 1);
+(* case x#xl *)
+by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (!simpset)) 1);
+qed_spec_mp "eq_free_eq_subst_scheme_list";
+
+goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
+by (Fast_tac 1);
+val weaken_asm_Un = result ();
+
+goal thy "!!S S'. (!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac weaken_asm_Un 1);
+by (strip_tac 1);
+by (etac scheme_substitutions_only_on_free_variables 1);
+qed_spec_mp "scheme_list_substitutions_only_on_free_variables";
+
+goal thy
+  "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
+by (typ.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 thy
+  "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
+by (type_scheme.induct_tac "sch" 1);
+(* case TVar n *)
+by (Asm_simp_tac 1);
+(* case BVar n *)
+by (strip_tac 1);
+by (etac mk_scheme_injective 1);
+by (Asm_simp_tac 1);
+(* case Fun t1 t2 *)
+by (Asm_full_simp_tac 1);
+qed_spec_mp "eq_subst_type_scheme_eq_free";
+
+goal thy
+  "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
+by (list.induct_tac "A" 1);
+(* case [] *)
+by (fast_tac (HOL_cs addss !simpset) 1);
+(* case x#xl *)
+by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (!simpset)) 1);
+qed_spec_mp "eq_subst_scheme_list_eq_free";
+
+goalw thy [free_tv_subst] 
+      "!!v. v : cod S ==> v : free_tv S";
+by( fast_tac set_cs 1);
+qed "codD";
+ 
+goalw thy [free_tv_subst,dom_def] 
+      "!! x. x ~: free_tv S ==> S x = TVar x";
+by( fast_tac set_cs 1);
+qed "not_free_impl_id";
+
+goalw thy [new_tv_def] 
+      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
+by( fast_tac HOL_cs 1 );
+qed "free_tv_le_new_tv";
+
 goalw thy [dom_def,cod_def,UNION_def,Bex_def]
-  "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
+  "!!v. [| 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);
@@ -61,286 +262,43 @@
 qed "cod_app_subst";
 Addsimps [cod_app_subst];
 
-
-(* composition of substitutions *)
-goal thy
-  "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
-by (typ.induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "subst_comp_te";
-
-goalw thy [app_subst_list]
-  "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
-by (list.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 thy [app_subst_list]
-  "$ s [] = []";
-by (Simp_tac 1);
-qed "app_subst_Nil";
-
-goalw thy [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 thy [new_tv_def]
-  "new_tv n (TVar m) = (m<n)";
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed "new_tv_TVar";
-
-goalw thy [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 thy [new_tv_def]
-  "new_tv n []";
-by (Simp_tac 1);
-qed "new_tv_Nil";
-
-goalw thy [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 Type.thy [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 thy [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 thy 
-  "new_tv n  = list_all (new_tv n)";
-by (rtac ext 1);
-by (list.induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "new_tv_list";
-
-(* substitution affects only variables occurring freely *)
-goal thy
-  "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
-by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed "subst_te_new_tv";
-Addsimps [subst_te_new_tv];
-
-goal thy
-  "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
-by (list.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 thy
-  "n<=m --> new_tv n (t::typ) --> new_tv m t";
-by (typ.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 thy 
-  "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by (list.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 thy
-  "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
-by (rtac conjI 1);
-by (slow_tac (HOL_cs addIs [le_trans]) 1);
-by (safe_tac HOL_cs );
-by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
-by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 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 thy
-  "!!n. [| 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 thy
-  "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
-by (typ.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 thy
-  "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 (list.induct_tac "ts" 1);
-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 thy
-  "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
-by (simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "new_tv_Suc_list";
-
-
-(* composition of substitutions preserves new_tv proposition *)
-goal thy 
-     "!! n. [| 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 thy
-     "!! n. [| 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 thy [new_tv_def] 
-      "!!n. 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 thy
-  "(t::typ) mem ts --> free_tv t <= free_tv ts";
-by (list.induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 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 thy
-  "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (typ.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 thy
-  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
-by (typ.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 thy
-  "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
-by (list.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 thy
-  "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
-by (list.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 thy [free_tv_subst] 
-      "!!v. v : cod s ==> v : free_tv s";
-by (fast_tac set_cs 1);
-qed "codD";
- 
-goalw thy [free_tv_subst,dom_def] 
-      "!! x. x ~: free_tv s ==> s x = TVar x";
-by (fast_tac set_cs 1);
-qed "not_free_impl_id";
-
-goalw thy [new_tv_def] 
-      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
-by (fast_tac HOL_cs 1 );
-qed "free_tv_le_new_tv";
-
-goal thy 
-     "free_tv (s (v::nat)) <= cod s Un {v}";
-by (cut_inst_tac [("P","v:dom s")] excluded_middle 1);
-by (safe_tac (HOL_cs addSIs [subsetI]) );
+     "free_tv (S (v::nat)) <= cod S Un {v}";
+by( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
+by( safe_tac (HOL_cs addSIs [subsetI]) );
 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 qed "free_tv_subst_var";
 
 goal thy 
-     "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by (typ.induct_tac "t" 1);
+     "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
+by( typ.induct_tac "t" 1);
 (* case TVar n *)
-by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
-by (fast_tac (set_cs addss !simpset) 1);
+by( fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_te";     
 
 goal thy 
-     "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by (list.induct_tac "ts" 1);
+     "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
+by( type_scheme.induct_tac "sch" 1);
+(* case FVar n *)
+by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+(* case BVar n *)
+by (Simp_tac 1);
+(* case Fun t1 t2 *)
+by (fast_tac (set_cs addss !simpset) 1);
+qed "free_tv_app_subst_type_scheme";  
+
+goal thy 
+     "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
+by( list.induct_tac "A" 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";
+by( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
+by( fast_tac (set_cs addss !simpset) 1);
+qed "free_tv_app_subst_scheme_list";
 
 goalw thy [free_tv_subst,dom_def]
      "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
@@ -351,3 +309,440 @@
 				     addsimps [cod_def,dom_def])) 1);
 qed "free_tv_comp_subst";
 
+goalw thy [o_def] 
+     "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)";
+by (rtac free_tv_comp_subst 1);
+qed "free_tv_o_subst";
+
+goal thy "!!n. n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_types";
+
+goal thy "!!n. n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
+
+goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists";
+
+Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
+
+goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (strip_tac 1);
+by (Fast_tac 1);
+qed "free_tv_ML_scheme";
+
+goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme]) 1);
+qed "free_tv_ML_scheme_list";
+
+
+(* lemmata for bound_tv *)
+
+goal thy "!!t. bound_tv (mk_scheme t) = {}";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "bound_tv_mk_scheme";
+
+Addsimps [bound_tv_mk_scheme];
+
+goal thy "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "bound_tv_subst_scheme";
+
+Addsimps [bound_tv_subst_scheme];
+
+goal thy "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
+by (rtac list.induct 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "bound_tv_subst_scheme_list";
+
+Addsimps [bound_tv_subst_scheme_list];
+
+
+(* lemmata for new_tv *)
+
+goalw thy [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 thy 
+  "new_tv n  = list_all (new_tv n)";
+by (rtac ext 1);
+by(list.induct_tac "x" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_tv_list";
+
+(* substitution affects only variables occurring freely *)
+goal thy
+  "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed "subst_te_new_tv";
+Addsimps [subst_te_new_tv];
+
+goal thy
+  "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed_spec_mp "subst_te_new_type_scheme";
+Addsimps [subst_te_new_type_scheme];
+
+goal thy
+  "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
+by (list.induct_tac "A" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "subst_tel_new_scheme_list";
+Addsimps [subst_tel_new_scheme_list];
+
+(* all greater variables are also new *)
+goalw thy [new_tv_def] 
+  "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
+by (safe_tac (!claset));
+by (dtac spec 1);
+by (mp_tac 1);
+by (trans_tac 1);
+qed "new_tv_le";
+Addsimps [lessI RS less_imp_le RS new_tv_le];
+
+goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_tv_typ_le";
+
+goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_scheme_list_le";
+
+goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_tv_subst_le";
+
+(* new_tv property remains if a substitution is applied *)
+goal thy
+  "!!n. [| 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 thy
+  "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
+by (typ.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 thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+by (rewrite_goals_tac [new_tv_def]);
+by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
+by (strip_tac 1);
+by (case_tac "S nat = TVar nat" 1);
+by (rotate_tac 3 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","m")] spec 1);
+by (Fast_tac 1);
+qed_spec_mp "new_tv_subst_type_scheme";
+Addsimps [new_tv_subst_type_scheme];
+
+goal thy
+  "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
+by (list.induct_tac "A" 1);
+by (ALLGOALS(fast_tac (HOL_cs addss (!simpset))));
+qed_spec_mp "new_tv_subst_scheme_list";
+Addsimps [new_tv_subst_scheme_list];
+
+goal thy
+  "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
+by( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (list.induct_tac "A" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "new_tv_Suc_list";
+
+goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
+by (Asm_simp_tac 1);
+qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme";
+
+goalw thy [new_tv_def] "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')";
+by (Asm_simp_tac 1);
+qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
+
+goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","nat")] nat_induct 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+qed_spec_mp "new_tv_nth_nat_A";
+
+
+(* composition of substitutions preserves new_tv proposition *)
+goal thy 
+     "!! n. [| 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 thy
+     "!! n. [| 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 thy [new_tv_def] 
+      "!!n. new_tv n A ==> n~:(free_tv A)";
+by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
+qed "new_tv_not_free_tv";
+Addsimps [new_tv_not_free_tv];
+
+goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (safe_tac (!claset));
+by (trans_tac 1);
+qed "less_maxL";
+
+goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
+qed "less_maxR";
+
+goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
+by (typ.induct_tac "t" 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Asm_simp_tac 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","max n n'")] exI 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1);
+qed "fresh_variable_types";
+
+Addsimps [fresh_variable_types];
+
+goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Simp_tac 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Simp_tac 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","max n n'")] exI 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1);
+qed "fresh_variable_type_schemes";
+
+Addsimps [fresh_variable_type_schemes];
+
+goalw thy [max_def] "!!n::nat. n <= (max n n')";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed "le_maxL";
+
+goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
+qed "le_maxR";
+
+goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (etac exE 1);
+by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1);
+by (etac exE 1);
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","(max n n')")] exI 1);
+by (subgoal_tac "n <= (max n n')" 1);
+by (subgoal_tac "n' <= (max n n')" 1);
+by (fast_tac (!claset addDs [new_tv_le]) 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [le_maxR,le_maxL])));
+qed "fresh_variable_type_scheme_lists";
+
+Addsimps [fresh_variable_type_scheme_lists];
+
+goal thy "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
+by (REPEAT (etac exE 1));
+by (rename_tac "n1 n2" 1);
+by (res_inst_tac [("x","(max n1 n2)")] exI 1);
+by (subgoal_tac "n1 <= max n1 n2" 1);
+by (subgoal_tac "n2 <= max n1 n2" 1);
+by (fast_tac (!claset addDs [new_tv_le]) 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [le_maxL,le_maxR])));
+qed "make_one_new_out_of_two";
+
+goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
+\         ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ;
+by (cut_inst_tac [("t","t")] fresh_variable_types 1);
+by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
+by (dtac make_one_new_out_of_two 1);
+ba 1;
+by (thin_tac "? n. new_tv n t'" 1);
+by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
+by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
+by (rotate_tac 1 1);
+by (dtac make_one_new_out_of_two 1);
+ba 1;
+by (thin_tac "? n. new_tv n A'" 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n2 n1" 1);
+by (res_inst_tac [("x","(max n1 n2)")] exI 1);
+by (rewrite_goals_tac [new_tv_def]);
+by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1);
+qed "ex_fresh_variable";
+
+(* mgu does not introduce new type variables *)
+goalw thy [new_tv_def] 
+      "!! n. [|mgu t1 t2 = Some 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";
+
+
+(* lemmata for substitutions *)
+
+goalw Type.thy [app_subst_list] "length ($ S A) = length A";
+by(Simp_tac 1);
+qed "length_app_subst_list";
+Addsimps [length_app_subst_list];
+
+goal thy "!!sch::type_scheme. $ TVar sch = sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "subst_TVar_scheme";
+
+Addsimps [subst_TVar_scheme];
+
+goal thy "!!A::type_scheme list. $ TVar A = A";
+by (rtac list.induct 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [app_subst_list])));
+qed "subst_TVar_scheme_list";
+
+Addsimps [subst_TVar_scheme_list];
+
+(* application of id_subst does not change type expression *)
+goalw thy [id_subst_def]
+  "$ id_subst = (%t::typ.t)";
+by (rtac ext 1);
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_te";
+Addsimps [app_subst_id_te];
+
+goalw thy [id_subst_def]
+  "$ id_subst = (%sch::type_scheme.sch)";
+by (rtac ext 1);
+by (type_scheme.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_type_scheme";
+Addsimps [app_subst_id_type_scheme];
+
+(* application of id_subst does not change list of type expressions *)
+goalw thy [app_subst_list]
+  "$ id_subst = (%A::type_scheme list.A)";
+by (rtac ext 1); 
+by (list.induct_tac "A" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_tel";
+Addsimps [app_subst_id_tel];
+
+goal thy "!!sch::type_scheme. $ id_subst sch = sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [id_subst_def])));
+qed "id_subst_sch";
+
+Addsimps [id_subst_sch];
+
+goal thy "!!A::type_scheme list. $ id_subst A = A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed "id_subst_A";
+
+Addsimps [id_subst_A];
+
+(* composition of substitutions *)
+goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
+br ext 1;
+by(Simp_tac 1);
+qed "o_id_subst";
+Addsimps[o_id_subst];
+
+goal thy
+  "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "subst_comp_te";
+
+goal thy
+  "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "subst_comp_type_scheme";
+
+goalw thy [app_subst_list]
+  "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
+by (list.induct_tac "A" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (asm_full_simp_tac (!simpset addsimps [subst_comp_type_scheme]) 1);
+qed "subst_comp_scheme_list";
+
+goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A";
+by (rtac scheme_list_substitutions_only_on_free_variables 1);
+by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1);
+qed "subst_id_on_type_scheme_list'";
+
+goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
+by (stac subst_id_on_type_scheme_list' 1);
+ba 1;
+by (Simp_tac 1);
+qed "subst_id_on_type_scheme_list";
+
+goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (rename_tac "n1" 1);
+by (res_inst_tac[("n","n1")] nat_induct 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "nth_subst";
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Type.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -1,7 +1,7 @@
 (* Title:     HOL/MiniML/Type.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 MiniML-types and type substitutions.
 *)
@@ -9,24 +9,105 @@
 Type = Maybe + 
 
 (* new class for structures containing type variables *)
-classes
-        type_struct < term 
+axclass  type_struct < term 
+
 
 (* type expressions *)
 datatype
         typ = TVar nat | "->" typ typ (infixr 70)
 
-(* type variable substitution *)
+(* type schemata *)
+datatype
+        type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
+
+
+(* embedding types into type schemata *)    
+consts
+  mk_scheme :: typ => type_scheme
+
+primrec mk_scheme typ
+  "mk_scheme (TVar n) = (FVar n)"
+  "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
+
+
+instance  typ::type_struct
+instance  type_scheme::type_struct  
+instance  list::(type_struct)type_struct
+instance  fun::(term,type_struct)type_struct
+
+
+(* free_tv s: the type variables occuring freely in the type structure s *)
+
+consts
+  free_tv :: ['a::type_struct] => nat set
+
+primrec free_tv typ
+  free_tv_TVar    "free_tv (TVar m) = {m}"
+  free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+
+primrec free_tv type_scheme
+  "free_tv (FVar m) = {m}"
+  "free_tv (BVar m) = {}"
+  "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
+
+primrec free_tv list
+  "free_tv [] = {}"
+  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+
+(* executable version of free_tv: Implementation with lists *)
+consts
+  free_tv_ML :: ['a::type_struct] => nat list
+
+primrec free_tv_ML type_scheme
+  "free_tv_ML (FVar m) = [m]"
+  "free_tv_ML (BVar m) = []"
+  "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
+
+primrec free_tv_ML list
+  "free_tv_ML [] = []"
+  "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
+
+  
+(* 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"
+
+  
+(* bound_tv s: the type variables occuring bound in the type structure s *)
+
+consts
+  bound_tv :: ['a::type_struct] => nat set
+
+primrec bound_tv type_scheme
+  "bound_tv (FVar m) = {}"
+  "bound_tv (BVar m) = {m}"
+  "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
+
+primrec bound_tv list
+  "bound_tv [] = {}"
+  "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
+
+
+(* minimal new free / bound variable *)
+
+consts
+  min_new_bound_tv :: 'a::type_struct => nat
+
+primrec min_new_bound_tv type_scheme
+  "min_new_bound_tv (FVar n) = 0"
+  "min_new_bound_tv (BVar n) = Suc n"
+  "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
+
+
+(* substitutions *)
+
+(* type variable substitution *) 
 types
         subst = nat => typ
 
-arities
-        typ::type_struct
-        list::(type_struct)type_struct
-        fun::(term,type_struct)type_struct
-
-(* substitutions *)
-
 (* identity *)
 constdefs
         id_subst :: subst
@@ -34,56 +115,44 @@
 
 (* extension of substitution to type structures *)
 consts
-        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
+  app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-primrec app_subst typ
-  app_subst_TVar  "$ s (TVar n) = s n" 
-  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+primrec app_subst typ 
+  app_subst_TVar "$ S (TVar n) = S n" 
+  app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
+
+primrec app_subst type_scheme
+  "$ S (FVar n) = mk_scheme (S n)"
+  "$ S (BVar n) = (BVar n)"
+  "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
 
 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 typ
-  "free_tv (TVar m) = {m}"
-  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-
-primrec free_tv List.list
-  "free_tv [] = {}"
-  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+  app_subst_list "$ S == map ($ S)"
 
 (* domain of a substitution *)
 constdefs
         dom :: subst => nat set
-        "dom s == {n. s n ~= TVar n}" 
+        "dom S == {n. S n ~= TVar n}" 
 
-(* codomain of a substitutions: the introduced variables *)
+(* codomain of a substitution: the introduced variables *)
+
 constdefs
         cod :: subst => nat set
-        "cod s == (UN m:dom s. free_tv (s m))"
+        "cod S == (UN m:dom S. (free_tv (S m)))"
 
 defs
-        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
+        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
+        mgu :: [typ,typ] => subst option
 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"
+        mgu_eq   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
+        mgu_mg   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
+                  ? R. S = $R o U"
+        mgu_Some   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
+        mgu_free "mgu t1 t2 = Some U ==>   \
+\		  (free_tv U) <= (free_tv t1) Un (free_tv t2)"
 
 end
-
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -8,204 +8,296 @@
 
 open W;
 
-Addsimps [Suc_le_lessD];
-Delsimps (ex_simps @ all_simps);
-
-(* correctness of W with respect to has_type *)
-goal W.thy
-        "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
-by (expr.induct_tac "e" 1);
-(* case Var n *)
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-(* case Abs e *)
-by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
-                        setloop (split_tac [expand_bind])) 1);
-by (strip_tac 1);
-by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
-by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
-(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_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]) 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";
+Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
-        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
-
+        [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
 
 (* the resulting type variable is always greater or equal than the given one *)
 goal thy
-        "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
+        "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (etac conjE 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (Asm_full_simp_tac 1);
 (* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
-by (eres_inst_tac [("x","a")] allE 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 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","$ 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 (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 by (etac conjE 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 (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
 by (etac conjE 1);
-by (res_inst_tac [("j","na")] le_trans 1); 
+by (res_inst_tac [("j","n1")] le_trans 1); 
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
+(* case LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
+by (REPEAT (etac conjE 1));
+by (REPEAT (etac allE 1));
+by (mp_tac 1);
+by (mp_tac 1);
+by (best_tac (!claset addEs [le_trans]) 1);
 qed_spec_mp "W_var_ge";
 
 Addsimps [W_var_ge];
 
 goal thy
-        "!! s. Ok (s,t,m) = W e a n ==> n<=m";
+        "!! s. Some (S,t,m) = W e A n ==> n<=m";
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 qed "W_var_geD";
 
+goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
+by (dtac W_var_geD 1);
+by (rtac new_scheme_list_le 1);
+ba 1;
+ba 1;
+qed "new_tv_compatible_W";
 
 (* auxiliary lemma *)
-goal Maybe.thy "(y = Ok x) = (Ok x = y)";
-by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-qed "rotate_Ok";
+goal Maybe.thy "(y = Some x) = (Some x = y)";
+by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "rotate_Some";
 
+goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac conjE 1);
+by (rtac conjI 1);
+by (rtac new_tv_le 1);
+by (mp_tac 2);
+by (mp_tac 2);
+ba 2;
+by (rtac add_le_mono 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (strip_tac 1);
+by (rtac new_tv_le 1);
+by (mp_tac 2);
+by (mp_tac 2);
+ba 2;
+by (rtac add_le_mono 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (strip_tac 1);
+by (dtac not_leE 1);
+by (rtac less_or_eq_imp_le 1);
+by (Fast_tac 1);
+qed_spec_mp "new_tv_bound_typ_inst_sch";
+
+Addsimps [new_tv_bound_typ_inst_sch];
 
 (* resulting type variable is new *)
 goal thy
-     "!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";
+     "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
+\                 new_tv m S & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addss (!simpset 
-        addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
-        setloop (split_tac [expand_if]))) 1);
-
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+by (rtac conjI 1);
+by (dtac sym 1);
+by (Asm_full_simp_tac 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac new_tv_nth_nat_A 1);
+ba 1;
+by (Asm_full_simp_tac 1);
 (* case Abs e *)
 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
-    setloop (split_tac [expand_bind])) 1);
+    setloop (split_tac [expand_option_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 (eres_inst_tac [("x","(FVar 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 setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 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","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 (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
+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( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 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 (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
+by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 
+by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 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])
+     [new_scheme_list_le,new_tv_subst_scheme_list,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 (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
+   new_tv_subst_scheme_list,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_scheme_list_le,new_tv_subst_scheme_list,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);
+   addDs [W_var_geD] addIs
+   [new_scheme_list_le,new_tv_subst_scheme_list,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_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
+     addss (!simpset)) 1);
+(* case LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
+by (REPEAT (etac conjE 1));
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (rotate_tac 1 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac conjE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
+by (dtac sym 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (eres_inst_tac [("x","gen ($ S1 A) t1 # $ S1 A")] allE 1);
+by (eres_inst_tac [("x","S2")] allE 1);
+by (eres_inst_tac [("x","t2")] allE 1);
+by (eres_inst_tac [("x","m2")] allE 1);
+by (subgoal_tac "new_tv n2 (gen ($ S1 A) t1 # $ S1 A)" 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac conjE 1);
+by (rtac conjI 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (rtac new_tv_subst_comp_2 1);
+by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
+by (etac W_var_ge 1);
+ba 1;
+ba 1;
+ba 1;
+by (rewrite_goals_tac [new_tv_def]);
+by (Asm_simp_tac 1);
+by (dtac W_var_ge 1);
+by (rtac allI 1);
+by (rename_tac "p" 1);
+by (strip_tac 1);
+by (rewrite_goals_tac [free_tv_subst]);
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
+fun restrict_prems is tacf =
+  METAHYPS(fn prems =>
+    let val iprems = map (fn i => nth_elem(i,prems)) is
+    in cut_facts_tac iprems 1 THEN tacf 1 end);
+by (restrict_prems [0,4,8,9] (best_tac (!claset addEs [less_le_trans])) 1);
 qed_spec_mp "new_tv_W";
 
+goal thy "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
+by (type_scheme.induct_tac "sch" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (rtac exI 1);
+by (rtac refl 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "free_tv_bound_typ_inst1";
+
+Addsimps [free_tv_bound_typ_inst1];
 
 goal thy
-     "!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";
+     "!n A S t m v. W e A n = Some (S,t,m) -->            \
+\         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
-    addss (!simpset setloop (split_tac [expand_if]))) 1);
-
+by (simp_tac (!simpset addsimps
+    [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1);
+by (case_tac "v : free_tv (nth nat A)" 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (dtac free_tv_bound_typ_inst1 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (rotate_tac 3 1);
+by (etac exE 1);
+by (rotate_tac 3 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (dtac add_lessD1 1);
+by (fast_tac (!claset addIs [less_irrefl]) 1);
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps
-    [free_tv_subst] setloop (split_tac [expand_bind])) 1);
+    [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta m v" 1);
+by (rename_tac "S t n1 S1 t1 m 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","FVar 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","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-by (fast_tac (HOL_cs addSEs [allE]
-	             addIs [cod_app_subst]
+by (best_tac (HOL_cs addIs [cod_app_subst]
                      addss (!simpset addsimps [less_Suc_eq])) 1);
-(** LEVEL 12 **)
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
 by (strip_tac 1); 
-by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m 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","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 (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-(** LEVEL 22 **)
 (* second case *)
-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 (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 (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1);
 by (dtac W_var_geD 1);
 by (dtac W_var_geD 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
-(** LEVEL 32 **)
 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,
+    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
     less_le_trans,less_not_refl2,subsetD]
   addEs [UnE] 
   addss !simpset) 1);
@@ -214,54 +306,224 @@
 by (dtac (sym RS W_var_geD) 1);
 by ( (forward_tac [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) 1); 
+    free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
+    less_le_trans,subsetD]
+  addEs [UnE]
+  addss !simpset) 1);
+(* LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (strip_tac 1); 
+by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
+by (eres_inst_tac [("x","nat")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (rotate_tac 1 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (rotate_tac 4 1);
+by (eres_inst_tac [("x","v")] allE 1);
+by (mp_tac 1);
+by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
+by (mp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
+              addDs [less_le_trans]) 1);
+by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
+              addDs [less_le_trans]) 1);
 qed_spec_mp "free_tv_W"; 
 
+goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
+by (Fast_tac 1);
+qed "weaken_A_Int_B_eq_empty";
+
+goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
+by (Fast_tac 1);
+qed "weaken_not_elem_A_minus_B";
+
+(* correctness of W with respect to has_type *)
+goal W.thy
+        "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
+by (expr.induct_tac "e" 1);
+(* case Var n *)
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (strip_tac 1);
+by (rtac has_type.VarI 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
+by (rtac exI 1);
+by (rtac refl 1);
+(* case Abs e *)
+by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
+                        setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
+by (Asm_full_simp_tac 1);
+by (rtac has_type.AbsI 1);
+by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
+bd sym 1;
+by (REPEAT (etac allE 1));
+by (etac impE 1);
+by (mp_tac 2);
+by (Asm_simp_tac 1);
+ba 1;
+(* case App e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
+by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
+by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
+by (rtac (app_subst_Fun RS subst) 1);
+by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
+by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
+by (rtac (has_type_cl_sub RS spec) 1);
+by (forward_tac [new_tv_W] 1);
+ba 1;
+by (dtac conjunct1 1);
+by (dtac conjunct1 1);
+by (forward_tac [new_tv_subst_scheme_list] 1);
+by (rtac new_scheme_list_le 1);
+by (rtac W_var_ge 1);
+ba 1;
+ba 1;
+by (etac thin_rl 1);
+by (REPEAT (etac allE 1));
+bd sym 1;
+bd sym 1;
+by (etac thin_rl 1);
+by (etac thin_rl 1);
+by (mp_tac 1);
+by (mp_tac 1);
+ba 1;
+(* case Let e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
+by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by (rtac (has_type_cl_sub RS spec) 1);
+by (dres_inst_tac [("x","A")] spec 1);
+by (dres_inst_tac [("x","S1")] spec 1);
+by (dres_inst_tac [("x","t1")] spec 1);
+by (dres_inst_tac [("x","m2")] spec 1);
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x","m1")] spec 1);
+by (mp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by (rtac (gen_subst_commutes RS sym RS subst) 1);
+by (rtac (app_subst_Cons RS subst) 2);
+by (etac thin_rl 2);
+by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
+by (dres_inst_tac [("x","S2")] spec 2);
+by (dres_inst_tac [("x","t")] spec 2);
+by (dres_inst_tac [("x","n2")] spec 2);
+by (dres_inst_tac [("x","m2")] spec 2);
+by (forward_tac [new_tv_W] 2);
+ba 2;
+by (dtac conjunct1 2);
+by (dtac conjunct1 2);
+by (forward_tac [new_tv_subst_scheme_list] 2);
+by (rtac new_scheme_list_le 2);
+by (rtac W_var_ge 2);
+ba 2;
+ba 2;
+by (etac impE 2);
+by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
+by (Simp_tac 2);
+by (Fast_tac 2);
+ba 2;
+by (Asm_full_simp_tac 2);
+by (rtac weaken_A_Int_B_eq_empty 1);
+by (rtac allI 1);
+by (strip_tac 1);
+by (rtac weaken_not_elem_A_minus_B 1);
+by (case_tac "x < m2" 1);
+by (rtac disjI2 1);
+by (rtac (free_tv_gen_cons RS subst) 1);
+by (rtac free_tv_W 1);
+ba 1;
+by (Asm_full_simp_tac 1);
+ba 1;
+by (rtac disjI1 1);
+by (dtac new_tv_W 1);
+ba 1;
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (rtac new_tv_not_free_tv 1);
+by (rtac new_tv_le 1);
+ba 2;
+by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
+qed_spec_mp "W_correct_lemma";
+
+goal Type.thy "new_tv n (sch::type_scheme) --> \
+\              $(%k.if k<n then S k else S' k) sch = $S sch";
+by (type_scheme.induct_tac "sch" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme";
+Addsimps [new_if_subst_type_scheme];
+
+goal Type.thy "new_tv n (A::type_scheme list) --> \
+\              $(%k.if k<n then S k else S' k) A = $S A";
+by (list.induct_tac "A" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme_list";
+Addsimps [new_if_subst_type_scheme_list];
+
+goal Arith.thy "!!n::nat. ~ k+n < n";
+by (nat_ind_tac "k" 1);
+by(ALLGOALS Asm_simp_tac);
+by(trans_tac 1);
+qed "not_add_less1";
+Addsimps [not_add_less1];
 
 (* Completeness of W w.r.t. has_type *)
 goal thy
- "!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))";
+ "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
+\             (? S t. (? m. W e A n = Some (S,t,m)) &  \
+\                     (? R. $S' A = $R ($S A) & t' = $R t))";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
 by (simp_tac (!simpset addcongs [conj_cong] 
-              setloop (split_tac [expand_if])) 1);
+    setloop (split_tac [expand_if])) 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","id_subst")] exI 1);
-by (res_inst_tac [("x","nth nat a")] exI 1);
-by (Simp_tac 1);
-by (res_inst_tac [("x","s'")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (rename_tac "S" 1);
+by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
+by (rtac conjI 1);
 by (Asm_simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
+                           delsimps [bound_typ_inst_composed_subst]) 1);
 
-(** LEVEL 10 **)
 (* 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","%x.if x=n then t1 else (S' x)")] allE 1);
+by (eres_inst_tac [("x","(FVar 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]
-                            setloop (split_tac [expand_bind]))) 1);
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong] 
+    setloop (split_tac [expand_option_bind]))) 1);
 
-(** LEVEL 17 **)
 (* 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","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","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 (dtac asm_rl 1);
@@ -271,119 +533,140 @@
 by (safe_tac HOL_cs);
 by (fast_tac HOL_cs 1);
 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);
+        conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
 
-(** LEVEL 35 **)
 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);
+  "$ (%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);
+\   (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 42 **)
-by (case_tac "na:free_tv sa" 2);
-(* na ~: free_tv sa *)
-by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
-                  setloop (split_tac [expand_if])) 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);
+    new_tv_not_free_tv,new_tv_le]) 3);
+by (case_tac "na:free_tv Sa" 2);
+(* n1 ~: free_tv S1 *)
+by (forward_tac [not_free_impl_id] 3);
+by (asm_simp_tac (!simpset 
+    setloop (split_tac [expand_if])) 3);
+(* na : free_tv Sa *)
+by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
+by (dtac eq_subst_scheme_list_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 *)
+by (case_tac "na:dom Sa" 2);
+(* na ~: dom Sa *)
 by (asm_full_simp_tac (!simpset addsimps [dom_def] 
-                       setloop (split_tac [expand_if])) 3);
-(** LEVEL 50 **)
-(* na : dom sa *)
+    setloop (split_tac [expand_if])) 3);
+(* na : dom Sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
 by (subgoal_tac "nb ~= ma" 2);
 by ((forward_tac [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 (dtac new_tv_subst_scheme_list 3);
+by (fast_tac (HOL_cs addIs [new_scheme_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);
+    (!simpset addsimps [cod_def,free_tv_subst])) 3);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
-                            setloop (split_tac [expand_if]))) 2);
-
+    setloop (split_tac [expand_if]))) 2);
 by (Simp_tac 2);  
-(** LEVEL 60 **)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
 by (subgoal_tac "na ~= ma" 2);
 by ((forward_tac [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 68 **)
-(* case na ~: free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
-(* case na : free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 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 addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
+by (case_tac "na: free_tv t - free_tv Sa" 2);
+(* case na ~: free_tv t - free_tv Sa *)
+by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+(* case na : free_tv t - free_tv Sa *)
+by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
+by (dtac eq_subst_scheme_list_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,de_Morgan_disj]) 2);
-(** LEVEL 74 **)
-by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
+
+by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
 by (safe_tac HOL_cs );
-by (dtac mgu_Ok 1);
-by ( fast_tac (HOL_cs addss !simpset) 1);
-by (REPEAT (resolve_tac [exI,conjI] 1));
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (dtac mgu_Some 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 (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 [subst_comp_tel RS sym]) 1);
-by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
+by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
+by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
+by (res_inst_tac [("A2","($ Sa ($ S A))")] ((subst_comp_scheme_list RS sym) RSN 
     (2,trans)) 1);
-by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
-(** LEVEL 90 **)
-by (rtac eq_free_eq_subst_tel 1);
-by ( safe_tac HOL_cs );
+by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+by (rtac eq_free_eq_subst_scheme_list 1);
+by( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
 by ((forward_tac [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 (dtac new_tv_subst_scheme_list 2);
+by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
 by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
 by (etac conjE 2);
-by (dtac (free_tv_app_subst_tel RS subsetD) 2);
-(** LEVEL 100 **)
-by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
+by (fast_tac (set_cs addDs [W_var_geD,new_scheme_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 (case_tac "na: free_tv t - free_tv Sa" 1);
+(* case na ~: free_tv t - free_tv Sa *)
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
-(* case na : free_tv t - free_tv sa *)
+(* case na : free_tv t - free_tv Sa *)
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 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 [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
-(** LEVEL 106 **)
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
+by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
+    eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 
+    [free_tv_subst,dom_def]))) 1);
 by (Fast_tac 1);
+(* case Let e1 e2 *)
+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","t1")] allE 1);
+by (eres_inst_tac [("x","n")] allE 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (safe_tac HOL_cs);
+by (Asm_simp_tac 1); 
+by (eres_inst_tac [("x","R")] allE 1);
+by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
+by (eres_inst_tac [("x","t'")] allE 1);
+by (eres_inst_tac [("x","m")] allE 1);
+by (rotate_tac 4 1);
+by (Asm_full_simp_tac 1);
+by (dtac mp 1);
+by (rtac has_type_le_env 1);
+ba 1;
+by (Simp_tac 1);
+by (rtac gen_bound_typ_instance 1);
+by (dtac mp 1);
+by (forward_tac [new_tv_compatible_W] 1);
+by (rtac sym 1);
+ba 1;
+by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
+by (safe_tac HOL_cs);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","Ra")] exI 1);
+by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
 qed_spec_mp "W_complete_lemma";
 
 goal W.thy
- "!!e. [] |- 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'")]
+ "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(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);
+by(ALLGOALS Asm_full_simp_tac);
 qed "W_complete";
diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/W.thy	Fri Jan 17 18:50:04 1997 +0100
@@ -1,28 +1,38 @@
 (* Title:     HOL/MiniML/W.thy
    ID:        $Id$
-   Author:    Dieter Nazareth and Tobias Nipkow
-   Copyright  1995 TU Muenchen
+   Author:    Wolfgang Naraschewski and Tobias Nipkow
+   Copyright  1996 TU Muenchen
 
 Type inference algorithm W
 *)
 
+
 W = MiniML + 
 
 types 
-        result_W = "(subst * typ * nat)maybe"
+        result_W = "(subst * typ * nat)option"
 
 (* type inference algorithm W *)
+
 consts
-        W :: [expr, typ list, nat] => result_W
+        W :: [expr, ctxt, nat] => result_W
 
 primrec W expr
-  "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, 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) )"
+  "W (Var i) A n =  
+     (if i < length A then Some( id_subst,   
+	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
+	                         n + (min_new_bound_tv (nth i A)) )  
+	              else None)"
+  
+  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
+                     Some( 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));
+                         Some( $U o $S2 o S1, U m2, Suc m2) )"
+  
+  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
+                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
+                         Some( $S2 o S1, t2, m2) )"
 end