src/HOL/IMP/Denotation.thy
changeset 32235 8f9b8d14fc9f
parent 27362 a6dc1769fdda
child 34055 fdf294ee08b2
     1.1 --- a/src/HOL/IMP/Denotation.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -12,14 +12,14 @@
     1.4  
     1.5  definition
     1.6    Gamma :: "[bexp,com_den] => (com_den => com_den)" where
     1.7 -  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
     1.8 +  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
     1.9                         {(s,t). s=t \<and> \<not>b s})"
    1.10  
    1.11  primrec C :: "com => com_den"
    1.12  where
    1.13    C_skip:   "C \<SKIP>   = Id"
    1.14  | C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    1.15 -| C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    1.16 +| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
    1.17  | C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    1.18                                                  {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    1.19  | C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"