|
1 (* Title: HOL/ex/Fib |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Fibonacci numbers: proofs of laws taken from |
|
7 |
|
8 R. L. Graham, D. E. Knuth, O. Patashnik. |
|
9 Concrete Mathematics. |
|
10 (Addison-Wesley, 1989) |
|
11 *) |
|
12 |
|
13 |
|
14 (** The difficulty in these proofs is to ensure that the induction hypotheses |
|
15 are applied before the definition of "fib". Towards this end, the |
|
16 "fib" equations are not added to the simpset and are applied very |
|
17 selectively at first. |
|
18 **) |
|
19 |
|
20 bind_thm ("fib_Suc_Suc", hd(rev fib.rules)); |
|
21 |
|
22 |
|
23 (*Concrete Mathematics, page 280*) |
|
24 goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; |
|
25 by (res_inst_tac [("u","n")] fib.induct 1); |
|
26 (*Simplify the LHS just enough to apply the induction hypotheses*) |
|
27 by (asm_full_simp_tac |
|
28 (!simpset addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3); |
|
29 by (ALLGOALS |
|
30 (asm_simp_tac (!simpset addsimps |
|
31 (fib.rules @ add_ac @ mult_ac @ |
|
32 [add_mult_distrib, add_mult_distrib2])))); |
|
33 qed "fib_add"; |
|
34 |
|
35 |
|
36 goal thy "fib (Suc n) ~= 0"; |
|
37 by (res_inst_tac [("u","n")] fib.induct 1); |
|
38 by (ALLGOALS (asm_simp_tac (!simpset addsimps fib.rules))); |
|
39 qed "fib_Suc_neq_0"; |
|
40 Addsimps [fib_Suc_neq_0]; |
|
41 |
|
42 |
|
43 |
|
44 (*Concrete Mathematics, page 278: Cassini's identity*) |
|
45 goal thy "fib (Suc (Suc n)) * fib n = \ |
|
46 \ (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \ |
|
47 \ else Suc (fib(Suc n) * fib(Suc n)))"; |
|
48 by (res_inst_tac [("u","n")] fib.induct 1); |
|
49 by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3); |
|
50 by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3); |
|
51 by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3); |
|
52 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3); |
|
53 by (ALLGOALS (*using fib.rules here results in a longer proof!*) |
|
54 (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, |
|
55 mod_less, mod_Suc] |
|
56 setloop split_tac[expand_if]))); |
|
57 by (step_tac (!claset addSDs [mod2_neq_0]) 1); |
|
58 by (ALLGOALS |
|
59 (asm_full_simp_tac |
|
60 (!simpset addsimps (fib.rules @ add_ac @ mult_ac @ |
|
61 [add_mult_distrib, add_mult_distrib2, |
|
62 mod_less, mod_Suc])))); |
|
63 qed "fib_Cassini"; |
|
64 |
|
65 |
|
66 (** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **) |