author | wenzelm |
Sun, 30 Jan 2011 13:02:18 +0100 | |
changeset 41648 | 6d736d983d5c |
parent 32960 | 69916a850301 |
child 41779 | a68f503805ed |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Coind/Static.thy |
2 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
|
916 | 3 |
Copyright 1995 University of Cambridge |
4 |
*) |
|
5 |
||
16417 | 6 |
theory Static imports Values Types begin |
12595 | 7 |
|
8 |
(*** Basic correspondence relation -- not completely specified, as it is a |
|
9 |
parameter of the proof. A concrete version could be defined inductively. |
|
10 |
***) |
|
11 |
||
12 |
consts |
|
13 |
isof :: "[i,i] => o" |
|
14 |
||
15 |
axioms |
|
16 |
isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)" |
|
17 |
||
18 |
(*Its extension to environments*) |
|
19 |
||
24893 | 20 |
definition |
21 |
isofenv :: "[i,i] => o" where |
|
12595 | 22 |
"isofenv(ve,te) == |
23 |
ve_dom(ve) = te_dom(te) & |
|
24 |
(\<forall>x \<in> ve_dom(ve). |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
25 |
\<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))" |
12595 | 26 |
|
27 |
||
28 |
(*** Elaboration ***) |
|
916 | 29 |
|
6141 | 30 |
consts ElabRel :: i |
31 |
||
916 | 32 |
inductive |
33 |
domains "ElabRel" <= "TyEnv * Exp * Ty" |
|
12595 | 34 |
intros |
35 |
constI [intro!]: |
|
36 |
"[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==> |
|
37 |
<te,e_const(c),t> \<in> ElabRel" |
|
38 |
varI [intro!]: |
|
39 |
"[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> |
|
40 |
<te,e_var(x),te_app(te,x)> \<in> ElabRel" |
|
41 |
fnI [intro!]: |
|
42 |
"[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; |
|
43 |
<te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==> |
|
44 |
<te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel" |
|
45 |
fixI [intro!]: |
|
46 |
"[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty; |
|
47 |
<te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==> |
|
48 |
<te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel" |
|
49 |
appI [intro]: |
|
50 |
"[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty; |
|
51 |
<te,e1,t_fun(t1,t2)> \<in> ElabRel; |
|
52 |
<te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel" |
|
53 |
type_intros te_appI Exp.intros Ty.intros |
|
54 |
||
55 |
||
12610 | 56 |
inductive_cases |
57 |
elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel" |
|
58 |
and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel" |
|
59 |
and elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel" |
|
60 |
and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel" |
|
61 |
and elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel" |
|
12595 | 62 |
|
63 |
declare ElabRel.dom_subset [THEN subsetD, dest] |
|
916 | 64 |
|
65 |
end |
|
66 |
||
67 |
||
68 |
||
69 |
||
70 |
||
71 |
||
72 |