|
2278
|
1 |
(* Title: HOLCF/Up1.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Franz Regensburger
|
|
|
4 |
Copyright 1993 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
|
|
|
7 |
Lifting
|
|
|
8 |
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
Up1 = Cfun3 + Sum +
|
|
|
12 |
|
|
|
13 |
(* new type for lifting *)
|
|
|
14 |
|
|
|
15 |
types "u" 1
|
|
|
16 |
|
|
|
17 |
arities "u" :: (pcpo)term
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
|
|
|
21 |
Rep_Up :: "('a)u => (void + 'a)"
|
|
|
22 |
Abs_Up :: "(void + 'a) => ('a)u"
|
|
|
23 |
|
|
|
24 |
Iup :: "'a => ('a)u"
|
|
|
25 |
UU_up :: "('a)u"
|
|
|
26 |
Ifup :: "('a->'b)=>('a)u => 'b"
|
|
|
27 |
less_up :: "('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_Up_inverse "Abs_Up(Rep_Up(p)) = p"
|
|
|
35 |
Abs_Up_inverse "Rep_Up(Abs_Up(p)) = p"
|
|
|
36 |
|
|
|
37 |
(*defining the abstract constants*)
|
|
|
38 |
|
|
|
39 |
defs
|
|
|
40 |
|
|
|
41 |
UU_up_def "UU_up == Abs_Up(Inl(UU))"
|
|
|
42 |
Iup_def "Iup x == Abs_Up(Inr(x))"
|
|
|
43 |
|
|
|
44 |
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
|
|
|
45 |
|
|
|
46 |
less_up_def "less_up(x1)(x2) == (case Rep_Up(x1) of
|
|
|
47 |
Inl(y1) => True
|
|
|
48 |
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
|
|
|
49 |
| Inr(z2) => y2<<z2))"
|
|
|
50 |
|
|
|
51 |
end
|