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