author | wenzelm |
Tue, 28 Sep 1999 14:24:22 +0200 | |
changeset 7621 | 4074bc1e380d |
child 7649 | ae25e28e5ce9 |
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 |
Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow. |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
7 |
*) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
8 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
9 |
theory W_correct = Main + Type:; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
10 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
11 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
12 |
section "Mini ML with type inference rules"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
13 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
14 |
datatype |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
15 |
expr = Var nat | Abs expr | App expr expr; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
16 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
17 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
18 |
text {* type inference rules *}; |
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 |
consts |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
21 |
has_type :: "(typ list * expr * typ) set"; |
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 |
syntax |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
24 |
"@has_type" :: "[typ list, expr, typ] => bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
25 |
translations |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
26 |
"a |- e :: t" == "(a,e,t) : has_type"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
27 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
28 |
inductive has_type |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
29 |
intrs [simp] |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
33 |
==> a |- App e1 e2 :: t1"; |
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 |
theorem has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
36 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
37 |
assume "a |- e :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
38 |
thus ?thesis (is "?P a e t"); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
39 |
proof (rule has_type.induct); (* FIXME induct method *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
40 |
fix a n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
41 |
assume "n < length a"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
42 |
hence "n < length (map ($ s) a)"; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
43 |
hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
44 |
also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
45 |
also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list); (* FIXME unfold fails!? *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
46 |
finally; show "?P a (Var n) (a ! n)"; .; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
47 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
48 |
fix a e t1 t2; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
49 |
assume "?P (t1 # a) e t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
50 |
hence "$ s t1 # map ($ s) a |- e :: $ s t2"; by (simp add: app_subst_list); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
51 |
hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.AbsI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
52 |
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
|
53 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
54 |
fix a e1 e2 t1 t2; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
58 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
59 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
60 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
61 |
section {* Type inference algorithm W *}; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
62 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
63 |
consts |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
66 |
primrec |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
67 |
"W (Var i) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
68 |
(if i < length a then Ok(id_subst, a ! i, n) else Fail)" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
69 |
"W (Abs e) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
70 |
((s, t, m) := W e (TVar n # a) (Suc n); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
71 |
Ok(s, (s n) -> t, m))" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
72 |
"W (App e1 e2) a n = |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
73 |
((s1, t1, m1) := W e1 a n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
74 |
(s2, t2, m2) := W e2 ($s1 a) m1; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
75 |
u := mgu ($ s2 t1) (t2 -> TVar m2); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
76 |
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
|
77 |
|
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 |
(* FIXME proper split att/mod *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
80 |
ML_setup {* Addsplits [split_bind]; *}; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
81 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
82 |
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
|
83 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
84 |
assume W_ok: "W e a n = Ok (s, t, m)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
85 |
let ?P = "%e. ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
86 |
(* FIXME (is ...) fails!? *) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
87 |
have "?P e"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
88 |
proof (induct e); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
89 |
fix n; show "?P (Var n)"; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
90 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
91 |
fix e; assume hyp: "?P e"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
92 |
show "?P (Abs e)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
93 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
94 |
fix a s t m n; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
95 |
assume "Ok (s, t, m) = W (Abs e) a n"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
96 |
hence "EX t'. t = s n -> t' & Ok (s, t', m) = W e (TVar n # a) (Suc n)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
97 |
by (rule rev_mp) simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
98 |
with hyp; show "$ s a |- Abs e :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
99 |
by (force intro: has_type.AbsI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
100 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
101 |
next; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
102 |
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
|
103 |
show "?P (App e1 e2)"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
104 |
proof (intro allI impI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
105 |
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
|
106 |
hence "EX s1 t1 n1 s2 t2 n2 u. |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
107 |
s = $ u o $ s2 o s1 & t = u n2 & |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
108 |
mgu ($ s2 t1) (t2 -> TVar n2) = Ok u & |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
109 |
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
|
110 |
W e1 a n = Ok (s1, t1, n1)"; by (rule rev_mp) (simp, force); (* FIXME force fails !??*) |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
111 |
thus "$ s a |- App e1 e2 :: t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
112 |
proof (elim exE conjE); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
113 |
fix s1 t1 n1 s2 t2 n2 u; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
114 |
assume s: "s = $ u o $ s2 o s1" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
115 |
and t: "t = u n2" |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
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
|
119 |
show ?thesis; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
120 |
proof (rule has_type.AppI); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
121 |
from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; by (simp add: subst_comp_tel o_def); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
122 |
show "$s a |- e1 :: $ u t2 -> t"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
123 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
124 |
from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
125 |
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
|
126 |
by (intro has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
127 |
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
|
128 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
129 |
show "$ s a |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
130 |
proof -; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
131 |
from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
132 |
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
133 |
by (rule has_type_subst_closed); |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
134 |
with s'; show ?thesis; by simp; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
135 |
qed; |
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 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
138 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
139 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
140 |
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
|
141 |
qed; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
142 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
143 |
|
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
144 |
end; |
4074bc1e380d
added W_correct -- correctness of Milner's type inference algorithm W
wenzelm
parents:
diff
changeset
|
145 |