1(*  Title:      ZF/Coind/ECR.thy
2    Author:     Jacob Frost, Cambridge University Computer Laboratory
3    Copyright   1995  University of Cambridge
4*)
5
6theory ECR imports Static Dynamic begin
7
8(* The extended correspondence relation *)
9
10consts
11  HasTyRel :: i
12coinductive
13  domains "HasTyRel" \<subseteq> "Val * Ty"
14  intros
15    htr_constI [intro!]:
16      "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
17    htr_closI [intro]:
18      "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv; 
19          <te,e_fn(x,e),t> \<in> ElabRel;  
20          ve_dom(ve) = te_dom(te);   
21          {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |] 
22       ==> <v_clos(x,e,ve),t> \<in> HasTyRel" 
23  monos  Pow_mono
24  type_intros Val_ValEnv.intros
25  
26(* Pointwise extension to environments *)
27 
28definition
29  hastyenv :: "[i,i] => o"  where
30    "hastyenv(ve,te) ==                        
31         ve_dom(ve) = te_dom(te) &          
32         (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)"
33
34(* Specialised co-induction rule *)
35
36lemma htr_closCI [intro]:
37     "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;   
38         <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);  
39         {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
40           Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel) |]     
41      ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
42apply (rule singletonI [THEN HasTyRel.coinduct], auto)
43done
44
45(* Specialised elimination rules *)
46
47inductive_cases
48    htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
49  and htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel"
50
51
52(* Properties of the pointwise extension to environments *)
53
54lemmas HasTyRel_non_zero =
55       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]
56
57lemma hastyenv_owr: 
58  "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |] 
59   ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
60by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)
61
62lemma basic_consistency_lem: 
63  "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"
64apply (unfold isofenv_def hastyenv_def)
65apply (force intro: te_appI ve_domI) 
66done
67
68
69(* ############################################################ *)
70(* The Consistency theorem                                      *)
71(* ############################################################ *)
72
73lemma consistency_const:
74     "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |] 
75      ==> <v_const(c), t> \<in> HasTyRel"
76by blast
77
78
79lemma consistency_var: 
80  "[| x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel |] ==>      
81   <ve_app(ve,x),t> \<in> HasTyRel"
82by (unfold hastyenv_def, blast)
83
84lemma consistency_fn: 
85  "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; hastyenv(ve,te);        
86           <te,e_fn(x,e),t> \<in> ElabRel   
87        |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel"
88by (unfold hastyenv_def, blast)
89
90declare ElabRel.dom_subset [THEN subsetD, dest]
91
92declare Ty.intros [simp, intro!]
93declare TyEnv.intros [simp, intro!]
94declare Val_ValEnv.intros [simp, intro!]
95
96lemma consistency_fix: 
97  "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;                
98      v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
99      hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>        
100   <cl,t> \<in> HasTyRel"
101apply (unfold hastyenv_def)
102apply (erule elab_fixE, safe)
103apply hypsubst_thin
104apply (rule subst, assumption) 
105apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
106apply simp_all
107apply (blast intro: ve_owrI) 
108apply (rule ElabRel.fnI)
109apply (simp_all add: ValNEE, force)
110done
111
112
113lemma consistency_app1:
114 "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;    
115     <ve,e1,v_const(c1)> \<in> EvalRel;                       
116     \<forall>t te.                                          
117       hastyenv(ve,te) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel;
118     <ve, e2, v_const(c2)> \<in> EvalRel;                   
119     \<forall>t te.                                          
120       hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v_const(c2),t> \<in> HasTyRel;
121     hastyenv(ve, te);                                  
122     <te,e_app(e1,e2),t> \<in> ElabRel |] 
123  ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
124by (blast intro!: c_appI intro: isof_app)
125
126lemma consistency_app2:
127 "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; 
128     v \<in> Val;   
129     <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;        
130     \<forall>t te. hastyenv(ve,te) \<longrightarrow>                     
131            <te,e1,t> \<in> ElabRel \<longrightarrow> <v_clos(xm,em,vem),t> \<in> HasTyRel;         
132     <ve,e2,v2> \<in> EvalRel;                       
133     \<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v2,t> \<in> HasTyRel;
134     <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;         
135     \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow>      
136            <te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel;
137     hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |] 
138   ==> <v,t> \<in> HasTyRel"
139apply (erule elab_appE)
140apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
141apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
142apply (erule htr_closE)
143apply (erule elab_fnE, simp)
144apply clarify
145apply (drule spec [THEN spec, THEN mp, THEN mp])
146prefer 2 apply assumption+
147apply (rule hastyenv_owr, assumption)
148apply assumption 
149apply (simp add: hastyenv_def, blast+)
150done
151
152lemma consistency [rule_format]:
153   "<ve,e,v> \<in> EvalRel 
154    ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
155apply (erule EvalRel.induct)
156apply (simp_all add: consistency_const consistency_var consistency_fn 
157                     consistency_fix consistency_app1)
158apply (blast intro: consistency_app2)
159done
160
161lemma basic_consistency:
162     "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te);                    
163         <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |] 
164      ==> isof(c,t)"
165by (blast dest: consistency intro!: basic_consistency_lem)
166
167end
168