Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Coind/Dynamic.thy
author wenzelm
Thu, 14 Oct 1999 15:04:36 +0200
changeset 7866 3ccaa11b6df9
parent 1478 2b8c2a7547ab
child 11318 6536fb8c9fc6
permissions -rw-r--r--
pdf: generate thumbnails if ISABELLE_THUMBPDF set;

(*  Title:      ZF/Coind/Dynamic.thy
    ID:         $Id$
    Author:     Jacob Frost, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge
*)

Dynamic = Values +

consts
  EvalRel :: i
inductive
  domains "EvalRel" <= "ValEnv * Exp * Val"
  intrs
    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_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"

  
end
isabelle