equal
deleted
inserted
replaced
6 Class Instance lift::(term)pcpo |
6 Class Instance lift::(term)pcpo |
7 *) |
7 *) |
8 |
8 |
9 Lift3 = Lift2 + |
9 Lift3 = Lift2 + |
10 |
10 |
11 default term |
11 instance lift :: (term)pcpo (cpo_lift,least_lift) |
12 |
|
13 arities |
|
14 "lift" :: (term)pcpo |
|
15 |
12 |
16 consts |
13 consts |
17 flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" |
14 flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" |
18 blift :: "bool => tr" |
|
19 plift :: "('a => bool) => 'a lift -> tr" |
|
20 flift2 :: "('a => 'b) => ('a lift -> 'b lift)" |
15 flift2 :: "('a => 'b) => ('a lift -> 'b lift)" |
21 |
16 |
22 translations |
17 translations |
23 "UU" <= "Undef" |
18 "UU" <= "Undef" |
24 |
19 |
25 defs |
20 defs |
26 blift_def |
|
27 "blift b == (if b then TT else FF)" |
|
28 |
|
29 flift1_def |
21 flift1_def |
30 "flift1 f == (LAM x. (case x of |
22 "flift1 f == (LAM x. (case x of |
31 Undef => UU |
23 Undef => UU |
32 | Def y => (f y)))" |
24 | Def y => (f y)))" |
33 |
|
34 flift2_def |
25 flift2_def |
35 "flift2 f == (LAM x. (case x of |
26 "flift2 f == (LAM x. (case x of |
36 Undef => Undef |
27 Undef => Undef |
37 | Def y => Def (f y)))" |
28 | Def y => Def (f y)))" |
38 |
29 |
39 plift_def |
|
40 "plift p == (LAM x. flift1 (%a. blift (p a))`x)" |
|
41 |
|
42 |
|
43 rules |
|
44 inst_lift_pcpo "(UU::'a lift) = Undef" |
|
45 |
|
46 end |
30 end |
47 |
31 |