! 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). ! >> 1st & 2nd axioms could be replaced with: (>> 2nd and 3rd axioms could be combined: (valid (>> 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 ) (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 ) (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 ) (length () 0). (length (% \$) (s %n))< (length (\$) %n). ! select - select element from sequence (indexed from 0) ! (select ) ! ??? order of args? ! -- valid expressions are only generated for i in 0..-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 from sequence ! (prefix -prefix>) ! -- valid expressions are only genereted for in 0.. (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 ) 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 - select the nth element of sequence from 0, 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 - get the prefix of length n of a sequence, is decimal symbol ! example: (pref ((` ('pre' \$n)) (\$pre \$suf) (\$pre))< (dec_sym (` (\$n)) %n), (length (\$pre) %n). ! *** define both sel and pre 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). !