# Theory Static

Up to index of Isabelle/ZF/Coind

theory Static
imports Values Types
begin

    (*  Title:      ZF/Coind/Static.thy
        ID:         $Id: Static.thy,v 1.9 2005/06/17 14:15:10 haftmann Exp $
        Author:     Jacob Frost, Cambridge University Computer Laboratory
        Copyright   1995  University of Cambridge
    *)

    theory Static imports Values Types begin

    (*** Basic correspondence relation -- not completely specified, as it is a
         parameter of the proof.  A concrete version could be defined inductively.
    ***)

    consts
      isof :: "[i,i] => o"

    axioms
      isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"

    (*Its extension to environments*)

    constdefs
      isofenv :: "[i,i] => o"
       "isofenv(ve,te) ==
          ve_dom(ve) = te_dom(te) &
          (∀x ∈ ve_dom(ve).
            ∃c ∈ Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"

    (*** Elaboration ***)

    consts  ElabRel :: i

    inductive
      domains "ElabRel" <= "TyEnv * Exp * Ty"
      intros
        constI [intro!]:
          "[| te ∈ TyEnv; c ∈ Const; t ∈ Ty; isof(c,t) |] ==>
           <te,e_const(c),t> ∈ ElabRel"
        varI [intro!]:
          "[| te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te) |] ==>
           <te,e_var(x),te_app(te,x)> ∈ ElabRel"
        fnI [intro!]:
          "[| te ∈ TyEnv; x ∈ ExVar; e ∈ Exp; t1 ∈ Ty; t2 ∈ Ty;
              <te_owr(te,x,t1),e,t2> ∈ ElabRel |] ==>
           <te,e_fn(x,e),t_fun(t1,t2)> ∈ ElabRel"
        fixI [intro!]:
          "[| te ∈ TyEnv; f ∈ ExVar; x ∈ ExVar; t1 ∈ Ty; t2 ∈ Ty;
              <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> ∈ ElabRel |] ==>
           <te,e_fix(f,x,e),t_fun(t1,t2)> ∈ ElabRel"
        appI [intro]:
          "[| te ∈ TyEnv; e1 ∈ Exp; e2 ∈ Exp; t1 ∈ Ty; t2 ∈ Ty;
              <te,e1,t_fun(t1,t2)> ∈ ElabRel;
              <te,e2,t1> ∈ ElabRel |] ==> <te,e_app(e1,e2),t2> ∈ ElabRel"
      type_intros te_appI Exp.intros Ty.intros

    inductive_cases
        elab_constE [elim!]: "<te,e_const(c),t> ∈ ElabRel"
      and elab_varE [elim!]: "<te,e_var(x),t> ∈ ElabRel"
      and elab_fnE [elim]:   "<te,e_fn(x,e),t> ∈ ElabRel"
      and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> ∈ ElabRel"
      and elab_appE [elim]:  "<te,e_app(e1,e2),t> ∈ ElabRel"

    declare ElabRel.dom_subset [THEN subsetD, dest]

    end

lemmas elab_constE:

      [| ⟨te, e_const(c), t⟩ ∈ ElabRel;
         [| te ∈ TyEnv; c ∈ Const; t ∈ Ty; isof(c, t) |] ==> Q |]
      ==> Q

and elab_varE:

      [| ⟨te, e_var(x), t⟩ ∈ ElabRel;
         [| te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te); t = te_app(te, x) |] ==> Q |]
      ==> Q

and elab_fnE:

      [| ⟨te, e_fn(x, e), t⟩ ∈ ElabRel;
         !!t1 t2.
            [| te ∈ TyEnv; x ∈ ExVar; e ∈ Exp; t1 ∈ Ty; t2 ∈ Ty;
               ⟨te_owr(te, x, t1), e, t2⟩ ∈ ElabRel; t = t_fun(t1, t2) |]
            ==> Q |]
      ==> Q

and elab_fixE:

      [| ⟨te, e_fix(f, x, e), t⟩ ∈ ElabRel;
         !!t1 t2.
            [| te ∈ TyEnv; f ∈ ExVar; x ∈ ExVar; t1 ∈ Ty; t2 ∈ Ty;
               ⟨te_owr(te_owr(te, f, t_fun(t1, t2)), x, t1), e, t2⟩ ∈ ElabRel;
               t = t_fun(t1, t2) |]
            ==> Q |]
      ==> Q

and elab_appE:

      [| ⟨te, e_app(e1.0, e2.0), t⟩ ∈ ElabRel;
         !!t1. [| te ∈ TyEnv; e1.0 ∈ Exp; e2.0 ∈ Exp; t1 ∈ Ty; t ∈ Ty;
                  ⟨te, e1.0, t_fun(t1, t)⟩ ∈ ElabRel; ⟨te, e2.0, t1⟩ ∈ ElabRel |]
               ==> Q |]
      ==> Q