src/HOL/Isar_examples/W_correct.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8103 86f94a8116a9
permissions -rw-r--r--
improved presentation;
     1 (*  Title:      HOL/Isar_examples/W_correct.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Correctness of Milner's type inference algorithm W (let-free version).
     6 *)
     7 
     8 header {* Milner's type inference algorithm~W (let-free version) *};
     9 
    10 theory W_correct = Main + Type:;
    11 
    12 text_raw {*
    13   \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
    14   by Dieter Nazareth and Tobias Nipkow.}
    15 *};
    16 
    17 
    18 subsection "Mini ML with type inference rules";
    19 
    20 datatype
    21   expr = Var nat | Abs expr | App expr expr;
    22 
    23 
    24 text {* Type inference rules. *};
    25 
    26 consts
    27   has_type :: "(typ list * expr * typ) set";
    28 
    29 syntax
    30   "@has_type" :: "[typ list, expr, typ] => bool"
    31     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
    32 translations
    33   "a |- e :: t" == "(a,e,t) : has_type";
    34 
    35 inductive has_type
    36   intrs [simp]
    37     VarI: "n < length a ==> a |- Var n :: a ! n"
    38     AbsI: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    39     AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
    40               ==> a |- App e1 e2 :: t1";
    41 
    42 text {* Type assigment is closed wrt.\ substitution. *};
    43 
    44 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
    45 proof -;
    46   assume "a |- e :: t";
    47   thus ?thesis (is "?P a e t");
    48   proof (rule has_type.induct);     (* FIXME induct method *)
    49     fix a n;
    50     assume "n < length a";
    51     hence "n < length (map ($ s) a)"; by simp;
    52     hence "map ($ s) a |- Var n :: map ($ s) a ! n";
    53       by (rule has_type.VarI);
    54     also; have "map ($ s) a ! n = $ s (a ! n)";
    55       by (rule nth_map);
    56     also; have "map ($ s) a = $ s a";
    57       by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
    58     finally; show "?P a (Var n) (a ! n)"; .;
    59   next;
    60     fix a e t1 t2;
    61     assume "?P (t1 # a) e t2";
    62     hence "$ s t1 # map ($ s) a |- e :: $ s t2";
    63       by (simp add: app_subst_list);
    64     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2";
    65       by (rule has_type.AbsI);
    66     thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list);
    67   next;
    68     fix a e1 e2 t1 t2;
    69     assume "?P a e1 (t2 -> t1)" "?P a e2 t2";
    70     thus "?P a (App e1 e2) t1"; by simp;
    71   qed;
    72 qed;
    73 
    74 
    75 subsection {* Type inference algorithm W *};
    76 
    77 consts
    78   W :: "[expr, typ list, nat] => (subst * typ * nat) maybe";
    79 
    80 primrec
    81   "W (Var i) a n =
    82       (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
    83   "W (Abs e) a n =
    84       ((s, t, m) := W e (TVar n # a) (Suc n);
    85        Ok (s, (s n) -> t, m))"
    86   "W (App e1 e2) a n =
    87       ((s1, t1, m1) := W e1 a n;
    88        (s2, t2, m2) := W e2 ($s1 a) m1;
    89        u := mgu ($ s2 t1) (t2 -> TVar m2);
    90        Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))";
    91 
    92 
    93 subsection {* Correctness theorem *};
    94 
    95 text_raw {* \begin{comment} *};
    96 
    97 (* FIXME proper split att/mod *)
    98 ML_setup {* Addsplits [split_bind]; *};
    99 
   100 text_raw {* \end{comment} *};
   101 
   102 theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
   103 proof -;
   104   assume W_ok: "W e a n = Ok (s, t, m)";
   105   have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t"
   106     (is "?P e");
   107   proof (induct e);
   108     fix n; show "?P (Var n)"; by simp;
   109   next;
   110     fix e; assume hyp: "?P e";
   111     show "?P (Abs e)";
   112     proof (intro allI impI);
   113       fix a s t m n;
   114       assume "Ok (s, t, m) = W (Abs e) a n";
   115       hence "EX t'. t = s n -> t' &
   116           Ok (s, t', m) = W e (TVar n # a) (Suc n)";
   117         by (rule rev_mp) simp;
   118       with hyp; show "$ s a |- Abs e :: t";
   119         by (force intro: has_type.AbsI);
   120     qed;
   121   next;
   122     fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2";
   123     show "?P (App e1 e2)";
   124     proof (intro allI impI);
   125       fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
   126       hence "EX s1 t1 n1 s2 t2 n2 u.
   127           s = $ u o $ s2 o s1 & t = u n2 &
   128           mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
   129              W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
   130              W e1 a n = Ok (s1, t1, n1)";
   131         by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
   132       thus "$ s a |- App e1 e2 :: t";
   133       proof (elim exE conjE);
   134         fix s1 t1 n1 s2 t2 n2 u;
   135         assume s: "s = $ u o $ s2 o s1"
   136           and t: "t = u n2"
   137           and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
   138           and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
   139           and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
   140         show ?thesis;
   141         proof (rule has_type.AppI);
   142           from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";
   143             by (simp add: subst_comp_tel o_def);
   144           show "$s a |- e1 :: $ u t2 -> t";
   145           proof -;
   146             from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
   147               by blast;
   148             hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
   149               by (intro has_type_subst_closed);
   150             with s' t mgu_ok; show ?thesis; by simp;
   151           qed;
   152           show "$ s a |- e2 :: $ u t2";
   153           proof -;
   154             from hyp2 W2_ok [RS sym];
   155               have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
   156             hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
   157               by (rule has_type_subst_closed);
   158             with s'; show ?thesis; by simp;
   159           qed;
   160         qed;
   161       qed;
   162     qed;
   163   qed;
   164   with W_ok [RS sym]; show ?thesis; by blast;
   165 qed;
   166 
   167 end;