src/HOLCF/One.thy
author clasohm
Tue Feb 06 12:42:31 1996 +0100 (1996-02-06)
changeset 1479 21eb5e156d91
parent 1274 ea0668a1c0ba
child 2275 dbce3dce821a
permissions -rw-r--r--
expanded tabs
     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.lift`(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