--- a/src/HOL/Tools/groebner.ML Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Tools/groebner.ML Wed Jun 01 15:10:27 2016 +0200
@@ -32,8 +32,6 @@
if is_binop ct ct' then Thm.dest_binop ct'
else raise CTERM ("dest_binary: bad binop", [ct, ct'])
-val rat_0 = Rat.zero;
-val rat_1 = Rat.one;
val minus_rat = Rat.neg;
val denominator_rat = Rat.dest #> snd #> Rat.of_int;
fun int_of_rat a =
@@ -81,7 +79,7 @@
| ((c1,m1)::o1,(c2,m2)::o2) =>
if m1 = m2 then
let val c = c1 + c2 val rest = grob_add o1 o2 in
- if c = rat_0 then rest else (c,m1)::rest end
+ if c = @0 then rest else (c,m1)::rest end
else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
else (c2,m2)::(grob_add l1 o2);
@@ -99,22 +97,22 @@
fun grob_inv l =
case l of
[(c,vs)] => if (forall (fn x => x = 0) vs) then
- if (c = rat_0) then error "grob_inv: division by zero"
- else [(rat_1 / c,vs)]
+ if c = @0 then error "grob_inv: division by zero"
+ else [(@1 / c,vs)]
else error "grob_inv: non-constant divisor polynomial"
| _ => error "grob_inv: non-constant divisor polynomial";
fun grob_div l1 l2 =
case l2 of
[(c,l)] => if (forall (fn x => x = 0) l) then
- if c = rat_0 then error "grob_div: division by zero"
- else grob_cmul (rat_1 / c,l) l1
+ if c = @0 then error "grob_div: division by zero"
+ else grob_cmul (@1 / c,l) l1
else error "grob_div: non-constant divisor polynomial"
| _ => error "grob_div: non-constant divisor polynomial";
fun grob_pow vars l n =
if n < 0 then error "grob_pow: negative power"
- else if n = 0 then [(rat_1,map (K 0) vars)]
+ else if n = 0 then [(@1,map (K 0) vars)]
else grob_mul l (grob_pow vars l (n - 1));
(* Monomial division operation. *)
@@ -125,7 +123,7 @@
(* Lowest common multiple of two monomials. *)
-fun mlcm (_,m1) (_,m2) = (rat_1, ListPair.map Int.max (m1, m2));
+fun mlcm (_,m1) (_,m2) = (@1, ListPair.map Int.max (m1, m2));
(* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
@@ -179,7 +177,7 @@
if null pol then (pol,hist) else
let val (c',m') = hd pol in
(map (fn (c,m) => (c / c',m)) pol,
- Mmul((rat_1 / c',map (K 0) m'),hist)) end;
+ Mmul((@1 / c',map (K 0) m'),hist)) end;
(* The most popular heuristic is to order critical pairs by LCM monomial. *)
@@ -299,7 +297,7 @@
fun resolve_proof vars prf =
case prf of
Start(~1) => []
- | Start m => [(m,[(rat_1,map (K 0) vars)])]
+ | Start m => [(m,[(@1,map (K 0) vars)])]
| Mmul(pol,lin) =>
let val lis = resolve_proof vars lin in
map (fn (n,p) => (n,grob_cmul pol p)) lis end
@@ -317,7 +315,7 @@
fun grobner_weak vars pols =
let val cert = resolve_proof vars (grobner_refute pols)
val l =
- fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
+ fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert @1 in
(l,map (fn (i,p) => (i,map (fn (d,m) => (l * d,m)) p)) cert) end;
(* Prove a polynomial is in ideal generated by others, using Grobner basis. *)
@@ -331,8 +329,8 @@
fun grobner_strong vars pols pol =
let val vars' = @{cterm "True"}::vars
- val grob_z = [(rat_1,1::(map (K 0) vars))]
- val grob_1 = [(rat_1,(map (K 0) vars'))]
+ val grob_z = [(@1, 1::(map (K 0) vars))]
+ val grob_1 = [(@1, (map (K 0) vars'))]
fun augment p= map (fn (c,m) => (c,0::m)) p
val pols' = map augment pols
val pol' = augment pol
@@ -605,10 +603,10 @@
fun grobify_term vars tm =
((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
- [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
+ [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
handle CTERM _ =>
((let val x = dest_const tm
- in if x = rat_0 then [] else [(x,map (K 0) vars)]
+ in if x = @0 then [] else [(x,map (K 0) vars)]
end)
handle ERROR _ =>
((grob_neg(grobify_term vars (ring_dest_neg tm)))
@@ -662,15 +660,15 @@
in end_itlist ring_mk_mul (mk_const c :: xps)
end
fun holify_polynomial vars p =
- if null p then mk_const (rat_0)
+ if null p then mk_const @0
else end_itlist ring_mk_add (map (holify_monomial vars) p)
in holify_polynomial
end ;
fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]);
fun prove_nz n = eqF_elim
- (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
-val neq_01 = prove_nz (rat_1);
+ (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0)));
+val neq_01 = prove_nz @1;
fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
@@ -712,13 +710,13 @@
val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
in (vars,l,cert,th2)
end)
- val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > rat_0) p)) cert
+ val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
- (filter (fn (c,_) => c < rat_0) p))) cert
+ (filter (fn (c,_) => c < @0) p))) cert
val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
fun thm_fn pols =
- if null pols then Thm.reflexive(mk_const rat_0) else
+ if null pols then Thm.reflexive(mk_const @0) else
end_itlist mk_add
(map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
(nth eths i |> mk_meta_eq)) pols)