--- a/src/HOL/IMP/Denotation.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Denotation.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/Denotation.thy
+(* Title: HOL/IMP/Denotation.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Denotational semantics of expressions & commands
@@ -16,31 +16,31 @@
Gamma :: [bexp,com_den] => (com_den => com_den)
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))"
+ 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))"
+ 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))"
defs
- Gamma_def "Gamma b cd ==
- (%phi.{st. st : (phi O cd) & B b (fst st)} Un
- {st. st : id & ~B b (fst st)})"
+ Gamma_def "Gamma b cd ==
+ (%phi.{st. st : (phi O cd) & B b (fst st)} Un
+ {st. st : id & ~B b (fst st)})"
primrec C com
C_skip "C(skip) = id"
C_assign "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
- C_if "C(ifc b then c0 else c1) =
- {st. st:C(c0) & (B b (fst st))} Un
- {st. st:C(c1) & ~(B b (fst st))}"
+ C_if "C(ifc b then c0 else c1) =
+ {st. st:C(c0) & (B b (fst st))} Un
+ {st. st:C(c1) & ~(B b (fst st))}"
C_while "C(while b do c) = lfp (Gamma b (C c))"
end