equal
deleted
inserted
replaced
15 datatype 'a u = Ibottom | Iup 'a |
15 datatype 'a u = Ibottom | Iup 'a |
16 |
16 |
17 syntax (xsymbols) |
17 syntax (xsymbols) |
18 "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999) |
18 "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999) |
19 |
19 |
20 consts |
20 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where |
21 Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" |
21 "Ifup f Ibottom = \<bottom>" |
22 |
22 | "Ifup f (Iup x) = f\<cdot>x" |
23 primrec |
|
24 "Ifup f Ibottom = \<bottom>" |
|
25 "Ifup f (Iup x) = f\<cdot>x" |
|
26 |
23 |
27 subsection {* Ordering on lifted cpo *} |
24 subsection {* Ordering on lifted cpo *} |
28 |
25 |
29 instantiation u :: (cpo) below |
26 instantiation u :: (cpo) below |
30 begin |
27 begin |