Structure GenPolyCanon

signature GenPolyCanon =
sig

include Abbrev
datatype assoc_mode = L | R | L_Cflipped

datatype gci =
         GCI of {dest : term -> term * term,
                 is_literal : term -> bool,
                 assoc_mode : assoc_mode,
                 assoc : thm,
                 symassoc : thm ,
                 comm : thm,
                 l_asscomm : thm ,
                 r_asscomm : thm ,
                 non_coeff : term -> term,
                 merge : term -> thm,
                 postnorm : term -> thm,
                 left_id : thm,
                 right_id : thm ,
                 reducer : term -> thm}

val update_mode : assoc_mode -> gci -> gci
val gencanon : gci -> term -> thm

val derive_l_asscomm : thm -> thm -> thm
val derive_r_asscomm : thm -> thm -> thm

end

(*

   The gci type stores sufficient information about a type and operators over
   it to allow normalisation of "polynomials" over that type, collecting up
   coefficients etc.

   The required fields of the record are
     dest         : pulls apart a term (e.g., x + y  ->  (x,y))
     is_literal   : returns true iff a term is a numeric literal - in L & R
                    modes literals are shunted to the right end of the term.
                    In L_Cflipped they appear on the front.
     assoc_mode   : how the term should be associated when built.
                      L & R are obvious.  L_Cflipped has non-literals
                      left-associated, but possibly prepended by a literal to
                      the left.  This is appropriate for multiplication, e.g.,
                         c((xy)z)
     assoc        : associativity theorem (e.g., |- x + (y + z) = (x + y) + z)
     symassoc     : associativity theorem with equality flipped
     comm         : commutativity theorem (e.g., |- x + y = y + x)
     l_asscomm    : right-commutativity theorem  (letter 'l' indicates that
                    terms are left-associated)
                       (e.g., |- (x + y) + z = (x + z) + y)
     r_asscomm    : left-commutativity theorem (terms are right-associated)
                       (e.g., |- x + (y + z) = y + (x + z))
     non_coeff    : returns the "base" of a term, ignoring the coefficient.
                       (e.g., x  ->  x,  2 * x  ->  x,  ~y  ->  y,  3  ->  1)
     merge        : takes a term of the form t1 op t2, where t1 and t2 have
                    equal base, and merges them into one by summing
                    coefficients.  The result will be subjected to
                    post-normalisation (see below)
     postnorm     : conversion to normalise certain coeff-term pairs.  Must
                    include the analogue of
                             0 * x  ->  |- 0 * x = 0
                    and might reasonably include
                             x ** 1  ->  |- x ** 1 = x
                             ~1 * x  ->  |- ~1 * x = ~x
                              3 * 1  ->  |- 3 * 1 = 3
     left_id      : theorem stating left-identity for the base operator
                        (e.g.,  |- 0 + x = x  and  |- 1 * x = x)
     right_id     : theorem stating right-identity for the base operator
     reducer      : conversion for doing ground arithmetic on coefficients

   To handle literals, get non_coeff to return a base of 1 for them, and then
   handle their merging separately in the merge function.

   [update_mode m g] returns a g' that is identical to g except that
   the assoc_mode field of the record has been updated to have value m.

   [gencanon g t] returns a theorem of the form |- t = t', where t' is a normal
   form.  The polynomial will be right-associated (for backwards compatibility
   reasons).

   [derive_l_asscomm ass comm] derives an l_asscomm theorem from assoc and comm
   theorems.

   [derive_r_asscomm ass comm] derives an r_asscomm theorem from assoc and comm
   theorems.

*)

HOL 4, Kananaskis-14