author | wenzelm |
Thu, 16 Mar 2000 00:36:22 +0100 | |
changeset 8491 | 82826ed95d4b |
parent 8441 | 18d67c88939c |
child 9475 | b24516d96847 |
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 |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
36 |
intrs [simp] |
8441 | 37 |
Var: "n < length a ==> a |- Var n :: a ! n" |
38 |
Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2" |
|
39 |
App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] |
|
7621
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 |
|
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"); |
8441 | 49 |
proof (induct ?P a e t); |
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); |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
next; |
8441 | 67 |
case App; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
68 |
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
|
69 |
qed; |
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 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
72 |
|
7761 | 73 |
subsection {* Type inference algorithm W *}; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
74 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
75 |
consts |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
76 |
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
|
77 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
78 |
primrec |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
79 |
"W (Var i) a n = |
7982 | 80 |
(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
|
81 |
"W (Abs e) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
82 |
((s, t, m) := W e (TVar n # a) (Suc n); |
7982 | 83 |
Ok (s, (s n) -> t, m))" |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
84 |
"W (App e1 e2) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
85 |
((s1, t1, m1) := W e1 a n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
86 |
(s2, t2, m2) := W e2 ($s1 a) m1; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
87 |
u := mgu ($ s2 t1) (t2 -> TVar m2); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
88 |
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
|
89 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
90 |
|
7761 | 91 |
subsection {* Correctness theorem *}; |
92 |
||
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
93 |
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
|
94 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
95 |
assume W_ok: "W e a n = Ok (s, t, m)"; |
8441 | 96 |
have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t" |
7761 | 97 |
(is "?P e"); |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
98 |
proof (induct e); |
8441 | 99 |
fix i; show "?P (Var i)"; by simp; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
100 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
101 |
fix e; assume hyp: "?P e"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
102 |
show "?P (Abs e)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
103 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
104 |
fix a s t m n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
105 |
assume "Ok (s, t, m) = W (Abs e) a n"; |
8103 | 106 |
thus "$ s a |- Abs e :: t"; |
8109 | 107 |
obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)"; |
8491 | 108 |
by (rule rev_mp) (simp split: split_bind); |
8441 | 109 |
with hyp; show ?thesis; by (force intro: has_type.Abs); |
8103 | 110 |
qed; |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
111 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
112 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
113 |
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
|
114 |
show "?P (App e1 e2)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
115 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
116 |
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
|
117 |
thus "$ s a |- App e1 e2 :: t"; |
8109 | 118 |
obtain s1 t1 n1 s2 t2 n2 u where |
8103 | 119 |
s: "s = $ u o $ s2 o s1" |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
120 |
and t: "t = u n2" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; |
8491 | 124 |
by (rule rev_mp) (simp split: split_bind); |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
125 |
show ?thesis; |
8441 | 126 |
proof (rule has_type.App); |
7761 | 127 |
from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; |
128 |
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
|
129 |
show "$s a |- e1 :: $ u t2 -> t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
130 |
proof -; |
7800 | 131 |
from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; |
132 |
by blast; |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
133 |
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
|
134 |
by (intro has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
135 |
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
|
136 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
137 |
show "$ s a |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
138 |
proof -; |
7809 | 139 |
from hyp2 W2_ok [RS sym]; |
140 |
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
|
141 |
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
142 |
by (rule has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
143 |
with s'; show ?thesis; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
144 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
145 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
146 |
qed; |
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 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
149 |
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
|
150 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
151 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
152 |
end; |