Theory ECR

(*  Title:      ZF/Coind/ECR.thy
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

theory ECR imports Static Dynamic begin

(* The extended correspondence relation *)

consts
  HasTyRel :: i
coinductive
  domains "HasTyRel" ⊆ "Val * Ty"
  intros
    htr_constI [intro!]:
      "⟦c ∈ Const; t ∈ Ty; isof(c,t)⟧ ⟹ <v_const(c),t> ∈ HasTyRel"
    htr_closI [intro]:
      "⟦x ∈ ExVar; e ∈ Exp; t ∈ Ty; ve ∈ ValEnv; te ∈ TyEnv; 
          <te,e_fn(x,e),t> ∈ ElabRel;  
          ve_dom(ve) = te_dom(te);   
          {<ve_app(ve,y),te_app(te,y)>.y ∈ ve_dom(ve)} ∈ Pow(HasTyRel)⟧ 
       ⟹ <v_clos(x,e,ve),t> ∈ HasTyRel" 
  monos  Pow_mono
  type_intros Val_ValEnv.intros
  
(* Pointwise extension to environments *)
 
definition
  hastyenv :: "[i,i] ⇒ o"  where
    "hastyenv(ve,te) ≡                        
         ve_dom(ve) = te_dom(te) ∧          
         (∀x ∈ ve_dom(ve). <ve_app(ve,x),te_app(te,x)> ∈ HasTyRel)"

(* Specialised co-induction rule *)

lemma htr_closCI [intro]:
     "⟦x ∈ ExVar; e ∈ Exp; t ∈ Ty; ve ∈ ValEnv; te ∈ TyEnv;   
         <te, e_fn(x, e), t> ∈ ElabRel; ve_dom(ve) = te_dom(te);  
         {<ve_app(ve,y),te_app(te,y)>.y ∈ ve_dom(ve)} ∈
           Pow({<v_clos(x,e,ve),t>} ∪ HasTyRel)⟧     
      ⟹ <v_clos(x, e, ve),t> ∈ HasTyRel"
apply (rule singletonI [THEN HasTyRel.coinduct], auto)
done

(* Specialised elimination rules *)

inductive_cases
    htr_constE [elim!]: "<v_const(c),t> ∈ HasTyRel"
  and htr_closE [elim]: "<v_clos(x,e,ve),t> ∈ HasTyRel"


(* Properties of the pointwise extension to environments *)

lemmas HasTyRel_non_zero =
       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]

lemma hastyenv_owr: 
  "⟦ve ∈ ValEnv; te ∈ TyEnv; hastyenv(ve,te); ⟨v,t⟩ ∈ HasTyRel⟧ 
   ⟹ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)

lemma basic_consistency_lem: 
  "⟦ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve,te)⟧ ⟹ hastyenv(ve,te)"
  unfolding isofenv_def hastyenv_def
apply (force intro: te_appI ve_domI) 
done


(* ############################################################ *)
(* The Consistency theorem                                      *)
(* ############################################################ *)

lemma consistency_const:
     "⟦c ∈ Const; hastyenv(ve,te);<te,e_const(c),t> ∈ ElabRel⟧ 
      ⟹ <v_const(c), t> ∈ HasTyRel"
by blast


lemma consistency_var: 
  "⟦x ∈ ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> ∈ ElabRel⟧ ⟹      
   <ve_app(ve,x),t> ∈ HasTyRel"
by (unfold hastyenv_def, blast)

lemma consistency_fn: 
  "⟦ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; hastyenv(ve,te);        
           <te,e_fn(x,e),t> ∈ ElabRel   
⟧ ⟹ <v_clos(x, e, ve), t> ∈ HasTyRel"
by (unfold hastyenv_def, blast)

declare ElabRel.dom_subset [THEN subsetD, dest]

declare Ty.intros [simp, intro!]
declare TyEnv.intros [simp, intro!]
declare Val_ValEnv.intros [simp, intro!]

lemma consistency_fix: 
  "⟦ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; f ∈ ExVar; cl ∈ Val;                
      v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
      hastyenv(ve,te); <te,e_fix(f,x,e),t> ∈ ElabRel⟧ ⟹        
   ⟨cl,t⟩ ∈ HasTyRel"
  unfolding hastyenv_def
apply (erule elab_fixE, safe)
apply hypsubst_thin
apply (rule subst, assumption) 
apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
apply simp_all
apply (blast intro: ve_owrI) 
apply (rule ElabRel.fnI)
apply (simp_all add: ValNEE, force)
done


lemma consistency_app1:
 "⟦ve ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; c1 ∈ Const; c2 ∈ Const;    
     <ve,e1,v_const(c1)> ∈ EvalRel;                       
     ∀t te.                                          
       hastyenv(ve,te) ⟶ <te,e1,t> ∈ ElabRel ⟶ <v_const(c1),t> ∈ HasTyRel;
     <ve, e2, v_const(c2)> ∈ EvalRel;                   
     ∀t te.                                          
       hastyenv(ve,te) ⟶ <te,e2,t> ∈ ElabRel ⟶ <v_const(c2),t> ∈ HasTyRel;
     hastyenv(ve, te);                                  
     <te,e_app(e1,e2),t> ∈ ElabRel⟧ 
  ⟹ <v_const(c_app(c1, c2)),t> ∈ HasTyRel"
by (blast intro!: c_appI intro: isof_app)

lemma consistency_app2:
 "⟦ve ∈ ValEnv; vem ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; em ∈ Exp; xm ∈ ExVar; 
     v ∈ Val;   
     <ve,e1,v_clos(xm,em,vem)> ∈ EvalRel;        
     ∀t te. hastyenv(ve,te) ⟶                     
            <te,e1,t> ∈ ElabRel ⟶ <v_clos(xm,em,vem),t> ∈ HasTyRel;         
     <ve,e2,v2> ∈ EvalRel;                       
     ∀t te. hastyenv(ve,te) ⟶ <te,e2,t> ∈ ElabRel ⟶ ⟨v2,t⟩ ∈ HasTyRel;
     <ve_owr(vem,xm,v2),em,v> ∈ EvalRel;         
     ∀t te. hastyenv(ve_owr(vem,xm,v2),te) ⟶      
            <te,em,t> ∈ ElabRel ⟶ ⟨v,t⟩ ∈ HasTyRel;
     hastyenv(ve,te); <te,e_app(e1,e2),t> ∈ ElabRel⟧ 
   ⟹ ⟨v,t⟩ ∈ HasTyRel"
apply (erule elab_appE)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (erule htr_closE)
apply (erule elab_fnE, simp)
apply clarify
apply (drule spec [THEN spec, THEN mp, THEN mp])
prefer 2 apply assumption+
apply (rule hastyenv_owr, assumption)
apply assumption 
apply (simp add: hastyenv_def, blast+)
done

lemma consistency [rule_format]:
   "<ve,e,v> ∈ EvalRel 
    ⟹ (∀t te. hastyenv(ve,te) ⟶ <te,e,t> ∈ ElabRel ⟶ ⟨v,t⟩ ∈ HasTyRel)"
apply (erule EvalRel.induct)
apply (simp_all add: consistency_const consistency_var consistency_fn 
                     consistency_fix consistency_app1)
apply (blast intro: consistency_app2)
done

lemma basic_consistency:
     "⟦ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve,te);                    
         <ve,e,v_const(c)> ∈ EvalRel; <te,e,t> ∈ ElabRel⟧ 
      ⟹ isof(c,t)"
by (blast dest: consistency intro!: basic_consistency_lem)

end