Quelle  ECR.thy

(*  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)] ==> ∈ HasTyRel"
    htr_closI [intro]:
      "[x ∈ ExVar; e ∈ Exp; t ∈ Ty; ve ∈ ValEnv; te ∈ TyEnv;
           ∈ ElabRel;
          ve_dom(ve) = te_dom(te);
          {.y ∈ ve_dom(ve)} ∈ Pow(HasTyRel)]
       ==> ∈ 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). ∈ HasTyRel)"

(* Specialised co-induction rule *)

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

(* Specialised elimination rules *)

inductive_cases
    htr_constE [elim!]: " ∈ HasTyRel"
  and htr_closE [elim]: " ∈ 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); ∈ ElabRel]
      ==> ∈ HasTyRel"
by blast


lemma consistency_var: 
  "[x ∈ ve_dom(ve); hastyenv(ve,te); ∈ ElabRel] ==>
    ∈ HasTyRel"
by (unfold hastyenv_def, blast)

lemma consistency_fn: 
  "[ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; hastyenv(ve,te);
            ∈ ElabRel
\ ==> ∈ 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); ∈ 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;
      ∈ EvalRel;
     ∀t te.
       hastyenv(ve,te) ⟶ ∈ ElabRel ⟶ ∈ HasTyRel;
      ∈ EvalRel;
     ∀t te.
       hastyenv(ve,te) ⟶ ∈ ElabRel ⟶ ∈ HasTyRel;
     hastyenv(ve, te);
      ∈ ElabRel]
  ==> ∈ 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;
      ∈ EvalRel;
     ∀t te. hastyenv(ve,te) ⟶
             ∈ ElabRel ⟶ ∈ HasTyRel;
      ∈ EvalRel;
     ∀t te. hastyenv(ve,te) ⟶ ∈ ElabRel ⟶ ⟨v2,t⟩ ∈ HasTyRel;
      ∈ EvalRel;
     ∀t te. hastyenv(ve_owr(vem,xm,v2),te) ⟶
             ∈ ElabRel ⟶ ⟨v,t⟩ ∈ HasTyRel;
     hastyenv(ve,te); ∈ 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]:
   " ∈ EvalRel
    ==> (∀t te. hastyenv(ve,te) ⟶ ∈ 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);
          ∈ EvalRel; ∈ ElabRel]
      ==> isof(c,t)"
by (blast dest: consistency intro!: basic_consistency_lem)

end