added W_correct -- correctness of Milner's type inference algorithm W
(let-free version);

--- a/src/HOL/Isar_examples/ROOT.ML	Tue Sep 28 14:15:57 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Tue Sep 28 14:24:22 1999 +0200
@@ -14,3 +14,4 @@
 time_use_thy "KnasterTarski";
 time_use_thy "MutilatedCheckerboard";
 with_path "../Induct" time_use_thy "MultisetOrder";
+with_path "../W0" time_use_thy "W_correct";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Sep 28 14:24:22 1999 +0200
@@ -0,0 +1,145 @@
+(*  Title:      HOL/Isar_examples/W_correct.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Correctness of Milner's type inference algorithm W (let-free version).
+Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
+*)
+
+theory W_correct = Main + Type:;
+
+
+section "Mini ML with type inference rules";
+
+datatype
+  expr = Var nat | Abs expr | App expr expr;
+
+
+text {* type inference rules *};
+
+consts
+  has_type :: "(typ list * expr * typ) set";
+
+syntax
+  "@has_type" :: "[typ list, expr, typ] => bool"  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
+translations
+  "a |- e :: t" == "(a,e,t) : has_type";
+
+inductive has_type
+  intrs [simp]
+    VarI: "n < length a ==> a |- Var n :: a ! n"
+    AbsI: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
+    AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
+              ==> a |- App e1 e2 :: t1";
+
+theorem has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
+proof -;
+  assume "a |- e :: t";
+  thus ?thesis (is "?P a e t");
+  proof (rule has_type.induct);     (* FIXME induct method *)
+    fix a n;
+    assume "n < length a";
+    hence "n < length (map ($ s) a)"; by simp;
+    hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI);
+    also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map);
+    also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list);   (* FIXME unfold fails!? *)
+    finally; show "?P a (Var n) (a ! n)"; .;
+  next;
+    fix a e t1 t2;
+    assume "?P (t1 # a) e t2";
+    hence "$ s t1 # map ($ s) a |- e :: $ s t2"; by (simp add: app_subst_list);
+    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.AbsI);
+    thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list);
+  next;
+    fix a e1 e2 t1 t2;
+    assume "?P a e1 (t2 -> t1)" "?P a e2 t2";
+    thus "?P a (App e1 e2) t1"; by simp;
+  qed;
+qed;
+
+
+section {* Type inference algorithm W *};
+
+consts
+  W :: "[expr, typ list, nat] => (subst * typ * nat) maybe";
+
+primrec
+  "W (Var i) a n =
+      (if i < length a then Ok(id_subst, a ! i, n) else Fail)"
+  "W (Abs e) a n =
+      ((s, t, m) := W e (TVar n # a) (Suc n);
+       Ok(s, (s n) -> t, m))"
+  "W (App e1 e2) a n =
+      ((s1, t1, m1) := W e1 a n;
+       (s2, t2, m2) := W e2 ($s1 a) m1;
+       u := mgu ($ s2 t1) (t2 -> TVar m2);
+       Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))";
+
+
+(* FIXME proper split att/mod *)
+ML_setup {* Addsplits [split_bind]; *};
+
+theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
+proof -;
+  assume W_ok: "W e a n = Ok (s, t, m)";
+  let ?P = "%e. ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t";
+    (* FIXME (is ...) fails!? *)
+  have "?P e";
+  proof (induct e);
+    fix n; show "?P (Var n)"; by simp;
+  next;
+    fix e; assume hyp: "?P e";
+    show "?P (Abs e)";
+    proof (intro allI impI);
+      fix a s t m n;
+      assume "Ok (s, t, m) = W (Abs e) a n";
+      hence "EX t'. t = s n -> t' & Ok (s, t', m) = W e (TVar n # a) (Suc n)";
+        by (rule rev_mp) simp;
+      with hyp; show "$ s a |- Abs e :: t";
+        by (force intro: has_type.AbsI);
+    qed;
+  next;
+    fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2";
+    show "?P (App e1 e2)";
+    proof (intro allI impI);
+      fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
+      hence "EX s1 t1 n1 s2 t2 n2 u.
+        s = $ u o $ s2 o s1 & t = u n2 &
+        mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
+           W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
+           W e1 a n = Ok (s1, t1, n1)"; by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
+      thus "$ s a |- App e1 e2 :: t";
+      proof (elim exE conjE);
+        fix s1 t1 n1 s2 t2 n2 u;
+        assume s: "s = $ u o $ s2 o s1"
+          and t: "t = u n2"
+          and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
+          and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
+          and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
+        show ?thesis;
+        proof (rule has_type.AppI);
+          from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; by (simp add: subst_comp_tel o_def);
+          show "$s a |- e1 :: $ u t2 -> t";
+          proof -;
+            from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast;
+            hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
+              by (intro has_type_subst_closed);
+            with s' t mgu_ok; show ?thesis; by simp;
+          qed;
+          show "$ s a |- e2 :: $ u t2";
+          proof -;
+            from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
+            hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
+              by (rule has_type_subst_closed);
+            with s'; show ?thesis; by simp;
+          qed;
+        qed;
+      qed;
+    qed;
+  qed;
+  with W_ok [RS sym]; show ?thesis; by blast;
+qed;
+
+
+end;
+