--- a/IMP/Denotation.thy Tue Sep 06 16:15:59 1994 +0200
+++ b/IMP/Denotation.thy Tue Sep 06 16:46:27 1994 +0200
@@ -15,20 +15,18 @@
Gamma :: "[bexp,com,(state*state)set] => (state*state)set"
primrec A aexp
- A_nat_def "A(N(n)) = (%s. n)"
- A_loc_def "A(X(x)) = (%s. s(x))"
- A_op1_def "A(Op1(f,a)) = (%s. f(A(a,s)))"
- A_op2_def "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_def "B(true) = (%s. True)"
- B_false_def "B(false) = (%s. False)"
- B_op_def "B(ROp(f,a0,a1)) = (%s. f(A(a0,s),A(a1,s)))"
-
-
- B_not_def "B(noti(b)) = (%s. ~B(b,s))"
- B_and_def "B(b0 andi b1) = (%s. B(b0,s) & B(b1,s))"
- B_or_def "B(b0 ori b1) = (%s. B(b0,s) | B(b1,s))"
+ 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))"
defs
Gamma_def "Gamma(b,c) == \
@@ -36,12 +34,12 @@
\ {io. io : id & ~B(b,fst(io))})"
primrec C com
- C_skip_def "C(skip) = id"
- C_assign_def "C(x := a) = {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
- C_comp_def "C(c0 ; c1) = C(c1) O C(c0)"
- C_if_def "C(ifc b then c0 else c1) = \
+ C_skip "C(skip) = id"
+ C_assign "C(x := a) = {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
+ C_comp "C(c0 ; c1) = C(c1) O C(c0)"
+ C_if "C(ifc b then c0 else c1) = \
\ {io. io:C(c0) & B(b,fst(io))} Un \
\ {io. io:C(c1) & ~B(b,fst(io))}"
- C_while_def "C(while b do c) = lfp(Gamma(b,c))"
+ C_while "C(while b do c) = lfp(Gamma(b,c))"
end