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