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