# Structure Normalizer

Source File Identifier index Theory binding index

```(* ========================================================================= *)
(* Relatively efficient HOL conversions for canonical polynomial form.       *)
(*   (HOL-Light's normalizer.ml)                                             *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

signature Normalizer =
sig
include Abbrev

(* Usage: SEMIRING_NORMALIZERS_CONV sth rth
(is_semiring_constant,
variable_order

- "sth" is a theorem as axioms of a semiring system of the following form:

(!x. add r0 x = x) /\
(!x y z. mul x (mul y z) = mul (mul x y) z) /\
(!x y. mul x y = mul y x) /\
(!x. mul r1 x = x) /\
(!x. mul r0 x = r0) /\
(!x y z. mul x (add y z) = add (mul x y) (mul x z)) /\
(!x. pwr x 0 = r1) /\
(!x n. pwr x (SUC n) = mul x (pwr x n))

- "rth" is a theorem as additional axioms of negation and subtraction of
the following form:

|- (!x:'a. neg x = (neg r1) * x) /\
(!x y. sub x y = add x ((neg r1) mul y))

- is_semiring_constant tests if a term is a literal numeral. For :num, it can
be numSyntax.is_numeral

(NOTE: is_semiring_constant (neg r1) is expected to return true when "rth"
is provided.)

- variable_order can be (Term.compare (x,y) = LESS) in HOL4.

- SEMIRING_ADD_CONV, SEMIRING_MUL_CONV and SEMIRING_POW_CONV are conversions
that simplifies ‘add’, ‘mul’ and ‘pow’ of literal numerals (one-step). For
:num, they can be ADD_CONV, MULT_CONV and EXP_CONV of reduceLib (or Arithconv).

SEMIRING_NORMALIZERS_CONV returns 6 conversions correspoding to the following
simplification tasks: (the last one subsumes the other five.)

POLYNOMIAL_NEG_CONV,
POLYNOMIAL_SUB_CONV,
POLYNOMIAL_MUL_CONV,
POLYNOMIAL_POW_CONV,
POLYNOMIAL_CONV
*)
val SEMIRING_NORMALIZERS_CONV :
thm -> thm -> (term -> bool) * conv * conv * conv -> (term -> term -> bool) ->
conv * conv * conv * conv * conv * conv;

(* Sample application of SEMIRING_NORMALIZERS_CONV for :num *)
val NUM_NORMALIZE_CONV : conv;
end

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1