\documentclass{article}
\usepackage{axiom}
\begin{document}
\title{\$SPAD/src/algebra equation2.spad}
\author{Stephen M. Watt, Johannes Grabmeier}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
\section{domain EQ Equation}
<<domain EQ Equation>>=
)abbrev domain EQ Equation
--FOR THE BENEFIT  OF LIBAX0 GENERATION
++ Author: Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: April 1985
++ Date Last Updated: June 3, 1991; September 2, 1992
++ Basic Operations: =
++ Related Domains:
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   Equations as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "=" to "equation".  Otherwise, it will
--   find a modemap for "=" in the domain of the arguments.

Equation(S: Type): public == private where
  Ex ==> OutputForm
  public ==> Type with
    "=": (S, S) -> $
        ++ a=b creates an equation.
    equation: (S, S) -> $
        ++ equation(a,b) creates an equation.
    swap: $ -> $
        ++ swap(eq) interchanges left and right hand side of equation eq.
    lhs: $ -> S
        ++ lhs(eqn) returns the left hand side of equation eqn.
    rhs: $ -> S
        ++ rhs(eqn) returns the right hand side of equation eqn.
    map: (S -> S, $) -> $
        ++ map(f,eqn) constructs a new equation by applying f to both
        ++ sides of eqn.
    if S has InnerEvalable(Symbol,S) then
             InnerEvalable(Symbol,S)
    if S has SetCategory then
        SetCategory
        CoercibleTo Boolean
        if S has Evalable(S) then
           eval: ($, $) -> $
               ++ eval(eqn, x=f) replaces x by f in equation eqn.
           eval: ($, List $) -> $
               ++ eval(eqn, [x1=v1, ... xn=vn]) replaces xi by vi in equation eqn.
    if S has AbelianSemiGroup then
        AbelianSemiGroup
        "+": (S, $) -> $
            ++ x+eqn produces a new equation by adding x to both sides of
            ++ equation eqn.
        "+": ($, S) -> $
            ++ eqn+x produces a new equation by adding x to  both sides of
            ++ equation eqn.
    if S has AbelianGroup then
        AbelianGroup
        leftZero : $ -> $
          ++ leftZero(eq) subtracts the left hand side.
        rightZero : $ -> $
          ++ rightZero(eq) subtracts the right hand side.
        "-": (S, $) -> $
            ++ x-eqn produces a new equation by subtracting both sides of
            ++ equation eqn from x.
        "-": ($, S) -> $
            ++ eqn-x produces a new equation by subtracting x from  both sides of
            ++ equation eqn.
    if S has SemiGroup then
        SemiGroup
        "*": (S, $) -> $
            ++ x*eqn produces a new equation by multiplying both sides of
            ++ equation eqn by x.
        "*": ($, S) -> $
            ++ eqn*x produces a new equation by multiplying both sides of
            ++ equation eqn by x.
    if S has Monoid then
        Monoid
        leftOne : $ -> Union($,"failed")
          ++ leftOne(eq) divides by the left hand side, if possible.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(eq) divides by the right hand side, if possible.
    if S has Group then
        Group
        leftOne : $ -> Union($,"failed")
          ++ leftOne(eq) divides by the left hand side.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(eq) divides by the right hand side.
    if S has Ring then
      Ring
      BiModule(S,S)
    if S has CommutativeRing then
      Module(S)
      --Algebra(S)
    if S has IntegralDomain then
      factorAndSplit : $ -> List $
        ++ factorAndSplit(eq) make the right hand side 0 and
        ++ factors the new left hand side. Each factor is equated
        ++ to 0 and put into the resulting list without repetitions.
    if S has PartialDifferentialRing(Symbol) then
      PartialDifferentialRing(Symbol)
    if S has Field then
      VectorSpace(S)
      "/": ($, $) -> $
          ++ e1/e2 produces a new equation by dividing the left and right
          ++ hand sides of equations e1 and e2.
      inv: $ -> $
          ++ inv(x) returns the multiplicative inverse of x.
    if S has ExpressionSpace then
        subst: ($, $) -> $
             ++ subst(eq1,eq2) substitutes eq2 into both sides of eq1
             ++ the lhs of eq2 should be a kernel

  private ==> add
    Rep := Record(lhs: S, rhs: S)
    eq1,eq2: $
    s : S
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [equation(rcf.factor,0) for rcf in factors factor lhs eq0]
          [eq]
    l:S = r:S      == [l, r]
    equation(l, r) == [l, r]    -- hack!  See comment above.
    lhs eqn        == eqn.lhs
    rhs eqn        == eqn.rhs
    swap eqn     == [rhs eqn, lhs eqn]
    map(fn, eqn)   == equation(fn(eqn.lhs), fn(eqn.rhs))

    if S has InnerEvalable(Symbol,S) then
        s:Symbol
        ls:List Symbol
        x:S
        lx:List S
        eval(eqn,s,x) == eval(eqn.lhs,s,x) = eval(eqn.rhs,s,x)
        eval(eqn,ls,lx) == eval(eqn.lhs,ls,lx) = eval(eqn.rhs,ls,lx)
    if S has Evalable(S) then
        eval(eqn1:$, eqn2:$):$ ==
           eval(eqn1.lhs, eqn2 pretend Equation S) =
               eval(eqn1.rhs, eqn2 pretend Equation S)
        eval(eqn1:$, leqn2:List $):$ ==
           eval(eqn1.lhs, leqn2 pretend List Equation S) =
               eval(eqn1.rhs, leqn2 pretend List Equation S)
    if S has SetCategory then
        eq1 = eq2 == (eq1.lhs = eq2.lhs)@Boolean and
                     (eq1.rhs = eq2.rhs)@Boolean
        coerce(eqn:$):Ex == eqn.lhs::Ex = eqn.rhs::Ex
        coerce(eqn:$):Boolean == eqn.lhs = eqn.rhs
    if S has AbelianSemiGroup then
        eq1 + eq2 == eq1.lhs + eq2.lhs = eq1.rhs + eq2.rhs
        s + eq2 == [s,s] + eq2
        eq1 + s == eq1 + [s,s]
    if S has AbelianGroup then
        - eq == (- lhs eq) = (-rhs eq)
        s - eq2 == [s,s] - eq2
        eq1 - s == eq1 - [s,s]
        leftZero eq == 0 = rhs eq - lhs eq
        rightZero eq == lhs eq - rhs eq = 0
        0 == equation(0$S,0$S)
        eq1 - eq2 == eq1.lhs - eq2.lhs = eq1.rhs - eq2.rhs
    if S has SemiGroup then
        eq1:$ * eq2:$ == eq1.lhs * eq2.lhs = eq1.rhs * eq2.rhs
        l:S   * eqn:$ == l       * eqn.lhs = l       * eqn.rhs
        l:S * eqn:$  ==  l * eqn.lhs    =    l * eqn.rhs
        eqn:$ * l:S  ==  eqn.lhs * l    =    eqn.rhs * l
        -- We have to be a bit careful here: raising to a +ve integer is OK
        -- (since it's the equivalent of repeated multiplication)
        -- but other powers may cause contradictions
        -- Watch what else you add here! JHD 2/Aug 1990
    if S has Monoid then
        1 == equation(1$S,1$S)
        recip eq ==
          (lh := recip lhs eq) case "failed" => "failed"
          (rh := recip rhs eq) case "failed" => "failed"
          [lh :: S, rh :: S]
        leftOne eq ==
          (re := recip lhs eq) case "failed" => "failed"
          1 = rhs eq * re
        rightOne eq ==
          (re := recip rhs eq) case "failed" => "failed"
          lhs eq * re = 1
    if S has Group then
        inv eq == [inv lhs eq, inv rhs eq]
        leftOne eq == 1 = rhs eq * inv rhs eq
        rightOne eq == lhs eq * inv rhs eq = 1
    if S has Ring then
        characteristic() == characteristic()$S
        i:Integer * eq:$ == (i::S) * eq
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [equation(rcf.factor,0) for rcf in factors factor lhs eq0]
          (S has Polynomial Integer) =>
            eq0 := rightZero eq
            MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _
               Integer, Polynomial Integer)
            p : Polynomial Integer := (lhs eq0) pretend Polynomial Integer
            [equation((rcf.factor) pretend S,0) for rcf in factors factor(p)$MF]
          [eq]
    if S has PartialDifferentialRing(Symbol) then
        differentiate(eq:$, sym:Symbol):$ ==
           [differentiate(lhs eq, sym), differentiate(rhs eq, sym)]
    if S has Field then
        dimension() == 2 :: CardinalNumber
        eq1:$ / eq2:$ == eq1.lhs / eq2.lhs = eq1.rhs / eq2.rhs
        inv eq == [inv lhs eq, inv rhs eq]
    if S has ExpressionSpace then
        subst(eq1,eq2) ==
            eq3 := eq2 pretend Equation S
            [subst(lhs eq1,eq3),subst(rhs eq1,eq3)]

@
\section{package EQ2 EquationFunctions2}
<<package EQ2 EquationFunctions2>>=
)abbrev package EQ2 EquationFunctions2
++ Author:
++ Date Created:
++ Date Last Updated: June 3, 1991
++ Basic Operations:
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   This package provides operations for mapping the sides of equations.
EquationFunctions2(S: Type, R: Type): with
    map: (S ->R ,Equation S) -> Equation R
	++ map(f,eq) returns an equation where f is applied to the sides of eq
 == add
    map(fn, eqn) == equation(fn lhs eqn, fn rhs eqn)

@
\section{category FEVALAB FullyEvalableOver}
<<category FEVALAB FullyEvalableOver>>=
)abbrev category FEVALAB FullyEvalableOver
++ Author:
++ Date Created:
++ Date Last Updated: June 3, 1991
++ Basic Operations:
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++    This category provides a selection of evaluation operations
++    depending on what the argument type R provides.
FullyEvalableOver(R:SetCategory): Category == with
    map: (R -> R, $) -> $
        ++ map(f, ex) evaluates ex, applying f to values of type R in ex.
    if R has Eltable(R, R) then Eltable(R, $)
    if R has Evalable(R) then Evalable(R)
    if R has InnerEvalable(Symbol, R) then InnerEvalable(Symbol, R)
 add
    if R has Eltable(R, R) then
      elt(x:$, r:R) == map(#1.r, x)

    if R has Evalable(R) then
      eval(x:$, l:List Equation R) == map(eval(#1, l), x)

    if R has InnerEvalable(Symbol, R) then
      eval(x:$, ls:List Symbol, lv:List R) == map(eval(#1, ls, lv), x)

@
\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 EQ Equation>>
<<package EQ2 EquationFunctions2>>
<<category FEVALAB FullyEvalableOver>>
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}