src/HOL/IMP/Com.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 27362 a6dc1769fdda
child 41589 bbd861837ebc
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     1 (*  Title:        HOL/IMP/Com.thy
     2     ID:           $Id$
     3     Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     4     Isar Version: Gerwin Klein, 2001
     5     Copyright     1994 TUM
     6 *)
     7 
     8 header "Syntax of Commands"
     9 
    10 theory Com imports Main begin
    11 
    12 typedecl loc 
    13   -- "an unspecified (arbitrary) type of locations 
    14       (adresses/names) for variables"
    15       
    16 types 
    17   val   = nat -- "or anything else, @{text nat} used in examples"
    18   state = "loc \<Rightarrow> val"
    19   aexp  = "state \<Rightarrow> val"  
    20   bexp  = "state \<Rightarrow> bool"
    21   -- "arithmetic and boolean expressions are not modelled explicitly here,"
    22   -- "they are just functions on states"
    23 
    24 datatype
    25   com = SKIP                    
    26       | Assign loc aexp         ("_ :== _ " 60)
    27       | Semi   com com          ("_; _"  [60, 60] 10)
    28       | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
    29       | While  bexp com         ("WHILE _ DO _"  60)
    30 
    31 notation (latex)
    32   SKIP  ("\<SKIP>") and
    33   Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
    34   While  ("\<WHILE> _ \<DO> _"  60)
    35 
    36 end