author | paulson |
Fri, 21 Jan 2005 13:54:09 +0100 | |
changeset 15450 | 43dfc914d1b8 |
parent 12338 | de0f4a63baa5 |
child 17289 | 8608f7a881eb |
permissions | -rw-r--r-- |
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 |
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 |
||
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 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
34 |
Const :: type |
969 | 35 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
36 |
ExVar :: type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
37 |
Ex :: type |
969 | 38 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
39 |
TyConst :: type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
40 |
Ty :: type |
969 | 41 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
42 |
Clos :: type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
43 |
Val :: type |
969 | 44 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
45 |
ValEnv :: type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
5102
diff
changeset
|
46 |
TyEnv :: type |
969 | 47 |
|
48 |
consts |
|
15450 | 49 |
c_app :: "[Const, Const] => Const" |
969 | 50 |
|
15450 | 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 |
|
15450 | 58 |
t_const :: "TyConst => Ty" |
59 |
t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000) |
|
969 | 60 |
|
15450 | 61 |
v_const :: "Const => Val" |
62 |
v_clos :: "Clos => Val" |
|
969 | 63 |
|
1376 | 64 |
ve_emp :: ValEnv |
15450 | 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 |
|
15450 | 69 |
clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000) |
969 | 70 |
|
1376 | 71 |
te_emp :: TyEnv |
15450 | 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" |
|
15450 | 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" |
|
15450 | 82 |
elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50) |
969 | 83 |
|
15450 | 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" |
|
15450 | 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 |
||
15450 | 164 |
(* No induction on values: they are a codatatype! ... *) |
969 | 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 |