converted;
authorwenzelm
Tue Feb 26 00:19:04 2002 +0100 (2002-02-26)
changeset 12944fa6a3ddec27f
parent 12943 1db24da0537b
child 12945 95853fbcc718
converted;
src/HOL/W0/I.ML
src/HOL/W0/I.thy
src/HOL/W0/Maybe.ML
src/HOL/W0/Maybe.thy
src/HOL/W0/MiniML.ML
src/HOL/W0/MiniML.thy
src/HOL/W0/ROOT.ML
src/HOL/W0/Type.ML
src/HOL/W0/Type.thy
src/HOL/W0/W.ML
src/HOL/W0/W.thy
src/HOL/W0/W0.thy
src/HOL/W0/document/root.tex
     1.1 --- a/src/HOL/W0/I.ML	Mon Feb 25 20:51:48 2002 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,207 +0,0 @@
     1.4 -(* Title:     HOL/W0/I.ML
     1.5 -   ID:        $Id$
     1.6 -   Author:    Thomas Stauner
     1.7 -   Copyright  1995 TU Muenchen
     1.8 -
     1.9 -Equivalence of W and I.
    1.10 -*)
    1.11 -
    1.12 -open I;
    1.13 -
    1.14 -Goal "! a m s s' t n.  \
    1.15 -\    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
    1.16 -\    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
    1.17 -by (induct_tac "e" 1);
    1.18 -
    1.19 -  (* case Var n *)
    1.20 -  by (simp_tac (simpset() addsimps [app_subst_list]
    1.21 -      setloop (split_inside_tac [split_if])) 1);
    1.22 -
    1.23 - (* case Abs e *)
    1.24 - by (asm_full_simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
    1.25 - by (strip_tac 1);
    1.26 - by (rtac conjI 1);
    1.27 -  by (strip_tac 1);
    1.28 -  by (REPEAT (etac allE 1));
    1.29 -  by (etac impE 1);
    1.30 -   by (fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])) 2);
    1.31 -  by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.32 -                              less_imp_le,lessI]) 1); 
    1.33 -(** LEVEL 10 **)
    1.34 - by (strip_tac 1);
    1.35 - by (REPEAT (etac allE 1));
    1.36 - by (etac impE 1);
    1.37 -  by (fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst])) 2);
    1.38 - by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.39 -                             less_imp_le,lessI]) 1);
    1.40 -(** LEVEL 15 **)
    1.41 -(* case App e1 e2 *)
    1.42 -by (simp_tac (simpset() setloop (split_inside_tac [split_bind])) 1);
    1.43 -by (strip_tac 1);
    1.44 -by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
    1.45 -by (rtac conjI 1);
    1.46 - by (fast_tac (HOL_cs addss simpset()) 1);
    1.47 -by (strip_tac 1);
    1.48 -by (rename_tac "s1 t1' n1'" 1);
    1.49 -by (eres_inst_tac [("x","a")] allE 1);
    1.50 -by (eres_inst_tac [("x","m")] allE 1);
    1.51 -by (eres_inst_tac [("x","s")] allE 1);
    1.52 -by (eres_inst_tac [("x","s1'")] allE 1);
    1.53 -by (eres_inst_tac [("x","t1")] allE 1);
    1.54 -by (eres_inst_tac [("x","n1")] allE 1);
    1.55 -by (eres_inst_tac [("x","a")] allE 1);
    1.56 -by (eres_inst_tac [("x","n1")] allE 1);
    1.57 -by (eres_inst_tac [("x","s1'")] allE 1);
    1.58 -by (eres_inst_tac [("x","s2'")] allE 1);
    1.59 -by (eres_inst_tac [("x","t2")] allE 1);
    1.60 -by (eres_inst_tac [("x","n2")] allE 1);
    1.61 -(** LEVEL 34 **)
    1.62 -by (rtac conjI 1);
    1.63 - by (strip_tac 1);
    1.64 - by (rtac notI 1);
    1.65 - by (Asm_full_simp_tac 1);
    1.66 -(* by (mp_tac 1);
    1.67 - by (mp_tac 1);
    1.68 - by (etac exE 1);
    1.69 - by (etac conjE 1);*)
    1.70 - by (etac impE 1);
    1.71 -  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
    1.72 -  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    1.73 -  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    1.74 -                       addss simpset()) 1);
    1.75 - by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel])) 1);
    1.76 -(** LEVEL 45 **)
    1.77 -by (strip_tac 1);
    1.78 -by (rename_tac "s2 t2' n2'" 1);
    1.79 -by (rtac conjI 1);
    1.80 - by (strip_tac 1);
    1.81 - by (rtac notI 1);
    1.82 - by (Asm_full_simp_tac 1);
    1.83 -(*
    1.84 - by (mp_tac 1);
    1.85 - by (mp_tac 1);
    1.86 - by (etac exE 1);
    1.87 - by (etac conjE 1);*)
    1.88 - by (etac impE 1);
    1.89 -  by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
    1.90 -  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    1.91 -  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    1.92 -                       addss simpset()) 1);
    1.93 - by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel,subst_comp_te])) 1);
    1.94 -by (strip_tac 1);
    1.95 -by (mp_tac 1);
    1.96 -(** LEVEL 60 **)
    1.97 -by (mp_tac 1);
    1.98 -by (etac exE 1);
    1.99 -by (etac conjE 1);
   1.100 -by (etac impE 1);
   1.101 - by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
   1.102 - by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.103 - by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.104 -                      addss simpset()) 1);
   1.105 -by (mp_tac 1);
   1.106 -by (REPEAT (eresolve_tac [exE,conjE] 1));
   1.107 -by (REPEAT(EVERY1
   1.108 -     [asm_full_simp_tac (simpset() addsimps [subst_comp_tel,subst_comp_te,o_def]),
   1.109 -      REPEAT o etac conjE, hyp_subst_tac]));
   1.110 -(** LEVEL 70 **)
   1.111 -by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
   1.112 - by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   1.113 -by ((ftac new_tv_subst_tel 1) THEN (atac 1));
   1.114 -by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.115 -by (safe_tac HOL_cs);
   1.116 -  by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.117 -                       addss simpset()) 1);
   1.118 - by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.119 -                      addss simpset()) 1);
   1.120 -(** LEVEL 77 **)
   1.121 -by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
   1.122 -by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   1.123 -by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
   1.124 -by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   1.125 -by (best_tac (HOL_cs addDs [new_tv_W] 
   1.126 -                     addss (simpset() addsimps [subst_comp_tel])) 1);
   1.127 -(** LEVEL 82 **)
   1.128 -qed_spec_mp "I_correct_wrt_W";
   1.129 -
   1.130 -(***
   1.131 -We actually want the corollary
   1.132 -
   1.133 -Goal "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
   1.134 -by (cut_facts_tac [(read_instantiate[("x","id_subst")]
   1.135 - (read_instantiate[("x","[]")](thm RS spec)
   1.136 -  RS spec RS spec))] 1);
   1.137 -by (Full_simp_tac 1);
   1.138 -by (fast_tac HOL_cs 1);
   1.139 -qed;
   1.140 -
   1.141 -assuming that thm is the undischarged version of I_correct_wrt_W.
   1.142 -
   1.143 -Wait until simplification of thms is possible.
   1.144 -***)
   1.145 -
   1.146 -val lemma = I_correct_wrt_W COMP swap_prems_rl;
   1.147 -
   1.148 -Addsimps [split_paired_Ex];
   1.149 -
   1.150 -Goal "!a m s. \
   1.151 -\  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
   1.152 -by (induct_tac "e" 1);
   1.153 -  by (simp_tac (simpset() addsimps [app_subst_list]) 1);
   1.154 - by (Simp_tac 1);
   1.155 - by (strip_tac 1);
   1.156 - by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
   1.157 -  by (asm_simp_tac (HOL_ss addsimps
   1.158 -        [new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);
   1.159 - by (etac conjE 1);
   1.160 - by (dtac (new_tv_not_free_tv RS not_free_impl_id) 1);
   1.161 - by (Asm_simp_tac 1);
   1.162 -(** LEVEL 9 **)
   1.163 -by (Asm_simp_tac 1);
   1.164 -by (strip_tac 1);
   1.165 -by (REPEAT(etac exE 1));
   1.166 -by (REPEAT(etac conjE 1));
   1.167 -by (dtac lemma 1);
   1.168 - by (fast_tac HOL_cs 1);
   1.169 -(** LEVEL 15 **)
   1.170 -by (etac exE 1);
   1.171 -by (etac conjE 1);
   1.172 -by (hyp_subst_tac 1);
   1.173 -by (Asm_simp_tac 1);
   1.174 -by (REPEAT(resolve_tac [exI,conjI,refl] 1));
   1.175 -by (etac disjE 1);
   1.176 - by (rtac disjI1 1);
   1.177 -(** LEVEL 22 **)
   1.178 - by (full_simp_tac (simpset() addsimps [o_def,subst_comp_tel]) 1);
   1.179 - by (EVERY[etac allE 1, etac allE 1, etac allE 1,
   1.180 -          etac impE 1, etac impE 2, atac 2, atac 2]);
   1.181 - by (rtac conjI 1);
   1.182 -  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
   1.183 - by (rtac new_tv_subst_comp_2 1);
   1.184 -  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
   1.185 - by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
   1.186 -by (rtac disjI2 1);
   1.187 -by (REPEAT(etac exE 1));
   1.188 -by (etac conjE 1);
   1.189 -(** LEVEL 32 **)
   1.190 -by (dtac lemma 1);
   1.191 - by (rtac conjI 1);
   1.192 -  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
   1.193 - by (rtac new_tv_subst_comp_1 1);
   1.194 -  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
   1.195 - by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
   1.196 -by (etac exE 1);
   1.197 -by (etac conjE 1);
   1.198 -by (hyp_subst_tac 1);
   1.199 -(** LEVEL 41 **)
   1.200 -by (asm_full_simp_tac (simpset() addsimps
   1.201 -     [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
   1.202 -qed_spec_mp "I_complete_wrt_W";
   1.203 -
   1.204 -(***
   1.205 -We actually want the corollary
   1.206 -
   1.207 -  "I e [] m id_subst = Fail ==> W e [] m = Fail";
   1.208 -
   1.209 -Wait until simplification of thms is possible.
   1.210 -***)
     2.1 --- a/src/HOL/W0/I.thy	Mon Feb 25 20:51:48 2002 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,24 +0,0 @@
     2.4 -(* Title:     HOL/W0/I.thy
     2.5 -   ID:        $Id$
     2.6 -   Author:    Thomas Stauner
     2.7 -   Copyright  1995 TU Muenchen
     2.8 -
     2.9 -   Recursive definition of type inference algorithm I for Mini_ML.
    2.10 -*)
    2.11 -
    2.12 -I = W +
    2.13 -
    2.14 -consts
    2.15 -        I :: [expr, typ list, nat, subst] => result_W
    2.16 -
    2.17 -primrec
    2.18 -        "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
    2.19 -                                    else Fail)"
    2.20 -        "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
    2.21 -                                     Ok(s, TVar n -> t, m) )"
    2.22 -        "I (App e1 e2) a n s =
    2.23 -                   ( (s1,t1,m1) := I e1 a n s;
    2.24 -                     (s2,t2,m2) := I e2 a m1 s1;
    2.25 -                     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
    2.26 -                     Ok($u o s2, TVar m2, Suc m2) )"
    2.27 -end
     3.1 --- a/src/HOL/W0/Maybe.ML	Mon Feb 25 20:51:48 2002 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,39 +0,0 @@
     3.4 -(* Title:     HOL/W0/Maybe.ML
     3.5 -   ID:        $Id$
     3.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     3.7 -   Copyright  1995 TU Muenchen
     3.8 -*)
     3.9 -
    3.10 -
    3.11 -(* constructor laws for bind *)
    3.12 -Goalw [bind_def] "(Ok s) bind f = (f s)";
    3.13 -by (Simp_tac 1);
    3.14 -qed "bind_Ok";
    3.15 -
    3.16 -Goalw [bind_def] "Fail bind f = Fail";
    3.17 -by (Simp_tac 1);
    3.18 -qed "bind_Fail";
    3.19 -
    3.20 -Addsimps [bind_Ok,bind_Fail];
    3.21 -
    3.22 -(* case splitting of bind *)
    3.23 -Goal
    3.24 -  "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
    3.25 -by (induct_tac "res" 1);
    3.26 -by (fast_tac (HOL_cs addss simpset()) 1);
    3.27 -by (Asm_simp_tac 1);
    3.28 -qed "split_bind";
    3.29 -
    3.30 -Goal
    3.31 -  "P(res bind f) = (~ (res = Fail & ~ P Fail | (? s. res = Ok s & ~ P(f s))))";
    3.32 - by (simp_tac (simpset() addsplits [split_bind]) 1);
    3.33 -qed "split_bind_asm";
    3.34 -
    3.35 -bind_thms ("bind_splits", [split_bind, split_bind_asm]);
    3.36 -
    3.37 -Goal
    3.38 -  "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
    3.39 -by (simp_tac (simpset() addsplits [split_bind]) 1);
    3.40 -qed "bind_eq_Fail";
    3.41 -
    3.42 -Addsimps [bind_eq_Fail];
     4.1 --- a/src/HOL/W0/Maybe.thy	Mon Feb 25 20:51:48 2002 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,20 +0,0 @@
     4.4 -(* Title:     HOL/W0/Maybe.thy
     4.5 -   ID:        $Id$
     4.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     4.7 -   Copyright  1995 TU Muenchen
     4.8 -
     4.9 -Universal error monad.
    4.10 -*)
    4.11 -
    4.12 -Maybe = List +
    4.13 -
    4.14 -datatype 'a maybe =  Ok 'a | Fail
    4.15 -
    4.16 -constdefs
    4.17 -  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
    4.18 -  "m bind f == case m of Ok r => f r | Fail => Fail"
    4.19 -
    4.20 -syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
    4.21 -translations "P := E; F" == "E bind (%P. F)"
    4.22 -
    4.23 -end
     5.1 --- a/src/HOL/W0/MiniML.ML	Mon Feb 25 20:51:48 2002 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,24 +0,0 @@
     5.4 -(* Title:     HOL/W0/MiniML.ML
     5.5 -   ID:        $Id$
     5.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     5.7 -   Copyright  1995 TU Muenchen
     5.8 -*)
     5.9 -
    5.10 -open MiniML;
    5.11 -
    5.12 -Addsimps has_type.intrs;
    5.13 -Addsimps [Un_upper1,Un_upper2];
    5.14 -
    5.15 -
    5.16 -(* has_type is closed w.r.t. substitution *)
    5.17 -Goal "a |- e :: t ==> $s a |- e :: $s t";
    5.18 -by (etac has_type.induct 1);
    5.19 -(* case VarI *)
    5.20 -by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
    5.21 -by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
    5.22 -by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (simpset() delsimps [nth_map])) 1);
    5.23 -(* case AbsI *)
    5.24 -by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
    5.25 -(* case AppI *)
    5.26 -by (Asm_full_simp_tac 1);
    5.27 -qed "has_type_cl_sub";
     6.1 --- a/src/HOL/W0/MiniML.thy	Mon Feb 25 20:51:48 2002 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,32 +0,0 @@
     6.4 -(* Title:     HOL/W0/MiniML.thy
     6.5 -   ID:        $Id$
     6.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     6.7 -   Copyright  1995 TU Muenchen
     6.8 -
     6.9 -Mini_ML with type inference rules.
    6.10 -*)
    6.11 -
    6.12 -MiniML = Type + 
    6.13 -
    6.14 -(* expressions *)
    6.15 -datatype
    6.16 -        expr = Var nat | Abs expr | App expr expr
    6.17 -
    6.18 -(* type inference rules *)
    6.19 -consts
    6.20 -        has_type :: "(typ list * expr * typ)set"
    6.21 -syntax
    6.22 -        "@has_type" :: [typ list, expr, typ] => bool
    6.23 -                       ("((_) |-/ (_) :: (_))" [60,0,60] 60)
    6.24 -translations 
    6.25 -        "a |- e :: t" == "(a,e,t):has_type"
    6.26 -
    6.27 -inductive has_type
    6.28 -intrs
    6.29 -        VarI "[| n < length a |] ==> a |- Var n :: a!n"
    6.30 -        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
    6.31 -        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
    6.32 -              ==> a |- App e1 e2 :: t1"
    6.33 -
    6.34 -end
    6.35 -
     7.1 --- a/src/HOL/W0/ROOT.ML	Mon Feb 25 20:51:48 2002 +0100
     7.2 +++ b/src/HOL/W0/ROOT.ML	Tue Feb 26 00:19:04 2002 +0100
     7.3 @@ -1,13 +1,2 @@
     7.4 -(*  Title:      HOL/W0/ROOT.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Tobias Nipkow
     7.7 -    Copyright   1995 TUM
     7.8  
     7.9 -Type inference for let-free MiniML
    7.10 -*)
    7.11 -
    7.12 -Unify.trace_bound := 20;
    7.13 -
    7.14 -AddSEs [less_SucE];
    7.15 -
    7.16 -time_use_thy "I";
    7.17 +use_thy "W0";
     8.1 --- a/src/HOL/W0/Type.ML	Mon Feb 25 20:51:48 2002 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,341 +0,0 @@
     8.4 -(* Title:     HOL/W0/Type.ML
     8.5 -   ID:        $Id$
     8.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     8.7 -   Copyright  1995 TU Muenchen
     8.8 -*)
     8.9 -
    8.10 -Addsimps [mgu_eq,mgu_mg,mgu_free];
    8.11 -
    8.12 -(* mgu does not introduce new type variables *)
    8.13 -Goalw [new_tv_def] 
    8.14 -      "[|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
    8.15 -\            new_tv n u";
    8.16 -by (fast_tac (set_cs addDs [mgu_free]) 1);
    8.17 -qed "mgu_new";
    8.18 -
    8.19 -(* application of id_subst does not change type expression *)
    8.20 -Goalw [id_subst_def]
    8.21 -  "$ id_subst = (%t::typ. t)";
    8.22 -by (rtac ext 1);
    8.23 -by (induct_tac "t" 1);
    8.24 -by (ALLGOALS Asm_simp_tac);
    8.25 -qed "app_subst_id_te";
    8.26 -Addsimps [app_subst_id_te];
    8.27 -
    8.28 -(* application of id_subst does not change list of type expressions *)
    8.29 -Goalw [app_subst_list]
    8.30 -  "$ id_subst = (%ts::typ list. ts)";
    8.31 -by (rtac ext 1); 
    8.32 -by (induct_tac "ts" 1);
    8.33 -by (ALLGOALS Asm_simp_tac);
    8.34 -qed "app_subst_id_tel";
    8.35 -Addsimps [app_subst_id_tel];
    8.36 -
    8.37 -Goalw [id_subst_def,o_def] "$s o id_subst = s";
    8.38 -by (rtac ext 1);
    8.39 -by (Simp_tac 1);
    8.40 -qed "o_id_subst";
    8.41 -Addsimps[o_id_subst];
    8.42 -
    8.43 -Goalw [dom_def,id_subst_def,empty_def]
    8.44 -  "dom id_subst = {}";
    8.45 -by (Simp_tac 1);
    8.46 -qed "dom_id_subst";
    8.47 -Addsimps [dom_id_subst];
    8.48 -
    8.49 -Goalw [cod_def]
    8.50 -  "cod id_subst = {}";
    8.51 -by (Simp_tac 1);
    8.52 -qed "cod_id_subst";
    8.53 -Addsimps [cod_id_subst];
    8.54 -
    8.55 -Goalw [free_tv_subst]
    8.56 -  "free_tv id_subst = {}";
    8.57 -by (Simp_tac 1);
    8.58 -qed "free_tv_id_subst";
    8.59 -Addsimps [free_tv_id_subst];
    8.60 -
    8.61 -Goalw [dom_def,cod_def,UNION_def,Bex_def]
    8.62 -  "[| v : free_tv(s n); v~=n |] ==> v : cod s";
    8.63 -by (Simp_tac 1);
    8.64 -by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
    8.65 -by (assume_tac 2);
    8.66 -by (rotate_tac 1 1);
    8.67 -by (Asm_full_simp_tac 1);
    8.68 -qed "cod_app_subst";
    8.69 -Addsimps [cod_app_subst];
    8.70 -
    8.71 -
    8.72 -(* composition of substitutions *)
    8.73 -Goal
    8.74 -  "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
    8.75 -by (induct_tac "t" 1);
    8.76 -by (ALLGOALS Asm_simp_tac);
    8.77 -qed "subst_comp_te";
    8.78 -
    8.79 -Goalw [app_subst_list]
    8.80 -  "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
    8.81 -by (induct_tac "ts" 1);
    8.82 -(* case [] *)
    8.83 -by (Simp_tac 1);
    8.84 -(* case x#xl *)
    8.85 -by (asm_full_simp_tac (simpset() addsimps [subst_comp_te]) 1);
    8.86 -qed "subst_comp_tel";
    8.87 -
    8.88 -
    8.89 -(* constructor laws for app_subst *)
    8.90 -Goalw [app_subst_list]
    8.91 -  "$ s [] = []";
    8.92 -by (Simp_tac 1);
    8.93 -qed "app_subst_Nil";
    8.94 -
    8.95 -Goalw [app_subst_list]
    8.96 -  "$ s (t#ts) = ($ s t)#($ s ts)";
    8.97 -by (Simp_tac 1);
    8.98 -qed "app_subst_Cons";
    8.99 -
   8.100 -Addsimps [app_subst_Nil,app_subst_Cons];
   8.101 -
   8.102 -(* constructor laws for new_tv *)
   8.103 -Goalw [new_tv_def]
   8.104 -  "new_tv n (TVar m) = (m<n)";
   8.105 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.106 -qed "new_tv_TVar";
   8.107 -
   8.108 -Goalw [new_tv_def]
   8.109 -  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
   8.110 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.111 -qed "new_tv_Fun";
   8.112 -
   8.113 -Goalw [new_tv_def]
   8.114 -  "new_tv n []";
   8.115 -by (Simp_tac 1);
   8.116 -qed "new_tv_Nil";
   8.117 -
   8.118 -Goalw [new_tv_def]
   8.119 -  "new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
   8.120 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.121 -qed "new_tv_Cons";
   8.122 -
   8.123 -Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons];
   8.124 -
   8.125 -Goalw [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
   8.126 -  "new_tv n id_subst";
   8.127 -by (Simp_tac 1);
   8.128 -qed "new_tv_id_subst";
   8.129 -Addsimps[new_tv_id_subst];
   8.130 -
   8.131 -Goalw [new_tv_def]
   8.132 -  "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
   8.133 -\                (! l. l < n --> new_tv n (s l) ))";
   8.134 -by (safe_tac HOL_cs );
   8.135 -(* ==> *)
   8.136 -by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1);
   8.137 -by (subgoal_tac "m:cod s | s l = TVar l" 1);
   8.138 -by (safe_tac HOL_cs );
   8.139 -by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1);
   8.140 -by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
   8.141 -by (Asm_full_simp_tac 1);
   8.142 -by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1);
   8.143 -(* <== *)
   8.144 -by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
   8.145 -by (safe_tac set_cs );
   8.146 -by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
   8.147 -by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   8.148 -by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
   8.149 -by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
   8.150 -qed "new_tv_subst";
   8.151 -
   8.152 -Goal "new_tv n x = (!y:set x. new_tv n y)";
   8.153 -by (induct_tac "x" 1);
   8.154 -by (ALLGOALS Asm_simp_tac);
   8.155 -qed "new_tv_list";
   8.156 -
   8.157 -(* substitution affects only variables occurring freely *)
   8.158 -Goal
   8.159 -  "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
   8.160 -by (induct_tac "t" 1);
   8.161 -by (ALLGOALS Asm_simp_tac);
   8.162 -qed "subst_te_new_tv";
   8.163 -Addsimps [subst_te_new_tv];
   8.164 -
   8.165 -Goal
   8.166 -  "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
   8.167 -by (induct_tac "ts" 1);
   8.168 -by (ALLGOALS Asm_full_simp_tac);
   8.169 -qed "subst_tel_new_tv";
   8.170 -Addsimps [subst_tel_new_tv];
   8.171 -
   8.172 -(* all greater variables are also new *)
   8.173 -Goal
   8.174 -  "n<=m --> new_tv n (t::typ) --> new_tv m t";
   8.175 -by (induct_tac "t" 1);
   8.176 -(* case TVar n *)
   8.177 -by (fast_tac (HOL_cs addIs [less_le_trans] addss simpset()) 1);
   8.178 -(* case Fun t1 t2 *)
   8.179 -by (Asm_simp_tac 1);
   8.180 -qed_spec_mp "new_tv_le";
   8.181 -Addsimps [lessI RS less_imp_le RS new_tv_le];
   8.182 -
   8.183 -Goal 
   8.184 -  "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
   8.185 -by (induct_tac "ts" 1);
   8.186 -(* case [] *)
   8.187 -by (Simp_tac 1);
   8.188 -(* case a#al *)
   8.189 -by (fast_tac (HOL_cs addIs [new_tv_le] addss simpset()) 1);
   8.190 -qed_spec_mp "new_tv_list_le";
   8.191 -Addsimps [lessI RS less_imp_le RS new_tv_list_le];
   8.192 -
   8.193 -Goal
   8.194 -  "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
   8.195 -by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   8.196 -by (Clarify_tac 1);
   8.197 -by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
   8.198 -by (Clarify_tac 1);
   8.199 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) );
   8.200 -qed "new_tv_subst_le";
   8.201 -Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
   8.202 -
   8.203 -(* new_tv property remains if a substitution is applied *)
   8.204 -Goal
   8.205 -  "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
   8.206 -by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   8.207 -qed "new_tv_subst_var";
   8.208 -
   8.209 -Goal "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
   8.210 -by (induct_tac "t" 1);
   8.211 -by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
   8.212 -qed_spec_mp "new_tv_subst_te";
   8.213 -Addsimps [new_tv_subst_te];
   8.214 -
   8.215 -Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
   8.216 -by (simp_tac (simpset() addsimps [new_tv_list]) 1);
   8.217 -by (induct_tac "ts" 1);
   8.218 -by Safe_tac;
   8.219 -by    (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
   8.220 -qed_spec_mp "new_tv_subst_tel";
   8.221 -Addsimps [new_tv_subst_tel];
   8.222 -
   8.223 -(* auxilliary lemma *)
   8.224 -Goal "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
   8.225 -by (simp_tac (simpset() addsimps [new_tv_list]) 1);
   8.226 -qed "new_tv_Suc_list";
   8.227 -
   8.228 -
   8.229 -(* composition of substitutions preserves new_tv proposition *)
   8.230 -Goal 
   8.231 -     "[| new_tv n (s::subst); new_tv n r |] ==> \
   8.232 -\           new_tv n (($ r) o s)";
   8.233 -by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   8.234 -qed "new_tv_subst_comp_1";
   8.235 -
   8.236 -Goal
   8.237 -     "[| new_tv n (s::subst); new_tv n r |] ==>  \ 
   8.238 -\     new_tv n (%v.$ r (s v))";
   8.239 -by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   8.240 -qed "new_tv_subst_comp_2";
   8.241 -
   8.242 -Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
   8.243 -
   8.244 -(* new type variables do not occur freely in a type structure *)
   8.245 -Goalw [new_tv_def] 
   8.246 -      "new_tv n ts ==> n~:(free_tv ts)";
   8.247 -by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
   8.248 -qed "new_tv_not_free_tv";
   8.249 -Addsimps [new_tv_not_free_tv];
   8.250 -
   8.251 -Goal
   8.252 -  "(t::typ): set ts --> free_tv t <= free_tv ts";
   8.253 -by (induct_tac "ts" 1);
   8.254 -(* case [] *)
   8.255 -by (Simp_tac 1);
   8.256 -(* case x#xl *)
   8.257 -by (fast_tac (set_cs addss simpset()) 1);
   8.258 -qed_spec_mp "ftv_mem_sub_ftv_list";
   8.259 -Addsimps [ftv_mem_sub_ftv_list];
   8.260 -
   8.261 -
   8.262 -(* if two substitutions yield the same result if applied to a type
   8.263 -   structure the substitutions coincide on the free type variables
   8.264 -   occurring in the type structure *)
   8.265 -Goal
   8.266 -  "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
   8.267 -by (induct_tac "t" 1);
   8.268 -(* case TVar n *)
   8.269 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.270 -(* case Fun t1 t2 *)
   8.271 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.272 -qed_spec_mp "eq_subst_te_eq_free";
   8.273 -
   8.274 -Goal
   8.275 -  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
   8.276 -by (induct_tac "t" 1);
   8.277 -(* case TVar n *)
   8.278 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.279 -(* case Fun t1 t2 *)
   8.280 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.281 -qed_spec_mp "eq_free_eq_subst_te";
   8.282 -
   8.283 -Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
   8.284 -by (induct_tac "ts" 1);
   8.285 -(* case [] *)
   8.286 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.287 -(* case x#xl *)
   8.288 -by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1);
   8.289 -qed_spec_mp "eq_subst_tel_eq_free";
   8.290 -
   8.291 -Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
   8.292 -by (induct_tac "ts" 1); 
   8.293 -(* case [] *)
   8.294 -by (fast_tac (HOL_cs addss simpset()) 1);
   8.295 -(* case x#xl *)
   8.296 -by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (simpset())) 1);
   8.297 -qed_spec_mp "eq_free_eq_subst_tel";
   8.298 -
   8.299 -(* some useful theorems *)
   8.300 -Goalw [free_tv_subst] 
   8.301 -      "v : cod s ==> v : free_tv s";
   8.302 -by (fast_tac set_cs 1);
   8.303 -qed "codD";
   8.304 - 
   8.305 -Goalw [free_tv_subst,dom_def] 
   8.306 -      "x ~: free_tv s ==> s x = TVar x";
   8.307 -by (fast_tac set_cs 1);
   8.308 -qed "not_free_impl_id";
   8.309 -
   8.310 -Goalw [new_tv_def] "[| new_tv n t; m:free_tv t |] ==> m<n";
   8.311 -by (fast_tac HOL_cs 1 );
   8.312 -qed "free_tv_le_new_tv";
   8.313 -
   8.314 -Goal "free_tv (s (v::nat)) <= insert v (cod s)";
   8.315 -by (expand_case_tac "v:dom s" 1);
   8.316 -by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
   8.317 -by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
   8.318 -qed "free_tv_subst_var";
   8.319 -
   8.320 -Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
   8.321 -by (induct_tac "t" 1);
   8.322 -(* case TVar n *)
   8.323 -by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
   8.324 -(* case Fun t1 t2 *)
   8.325 -by (fast_tac (set_cs addss simpset()) 1);
   8.326 -qed "free_tv_app_subst_te";     
   8.327 -
   8.328 -Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
   8.329 -by (induct_tac "ts" 1);
   8.330 -(* case [] *)
   8.331 -by (Simp_tac 1);
   8.332 -(* case a#al *)
   8.333 -by (cut_facts_tac [free_tv_app_subst_te] 1);
   8.334 -by (fast_tac (set_cs addss simpset()) 1);
   8.335 -qed "free_tv_app_subst_tel";
   8.336 -
   8.337 -Goalw [free_tv_subst,dom_def]
   8.338 -     "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
   8.339 -\     free_tv s1 Un free_tv s2";
   8.340 -by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
   8.341 -			     free_tv_subst_var RS subsetD] 
   8.342 -	             addss (simpset() delsimps bex_simps
   8.343 -				     addsimps [cod_def,dom_def])) 1);
   8.344 -qed "free_tv_comp_subst";
     9.1 --- a/src/HOL/W0/Type.thy	Mon Feb 25 20:51:48 2002 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,89 +0,0 @@
     9.4 -(* Title:     HOL/W0/Type.thy
     9.5 -   ID:        $Id$
     9.6 -   Author:    Dieter Nazareth and Tobias Nipkow
     9.7 -   Copyright  1995 TU Muenchen
     9.8 -
     9.9 -MiniML-types and type substitutions.
    9.10 -*)
    9.11 -
    9.12 -Type = Maybe + 
    9.13 -
    9.14 -(* new class for structures containing type variables *)
    9.15 -classes
    9.16 -        type_struct < type
    9.17 -
    9.18 -(* type expressions *)
    9.19 -datatype
    9.20 -        typ = TVar nat | "->" typ typ (infixr 70)
    9.21 -
    9.22 -(* type variable substitution *)
    9.23 -types
    9.24 -        subst = nat => typ
    9.25 -
    9.26 -arities
    9.27 -        typ::type_struct
    9.28 -        list::(type_struct)type_struct
    9.29 -        fun::(type,type_struct)type_struct
    9.30 -
    9.31 -(* substitutions *)
    9.32 -
    9.33 -(* identity *)
    9.34 -constdefs
    9.35 -        id_subst :: subst
    9.36 -        "id_subst == (%n. TVar n)"
    9.37 -
    9.38 -(* extension of substitution to type structures *)
    9.39 -consts
    9.40 -        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
    9.41 -
    9.42 -primrec
    9.43 -  app_subst_TVar  "$ s (TVar n) = s n" 
    9.44 -  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
    9.45 -
    9.46 -defs
    9.47 -        app_subst_list  "$ s == map ($ s)"
    9.48 -  
    9.49 -(* free_tv s: the type variables occuring freely in the type structure s *)
    9.50 -consts
    9.51 -        free_tv :: ['a::type_struct] => nat set
    9.52 -
    9.53 -primrec
    9.54 -  "free_tv (TVar m) = {m}"
    9.55 -  "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
    9.56 -
    9.57 -primrec
    9.58 -  "free_tv [] = {}"
    9.59 -  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    9.60 -
    9.61 -(* domain of a substitution *)
    9.62 -constdefs
    9.63 -        dom :: subst => nat set
    9.64 -        "dom s == {n. s n ~= TVar n}" 
    9.65 -
    9.66 -(* codomain of a substitutions: the introduced variables *)
    9.67 -constdefs
    9.68 -        cod :: subst => nat set
    9.69 -        "cod s == (UN m:dom s. free_tv (s m))"
    9.70 -
    9.71 -defs
    9.72 -        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
    9.73 -
    9.74 -(* new_tv s n computes whether n is a new type variable w.r.t. a type 
    9.75 -   structure s, i.e. whether n is greater than any type variable 
    9.76 -   occuring in the type structure *)
    9.77 -constdefs
    9.78 -        new_tv :: [nat,'a::type_struct] => bool
    9.79 -        "new_tv n ts == ! m. m:free_tv ts --> m<n"
    9.80 -
    9.81 -(* unification algorithm mgu *)
    9.82 -consts
    9.83 -        mgu :: [typ,typ] => subst maybe
    9.84 -rules
    9.85 -        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
    9.86 -        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
    9.87 -                  ? r. s = $r o u"
    9.88 -        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
    9.89 -        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
    9.90 -
    9.91 -end
    9.92 -
    10.1 --- a/src/HOL/W0/W.ML	Mon Feb 25 20:51:48 2002 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,361 +0,0 @@
    10.4 -(* Title:     HOL/W0/W.ML
    10.5 -   ID:        $Id$
    10.6 -   Author:    Dieter Nazareth and Tobias Nipkow
    10.7 -   Copyright  1995 TU Muenchen
    10.8 -
    10.9 -Correctness and completeness of type inference algorithm W
   10.10 -*)
   10.11 -
   10.12 -Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
   10.13 -
   10.14 -Delsimps (ex_simps @ all_simps);
   10.15 -
   10.16 -(* correctness of W with respect to has_type *)
   10.17 -Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
   10.18 -by (induct_tac "e" 1);
   10.19 -(* case Var n *)
   10.20 -by (Asm_simp_tac 1);
   10.21 -(* case Abs e *)
   10.22 -by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
   10.23 -                        addsplits [split_bind]) 1);
   10.24 -by (strip_tac 1);
   10.25 -by (dtac sym 1);
   10.26 -by (fast_tac (HOL_cs addss simpset()) 1);
   10.27 -(* case App e1 e2 *)
   10.28 -by (simp_tac (simpset() addsplits [split_bind]) 1);
   10.29 -by (strip_tac 1);
   10.30 -by ( rename_tac "sa ta na sb tb nb sc" 1);
   10.31 -by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
   10.32 -by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
   10.33 -by (rtac (app_subst_Fun RS subst) 1);
   10.34 -by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
   10.35 -by (Asm_full_simp_tac 1);
   10.36 -by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym,o_def]) 1);
   10.37 -by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
   10.38 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   10.39 -by (asm_full_simp_tac (simpset() addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
   10.40 -qed_spec_mp "W_correct";
   10.41 -
   10.42 -val has_type_casesE = map has_type.mk_cases
   10.43 -        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
   10.44 -
   10.45 -(* the resulting type variable is always greater or equal than the given one *)
   10.46 -Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   10.47 -by (induct_tac "e" 1);
   10.48 -(* case Var(n) *)
   10.49 -by (Clarsimp_tac 1);
   10.50 -(* case Abs e *)
   10.51 -by (simp_tac (simpset() addsplits [split_bind]) 1);
   10.52 -by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   10.53 -(* case App e1 e2 *)
   10.54 -by (simp_tac (simpset() addsplits [split_bind]) 1);
   10.55 -by (strip_tac 1);
   10.56 -by (rename_tac "s t na sa ta nb sb" 1);
   10.57 -by (eres_inst_tac [("x","a")] allE 1);
   10.58 -by (eres_inst_tac [("x","n")] allE 1);
   10.59 -by (eres_inst_tac [("x","$ s a")] allE 1);
   10.60 -by (eres_inst_tac [("x","s")] allE 1);
   10.61 -by (eres_inst_tac [("x","t")] allE 1);
   10.62 -by (eres_inst_tac [("x","na")] allE 1);
   10.63 -by (eres_inst_tac [("x","na")] allE 1);
   10.64 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   10.65 -by (eres_inst_tac [("x","sa")] allE 1);
   10.66 -by (eres_inst_tac [("x","ta")] allE 1);
   10.67 -by (eres_inst_tac [("x","nb")] allE 1);
   10.68 -by (Asm_full_simp_tac 1);
   10.69 -qed_spec_mp "W_var_ge";
   10.70 -
   10.71 -Addsimps [W_var_ge];
   10.72 -
   10.73 -Goal "Ok (s,t,m) = W e a n ==> n<=m";
   10.74 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   10.75 -qed "W_var_geD";
   10.76 -
   10.77 -
   10.78 -(* auxiliary lemma *)
   10.79 -goal Maybe.thy "(y = Ok x) = (Ok x = y)";
   10.80 -by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   10.81 -qed "rotate_Ok";
   10.82 -
   10.83 -
   10.84 -(* resulting type variable is new *)
   10.85 -Goal "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
   10.86 -\                 new_tv m s & new_tv m t";
   10.87 -by (induct_tac "e" 1);
   10.88 -(* case Var n *)
   10.89 -  by (Clarsimp_tac 1);
   10.90 -  by (force_tac (claset() addEs [list_ball_nth],
   10.91 -		simpset() addsimps [id_subst_def,new_tv_list,new_tv_subst])1);
   10.92 -(* case Abs e *)
   10.93 - by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
   10.94 -    addsplits [split_bind]) 1);
   10.95 - by (strip_tac 1);
   10.96 - by (eres_inst_tac [("x","Suc n")] allE 1);
   10.97 - by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
   10.98 - by (fast_tac (HOL_cs addss (simpset()
   10.99 -              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
  10.100 -
  10.101 -(* case App e1 e2 *)
  10.102 -by (simp_tac (simpset() addsplits [split_bind]) 1);
  10.103 -by (strip_tac 1);
  10.104 -by (rename_tac "s t na sa ta nb sb" 1);
  10.105 -by (eres_inst_tac [("x","n")] allE 1);
  10.106 -by (eres_inst_tac [("x","a")] allE 1);
  10.107 -by (eres_inst_tac [("x","s")] allE 1);
  10.108 -by (eres_inst_tac [("x","t")] allE 1);
  10.109 -by (eres_inst_tac [("x","na")] allE 1);
  10.110 -by (eres_inst_tac [("x","na")] allE 1);
  10.111 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
  10.112 -by (eres_inst_tac [("x","$ s a")] allE 1);
  10.113 -by (eres_inst_tac [("x","sa")] allE 1);
  10.114 -by (eres_inst_tac [("x","ta")] allE 1);
  10.115 -by (eres_inst_tac [("x","nb")] allE 1);
  10.116 -by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Ok]) 1);
  10.117 -by (rtac conjI 1);
  10.118 -by (rtac new_tv_subst_comp_2 1);
  10.119 -by (rtac new_tv_subst_comp_2 1);
  10.120 -by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
  10.121 -by (res_inst_tac [("n","na")] new_tv_subst_le 1); 
  10.122 -by (asm_full_simp_tac (simpset() addsimps [rotate_Ok]) 1);
  10.123 -by (Asm_simp_tac 1);
  10.124 -by (fast_tac (HOL_cs addDs [W_var_geD] addIs
  10.125 -     [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
  10.126 -    1);
  10.127 -by (etac (sym RS mgu_new) 1);
  10.128 -by (best_tac (HOL_cs addDs [W_var_geD] 
  10.129 -                     addIs [new_tv_subst_te,new_tv_list_le,
  10.130 -                            new_tv_subst_tel,
  10.131 -                            lessI RS less_imp_le RS new_tv_le,
  10.132 -                            lessI RS less_imp_le RS new_tv_subst_le,
  10.133 -                            new_tv_le]) 1);
  10.134 -by (fast_tac (HOL_cs addDs [W_var_geD] 
  10.135 -                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
  10.136 -                     addss (simpset())) 1);
  10.137 -by (rtac (lessI RS new_tv_subst_var) 1);
  10.138 -by (etac (sym RS mgu_new) 1);
  10.139 -by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
  10.140 -                     addDs [W_var_geD]
  10.141 -                     addIs [new_tv_list_le,
  10.142 -                            new_tv_subst_tel,
  10.143 -                            lessI RS less_imp_le RS new_tv_subst_le,
  10.144 -                            new_tv_le] 
  10.145 -                     addss simpset()) 1);
  10.146 -by (fast_tac (HOL_cs addDs [W_var_geD] 
  10.147 -                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
  10.148 -                     addss (simpset())) 1);
  10.149 -qed_spec_mp "new_tv_W";
  10.150 -
  10.151 -
  10.152 -Goal "!n a s t m v. W e a n = Ok (s,t,m) -->            \
  10.153 -\         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
  10.154 -by (induct_tac "e" 1);
  10.155 -(* case Var n *)
  10.156 -by (Clarsimp_tac 1);
  10.157 -by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list])1);
  10.158 -
  10.159 -(* case Abs e *)
  10.160 -by (asm_full_simp_tac (simpset() addsimps
  10.161 -    [free_tv_subst] addsplits [split_bind]) 1);
  10.162 -by (strip_tac 1);
  10.163 -by (rename_tac "s t n1 v" 1);
  10.164 -by (eres_inst_tac [("x","Suc n")] allE 1);
  10.165 -by (eres_inst_tac [("x","TVar n # a")] allE 1);
  10.166 -by (eres_inst_tac [("x","s")] allE 1);
  10.167 -by (eres_inst_tac [("x","t")] allE 1);
  10.168 -by (eres_inst_tac [("x","n1")] allE 1);
  10.169 -by (eres_inst_tac [("x","v")] allE 1);
  10.170 -by (force_tac (claset() addSEs [allE] addIs [cod_app_subst], simpset()) 1);
  10.171 -(** LEVEL 13 **)
  10.172 -(* case App e1 e2 *)
  10.173 -by (simp_tac (simpset() addsplits [split_bind]) 1);
  10.174 -by (strip_tac 1);
  10.175 -by (rename_tac "s t n1 s1 t1 n2 s3 v" 1);
  10.176 -by (eres_inst_tac [("x","n")] allE 1);
  10.177 -by (eres_inst_tac [("x","a")] allE 1);
  10.178 -by (eres_inst_tac [("x","s")] allE 1);
  10.179 -by (eres_inst_tac [("x","t")] allE 1);
  10.180 -by (eres_inst_tac [("x","n1")] allE 1);
  10.181 -by (eres_inst_tac [("x","n1")] allE 1);
  10.182 -by (eres_inst_tac [("x","v")] allE 1);
  10.183 -(** LEVEL 23 **)
  10.184 -(* second case *)
  10.185 -by (eres_inst_tac [("x","$ s a")] allE 1);
  10.186 -by (eres_inst_tac [("x","s1")] allE 1);
  10.187 -by (eres_inst_tac [("x","t1")] allE 1);
  10.188 -by (eres_inst_tac [("x","n2")] allE 1);
  10.189 -by (eres_inst_tac [("x","v")] allE 1);
  10.190 -by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
  10.191 - by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1);
  10.192 - by (dtac W_var_geD 1);
  10.193 - by (dtac W_var_geD 1);
  10.194 - by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
  10.195 -(** LEVEL 33 **)
  10.196 - by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
  10.197 -    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
  10.198 -    subsetD]
  10.199 -  addEs [UnE] 
  10.200 -  addss simpset()) 1);
  10.201 -by (Asm_full_simp_tac 1); 
  10.202 -by (dtac (sym RS W_var_geD) 1);
  10.203 -by (dtac (sym RS W_var_geD) 1);
  10.204 -by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
  10.205 -by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
  10.206 -                            free_tv_app_subst_te RS subsetD,
  10.207 -                            free_tv_app_subst_tel RS subsetD,
  10.208 -                            less_le_trans,subsetD]
  10.209 -                     addSEs [UnE]
  10.210 -                     addss (simpset() setSolver unsafe_solver)) 1);
  10.211 -(* builtin arithmetic in simpset messes things up *)
  10.212 -qed_spec_mp "free_tv_W"; 
  10.213 -
  10.214 -(* Completeness of W w.r.t. has_type *)
  10.215 -Goal "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
  10.216 -\             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
  10.217 -\                     (? r. $s' a = $r ($s a) & t' = $r t))";
  10.218 -by (induct_tac "e" 1);
  10.219 -(* case Var n *)
  10.220 -by (strip_tac 1);
  10.221 -by (simp_tac (simpset() addcongs [conj_cong]) 1);
  10.222 -by (eresolve_tac has_type_casesE 1); 
  10.223 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1);
  10.224 -by (res_inst_tac [("x","s'")] exI 1);
  10.225 -by (Asm_simp_tac 1);
  10.226 -
  10.227 -(** LEVEL 7 **)
  10.228 -(* case Abs e *)
  10.229 -by (strip_tac 1);
  10.230 -by (eresolve_tac has_type_casesE 1);
  10.231 -by (eres_inst_tac [("x","%x. if x=n then t1 else (s' x)")] allE 1);
  10.232 -by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
  10.233 -by (eres_inst_tac [("x","t2")] allE 1);
  10.234 -by (eres_inst_tac [("x","Suc n")] allE 1);
  10.235 -by (fast_tac (HOL_cs addss (simpset() addcongs [conj_cong]
  10.236 -                            addsplits [split_bind])) 1);
  10.237 -
  10.238 -(** LEVEL 14 **)
  10.239 -(* case App e1 e2 *)
  10.240 -by (strip_tac 1);
  10.241 -by (eresolve_tac has_type_casesE 1);
  10.242 -by (eres_inst_tac [("x","s'")] allE 1);
  10.243 -by (eres_inst_tac [("x","a")] allE 1);
  10.244 -by (eres_inst_tac [("x","t2 -> t'")] allE 1);
  10.245 -by (eres_inst_tac [("x","n")] allE 1);
  10.246 -by (safe_tac HOL_cs);
  10.247 -by (eres_inst_tac [("x","r")] allE 1);
  10.248 -by (eres_inst_tac [("x","$ s a")] allE 1);
  10.249 -by (eres_inst_tac [("x","t2")] allE 1);
  10.250 -by (eres_inst_tac [("x","m")] allE 1);
  10.251 -by (Asm_full_simp_tac 1);
  10.252 -by (safe_tac HOL_cs);
  10.253 -by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
  10.254 -                            conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
  10.255 -
  10.256 -(** LEVEL 28 **)
  10.257 -by (subgoal_tac
  10.258 -  "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
  10.259 -\        else ra x)) ($ sa t) = \
  10.260 -\  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
  10.261 -\        else ra x)) (ta -> (TVar ma))" 1);
  10.262 -by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
  10.263 -\   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
  10.264 -    ("s","($ ra ta) -> t'")] ssubst 2);
  10.265 -by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2);
  10.266 -by (rtac eq_free_eq_subst_te 2);  
  10.267 -by (strip_tac 2);
  10.268 -by (subgoal_tac "na ~=ma" 2);
  10.269 -by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
  10.270 -                            new_tv_not_free_tv,new_tv_le]) 3);
  10.271 -(** LEVEL 35 **)
  10.272 -by (case_tac "na:free_tv sa" 2);
  10.273 -(* na ~: free_tv sa *)
  10.274 -by (ftac not_free_impl_id 3);
  10.275 -by (Asm_simp_tac 3);
  10.276 -(* na : free_tv sa *)
  10.277 -by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  10.278 -by (dtac eq_subst_tel_eq_free 2);
  10.279 -by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  10.280 -by (Asm_simp_tac 2); 
  10.281 -by (case_tac "na:dom sa" 2);
  10.282 -(* na ~: dom sa *)
  10.283 -(** LEVEL 43 **)
  10.284 -by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
  10.285 -(* na : dom sa *)
  10.286 -by (rtac eq_free_eq_subst_te 2);
  10.287 -by (strip_tac 2);
  10.288 -by (subgoal_tac "nb ~= ma" 2);
  10.289 -by ((ftac new_tv_W 3) THEN (atac 3));
  10.290 -by (etac conjE 3);
  10.291 -by (dtac new_tv_subst_tel 3);
  10.292 -by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
  10.293 -by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
  10.294 -              (simpset() addsimps [cod_def,free_tv_subst])) 3);
  10.295 -by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
  10.296 -
  10.297 -(** LEVEL 53 **)
  10.298 -by (Simp_tac 2);  
  10.299 -by (rtac eq_free_eq_subst_te 2);
  10.300 -by (strip_tac 2 );
  10.301 -by (subgoal_tac "na ~= ma" 2);
  10.302 -by ((ftac new_tv_W 3) THEN (atac 3));
  10.303 -by (etac conjE 3);
  10.304 -by (dtac (sym RS W_var_geD) 3);
  10.305 -by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
  10.306 -by (case_tac "na: free_tv t - free_tv sa" 2);
  10.307 -(** LEVEL 62 **)
  10.308 -(* case na ~: free_tv t - free_tv sa *)
  10.309 -by (Asm_full_simp_tac 3);
  10.310 -(* case na : free_tv t - free_tv sa *)
  10.311 -by (Asm_full_simp_tac 2);
  10.312 -by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  10.313 -by (dtac eq_subst_tel_eq_free 2);
  10.314 -by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  10.315 -by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2);
  10.316 -by (Fast_tac 2);
  10.317 -(** LEVEL 69 **)
  10.318 -by (asm_simp_tac (simpset() addsplits [split_bind]) 1);
  10.319 -by (safe_tac HOL_cs);
  10.320 -by (dtac mgu_Ok 1);
  10.321 -by ( fast_tac (HOL_cs addss simpset()) 1);
  10.322 -by ((dtac mgu_mg 1) THEN (atac 1));
  10.323 -by (etac exE 1);
  10.324 -by (res_inst_tac [("x","rb")] exI 1);
  10.325 -by (rtac conjI 1);
  10.326 -by (dres_inst_tac [("x","ma")] fun_cong 2);
  10.327 -by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2);
  10.328 -by (simp_tac (simpset() addsimps [o_def,subst_comp_tel RS sym]) 1);
  10.329 -(** LEVEL 80 **)
  10.330 -by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
  10.331 -by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
  10.332 -by (dres_inst_tac [("s","Ok ?X")] sym 1);
  10.333 -by (rtac eq_free_eq_subst_tel 1);
  10.334 -by ( safe_tac HOL_cs );
  10.335 -by (subgoal_tac "ma ~= na" 1);
  10.336 -by ((ftac new_tv_W 2) THEN (atac 2));
  10.337 -by (etac conjE 2);
  10.338 -by (dtac new_tv_subst_tel 2);
  10.339 -by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
  10.340 -by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2);
  10.341 -(** LEVEL 100 **)
  10.342 -by (etac conjE 2);
  10.343 -by (dtac (free_tv_app_subst_tel RS subsetD) 2);
  10.344 -by (fast_tac (set_cs addDs [sym RS W_var_geD,new_tv_list_le,codD,
  10.345 -    new_tv_not_free_tv]) 2);
  10.346 -by (case_tac "na: free_tv t - free_tv sa" 1);
  10.347 -(* case na ~: free_tv t - free_tv sa *)
  10.348 -by (Asm_full_simp_tac 2);
  10.349 -(* case na : free_tv t - free_tv sa *)
  10.350 -by (Asm_full_simp_tac 1);
  10.351 -by (dtac (free_tv_app_subst_tel RS subsetD) 1);
  10.352 -by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
  10.353 -                            eq_subst_tel_eq_free] 
  10.354 -       addss ((simpset() addsimps [free_tv_subst,dom_def]))) 1);
  10.355 -(** LEVEL 106 **)
  10.356 -by (Fast_tac 1);
  10.357 -qed_spec_mp "W_complete_lemma";
  10.358 -
  10.359 -Goal "[] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
  10.360 -\                                 (? r. t' = $r t))";
  10.361 -by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
  10.362 -                W_complete_lemma 1);
  10.363 -by (ALLGOALS Asm_full_simp_tac);
  10.364 -qed "W_complete";
    11.1 --- a/src/HOL/W0/W.thy	Mon Feb 25 20:51:48 2002 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,28 +0,0 @@
    11.4 -(* Title:     HOL/MiniML/W.thy
    11.5 -   ID:        $Id$
    11.6 -   Author:    Dieter Nazareth and Tobias Nipkow
    11.7 -   Copyright  1995 TU Muenchen
    11.8 -
    11.9 -Type inference algorithm W
   11.10 -*)
   11.11 -
   11.12 -W = MiniML + 
   11.13 -
   11.14 -types 
   11.15 -        result_W = "(subst * typ * nat)maybe"
   11.16 -
   11.17 -(* type inference algorithm W *)
   11.18 -consts
   11.19 -        W :: [expr, typ list, nat] => result_W
   11.20 -
   11.21 -primrec
   11.22 -  "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
   11.23 -                    else Fail)"
   11.24 -  "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
   11.25 -                     Ok(s, (s n) -> t, m) )"
   11.26 -  "W (App e1 e2) a n =
   11.27 -                 ( (s1,t1,m1) := W e1 a n;
   11.28 -                   (s2,t2,m2) := W e2 ($s1 a) m1;
   11.29 -                   u := mgu ($s2 t1) (t2 -> (TVar m2));
   11.30 -                   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
   11.31 -end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/W0/W0.thy	Tue Feb 26 00:19:04 2002 +0100
    12.3 @@ -0,0 +1,947 @@
    12.4 +(*  Title:      HOL/W0/W0.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, and Markus Wenzel
    12.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.8 +*)
    12.9 +
   12.10 +theory W0 = Main:
   12.11 +
   12.12 +section {* Universal error monad *}
   12.13 +
   12.14 +datatype 'a maybe = Ok 'a | Fail
   12.15 +
   12.16 +constdefs
   12.17 +  bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60)
   12.18 +  "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
   12.19 +
   12.20 +syntax
   12.21 +  "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
   12.22 +translations
   12.23 +  "P := E; F" == "E \<bind> (\<lambda>P. F)"
   12.24 +
   12.25 +lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)"
   12.26 +  by (simp add: bind_def)
   12.27 +
   12.28 +lemma bind_Fail [simp]: "Fail \<bind> f = Fail"
   12.29 +  by (simp add: bind_def)
   12.30 +
   12.31 +lemma split_bind:
   12.32 +    "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))"
   12.33 +  by (induct res) simp_all
   12.34 +
   12.35 +lemma split_bind_asm:
   12.36 +  "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))"
   12.37 +  by (simp split: split_bind)
   12.38 +
   12.39 +lemmas bind_splits = split_bind split_bind_asm
   12.40 +
   12.41 +lemma bind_eq_Fail [simp]:
   12.42 +  "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> f p = Fail))"
   12.43 +  by (simp split: split_bind)
   12.44 +
   12.45 +lemma rotate_Ok: "(y = Ok x) = (Ok x = y)"
   12.46 +  by (rule eq_sym_conv)
   12.47 +
   12.48 +
   12.49 +section {* MiniML-types and type substitutions *}
   12.50 +
   12.51 +axclass type_struct \<subseteq> type
   12.52 +  -- {* new class for structures containing type variables *}
   12.53 +
   12.54 +datatype "typ" = TVar nat | TFun "typ" "typ"    (infixr "->" 70)
   12.55 +  -- {* type expressions *}
   12.56 +
   12.57 +types subst = "nat => typ"
   12.58 +  -- {* type variable substitution *}
   12.59 +
   12.60 +instance "typ" :: type_struct ..
   12.61 +instance list :: (type_struct) type_struct ..
   12.62 +instance fun :: (type, type_struct) type_struct ..
   12.63 +
   12.64 +
   12.65 +subsection {* Substitutions *}
   12.66 +
   12.67 +consts
   12.68 +  app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
   12.69 +  -- {* extension of substitution to type structures *}
   12.70 +primrec
   12.71 +  app_subst_TVar: "$s (TVar n) = s n"
   12.72 +  app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
   12.73 +
   12.74 +defs (overloaded)
   12.75 +  app_subst_list: "$s \<equiv> map ($s)"
   12.76 +
   12.77 +consts
   12.78 +  free_tv :: "'a::type_struct \<Rightarrow> nat set"
   12.79 +  -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
   12.80 +
   12.81 +primrec
   12.82 +  "free_tv (TVar m) = {m}"
   12.83 +  "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
   12.84 +
   12.85 +primrec
   12.86 +  "free_tv [] = {}"
   12.87 +  "free_tv (x # xs) = free_tv x \<union> free_tv xs"
   12.88 +
   12.89 +constdefs
   12.90 +  dom :: "subst \<Rightarrow> nat set"
   12.91 +  "dom s \<equiv> {n. s n \<noteq> TVar n}"
   12.92 +  -- {* domain of a substitution *}
   12.93 +
   12.94 +  cod :: "subst \<Rightarrow> nat set"
   12.95 +  "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
   12.96 +  -- {* codomain of a substitutions: the introduced variables *}
   12.97 +
   12.98 +defs
   12.99 +  free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
  12.100 +
  12.101 +text {*
  12.102 +  @{text "new_tv s n"} checks whether @{text n} is a new type variable
  12.103 +  wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
  12.104 +  than any type variable occuring in the type structure.
  12.105 +*}
  12.106 +
  12.107 +constdefs
  12.108 +  new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
  12.109 +  "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
  12.110 +
  12.111 +
  12.112 +subsubsection {* Identity substitution *}
  12.113 +
  12.114 +constdefs
  12.115 +  id_subst :: subst
  12.116 +  "id_subst \<equiv> \<lambda>n. TVar n"
  12.117 +
  12.118 +lemma app_subst_id_te [simp]:
  12.119 +  "$id_subst = (\<lambda>t::typ. t)"
  12.120 +  -- {* application of @{text id_subst} does not change type expression *}
  12.121 +proof
  12.122 +  fix t :: "typ"
  12.123 +  show "$id_subst t = t"
  12.124 +    by (induct t) (simp_all add: id_subst_def)
  12.125 +qed
  12.126 +
  12.127 +lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)"
  12.128 +  -- {* application of @{text id_subst} does not change list of type expressions *}
  12.129 +proof
  12.130 +  fix ts :: "typ list"
  12.131 +  show "$id_subst ts = ts"
  12.132 +    by (induct ts) (simp_all add: app_subst_list)
  12.133 +qed
  12.134 +
  12.135 +lemma o_id_subst [simp]: "$s o id_subst = s"
  12.136 +  by (rule ext) (simp add: id_subst_def)
  12.137 +
  12.138 +lemma dom_id_subst [simp]: "dom id_subst = {}"
  12.139 +  by (simp add: dom_def id_subst_def empty_def)
  12.140 +
  12.141 +lemma cod_id_subst [simp]: "cod id_subst = {}"
  12.142 +  by (simp add: cod_def)
  12.143 +
  12.144 +lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
  12.145 +  by (simp add: free_tv_subst)
  12.146 +
  12.147 +
  12.148 +lemma cod_app_subst [simp]:
  12.149 +  assumes free: "v \<in> free_tv (s n)"
  12.150 +    and neq: "v \<noteq> n"
  12.151 +  shows "v \<in> cod s"
  12.152 +proof -
  12.153 +  have "s n \<noteq> TVar n"
  12.154 +  proof
  12.155 +    assume "s n = TVar n"
  12.156 +    with free have "v = n" by simp
  12.157 +    with neq show False ..
  12.158 +  qed
  12.159 +  with free show ?thesis
  12.160 +    by (auto simp add: dom_def cod_def)
  12.161 +qed
  12.162 +
  12.163 +lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t"
  12.164 +  -- {* composition of substitutions *}
  12.165 +  by (induct t) simp_all
  12.166 +
  12.167 +lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts"
  12.168 +  by (induct ts) (simp_all add: app_subst_list subst_comp_te)
  12.169 +
  12.170 +
  12.171 +lemma app_subst_Nil [simp]: "$s [] = []"
  12.172 +  by (simp add: app_subst_list)
  12.173 +
  12.174 +lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
  12.175 +  by (simp add: app_subst_list)
  12.176 +
  12.177 +lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
  12.178 +  by (simp add: new_tv_def)
  12.179 +
  12.180 +lemma new_tv_Fun [simp]:
  12.181 +  "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
  12.182 +  by (auto simp add: new_tv_def)
  12.183 +
  12.184 +lemma new_tv_Nil [simp]: "new_tv n []"
  12.185 +  by (simp add: new_tv_def)
  12.186 +
  12.187 +lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)"
  12.188 +  by (auto simp add: new_tv_def)
  12.189 +
  12.190 +lemma new_tv_id_subst [simp]: "new_tv n id_subst"
  12.191 +  by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
  12.192 +
  12.193 +lemma new_tv_subst:
  12.194 +  "new_tv n s =
  12.195 +    ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
  12.196 +     (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
  12.197 +  apply (unfold new_tv_def)
  12.198 +  apply (tactic "safe_tac HOL_cs")
  12.199 +  -- {* @{text \<Longrightarrow>} *}
  12.200 +    apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
  12.201 +      addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
  12.202 +   apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
  12.203 +    apply (tactic "safe_tac HOL_cs")
  12.204 +     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
  12.205 +       addsimps [thm "free_tv_subst"])) 1 *})
  12.206 +    apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
  12.207 +    apply simp
  12.208 +   apply (tactic {* fast_tac (set_cs addss (simpset()
  12.209 +     addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
  12.210 +  -- {* @{text \<Longleftarrow>} *}
  12.211 +  apply (unfold free_tv_subst cod_def dom_def)
  12.212 +  apply (tactic "safe_tac set_cs")
  12.213 +   apply (cut_tac m = m and n = n in less_linear)
  12.214 +   apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
  12.215 +  apply (cut_tac m = ma and n = n in less_linear)
  12.216 +  apply (fast intro!: less_or_eq_imp_le)
  12.217 +  done
  12.218 +
  12.219 +lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
  12.220 +  by (induct x) simp_all
  12.221 +
  12.222 +lemma subst_te_new_tv [simp]:
  12.223 +  "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
  12.224 +  -- {* substitution affects only variables occurring freely *}
  12.225 +  by (induct t) simp_all
  12.226 +
  12.227 +lemma subst_tel_new_tv [simp]:
  12.228 +  "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
  12.229 +  by (induct ts) simp_all
  12.230 +
  12.231 +lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
  12.232 +  -- {* all greater variables are also new *}
  12.233 +proof (induct t)
  12.234 +  case (TVar n)
  12.235 +  thus ?case by (auto intro: less_le_trans)
  12.236 +next
  12.237 +  case TFun
  12.238 +  thus ?case by simp
  12.239 +qed
  12.240 +
  12.241 +lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
  12.242 +  by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
  12.243 +
  12.244 +lemma new_tv_list_le:
  12.245 +  "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
  12.246 +proof (induct ts)
  12.247 +  case Nil
  12.248 +  thus ?case by simp
  12.249 +next
  12.250 +  case Cons
  12.251 +  thus ?case by (auto intro: new_tv_le)
  12.252 +qed
  12.253 +
  12.254 +lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
  12.255 +  by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
  12.256 +
  12.257 +lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
  12.258 +  apply (simp add: new_tv_subst)
  12.259 +  apply clarify
  12.260 +  apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
  12.261 +    apply clarify
  12.262 +    apply (simp_all add: new_tv_le)
  12.263 +  done
  12.264 +
  12.265 +lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
  12.266 +  by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
  12.267 +
  12.268 +lemma new_tv_subst_var:
  12.269 +    "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
  12.270 +  -- {* @{text new_tv} property remains if a substitution is applied *}
  12.271 +  by (simp add: new_tv_subst)
  12.272 +
  12.273 +lemma new_tv_subst_te [simp]:
  12.274 +    "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
  12.275 +  by (induct t) (auto simp add: new_tv_subst)
  12.276 +
  12.277 +lemma new_tv_subst_tel [simp]:
  12.278 +    "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
  12.279 +  by (induct ts) (fastsimp simp add: new_tv_subst)+
  12.280 +
  12.281 +lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
  12.282 +  -- {* auxilliary lemma *}
  12.283 +  by (simp add: new_tv_list)
  12.284 +
  12.285 +lemma new_tv_subst_comp_1 [simp]:
  12.286 +    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
  12.287 +  -- {* composition of substitutions preserves @{text new_tv} proposition *}
  12.288 +  by (simp add: new_tv_subst)
  12.289 +
  12.290 +lemma new_tv_subst_comp_2 [simp]:
  12.291 +    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
  12.292 +  by (simp add: new_tv_subst)
  12.293 +
  12.294 +lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
  12.295 +  -- {* new type variables do not occur freely in a type structure *}
  12.296 +  by (auto simp add: new_tv_def)
  12.297 +
  12.298 +lemma ftv_mem_sub_ftv_list [simp]:
  12.299 +    "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
  12.300 +  by (induct ts) auto
  12.301 +
  12.302 +text {*
  12.303 +  If two substitutions yield the same result if applied to a type
  12.304 +  structure the substitutions coincide on the free type variables
  12.305 +  occurring in the type structure.
  12.306 +*}
  12.307 +
  12.308 +lemma eq_subst_te_eq_free:
  12.309 +    "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
  12.310 +  by (induct t) auto
  12.311 +
  12.312 +lemma eq_free_eq_subst_te:
  12.313 +    "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
  12.314 +  by (induct t) auto
  12.315 +
  12.316 +lemma eq_subst_tel_eq_free:
  12.317 +    "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
  12.318 +  by (induct ts) (auto intro: eq_subst_te_eq_free)
  12.319 +
  12.320 +lemma eq_free_eq_subst_tel:
  12.321 +    "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
  12.322 +  by (induct ts) (auto intro: eq_free_eq_subst_te)
  12.323 +
  12.324 +text {*
  12.325 +  \medskip Some useful lemmas.
  12.326 +*}
  12.327 +
  12.328 +lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
  12.329 +  by (simp add: free_tv_subst)
  12.330 +
  12.331 +lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
  12.332 +  by (simp add: free_tv_subst dom_def)
  12.333 +
  12.334 +lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
  12.335 +  by (unfold new_tv_def) fast
  12.336 +
  12.337 +lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
  12.338 +  by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
  12.339 +
  12.340 +lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
  12.341 +  by (induct t) (auto simp add: free_tv_subst_var)
  12.342 +
  12.343 +lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
  12.344 +  apply (induct ts)
  12.345 +   apply simp
  12.346 +  apply (cut_tac free_tv_app_subst_te)
  12.347 +  apply fastsimp
  12.348 +  done
  12.349 +
  12.350 +lemma free_tv_comp_subst:
  12.351 +    "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
  12.352 +  apply (unfold free_tv_subst dom_def)
  12.353 +  apply (tactic {*
  12.354 +    fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
  12.355 +    thm "free_tv_subst_var" RS subsetD]
  12.356 +    addss (simpset() delsimps bex_simps
  12.357 +    addsimps [thm "cod_def", thm "dom_def"])) 1 *})
  12.358 +  done
  12.359 +
  12.360 +
  12.361 +subsection {* Most general unifiers *}
  12.362 +
  12.363 +consts
  12.364 +  mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
  12.365 +axioms
  12.366 +  mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
  12.367 +  mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
  12.368 +  mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
  12.369 +  mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
  12.370 +
  12.371 +lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
  12.372 +  -- {* @{text mgu} does not introduce new type variables *}
  12.373 +  by (unfold new_tv_def) (blast dest: mgu_free)
  12.374 +
  12.375 +
  12.376 +section {* Mini-ML with type inference rules *}
  12.377 +
  12.378 +datatype
  12.379 +  expr = Var nat | Abs expr | App expr expr
  12.380 +
  12.381 +
  12.382 +text {* Type inference rules. *}
  12.383 +
  12.384 +consts
  12.385 +  has_type :: "(typ list \<times> expr \<times> typ) set"
  12.386 +
  12.387 +syntax
  12.388 +  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
  12.389 +    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
  12.390 +translations
  12.391 +  "a |- e :: t" == "(a, e, t) \<in> has_type"
  12.392 +
  12.393 +inductive has_type
  12.394 +  intros
  12.395 +    Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
  12.396 +    Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
  12.397 +    App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
  12.398 +      \<Longrightarrow> a |- App e1 e2 :: t1"
  12.399 +
  12.400 +
  12.401 +text {* Type assigment is closed wrt.\ substitution. *}
  12.402 +
  12.403 +lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
  12.404 +proof -
  12.405 +  assume "a |- e :: t"
  12.406 +  thus ?thesis (is "?P a e t")
  12.407 +  proof induct
  12.408 +    case (Var a n)
  12.409 +    hence "n < length (map ($ s) a)" by simp
  12.410 +    hence "map ($ s) a |- Var n :: map ($ s) a ! n"
  12.411 +      by (rule has_type.Var)
  12.412 +    also have "map ($ s) a ! n = $ s (a ! n)"
  12.413 +      by (rule nth_map)
  12.414 +    also have "map ($ s) a = $ s a"
  12.415 +      by (simp only: app_subst_list)
  12.416 +    finally show "?P a (Var n) (a ! n)" .
  12.417 +  next
  12.418 +    case (Abs a e t1 t2)
  12.419 +    hence "$ s t1 # map ($ s) a |- e :: $ s t2"
  12.420 +      by (simp add: app_subst_list)
  12.421 +    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
  12.422 +      by (rule has_type.Abs)
  12.423 +    thus "?P a (Abs e) (t1 -> t2)"
  12.424 +      by (simp add: app_subst_list)
  12.425 +  next
  12.426 +    case App
  12.427 +    thus ?case by (simp add: has_type.App)
  12.428 +  qed
  12.429 +qed
  12.430 +
  12.431 +
  12.432 +section {* Correctness and completeness of the type inference algorithm @{text \<W>} *}
  12.433 +
  12.434 +consts
  12.435 +  W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
  12.436 +
  12.437 +primrec
  12.438 +  "\<W> (Var i) a n =
  12.439 +    (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
  12.440 +  "\<W> (Abs e) a n =
  12.441 +    ((s, t, m) := \<W> e (TVar n # a) (Suc n);
  12.442 +     Ok (s, (s n) -> t, m))"
  12.443 +  "\<W> (App e1 e2) a n =
  12.444 +    ((s1, t1, m1) := \<W> e1 a n;
  12.445 +     (s2, t2, m2) := \<W> e2 ($s1 a) m1;
  12.446 +     u := mgu ($ s2 t1) (t2 -> TVar m2);
  12.447 +     Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
  12.448 +
  12.449 +theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
  12.450 +  (is "PROP ?P e")
  12.451 +proof (induct e)
  12.452 +  fix a s t m n
  12.453 +  {
  12.454 +    fix i
  12.455 +    assume "Ok (s, t, m) = \<W> (Var i) a n"
  12.456 +    thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
  12.457 +  next
  12.458 +    fix e assume hyp: "PROP ?P e"
  12.459 +    assume "Ok (s, t, m) = \<W> (Abs e) a n"
  12.460 +    then obtain t' where "t = s n -> t'"
  12.461 +        and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
  12.462 +      by (auto split: bind_splits)
  12.463 +    with hyp show "$s a |- Abs e :: t"
  12.464 +      by (force intro: has_type.Abs)
  12.465 +  next
  12.466 +    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
  12.467 +    assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
  12.468 +    then obtain s1 t1 n1 s2 t2 n2 u where
  12.469 +          s: "s = $u o $s2 o s1"
  12.470 +        and t: "t = u n2"
  12.471 +        and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
  12.472 +        and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
  12.473 +        and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
  12.474 +      by (auto split: bind_splits simp: that)
  12.475 +    show "$s a |- App e1 e2 :: t"
  12.476 +    proof (rule has_type.App)
  12.477 +      from s have s': "$u ($s2 ($s1 a)) = $s a"
  12.478 +        by (simp add: subst_comp_tel o_def)
  12.479 +      show "$s a |- e1 :: $u t2 -> t"
  12.480 +      proof -
  12.481 +        from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
  12.482 +        hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
  12.483 +          by (intro has_type_subst_closed)
  12.484 +        with s' t mgu_ok show ?thesis by simp
  12.485 +      qed
  12.486 +      show "$s a |- e2 :: $u t2"
  12.487 +      proof -
  12.488 +        from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
  12.489 +        hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
  12.490 +          by (rule has_type_subst_closed)
  12.491 +        with s' show ?thesis by simp
  12.492 +      qed
  12.493 +    qed
  12.494 +  }
  12.495 +qed
  12.496 +
  12.497 +
  12.498 +inductive_cases has_type_casesE:
  12.499 +  "s |- Var n :: t"
  12.500 +  "s |- Abs e :: t"
  12.501 +  "s |- App e1 e2 ::t"
  12.502 +
  12.503 +
  12.504 +lemmas [simp] = Suc_le_lessD
  12.505 +  and [simp del] = less_imp_le ex_simps all_simps
  12.506 +
  12.507 +lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
  12.508 +  -- {* the resulting type variable is always greater or equal than the given one *}
  12.509 +  apply (atomize (full))
  12.510 +  apply (induct e)
  12.511 +    txt {* case @{text "Var n"} *}
  12.512 +    apply clarsimp
  12.513 +   txt {* case @{text "Abs e"} *}
  12.514 +   apply (simp split add: split_bind)
  12.515 +   apply (fast dest: Suc_leD)
  12.516 +  txt {* case @{text "App e1 e2"} *}
  12.517 +  apply (simp (no_asm) split add: split_bind)
  12.518 +  apply (intro strip)
  12.519 +  apply (rename_tac s t na sa ta nb sb)
  12.520 +  apply (erule_tac x = a in allE)
  12.521 +  apply (erule_tac x = n in allE)
  12.522 +  apply (erule_tac x = "$s a" in allE)
  12.523 +  apply (erule_tac x = s in allE)
  12.524 +  apply (erule_tac x = t in allE)
  12.525 +  apply (erule_tac x = na in allE)
  12.526 +  apply (erule_tac x = na in allE)
  12.527 +  apply (simp add: eq_sym_conv)
  12.528 +  done
  12.529 +
  12.530 +lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
  12.531 +  by (simp add: eq_sym_conv)
  12.532 +
  12.533 +lemma new_tv_W: "!!n a s t m.
  12.534 +  new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
  12.535 +  -- {* resulting type variable is new *}
  12.536 +  apply (atomize (full))
  12.537 +  apply (induct e)
  12.538 +    txt {* case @{text "Var n"} *}
  12.539 +    apply clarsimp
  12.540 +    apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
  12.541 +   txt {* case @{text "Abs e"} *}
  12.542 +   apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
  12.543 +   apply (intro strip)
  12.544 +   apply (erule_tac x = "Suc n" in allE)
  12.545 +   apply (erule_tac x = "TVar n # a" in allE)
  12.546 +   apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
  12.547 +  txt {* case @{text "App e1 e2"} *}
  12.548 +  apply (simp (no_asm) split add: split_bind)
  12.549 +  apply (intro strip)
  12.550 +  apply (rename_tac s t na sa ta nb sb)
  12.551 +  apply (erule_tac x = n in allE)
  12.552 +  apply (erule_tac x = a in allE)
  12.553 +  apply (erule_tac x = s in allE)
  12.554 +  apply (erule_tac x = t in allE)
  12.555 +  apply (erule_tac x = na in allE)
  12.556 +  apply (erule_tac x = na in allE)
  12.557 +  apply (simp add: eq_sym_conv)
  12.558 +  apply (erule_tac x = "$s a" in allE)
  12.559 +  apply (erule_tac x = sa in allE)
  12.560 +  apply (erule_tac x = ta in allE)
  12.561 +  apply (erule_tac x = nb in allE)
  12.562 +  apply (simp add: o_def rotate_Ok)
  12.563 +  apply (rule conjI)
  12.564 +   apply (rule new_tv_subst_comp_2)
  12.565 +    apply (rule new_tv_subst_comp_2)
  12.566 +     apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
  12.567 +     apply (rule_tac n = na in new_tv_subst_le)
  12.568 +      apply (simp add: rotate_Ok)
  12.569 +     apply (simp (no_asm_simp))
  12.570 +    apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
  12.571 +      lessI [THEN less_imp_le, THEN new_tv_subst_le])
  12.572 +   apply (erule sym [THEN mgu_new])
  12.573 +    apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
  12.574 +      lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
  12.575 +      new_tv_le)
  12.576 +   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
  12.577 +     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
  12.578 +     addss (simpset())) 1 *})
  12.579 +  apply (rule lessI [THEN new_tv_subst_var])
  12.580 +  apply (erule sym [THEN mgu_new])
  12.581 +    apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
  12.582 +      dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
  12.583 +        lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
  12.584 +  apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
  12.585 +    addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
  12.586 +    addss (simpset())) 1 *})
  12.587 +  done
  12.588 +
  12.589 +lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
  12.590 +    (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
  12.591 +  apply (atomize (full))
  12.592 +  apply (induct e)
  12.593 +    txt {* case @{text "Var n"} *}
  12.594 +    apply clarsimp
  12.595 +    apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
  12.596 +   txt {* case @{text "Abs e"} *}
  12.597 +   apply (simp add: free_tv_subst split add: split_bind)
  12.598 +   apply (intro strip)
  12.599 +   apply (rename_tac s t n1 v)
  12.600 +   apply (erule_tac x = "Suc n" in allE)
  12.601 +   apply (erule_tac x = "TVar n # a" in allE)
  12.602 +   apply (erule_tac x = s in allE)
  12.603 +   apply (erule_tac x = t in allE)
  12.604 +   apply (erule_tac x = n1 in allE)
  12.605 +   apply (erule_tac x = v in allE)
  12.606 +   apply (force elim!: allE intro: cod_app_subst)
  12.607 +  txt {* case @{text "App e1 e2"} *}
  12.608 +  apply (simp (no_asm) split add: split_bind)
  12.609 +  apply (intro strip)
  12.610 +  apply (rename_tac s t n1 s1 t1 n2 s3 v)
  12.611 +  apply (erule_tac x = n in allE)
  12.612 +  apply (erule_tac x = a in allE)
  12.613 +  apply (erule_tac x = s in allE)
  12.614 +  apply (erule_tac x = t in allE)
  12.615 +  apply (erule_tac x = n1 in allE)
  12.616 +  apply (erule_tac x = n1 in allE)
  12.617 +  apply (erule_tac x = v in allE)
  12.618 +  txt {* second case *}
  12.619 +  apply (erule_tac x = "$ s a" in allE)
  12.620 +  apply (erule_tac x = s1 in allE)
  12.621 +  apply (erule_tac x = t1 in allE)
  12.622 +  apply (erule_tac x = n2 in allE)
  12.623 +  apply (erule_tac x = v in allE)
  12.624 +  apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
  12.625 +   apply (simp add: rotate_Ok o_def)
  12.626 +   apply (drule W_var_geD)
  12.627 +   apply (drule W_var_geD)
  12.628 +   apply (frule less_le_trans, assumption)
  12.629 +   apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
  12.630 +     free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
  12.631 +  apply simp
  12.632 +  apply (drule sym [THEN W_var_geD])
  12.633 +  apply (drule sym [THEN W_var_geD])
  12.634 +  apply (frule less_le_trans, assumption)
  12.635 +  apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
  12.636 +    thm "free_tv_subst_var" RS subsetD,
  12.637 +    thm "free_tv_app_subst_te" RS subsetD,
  12.638 +    thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
  12.639 +    addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
  12.640 +      -- {* builtin arithmetic in simpset messes things up *}
  12.641 +  done
  12.642 +
  12.643 +text {*
  12.644 +  \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
  12.645 +*}
  12.646 +
  12.647 +lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
  12.648 +    (\<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))"
  12.649 +  apply (atomize (full))
  12.650 +  apply (induct e)
  12.651 +    txt {* case @{text "Var n"} *}
  12.652 +    apply (intro strip)
  12.653 +    apply (simp (no_asm) cong add: conj_cong)
  12.654 +    apply (erule has_type_casesE)
  12.655 +    apply (simp add: eq_sym_conv app_subst_list)
  12.656 +    apply (rule_tac x = s' in exI)
  12.657 +    apply simp
  12.658 +   txt {* case @{text "Abs e"} *}
  12.659 +   apply (intro strip)
  12.660 +   apply (erule has_type_casesE)
  12.661 +   apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
  12.662 +   apply (erule_tac x = "TVar n # a" in allE)
  12.663 +   apply (erule_tac x = t2 in allE)
  12.664 +   apply (erule_tac x = "Suc n" in allE)
  12.665 +   apply (fastsimp cong add: conj_cong split add: split_bind)
  12.666 +  txt {* case @{text "App e1 e2"} *}
  12.667 +  apply (intro strip)
  12.668 +  apply (erule has_type_casesE)
  12.669 +  apply (erule_tac x = s' in allE)
  12.670 +  apply (erule_tac x = a in allE)
  12.671 +  apply (erule_tac x = "t2 -> t'" in allE)
  12.672 +  apply (erule_tac x = n in allE)
  12.673 +  apply (tactic "safe_tac HOL_cs")
  12.674 +  apply (erule_tac x = r in allE)
  12.675 +  apply (erule_tac x = "$s a" in allE)
  12.676 +  apply (erule_tac x = t2 in allE)
  12.677 +  apply (erule_tac x = m in allE)
  12.678 +  apply simp
  12.679 +  apply (tactic "safe_tac HOL_cs")
  12.680 +   apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
  12.681 +     thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
  12.682 +  apply (subgoal_tac
  12.683 +    "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
  12.684 +      else ra x)) ($ sa t) =
  12.685 +    $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
  12.686 +      else ra x)) (ta -> (TVar ma))")
  12.687 +   apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
  12.688 +     else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
  12.689 +     s = "($ ra ta) -> t'" in ssubst)
  12.690 +    prefer 2
  12.691 +    apply (simp add: subst_comp_te)
  12.692 +    apply (rule eq_free_eq_subst_te)
  12.693 +    apply (intro strip)
  12.694 +    apply (subgoal_tac "na \<noteq> ma")
  12.695 +     prefer 2
  12.696 +     apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
  12.697 +    apply (case_tac "na \<in> free_tv sa")
  12.698 +     txt {* @{text "na \<notin> free_tv sa"} *}
  12.699 +     prefer 2
  12.700 +     apply (frule not_free_impl_id)
  12.701 +     apply simp
  12.702 +    txt {* @{text "na \<in> free_tv sa"} *}
  12.703 +    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
  12.704 +    apply (drule_tac eq_subst_tel_eq_free)
  12.705 +     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
  12.706 +    apply simp
  12.707 +    apply (case_tac "na \<in> dom sa")
  12.708 +     prefer 2
  12.709 +     txt {* @{text "na \<noteq> dom sa"} *}
  12.710 +     apply (simp add: dom_def)
  12.711 +    txt {* @{text "na \<in> dom sa"} *}
  12.712 +    apply (rule eq_free_eq_subst_te)
  12.713 +    apply (intro strip)
  12.714 +    apply (subgoal_tac "nb \<noteq> ma")
  12.715 +     prefer 2
  12.716 +     apply (frule new_tv_W, assumption)
  12.717 +     apply (erule conjE)
  12.718 +     apply (drule new_tv_subst_tel)
  12.719 +      apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
  12.720 +     apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
  12.721 +    apply (fastsimp simp add: cod_def free_tv_subst)
  12.722 +   prefer 2
  12.723 +   apply (simp (no_asm))
  12.724 +   apply (rule eq_free_eq_subst_te)
  12.725 +   apply (intro strip)
  12.726 +   apply (subgoal_tac "na \<noteq> ma")
  12.727 +    prefer 2
  12.728 +    apply (frule new_tv_W, assumption)
  12.729 +    apply (erule conjE)
  12.730 +    apply (drule sym [THEN W_var_geD])
  12.731 +    apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
  12.732 +   apply (case_tac "na \<in> free_tv t - free_tv sa")
  12.733 +    prefer 2
  12.734 +    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
  12.735 +    apply simp
  12.736 +    defer
  12.737 +    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
  12.738 +    apply simp
  12.739 +    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
  12.740 +    apply (drule eq_subst_tel_eq_free)
  12.741 +     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
  12.742 +    apply (simp add: free_tv_subst dom_def)
  12.743 +   prefer 2 apply fast
  12.744 +  apply (simp (no_asm_simp) split add: split_bind)
  12.745 +  apply (tactic "safe_tac HOL_cs")
  12.746 +   apply (drule mgu_Ok)
  12.747 +   apply fastsimp
  12.748 +  apply (drule mgu_mg, assumption)
  12.749 +  apply (erule exE)
  12.750 +  apply (rule_tac x = rb in exI)
  12.751 +  apply (rule conjI)
  12.752 +   prefer 2
  12.753 +   apply (drule_tac x = ma in fun_cong)
  12.754 +   apply (simp add: eq_sym_conv)
  12.755 +  apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
  12.756 +  apply (rule subst_comp_tel [symmetric, THEN [2] trans])
  12.757 +  apply (simp add: o_def eq_sym_conv)
  12.758 +  apply (rule eq_free_eq_subst_tel)
  12.759 +  apply (tactic "safe_tac HOL_cs")
  12.760 +  apply (subgoal_tac "ma \<noteq> na")
  12.761 +   prefer 2
  12.762 +   apply (frule new_tv_W, assumption)
  12.763 +   apply (erule conjE)
  12.764 +   apply (drule new_tv_subst_tel)
  12.765 +    apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
  12.766 +   apply (frule_tac n = m in new_tv_W, assumption)
  12.767 +   apply (erule conjE)
  12.768 +   apply (drule free_tv_app_subst_tel [THEN subsetD])
  12.769 +   apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
  12.770 +     thm "codD", thm "new_tv_not_free_tv"]) 1 *})
  12.771 +  apply (case_tac "na \<in> free_tv t - free_tv sa")
  12.772 +   prefer 2
  12.773 +   txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
  12.774 +   apply simp
  12.775 +   defer
  12.776 +   txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
  12.777 +   apply simp
  12.778 +   apply (drule free_tv_app_subst_tel [THEN subsetD])
  12.779 +   apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
  12.780 +     eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
  12.781 +  apply fast
  12.782 +  done
  12.783 +
  12.784 +lemma W_complete: "[] |- e :: t' ==>
  12.785 +    \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
  12.786 +  apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
  12.787 +    apply simp_all
  12.788 +  done
  12.789 +
  12.790 +
  12.791 +section {* Equivalence of @{text \<W>} and @{text \<I>} *}
  12.792 +
  12.793 +text {*
  12.794 +  Recursive definition of type inference algorithm @{text \<I>} for
  12.795 +  Mini-ML.
  12.796 +*}
  12.797 +
  12.798 +consts
  12.799 +  I :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<I>")
  12.800 +primrec
  12.801 +  "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
  12.802 +  "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
  12.803 +    Ok (s, TVar n -> t, m))"
  12.804 +  "\<I> (App e1 e2) a n s =
  12.805 +    ((s1, t1, m1) := \<I> e1 a n s;
  12.806 +    (s2, t2, m2) := \<I> e2 a m1 s1;
  12.807 +    u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
  12.808 +    Ok($u o s2, TVar m2, Suc m2))"
  12.809 +
  12.810 +text {* \medskip Correctness. *}
  12.811 +
  12.812 +lemma I_correct_wrt_W: "!!a m s s' t n.
  12.813 +    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
  12.814 +    \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
  12.815 +  apply (atomize (full))
  12.816 +  apply (induct e)
  12.817 +    txt {* case @{text "Var n"} *}
  12.818 +    apply (simp add: app_subst_list split: split_if)
  12.819 +   txt {* case @{text "Abs e"} *}
  12.820 +   apply (tactic {* asm_full_simp_tac
  12.821 +     (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
  12.822 +   apply (intro strip)
  12.823 +   apply (rule conjI)
  12.824 +    apply (intro strip)
  12.825 +    apply (erule allE)+
  12.826 +    apply (erule impE)
  12.827 +     prefer 2 apply (fastsimp simp add: new_tv_subst)
  12.828 +    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
  12.829 +      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
  12.830 +   apply (intro strip)
  12.831 +   apply (erule allE)+
  12.832 +   apply (erule impE)
  12.833 +    prefer 2 apply (fastsimp simp add: new_tv_subst)
  12.834 +   apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
  12.835 +     thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
  12.836 +  txt {* case @{text "App e1 e2"} *}
  12.837 +  apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
  12.838 +  apply (intro strip)
  12.839 +  apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
  12.840 +  apply (rule conjI)
  12.841 +   apply fastsimp
  12.842 +  apply (intro strip)
  12.843 +  apply (rename_tac s1 t1' n1')
  12.844 +  apply (erule_tac x = a in allE)
  12.845 +  apply (erule_tac x = m in allE)
  12.846 +  apply (erule_tac x = s in allE)
  12.847 +  apply (erule_tac x = s1' in allE)
  12.848 +  apply (erule_tac x = t1 in allE)
  12.849 +  apply (erule_tac x = n1 in allE)
  12.850 +  apply (erule_tac x = a in allE)
  12.851 +  apply (erule_tac x = n1 in allE)
  12.852 +  apply (erule_tac x = s1' in allE)
  12.853 +  apply (erule_tac x = s2' in allE)
  12.854 +  apply (erule_tac x = t2 in allE)
  12.855 +  apply (erule_tac x = n2 in allE)
  12.856 +  apply (rule conjI)
  12.857 +   apply (intro strip)
  12.858 +   apply (rule notI)
  12.859 +   apply simp
  12.860 +   apply (erule impE)
  12.861 +    apply (frule new_tv_subst_tel, assumption)
  12.862 +    apply (drule_tac a = "$s a" in new_tv_W, assumption)
  12.863 +    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
  12.864 +   apply (fastsimp simp add: subst_comp_tel)
  12.865 +  apply (intro strip)
  12.866 +  apply (rename_tac s2 t2' n2')
  12.867 +  apply (rule conjI)
  12.868 +   apply (intro strip)
  12.869 +   apply (rule notI)
  12.870 +   apply simp
  12.871 +   apply (erule impE)
  12.872 +   apply (frule new_tv_subst_tel, assumption)
  12.873 +   apply (drule_tac a = "$s a" in new_tv_W, assumption)
  12.874 +    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
  12.875 +   apply (fastsimp simp add: subst_comp_tel subst_comp_te)
  12.876 +  apply (intro strip)
  12.877 +  apply (erule (1) notE impE)
  12.878 +  apply (erule (1) notE impE)
  12.879 +  apply (erule exE)
  12.880 +  apply (erule conjE)
  12.881 +  apply (erule impE)
  12.882 +   apply (frule new_tv_subst_tel, assumption)
  12.883 +   apply (drule_tac a = "$s a" in new_tv_W, assumption)
  12.884 +   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
  12.885 +  apply (erule (1) notE impE)
  12.886 +  apply (erule exE conjE)+
  12.887 +  apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
  12.888 +  apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
  12.889 +   apply (simp add: new_tv_subst)
  12.890 +  apply (frule new_tv_subst_tel, assumption)
  12.891 +  apply (drule_tac a = "$s a" in new_tv_W, assumption)
  12.892 +  apply (tactic "safe_tac HOL_cs")
  12.893 +    apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
  12.894 +   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
  12.895 +  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
  12.896 +  apply (drule new_tv_subst_tel, assumption)
  12.897 +  apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
  12.898 +  apply (drule new_tv_subst_tel, assumption)
  12.899 +  apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
  12.900 +  done
  12.901 +
  12.902 +lemma I_complete_wrt_W: "!!a m s.
  12.903 +    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
  12.904 +  apply (atomize (full))
  12.905 +  apply (induct e)
  12.906 +    apply (simp add: app_subst_list)
  12.907 +   apply (simp (no_asm))
  12.908 +   apply (intro strip)
  12.909 +   apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
  12.910 +    apply (tactic {* asm_simp_tac (HOL_ss addsimps
  12.911 +      [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
  12.912 +    apply (erule conjE)
  12.913 +    apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
  12.914 +    apply (simp (no_asm_simp))
  12.915 +  apply (simp (no_asm_simp))
  12.916 +  apply (intro strip)
  12.917 +  apply (erule exE)+
  12.918 +  apply (erule conjE)+
  12.919 +  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
  12.920 +   apply fast
  12.921 +  apply (erule exE)
  12.922 +  apply (erule conjE)
  12.923 +  apply hypsubst
  12.924 +  apply (simp (no_asm_simp))
  12.925 +  apply (erule disjE)
  12.926 +   apply (rule disjI1)
  12.927 +   apply (simp (no_asm_use) add: o_def subst_comp_tel)
  12.928 +   apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
  12.929 +     erule_tac [2] asm_rl, erule_tac [2] asm_rl)
  12.930 +   apply (rule conjI)
  12.931 +    apply (fast intro: W_var_ge [THEN new_tv_list_le])
  12.932 +   apply (rule new_tv_subst_comp_2)
  12.933 +    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
  12.934 +   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
  12.935 +  apply (rule disjI2)
  12.936 +  apply (erule exE)+
  12.937 +  apply (erule conjE)
  12.938 +  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
  12.939 +   apply (rule conjI)
  12.940 +   apply (fast intro: W_var_ge [THEN new_tv_list_le])
  12.941 +   apply (rule new_tv_subst_comp_1)
  12.942 +   apply (fast intro: W_var_ge [THEN new_tv_subst_le])
  12.943 +   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
  12.944 +  apply (erule exE)
  12.945 +  apply (erule conjE)
  12.946 +  apply hypsubst
  12.947 +  apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
  12.948 +  done
  12.949 +
  12.950 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/W0/document/root.tex	Tue Feb 26 00:19:04 2002 +0100
    13.3 @@ -0,0 +1,25 @@
    13.4 +
    13.5 +\documentclass[11pt,a4paper]{article}
    13.6 +\usepackage{isabelle,isabellesym}
    13.7 +\usepackage{pdfsetup}
    13.8 +
    13.9 +\urlstyle{rm}
   13.10 +\isabellestyle{it}
   13.11 +
   13.12 +\newcommand{\isasymbind}{\textsf{bind}}
   13.13 +
   13.14 +\begin{document}
   13.15 +
   13.16 +\title{Type inference for let-free MiniML}
   13.17 +\author{Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel}
   13.18 +\maketitle
   13.19 +
   13.20 +\tableofcontents
   13.21 +
   13.22 +\parindent 0pt\parskip 0.5ex
   13.23 +\input{session}
   13.24 +
   13.25 +%\bibliographystyle{abbrv}
   13.26 +%\bibliography{root}
   13.27 +
   13.28 +\end{document}