src/HOL/ex/NatSum.ML
changeset 1783 173ce86b4c22
parent 1465 5d7a7e439cec
child 1805 10494d0241cd
equal deleted inserted replaced
1782:ab45b881fa62 1783:173ce86b4c22
     7 *)
     7 *)
     8 
     8 
     9 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
     9 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
    10 
    10 
    11 (*The sum of the first n positive integers equals n(n+1)/2.*)
    11 (*The sum of the first n positive integers equals n(n+1)/2.*)
    12 goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)";
    12 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
    13 by (Simp_tac 1);
    13 by (Simp_tac 1);
    14 by (nat_ind_tac "n" 1);
    14 by (nat_ind_tac "n" 1);
    15 by (Simp_tac 1);
    15 by (Simp_tac 1);
    16 by (Asm_simp_tac 1);
    16 by (Asm_simp_tac 1);
    17 qed "sum_of_naturals";
    17 qed "sum_of_naturals";