# HG changeset patch
# User nipkow
# Date 917174034 -3600
# Node ID 5892fdda22c9b3bc31666131ba3b62170670003a
# Parent  71974ec3ebfbdc38d4affff28748fa36c55fe343
Fixed a bug in lin.arith.

diff -r 71974ec3ebfb -r 5892fdda22c9 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Jan 22 17:47:46 1999 +0100
+++ b/src/HOL/Arith.ML	Sun Jan 24 11:33:54 1999 +0100
@@ -880,6 +880,8 @@
 
 val lessD = [Suc_leI];
 
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
@@ -887,6 +889,14 @@
       if t = Const("0",HOLogic.natT) then (p,i)
       else (case assoc(p,t) of None => ((t,1)::p,i)
             | Some m => (overwrite(p,(t,m+1)), i))
+fun poly(t, pi as (p,i)) =
+  if HOLogic.is_zero t then pi else
+  (case try HOLogic.dest_Suc t of
+    Some u => poly(u, (p,i+1))
+  | None => (case try dest_plus t of
+               Some(r,s) => poly(r,poly(s,pi))
+             | None => (case assoc(p,t) of None => ((t,1)::p,i)
+                        | Some m => (overwrite(p,(t,m+1)), i))))
 
 fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
 
@@ -912,7 +922,7 @@
 (* reduce contradictory <= to False.
    Most of the work is done by the cancel tactics.
 *)
-val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
+val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
 
 val cancel_sums_ss = HOL_basic_ss addsimps add_rules
                                   addsimprocs nat_cancel_sums_add;