author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5102  8c782c25a11e 
child 12338  de0f4a63baa5 
permissions  rwrr 
1476  1 
(* Title: HOL/ex/mt.thy 
969  2 
ID: $Id$ 
1476  3 
Author: Jacob Frost, Cambridge University Computer Laboratory 
969  4 
Copyright 1993 University of Cambridge 
5 

6 
Based upon the article 

7 
Robin Milner and Mads Tofte, 

8 
Coinduction in Relational Semantics, 

9 
Theoretical Computer Science 87 (1991), pages 209220. 

10 

11 
Written up as 

12 
Jacob Frost, A Case Study of Co_induction in Isabelle/HOL 

13 
Report 308, Computer Lab, University of Cambridge (1993). 

14 
*) 

15 

5102  16 
MT = Inductive + 
969  17 

18 
types 

19 
Const 

20 

21 
ExVar 

22 
Ex 

23 

24 
TyConst 

25 
Ty 

26 

27 
Clos 

28 
Val 

29 

30 
ValEnv 

31 
TyEnv 

32 

33 
arities 

34 
Const :: term 

35 

36 
ExVar :: term 

37 
Ex :: term 

38 

39 
TyConst :: term 

40 
Ty :: term 

41 

42 
Clos :: term 

43 
Val :: term 

44 

45 
ValEnv :: term 

46 
TyEnv :: term 

47 

48 
consts 

1376  49 
c_app :: [Const, Const] => Const 
969  50 

1376  51 
e_const :: Const => Ex 
52 
e_var :: ExVar => Ex 

53 
e_fn :: [ExVar, Ex] => Ex ("fn _ => _" [0,51] 1000) 

54 
e_fix :: [ExVar, ExVar, Ex] => Ex ("fix _ ( _ ) = _" [0,51,51] 1000) 

55 
e_app :: [Ex, Ex] => Ex ("_ @ _" [51,51] 1000) 

56 
e_const_fst :: Ex => Const 

969  57 

1376  58 
t_const :: TyConst => Ty 
59 
t_fun :: [Ty, Ty] => Ty ("_ > _" [51,51] 1000) 

969  60 

1376  61 
v_const :: Const => Val 
62 
v_clos :: Clos => Val 

969  63 

1376  64 
ve_emp :: ValEnv 
65 
ve_owr :: [ValEnv, ExVar, Val] => ValEnv ("_ + { _ > _ }" [36,0,0] 50) 

66 
ve_dom :: ValEnv => ExVar set 

67 
ve_app :: [ValEnv, ExVar] => Val 

969  68 

1376  69 
clos_mk :: [ExVar, Ex, ValEnv] => Clos ("< _ , _ , _ >" [0,0,0] 1000) 
969  70 

1376  71 
te_emp :: TyEnv 
72 
te_owr :: [TyEnv, ExVar, Ty] => TyEnv ("_ + { _ => _ }" [36,0,0] 50) 

73 
te_app :: [TyEnv, ExVar] => Ty 

74 
te_dom :: TyEnv => ExVar set 

969  75 

76 
eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set" 

77 
eval_rel :: "((ValEnv * Ex) * Val) set" 

1376  78 
eval :: [ValEnv, Ex, Val] => bool ("_  _ > _" [36,0,36] 50) 
969  79 

80 
elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" 

81 
elab_rel :: "((TyEnv * Ex) * Ty) set" 

1376  82 
elab :: [TyEnv, Ex, Ty] => bool ("_  _ ===> _" [36,0,36] 50) 
969  83 

1376  84 
isof :: [Const, Ty] => bool ("_ isof _" [36,36] 50) 
85 
isof_env :: [ValEnv,TyEnv] => bool ("_ isofenv _") 

969  86 

87 
hasty_fun :: "(Val * Ty) set => (Val * Ty) set" 

88 
hasty_rel :: "(Val * Ty) set" 

1376  89 
hasty :: [Val, Ty] => bool ("_ hasty _" [36,36] 50) 
90 
hasty_env :: [ValEnv,TyEnv] => bool ("_ hastyenv _ " [36,36] 35) 

969  91 

92 
rules 

93 

94 
(* 

95 
Expression constructors must be injective, distinct and it must be possible 

96 
to do induction over expressions. 

97 
*) 

98 

99 
(* All the constructors are injective *) 

100 

101 
e_const_inj "e_const(c1) = e_const(c2) ==> c1 = c2" 

102 
e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" 

103 
e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" 

104 
e_fix_inj 

1151  105 
" fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> 
106 
ev11 = ev21 & ev12 = ev22 & e1 = e2 

107 
" 

969  108 
e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22" 
109 

110 
(* All constructors are distinct *) 

111 

112 
e_disj_const_var "~e_const(c) = e_var(ev)" 

113 
e_disj_const_fn "~e_const(c) = fn ev => e" 

114 
e_disj_const_fix "~e_const(c) = fix ev1(ev2) = e" 

115 
e_disj_const_app "~e_const(c) = e1 @ e2" 

116 
e_disj_var_fn "~e_var(ev1) = fn ev2 => e" 

117 
e_disj_var_fix "~e_var(ev) = fix ev1(ev2) = e" 

118 
e_disj_var_app "~e_var(ev) = e1 @ e2" 

119 
e_disj_fn_fix "~fn ev1 => e1 = fix ev21(ev22) = e2" 

120 
e_disj_fn_app "~fn ev1 => e1 = e21 @ e22" 

121 
e_disj_fix_app "~fix ev11(ev12) = e1 = e21 @ e22" 

122 

123 
(* Strong elimination, induction on expressions *) 

124 

125 
e_ind 

1151  126 
" [ !!ev. P(e_var(ev)); 
127 
!!c. P(e_const(c)); 

128 
!!ev e. P(e) ==> P(fn ev => e); 

129 
!!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); 

130 
!!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) 

131 
] ==> 

132 
P(e) 

133 
" 

969  134 

135 
(* Types  same scheme as for expressions *) 

136 

137 
(* All constructors are injective *) 

138 

139 
t_const_inj "t_const(c1) = t_const(c2) ==> c1 = c2" 

140 
t_fun_inj "t11 > t12 = t21 > t22 ==> t11 = t21 & t12 = t22" 

141 

142 
(* All constructors are distinct, not needed so far ... *) 

143 

144 
(* Strong elimination, induction on types *) 

145 

146 
t_ind 

1151  147 
"[ !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) ] 
148 
==> P(t)" 

969  149 

150 

151 
(* Values  same scheme again *) 

152 

153 
(* All constructors are injective *) 

154 

155 
v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2" 

156 
v_clos_inj 

1151  157 
" v_clos(<ev1,e1,ve1>) = v_clos(<ev2,e2,ve2>) ==> 
158 
ev1 = ev2 & e1 = e2 & ve1 = ve2" 

969  159 

160 
(* All constructors are distinct *) 

161 

162 
v_disj_const_clos "~v_const(c) = v_clos(cl)" 

163 

164 
(* Strong elimination, induction on values, not needed yet ... *) 

165 

166 

167 
(* 

168 
Value environments bind variables to values. Only the following trivial 

169 
properties are needed. 

170 
*) 

171 

172 
ve_dom_owr "ve_dom(ve + {ev > v}) = ve_dom(ve) Un {ev}" 

173 

174 
ve_app_owr1 "ve_app (ve + {ev > v}) ev=v" 

175 
ve_app_owr2 "~ev1=ev2 ==> ve_app (ve+{ev1 > v}) ev2=ve_app ve ev2" 

176 

177 

178 
(* Type Environments bind variables to types. The following trivial 

179 
properties are needed. *) 

180 

181 
te_dom_owr "te_dom(te + {ev => t}) = te_dom(te) Un {ev}" 

182 

183 
te_app_owr1 "te_app (te + {ev => t}) ev=t" 

184 
te_app_owr2 "~ev1=ev2 ==> te_app (te+{ev1 => t}) ev2=te_app te ev2" 

185 

186 

187 
(* The dynamic semantics is defined inductively by a set of inference 

188 
rules. These inference rules allows one to draw conclusions of the form ve 

189 
 e > v, read the expression e evaluates to the value v in the value 

190 
environment ve. Therefore the relation _  _ > _ is defined in Isabelle 

191 
as the least fixpoint of the functor eval_fun below. From this definition 

192 
introduction rules and a strong elimination (induction) rule can be 

193 
derived. 

194 
*) 

195 

196 
eval_fun_def 

1151  197 
" eval_fun(s) == 
198 
{ pp. 

199 
(? ve c. pp=((ve,e_const(c)),v_const(c)))  

200 
(? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve))  

201 
(? ve e x. pp=((ve,fn x => e),v_clos(<x,e,ve>))) 

202 
( ? ve e x f cl. 

203 
pp=((ve,fix f(x) = e),v_clos(cl)) & 

204 
cl=<x, e, ve+{f > v_clos(cl)} > 

205 
)  

206 
( ? ve e1 e2 c1 c2. 

207 
pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & 

208 
((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s 

209 
)  

210 
( ? ve vem e1 e2 em xm v v2. 

211 
pp=((ve,e1 @ e2),v) & 

212 
((ve,e1),v_clos(<xm,em,vem>)):s & 

213 
((ve,e2),v2):s & 

214 
((vem+{xm > v2},em),v):s 

215 
) 

216 
}" 

969  217 

218 
eval_rel_def "eval_rel == lfp(eval_fun)" 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

219 
eval_def "ve  e > v == ((ve,e),v):eval_rel" 
969  220 

221 
(* The static semantics is defined in the same way as the dynamic 

222 
semantics. The relation te  e ===> t express the expression e has the 

223 
type t in the type environment te. 

224 
*) 

225 

226 
elab_fun_def 

1151  227 
"elab_fun(s) == 
228 
{ pp. 

229 
(? te c t. pp=((te,e_const(c)),t) & c isof t)  

230 
(? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te))  

231 
(? te x e t1 t2. pp=((te,fn x => e),t1>t2) & ((te+{x => t1},e),t2):s)  

232 
(? te f x e t1 t2. 

233 
pp=((te,fix f(x)=e),t1>t2) & ((te+{f => t1>t2}+{x => t1},e),t2):s 

234 
)  

235 
(? te e1 e2 t1 t2. 

236 
pp=((te,e1 @ e2),t2) & ((te,e1),t1>t2):s & ((te,e2),t1):s 

237 
) 

238 
}" 

969  239 

240 
elab_rel_def "elab_rel == lfp(elab_fun)" 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

241 
elab_def "te  e ===> t == ((te,e),t):elab_rel" 
969  242 

243 
(* The original correspondence relation *) 

244 

245 
isof_env_def 

1151  246 
" ve isofenv te == 
247 
ve_dom(ve) = te_dom(te) & 

248 
( ! x. 

249 
x:ve_dom(ve) > 

3842  250 
(? c. ve_app ve x = v_const(c) & c isof te_app te x) 
1151  251 
) 
252 
" 

969  253 

254 
isof_app "[ c1 isof t1>t2; c2 isof t1 ] ==> c_app c1 c2 isof t2" 

255 

256 
(* The extented correspondence relation *) 

257 

258 
hasty_fun_def 

1151  259 
" hasty_fun(r) == 
260 
{ p. 

261 
( ? c t. p = (v_const(c),t) & c isof t)  

262 
( ? ev e ve t te. 

263 
p = (v_clos(<ev,e,ve>),t) & 

264 
te  fn ev => e ===> t & 

265 
ve_dom(ve) = te_dom(te) & 

3842  266 
(! ev1. ev1:ve_dom(ve) > (ve_app ve ev1,te_app te ev1) : r) 
1151  267 
) 
268 
} 

269 
" 

969  270 

271 
hasty_rel_def "hasty_rel == gfp(hasty_fun)" 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

272 
hasty_def "v hasty t == (v,t) : hasty_rel" 
969  273 
hasty_env_def 
1151  274 
" ve hastyenv te == 
275 
ve_dom(ve) = te_dom(te) & 

276 
(! x. x: ve_dom(ve) > ve_app ve x hasty te_app te x)" 

969  277 

278 
end 