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