Structure AC_Sort

signature AC_Sort =
sig

  include Abbrev
  val sort : {assoc : thm, comm : thm,
              dest : term -> term * term, mk : term * term -> term,
              cmp : term * term -> order,
              combine : conv, preprocess : conv} -> conv

end

(*

  [sort {assoc,comm,dest,mk,cmp,combine,preprocess}] is a conversion for
  sorting terms with respect to an associative and commutative operator.
  It uses a merge sort internally, so should be reasonably efficient.

  The record's fields are:

    assoc:      associativity theorem in standard r-to-l format:
                 a + (b + c) = (a + b) + c
                can be universally quantified

    comm:       commutativity theorem (can be universally quantified)

    dest:       destructor function for operator

    mk:         constructor function for operator

    cmp:        comparison function for performing sort.  Terms identified
                as EQUAL will be combined by combine conversion.

    combine:    conv taking terms of the form (t1 op t2) where t1 and t2
                have compared as equal.  Should always succeed (can be
                ALL_CONV).

    preprocess: applied to all leaf terms as term is first examined.
                If it fails or raises UNCHANGED (i.e., both ALL_CONV and
                NO_CONV are OK here), nothing further is done.  If it
                succeeds, further processing is performed on the resulting
                term

   E.g., combine can combine numeric literals; preprocess could convert
   a - b into a + -b, or -x into -1 * x, or ~~p into p.

*)

HOL 4, Kananaskis-10