src/HOL/IMP/Com.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 12431 07ec657249e5
child 27362 a6dc1769fdda
permissions -rw-r--r--
migrated theory headers to new format
     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 syntax (latex)
    32   SKIP :: com   ("\<SKIP>")
    33   Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
    34   While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
    35 
    36 end