src/HOL/IMP/Com.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 16417 9bc16273c2d4
child 27362 a6dc1769fdda
permissions -rw-r--r--
avoid rebinding of existing facts;
kleing@12431
     1
(*  Title:        HOL/IMP/Com.thy
kleing@12431
     2
    ID:           $Id$
kleing@12431
     3
    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
kleing@12431
     4
    Isar Version: Gerwin Klein, 2001
kleing@12431
     5
    Copyright     1994 TUM
clasohm@924
     6
*)
clasohm@924
     7
kleing@12431
     8
header "Syntax of Commands"
kleing@12431
     9
haftmann@16417
    10
theory Com imports Main begin
clasohm@924
    11
kleing@12431
    12
typedecl loc 
kleing@12431
    13
  -- "an unspecified (arbitrary) type of locations 
kleing@12431
    14
      (adresses/names) for variables"
kleing@12431
    15
      
kleing@12431
    16
types 
kleing@12431
    17
  val   = nat -- "or anything else, @{text nat} used in examples"
kleing@12431
    18
  state = "loc \<Rightarrow> val"
kleing@12431
    19
  aexp  = "state \<Rightarrow> val"  
kleing@12431
    20
  bexp  = "state \<Rightarrow> bool"
kleing@12431
    21
  -- "arithmetic and boolean expressions are not modelled explicitly here,"
kleing@12431
    22
  -- "they are just functions on states"
clasohm@924
    23
clasohm@924
    24
datatype
kleing@12431
    25
  com = SKIP                    
kleing@12431
    26
      | Assign loc aexp         ("_ :== _ " 60)
kleing@12431
    27
      | Semi   com com          ("_; _"  [60, 60] 10)
kleing@12431
    28
      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
kleing@12431
    29
      | While  bexp com         ("WHILE _ DO _"  60)
kleing@12431
    30
kleing@12431
    31
syntax (latex)
kleing@12431
    32
  SKIP :: com   ("\<SKIP>")
kleing@12431
    33
  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
kleing@12431
    34
  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
clasohm@924
    35
clasohm@924
    36
end