author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
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 |