# HG changeset patch
# User nipkow
# Date 991318055 -7200
# Node ID a16eaf2a1edd9b9b085ea06b4f6a1a9facfe32f5
# Parent  d6b69fe04c1b10548d74735d3a2fb3ff7b1ad09b
Allow Suc-numerals as coefficients in lin-arith formulae

diff -r d6b69fe04c1b -r a16eaf2a1edd src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Thu May 31 12:43:56 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Thu May 31 16:07:35 2001 +0200
@@ -574,7 +574,7 @@
    le_Suc_number_of,le_number_of_Suc,
    less_Suc_number_of,less_number_of_Suc,
    Suc_eq_number_of,eq_number_of_Suc,
-   mult_Suc, mult_Suc_right,
+   mult_0, mult_0_right, mult_Suc, mult_Suc_right,
    eq_number_of_0, eq_0_number_of, less_0_number_of,
    nat_number_of, Let_number_of, if_True, if_False];
 
diff -r d6b69fe04c1b -r a16eaf2a1edd src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu May 31 12:43:56 2001 +0200
+++ b/src/HOL/arith_data.ML	Thu May 31 16:07:35 2001 +0200
@@ -253,8 +253,14 @@
 
 (* Warning: in rare cases number_of encloses a non-numeral,
    in which case dest_binum raises TERM; hence all the handles below.
+   Same for Suc-terms that turn out not to be numerals -
+   although the simplifier should eliminate those anyway...
 *)
 
+fun number_of_Sucs (Const("Suc",_) $ n) = number_of_Sucs n + 1
+  | number_of_Sucs t = if HOLogic.is_zero t then 0
+                       else raise TERM("number_of_Sucs",[])
+
 (* decompose nested multiplications, bracketing them to the right and combining all
    their coefficients
 *)
@@ -262,6 +268,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("Suc",_) $ _
+        => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
       | 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