Initial population.

1 files changed, 325 insertions, 0 deletions

diff --git a/src/algebra/equation2.spad.pamphlet b/src/algebra/equation2.spad.pamphlet
new file mode 100644
index 00000000..8ae385bb
--- /dev/null
+++ b/src/algebra/equation2.spad.pamphlet
@@ -0,0 +1,325 @@
+\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}