src/HOL/IMP/Com.thy
changeset 1696 e84bff5c519b
parent 1481 03f096efa26d
child 5183 89f162de39cf
--- a/src/HOL/IMP/Com.thy	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Com.thy	Sat Apr 27 18:47:31 1996 +0200
@@ -1,112 +1,28 @@
 (*  Title:      HOL/IMP/Com.thy
     ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     Copyright   1994 TUM
 
-Arithmetic expressions, Boolean expressions, Commands
-
-And their Operational semantics
+Semantics of arithmetic and boolean expressions
+Syntax of commands
 *)
 
 Com = Arith +
 
-(** Arithmetic expressions **)
-types loc
-      state = "loc => nat"
-      n2n = "nat => nat"
-      n2n2n = "nat => nat => nat"
+types 
+      val
+      loc
+      state = "loc => val"
+      aexp  = "state => val"
+      bexp  = state => bool
 
-arities loc :: term
+arities loc,val :: term
 
 datatype
-  aexp = N nat
-       | X loc
-       | Op1 n2n aexp
-       | Op2 n2n2n aexp aexp
-
-(** Evaluation of arithmetic expressions **)
-consts  evala    :: "(aexp*state*nat)set"
-       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
-translations
-    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
-inductive "evala"
-  intrs 
-    N   "<N(n),s> -a-> n"
-    X   "<X(x),s> -a-> s(x)"
-    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
-    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
-           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
-
-types n2n2b = "[nat,nat] => bool"
-
-(** Boolean expressions **)
-
-datatype
-  bexp = true
-       | false
-       | ROp  n2n2b aexp aexp
-       | noti bexp
-       | andi bexp bexp         (infixl 60)
-       | ori  bexp bexp         (infixl 60)
-
-(** Evaluation of boolean expressions **)
-consts evalb    :: "(bexp*state*bool)set"       
-       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
-
-translations
-    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
-
-inductive "evalb"
- intrs (*avoid clash with ML constructors true, false*)
-    tru   "<true,s> -b-> True"
-    fls   "<false,s> -b-> False"
-    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
-           ==> <ROp f a0 a1,s> -b-> f n0 n1"
-    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
-    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-          ==> <b0 andi b1,s> -b-> (w0 & w1)"
-    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-            ==> <b0 ori b1,s> -b-> (w0 | w1)"
-
-(** Commands **)
-
-datatype
-  com = Skip
+  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)
 
-(** Execution of commands **)
-consts  evalc    :: "(com*state*state)set"
-        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
-        "assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
-
-translations
-       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
-
-defs 
-  assign_def   "s[m/x] == (%y. if y=x then m else s y)"
-
-inductive "evalc"
-  intrs
-    skip    "<Skip,s> -c-> s"
-
-    assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
-
-    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
-            ==> <c0 ; c1, s> -c-> s1"
-
-    IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
-            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
-
-    IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
-             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
-
-    WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s"
-
-    WhileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
-                  <WHILE b DO c, s2> -c-> s1 |] 
-               ==> <WHILE b DO c, s> -c-> s1"
- 
 end