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
wenzelm@7621
     1
(*  Title:      HOL/Isar_examples/W_correct.thy
wenzelm@7621
     2
    ID:         $Id$
wenzelm@7621
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@7621
     4
wenzelm@7621
     5
Correctness of Milner's type inference algorithm W (let-free version).
wenzelm@7621
     6
*)
wenzelm@7621
     7
wenzelm@10007
     8
header {* Milner's type inference algorithm~W (let-free version) *}
wenzelm@7761
     9
wenzelm@10007
    10
theory W_correct = Main + Type:
wenzelm@7621
    11
wenzelm@7968
    12
text_raw {*
wenzelm@10146
    13
  \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0/}
wenzelm@7968
    14
  by Dieter Nazareth and Tobias Nipkow.}
wenzelm@10007
    15
*}
wenzelm@7968
    16
wenzelm@7621
    17
wenzelm@10007
    18
subsection "Mini ML with type inference rules"
wenzelm@7621
    19
wenzelm@7621
    20
datatype
wenzelm@10007
    21
  expr = Var nat | Abs expr | App expr expr
wenzelm@7621
    22
wenzelm@7621
    23
wenzelm@10007
    24
text {* Type inference rules. *}
wenzelm@7621
    25
wenzelm@7621
    26
consts
wenzelm@10007
    27
  has_type :: "(typ list * expr * typ) set"
wenzelm@7621
    28
wenzelm@7621
    29
syntax
wenzelm@10408
    30
  "_has_type" :: "typ list => expr => typ => bool"
wenzelm@10007
    31
    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
wenzelm@7621
    32
translations
wenzelm@10146
    33
  "a |- e :: t" == "(a, e, t) : has_type"
wenzelm@7621
    34
wenzelm@7621
    35
inductive has_type
wenzelm@9596
    36
  intros [simp]
wenzelm@8441
    37
    Var: "n < length a ==> a |- Var n :: a ! n"
wenzelm@8441
    38
    Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
wenzelm@9659
    39
    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
wenzelm@10007
    40
      ==> a |- App e1 e2 :: t1"
wenzelm@7621
    41
wenzelm@8441
    42
wenzelm@10007
    43
text {* Type assigment is closed wrt.\ substitution. *}
wenzelm@7761
    44
wenzelm@10007
    45
lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
wenzelm@10007
    46
proof -
wenzelm@10007
    47
  assume "a |- e :: t"
wenzelm@10007
    48
  thus ?thesis (is "?P a e t")
wenzelm@10007
    49
  proof (induct (open) ?P a e t)
wenzelm@10007
    50
    case Var
wenzelm@10007
    51
    hence "n < length (map ($ s) a)" by simp
wenzelm@10007
    52
    hence "map ($ s) a |- Var n :: map ($ s) a ! n"
wenzelm@10007
    53
      by (rule has_type.Var)
wenzelm@10007
    54
    also have "map ($ s) a ! n = $ s (a ! n)"
wenzelm@10007
    55
      by (rule nth_map)
wenzelm@10007
    56
    also have "map ($ s) a = $ s a"
wenzelm@10007
    57
      by (simp only: app_subst_list)
wenzelm@10007
    58
    finally show "?P a (Var n) (a ! n)" .
wenzelm@10007
    59
  next
wenzelm@10007
    60
    case Abs
wenzelm@10007
    61
    hence "$ s t1 # map ($ s) a |- e :: $ s t2"
wenzelm@10007
    62
      by (simp add: app_subst_list)
wenzelm@10007
    63
    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
wenzelm@10007
    64
      by (rule has_type.Abs)
wenzelm@10007
    65
    thus "?P a (Abs e) (t1 -> t2)"
wenzelm@10007
    66
      by (simp add: app_subst_list)
wenzelm@10007
    67
  next
wenzelm@10007
    68
    case App
wenzelm@10007
    69
    thus "?P a (App e1 e2) t1" by simp
wenzelm@10007
    70
  qed
wenzelm@10007
    71
qed
wenzelm@7621
    72
wenzelm@7621
    73
wenzelm@10007
    74
subsection {* Type inference algorithm W *}
wenzelm@7621
    75
wenzelm@7621
    76
consts
wenzelm@10408
    77
  W :: "expr => typ list => nat => (subst * typ * nat) maybe"
wenzelm@7621
    78
wenzelm@7621
    79
primrec
wenzelm@7621
    80
  "W (Var i) a n =
wenzelm@9475
    81
    (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
wenzelm@7621
    82
  "W (Abs e) a n =
wenzelm@9475
    83
    ((s, t, m) := W e (TVar n # a) (Suc n);
wenzelm@9475
    84
     Ok (s, (s n) -> t, m))"
wenzelm@7621
    85
  "W (App e1 e2) a n =
wenzelm@9475
    86
    ((s1, t1, m1) := W e1 a n;
wenzelm@9475
    87
     (s2, t2, m2) := W e2 ($s1 a) m1;
wenzelm@9475
    88
     u := mgu ($ s2 t1) (t2 -> TVar m2);
wenzelm@10007
    89
     Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
wenzelm@7621
    90
wenzelm@7621
    91
wenzelm@10007
    92
subsection {* Correctness theorem *}
wenzelm@7761
    93
wenzelm@10408
    94
theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t"
wenzelm@10408
    95
  (is "PROP ?P e")
wenzelm@10408
    96
proof (induct e)
wenzelm@10408
    97
  fix a s t m n
wenzelm@10408
    98
  {
wenzelm@10408
    99
    fix i
wenzelm@10408
   100
    assume "Ok (s, t, m) = W (Var i) a n"
wenzelm@10408
   101
    thus "$ s a |- Var i :: t" by (simp split: if_splits)
wenzelm@10408
   102
  next
wenzelm@10408
   103
    fix e assume hyp: "PROP ?P e"
wenzelm@10408
   104
    assume "Ok (s, t, m) = W (Abs e) a n"
wenzelm@10408
   105
    then obtain t' where "t = s n -> t'"
wenzelm@10408
   106
        and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
wenzelm@10408
   107
      by (auto split: bind_splits)
wenzelm@10408
   108
    with hyp show "$ s a |- Abs e :: t"
wenzelm@10408
   109
      by (force intro: has_type.Abs)
wenzelm@10408
   110
  next
wenzelm@10408
   111
    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
wenzelm@10408
   112
    assume "Ok (s, t, m) = W (App e1 e2) a n"
wenzelm@10408
   113
    then obtain s1 t1 n1 s2 t2 n2 u where
wenzelm@8103
   114
          s: "s = $ u o $ s2 o s1"
wenzelm@10408
   115
        and t: "t = u n2"
wenzelm@10408
   116
        and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
wenzelm@10408
   117
        and W1_ok: "Ok (s1, t1, n1) = W e1 a n"
wenzelm@10408
   118
        and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1"
wenzelm@10408
   119
      by (auto split: bind_splits simp: that)
wenzelm@10408
   120
    show "$ s a |- App e1 e2 :: t"
wenzelm@10408
   121
    proof (rule has_type.App)
wenzelm@10408
   122
      from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
wenzelm@10408
   123
        by (simp add: subst_comp_tel o_def)
wenzelm@10408
   124
      show "$s a |- e1 :: $ u t2 -> t"
wenzelm@10408
   125
      proof -
wenzelm@10408
   126
        from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1)
wenzelm@10408
   127
        hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
wenzelm@10408
   128
          by (intro has_type_subst_closed)
wenzelm@10408
   129
        with s' t mgu_ok show ?thesis by simp
wenzelm@10007
   130
      qed
wenzelm@10408
   131
      show "$ s a |- e2 :: $ u t2"
wenzelm@10408
   132
      proof -
wenzelm@10408
   133
        from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2)
wenzelm@10408
   134
        hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
wenzelm@10408
   135
          by (rule has_type_subst_closed)
wenzelm@10408
   136
        with s' show ?thesis by simp
wenzelm@10408
   137
      qed
wenzelm@10408
   138
    qed
wenzelm@10408
   139
  }
wenzelm@10007
   140
qed
wenzelm@7621
   141
wenzelm@10007
   142
end