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;