src/HOL/IMP/Com.thy
changeset 12431 07ec657249e5
parent 12338 de0f4a63baa5
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:11 2001 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:36 2001 +0100
     1.3 @@ -1,28 +1,36 @@
     1.4 -(*  Title:      HOL/IMP/Com.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     1.7 -    Copyright   1994 TUM
     1.8 -
     1.9 -Semantics of arithmetic and boolean expressions
    1.10 -Syntax of commands
    1.11 +(*  Title:        HOL/IMP/Com.thy
    1.12 +    ID:           $Id$
    1.13 +    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
    1.14 +    Isar Version: Gerwin Klein, 2001
    1.15 +    Copyright     1994 TUM
    1.16  *)
    1.17  
    1.18 -Com = Main +
    1.19 +header "Syntax of Commands"
    1.20 +
    1.21 +theory Com = Main:
    1.22  
    1.23 -types
    1.24 -      loc
    1.25 -      val   = nat (* or anything else, nat used in examples *)
    1.26 -      state = loc => val
    1.27 -      aexp  = state => val
    1.28 -      bexp  = state => bool
    1.29 -
    1.30 -arities loc :: type
    1.31 +typedecl loc 
    1.32 +  -- "an unspecified (arbitrary) type of locations 
    1.33 +      (adresses/names) for variables"
    1.34 +      
    1.35 +types 
    1.36 +  val   = nat -- "or anything else, @{text nat} used in examples"
    1.37 +  state = "loc \<Rightarrow> val"
    1.38 +  aexp  = "state \<Rightarrow> val"  
    1.39 +  bexp  = "state \<Rightarrow> bool"
    1.40 +  -- "arithmetic and boolean expressions are not modelled explicitly here,"
    1.41 +  -- "they are just functions on states"
    1.42  
    1.43  datatype
    1.44 -  com = SKIP
    1.45 -      | ":=="  loc aexp         (infixl  60)
    1.46 -      | Semi  com com          ("_; _"  [60, 60] 10)
    1.47 -      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.48 -      | While bexp com         ("WHILE _ DO _"  60)
    1.49 +  com = SKIP                    
    1.50 +      | Assign loc aexp         ("_ :== _ " 60)
    1.51 +      | Semi   com com          ("_; _"  [60, 60] 10)
    1.52 +      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.53 +      | While  bexp com         ("WHILE _ DO _"  60)
    1.54 +
    1.55 +syntax (latex)
    1.56 +  SKIP :: com   ("\<SKIP>")
    1.57 +  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
    1.58 +  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
    1.59  
    1.60  end