# Theory Dynamic

Up to index of Isabelle/ZF/Coind

theory Dynamic
imports Values
begin

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

    theory Dynamic imports Values begin

    consts
      EvalRel :: i
    inductive
      domains "EvalRel" <= "ValEnv * Exp * Val"
      intros
        eval_constI:
          " [| ve ∈ ValEnv; c ∈ Const |] ==>
           <ve,e_const(c),v_const(c)>:EvalRel"
        eval_varI:
          " [| ve ∈ ValEnv; x ∈ ExVar; x ∈ ve_dom(ve) |] ==>
           <ve,e_var(x),ve_app(ve,x)>:EvalRel"
        eval_fnI:
          " [| ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp |] ==>
           <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
        eval_fixI:
          " [| ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; f ∈ ExVar; cl ∈ Val;
              v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>
           <ve,e_fix(f,x,e),cl>:EvalRel "
        eval_appI1:
          " [| ve ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; c1 ∈ Const; c2 ∈ Const;
              <ve,e1,v_const(c1)>:EvalRel;
              <ve,e2,v_const(c2)>:EvalRel |] ==>
           <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
        eval_appI2:
          " [| ve ∈ ValEnv; vem ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; em ∈ Exp; xm ∈ ExVar; v ∈ Val;
              <ve,e1,v_clos(xm,em,vem)>:EvalRel;
              <ve,e2,v2>:EvalRel;
              <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>
           <ve,e_app(e1,e2),v>:EvalRel "
      type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros

    end