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
nipkow@243
     1
(*  Title: 	HOLCF/one.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@625
     6
Introduce atomic type one = (void)u
nipkow@243
     7
nipkow@625
     8
The type is axiomatized as the least solution of a domain equation.
nipkow@625
     9
The functor term that specifies the domain equation is: 
nipkow@243
    10
nipkow@625
    11
  FT = <U,K_{void}>
nipkow@243
    12
nipkow@625
    13
For details see chapter 5 of:
nipkow@243
    14
nipkow@625
    15
[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
nipkow@625
    16
                     Dissertation, Technische Universit"at M"unchen, 1994
nipkow@243
    17
nipkow@243
    18
*)
nipkow@243
    19
nipkow@243
    20
One = ccc1+
nipkow@243
    21
nipkow@243
    22
types one 0
nipkow@243
    23
arities one :: pcpo
nipkow@243
    24
nipkow@243
    25
consts
nipkow@243
    26
	abs_one		:: "(void)u -> one"
nipkow@243
    27
	rep_one		:: "one -> (void)u"
nipkow@243
    28
	one 		:: "one"
nipkow@243
    29
	one_when 	:: "'c -> one -> 'c"
nipkow@243
    30
nipkow@243
    31
rules
nipkow@243
    32
  abs_one_iso	"abs_one[rep_one[u]] = u"
nipkow@243
    33
  rep_one_iso  "rep_one[abs_one[x]] = x"
nipkow@243
    34
nipkow@243
    35
  one_def	"one == abs_one[up[UU]]"
nipkow@243
    36
  one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
nipkow@243
    37
nipkow@243
    38
end
nipkow@243
    39
nipkow@243
    40
nipkow@243
    41
nipkow@243
    42
nipkow@243
    43