1 (* ========================================================================= *)
2 (* Trivial restriction of complex Groebner bases to reals. *)
3 (* ========================================================================= *)
5 let GROBNER_REAL_ARITH =
6 let trans_conv = GEN_REWRITE_CONV TOP_SWEEP_CONV
7 [GSYM CX_INJ; CX_POW; CX_MUL; CX_ADD; CX_NEG; CX_SUB] in
8 fun tm -> let th = trans_conv tm in
9 EQ_MP (SYM th) (COMPLEX_ARITH(rand(concl th)));;