! ELC13_utilities.txt - Utility Functions for Emerging Languages Camp 2013
!/
  This file gives axioms for various utility functions used in examples
  for the 2013 Emerging Languages Camp presentation on axiomatic language.
  The following utility functions are defined:

    == - identical expressions

    all_valid - all expressions in list are valid
    one_valid - one expression in list is valid

    seq_set - set is sequence of elements of other set

    `number - set of natural numbers
    `plus - addition of natural numbers
    `times - multiplication of natural numbers

    <num - < ordering of natural numbers
    <=num - <=       "

    concat - concatenation of two sequences
    member - expression is member of a sequence
    reverse - reverse of a sequence
    length - natural number length of a sequence
    =length - two sequences of equal length
    permute - permutation of a sequence

    <, <= - ordering of bit atom expressions
    ordered - sequence of bit atom expressions is ordered

    /= - inequality of bit atom expressions
    not_member - expression not member of sequence (of bit atom expressions)

    blanks - sequences of blanks

    bit - set of bits
    bitseq - set of bit sequences

    char - set of characters
    charstr - set of character strings
    file - set of character string sequences

    digit - map decimal digit character to its natural number
    dec>num - map decimal digit character string to its natural number
    num>dec - map natural number to decimal digit string (w/o leading 0s)
    decnum - map decimal digit symbol to its natural number

    `and - "and" operation on `true/`false values
    `or - "or"            "
!\

! == - identical expressions

  (== % %).


! -- Some Higher-Order Forms --

! all_valid - all expressions in list are valid

  (all_valid).
  (all_valid % $)< % , (all_valid $).

! one_valid - one expression in list is valid
! (see /= example below)

  (one_valid $1 % $2)< % .

! seq_set - set is sequence of elements of other set
! (see bit -> bitseq and char -> charstr examples below)

  (%seqset ())< (seq_set %seqset %set).
  (%seqset (% $))< (seq_set %seqset %set), (%set %), (%seqset ($)).


! -- Natural Numbers in Successor Notation and their Addition & Multiplication

! `number - set of natural numbers (in successor notation)

  (`number (`0)).                      ! zero is a natural number
  (`number (`s $n))< (`number ($n)).   ! if n is a nat num, succ(n) is too

! `plus - addition of natural numbers

  (`plus %n (`0) %n)< (`number %n).
  (`plus %1 (`s $2) (`s $3))< (`plus %1 ($2) ($3)).

! `times - multiplication of natural numbers

  (`times %n (`0) (`0))< (`number %n).
  (`times %1 (`s $2) %3')<
    (`times %1 ($2) %3),
    (`plus %1 %3 %3').


! -- Ordering of Natural Numbers --

! <num - < ordering of natural numbers

  (<num ($n) (`s $n))< (`number ($n)).
  (<num %n1 %n3)< (<num %n1 %2), (<num %n2 %n3).

! <=num - <= ordering of natural numbers 

  (<=num %n %n)< (`number %n).
  (<=num %n1 (`s $n2))< (<=num %n1 ($n2)).


! -- Some List Predicates --

! concat - concatenation of two sequences

  (concat ($1) ($2) ($3)).

! member - expression is member of a sequence

  (member % ($1 % $2).

! reverse - reverse of a sequence

  (reverse () ()).
  (reverse (% $) ($rev %))< (reverse ($) ($rev)).

! length - length of a sequence as a natural number

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

! =length - two sequences of equal length

  (=length () ()).
  (=length (%1 $1) (%2 $2))< (=length ($1) ($2)).

! permute - permutation of a sequence

  (permute () ()).
  (permute (% $) ($1 % $2))< (permute ($) ($1 $2)).


! -- Ordering of Bit Atom Expressions --

! < - < order of bit atom expressions

  (< `0 `1).              ! ordering of bits

  (< ($) ($ % $x)).       ! lexicographic ordering of sequences
  (< ($ %1 $1) ($ %2 $2))< (< %1 %2).

! <= - <= order of bit atom expressions

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

! ordered - sequence of bit atom expressions is ordered

  (ordered ()).
  (ordered (%)).
  (ordered (% %1 $))< (ordered (%1 $)), (<= % %1).


! -- Inequality of Bit Atom Expressions
    
! /= - unequal bit atom expressions
! (see one_valid higher-order form above)

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

! not_member - expression not member of sequence (of bit atom expressions)

  (not_member %x ()).
  (not_member %x (% $))< (/= %x %), (not_member %x ($)).


! -- Character Definitions --

! blanks - sequences of blanks

  (blanks ()).
  (blanks (' ' $))< (blanks ($)).

! bit - set of bits

  (bit `0).
  (bit `1).

! bitseq - set of bit sequences
! (see seq_set higher order form above)

  (seq_set bitseq bit).

! char - set of characters

  (char (`char %8bits))< (bitseq %8bits),
      (=length %8bits (* * * *  * * * *)).

! charstr - set of character strings

  (seq_set charstr char).

! file - set of character string sequences

  (seq_set file charstr).


! -- Decimal Number Representation --

! digit - map decimal digit character to its natural number

  (digit %digit %num)<
    (== "0123456789" ($digits1 %digit $digits2)),
    (length ($digits1) %num).

! dec>num - map decimal digit character string to natural number

  (dec>num () (`0)).
  (dec>num ($digits %digit) %num')<
    (dec>num ($digits) %num),
    (`times %num (`s `s `s `s `s  `s `s `s `s `s `0) %10num),
    (digit %digit %dignum),
    (`plus %10num %dignum %num').

! num>dec - map natural number to decimal digit string

  (num>dec (`0) "0").         ! number zero represented by single zero digit
  (num>dec %num (%digit $digits))<
    (dec>num (%digit $digits) %num),
    (< '0' %digit).           ! otherwise, leading digit is non-zero

! decnum - map decimal digit symbol to its natural number

  (decnum (` (%d $d)) %num)< (dec>num (%d $d) %num).


! -- Boolean Operations on `true/`false --

! `and - "and" operation on `true/`false values

  (`and `false `false `false).
  (`and `false `true  `false).
  (`and `true  `false `false).
  (`and `true  `true  `true).

! `or - "or" operation on `true/`false values 

  (`or `false `false `false).
  (`or `false `true  `true).
  (`or `true  `false `true).
  (`or `true  `true  `true).