ex/NatSum.ML
author lcp
Thu, 21 Apr 1994 11:28:32 +0200
changeset 68 acad709cad5d
parent 65 52771c21d9ca
child 82 0dbbf4426782
permissions -rw-r--r--
tidied definitions and proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63
94436622324d Added some sums.
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/ex/natsum.ML
94436622324d Added some sums.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
94436622324d Added some sums.
nipkow
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
94436622324d Added some sums.
nipkow
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
94436622324d Added some sums.
nipkow
parents:
diff changeset
     5
94436622324d Added some sums.
nipkow
parents:
diff changeset
     6
Summing natural numbers, squares and cubes. Could be continued...
94436622324d Added some sums.
nipkow
parents:
diff changeset
     7
*)
94436622324d Added some sums.
nipkow
parents:
diff changeset
     8
94436622324d Added some sums.
nipkow
parents:
diff changeset
     9
val natsum_ss = arith_ss addsimps
94436622324d Added some sums.
nipkow
parents:
diff changeset
    10
  ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
94436622324d Added some sums.
nipkow
parents:
diff changeset
    11
94436622324d Added some sums.
nipkow
parents:
diff changeset
    12
goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
65
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    13
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    14
by (nat_ind_tac "n" 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    15
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    16
by (asm_simp_tac natsum_ss 1);
63
94436622324d Added some sums.
nipkow
parents:
diff changeset
    17
result();
94436622324d Added some sums.
nipkow
parents:
diff changeset
    18
94436622324d Added some sums.
nipkow
parents:
diff changeset
    19
goal NatSum.thy
94436622324d Added some sums.
nipkow
parents:
diff changeset
    20
  "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
94436622324d Added some sums.
nipkow
parents:
diff changeset
    21
\  n*Suc(n)*Suc(Suc(Suc(0))*n)";
65
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    22
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    23
by (nat_ind_tac "n" 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    24
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    25
by (asm_simp_tac natsum_ss 1);
63
94436622324d Added some sums.
nipkow
parents:
diff changeset
    26
result();
94436622324d Added some sums.
nipkow
parents:
diff changeset
    27
94436622324d Added some sums.
nipkow
parents:
diff changeset
    28
goal NatSum.thy
94436622324d Added some sums.
nipkow
parents:
diff changeset
    29
  "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
65
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    30
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    31
by (nat_ind_tac "n" 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    32
by (simp_tac natsum_ss 1);
52771c21d9ca Now simplifies before the induction
lcp
parents: 63
diff changeset
    33
by (asm_simp_tac natsum_ss 1);
63
94436622324d Added some sums.
nipkow
parents:
diff changeset
    34
result();