src/HOL/IMP/Com.thy

integrated with LOrder.thy

(*  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)

syntax (latex)
  SKIP :: com   ("\<SKIP>")
  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)

end