author  wenzelm 
Sat, 30 Oct 1999 20:20:48 +0200  
changeset 7982  d534b897ce39 
parent 7968  964b65b4e433 
child 8103  86f94a8116a9 
permissions  rwrr 
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 (letfree 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 (letfree 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; 