# HG changeset patch
# User paulson
# Date 981110556 -3600
# Node ID 1b709f59e33a20598524469414aab0caedff462d
# Parent  a221d8a9413cc7fccb9035a779d15badb5583d35
new theorem fib_mult_eq_setsum

diff -r a221d8a9413c -r 1b709f59e33a src/HOL/NumberTheory/Fib.ML
--- a/src/HOL/NumberTheory/Fib.ML	Fri Feb 02 00:31:39 2001 +0100
+++ b/src/HOL/NumberTheory/Fib.ML	Fri Feb 02 11:42:36 2001 +0100
@@ -111,3 +111,11 @@
 by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
 by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
 qed "fib_gcd";
+
+Goal "fib (Suc n) * fib n = setsum (%k. fib k * fib k) (atMost n)";
+by (induct_thm_tac fib.induct "n" 1);
+by (auto_tac (claset(), simpset() addsimps [atMost_Suc, fib_Suc_Suc]));  
+by (asm_full_simp_tac
+     (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 1);
+qed "fib_mult_eq_setsum";
+