src/HOLCF/One.thy
author nipkow
Thu Oct 06 18:40:18 1994 +0100 (1994-10-06)
changeset 625 119391dd1d59
parent 243 c22b85994e17
child 1168 74be52691d62
permissions -rw-r--r--
New version
     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   one_def	"one == abs_one[up[UU]]"
    36   one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
    37 
    38 end
    39 
    40 
    41 
    42 
    43