author | wenzelm |
Fri, 28 Sep 2001 19:19:26 +0200 | |
changeset 11628 | e57a6e51715e |
parent 10408 | d8b3613158b1 |
child 11809 | c9ffdd63dd93 |
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 |
|
10007 | 8 |
header {* Milner's type inference algorithm~W (let-free version) *} |
7761 | 9 |
|
10007 | 10 |
theory W_correct = Main + Type: |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
11 |
|
7968 | 12 |
text_raw {* |
10146 | 13 |
\footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0/} |
7968 | 14 |
by Dieter Nazareth and Tobias Nipkow.} |
10007 | 15 |
*} |
7968 | 16 |
|
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
17 |
|
10007 | 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 |
10007 | 21 |
expr = Var nat | Abs expr | App expr expr |
7621
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 |
|
10007 | 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 |
10007 | 27 |
has_type :: "(typ list * expr * typ) set" |
7621
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 |
10408 | 30 |
"_has_type" :: "typ list => expr => typ => bool" |
10007 | 31 |
("((_) |-/ (_) :: (_))" [60, 0, 60] 60) |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
32 |
translations |
10146 | 33 |
"a |- e :: t" == "(a, e, t) : has_type" |
7621
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 |
11628 | 36 |
intros |
37 |
Var [simp]: "n < length a ==> a |- Var n :: a ! n" |
|
38 |
Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2" |
|
39 |
App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2 |
|
10007 | 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 |
|
10007 | 43 |
text {* Type assigment is closed wrt.\ substitution. *} |
7761 | 44 |
|
10007 | 45 |
lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t" |
46 |
proof - |
|
47 |
assume "a |- e :: t" |
|
48 |
thus ?thesis (is "?P a e t") |
|
49 |
proof (induct (open) ?P a e t) |
|
50 |
case Var |
|
51 |
hence "n < length (map ($ s) a)" by simp |
|
52 |
hence "map ($ s) a |- Var n :: map ($ s) a ! n" |
|
53 |
by (rule has_type.Var) |
|
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) |
|
58 |
finally show "?P a (Var n) (a ! n)" . |
|
59 |
next |
|
60 |
case Abs |
|
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" |
|
64 |
by (rule has_type.Abs) |
|
65 |
thus "?P a (Abs e) (t1 -> t2)" |
|
66 |
by (simp add: app_subst_list) |
|
67 |
next |
|
68 |
case App |
|
69 |
thus "?P a (App e1 e2) t1" by simp |
|
70 |
qed |
|
71 |
qed |
|
7621
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 |
|
10007 | 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 |
10408 | 77 |
W :: "expr => typ list => nat => (subst * typ * nat) maybe" |
7621
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); |
|
10007 | 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 |
|
10007 | 92 |
subsection {* Correctness theorem *} |
7761 | 93 |
|
10408 | 94 |
theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t" |
95 |
(is "PROP ?P e") |
|
96 |
proof (induct e) |
|
97 |
fix a s t m n |
|
98 |
{ |
|
99 |
fix i |
|
100 |
assume "Ok (s, t, m) = W (Var i) a n" |
|
101 |
thus "$ s a |- Var i :: t" by (simp split: if_splits) |
|
102 |
next |
|
103 |
fix e assume hyp: "PROP ?P e" |
|
104 |
assume "Ok (s, t, m) = W (Abs e) a n" |
|
105 |
then obtain t' where "t = s n -> t'" |
|
106 |
and "Ok (s, t', m) = W e (TVar n # a) (Suc n)" |
|
107 |
by (auto split: bind_splits) |
|
108 |
with hyp show "$ s a |- Abs e :: t" |
|
109 |
by (force intro: has_type.Abs) |
|
110 |
next |
|
111 |
fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2" |
|
112 |
assume "Ok (s, t, m) = W (App e1 e2) a n" |
|
113 |
then obtain s1 t1 n1 s2 t2 n2 u where |
|
8103 | 114 |
s: "s = $ u o $ s2 o s1" |
10408 | 115 |
and t: "t = u n2" |
116 |
and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" |
|
117 |
and W1_ok: "Ok (s1, t1, n1) = W e1 a n" |
|
118 |
and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1" |
|
119 |
by (auto split: bind_splits simp: that) |
|
120 |
show "$ s a |- App e1 e2 :: t" |
|
121 |
proof (rule has_type.App) |
|
122 |
from s have s': "$ u ($ s2 ($ s1 a)) = $s a" |
|
123 |
by (simp add: subst_comp_tel o_def) |
|
124 |
show "$s a |- e1 :: $ u t2 -> t" |
|
125 |
proof - |
|
126 |
from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1) |
|
127 |
hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)" |
|
128 |
by (intro has_type_subst_closed) |
|
129 |
with s' t mgu_ok show ?thesis by simp |
|
10007 | 130 |
qed |
10408 | 131 |
show "$ s a |- e2 :: $ u t2" |
132 |
proof - |
|
133 |
from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2) |
|
134 |
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2" |
|
135 |
by (rule has_type_subst_closed) |
|
136 |
with s' show ?thesis by simp |
|
137 |
qed |
|
138 |
qed |
|
139 |
} |
|
10007 | 140 |
qed |
7621
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
141 |
|
10007 | 142 |
end |