integer.txt -- integers and their arithmetic
uses: higher.txt

*** Define type specific operations (+n, succn, succi0+, etc.) in
    addition to "overloaded" operations (+, succ, etc.) that are defined
    below?

This file supercedes the natnum.txt file defined earlier.  We represent
integers uniquely by the following expressions:

   ..., (p p z), (p z), (z), (s z), (s s z), ...

Note that an expression such as (p s s p p z) is invalid.  The axioms for
this integer definition are as follows:

   (zero (z)).            ! number zero  (same as in natnum.txt) 

   (succ ($i) (s $i))<    ! successor defined for non-negative integers
     (integer0+ ($i)).

   (integer0+ %0)<        ! definition of non-negative integers
     (zero %0).           ! (same as natural numbers)
   (integer0+ %i+1)<
     (integer0+ %i),
     (succ %i %i+1).

   (pred ($i) (p $i))<    ! predecessor function for non-positive integers
     (integer0- ($i)).

   (integer0- %0)<        ! definition of non-positive integers
     (zero %0).
   (integer0- %i-1)<
     (integer0- %i),
     (pred %i %i-1).

   (integer %)<           ! complete set of integers
     (one_valid
         (integer0- %)
         (integer0+ %)).

   (Valid                 ! generalizing succ and pred to all integers
       (succ %- %+)
       (pred %+ %-))<
     (one_valid
         (succ %- %+)
         (pred %+ %-)).

   ! alternative defn:
   !   (succ %- %+)< (pred %+ %-).
   !   (pred %+ %-)< (succ %- %+).
   !    -- this is probably better

definition of integer addition:

   (+ % %0 %)<
     (zero %0),
     (integer %).
   (+ %1 %2' %3')<
     (+ %1 %2 %3),
     (one_valid
         (*:succ (%2 %3) (%2' %3'))
         (*:pred (%2 %3) (%2' %3'))).

definition of integer subtraction:

   (- %3 %2 %1)<
     (+ %1 %2 %3).

   ! -- not restricted to integers!

a negation operator is as follows:

   (- %i %-i)<
     (- %0 %i %-i),
     (zero %0).

   ! -- not restricted to integers!

an absolute value operator is as follows:

   (abs %i+ %i+)<
     (integer+ %i+).
   (abs %i- %i+)<
     (integer- %i-),
     (- %i- %i+).

definition of integer multiplication:

   (* % %0 %0)< 
     (zero %0),
     (integer %).
   (* %1 %2' %4)<
     (* %1 %2 %3),
     (one_valid
       (valid (succ %2 %2') (+ %3 %1 %4))
       (valid (pred %2 %2') (- %3 %1 %4))).

ordering of integers:

   (< %k %k+1)<
     (integer %k),
     (succ %k %k+1).
   (< %k %l+1)<
     (< %k %l),
     (succ %l %l+1).

   ! *** restrict 2nd axiom to just integers?

   ! *** higher-order definition needed here to define < from succ

! <=, >, >= defined from < in order.txt
! ~= defined from < in notequal.txt
! -- don't really need = ?

signed integer division, remainder, and modulo:

Ada definition:
   n   d  n/d  n rem d  n mod d  
   5   3   1      2        2
  -5   3  -1     -2        1
   5  -3  -1      2       -1
  -5  -3   1     -2       -2

David Goldberg, "Computer Arithmetic", in Hennessy & Patterson, Computer
Architecture, a Quantitative Approach, advocates a "floor division"
operation with a corresponding modulo operation, which is always positive:

   n   d  n fldiv d  n flmod d
   5   3      1          2
  -5   3     -2          1
   5  -3     -1          2
  -5  -3      2          1

x fldiv y = floor(x/y) and
x = (x fkdiv y) * y + x flmod y with 0 <= x flmod y < abs(y)

The definition of div (/), rem, and mod are as follows:

   (div&rem&mod %n %d %q %r %m)<    ! get quotient, remainder, and modulo
     (* %d %q %k),
     (+ %k %r %n),
     (one_valid                     ! the 4 cases are handled separately
       (valid (integer0+ %n) (integer0+ %d)
              (< %r %d) (== %r %m))
       (valid (integer0- %n) (integer0+ %d)
              (- %r %-r) (< %-r %d) (+ %d %r %m))
       (valid (integer0+ %n) (integer0- %d)
              (- %d %-d) (< %r %-d) (+ %d %r %m))
       (valid (integer0- %n) (integer0- %d)
              (< %d %r) (== %r %m)))

   ! -- need to come up with a simpler definition

   (div %n %d %q)< (div&rem&mod %n %d %q %r %m).
   (rem %n %d %r)< (div&rem&mod %n %d %q %r %m).
   (mod %n %d %m)< (div&rem&mod %n %d %q %r %m).

The "floor division" and "floor modulo" operations are defined as follows:

   (fldiv&flmod %n %d %q %m)<    ! get floor division and floor modulo
     (* %d %q %k),
     (+ %k %m %n),
     (abs %d %absd),
     (< %m %absd).

   (fldiv %n %d %q)< (fldiv&flmod %n %d %q %m).
   (flmod %n %d %m)< (fldiv&flmod %n %d %q %m).