src/HOLCF/One.thy
 author nipkow Wed Jan 19 17:35:01 1994 +0100 (1994-01-19) changeset 243 c22b85994e17 child 625 119391dd1d59 permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
```     1 (*  Title: 	HOLCF/one.thy
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Franz Regensburger
```
```     4     Copyright   1993 Technische Universitaet Muenchen
```
```     5
```
```     6 Introduve atomic type one = (void)u
```
```     7
```
```     8 This is the first type that is introduced using a domain isomorphism.
```
```     9 The type axiom
```
```    10
```
```    11 	arities one :: pcpo
```
```    12
```
```    13 and the continuity of the Isomorphisms are taken for granted. Since the
```
```    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
```
```    20 The partial ordering on type one is implicitly defined via the
```
```    21 isomorphism axioms and the continuity of abs_one and rep_one.
```
```    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
```
```    28 *)
```
```    29
```
```    30 One = ccc1+
```
```    31
```
```    32 types one 0
```
```    33 arities one :: pcpo
```
```    34
```
```    35 consts
```
```    36 	abs_one		:: "(void)u -> one"
```
```    37 	rep_one		:: "one -> (void)u"
```
```    38 	one 		:: "one"
```
```    39 	one_when 	:: "'c -> one -> 'c"
```
```    40
```
```    41 rules
```
```    42   abs_one_iso	"abs_one[rep_one[u]] = u"
```
```    43   rep_one_iso  "rep_one[abs_one[x]] = x"
```
```    44
```
```    45   one_def	"one == abs_one[up[UU]]"
```
```    46   one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
```
```    47
```
```    48 end
```
```    49
```
```    50
```
```    51
```
```    52
```
```    53
```