src/HOLCF/IMP/Denotational.thy
changeset 12032 0f6417c9a187
parent 10835 f4745d77e620
child 12338 de0f4a63baa5
equal deleted inserted replaced
12031:1b883fa9458e 12032:0f6417c9a187
     8 
     8 
     9 Denotational = HOLCF + Natural +
     9 Denotational = HOLCF + Natural +
    10 
    10 
    11 constdefs
    11 constdefs
    12    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
    12    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
    13   "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))"
    13   "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
    14 
    14 
    15 consts D :: "com => state discr -> state lift"
    15 consts D :: "com => state discr -> state lift"
    16 
    16 
    17 primrec
    17 primrec
    18   "D(SKIP) = (LAM s. Def(undiscr s))"
    18   "D(SKIP) = (LAM s. Def(undiscr s))"