(*  Title:        HOL/IMP/Com.thy

    ID:           $Id$

    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM

    Isar Version: Gerwin Klein, 2001

    Copyright     1994 TUM

*)

header "Syntax of Commands"

theory Com imports Main begin

typedecl loc 

  -- "an unspecified (arbitrary) type of locations 

      (adresses/names) for variables"

types 

  val   = nat -- "or anything else, @{text nat} used in examples"

  state = "loc \<Rightarrow> val"

  aexp  = "state \<Rightarrow> val"  

  bexp  = "state \<Rightarrow> bool"

  -- "arithmetic and boolean expressions are not modelled explicitly here,"

  -- "they are just functions on states"

datatype

  com = SKIP                    

      | Assign loc aexp         ("_ :== _ " 60)

      | Semi   com com          ("_; _"  [60, 60] 10)

      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)

      | While  bexp com         ("WHILE _ DO _"  60)

notation (latex)

  SKIP  ("\<SKIP>") and

  Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and

  While  ("\<WHILE> _ \<DO> _"  60)

end