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