author nipkow Wed, 12 Dec 2001 19:19:59 +0100 changeset 12480 32e67277a4b9 parent 12479 ed46612ad7ec child 12481 ea5d6da573c5
tuned conversion from terms to "polynomials" for arith_tac: takes care of "uminus" now.
 src/HOL/arith_data.ML file | annotate | diff | comparison | revisions
```--- 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')```