equal
deleted
inserted
replaced
|
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 |