# HG changeset patch
# User nipkow
# Date 830623761 -7200
# Node ID 687f0710c22df5afc00bef65e2969781b5e15aa0
# Parent  e84bff5c519b348887c6b2db05aa8f8999122622
Arithemtic and boolean expressions are now in a separate theory.
The commands don not use them directly. Instead they are based on
the semantics (rather than the syntax) of expressions.

diff -r e84bff5c519b -r 687f0710c22d src/HOL/IMP/Expr.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Expr.ML	Sat Apr 27 18:49:21 1996 +0200
@@ -0,0 +1,46 @@
+(*  Title:      HOL/IMP/Expr.ML
+    ID:         $Id$
+    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
+    Copyright   1994 TUM
+
+Arithmetic expressions and Boolean expressions.
+Not used in the rest of the language, but included for completeness.
+*)
+
+open Expr;
+
+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 Expr.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)))"];
+
+goal Expr.thy "!n. (<a,s> -a-> n) = (n = A a s)";
+by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
+by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
+by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
+                             addSEs evala_elim_cases)));
+qed_spec_mp "aexp_iff";
+
+goal Expr.thy "!w. (<b,s> -b-> w) = (w = B b s)";
+by (bexp.induct_tac "b" 1);
+by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
+                                    addsimps (aexp_iff::evalb_simps))));
+qed_spec_mp "bexp_iff";
diff -r e84bff5c519b -r 687f0710c22d src/HOL/IMP/Expr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Expr.thy	Sat Apr 27 18:49:21 1996 +0200
@@ -0,0 +1,89 @@
+(*  Title:      HOL/IMP/Expr.thy
+    ID:         $Id$
+    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
+    Copyright   1994 TUM
+
+Arithmetic expressions and Boolean expressions.
+Not used in the rest of the language, but included for completeness.
+*)
+
+Expr = 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)"
+
+(** Denotational semantics of arithemtic and boolean expressions **)
+consts
+  A     :: aexp => state => nat
+  B     :: bexp => state => bool
+
+primrec A aexp
+  A_nat "A(N(n)) = (%s. n)"
+  A_loc "A(X(x)) = (%s. s(x))" 
+  A_op1 "A(Op1 f a) = (%s. f(A a s))"
+  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+
+primrec B bexp
+  B_true  "B(true) = (%s. True)"
+  B_false "B(false) = (%s. False)"
+  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
+  B_not   "B(noti(b)) = (%s. ~(B b s))"
+  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+
+end