58 te_emp :: TyEnv |
58 te_emp :: TyEnv |
59 te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50) |
59 te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50) |
60 te_app :: "[TyEnv, ExVar] => Ty" |
60 te_app :: "[TyEnv, ExVar] => Ty" |
61 te_dom :: "TyEnv => ExVar set" |
61 te_dom :: "TyEnv => ExVar set" |
62 |
62 |
63 eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set" |
|
64 eval_rel :: "((ValEnv * Ex) * Val) set" |
|
65 eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50) |
|
66 |
|
67 elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" |
|
68 elab_rel :: "((TyEnv * Ex) * Ty) set" |
|
69 elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50) |
|
70 |
|
71 isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) |
63 isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) |
72 isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") |
|
73 |
|
74 hasty_fun :: "(Val * Ty) set => (Val * Ty) set" |
|
75 hasty_rel :: "(Val * Ty) set" |
|
76 hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) |
|
77 hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) |
|
78 |
64 |
79 (* |
65 (* |
80 Expression constructors must be injective, distinct and it must be possible |
66 Expression constructors must be injective, distinct and it must be possible |
81 to do induction over expressions. |
67 to do induction over expressions. |
82 *) |
68 *) |
206 ((ve,e2),v2):s & |
191 ((ve,e2),v2):s & |
207 ((vem+{xm |-> v2},em),v):s |
192 ((vem+{xm |-> v2},em),v):s |
208 ) |
193 ) |
209 }" |
194 }" |
210 |
195 |
211 eval_rel_def: "eval_rel == lfp(eval_fun)" |
196 definition eval_rel :: "((ValEnv * Ex) * Val) set" |
212 eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel" |
197 where "eval_rel == lfp(eval_fun)" |
|
198 |
|
199 definition eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50) |
|
200 where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel" |
213 |
201 |
214 (* The static semantics is defined in the same way as the dynamic |
202 (* The static semantics is defined in the same way as the dynamic |
215 semantics. The relation te |- e ===> t express the expression e has the |
203 semantics. The relation te |- e ===> t express the expression e has the |
216 type t in the type environment te. |
204 type t in the type environment te. |
217 *) |
205 *) |
218 |
206 |
219 elab_fun_def: |
207 definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" |
220 "elab_fun(s) == |
208 where "elab_fun(s) == |
221 { pp. |
209 { pp. |
222 (? te c t. pp=((te,e_const(c)),t) & c isof t) | |
210 (? te c t. pp=((te,e_const(c)),t) & c isof t) | |
223 (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | |
211 (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | |
224 (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | |
212 (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | |
225 (? te f x e t1 t2. |
213 (? te f x e t1 t2. |
226 pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s |
214 pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s |
227 ) | |
215 ) | |
228 (? te e1 e2 t1 t2. |
216 (? te e1 e2 t1 t2. |
229 pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s |
217 pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s |
230 ) |
218 ) |
231 }" |
219 }" |
232 |
220 |
233 elab_rel_def: "elab_rel == lfp(elab_fun)" |
221 definition elab_rel :: "((TyEnv * Ex) * Ty) set" |
234 elab_def: "te |- e ===> t == ((te,e),t):elab_rel" |
222 where "elab_rel == lfp(elab_fun)" |
|
223 |
|
224 definition elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50) |
|
225 where "te |- e ===> t == ((te,e),t):elab_rel" |
|
226 |
235 |
227 |
236 (* The original correspondence relation *) |
228 (* The original correspondence relation *) |
237 |
229 |
238 isof_env_def: |
230 definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") |
239 " ve isofenv te == |
231 where "ve isofenv te == |
240 ve_dom(ve) = te_dom(te) & |
232 ve_dom(ve) = te_dom(te) & |
241 ( ! x. |
233 (! x. |
242 x:ve_dom(ve) --> |
234 x:ve_dom(ve) --> |
243 (? c. ve_app ve x = v_const(c) & c isof te_app te x) |
235 (? c. ve_app ve x = v_const(c) & c isof te_app te x))" |
244 ) |
|
245 " |
|
246 |
236 |
247 axiomatization where |
237 axiomatization where |
248 isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2" |
238 isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2" |
249 |
239 |
250 defs |
240 |
251 (* The extented correspondence relation *) |
241 (* The extented correspondence relation *) |
252 |
242 |
253 hasty_fun_def: |
243 definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set" |
254 " hasty_fun(r) == |
244 where "hasty_fun(r) == |
255 { p. |
245 { p. |
256 ( ? c t. p = (v_const(c),t) & c isof t) | |
246 ( ? c t. p = (v_const(c),t) & c isof t) | |
257 ( ? ev e ve t te. |
247 ( ? ev e ve t te. |
258 p = (v_clos(<|ev,e,ve|>),t) & |
248 p = (v_clos(<|ev,e,ve|>),t) & |
259 te |- fn ev => e ===> t & |
249 te |- fn ev => e ===> t & |
260 ve_dom(ve) = te_dom(te) & |
250 ve_dom(ve) = te_dom(te) & |
261 (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) |
251 (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) |
262 ) |
252 ) |
263 } |
253 }" |
264 " |
254 |
265 |
255 definition hasty_rel :: "(Val * Ty) set" |
266 hasty_rel_def: "hasty_rel == gfp(hasty_fun)" |
256 where "hasty_rel == gfp(hasty_fun)" |
267 hasty_def: "v hasty t == (v,t) : hasty_rel" |
257 |
268 hasty_env_def: |
258 definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) |
269 " ve hastyenv te == |
259 where "v hasty t == (v,t) : hasty_rel" |
270 ve_dom(ve) = te_dom(te) & |
260 |
271 (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)" |
261 definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) |
|
262 where "ve hastyenv te == |
|
263 ve_dom(ve) = te_dom(te) & |
|
264 (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)" |
272 |
265 |
273 |
266 |
274 (* ############################################################ *) |
267 (* ############################################################ *) |
275 (* Inference systems *) |
268 (* Inference systems *) |
276 (* ############################################################ *) |
269 (* ############################################################ *) |