src/HOL/IMP/Com.thy
author wenzelm
Wed Mar 30 23:26:40 2011 +0200 (2011-03-30)
changeset 42174 d0be2722ce9f
parent 41589 bbd861837ebc
child 43141 11fce8564415
permissions -rw-r--r--
modernized specifications;
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
      
wenzelm@42174
    14
type_synonym val = nat -- "or anything else, @{text nat} used in examples"
wenzelm@42174
    15
type_synonym state = "loc \<Rightarrow> val"
wenzelm@42174
    16
type_synonym aexp = "state \<Rightarrow> val"
wenzelm@42174
    17
type_synonym bexp = "state \<Rightarrow> bool"
kleing@12431
    18
  -- "arithmetic and boolean expressions are not modelled explicitly here,"
kleing@12431
    19
  -- "they are just functions on states"
clasohm@924
    20
clasohm@924
    21
datatype
kleing@12431
    22
  com = SKIP                    
kleing@12431
    23
      | Assign loc aexp         ("_ :== _ " 60)
kleing@12431
    24
      | Semi   com com          ("_; _"  [60, 60] 10)
kleing@12431
    25
      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
kleing@12431
    26
      | While  bexp com         ("WHILE _ DO _"  60)
kleing@12431
    27
wenzelm@27362
    28
notation (latex)
wenzelm@27362
    29
  SKIP  ("\<SKIP>") and
wenzelm@27362
    30
  Cond  ("\<IF> _ \<THEN> _ \<ELSE> _"  60) and
wenzelm@27362
    31
  While  ("\<WHILE> _ \<DO> _"  60)
clasohm@924
    32
clasohm@924
    33
end