src/HOLCF/One.thy
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 625 119391dd1d59
child 1274 ea0668a1c0ba
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
     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 end
    39 
    40 
    41 
    42 
    43