src/HOL/Isar_examples/W_correct.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10408 d8b3613158b1
child 11628 e57a6e51715e
permissions -rw-r--r--
improved theory reference in comment
     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   intros [simp]
    37     Var: "n < length a ==> a |- Var n :: a ! n"
    38     Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
    39     App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
    40       ==> a |- App e1 e2 :: t1"
    41 
    42 
    43 text {* Type assigment is closed wrt.\ substitution. *}
    44 
    45 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
    46 proof -
    47   assume "a |- e :: t"
    48   thus ?thesis (is "?P a e t")
    49   proof (induct (open) ?P a e t)
    50     case Var
    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.Var)
    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)
    58     finally show "?P a (Var n) (a ! n)" .
    59   next
    60     case Abs
    61     hence "$ s t1 # map ($ s) a |- e :: $ s t2"
    62       by (simp add: app_subst_list)
    63     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
    64       by (rule has_type.Abs)
    65     thus "?P a (Abs e) (t1 -> t2)"
    66       by (simp add: app_subst_list)
    67   next
    68     case App
    69     thus "?P a (App e1 e2) t1" by simp
    70   qed
    71 qed
    72 
    73 
    74 subsection {* Type inference algorithm W *}
    75 
    76 consts
    77   W :: "expr => typ list => nat => (subst * typ * nat) maybe"
    78 
    79 primrec
    80   "W (Var i) a n =
    81     (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
    82   "W (Abs e) a n =
    83     ((s, t, m) := W e (TVar n # a) (Suc n);
    84      Ok (s, (s n) -> t, m))"
    85   "W (App e1 e2) a n =
    86     ((s1, t1, m1) := W e1 a n;
    87      (s2, t2, m2) := W e2 ($s1 a) m1;
    88      u := mgu ($ s2 t1) (t2 -> TVar m2);
    89      Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
    90 
    91 
    92 subsection {* Correctness theorem *}
    93 
    94 theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t"
    95   (is "PROP ?P e")
    96 proof (induct e)
    97   fix a s t m n
    98   {
    99     fix i
   100     assume "Ok (s, t, m) = W (Var i) a n"
   101     thus "$ s a |- Var i :: t" by (simp split: if_splits)
   102   next
   103     fix e assume hyp: "PROP ?P e"
   104     assume "Ok (s, t, m) = W (Abs e) a n"
   105     then obtain t' where "t = s n -> t'"
   106         and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
   107       by (auto split: bind_splits)
   108     with hyp show "$ s a |- Abs e :: t"
   109       by (force intro: has_type.Abs)
   110   next
   111     fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
   112     assume "Ok (s, t, m) = W (App e1 e2) a n"
   113     then obtain s1 t1 n1 s2 t2 n2 u where
   114           s: "s = $ u o $ s2 o s1"
   115         and t: "t = u n2"
   116         and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
   117         and W1_ok: "Ok (s1, t1, n1) = W e1 a n"
   118         and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1"
   119       by (auto split: bind_splits simp: that)
   120     show "$ s a |- App e1 e2 :: t"
   121     proof (rule has_type.App)
   122       from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
   123         by (simp add: subst_comp_tel o_def)
   124       show "$s a |- e1 :: $ u t2 -> t"
   125       proof -
   126         from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1)
   127         hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
   128           by (intro has_type_subst_closed)
   129         with s' t mgu_ok show ?thesis by simp
   130       qed
   131       show "$ s a |- e2 :: $ u t2"
   132       proof -
   133         from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2)
   134         hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
   135           by (rule has_type_subst_closed)
   136         with s' show ?thesis by simp
   137       qed
   138     qed
   139   }
   140 qed
   141 
   142 end