# Theory ECR

Up to index of Isabelle/ZF/Coind

theory ECR
imports Static Dynamic
begin

    (*  Title:      ZF/Coind/ECR.thy
        ID:         $Id: ECR.thy,v 1.11 2005/06/17 14:15:10 haftmann Exp $
        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 *)

    constdefs
      hastyenv :: "[i,i] => o"
        "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>} Un 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, standard]

    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)"
    apply (unfold 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"
    apply (unfold hastyenv_def)
    apply (erule elab_fixE, safe)
    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

lemma htr_closCI:

      [| 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

lemmas htr_constE:

      [| ⟨v_const(c), t⟩ ∈ HasTyRel; [| c ∈ Const; t ∈ Ty; isof(c, t) |] ==> Q |]
      ==> Q

and htr_closE:

      [| ⟨v_clos(x, e, ve), t⟩ ∈ HasTyRel;
         !!te. [| 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, x), te_app(te, x)⟩ . x ∈ te_dom(te)} ⊆ HasTyRel |]
               ==> Q |]
      ==> Q

lemmas HasTyRel_non_zero:

      ⟨v, b⟩ ∈ HasTyRel ==> v ≠ 0

lemmas HasTyRel_non_zero:

      ⟨v, b⟩ ∈ HasTyRel ==> v ≠ 0

lemma hastyenv_owr:

      [| ve ∈ ValEnv; te ∈ TyEnv; hastyenv(ve, te); ⟨v, t⟩ ∈ HasTyRel |]
      ==> hastyenv(ve_owr(ve, x, v), te_owr(te, x, t))

lemma basic_consistency_lem:

      [| ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve, te) |] ==> hastyenv(ve, te)

lemma consistency_const:

      [| c ∈ Const; hastyenv(ve, te); ⟨te, e_const(c), t⟩ ∈ ElabRel |]
      ==> ⟨v_const(c), t⟩ ∈ HasTyRel

lemma consistency_var:

      [| x ∈ ve_dom(ve); hastyenv(ve, te); ⟨te, e_var(x), t⟩ ∈ ElabRel |]
      ==> ⟨ve_app(ve, x), t⟩ ∈ HasTyRel

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

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

lemma consistency_app1:

      [| ve ∈ ValEnv; e1.0 ∈ Exp; e2.0 ∈ Exp; c1.0 ∈ Const; c2.0 ∈ Const;
         ⟨ve, e1.0, v_const(c1.0)⟩ ∈ EvalRel;
         ∀t te. hastyenv(ve, te) -->
                ⟨te, e1.0, t⟩ ∈ ElabRel --> ⟨v_const(c1.0), t⟩ ∈ HasTyRel;
         ⟨ve, e2.0, v_const(c2.0)⟩ ∈ EvalRel;
         ∀t te. hastyenv(ve, te) -->
                ⟨te, e2.0, t⟩ ∈ ElabRel --> ⟨v_const(c2.0), t⟩ ∈ HasTyRel;
         hastyenv(ve, te); ⟨te, e_app(e1.0, e2.0), t⟩ ∈ ElabRel |]
      ==> ⟨v_const(c_app(c1.0, c2.0)), t⟩ ∈ HasTyRel

lemma consistency_app2:

      [| ve ∈ ValEnv; vem ∈ ValEnv; e1.0 ∈ Exp; e2.0 ∈ Exp; em ∈ Exp; xm ∈ ExVar;
         v ∈ Val; ⟨ve, e1.0, v_clos(xm, em, vem)⟩ ∈ EvalRel;
         ∀t te. hastyenv(ve, te) -->
                ⟨te, e1.0, t⟩ ∈ ElabRel --> ⟨v_clos(xm, em, vem), t⟩ ∈ HasTyRel;
         ⟨ve, e2.0, v2.0⟩ ∈ EvalRel;
         ∀t te. hastyenv(ve, te) --> ⟨te, e2.0, t⟩ ∈ ElabRel --> ⟨v2.0, t⟩ ∈ HasTyRel;
         ⟨ve_owr(vem, xm, v2.0), em, v⟩ ∈ EvalRel;
         ∀t te. hastyenv(ve_owr(vem, xm, v2.0), te) -->
                ⟨te, em, t⟩ ∈ ElabRel --> ⟨v, t⟩ ∈ HasTyRel;
         hastyenv(ve, te); ⟨te, e_app(e1.0, e2.0), t⟩ ∈ ElabRel |]
      ==> ⟨v, t⟩ ∈ HasTyRel

lemma consistency:

      [| ⟨ve, e, v⟩ ∈ EvalRel; hastyenv(ve, te); ⟨te, e, t⟩ ∈ ElabRel |]
      ==> ⟨v, t⟩ ∈ HasTyRel

lemma basic_consistency:

      [| ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve, te); ⟨ve, e, v_const(c)⟩ ∈ EvalRel;
         ⟨te, e, t⟩ ∈ ElabRel |]
      ==> isof(c, t)