# HG changeset patch
# User nipkow
# Date 853503714 -3600
# Node ID bee082efaa4608e8260a1f6444d150649da72da5
# Parent 2af078382853c4e4188a7fe177530affb077553d
This is the old version og MiniML for the monomorphic case.
The new version is now in MiniML.
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/I.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/I.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,206 @@
+open I;
+
+goal thy
+ "! a m s s' t n. \
+\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \
+\ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
+by (expr.induct_tac "e" 1);
+
+ (* case Var n *)
+ by (simp_tac (!simpset addsimps [app_subst_list]
+ setloop (split_inside_tac [expand_if])) 1);
+
+ (* case Abs e *)
+ by (asm_full_simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);
+ by (strip_tac 1);
+ by (rtac conjI 1);
+ by (strip_tac 1);
+ by (REPEAT (etac allE 1));
+ by (etac impE 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
+ by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
+ less_imp_le,lessI]) 1);
+(** LEVEL 10 **)
+ by (strip_tac 1);
+ by (REPEAT (etac allE 1));
+ by (etac impE 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
+ by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
+ less_imp_le,lessI]) 1);
+(** LEVEL 15 **)
+(* case App e1 e2 *)
+by (simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
+by (rtac conjI 1);
+ by (fast_tac (HOL_cs addss !simpset) 1);
+by (strip_tac 1);
+by (rename_tac "s1 t1' n1'" 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","m")] allE 1);
+by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","s1'")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","s1'")] allE 1);
+by (eres_inst_tac [("x","s2'")] allE 1);
+by (eres_inst_tac [("x","t2")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+(** LEVEL 34 **)
+by (rtac conjI 1);
+ by (strip_tac 1);
+ by (mp_tac 1);
+ by (mp_tac 1);
+ by (etac exE 1);
+ by (etac conjE 1);
+ by (etac impE 1);
+ by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
+ by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
+ addss !simpset) 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
+(** LEVEL 45 **)
+by (strip_tac 1);
+by (rename_tac "s2 t2' n2'" 1);
+by (rtac conjI 1);
+ by (strip_tac 1);
+ by (mp_tac 1);
+ by (mp_tac 1);
+ by (etac exE 1);
+ by (etac conjE 1);
+ by (etac impE 1);
+ by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
+ by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
+ addss !simpset) 1);
+ by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
+by (strip_tac 1);
+by (mp_tac 1);
+(** LEVEL 60 **)
+by (mp_tac 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (etac impE 1);
+ by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
+ by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
+ addss !simpset) 1);
+by (mp_tac 1);
+by (REPEAT (eresolve_tac [exE,conjE] 1));
+by (REPEAT(EVERY1
+ [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
+ REPEAT o etac conjE, hyp_subst_tac]));
+(** LEVEL 70 **)
+by (safe_tac HOL_cs);
+ by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);
+by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
+ by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
+by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
+by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
+by (safe_tac HOL_cs);
+ by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
+ addss !simpset) 1);
+ by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
+ addss !simpset) 1);
+(** LEVEL 79 **)
+by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
+by ((dtac new_tv_subst_tel 1) THEN (atac 1));
+by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
+by ((dtac new_tv_subst_tel 1) THEN (atac 1));
+by (best_tac (HOL_cs addDs [new_tv_W]
+ addss (!simpset addsimps [subst_comp_tel])) 1);
+(** LEVEL 84 **)
+qed_spec_mp "I_correct_wrt_W";
+
+(***
+We actually want the corollary
+
+goal I.thy
+ "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
+by (cut_facts_tac [(read_instantiate[("x","id_subst")]
+ (read_instantiate[("x","[]")](thm RS spec)
+ RS spec RS spec))] 1);
+by (Full_simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed;
+
+assuming that thm is the undischarged version of I_correct_wrt_W.
+
+Wait until simplification of thms is possible.
+***)
+
+val lemma = I_correct_wrt_W COMP swap_prems_rl;
+
+goal I.thy "!a m s. \
+\ new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
+by (expr.induct_tac "e" 1);
+ by (simp_tac (!simpset addsimps [app_subst_list]
+ setloop (split_tac [expand_if])) 1);
+ by (Simp_tac 1);
+ by (strip_tac 1);
+ by (rtac conjI 1);
+ by (strip_tac 1);
+ by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
+ by (asm_simp_tac (HOL_ss addsimps
+ [new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);
+ by (etac conjE 1);
+ by (dtac (new_tv_not_free_tv RS not_free_impl_id) 1);
+ by (Asm_simp_tac 1);
+ by (strip_tac 1);
+ by (etac exE 1);
+ by (split_all_tac 1);
+ by (Full_simp_tac 1);
+(** LEVEL 15 **)
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (etac exE 1);
+by (REPEAT(etac conjE 1));
+by (split_all_tac 1);
+by (Full_simp_tac 1);
+by (dtac lemma 1);
+ by (fast_tac HOL_cs 1);
+(** LEVEL 23 **)
+by (etac exE 1);
+by (etac conjE 1);
+by (hyp_subst_tac 1);
+by (Asm_simp_tac 1);
+by (etac disjE 1);
+ by (rtac disjI1 1);
+(** LEVEL 29 **)
+ by (full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1);
+ by (EVERY[etac allE 1, etac allE 1, etac allE 1,
+ etac impE 1, etac impE 2, atac 2, atac 2]);
+ by (rtac conjI 1);
+ by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
+ by (rtac new_tv_subst_comp_2 1);
+ by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
+ by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
+by (rtac disjI2 1);
+by (etac exE 1);
+by (split_all_tac 1);
+by (etac conjE 1);
+(** LEVEL 40 **)
+by (Full_simp_tac 1);
+by (dtac lemma 1);
+ by (rtac conjI 1);
+ by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
+ by (rtac new_tv_subst_comp_1 1);
+ by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
+ by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
+by (etac exE 1);
+by (etac conjE 1);
+by (hyp_subst_tac 1);
+(** LEVEL 50 **)
+by (asm_full_simp_tac (!simpset addsimps
+ [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
+qed_spec_mp "I_complete_wrt_W";
+
+(***
+We actually want the corollary
+
+ "I e [] m id_subst = Fail ==> W e [] m = Fail";
+
+Wait until simplification of thms is possible.
+***)
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/I.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/I.thy Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,23 @@
+(* Title: MiniML.thy
+ Author: Thomas Stauner
+ Copyright 1995 TU Muenchen
+
+ Recursive definition of type inference algorithm I for Mini_ML.
+*)
+
+I = W +
+
+consts
+ I :: [expr, typ list, nat, subst] => result_W
+
+primrec I expr
+ "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+ else Fail)"
+ "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+ Ok(s, TVar n -> t, m) )"
+ "I (App e1 e2) a n s =
+ ( (s1,t1,m1) := I e1 a n s;
+ (s2,t2,m2) := I e2 a m1 s1;
+ u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+ Ok($u o s2, TVar m2, Suc m2) )"
+end
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/Maybe.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/Maybe.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,27 @@
+open Maybe;
+
+(* 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";
+by (Simp_tac 1);
+qed "bind_Fail";
+
+Addsimps [bind_Ok,bind_Fail];
+
+(* expansion of bind *)
+goal thy
+ "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
+by (maybe.induct_tac "res" 1);
+by (fast_tac (HOL_cs addss !simpset) 1);
+by (Asm_simp_tac 1);
+qed "expand_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";
+
+Addsimps [bind_eq_Fail];
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/Maybe.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/Maybe.thy Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,20 @@
+(* Title: HOL/MiniML/Maybe.thy
+ ID: $Id$
+ Author: Dieter Nazareth and Tobias Nipkow
+ Copyright 1995 TU Muenchen
+
+Universal error monad.
+*)
+
+Maybe = List +
+
+datatype 'a maybe = Ok 'a | Fail
+
+constdefs
+ bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
+ "m bind f == case m of Ok r => f r | Fail => Fail"
+
+syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
+translations "P := E; F" == "E bind (%P.F)"
+
+end
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/MiniML.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/MiniML.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,24 @@
+(* Title: HOL/MiniML/MiniML.ML
+ ID: $Id$
+ Author: Dieter Nazareth and Tobias Nipkow
+ Copyright 1995 TU Muenchen
+*)
+
+open MiniML;
+
+Addsimps has_type.intrs;
+Addsimps [Un_upper1,Un_upper2];
+
+
+(* has_type is closed w.r.t. substitution *)
+goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+by (etac has_type.induct 1);
+(* case VarI *)
+by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
+by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
+by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
+(* case AbsI *)
+by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
+(* case AppI *)
+by (Asm_full_simp_tac 1);
+qed "has_type_cl_sub";
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/MiniML.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/MiniML.thy Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/MiniML/MiniML.thy
+ ID: $Id$
+ Author: Dieter Nazareth and Tobias Nipkow
+ Copyright 1995 TU Muenchen
+
+Mini_ML with type inference rules.
+*)
+
+MiniML = Type +
+
+(* expressions *)
+datatype
+ expr = Var nat | Abs expr | App expr expr
+
+(* type inference rules *)
+consts
+ has_type :: "(typ list * expr * typ)set"
+syntax
+ "@has_type" :: [typ list, expr, typ] => bool
+ ("((_) |-/ (_) :: (_))" [60,0,60] 60)
+translations
+ "a |- e :: t" == "(a,e,t):has_type"
+
+inductive has_type
+intrs
+ VarI "[| n < length a |] ==> a |- Var n :: 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"
+
+end
+
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/README.html Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,23 @@
+HOL/W0/README
+
+
+Type Inference for MiniML (without let)
+
+This theory defines the type inference rules and the type inference algorithm
+W for simply-typed lambda terms due to Milner. It proves the
+soundness and completeness of W w.r.t. to the rules. An optimized
+version I is shown to implement W.
+
+
+
+A report describing the theory is found here:
+
+Formal Verification of Algorithm W: The Monomorphic Case.
+
+
+
+NOTE: This theory has been superseded by a more recent development
+which formalizes type inference for a language including let. For
+details click here.
+
+
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/ROOT.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/ROOT.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,16 @@
+(* Title: HOL/MiniML/ROOT.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1995 TUM
+
+Type inference for let-free 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";
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/Type.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/Type.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,352 @@
+open Type;
+
+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";
+
+(* 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];
+
+(* application of id_subst does not change list of type expressions *)
+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];
+
+goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "o_id_subst";
+Addsimps[o_id_subst];
+
+goalw thy [dom_def,id_subst_def,empty_def]
+ "dom id_subst = {}";
+by (Simp_tac 1);
+qed "dom_id_subst";
+Addsimps [dom_id_subst];
+
+goalw thy [cod_def]
+ "cod id_subst = {}";
+by (Simp_tac 1);
+qed "cod_id_subst";
+Addsimps [cod_id_subst];
+
+goalw thy [free_tv_subst]
+ "free_tv id_subst = {}";
+by (Simp_tac 1);
+qed "free_tv_id_subst";
+Addsimps [free_tv_id_subst];
+
+goalw thy [dom_def,cod_def,UNION_def,Bex_def]
+ "!!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);
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+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 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 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" typ typ (infixr 70)
+
+(* 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
+ "id_subst == (%n.TVar n)"
+
+(* extension of substitution to type structures *)
+consts
+ 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)"
+
+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)"
+
+(* domain of a substitution *)
+constdefs
+ dom :: subst => nat set
+ "dom s == {n. s n ~= TVar n}"
+
+(* codomain of a substitutions: the introduced variables *)
+constdefs
+ cod :: subst => nat set
+ "cod s == (UN m:dom s. free_tv (s m))"
+
+defs
+ free_tv_subst "free_tv s == (dom s) Un (cod s)"
+
+(* new_tv s n computes whether n is a new type variable w.r.t. a type
+ structure s, i.e. whether n is greater than any type variable
+ occuring in the type structure *)
+constdefs
+ new_tv :: [nat,'a::type_struct] => bool
+ "new_tv n ts == ! m. m:free_tv ts --> m subst maybe
+rules
+ mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
+ mgu_mg "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
+ ? r. s = $r o u"
+ mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
+ mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
+
+end
+
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/W.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/W.ML Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,385 @@
+(* Title: HOL/MiniML/W.ML
+ ID: $Id$
+ Author: Dieter Nazareth and Tobias Nipkow
+ Copyright 1995 TU Muenchen
+
+Correctness and completeness of type inference algorithm W
+*)
+
+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";
+
+val has_type_casesE = map(has_type.mk_cases expr.simps)
+ [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
+
+
+(* the resulting type variable is always greater or equal than the given one *)
+goal thy
+ "!a n s t m. W e a n = Ok (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);
+(* case Abs e *)
+by (simp_tac (!simpset setloop (split_tac [expand_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 (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 (eres_inst_tac [("x","n")] allE 1);
+by (eres_inst_tac [("x","$ s a")] allE 1);
+by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","t")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (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 (etac conjE 1);
+by (res_inst_tac [("j","na")] le_trans 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "W_var_ge";
+
+Addsimps [W_var_ge];
+
+goal thy
+ "!! s. Ok (s,t,m) = W e a n ==> n<=m";
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "W_var_geD";
+
+
+(* auxiliary lemma *)
+goal Maybe.thy "(y = Ok x) = (Ok x = y)";
+by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "rotate_Ok";
+
+
+(* resulting type variable is new *)
+goal 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";
+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);
+
+(* case Abs e *)
+by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
+ setloop (split_tac [expand_bind])) 1);
+by (strip_tac 1);
+by (eres_inst_tac [("x","Suc n")] allE 1);
+by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
+by (fast_tac (HOL_cs addss (!simpset
+ addsimps [new_tv_subst,new_tv_Suc_list])) 1);
+
+(* case App e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_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","n")] allE 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","t")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (eres_inst_tac [("x","$ s a")] allE 1);
+by (eres_inst_tac [("x","sa")] allE 1);
+by (eres_inst_tac [("x","ta")] allE 1);
+by (eres_inst_tac [("x","nb")] allE 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
+by (rtac conjI 1);
+by (rtac new_tv_subst_comp_2 1);
+by (rtac new_tv_subst_comp_2 1);
+by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
+by (res_inst_tac [("n","na")] new_tv_subst_le 1);
+by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
+by (Asm_simp_tac 1);
+by (fast_tac (HOL_cs addDs [W_var_geD] addIs
+ [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
+ 1);
+by (etac (sym RS mgu_new) 1);
+by (best_tac (HOL_cs addDs [W_var_geD]
+ addIs [new_tv_subst_te,new_tv_list_le,
+ new_tv_subst_tel,
+ lessI RS less_imp_le RS new_tv_le,
+ lessI RS less_imp_le RS new_tv_subst_le,
+ new_tv_le]) 1);
+by (fast_tac (HOL_cs addDs [W_var_geD]
+ addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
+ addss (!simpset)) 1);
+by (rtac (lessI RS new_tv_subst_var) 1);
+by (etac (sym RS mgu_new) 1);
+by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
+ addDs [W_var_geD]
+ addIs [new_tv_list_le,
+ new_tv_subst_tel,
+ lessI RS less_imp_le RS new_tv_subst_le,
+ new_tv_le]
+ addss !simpset) 1);
+by (fast_tac (HOL_cs addDs [W_var_geD]
+ addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
+ addss (!simpset)) 1);
+qed_spec_mp "new_tv_W";
+
+
+goal thy
+ "!n a s t m v. W e a n = Ok (s,t,m) --> \
+\ (v:free_tv s | v:free_tv t) --> v 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);
+
+(* case Abs e *)
+by (asm_full_simp_tac (!simpset addsimps
+ [free_tv_subst] setloop (split_tac [expand_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "s t na sa ta 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","t")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","v")] allE 1);
+by (fast_tac (HOL_cs addIs [cod_app_subst]
+ addss (!simpset addsimps [less_Suc_eq])) 1);
+
+(* case App e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "s t na sa ta nb sb sc tb 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","t")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","v")] allE 1);
+(* 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","v")] allE 1);
+by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) );
+by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
+by (dtac W_var_geD 1);
+by (dtac W_var_geD 1);
+by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
+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,
+ less_le_trans,less_not_refl2,subsetD]
+ addEs [UnE]
+ addss !simpset) 1);
+by (Asm_full_simp_tac 1);
+by (dtac (sym RS W_var_geD) 1);
+by (dtac (sym RS W_var_geD) 1);
+by ( (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]
+ addEs [UnE]
+ addss !simpset) 1);
+qed_spec_mp "free_tv_W";
+
+
+(* 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))";
+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);
+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_simp_tac 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","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);
+
+(** 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","t2 -> t'")] allE 1);
+by (eres_inst_tac [("x","n")] allE 1);
+by (safe_tac HOL_cs);
+by (eres_inst_tac [("x","r")] allE 1);
+by (eres_inst_tac [("x","$ s a")] allE 1);
+by (eres_inst_tac [("x","t2")] allE 1);
+by (eres_inst_tac [("x","m")] allE 1);
+by (dtac asm_rl 1);
+by (dtac asm_rl 1);
+by (dtac asm_rl 1);
+by (Asm_full_simp_tac 1);
+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);
+
+(** 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);
+by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
+\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
+ ("s","($ ra ta) -> t'")] ssubst 2);
+by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
+by (rtac eq_free_eq_subst_te 2);
+by (strip_tac 2);
+by (subgoal_tac "na ~=ma" 2);
+by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
+ new_tv_not_free_tv,new_tv_le]) 3);
+(** LEVEL 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);
+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 (asm_full_simp_tac (!simpset addsimps [dom_def]
+ setloop (split_tac [expand_if])) 3);
+(** LEVEL 50 **)
+(* 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 (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
+ (!simpset addsimps [cod_def,free_tv_subst])) 3);
+by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
+ 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 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 (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_mg 1) THEN (atac 1));
+by (etac exE 1);
+by (res_inst_tac [("x","rb")] exI 1);
+by (rtac conjI 1);
+by (dres_inst_tac [("x","ma")] fun_cong 2);
+by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
+by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel 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 (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 (( 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,
+ new_tv_not_free_tv]) 2);
+by (case_tac "na: free_tv t - free_tv sa" 1);
+(* case na ~: free_tv t - free_tv sa *)
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+(* 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 (Fast_tac 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'")]
+ W_complete_lemma 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "W_complete";
diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/W.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/W.thy Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,28 @@
+(* Title: HOL/MiniML/W.thy
+ ID: $Id$
+ Author: Dieter Nazareth and Tobias Nipkow
+ Copyright 1995 TU Muenchen
+
+Type inference algorithm W
+*)
+
+W = MiniML +
+
+types
+ result_W = "(subst * typ * nat)maybe"
+
+(* type inference algorithm W *)
+consts
+ W :: [expr, typ list, nat] => result_W
+
+primrec W 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) )"
+end