src/HOL/IMP/Com.thy
changeset 12431 07ec657249e5
parent 12338 de0f4a63baa5
child 16417 9bc16273c2d4
--- a/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:36 2001 +0100
@@ -1,28 +1,36 @@
-(*  Title:      HOL/IMP/Com.thy
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-    Copyright   1994 TUM
-
-Semantics of arithmetic and boolean expressions
-Syntax of commands
+(*  Title:        HOL/IMP/Com.thy
+    ID:           $Id$
+    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
+    Isar Version: Gerwin Klein, 2001
+    Copyright     1994 TUM
 *)
 
-Com = Main +
+header "Syntax of Commands"
+
+theory Com = Main:
 
-types
-      loc
-      val   = nat (* or anything else, nat used in examples *)
-      state = loc => val
-      aexp  = state => val
-      bexp  = state => bool
-
-arities loc :: type
+typedecl loc 
+  -- "an unspecified (arbitrary) type of locations 
+      (adresses/names) for variables"
+      
+types 
+  val   = nat -- "or anything else, @{text nat} used in examples"
+  state = "loc \<Rightarrow> val"
+  aexp  = "state \<Rightarrow> val"  
+  bexp  = "state \<Rightarrow> bool"
+  -- "arithmetic and boolean expressions are not modelled explicitly here,"
+  -- "they are just functions on states"
 
 datatype
-  com = SKIP
-      | ":=="  loc aexp         (infixl  60)
-      | Semi  com com          ("_; _"  [60, 60] 10)
-      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
-      | While bexp com         ("WHILE _ DO _"  60)
+  com = SKIP                    
+      | Assign loc aexp         ("_ :== _ " 60)
+      | Semi   com com          ("_; _"  [60, 60] 10)
+      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
+      | While  bexp com         ("WHILE _ DO _"  60)
+
+syntax (latex)
+  SKIP :: com   ("\<SKIP>")
+  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
+  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
 
 end