natnum.ax.txt - natural numbers (0,1,2,...) and their basic functions
uses form.ax
----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8

 (zero _zero) - natural number zero value
 (succ _n _n+1) - successor function on natural numbers
   - We try to hide the natural number representation from other axioms!
 (natnum _num) - set of natural numbers in successor notation
   - representation of 0,1,2,...: (`z), (`s `z), (`s `s `z), ...
   (We use `z instead of `0 to make distinct from bit-atom `0.)
 (num _num) - synonym of natnum - for now all numbers are natural numbers
   - later, we will also have signed integers and rational numbers
 (plus _n1 _n2 _sum) - sum of natural numbers
 (times   "   _prod) - product of natural numbers
 (len _seq _len) - length of a sequence as a natural number
 (iota0n _n (0..n)) - sequence of natural numbers from 0 thru n (APL name)
 (iota0n- _n (0..n-1)) - map n to nat num seq 0..n-1
 (iota1n _n (1..n))    - map n to      "      1..n
 (ord _fset _elem _k) - ordinal number of an elem of a named finite set

--- comparison of natural numbers and their use
 (=n %1 %2) - equal natural numbers
 (<n %1 %2) - ordered natural numbers
 <=n, >n, >=n, /=n - other relational operators
 (div&mod _n _d _q _m) - quotient & modulo (remainder) of nat num division

--- sequence indexing functions where (0..) index is a natural number:
    (compare with (...#l ...) functions in form.ax, where index is seq len)
 (sel# _i _seq _elem) - select (nat num) ith (0..) element from sequence
 (pre# _i _seq _pre) - get seq prefix ending before [_i]
 (suf# _i _seq _suf) - get seq suffix starting at [_i]
 (rot# _i _seq _rot) - get seq rotation w suffix starting at _i
 (asn# _i _seq _ex _seq') - assign expr at sequence [_i]
 (ins# _i _seq _ex _seq') - insert element before ith element in sequence
 (find# _ex _seq _i) - find expr index in seq -> [_i] (or undefined) (nondet)

--- tbd:
  - reverse-index functions sel#-, pre#-, ... (see form.ax)

Alternatives for natural number representation:

   1. (`s (`s `0))  - atoms for s, 0
   2. (s (s `0))   - just atom for 0
   3. (s (s 0))    - just symbols
   4. (`s `s `z)   - flat representation with atoms

   Comments:  Using atoms helps distinguish natural numbers from other
       objects.  Option 2 was used in 2006.  But ordinary symbols
       have a clean look about them.  However, natural numbers in
       successor notation is a rather bloated representation, anyway.
       For this file we will use option 4.  (This bloated representation
       is just for internal definition and will not be used for actual
       number specification.)

   A. 0, (s (s 0))   -- nested expressions
   B. (0), (s s s 0)   -- sequence

   Comments:  Case A perhaps looks better for axioms -- no need to use
       string variables.  But case B has numbers that are easier to read.
       For now we will use option B.

   There may be a case for providing functions for all of these option
       combinations.

===== later - tbd =====

intnum.ax - file with signed integer definitions will extend these predicates
  negative integers: (num (`p `z)), (num (`p `p `z)), (num (`p `p `p `z)), ...
    - -1,-2,-3,... - these are added to (num _natnum) valid exprs
  Note that integers which are natural numbers have natural num representation.

ratnum.ax - file with rational number axioms will extend these axioms
  - `z's are added to end of num so that # `z represents integer denominator:
(num (`z)), (num (`s `z), (num (`s `z `z)), (num `p `p `z `z `z) - 0,1,1/2,-2/3
  - Note that ratnum is in lowest terms if number of `s/`p and `z have a GCD=1.
    (Function results will be in lowest terms, but input args may not be.)
  - This representation is a little peculiar and may be changed later!!
  - Note that rational numbers in lowest terms which are integers have
    integers representation.
!\


! zero - natural number zero

  (zero (`z)).

! succ - successor function for natural numbers

  (succ ($n) (`s $n))< (natnum ($n)).

! natnum - set of natural numbers in successor notation

  (natnum %z)<       ! zero is a natural number
    (zero %z).
  (natnum %sn)<     ! successor of n is a natural number,
    (natnum %n),     ! if n is a natural number
    (succ %n %sn).

  ! -- We hide the natural number representation from the other axioms!
  !    Note that natnum and succ are mutually recursive.

! num - synonym of natnum - for now all numbers are natural numbers
! (later we will have signed integers and rational numbers)

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

! plus - addition of natural numbers

  (plus %n %0 %n)<             ! n + 0 = n
    (natnum %n), (zero %0).
  (plus %1 %s2 %s3)<           ! n1 + n2+1 = n3+1
    (plus %1 %2 %3),           ! if n1 + n2 = n3
    (succ %2 %s2), (succ %3 %s3).
    
! times - multiplication of natural numbers

  (times %n %0 %0)<            ! n * 0 = 0
    (natnum %n), (zero %0).
  (times %1 %s2 %3')<          ! n1 * n2+1 = n3'
    (times %1 %2 %3),          !  if n1 * n2 = n3
    (plus %3 %1 %3'),          !  and n3 + n1 = n3'
    (succ %2 %s2).

! len - length of a sequence

  (len () %0)<           ! empty sequence has length zero
    (zero %0).
  (len (% $) (`s $l))<     ! adding element increments length
    (len ($) ($l)).

! iota0n - sequence of natural numbers from 0 thru n (APL function name)

  (iota0n %0 (%0))< (zero %0).
  (iota0n %sn ($0..n %sn))<
    (iota0n %n ($0..n)),
    (succ %n %sn).

! iota0n- - map n to natural numbers sequence 0..n-1

  (iota0n- %0 ())< (zero %0).
  (iota0n- %sn ($0..n-1 %n))<ms
    (iota0n- %n ($0..n-1)),
    (succ %n %sn).

! iota1n - map n to natural number sequence 1..n

  (iota1n %0 ())< (zero %0).
  (iota1n %sn ($1..n %sn))<
    (iota1n %n ($1..n)),
    (succ %n %sn).

! ord - ordinal number of a finite set element

  (ord %fsetname %elem %k)<
    (finite_set %fsetname ($1 %elem $2)),   ! (set elems must be unique)
    (len ($1) %k).
  ! -- _fsetname may not be needed in some cases?


! ===== comparison of natural numbers and their use
! -- also see old relation.txt file?

! =n - equal natural numbers

  (=n % %)< (natnum %).

! <n - ordering of natural numbers

  (<n ($) (`s $))< (natnum ($)).
  (<n ($1) (`s $2))< (<n ($1) ($2)).

! <=n

  (<=n %1 %2)< (one_valid (=n %1 %2) (<n %1 %2)).

! >n

  (>n %2 %1)< (<n %1 %2).

! >=n

  (>=n %2 %1)< (<=n %1 %2).

! /=n - not-equal natural numbers

  (/=n %1 %2)< (one_valid (<n %1 %2) (>n %1 %2)).

! div&mod -- do division and modulo operation on pure natural numbers
! (div&mod <dividend> <divisor> <quotient> <remainder/modulo>)

  (div&mod %n %d %q %m)<    ! -- n = q * d + m, m < d
    (times %d %q %qd).
    (plus %qd %m %n),
    (<n %m %d).         ! This condition prevents divisor from being zero!


! ===== sequence indexing functions where (0..) index is a natural number:
!     (compare with (...#l ...) functions in form.ax, where index is seq len)

! sel# - select (natural number)-ith (0..) element from sequence
! (sel# _i _seq _elem)

  (sel# %i ($1 % $2) %)<
    (len ($1) %i).
 
! pre# - get sequence prefix ending before [_i]
! (pre# _i _seq _pre)

  (pre# %i ($pre $suf) ($pre))<
    (len ($pre) %i). 
 
! suf# - get sequence suffix starting at [_i]
! (suf# _i _seq _suf)

  (suf# %i ($pre $suf) ($suf))<
    (len ($pre) %i).
  
! rot# - get sequence "rotation" with suffix starting at _i
! (rot# _i _seq _rot)

  (rot# %i ($pre $suf) ($suf $pre))<
    (len ($pre) %i).

! asn# - assign expression at sequence [_i]
! (asn# _i _seq _ex _seq')

  (asn# %i ($1 % $2) %ex ($1 %ex $2))<
    (len ($1) %i).

! ins# - insert expression before ith element in sequence
! (ins# _i _seq _ex _seq')

  (ins# %i ($1 $2) %ex ($1 %ex $2))<
    (len ($1) %i).
 
! find# - find expr in sequence, returning its index
! (find# _ex _seq _i) - nondeterministic if >1 occurrences, no soln if missing

  (find# %ex ($1 %ex $2) %i)<
    (len ($1) %i).2


! ===== reverse-index functions sel#-, pre#-, ... (see form.ax)
! --- tbd ---


!/ ------ tbd:
  
! min_num - minimum number from a (non-empty) natural number sequence
! (min_num <num-seq> <min-num>)

  (min_num %numseq %min)<
    ((/* <=num) %min %numseq),     ! %min <= all elements in sequence
         ! -- This higher-order form asserts the <=num relation between %min
         !    and each element in %numseqx. 
    (in %min %numseq).             ! and %min is in the sequence

! imin_num - get index of minimum natural number in a sequence
! (If min occurs more than once, then index could be any.)
! (imin_num <num-seq> <index-of-min>)

  (imin_num %numseq %i)<
    (select %i %numseq %min),   ! select ith value from sequence
    (min_num %numseq %min).     ! ith value is minimum!


! isort - index sort - return permutation of natural numbers defining order
  -- to be done


! digit - set of decimal digit characters

  (finite_set digit "0123456789").
     ! -- generates (digit <digit>) expressions

! dec_sym - decimal number symbol and its natural number value

  (dec_sym (` (%digit)) %value)<
    (index digit %digit %value).
       ! -> (dec_sym 2 (s (s 0)))   -- single digit symbol

  (dec_sym (` ($digits %digit)) %valuex)<
    (dec_sym (` ($digits)) %value),
    (index digit %digit %n),
    (length (* * * * *  * * * * *) %10),
        ! -- we use this to hide the natural number representation of 10
    (times %value %10 %10val),
    (plus %10val %n %valuex).
       ! -- multi-digit symbol


! sel<n> - select the nth element of sequence from 0, <n> is decimal symbol
! example: (sel1 (sym0 sym1 sym2) sym1)

  ((` ('sel' $n)) ($pre %elem $suf) %elem)<
    (dec_sym (` ($n)) %n),           ! value of decimal symbol
    (length ($pre) %n).

! pre<n> - get the prefix of length n of a sequence, <n> is decimal symbol
! example: (pref

  ((` ('pre' $n)) ($pre $suf) ($pre))<
    (dec_sym (` ($n)) %n),
    (length ($pre) %n).

 ! *** define both sel<n> and pre<n> in same axiom given same conditions:

   (valid ((` ('sel' $n) ($pre %elem $suf) %elem)
          ((` ('pre' $n) ($pre $suf) ($pre)))<
     (dec_sym (` ($n)) %n),        ! value of decimal symbol
     (length ($pre) %n).

!\