author  wenzelm 
Fri, 28 Sep 2001 19:19:26 +0200  
changeset 11628  e57a6e51715e 
parent 10408  d8b3613158b1 
child 11809  c9ffdd63dd93 
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 

10007  8 
header {* Milner's type inference algorithm~W (letfree 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 