src/HOL/ex/Fib.ML
 author wenzelm Mon, 09 Mar 1998 16:17:28 +0100 changeset 4710 05e57f1879ee parent 4686 74a12e86b20b child 4809 595f905cc348 permissions -rw-r--r--
eliminated pred function;
```
(*  Title:      HOL/ex/Fib
ID:         \$Id\$
Author:     Lawrence C Paulson

Fibonacci numbers: proofs of laws taken from

R. L. Graham, D. E. Knuth, O. Patashnik.
Concrete Mathematics.
*)

(** The difficulty in these proofs is to ensure that the induction hypotheses
are applied before the definition of "fib".  Towards this end, the
"fib" equations are not added to the simpset and are applied very
selectively at first.
**)

bind_thm ("fib_Suc_Suc", hd(rev fib.rules));

(*Concrete Mathematics, page 280*)
goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
by (res_inst_tac [("u","n")] fib.induct 1);
(*Simplify the LHS just enough to apply the induction hypotheses*)
by (asm_full_simp_tac
by (ALLGOALS
(fib.rules @ add_ac @ mult_ac @

goal thy "fib (Suc n) ~= 0";
by (res_inst_tac [("u","n")] fib.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
qed "fib_Suc_neq_0";

goal thy "0 < fib (Suc n)";
by (res_inst_tac [("u","n")] fib.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
qed "fib_Suc_gr_0";

(*Concrete Mathematics, page 278: Cassini's identity*)
goal thy "fib (Suc (Suc n)) * fib n = \
\              (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
\                              else Suc (fib(Suc n) * fib(Suc n)))";
by (res_inst_tac [("u","n")] fib.induct 1);
by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
by (ALLGOALS  (*using fib.rules here results in a longer proof!*)