Theory Com

Up to index of Isabelle/HOL/IMPP

(*  Title:    HOL/IMPP/Com.thy
    ID:       $Id: Com.thy,v 1.16 1999/11/24 13:48:18 oheimb Exp $
    Author:   Heiko Loetzbeyer&Robert Sandner&Tobias Nipkow&David von Oheimb,TUM
    Copyright 1994, 1999 TUM

Semantics of arithmetic and boolean expressions
Syntax of commands
*)

Com = Main +

types    val = nat (* for the meta theory, this may be anything *)
types    glb
         loc
arities  (*val,*)glb,loc :: term
datatype vname = Glb glb | Loc loc
types    globs = glb => val
         locals= loc => val
datatype state = st globs locals
types    aexp  = state => val
         bexp  = state => bool

rules   single_stateE "!s::state. s = t ==> False" (* at least two elements *)

axclass finite<term
  finite "finite UNIV"

types   pname
arities pname :: finite (* assert pname to be finite *)

datatype com
      = SKIP
      | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
      | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
      | Semi  com  com          ("_;; _"                [59, 60    ] 59)
      | Cond  bexp com com      ("IF _ THEN _ ELSE _"   [65, 60, 61] 60)
      | While bexp com          ("WHILE _ DO _"         [65,     61] 60)
      | BODY  pname
      | Call  vname pname aexp  ("_:=CALL _'(_')"       [65, 65,  0] 60)

consts  body     :: "pname => com"
        Arg, Res :: loc

rules 
  Arg_neq_Res "Arg ~= Res"

end