author nipkow Thu, 21 Dec 2000 16:19:39 +0100 changeset 10718 c058f78c3544 parent 10717 c09d4ebfec83 child 10719 8666477dd9a2
rational arithmetic
 src/HOL/arith_data.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/arith_data.ML	Thu Dec 21 16:18:40 2000 +0100
+++ b/src/HOL/arith_data.ML	Thu Dec 21 16:19:39 2000 +0100
@@ -306,9 +306,39 @@
fun rat_of_term(numt,dent) =
let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent
in if den = 0 then raise Zero else int_ratdiv(num,den) end;
-
+
+(* Warning: in rare cases number_of encloses a non-numeral,
+   in which case dest_binum raises TERM; hence all the handles below.
+*)
+
+(* decompose nested multiplications, bracketing them to the right and combining all
+   their coefficients
+*)
+
+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("op *",_) \$ s1 \$ s2 => demult(mC \$ s1 \$ (mC \$ s2 \$ t),m)
+      | Const("HOL.divide",_) \$ numt \$ (Const("Numeral.number_of",_)\$dent) =>
+          let val den = HOLogic.dest_binum dent
+          in if den = 0 then raise Zero
+             else demult(mC \$ numt \$ t,ratmul(m, ratinv(rat_of_int den)))
+          end
+      | _ => atomult(mC,s,t,m)
+      ) handle TERM _ => atomult(mC,s,t,m))
+  | demult(atom as Const("HOL.divide",_) \$ t \$ (Const("Numeral.number_of",_)\$dent), m) =
+      (let val den = HOLogic.dest_binum dent
+       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
+       handle TERM _ => (Some atom,m))
+  | 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(atom,m) = (Some atom,m)
+
+and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')
+                            | (Some t',m') => (Some(mC \$ atom \$ t'),m'))
+
fun decomp2 inj_consts (rel,lhs,rhs) =
-
let
(* Turn term into list of summand * multiplicity plus a constant *)
fun poly(Const("op +",_) \$ s \$ t, m, pi) = poly(s,m,poly(t,m,pi))
@@ -318,33 +348,23 @@
| poly(Const("uminus",_) \$ t, m, pi) = poly(t,ratneg m,pi)
| poly(Const("0",_), _, pi) = pi
| poly(Const("Suc",_)\$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
-  | poly(all as Const("op *",_) \$ (Const("Numeral.number_of",_)\$c) \$ t, m, pi)=
-      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
-       handle TERM _ => add_atom(all,m,pi))
-  | poly(all as Const("op *",_) \$ t \$ (Const("Numeral.number_of",_)\$c), m, pi)=
-      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
-       handle TERM _ => add_atom(all,m,pi))
-  | poly(Const("op *",_) \$ (Const("HOL.divide",_) \$ (Const("Numeral.number_of",_)\$numt) \$
-                                               (Const("Numeral.number_of",_)\$dent)) \$ t, m, pi) =
-      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
-  | poly(Const("op *",_) \$ t \$ (Const("HOL.divide",_) \$ (Const("Numeral.number_of",_)\$numt) \$
-                                               (Const("Numeral.number_of",_)\$dent)), m, pi) =
-      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
-  | poly(all as Const("HOL.divide",_) \$ t \$ (Const("Numeral.number_of",_)\$dent), m, pi) =
-      let val den = HOLogic.dest_binum dent
-      in if den = 0 then raise Zero else poly(t,ratmul(m, ratinv(rat_of_int den)),pi) end
-  | poly(all as Const("Numeral.number_of",_)\$t,m,(p,i)) =
-      handle TERM _ => add_atom(all,m,(p,i)))
-  | poly(Const("HOL.divide",_) \$ (Const("Numeral.number_of",_)\$numt) \$
-                                 (Const("Numeral.number_of",_)\$dent), m, (p,i)) =
+  | poly(t as Const("op *",_) \$ _ \$ _, m, pi as (p,i)) =
+      (case demult(t,m) of
+       | (Some u,m') => add_atom(u,m',pi))
+  | poly(t as Const("HOL.divide",_) \$ _ \$ _, m, pi as (p,i)) =
+      (case demult(t,m) of
+       | (Some u,m') => add_atom(u,m',pi))
+  | poly(all as (Const("Numeral.number_of",_)\$t,m,(p,i))) =