|
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 |
|
|
|
11 |
Up1 = Cfun3 + Sum +
|
|
|
12 |
|
|
|
13 |
(* new type for lifting *)
|
|
|
14 |
|
|
2640
|
15 |
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
|
|
2278
|
16 |
|
|
|
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))"
|
|
|
23 |
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
|
|
2640
|
24 |
less_up_def "less == (%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
|