! natnum.ax - utility functions & relations involving natural numbers
! We also give alternative definitions (>>>) and issues to resolve (???).
! uses: ho.ax, form.ax
  

! number - set of natural numbers

  (number 0).           ! zero is a natural number
  (number (s %n))<      ! the successor of %n is a natural number,
    (number %n).        !   if %n is a natural number

! plus - addition of natural numbers

  (plus 0 %n %n)< (number %n).    ! 0 + n = n
  (plus (s %1) %2 (s %3))<        ! if %1 + %2 = %3 then 1+%1 + %2 = 1+%3
    (plus  %1  %2    %3).

! times - multiplication of natural numbers

  (times 0 %n 0)< (number %n).     ! 0 * n = 0
  (times (s %1) %2 %3)<            ! if %1 * %2 = %x and %x + %2 = %3,
    (times %1 %2 %x),              !   then 1+%1 * %2 = %3
    (plus %x %2 %3).

! <num - ordering relation on natural numbers  (<nat ???)
! (We use <num instead of just < so that operation will be type-specific.) 

  (<num 0 (s 0)).
  (<num (s %1) (s %2))< (<num %1 %2).
  (<num %1 (s %2))< (<num %1 %2).

 !>>> 1st & 2nd axioms could be replaced with:

    (<num %n (s %n))< (number %n).

 !>>> 2nd and 3rd axioms could be combined:

    (valid (<num (s %1) (s %2)) (<num %1 (s %2)))< (<num %1 %2).

! <=num - <= on natural numbers

  (<=num %n %n)< (number %n).
  (<=num %1 %2)< (<num %1 %2).

 !>>> alternate defn:

    (<=num 0 0).
    (<=num (s %1) (s %2))< (<=num %1 %2).
    (<=num %1 (s %2))< (<=num %1 %2).

! 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
  

!==============================================================================

! Form functions involving counting using natural numbers

! length - length of a sequence
! (length <seq> <len>)

  (length () 0).
  (length (% $) (s %n))< (length ($) %n).

! select - select <ith> element from sequence (indexed from 0)
! (select <i> <seq> <ith-elem>)     ! ??? order of args?
! -- valid expressions are only generated for i in 0..<seq-len>-1

  (select 0 (%h $) %h).         ! head element has index 0
  (select (s %i) (% $) %e)<     ! selecting i+1-th element
    (select %i ($) %e).

 !>>> nicer defn?:

   (select %i ($pre %e $suf) %e)<    ! ith-elem occurs after length-i prefix
     (length ($pre) %i).

! prefix - select prefix of length <n> from sequence
! (prefix <n> <seq> <len-<n>-prefix>)
! -- valid expressions are only genereted for <n> in 0..<seq-len>

  (prefix %n ($pre $suf) ($pre))<
    (length ($pre) %n).

 !>>> could combine select and prefix into single axiom:

   (valid (select %n ($pre %e $suf) %e)
          (prefix %n ($pre $suf) ($pre)))<
     (length ($pre) %n).

! index - associate a finite set element with a natural number index

  (index %set %elem %index)<
    (finite_set %set ($1 %elem $2)),
    (length ($1) %index).

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



!