src/HOLCF/One.thy
 author oheimb Fri Nov 29 12:15:33 1996 +0100 (1996-11-29) changeset 2275 dbce3dce821a parent 1479 21eb5e156d91 child 2640 ee4dfce170a0 permissions -rw-r--r--
renamed is_flat to flat,
moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
(*lift* to *up*, except Ilift to Ifup, lift to fup)
```     1 (*  Title:      HOLCF/one.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Franz Regensburger
```
```     4     Copyright   1993 Technische Universitaet Muenchen
```
```     5
```
```     6 Introduce atomic type one = (void)u
```
```     7
```
```     8 The type is axiomatized as the least solution of a domain equation.
```
```     9 The functor term that specifies the domain equation is:
```
```    10
```
```    11   FT = <U,K_{void}>
```
```    12
```
```    13 For details see chapter 5 of:
```
```    14
```
```    15 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
```
```    16                      Dissertation, Technische Universit"at M"unchen, 1994
```
```    17
```
```    18 *)
```
```    19
```
```    20 One = ccc1+
```
```    21
```
```    22 types one 0
```
```    23 arities one :: pcpo
```
```    24
```
```    25 consts
```
```    26         abs_one         :: "(void)u -> one"
```
```    27         rep_one         :: "one -> (void)u"
```
```    28         one             :: "one"
```
```    29         one_when        :: "'c -> one -> 'c"
```
```    30
```
```    31 rules
```
```    32   abs_one_iso   "abs_one`(rep_one`u) = u"
```
```    33   rep_one_iso   "rep_one`(abs_one`x) = x"
```
```    34
```
```    35 defs
```
```    36   one_def       "one == abs_one`(up`UU)"
```
```    37   one_when_def "one_when == (LAM c u.fup`(LAM x.c)`(rep_one`u))"
```
```    38
```
```    39 translations
```
```    40   "case l of one => t1" == "one_when`t1`l"
```
```    41
```
```    42 end
```
```    43
```
```    44
```
```    45
```
```    46
```
```    47
```