[Axiom-developer] [Cartesian Product] (new)

[Bill Page]

Changes http://page.axiom-developer.org/zope/mathaction/CartesianProduct/diff
--
++ This domain implements cartesian product

\begin{axiom}
)show Product
\end{axiom}

\begin{axiom}
)abbrev domain PRODUCT Product
Product (A:SetCategory,B:SetCategory) : C == T
 where
  C == SetCategory  with
       if A has Finite and B has Finite then Finite
       if A has Monoid and B has Monoid then Monoid
       if A has AbelianMonoid and B has AbelianMonoid then AbelianMonoid
       if A has CancellationAbelianMonoid and
          B has CancellationAbelianMonoid then CancellationAbelianMonoid
       if A has Group  and B has Group  then  Group
       if A has AbelianGroup and B has AbelianGroup then  AbelianGroup
       if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup
                                             then OrderedAbelianMonoidSup
       if A has OrderedSet and B has OrderedSet then  OrderedSet
 
       makeprod     : (A,B) -> %
        ++ makeprod(a,b) \undocumented
       selectfirst  :   %   -> A
        ++ selectfirst(x) \undocumented
       selectsecond :   %   -> B
        ++ selectsecond(x) \undocumented
 
  T == add
 
    --representations
       Rep := Record(acomp:A,bcomp:B)
 
    --declarations
       x,y: %
       i: NonNegativeInteger
       p: NonNegativeInteger
       a: A
       b: B
       d: Integer
 
    --define
       coerce(x):OutputForm == paren [(x.acomp)::OutputForm,
                                      (x.bcomp)::OutputForm]
       x=y ==
           x.acomp = y.acomp => x.bcomp = y.bcomp
           false
       makeprod(a:A,b:B) :%   == [a,b]
 
       selectfirst(x:%) : A   == x.acomp
 
       selectsecond (x:%) : B == x.bcomp
 
       if A has Monoid and B has Monoid then
          1 == [1$A,1$B]
          x * y == [x.acomp * y.acomp,x.bcomp * y.bcomp]
          x ** p == [x.acomp ** p ,x.bcomp ** p]
 
       if A has Finite and B has Finite then
          size == size$A () * size$B ()
 
       if A has Group and B has Group then
          inv(x) == [inv(x.acomp),inv(x.bcomp)]
 
       if A has AbelianMonoid and B has AbelianMonoid then
          0 == [0$A,0$B]
 
          x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp]
 
          c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp]
 
       if A has CancellationAbelianMonoid and
          B has CancellationAbelianMonoid then
            subtractIfCan(x, y) : Union(%,"failed") ==
              (na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed"
              (nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed"
              [na::A,nb::B]
 
       if A has AbelianGroup and B has AbelianGroup then
          - x == [- x.acomp,-x.bcomp]
          (x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp]
          d * x == [d * x.acomp,d * x.bcomp]
 
       if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
          sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)]
 
       if A has OrderedSet and B has OrderedSet then
          x < y ==
               xa:= x.acomp ; ya:= y.acomp
               xa < ya => true
               xb:= x.bcomp ; yb:= y.bcomp
               xa = ya => (xb < yb)
               false
 
--     coerce(x:%):Symbol ==
--      PrintableForm()
--      formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm
\end{axiom}

--
forwarded from http://page.axiom-developer.org/zope/mathaction/address@hidden