src/HOL/ex/NatSum.ML
changeset 4558 31becfd8d329
parent 4246 c539e702e1d2
child 5069 3ea049f7979d
equal deleted inserted replaced
4557:03003b966e91 4558:31becfd8d329
     5 
     5 
     6 Summing natural numbers, squares and cubes.  Could be continued...
     6 Summing natural numbers, squares and cubes.  Could be continued...
     7 Demonstrates permutative rewriting.
     7 Demonstrates permutative rewriting.
     8 *)
     8 *)
     9 
     9 
       
    10 Delsimprocs nat_cancel;
    10 Addsimps add_ac;
    11 Addsimps add_ac;
    11 Addsimps [add_mult_distrib, add_mult_distrib2];
    12 Addsimps [add_mult_distrib, add_mult_distrib2];
    12 
    13 
    13 (*The sum of the first n positive integers equals n(n+1)/2.*)
    14 (*The sum of the first n positive integers equals n(n+1)/2.*)
    14 goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
    15 goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";