src/HOL/IMP/Com.thy
author wenzelm
Wed Mar 30 23:26:40 2011 +0200 (2011-03-30)
changeset 42174 d0be2722ce9f
parent 41589 bbd861837ebc
child 43141 11fce8564415
permissions -rw-r--r--
modernized specifications;
     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 type_synonym val = nat -- "or anything else, @{text nat} used in examples"
    15 type_synonym state = "loc \<Rightarrow> val"
    16 type_synonym aexp = "state \<Rightarrow> val"
    17 type_synonym bexp = "state \<Rightarrow> bool"
    18   -- "arithmetic and boolean expressions are not modelled explicitly here,"
    19   -- "they are just functions on states"
    20 
    21 datatype
    22   com = SKIP                    
    23       | Assign loc aexp         ("_ :== _ " 60)
    24       | Semi   com com          ("_; _"  [60, 60] 10)
    25       | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
    26       | While  bexp com         ("WHILE _ DO _"  60)
    27 
    28 notation (latex)
    29   SKIP  ("\<SKIP>") and
    30   Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
    31   While  ("\<WHILE> _ \<DO> _"  60)
    32 
    33 end