--- a/src/HOL/IMP/Denotation.thy Wed Jun 25 21:25:51 2008 +0200
+++ b/src/HOL/IMP/Denotation.thy Wed Jun 25 22:01:34 2008 +0200
@@ -10,21 +10,19 @@
types com_den = "(state\<times>state)set"
-constdefs
- Gamma :: "[bexp,com_den] => (com_den => com_den)"
- "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+definition
+ Gamma :: "[bexp,com_den] => (com_den => com_den)" where
+ "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
{(s,t). s=t \<and> \<not>b s})"
-consts
- C :: "com => com_den"
-
-primrec
+primrec C :: "com => com_den"
+where
C_skip: "C \<SKIP> = Id"
- C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
- C_comp: "C (c0;c1) = C(c1) O C(c0)"
- C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
+| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
+| C_comp: "C (c0;c1) = C(c1) O C(c0)"
+| C_if: "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
{(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
- C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
+| C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
(**** mono (Gamma(b,c)) ****)