accidentally deleted these files from the repository; now adding them and
"cvs rm"ing them again

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Com.ML	Fri Jan 19 12:49:36 1996 +0100
@@ -0,0 +1,30 @@
+(*  Title: 	HOL/IMP/Com.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Com;
+
+val evala_elim_cases = map (evala.mk_cases aexp.simps)
+   ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i",
+    "<Op1(f,e),sigma> -a-> i", "<Op2(f,a1,a2),sigma>  -a-> i"
+   ];
+
+val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
+   ["<true,sigma> -b-> x", "<false,sigma> -b-> x",
+    "<ROp(f,a0,a1),sigma> -b-> x", "<noti(b),sigma> -b-> x",
+    "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x"
+   ];
+
+val evalb_simps = map (fn s => prove_goal Com.thy s
+    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
+  ["(<true,sigma> -b-> w) = (w=True)",
+   "(<false,sigma> -b-> w) = (w=False)",
+   "(<ROp(f,a0,a1),sigma> -b-> w) = \
+\   (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f(m,n)))",
+   "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))",
+   "(<b0 andi b1,sigma> -b-> w) = \
+\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))",
+   "(<b0 ori b1,sigma> -b-> w) = \
+\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Com.thy	Fri Jan 19 12:49:36 1996 +0100
@@ -0,0 +1,112 @@
+(*  Title: 	HOL/IMP/Com.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+Arithmetic expressions, Boolean expressions, Commands
+
+And their Operational semantics
+*)
+
+Com = Arith +
+
+(** Arithmetic expressions **)
+types loc
+      state = "loc => nat"
+      n2n = "nat => nat"
+      n2n2n = "nat => nat => nat"
+
+arities loc :: 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
+      | ":="   (loc,aexp)	 (infixl  60)
+      | semic  (com,com)	 ("_; _"  [60, 60] 10)
+      | whileC (bexp,com)	 ("while _ do _"  60)
+      | ifC    (bexp, com, com)	 ("ifc _ then _ else _"  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"
+
+rules 
+	assign_def	"s[m/x] == (%y. if(y=x,m,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"
+
+    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
+            ==> <ifc b then c0 else c1, s> -c-> s1"
+
+    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
+             ==> <ifc 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IMP/Denotation.ML	Fri Jan 19 12:49:36 1996 +0100
@@ -0,0 +1,24 @@
+(*  Title: 	HOL/IMP/Denotation.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Denotation;
+
+(**** Rewrite Rules for A,B,C ****)
+
+val A_simps =
+     [A_nat,A_loc,A_op1,A_op2];
+
+val B_simps = map (fn t => t RS eq_reflection)
+     [B_true,B_false,B_op,B_not,B_and,B_or]
+
+val C_simps = map (fn t => t RS eq_reflection)
+  [C_skip,C_assign,C_comp,C_if,C_while]; 
+
+(**** mono (Gamma(b,c)) ****)
+
+qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
+	"mono(Gamma(b,c))"
+     (fn _ => [(best_tac comp_cs 1)]);