# Structure Grobner

Source File Identifier index Theory binding index

```(* ========================================================================= *)
(* Generic Grobner Basis algorithm. (HOL-Light's grobner.ml)                 *)
(*                                                                           *)
(* Whatever the instantiation, it basically solves the universal theory of   *)
(* the complex numbers, or equivalently something like the theory of all     *)
(* commutative cancellation semirings with no nilpotent elements and having  *)
(* characteristic zero. We could do "all rings" by a more elaborate integer  *)
(* version of Grobner bases, but I don't have any useful applications.       *)
(*                                                                           *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

signature Grobner =
sig
include Abbrev

type rat = Arbrat.rat

(* NOTE: RING_AND_IDEAL_CONV params := (RING params, ideal_cofactors params)

- structure of "params":

(ring_dest_const,ring_mk_const,RING_EQ_CONV,
ring_inv_tm,ring_mul_tm,ring_div_tm,ring_pow_tm,
RING_INTEGRAL,RABINOWITSCH_THM,RING_NORMALIZE_CONV)

where ring_neg_tm (unary), ring_sub_tm (binary), ring_inv_tm (unary) and
ring_div_tm (binary) are not used if RABINOWITSCH_THM is |- T. In the
latter case these terms can be created by genvar() from suitable types.

- statements of RING_INTEGRAL (`add` and `mul` are ring operators):

|- (!x:'a. mul r0 x = r0) /\
(!x y z. add x y = add x z <=> y = z) /\
!w x y z. add (mul w y) (mul x z) = add (mul w z) (mul x y) <=>
w = x \/ y = z

- statements of RABINOWITSCH_THM:

|- !x y. x <> y <=> ?z. mul (sub x y) z = r1 (or |- T)
*)
val RING_AND_IDEAL_CONV : (term -> rat) * (rat -> term) * conv *
term * term * term * term * term * term * term *
thm * thm * conv ->
(term -> thm) * (term list -> term -> term list)

val RING                : (term -> rat) * (rat -> term) * conv *
term * term * term * term * term * term * term *
thm * thm * conv ->
term -> thm

val ideal_cofactors     : (term -> rat) * (rat -> term) * conv *
term * term * term * term * term * term * term *
thm * thm * conv ->
term list -> term -> term list

(* Sample application of RING_AND_IDEAL_CONV to :num *)
val NUM_SIMPLIFY_CONV   : conv
val NUM_RING            : term -> thm

val verbose : bool ref (* default: true *)
end

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1