\documentclass{article}
\usepackage{open-axiom}
\begin{document}
\title{\$SPAD/src/algebra card.spad}
\author{Stephen M. Watt}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
\section{domain CARD CardinalNumber}
<<domain CARD CardinalNumber>>=
import Boolean
import NonNegativeInteger
)abbrev domain CARD CardinalNumber
++ Author: S.M. Watt
++ Date Created: June 1986
++ Date Last Updated: May 1990
++ Basic Operations: Aleph, +, -, *, **
++ Related Domains: 
++ Also See:
++ AMS Classifications:
++ Keywords: cardinal number, transfinite arithmetic
++ Examples:
++ References:
++   Goedel, "The consistency of the continuum hypothesis",
++   Ann. Math. Studies, Princeton Univ. Press, 1940
++ Description:
++   Members of the domain CardinalNumber are values indicating the
++   cardinality of sets, both finite and infinite.  Arithmetic operations
++   are defined on cardinal numbers as follows.
++
++   If \spad{x = #X}  and  \spad{y = #Y} then
++     \spad{x+y  = #(X+Y)}   \tab{30}disjoint union
++     \spad{x-y  = #(X-Y)}   \tab{30}relative complement
++     \spad{x*y  = #(X*Y)}   \tab{30}cartesian product
++     \spad{x**y = #(X**Y)}  \tab{30}\spad{X**Y = \{g| g:Y->X\}}
++
++   The non-negative integers have a natural construction as cardinals
++     \spad{0 = #\{\}}, \spad{1 = \{0\}}, \spad{2 = \{0, 1\}}, ..., \spad{n = \{i| 0 <= i < n\}}.
++
++   That \spad{0} acts as a zero for the multiplication of cardinals is
++   equivalent to the axiom of choice.
++
++   The generalized continuum hypothesis asserts 
++   \center{\spad{2**Aleph i = Aleph(i+1)}}
++   and is independent of the axioms of set theory [Goedel 1940].
++
++   Three commonly encountered cardinal numbers are
++      \spad{a = #Z}       \tab{30}countable infinity
++      \spad{c = #R}       \tab{30}the continuum
++      \spad{f = #\{g| g:[0,1]->R\}}
++
++   In this domain, these values are obtained using
++      \spad{a := Aleph 0}, \spad{c := 2**a}, \spad{f := 2**c}.
++
CardinalNumber: Join(OrderedSet, AbelianMonoid, Monoid,
                        RetractableTo NonNegativeInteger) with
        commutative "*"
            ++ a domain D has \spad{commutative("*")} if it has an operation
            ++ \spad{"*": (D,D) -> D} which is commutative.
        -: (%,%) -> Union(%,"failed")
           ++ \spad{x - y} returns an element z such that \spad{z+y=x} or "failed" 
           ++ if no such element exists.
        **: (%, %) -> %
            ++ \spad{x**y} returns \spad{#(X**Y)} where \spad{X**Y} is defined
            ++  as \spad{\{g| g:Y->X\}}.

        Aleph: NonNegativeInteger -> %
            ++ Aleph(n) provides the named (infinite) cardinal number.

        finite?: % -> Boolean
            ++ finite?(\spad{a}) determines whether 
            ++ \spad{a} is a finite cardinal,
            ++ i.e. an integer.

        countable?: % -> Boolean
            ++ countable?(\spad{a}) determines 
            ++ whether \spad{a} is a countable cardinal,
            ++ i.e. an integer or \spad{Aleph 0}.

        generalizedContinuumHypothesisAssumed?: () -> Boolean
            ++ generalizedContinuumHypothesisAssumed?()
            ++ tests if the hypothesis is currently assumed.

        generalizedContinuumHypothesisAssumed:  Boolean -> Boolean
            ++ generalizedContinuumHypothesisAssumed(bool)
            ++ is used to dictate whether the hypothesis is to be assumed.
    == add
        NNI ==> NonNegativeInteger
        FINord   ==> -1
        DUMMYval ==> -1
 
        Rep := Record(order: Integer, ival: Integer)
 
        GCHypothesis: Reference(Boolean) := ref false
 
        -- Creation
        0           == [FINord, 0]
        1           == [FINord, 1]
        coerce(n:NonNegativeInteger):% == [FINord, n]
        Aleph n     == [n, DUMMYval]
 
        -- Output
        ALEPHexpr := "Aleph"::OutputForm
 
        coerce(x: %): OutputForm ==
            x.order = FINord => (x.ival)::OutputForm
            prefix(ALEPHexpr, [(x.order)::OutputForm])
 
        -- Manipulation
        x = y ==
            x.order ~= y.order => false
            finite? x          => x.ival = y.ival
            true     -- equal transfinites
        x < y ==
            x.order < y.order => true
            x.order > y.order => false
            finite? x         => x.ival < y.ival
            false    -- equal transfinites
        x:% + y:% ==
            finite? x and finite? y => [FINord, x.ival+y.ival]
            max(x, y)
        x - y ==
            x < y     => "failed"
            finite? x => [FINord, x.ival-y.ival]
            x > y     => x
            "failed" -- equal transfinites
        x:% * y:% ==
            finite? x and finite? y => [FINord, x.ival*y.ival]
            x = 0 or y = 0          => 0
            max(x, y)
        n:NonNegativeInteger * x:% ==
            finite? x => [FINord, n*x.ival]
            n = 0     => 0
            x
        (x: %) ** (y: %) ==
            y = 0 =>
                x ~= 0 => 1
                error "0**0 not defined for cardinal numbers."
            finite? y =>
                not finite? x => x
                [FINord,x.ival**(y.ival):NNI]
            x = 0 => 0
            x = 1 => 1
            deref GCHypothesis => [max(x.order-1, y.order) + 1, DUMMYval]
            error "Transfinite exponentiation only implemented under GCH"
 
        finite? x    == x.order = FINord
        countable? x == x.order < 1
 
        retract(x:%):NonNegativeInteger ==
          finite? x => (x.ival)::NNI
          error "Not finite"
 
        retractIfCan(x:%):Union(NonNegativeInteger, "failed") ==
          finite? x => (x.ival)::NNI
          "failed"
 
        -- State manipulation
        generalizedContinuumHypothesisAssumed?() == deref GCHypothesis
        generalizedContinuumHypothesisAssumed b == setref(GCHypothesis,b)

@
\section{License}
<<license>>=
--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
@
<<*>>=
<<license>>

<<domain CARD CardinalNumber>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}