tuned conversion from terms to "polynomials" for arith_tac: takes care
of "uminus" now.
--- a/src/HOL/arith_data.ML Wed Dec 12 18:05:44 2001 +0100
+++ b/src/HOL/arith_data.ML Wed Dec 12 19:19:59 2001 +0100
@@ -267,6 +267,8 @@
fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
Const("Numeral.number_of",_)$n
=> demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
+ | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
+ => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
| Const("Suc",_) $ _
=> demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
| Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
@@ -284,6 +286,7 @@
| demult(t as Const("Numeral.number_of",_)$n,m) =
((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
handle TERM _ => (Some t,m))
+ | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
| demult(atom,m) = (Some atom,m)
and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')