| author | nipkow |
| Tue, 17 Oct 2000 08:00:46 +0200 | |
| changeset 10228 | e653cb933293 |
| parent 10212 | 33fe2d701ddd |
| child 10834 | a7897aebbffc |
| permissions | -rw-r--r-- |
| 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 |
||
| 10212 | 11 |
Up1 = Cfun3 + Sum_Type + Datatype + |
| 2278 | 12 |
|
13 |
(* new type for lifting *) |
|
14 |
||
| 2640 | 15 |
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
|
| 2278 | 16 |
|
|
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
17 |
instance u :: (sq_ord)sq_ord |
|
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
18 |
|
| 2278 | 19 |
consts |
20 |
Iup :: "'a => ('a)u"
|
|
21 |
Ifup :: "('a->'b)=>('a)u => 'b"
|
|
22 |
||
23 |
defs |
|
24 |
Iup_def "Iup x == Abs_Up(Inr(x))" |
|
25 |
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z" |
|
| 3842 | 26 |
less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of |
| 2278 | 27 |
Inl(y1) => True |
28 |
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False |
|
29 |
| Inr(z2) => y2<<z2))" |
|
30 |
end |