1(*  Title:      ZF/Coind/Static.thy
2    Author:     Jacob Frost, Cambridge University Computer Laboratory
3    Copyright   1995  University of Cambridge
4*)
5
6theory Static imports Values Types begin
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
12axiomatization isof :: "[i,i] => o"
13  where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
14
15(*Its extension to environments*)
16
17definition
18  isofenv :: "[i,i] => o"  where
19   "isofenv(ve,te) ==                
20      ve_dom(ve) = te_dom(te) &            
21      (\<forall>x \<in> ve_dom(ve).                          
22        \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
23  
24
25(*** Elaboration ***)
26
27consts  ElabRel :: i
28
29inductive
30  domains "ElabRel" \<subseteq> "TyEnv * Exp * Ty"
31  intros
32    constI [intro!]:
33      "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>   
34       <te,e_const(c),t> \<in> ElabRel"
35    varI [intro!]:
36      "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==>   
37       <te,e_var(x),te_app(te,x)> \<in> ElabRel"
38    fnI [intro!]:
39      "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
40          <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==>   
41       <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel"
42    fixI [intro!]:
43      "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty;   
44          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==>   
45       <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel"
46    appI [intro]:
47      "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
48          <te,e1,t_fun(t1,t2)> \<in> ElabRel;   
49          <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel"
50  type_intros te_appI Exp.intros Ty.intros
51
52
53inductive_cases
54    elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
55  and elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
56  and elab_fnE [elim]:   "<te,e_fn(x,e),t> \<in> ElabRel"
57  and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
58  and elab_appE [elim]:  "<te,e_app(e1,e2),t> \<in> ElabRel"
59
60declare ElabRel.dom_subset [THEN subsetD, dest]
61
62end
63
64
65
66
67
68
69
70