1.1 --- a/src/HOL/IMP/Denotation.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -10,21 +10,19 @@
     1.4  
     1.5  types com_den = "(state\<times>state)set"
     1.6  
     1.7 -constdefs
     1.8 -  Gamma :: "[bexp,com_den] => (com_den => com_den)"
     1.9 -  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
    1.10 +definition
    1.11 +  Gamma :: "[bexp,com_den] => (com_den => com_den)" where
    1.12 +  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
    1.13                         {(s,t). s=t \<and> \<not>b s})"
    1.14  
    1.15 -consts
    1.16 -  C :: "com => com_den"
    1.17 -
    1.18 -primrec
    1.19 +primrec C :: "com => com_den"
    1.20 +where
    1.21    C_skip:   "C \<SKIP>   = Id"
    1.22 -  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    1.23 -  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    1.24 -  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    1.25 +| C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    1.26 +| C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    1.27 +| C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    1.28                                                  {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    1.29 -  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    1.30 +| C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    1.31  
    1.32  
    1.33  (**** mono (Gamma(b,c)) ****)