# Structure Grobner

(* ========================================================================= *)
(* 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_neg_tm,ring_add_tm,ring_sub_tm,
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

*HOL 4, Trindemossen-1*