| author | nipkow |
| Sun, 22 Dec 2002 10:43:43 +0100 | |
| changeset 13763 | f94b569cd610 |
| parent 12030 | 46d57d0290a2 |
| child 14981 | e73f8140af78 |
| permissions | -rw-r--r-- |
| 2278 | 1 |
(* Title: HOLCF/Up1.thy |
2 |
ID: $Id$ |
|
3 |
Author: Franz Regensburger |
|
| 12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
| 2278 | 5 |
|
| 12030 | 6 |
Lifting. |
| 2278 | 7 |
*) |
8 |
||
| 10212 | 9 |
Up1 = Cfun3 + Sum_Type + Datatype + |
| 2278 | 10 |
|
11 |
(* new type for lifting *) |
|
12 |
||
| 2640 | 13 |
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
|
| 2278 | 14 |
|
|
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
15 |
instance u :: (sq_ord)sq_ord |
|
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
16 |
|
| 2278 | 17 |
consts |
18 |
Iup :: "'a => ('a)u"
|
|
19 |
Ifup :: "('a->'b)=>('a)u => 'b"
|
|
20 |
||
21 |
defs |
|
22 |
Iup_def "Iup x == Abs_Up(Inr(x))" |
|
| 10834 | 23 |
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z" |
| 3842 | 24 |
less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of |
| 2278 | 25 |
Inl(y1) => True |
26 |
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False |
|
27 |
| Inr(z2) => y2<<z2))" |
|
28 |
end |