author | wenzelm |
Sat, 30 Oct 1999 20:20:48 +0200 | |
changeset 7982 | d534b897ce39 |
parent 7968 | 964b65b4e433 |
child 8103 | 86f94a8116a9 |
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 |
7761 | 30 |
"@has_type" :: "[typ list, expr, typ] => bool" |
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 |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
36 |
intrs [simp] |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
37 |
VarI: "n < length a ==> a |- Var n :: a ! n" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
38 |
AbsI: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
39 |
AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
40 |
==> a |- App e1 e2 :: t1"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
41 |
|
7982 | 42 |
text {* Type assigment is closed wrt.\ substitution. *}; |
7761 | 43 |
|
7649 | 44 |
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
|
45 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
46 |
assume "a |- e :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
47 |
thus ?thesis (is "?P a e t"); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
48 |
proof (rule has_type.induct); (* FIXME induct method *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
49 |
fix a n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
50 |
assume "n < length a"; |
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"; |
53 |
by (rule has_type.VarI); |
|
7800 | 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); (* FIXME unfold fails!? *) |
|
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; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
60 |
fix a e t1 t2; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
61 |
assume "?P (t1 # a) e t2"; |
7761 | 62 |
hence "$ s t1 # map ($ s) a |- e :: $ s t2"; |
63 |
by (simp add: app_subst_list); |
|
64 |
hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; |
|
65 |
by (rule has_type.AbsI); |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
66 |
thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
67 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
68 |
fix a e1 e2 t1 t2; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
69 |
assume "?P a e1 (t2 -> t1)" "?P a e2 t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
70 |
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
|
71 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
72 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
73 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
74 |
|
7761 | 75 |
subsection {* Type inference algorithm W *}; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
76 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
77 |
consts |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
78 |
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
|
79 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
80 |
primrec |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
81 |
"W (Var i) a n = |
7982 | 82 |
(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
|
83 |
"W (Abs e) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
84 |
((s, t, m) := W e (TVar n # a) (Suc n); |
7982 | 85 |
Ok (s, (s n) -> t, m))" |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
86 |
"W (App e1 e2) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
87 |
((s1, t1, m1) := W e1 a n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
88 |
(s2, t2, m2) := W e2 ($s1 a) m1; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
89 |
u := mgu ($ s2 t1) (t2 -> TVar m2); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
90 |
Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
91 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
92 |
|
7761 | 93 |
subsection {* Correctness theorem *}; |
94 |
||
7982 | 95 |
text_raw {* \begin{comment} *}; |
96 |
||
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
97 |
(* FIXME proper split att/mod *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
98 |
ML_setup {* Addsplits [split_bind]; *}; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
99 |
|
7982 | 100 |
text_raw {* \end{comment} *}; |
101 |
||
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
102 |
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
|
103 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
104 |
assume W_ok: "W e a n = Ok (s, t, m)"; |
7761 | 105 |
have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" |
106 |
(is "?P e"); |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
107 |
proof (induct e); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
108 |
fix n; show "?P (Var n)"; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
109 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
110 |
fix e; assume hyp: "?P e"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
111 |
show "?P (Abs e)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
112 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
113 |
fix a s t m n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
114 |
assume "Ok (s, t, m) = W (Abs e) a n"; |
7761 | 115 |
hence "EX t'. t = s n -> t' & |
116 |
Ok (s, t', m) = W e (TVar n # a) (Suc n)"; |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
117 |
by (rule rev_mp) simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
118 |
with hyp; show "$ s a |- Abs e :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
119 |
by (force intro: has_type.AbsI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
120 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
121 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
122 |
fix e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
123 |
show "?P (App e1 e2)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
124 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
125 |
fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
126 |
hence "EX s1 t1 n1 s2 t2 n2 u. |
7800 | 127 |
s = $ u o $ s2 o s1 & t = u n2 & |
128 |
mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & |
|
129 |
W e2 ($ s1 a) n1 = Ok (s2, t2, n2) & |
|
130 |
W e1 a n = Ok (s1, t1, n1)"; |
|
131 |
by (rule rev_mp) (simp, force); (* FIXME force fails !??*) |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
132 |
thus "$ s a |- App e1 e2 :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
133 |
proof (elim exE conjE); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
134 |
fix s1 t1 n1 s2 t2 n2 u; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
135 |
assume s: "s = $ u o $ s2 o s1" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
136 |
and t: "t = u n2" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
137 |
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
|
138 |
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
|
139 |
and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
140 |
show ?thesis; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
141 |
proof (rule has_type.AppI); |
7761 | 142 |
from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; |
143 |
by (simp add: subst_comp_tel o_def); |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
144 |
show "$s a |- e1 :: $ u t2 -> t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
145 |
proof -; |
7800 | 146 |
from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; |
147 |
by blast; |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
148 |
hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
149 |
by (intro has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
150 |
with s' t mgu_ok; show ?thesis; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
151 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
152 |
show "$ s a |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
153 |
proof -; |
7809 | 154 |
from hyp2 W2_ok [RS sym]; |
155 |
have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
156 |
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
157 |
by (rule has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
158 |
with s'; show ?thesis; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
159 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
160 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
161 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
162 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
163 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
164 |
with W_ok [RS sym]; show ?thesis; by blast; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
165 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
166 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
167 |
end; |