src/HOL/IMP/Com.thy
author wenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589 bbd861837ebc
parent 27362 a6dc1769fdda
child 42174 d0be2722ce9f
permissions -rw-r--r--
tuned headers;
     1 (*  Title:        HOL/IMP/Com.thy
     2     Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     3     Author:       Gerwin Klein
     4 *)
     5 
     6 header "Syntax of Commands"
     7 
     8 theory Com imports Main begin
     9 
    10 typedecl loc 
    11   -- "an unspecified (arbitrary) type of locations 
    12       (adresses/names) for variables"
    13       
    14 types 
    15   val   = nat -- "or anything else, @{text nat} used in examples"
    16   state = "loc \<Rightarrow> val"
    17   aexp  = "state \<Rightarrow> val"  
    18   bexp  = "state \<Rightarrow> bool"
    19   -- "arithmetic and boolean expressions are not modelled explicitly here,"
    20   -- "they are just functions on states"
    21 
    22 datatype
    23   com = SKIP                    
    24       | Assign loc aexp         ("_ :== _ " 60)
    25       | Semi   com com          ("_; _"  [60, 60] 10)
    26       | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
    27       | While  bexp com         ("WHILE _ DO _"  60)
    28 
    29 notation (latex)
    30   SKIP  ("\<SKIP>") and
    31   Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
    32   While  ("\<WHILE> _ \<DO> _"  60)
    33 
    34 end