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
clasohm@1479
     1
(*  Title:      HOLCF/one.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     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
clasohm@1479
    26
        abs_one         :: "(void)u -> one"
clasohm@1479
    27
        rep_one         :: "one -> (void)u"
clasohm@1479
    28
        one             :: "one"
clasohm@1479
    29
        one_when        :: "'c -> one -> 'c"
nipkow@243
    30
nipkow@243
    31
rules
clasohm@1479
    32
  abs_one_iso   "abs_one`(rep_one`u) = u"
clasohm@1479
    33
  rep_one_iso   "rep_one`(abs_one`x) = x"
nipkow@243
    34
regensbu@1168
    35
defs
clasohm@1479
    36
  one_def       "one == abs_one`(up`UU)"
regensbu@1168
    37
  one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
regensbu@1274
    38
regensbu@1274
    39
translations
regensbu@1274
    40
  "case l of one => t1" == "one_when`t1`l"
regensbu@1274
    41
nipkow@243
    42
end
nipkow@243
    43
nipkow@243
    44
nipkow@243
    45
nipkow@243
    46
nipkow@243
    47