natnum.txt -- definition of natural numbers and their arithmetic
uses: higher.txt

This file defines natural number arithmetic.  The intent is that the
representation of natural numbers will be hidden and other axioms will
not need to know about it.

utilities defined:
!  zero -- number zero
!  succ -- successor function (for natural numbers)
!  natnum -- set of natural numbers
!  natnum_seq -- vector of sequential of natural numbers from 0 to n-1
!  +, -, * -- addition, subtraction, multiplication for natural numbers
!  <  -- ordering relation on natural numbers
!  div/mod, div, mod -- division/modulo operations on natural numbers


definition of set of natural numbers:

   (zero (z)).           ! definition of number zero

   (succ ($n) (s $n))<   ! definition of successor function
     (natnum ($n)).
       ! the successor function will be expanded later to other types

   (natnum %0)<
     (zero %0).
   (natnum %n+1)<
     (natnum %n),
     (succ %n %n+1).

Note that the defined representation for natural numbers is
   (z), (s z), (s s z), ...,
but this is "hidden" from all higher-level functions.
Signed integer and rational numbers will use this representation for
non-negative integer numbers.

*** a natural number is a value (see <eval.txt>):

   (value %num)<
     (natnum %num).

generate vector of sequential natural numbers:
!  (natnum_seq <n> (<0> ... <n-1>))     -- returns sequence 0..n-1 given n

   (natnum_seq %0 ())<
     (zero %0).
   (natnum_seq %n+1 ($0..n-1 %n))<
     (natnum_seq %n ($0..n-1)),
     (succ %n %n+1).

   ! -- or could call it "iota" from APL!

definition of natural number addition:

   (+ %0 %n %n)<
     (zero %0),
     (natnum %n).
   (+ %k+1 %n %j+1)<
     (+ %k %n %j),
     (succ %k %k+1),
     (succ %j %j+1).

Some comments:
Do we need to limit args to natural numbers?
  (Both + and succ will eventually get generalized.)
Do we need succn and +n operations defined first and then define succ and +
  from them?
Will the + input arguments eventually be generalized to accept arbitrary
  expressions that evaluate to a number?  -- Probably not.  It is nice to
  have pure relations on pure numbers.  The "eval" function will allow
  evaluating these pure predicates as nested functions with expression
  arguments.

Note that we prefer concise symbols + and * here instead of predicate names
such as "plus" and "times".

definition of natural number multiplication:

   (* %0 %n %0)<
     (zero %0),
     (natnum %n).
   (* %k+1 %n %m)<
     (* %k %n %l),
     (succ %k %k+1),
     (+ %l %n %m).

   ! -- restrict type here, too?

definition of natural number subtraction:

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

   ! -- this will apply to integers, rationals, etc. as well
   ! -- no need to define a "pred" function or have a recursive - definition

ordering of natural numbers:

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

     ! *** this second axiom may apply to non-natural numbers
     !     -- problem here?

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

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

ordering with respect to zero:

   (>0 %n)<
     (zero %0),
     (< %0 %n).

division of natural numbers giving a quotient and remainder:

   (div&mod %n %d %q %r)<
     (*:natnum (%n %d %q)),  ! this definition only applies to natural numbers
     (* %d %q %k),
     (+ %k %r %n),
     (< %r %d).

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

! Have type specific operations?:
!   +n, +i   -- natural number and integer addition
!   <n, <i, succn, succi    (these enforce type while doing operation)