src/HOLCF/one.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
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@243
     6
Introduve atomic type one = (void)u
nipkow@243
     7
nipkow@243
     8
This is the first type that is introduced using a domain isomorphism.
nipkow@243
     9
The type axiom 
nipkow@243
    10
nipkow@243
    11
	arities one :: pcpo
nipkow@243
    12
nipkow@243
    13
and the continuity of the Isomorphisms are taken for granted. Since the
nipkow@243
    14
type is not recursive, it could be easily introduced in a purely conservative
nipkow@243
    15
style as it was used for the types sprod, ssum, lift. The definition of the 
nipkow@243
    16
ordering is canonical using abstraction and representation, but this would take
nipkow@243
    17
again a lot of internal constants. It can easily be seen that the axioms below
nipkow@243
    18
are consistent.
nipkow@243
    19
nipkow@243
    20
The partial ordering on type one is implicitly defined via the
nipkow@243
    21
isomorphism axioms and the continuity of abs_one and rep_one.
nipkow@243
    22
nipkow@243
    23
We could also introduce the function less_one with definition
nipkow@243
    24
nipkow@243
    25
less_one(x,y) = rep_one[x] << rep_one[y]
nipkow@243
    26
nipkow@243
    27
nipkow@243
    28
*)
nipkow@243
    29
nipkow@243
    30
One = ccc1+
nipkow@243
    31
nipkow@243
    32
types one 0
nipkow@243
    33
arities one :: pcpo
nipkow@243
    34
nipkow@243
    35
consts
nipkow@243
    36
	abs_one		:: "(void)u -> one"
nipkow@243
    37
	rep_one		:: "one -> (void)u"
nipkow@243
    38
	one 		:: "one"
nipkow@243
    39
	one_when 	:: "'c -> one -> 'c"
nipkow@243
    40
nipkow@243
    41
rules
nipkow@243
    42
  abs_one_iso	"abs_one[rep_one[u]] = u"
nipkow@243
    43
  rep_one_iso  "rep_one[abs_one[x]] = x"
nipkow@243
    44
nipkow@243
    45
  one_def	"one == abs_one[up[UU]]"
nipkow@243
    46
  one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
nipkow@243
    47
nipkow@243
    48
end
nipkow@243
    49
nipkow@243
    50
nipkow@243
    51
nipkow@243
    52
nipkow@243
    53