src/HOL/ex/NatSum.ML
author wenzelm
Mon, 12 Jan 1998 17:26:34 +0100
changeset 4558 31becfd8d329
parent 4246 c539e702e1d2
child 5069 3ea049f7979d
permissions -rw-r--r--
Delsimprocs nat_cancel;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1805
10494d0241cd Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1783
diff changeset
     1
(*  Title:      HOL/ex/NatSum.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
diff changeset
     3
    Author:     Tobias Nipkow
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
3269
eca2a3634acd Function "sum" now defined using primrec
paulson
parents: 1805
diff changeset
     6
Summing natural numbers, squares and cubes.  Could be continued...
eca2a3634acd Function "sum" now defined using primrec
paulson
parents: 1805
diff changeset
     7
Demonstrates permutative rewriting.
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
4558
31becfd8d329 Delsimprocs nat_cancel;
wenzelm
parents: 4246
diff changeset
    10
Delsimprocs nat_cancel;
3269
eca2a3634acd Function "sum" now defined using primrec
paulson
parents: 1805
diff changeset
    11
Addsimps add_ac;
eca2a3634acd Function "sum" now defined using primrec
paulson
parents: 1805
diff changeset
    12
Addsimps [add_mult_distrib, add_mult_distrib2];
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
(*The sum of the first n positive integers equals n(n+1)/2.*)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3648
diff changeset
    15
goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    16
by (Simp_tac 1);
4246
c539e702e1d2 Now uses induct_tac
paulson
parents: 3842
diff changeset
    17
by (induct_tac "n" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    18
by (Simp_tac 1);
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    19
by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
qed "sum_of_naturals";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
goal NatSum.thy
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3648
diff changeset
    23
  "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    24
by (Simp_tac 1);
4246
c539e702e1d2 Now uses induct_tac
paulson
parents: 3842
diff changeset
    25
by (induct_tac "n" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    26
by (Simp_tac 1);
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    27
by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    28
qed "sum_of_squares";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    29
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    30
goal NatSum.thy
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3648
diff changeset
    31
  "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    32
by (Simp_tac 1);
4246
c539e702e1d2 Now uses induct_tac
paulson
parents: 3842
diff changeset
    33
by (induct_tac "n" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    34
by (Simp_tac 1);
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    35
by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    36
qed "sum_of_cubes";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    37
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    38
(*The sum of the first n odd numbers equals n squared.*)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3648
diff changeset
    39
goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n";
4246
c539e702e1d2 Now uses induct_tac
paulson
parents: 3842
diff changeset
    40
by (induct_tac "n" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    41
by (Simp_tac 1);
3ae9fe3c0f68 added local simpsets
clasohm
parents: 969
diff changeset
    42
by (Asm_simp_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    43
qed "sum_of_odds";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    44