;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; If you load this file (with translation into the "KIF" implementation
;;; -- the default ), then the definitions are saved on property lists
;;; and can be used for online documentation and in cross-reference reports.

(in-package "ONTOLINGUA-USER")   ;inherits from the KIF package
                                 ;all constants defined here are exported
                                 ;from the KIF package.

(define-theory KIF-NUMBERS ()
  "The KIF vocabulary concerning numbers and arithmetic.")


(in-theory 'kif-numbers)


(define-class NUMBER (?x)
  "Number")

(define-class REAL-NUMBER (?x)
  "Real number"
  :def (number ?x))

(define-class RATIONAL-NUMBER (?x)
  "Rational number"
  :iff-def (and (real-number ?x)
                (exists (?y)
                   (and (integer ?y)
                        (integer (* ?x ?y))))))

(define-class INTEGER (?x)
  "Integer"
  :def (rational-number ?x))

(define-class EVEN-INTEGER (?x)
  "Even integer"
  :def (and (integer ?x)
            (= (mod ?x 2) 0)))

(define-class ODD-INTEGER (?x)
  "Odd integer"
  :def (and (integer ?x)
            (= (mod ?x 2) 1)))

(define-class NATURAL (?x)
  "Natural number"
  :iff-def (and (integer ?x)
                (> ?x 0)))

(define-class NONNEGATIVE-INTEGER (?x)
  "Nonnegative integer"
  :def (and (integer ?x)
            (>= ?x 0)))

(define-class POSITIVE (?x)
  "Positive number"
  :def (and (number ?x)
            (> ?x 0)))

(define-class NEGATIVE (?x)
  "Negative number"
  :def (and (number ?x)
            (< ?x 0)))

(define-class COMPLEX-NUMBER (?x)
  "Complex number"
  :def (number ?x))

(define-class ZERO (?x)
  "The class containing 0.  May be used as a predicate."
  :iff-def (= ?x 0))

(define-relation LOGBIT (?x ?y)
   "The sentence {\tt (logbit $\tau_1$ $\tau_2$)} is true if bit $\tau_2$
of $\tau_1$ is 1.")

(define-relation LOGTEST (?x ?y)
   "The sentence {\tt (logtest $\tau_1$ $\tau_2$)} is true if the logical
{\it and} of the two's-complement representation of the integers
$\tau_1$ and $\tau_2$ is not zero.")

;;;---Arithmetic Functions and friends

;;; These are deliberately not axiomatized, waiting for a
;;; proper treatment.  Might want to leave room for operator
;;; overloading.

(define-function * (@args) :-> ?product
  "If $\tau_1$, ..., $\tau_n$ denote numbers, then the term
 {\tt (* $\tau_1 \ldots \tau_n$)} denotes the product of those numbers.")

(define-function + (@args) :-> ?sum
  "If $\tau_1$, ..., $\tau_n$ are numerical constants, then the term 
{\tt (+ $\tau_1 ... \tau_n$)} denotes the sum $\tau$ of the numbers
corresponding to those constants.")

(define-function - (@args) :-> ?difference
   "If $\tau$ and $\tau_1$, ..., $\tau_n$ denote numbers, then the term 
{\tt (- $\tau$ $\tau_1 ... \tau_n$)} denotes the difference between the
number denoted by $\tau$ and the numbers denoted by $\tau_1$ through
$\tau_n$.  An exception occurs when $n=0$, in which case the term
denotes the negation of the number denoted by $\tau$.")

(define-function / (@args) :-> ?result
  "If $\tau_1$, ..., $\tau_n$ are numbers, then the term
{\tt (/ $\tau_1 ...  \tau_n$)} denotes the result $\tau$ obtained by 
dividing the number denoted by $\tau_1$ by the numbers denoted by
$\tau_2$ through $\tau_n$.  An exception occurs when $n=1$, in which
case the term denotes the reciprocal $\tau$ of the number denoted by
$\tau_1$.")

(define-function 1+ (?x) :-> ?result
  "The term {\tt (1+ $\tau$)} denotes the sum of the object denoted by
$\tau$ and 1."
  :lambda-body (+ ?x 1))

(define-function 1- (?x) :-> ?result
  "The term {\tt (1- $\tau$)} denotes the difference of the object denoted by
$\tau$ and 1."
  :lambda-body (- ?x 1))

(define-function ABS (?x)
  "The term {\tt (abs $\tau$)} denotes the absolute value of the object
denoted by $\tau$. "
  :lambda-body (if (>= ?x 0) ?x (- ?x)))

(define-function ACOS (?x)
   "If $\tau$ denotes a number, then the term {\tt (acos $\tau$)} denotes
the arc cosine of that number (in radians).")

(define-function ACOSH (?x)
   "The term {\tt (acosh $\tau$)} denotes the arc cosine of the
object denoted by $\tau$ (in radians).")

(define-function ASH (?x)
   "The term {\tt (ash $\tau_1$ $\tau_2$)} denotes the result of
arithmetically shifting the object denoted by $\tau_1$ by the number
of bits denoted by $\tau_2$ (left or right shifting depending on the
sign of $\tau_2$).")

(define-function ASIN (?x)
   "The term {\tt (asin $\tau$)} denotes the arc sine of the object
denoted by $\tau$ (in radians).")

(define-function ASINH (?x)
   "The term {\tt (asinh $\tau$)} denotes the hyperbolic arc sine of the
object denoted by $\tau$ (in radians).")

(define-function ATAN (?x)
   "The term {\tt (atan $\tau$)} denotes the arc tangent of the object
denoted by $\tau$ (in radians).")

(define-function ATANH (?x)
   "The term {\tt (atanh $\tau$)} denotes the hyperbolic arc tangent
of the object denoted by $\tau$ (in radians).")

(define-function BOOLE (?x)
   "The term {\tt (boole $\tau$ $\tau_1$ $\tau_2$)} denotes the
result of applying the operation denoted by $\tau$ to the objects
denoted by $\tau_1$ and $\tau_2$.")

(define-function CEILING (?x)
   "If $\tau$ denotes a real number, then the term 
{\tt (ceiling $\tau$)} denotes the smallest integer greater than or 
equal to the anumber denoted by $\tau$.")

(define-function CIS (?radians) :-> ?complex
   "The term {\tt (cis $\tau$)} denotes the complex number denoted by
$cos(\tau) + i sin(\tau)$.  The argument is any non-complex number of
radians."
   :def (and (number ?radians) (not (complex-number ?radians))
             (complex-number ?complex)))

(define-function CONJUGATE (?c) :-> ?complex
   "If $\tau$ denotes a complex number, then the term {\tt (conjugate
$\tau$)} denotes the complex conjugate of the number denoted by
$\tau$.")

(define-function COS (?x)
   "The term {\tt (cos $\tau$)} denotes the cosine of the object
denoted by $\tau$ (in radians).")

(define-function COSH (?x)
   "The term {\tt (cosh $\tau$)} denotes the hyperbolic cosine of the
object denoted by $\tau$ (in radians).")

(define-function DECODE-FLOAT (?x)
   "The term {\tt (decode-float $\tau$)} denotes the mantissa of the
object denoted by $\tau$.")

(define-function DENOMINATOR (?x)
   "The term {\tt (denominator $\tau$)} denotes the denominator of the
canonical reduced form of the object denoted by $\tau$.")

(define-function EXP (?x)
   "The term {\tt (exp $\tau$)} denotes $e$ raised to the power the
object denoted by $\tau$."
   :lambda-body (expt the-exponentiation-constant-E ?x))

(define-instance the-exponentiation-constant-E (real-number)
  "The constant often called 'e' using in exponentiation.")

(define-function EXPT (?x ?power)
   "{The term {\tt (expt $\tau_1$ $\tau_2$)} denotes the object denoted by
$\tau_1$ raised to the power the object denoted by $\tau_2$.}")

(define-function FCEILING (?x)
   "The term {\tt (fceiling $\tau$)} denotes the smallest integer (as
a floating point number) greater than the object denoted by $\tau$.")

(define-function FFLOOR (?x)
   "The term {\tt (ffloor $\tau$)} denotes the largest integer
(as a floating point number) less than the object denoted by $\tau$.")

(define-function FLOAT (?x)
   "The term {\tt (float $\tau$)} denotes the floating point number
equal to the object denoted by $\tau$.")

(define-function FLOAT-DIGITS (?x) :-> ?integer
   "The term {\tt (float-digits $\tau$)} denotes the number of digits
used in the representation of a floating point number denoted by
$\tau$."
   :def (nonnegative-integer ?integer))

(define-function FLOAT-PRECISION (?x) :-> ?integer
   "The term {\tt (float-precision $\tau$)} denotes the number of significant digits
in the floating point number denoted by $\tau$."
   :def (nonnegative-integer ?integer))

(define-function FLOAT-RADIX (?x) :-> ?n
   "The term {\tt (float-radix $\tau$)} denotes the radix of the 
floating point number denoted by $\tau$. The most common values are 2
and 16."
   :def (natural ?n))

(define-function FLOAT-SIGN (?x)
   "The term {\tt (float-sign $\tau_1$ $\tau_2$)} denotes a floating-point
number with the same sign as the object denoted by $\tau_1$ and
the same absolute value as the object denoted by $\tau_2$.")

(define-function FLOOR (?x) :-> ?integer
   "The term {\tt (floor $\tau$)} denotes the largest integer less
than the object denoted by $\tau$."
   :def (integer ?integer))

(define-function FROUND (?x)
   "The term {\tt (fround $\tau$)} is equivalent to {\tt (ffloor (+ 0.5 $\tau$))}."
   :lambda-body (ffloor (+ 0.5 ?x)))

(define-function FTRUNCATE (?x)
   "The term {\tt (ftruncate $\tau$)} denotes the largest integer (as
a floating point number) less than the object denoted by $\tau$.")

(define-function GCD (?x)
   "The term {\tt (gcd $\tau_1 \ldots \tau_n$)} denotes the greatest
common divisor of the objects denoted by $\tau_1$ through $\tau_n$.")

(define-function IMAGPART (?x)
   "The term {\tt (imagpart $\tau$)} denotes the imaginary part of the
object denoted by $\tau$.")

(define-function INTEGER-DECODE-FLOAT (?x) :-> ?integer
   "The term {\tt (integer-decode-float $\tau$)} denotes the significand
of the object denoted by $\tau$."
   :def (integer ?integer))

(define-function INTEGER-LENGTH (?x) :-> ?integer
   "The term {\tt (integer-length $\tau$)} denotes the number of bits
required to store the absolute magnitude of the object denoted by
$\tau$."
   :def (nonnegative-integer ?integer))

(define-function ISQRT (?x) :-> ?integer
   "The term {\tt (isqrt $\tau$)} denotes the integer square root of the
object denoted by $\tau$."
   :def (nonnegative-integer ?integer))

(define-function LCM (@args)
   "The term {\tt (lcm $\tau_1 \ldots \tau_n$)} denotes the least common
multiple of the objects denoted by $\tau_1,\ldots,\tau_n$.")

(define-function LOG (?number ?base)
   "The term {\tt (log $\tau_1$ $\tau_2$)} denotes the logarithm of the
object denoted by $\tau_1$ in the base denoted by $\tau_2$.")

(define-function LOGAND (@args)
   "The term {\tt (logand $\tau_1 \ldots \tau_n$)} denotes the bit-wise
logical and of the objects denoted by $\tau_1$ through $\tau_n$.")

(define-function LOGANDC1 (?x ?y)
   "The term {\tt (logandc1 $\tau_1$ $\tau_2$)} is equivalent to
{\tt (logand (lognot $\tau_1$) $\tau_2$)}."
   :lambda-body (logand (lognot ?x) ?y))

(define-function LOGANDC2 (?x ?y)
   "The term {\tt (logandc2 $\tau_1$ $\tau_2$)} is equivalent to
{\tt (logand $\tau_1$ (lognot $\tau_2$))}."
   :lambda-body (logand ?x (lognot ?y)))

(define-function LOGCOUNT (?x)
   "The term {\tt (logcount $\tau$)} denotes the number of {\it on}
bits in the object denoted by $\tau$.  If the denotation of $\tau$ is
positive, then the one bits are counted; otherwise, the zero bits in
the twos-complement representation are counted.")

(define-function LOGEQV (@args)
   "The term {\tt (logeqv $\tau_1 \ldots \tau_n$)} denotes the
logical-exclusive-or of the objects denoted by
$\tau_1,\ldots,\tau_n$.")

(define-function LOGIOR (@args)
   "The term {\tt (logior $\tau_1 \ldots \tau_n$)} denotes the
bit-wise logical inclusive or of the objects denoted by $\tau_1$
through $\tau_n$.  It denotes 0 if there are no arguments.")

(define-function LOGNAND (?x ?y)
   "The term {\tt (lognand $\tau_1$ $\tau_2$)} is equivalent to
{\tt (lognot (logand $\tau_1$ $\tau_2$))}."
   :lambda-body (lognot (logand ?x ?y)))

(define-function LOGNOR (?x ?y)
   "The term {\tt (lognor $\tau_1$ $\tau_2$)} is equivalent to 
{\tt (lognot (logior $\tau_1$ $\tau_2$))}."
   :lambda-body (lognot (logior ?x ?y)))

(define-function LOGNOT (?x)
   "The term {\tt (lognot $\tau$)} denotes the bit-wise logical not of
the object denoted by $\tau$.")

(define-function LOGORC1 (?x ?y)
   "The term {\tt (logorc1 $\tau_1$ $\tau_2$)} is equivalent to
{\tt (logior (lognot $\tau_1$) $\tau_2$)}."
   :lambda-body (logior (lognot ?x) ?y))

(define-function LOGORC2 (?x ?y)
   "The term {\tt (logorc2 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logior
$\tau_1$ (lognot $\tau_2$))}."
   :lambda-body (logior ?x (lognot ?y)))

(define-function LOGXOR (@args)
   "The term {\tt (logxor $\tau_1 \ldots \tau_n$)} denotes the
bit-wise logical exclusive or of the objects denoted by $\tau_1$
through $\tau_n$.  It denotes 0 if there are no arguments.")

(define-function MAX (@args)
   "The term {\tt (max $\tau_1 \ldots \tau_k$)} denotes the largest object
denoted by $\tau_1$ through $\tau_n$.")

(define-function MIN (@args)
   "The term {\tt (min $\tau_1 \ldots \tau_k$)} denotes the smallest
object denoted by $\tau_1$ through $\tau_n$.")

(define-function MOD (?x ?y)
   "The term {\tt (mod $\tau_1$ $\tau_2$)} denotes the root of the object
denoted by $\tau_1$ modulo the object denoted by $\tau_2$.
The result will have the same sign as denoted by $\tau_1$.")

(define-function NUMERATOR (?x)
   "The term {\tt (numerator $\tau$)} denotes the numerator of the
canonical reduced form of the object denoted by $\tau$.")

(define-function PHASE (?x)
   "The term {\tt (phase $\tau$)} denotes the angle part of the polar
representation of the object denoted by $\tau$ (in radians).")

(define-function RATIONALIZE (?x)
   "The term {\tt (rationalize $\tau$)} denotes the rational
representation of the object denoted by $\tau$.")

(define-function REALPART (?x)
   "The term {\tt (realpart $\tau$)} denotes the real part of the
object denoted by $\tau$.")

(define-function REM (?number ?divisor)
   "The term {\tt (rem <number> <divisor>)} denotes the remainder of
the object denoted by {\tt <number>} divided by the object denoted by
{\tt <divisor>}.  The result has the same sign as the object denoted
by {\tt <divisor>}.")

(define-function ROUND (?x) :-> ?integer
   "The term {\tt (round $\tau$)} denotes the integer nearest to the
object denoted by $\tau$.  If the object denoted by $\tau$ is halfway
between two integers (for example 3.5), it denotes the nearest integer
divisible by 2."
   :def (integer ?integer))

(define-function SCALE-FLOAT (?x ?y)
   "The term {\tt (scale-float $\tau_1$ $\tau_2$)} denotes a floating-point
number that is the representational radix of the object denoted by
$\tau_1$ raised to the integer  denoted by $\tau_2$.")

(define-function SIGNUM (?x)
   "The term {\tt (signum $\tau$)} denotes the sign of the object
denoted by $\tau$.  This is one of -1, 1, or 0 for rational numbers
and one of -1.0, 1.0, or 0.0 for floating point numbers.")

(define-function SIN (?x)
   "The term {\tt (sin $\tau$)} denotes the sine of the object denoted
by $\tau$ (in radians).")

(define-function SINH (?x)
   "The term {\tt (sinh $\tau$)} denotes the hyperbolic sine of the object
denoted by $\tau$ (in radians).")

(define-function SQRT (?x)
   "The term {\tt (sqrt $\tau$)} denotes the principal square root of the
object denoted by $\tau$.")

(define-function TAN (?x)
   "The term {\tt (tan $\tau$)} denotes the tangent of the object denoted
by $\tau$ (in radians).")

(define-function TANH (?x)
   "The term {\tt (tanh $\tau$)} denotes the hyperbolic tangent of the
object denoted by $\tau$ (in radians).")

(define-function TRUNCATE (?x)
   "The term {\tt (truncate $\tau$)} denotes the largest integer less
than the object denoted by $\tau$.")


;;;--- Arithetic relations ----

(define-relation < (?x ?y)
   "The sentence {\tt (< $\tau_1$ $\tau_2$)} is true if and only if
the number denoted by $\tau_1$ is less than the number denoted by
$\tau_2$.")

(define-relation > (?x ?y)
  :iff-def (< ?y ?x))

(define-relation =< (?x ?y)
  :iff-def (or (= ?x ?y) (< ?x ?y)))

(define-relation >= (?x ?y)
  :iff-def (or (> ?x ?y) (= ?x ?y)))