src/HOL/IMP/Com.thy
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 12338 de0f4a63baa5
equal deleted inserted replaced
9240:f4d76cb26433 9241:f961c1fdff50
     7 Syntax of commands
     7 Syntax of commands
     8 *)
     8 *)
     9 
     9 
    10 Com = Main +
    10 Com = Main +
    11 
    11 
    12 types 
    12 types
    13       val
       
    14       loc
    13       loc
    15       state = "loc => val"
    14       val   = nat (* or anything else, nat used in examples *)
    16       aexp  = "state => val"
    15       state = loc => val
       
    16       aexp  = state => val
    17       bexp  = state => bool
    17       bexp  = state => bool
    18 
    18 
    19 arities loc,val :: term
    19 arities loc :: term
    20 
    20 
    21 datatype
    21 datatype
    22   com = SKIP
    22   com = SKIP
    23       | ":="  loc aexp         (infixl  60)
    23       | ":=="  loc aexp         (infixl  60)
    24       | Semi  com com          ("_; _"  [60, 60] 10)
    24       | Semi  com com          ("_; _"  [60, 60] 10)
    25       | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    25       | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    26       | While bexp com         ("WHILE _ DO _"  60)
    26       | While bexp com         ("WHILE _ DO _"  60)
    27 
    27 
    28 end
    28 end