! natnum.ax.txt - natural numbers (0,1,2,...) and their basic functions
! uses form.ax, ho.ax
!/

--- basic natural number functions
 (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 add signed integers and rational numbers
 (plus _n0 _n1 _sum) - sum of natural numbers
 (times   "   _prod) - product of natural numbers
 (len _seq _len) - length of a sequence as a natural number
 (ix0n _n (0..n)) - index generator of natural num seq (0 .. n)
 (ix0n- _n (0..n-1)) -      "          nat num seq 0..n-1
 (ix1n _n (1..n))    -      "                 "    1..n
x (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 nat num operators
 (div _n _d _q) - division of two natural numbers yielding quotient
 (mod _n _d _r) - modulo (remainder) of natural number division
 (div&mod _n _d _q _m) - quotient & modulo (remainder) of nat num division

--- sequence (0..) indexing functions where 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
      - can use sel# to "find" _elem in _seq!
 (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 [i..]
 (ins# _i _ex _seq _ex _seq') - insert expr before element [i] in sequence
      - can use ins# to remove element [i] from sequence
 (asn# _i _ex _seq _seq') - assign (replace) expr at [i] in sequence
-- string functions:
 (asnpre# _i _str _seq _seq') -assign (repl) prefix before [i] w str
 (asnsuf# _i _str _seq _seq') - assign (repl) suffix from [i] w str
 (selstr# _i _len _seq _str) - select str w len starting with [i]
     - can use selstr# to "find" str in seq! 
 (rmvstr# _i _len _seq _seq') - remove _len-string starting w seq[i]
 (insstr# _i _str _seq _seq') - insert string before seq[i]
 (asnstr# _i _str _seq _seq') - assign (repl) str starting at [i] (must fit)
tbd:   -- asnstr#|, asnstr#_ - analogous to asnpre|, asnpre#_

--- 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.  But ordinary symbols have a clean look about them.
       For this file we use option 4.  (This bloated representation
       is just for their axiomatic language definition.  See char.ax for
       a more readable decimal number representation.)

   A. 0, (s (s 0))   -- nested expressions vs.
   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 use option B, but with atoms and `z for zero.

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

===== later =====

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 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
    integer representation.
!\


----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8


! ======= natural numbers and some basic functions

! 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)

  (def num natnum).

! plus - addition of 2 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).

!/ later:
   plus_ - add >=0 nat nums in a list
   plus* - add        "          sequence
!\

! times - multiplication of 2 natural numbers

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

! later:  times_  times*

! len - length of a sequence

  (len () %0)<           ! empty sequence has zero length
    (zero %0).
  (len (% $) %sl)<       ! adding element increments length
    (len ($) %l),
    (succ %l %sl).

! (ix0n _n (0..n)) -  index generator of natural number seq (0..n)
! (alt: idx0n, iota0n - APL function name)

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

! (ix0n- _n (0..n-1)) - index generator: map n to nat num seq 0..n-1 (?

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

! (ix1n _n (1..n)) - index generator: map n to nat num seq 1..n

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

!/ later:
! ord - ordinal number (0..n-1) of a finite set element

  (ord %fsetname %elem %k)<
    (finite_set %fsetname ($1 %elem $2)),   ! finite set has been defined
                                            ! (its elem names must be unique)
    (len ($1) %k).
  ! -- _fsetname may not be needed in some cases
  !    where element names are only used for one set
!\


! ======= comparison of natural numbers and their use

! =n - equal natural numbers

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

! <n - ordering of natural numbers

  (<n %n %sn)< (natnum %n).
  (<n %n0 %sn1)< (<n %n0 %n1), (succ %n1 %sn1).

! <=n

  (<=n %n0 %n1)< (val1 (=n %n0 %n1) (<n %n0 %n1)).

! >n

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

! >=n

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

!/ tbd:
  (def >n @r<n).     ! reverse args of <n relation!

  (def >=n @r<=n).    ! rev args of <=n

! a possible h-o form:
  ((@r %pred) $rargs)<
    (%pred $args),
    (rev ($args) ($rargs)).

! in char.ax add
  (hopre @r).
!\       

! <>n - not-equal natural numbers (Pascal inequality operator here!)
! (alt: ~=n)

  (<>n %n0 %n1)< (val1 (<n %n0 %n1) (>n %n0 %n1)).

! div - division of natural numbers
! mod - modulo operation on natural numbers
! div&mod -- division & modulo operation on natural numbers
! (div&mod <dividend> <divisor> <quotient> <remainder/modulo>)
! *** Should I call it "remainder" instead of "modulo"???

  (val (div %n %d %q)
       (mod %n %d %m)
    (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 (0..) indexing functions where index is a natural number =====
!    (compare with (..#l ...) functions in form.ax, where index is seq len)

 (axs      ! use shared condition for compact definition!
  ((sel# %i ($pr %x $sf) %x))        ! select ith (0..) expr from seq
      ! Setting seq and x to solve for i, "finds" the(a) position of x in seq,
      ! if it exists.
  ((pre# %i ($pr $sf) ($pr)))        ! get seq prefix ending before [i]
  ((suf# %i ($pr $sf) ($sf)))        ! get seq suffix starting with [i]
  ((rot# %i ($pr $sf) ($sf $pr)))    ! dot seq rotation w suffix [i..]
  ((ins# %i %x ($pr $sf) ($pr %x $sf)))    ! insert x before suffix [i..]
      ! - can use ins# to remove expr at seq[i]
  ((asn# %i %x ($pr %z $sf) ($pr %x $sf)))   ! assign (replace) expr [i]
! - string functions:
  ((asnpre# %i ($str) ($pr $sf) ($str $sf)))   ! assign prefix before [i]
  ((asnsuf# %i ($str) ($pr $sf) ($pr $str)))   ! assign suffix [i..]
  ((selstr# %i %l ($pr $str $sf) ($str)))      ! select string [i..i+l-1]
      ! - can use selstr# to "find" str in seq
  ((rmvstr# %i %l ($pr $str $sf) ($pr $sf)))   ! remove       "
  ((insstr# %i ($str) ($pr $sf) ($pr $str $sf)))  ! insert string before [i]
  ((asnstr# %i ($str) ($pr $old $sf) ($pr $str $sf))) !asn str [i..] (must fit)
!    - no valid expr generated if _i + str len > seq len
!    - tbd:  asnstr#|, asnstr#_ - analogous to asnpre|, asnpre#_
 )<  ! shared conditions:
  (len ($pr) %i),    ! index i (0..) is length of seq prefix; suffix at [i..]
  (len ($str) %l),   ! l is nat num length of ($str) (string of interest)
  (=l ($old) ($str)).  ! asnstr# replaces old string w new one of same length


!/ tbd:

! (asnstr#| _i _str _seq _seq') - assign (repl) string at [_i]
! - if _i + str len > seq len, str truncated as needed

  (asnstr#| %i %str %seq %seq')<   ! _i + str len <= seq len
    (asnstr# %i %str %seq %seq').  ! - same as asnstr#
  (asnstr#| %i ($str0 $str1) ($pre $oldstr) ($pre $str0))<
    (len ($pre) %i),
    (=l ($str0) ($oldstr)).  ! if _i + str len >=l seq len, truncate str

! (asnstr#_ _pos _str _seq _seq') - assign (repl) string at [_pos]
! - if _i + str len > seq len, seq is extended to hold it

  (asnstr#_ %i %str %seq %seq')<   ! _i + str len <= seq len
    (asnstr# %i %str %seq %seq').  ! - same as asnstr#
  (asnstr#_ %i ($str0 $str1) ($pre $oldstr) ($pre $str0 $str1))<
    (len ($pre) %i),
    (=l ($str0) ($oldstr)).  ! _i + str len >=l seq len,  extend sequence
!\

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


!/ OLD ...  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

! **** covered by  char.ax  !!

! 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).

!\ ... OLD