2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 Static = BCR + |
7 theory Static = Values + Types: |
|
8 |
|
9 (*** Basic correspondence relation -- not completely specified, as it is a |
|
10 parameter of the proof. A concrete version could be defined inductively. |
|
11 ***) |
|
12 |
|
13 consts |
|
14 isof :: "[i,i] => o" |
|
15 |
|
16 axioms |
|
17 isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)" |
|
18 |
|
19 (*Its extension to environments*) |
|
20 |
|
21 constdefs |
|
22 isofenv :: "[i,i] => o" |
|
23 "isofenv(ve,te) == |
|
24 ve_dom(ve) = te_dom(te) & |
|
25 (\<forall>x \<in> ve_dom(ve). |
|
26 \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))" |
|
27 |
|
28 |
|
29 (*** Elaboration ***) |
8 |
30 |
9 consts ElabRel :: i |
31 consts ElabRel :: i |
10 |
32 |
11 inductive |
33 inductive |
12 domains "ElabRel" <= "TyEnv * Exp * Ty" |
34 domains "ElabRel" <= "TyEnv * Exp * Ty" |
13 intrs |
35 intros |
14 constI |
36 constI [intro!]: |
15 " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> |
37 "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==> |
16 <te,e_const(c),t>:ElabRel " |
38 <te,e_const(c),t> \<in> ElabRel" |
17 varI |
39 varI [intro!]: |
18 " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> |
40 "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> |
19 <te,e_var(x),te_app(te,x)>:ElabRel " |
41 <te,e_var(x),te_app(te,x)> \<in> ElabRel" |
20 fnI |
42 fnI [intro!]: |
21 " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty; |
43 "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; |
22 <te_owr(te,x,t1),e,t2>:ElabRel |] ==> |
44 <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==> |
23 <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel " |
45 <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel" |
24 fixI |
46 fixI [intro!]: |
25 " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty; |
47 "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty; |
26 <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==> |
48 <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==> |
27 <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel " |
49 <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel" |
28 appI |
50 appI [intro]: |
29 " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty; |
51 "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; |
30 <te,e1,t_fun(t1,t2)>:ElabRel; |
52 <te,e1,t_fun(t1,t2)> \<in> ElabRel; |
31 <te,e2,t1>:ElabRel |] ==> |
53 <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel" |
32 <te,e_app(e1,e2),t2>:ElabRel " |
54 type_intros te_appI Exp.intros Ty.intros |
33 type_intrs "te_appI::Exp.intrs@Ty.intrs" |
55 |
|
56 |
|
57 inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel" |
|
58 inductive_cases elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel" |
|
59 inductive_cases elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel" |
|
60 inductive_cases elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel" |
|
61 inductive_cases elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel" |
|
62 |
|
63 declare ElabRel.dom_subset [THEN subsetD, dest] |
34 |
64 |
35 end |
65 end |
36 |
66 |
37 |
67 |
38 |
68 |