equal
deleted
inserted
replaced
1 (* Title: HOLCF/lift1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 |
|
7 Lifting |
|
8 |
|
9 *) |
|
10 |
|
11 Lift1 = Cfun3 + |
|
12 |
|
13 (* new type for lifting *) |
|
14 |
|
15 types "u" 1 |
|
16 |
|
17 arities "u" :: (pcpo)term |
|
18 |
|
19 consts |
|
20 |
|
21 Rep_Lift :: "('a)u => (void + 'a)" |
|
22 Abs_Lift :: "(void + 'a) => ('a)u" |
|
23 |
|
24 Iup :: "'a => ('a)u" |
|
25 UU_lift :: "('a)u" |
|
26 Ilift :: "('a->'b)=>('a)u => 'b" |
|
27 less_lift :: "('a)u => ('a)u => bool" |
|
28 |
|
29 rules |
|
30 |
|
31 (*faking a type definition... *) |
|
32 (* ('a)u is isomorphic to void + 'a *) |
|
33 |
|
34 Rep_Lift_inverse "Abs_Lift(Rep_Lift(p)) = p" |
|
35 Abs_Lift_inverse "Rep_Lift(Abs_Lift(p)) = p" |
|
36 |
|
37 (*defining the abstract constants*) |
|
38 |
|
39 UU_lift_def "UU_lift == Abs_Lift(Inl(UU))" |
|
40 Iup_def "Iup(x) == Abs_Lift(Inr(x))" |
|
41 |
|
42 Ilift_def "Ilift(f)(x)==\ |
|
43 \ sum_case (Rep_Lift(x)) (%y.UU) (%z.f[z])" |
|
44 |
|
45 less_lift_def "less_lift(x1)(x2) == \ |
|
46 \ (sum_case (Rep_Lift(x1))\ |
|
47 \ (% y1.True)\ |
|
48 \ (% y2.sum_case (Rep_Lift(x2))\ |
|
49 \ (% z1.False)\ |
|
50 \ (% z2.y2<<z2)))" |
|
51 |
|
52 end |
|
53 |
|
54 |
|
55 |
|