Quelle  Dynamic.thy

(*  Title:      ZF/Coind/Dynamic.thy
  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] ==>
       :EvalRel"
    eval_varI:
      " [ve ∈ ValEnv; x ∈ ExVar; x ∈ ve_dom(ve)] ==>
       :EvalRel" 
    eval_fnI:
      " [ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp] ==>
       :EvalRel "  
    eval_fixI:
      " [ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; f ∈ ExVar; cl ∈ Val;
          v_clos(x,e,ve_owr(ve,f,cl))=cl] ==>
       :EvalRel " 
    eval_appI1:
      " [ve ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; c1 ∈ Const; c2 ∈ Const;
          :EvalRel;
          :EvalRel] ==>
       :EvalRel "
    eval_appI2:
      " [ve ∈ ValEnv; vem ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; em ∈ Exp; xm ∈ ExVar; v ∈ Val;
          :EvalRel;
          :EvalRel;
          :EvalRel] ==>
       :EvalRel "
  type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros

end