Edit detail for SandBoxSum revision 2 of 14

spad
)abbrev domain SUM Sum
++ Description:
++ This domain implements direct union
Sum (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
       selectsum     : % -> Union(acomp:A,bcomp:B)
        ++ selectsum(x) \undocumented
       makefirst  :   A -> %
        ++ makefirst(a) \undocumented
       makesecond :   B -> %
        ++ makesecond(b) \undocumented
  T == add
    --representations
       Rep := Union(acomp:A,bcomp:B)
    --declarations
       x,y: %
       i: NonNegativeInteger
       p: NonNegativeInteger
       a: A
       b: B
       d: Integer
    --define
       coerce(x):OutputForm ==
         x case acomp => (x.acomp)::OutputForm
         (x.bcomp)::OutputForm
       x=y == rep(x)= rep(y)
       selectsum(x:%) == rep(x)
       makefirst(a:A) : %   == per construct(a)$REP
       makesecond (b:B) : % == per construct(b)$REP
       if A has Monoid and B has Monoid then
          -- represent unit of Sum(A,B) as use 1$A (We could use either 1$A or 1$B)
          1 == per construct(1$A)$REP
          x * y == x case acomp and y case acomp => per construct(rep(x).acomp * rep(y).acomp)$REP
                   x case bcomp and y case bcomp => per construct(rep(x).bcomp * rep(y).bcomp)$REP
                   -- unit of Sum(A,B)=1$A is unit for B
                   x case acomp and x.acomp=1$A and y case bcomp => y
                   error "not same type"
          x ** p == x case acomp => per construct(rep(x).acomp ** p)$REP
                   per construct(rep(x).bcomp ** p)$REP
       if A has Finite and B has Finite then
          size == size$A + size$B
          index(n) == n > size$B => per construct(index((n::Integer - size$B)::PositiveInteger)$A)$REP
                      per construct(index(n)$B)$REP
          random() == random()$Boolean => per construct(random()$A)$REP
                      per construct(random()$B)REP
          lookup(x) == x case acomp => lookup(x.acomp)$A + size$B::Integer
                       lookup(x.bcomp)$B
          hash(x) == x case acomp => hash(x.acomp)$A + size$B::SingleInteger
                     hash(x.bcomp)$B
       if A has Group then
          inv(x) == x case acomp => per construct(inv(x.acomp))$REP
       if B has Group then
          inv(x) == x case bcomp => per construct(inv(x.bcomp))$REP
       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

axiom
size()$Sum(PF 7,PF 13)
   Sum is an unknown constructor and so is unavailable. Did you mean to
      use -> but type something different instead?
size()$Sum(PF 7,Product(PF 3,PF 13))
   Sum is an unknown constructor and so is unavailable. Did you mean to
      use -> but type something different instead?