1.1 --- a/src/HOL/IMP/Expr.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Expr.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -68,23 +68,22 @@
     1.4  lemmas [intro] = tru fls ROp noti andi ori
     1.5  
     1.6  subsection "Denotational semantics of arithmetic and boolean expressions"
     1.7 -consts
     1.8 -  A     :: "aexp => state => nat"
     1.9 -  B     :: "bexp => state => bool"
    1.10  
    1.11 -primrec
    1.12 +primrec A :: "aexp => state => nat"
    1.13 +where
    1.14    "A(N(n)) = (%s. n)"
    1.15 -  "A(X(x)) = (%s. s(x))"
    1.16 -  "A(Op1 f a) = (%s. f(A a s))"
    1.17 -  "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.18 +| "A(X(x)) = (%s. s(x))"
    1.19 +| "A(Op1 f a) = (%s. f(A a s))"
    1.20 +| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.21  
    1.22 -primrec
    1.23 +primrec B :: "bexp => state => bool"
    1.24 +where
    1.25    "B(true) = (%s. True)"
    1.26 -  "B(false) = (%s. False)"
    1.27 -  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.28 -  "B(noti(b)) = (%s. ~(B b s))"
    1.29 -  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.30 -  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.31 +| "B(false) = (%s. False)"
    1.32 +| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.33 +| "B(noti(b)) = (%s. ~(B b s))"
    1.34 +| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.35 +| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.36  
    1.37  lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
    1.38    by (rule,cases set: evala) auto