equal
deleted
inserted
replaced
12 |
12 |
13 definition |
13 definition |
14 dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where |
14 dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where |
15 "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))" |
15 "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))" |
16 |
16 |
17 consts D :: "com => state discr -> state lift" |
17 primrec D :: "com => state discr -> state lift" |
18 |
18 where |
19 primrec |
|
20 "D(\<SKIP>) = (LAM s. Def(undiscr s))" |
19 "D(\<SKIP>) = (LAM s. Def(undiscr s))" |
21 "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))" |
20 | "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))" |
22 "D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
21 | "D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
23 "D(\<IF> b \<THEN> c1 \<ELSE> c2) = |
22 | "D(\<IF> b \<THEN> c1 \<ELSE> c2) = |
24 (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
23 (LAM s. if b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)" |
25 "D(\<WHILE> b \<DO> c) = |
24 | "D(\<WHILE> b \<DO> c) = |
26 fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s) |
25 fix\<cdot>(LAM w s. if b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s) |
27 else Def(undiscr s))" |
26 else Def(undiscr s))" |
28 |
27 |
29 subsection |
28 subsection |
30 "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |
29 "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL" |