IMP/Denotation.thy

   B     :: "bexp => state => bool"
   C     :: "com => (state*state)set"
   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) ==   \
 \		   (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \
 \	                 {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