969
|
1 |
(* Title: HOL/ex/mt.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Jacob Frost, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Based upon the article
|
|
7 |
Robin Milner and Mads Tofte,
|
|
8 |
Co-induction in Relational Semantics,
|
|
9 |
Theoretical Computer Science 87 (1991), pages 209-220.
|
|
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 |
|
|
16 |
MT = Gfp + Sum +
|
|
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
|
|
49 |
c_app :: "[Const, Const] => Const"
|
|
50 |
|
|
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"
|
|
57 |
|
|
58 |
t_const :: "TyConst => Ty"
|
|
59 |
t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
|
|
60 |
|
|
61 |
v_const :: "Const => Val"
|
|
62 |
v_clos :: "Clos => Val"
|
|
63 |
|
|
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"
|
|
68 |
|
|
69 |
clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
|
|
70 |
|
|
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"
|
|
75 |
|
|
76 |
eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
|
|
77 |
eval_rel :: "((ValEnv * Ex) * Val) set"
|
|
78 |
eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
|
|
79 |
|
|
80 |
elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
|
|
81 |
elab_rel :: "((TyEnv * Ex) * Ty) set"
|
|
82 |
elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
|
|
83 |
|
|
84 |
isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
|
|
85 |
isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
|
|
86 |
|
|
87 |
hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
|
|
88 |
hasty_rel :: "(Val * Ty) set"
|
|
89 |
hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
|
|
90 |
hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
|
|
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
|
|
105 |
" fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \
|
|
106 |
\ ev11 = ev21 & ev12 = ev22 & e1 = e2 \
|
|
107 |
\ "
|
|
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
|
|
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 |
\ "
|
|
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
|
|
147 |
"[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] \
|
|
148 |
\ ==> P(t)"
|
|
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
|
|
157 |
" v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \
|
|
158 |
\ ev1 = ev2 & e1 = e2 & ve1 = ve2"
|
|
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
|
|
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 |
\ }"
|
|
217 |
|
|
218 |
eval_rel_def "eval_rel == lfp(eval_fun)"
|
|
219 |
eval_def "ve |- e ---> v == <<ve,e>,v>:eval_rel"
|
|
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
|
|
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 |
\ }"
|
|
239 |
|
|
240 |
elab_rel_def "elab_rel == lfp(elab_fun)"
|
|
241 |
elab_def "te |- e ===> t == <<te,e>,t>:elab_rel"
|
|
242 |
|
|
243 |
(* The original correspondence relation *)
|
|
244 |
|
|
245 |
isof_env_def
|
|
246 |
" ve isofenv te == \
|
|
247 |
\ ve_dom(ve) = te_dom(te) & \
|
|
248 |
\ ( ! x. \
|
|
249 |
\ x:ve_dom(ve) --> \
|
|
250 |
\ (? c.ve_app ve x = v_const(c) & c isof te_app te x) \
|
|
251 |
\ ) \
|
|
252 |
\ "
|
|
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
|
|
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) & \
|
|
266 |
\ (! ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : r) \
|
|
267 |
\ ) \
|
|
268 |
\ } \
|
|
269 |
\ "
|
|
270 |
|
|
271 |
hasty_rel_def "hasty_rel == gfp(hasty_fun)"
|
|
272 |
hasty_def "v hasty t == <v,t> : hasty_rel"
|
|
273 |
hasty_env_def
|
|
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)"
|
|
277 |
|
|
278 |
end
|