1 (* Title: HOLCF/one.thy |
1 (* Title: HOLCF/one.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Introduve atomic type one = (void)u |
6 Introduce atomic type one = (void)u |
7 |
7 |
8 This is the first type that is introduced using a domain isomorphism. |
8 The type is axiomatized as the least solution of a domain equation. |
9 The type axiom |
9 The functor term that specifies the domain equation is: |
10 |
10 |
11 arities one :: pcpo |
11 FT = <U,K_{void}> |
12 |
12 |
13 and the continuity of the Isomorphisms are taken for granted. Since the |
13 For details see chapter 5 of: |
14 type is not recursive, it could be easily introduced in a purely conservative |
|
15 style as it was used for the types sprod, ssum, lift. The definition of the |
|
16 ordering is canonical using abstraction and representation, but this would take |
|
17 again a lot of internal constants. It can easily be seen that the axioms below |
|
18 are consistent. |
|
19 |
14 |
20 The partial ordering on type one is implicitly defined via the |
15 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, |
21 isomorphism axioms and the continuity of abs_one and rep_one. |
16 Dissertation, Technische Universit"at M"unchen, 1994 |
22 |
|
23 We could also introduce the function less_one with definition |
|
24 |
|
25 less_one(x,y) = rep_one[x] << rep_one[y] |
|
26 |
|
27 |
17 |
28 *) |
18 *) |
29 |
19 |
30 One = ccc1+ |
20 One = ccc1+ |
31 |
21 |