Fixed a bug in lin.arith.
authornipkow
Sun Jan 24 11:33:54 1999 +0100 (1999-01-24)
changeset 61515892fdda22c9
parent 6150 71974ec3ebfb
child 6152 bc1e27bcc195
Fixed a bug in lin.arith.
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Jan 22 17:47:46 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sun Jan 24 11:33:54 1999 +0100
     1.3 @@ -880,6 +880,8 @@
     1.4  
     1.5  val lessD = [Suc_leI];
     1.6  
     1.7 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
     1.8 +
     1.9  (* Turn term into list of summand * multiplicity plus a constant *)
    1.10  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.11    | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
    1.12 @@ -887,6 +889,14 @@
    1.13        if t = Const("0",HOLogic.natT) then (p,i)
    1.14        else (case assoc(p,t) of None => ((t,1)::p,i)
    1.15              | Some m => (overwrite(p,(t,m+1)), i))
    1.16 +fun poly(t, pi as (p,i)) =
    1.17 +  if HOLogic.is_zero t then pi else
    1.18 +  (case try HOLogic.dest_Suc t of
    1.19 +    Some u => poly(u, (p,i+1))
    1.20 +  | None => (case try dest_plus t of
    1.21 +               Some(r,s) => poly(r,poly(s,pi))
    1.22 +             | None => (case assoc(p,t) of None => ((t,1)::p,i)
    1.23 +                        | Some m => (overwrite(p,(t,m+1)), i))))
    1.24  
    1.25  fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
    1.26  
    1.27 @@ -912,7 +922,7 @@
    1.28  (* reduce contradictory <= to False.
    1.29     Most of the work is done by the cancel tactics.
    1.30  *)
    1.31 -val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
    1.32 +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
    1.33  
    1.34  val cancel_sums_ss = HOL_basic_ss addsimps add_rules
    1.35                                    addsimprocs nat_cancel_sums_add;