src/HOL/IMP/Com.thy
author kleing
Sun Dec 09 14:35:36 2001 +0100 (2001-12-09)
changeset 12431 07ec657249e5
parent 12338 de0f4a63baa5
child 16417 9bc16273c2d4
permissions -rw-r--r--
converted to Isar
     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 = Main:
    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