order.txt -- definition of ordering and related utilities
(The axioms in this file need further refinement.)
uses:
   basicc -- conditional basic predicates
   higher -- higher-order definitions
   hosym -- higher-order definitions using symbol representation
   ... other axiom sets that define < relation and "value" predicate

The following functions are defined:
!   seqval  -- sequence of 0 or more values  (aggregate values)
!   value  -- additional definition as a sequence of >=1 values
!   <=  -- ordering relation defined from <, value
!   /=  -- inequality relation defined from < 
!   <seq  -- lexicographic ordering relation between sequences of values 
!   <  -- additional definition between sequences of >=1 values 

generalizing the "value" predicate:

   (generalize_cond1 value).

seqval -- sequence of zero or more values

   (Pred_defn seqval (map value)).

   ! This is somewhat unnecessary given that value has been generalized
   ! and that we can also "map" the value predicate.

A sequence of >=0 values is considered an aggregate value:
(nested sequences are also defined)

   (value %)<
     (seqval %).

ordering of atoms in an atom set:  (move to file <atom.txt>?)

   (< %atom1 %atom2)<
     (atom_set %set ($1 %atom1 $2 %atom2 $3)).

   ! Note that atoms in an atom set automatically have an ordering relation
   ! defined between them, but individually defined atoms have no inherent
   ! ordering.

an atom from an atom set is considered a value:

   (value %atom)<
     (atom_set %set ($1 %atom $2)).

   ! Individually defined atoms are not automatically considered values.

a character is a value:   (move to file <char.txt?>?)

   (value %char)<
     (char %char).

<seq  -- ordering among sequences of values:
(-- needed as a separate predicate?)

   (<seq (%1 $1) (%2 $2))<
     (< %1 %2),
     (seqval ($1)),     ! -- perhaps ignore rest of elements, if 1st ordered?
     (seqval ($2)).

   (<seq (% $1) (% $2))<
     (value %),
     (<seq ($1) ($2)).

   (<seq () (% $))<
     (seqval (% $)).

<  -- generalizing < to sequences of values:

   (< %1 %2)<
     (<seq %1 %2).

ordering of characters based on bit sequence ordering:

   (< (%char_atom %bitseq1) (%char_atom %bitseq2))<
     (char (%char_atom %bitseq1)),
     (char (%char_atom %bitseq2)),
     (< %bitseq1 %bitseq2).

<=  -- generic <= ordering relation

   (<= %1 %2),
     (< %1 %2);
   (<= % %),
     (value %);
        ! The equality case is only defined for actual data values,
        ! not arbitrary expressions!

~=  -- generic inequality relation
(this deals with "values", ~== deals with arbitrary expressions)

   (~= %1 %2),
     (< %1 %2);
   (~= %1 %2),
     (< %2 %1);

? =  -- equality of values
? (this is defined just for values, == is for arbitrary expressions)

   (= % %)<
     (value %).

>  and  >=

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

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

an ordered sequence of values:

   (ordered ()).
   (ordered (%))<
     (value %).
   (ordered ($ % %x)<
     (ordered ($ %)),
     (<= % %x).

   ! *** This is actually a folded generalization of the binary relation <=.

   ! -- Do we need to enforce the <= relation between each pair of elements
   !    in the sequence?  And/or do we need to enforce that the sequence
   !    values are all of the same "type"?

generic sorting definition:

   (sort %1 %2)<
     (permutation %1 %2),
     (ordered %2).



*** Obsolete -- from old notes ***

! Efficient sort definition:

! split a sorted sequence into elements < and >= a value:
! (we remove prefix of elements that are <)

   (split_sortseq %seq %val %seq1 %seq2),       ! keep %seq1 reversed?
     (split_sortseq$ %seq %val () %seq1$ %seq2),
     (rev %seq1$ %seq1);

   (split_sortseq$ (%0 $0) % ($1) %1 %2),
     (< %0 %),
     (split_sortseq$ ($0) % (%0 $1) %1 %2);

   (split_sortseq$ (%0 $0) % %1 %1 (%0 $0)),    ! efficiency of var ref???
     (<= % %0);                                 ! must avoid self-ref check

   (split_sortseq$ () % %1 %1 ());

! inserting a value into a sorted sequence:

   (insert_in_sortseq % %seq %seq'),
     (split_sortseq %seq % %seq1 ($seq2)),
     (concat %seq1 (% $seq2) %seq');

! sorting a sequence of values:
! (this is an O(n^2) sort)

   (sort2 %seq %seq'),
     (sort2$ %seq () %seq');

   (sort2$ (% $) %sorted %seq'),
     (insert_in_sortseq % %sorted %sorted'),
     (sort2$ ($) %sorted' %seq');

   (sort2$ () %sorted %sorted);

! O(nlogn) sort using a merge-sort algorithm:
! (this sort should be stable)

   (sort (%1 %2 $) %seq'),
     (divide_seq (%1 %2 $) %1st_half %2nd_half),
     (sort %1st_half %seq1'),
     (sort %2nd_half %seq2'),
     (merge %seq1' %seq2' %seq');
   (sort () ());
   (sort (%) (%));
  !  (value %);      -- can't use this if sorting (<key> <record>) 

! merge  -- merge sorted sequences

   (merge %seq1 %seq2 %seq),
     (merge$ %seq1 %seq2 () %seqr),
     (rev %seqr %seq);

   (merge$ (%1 $1) (%2 $2) ($) %seqr),
     (<= %1 %2),
     (merge$ ($1) (%2 $2) (%1 $) %seqr);
   (merge$ (%1 $1) (%2 $2) ($) %seqr),
     (< %2 %1),
     (merge$ (%1 $1) ($2) (%2 $) %seqr);
   (merge$ (%1 $1) () ($) %seqr),
     (merge$ ($1) () (%1 $) %seqr);
   (merge$ () (%2 $2) ($) %seqr),
     (merge$ () ($2) (%2 $) %seqr);
   (merge$ () () %seqr %seqr);

! verify_range -- verify range of numbers inside a sequence  (0..n-1)

   (verify_range %n ());
   (verify_range %n (%k $k)),
     (>=0 %k),
     (< %k %n),
     (verify_range %n ($k));