|
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 Delsimps fib.Suc_Suc; |
|
21 |
|
22 val [fib_Suc_Suc] = fib.Suc_Suc; |
|
23 val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; |
|
24 |
|
25 (*Concrete Mathematics, page 280*) |
|
26 Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; |
|
27 by (induct_thm_tac fib.induct "n" 1); |
|
28 (*Simplify the LHS just enough to apply the induction hypotheses*) |
|
29 by (asm_full_simp_tac |
|
30 (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3); |
|
31 by (ALLGOALS |
|
32 (asm_simp_tac (simpset() addsimps |
|
33 ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); |
|
34 qed "fib_add"; |
|
35 |
|
36 |
|
37 Goal "fib (Suc n) ~= 0"; |
|
38 by (induct_thm_tac fib.induct "n" 1); |
|
39 by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); |
|
40 qed "fib_Suc_neq_0"; |
|
41 |
|
42 (* Also add 0 < fib (Suc n) *) |
|
43 Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; |
|
44 |
|
45 Goal "0<n ==> 0 < fib n"; |
|
46 by (rtac (not0_implies_Suc RS exE) 1); |
|
47 by Auto_tac; |
|
48 qed "fib_gr_0"; |
|
49 |
|
50 (*Concrete Mathematics, page 278: Cassini's identity. |
|
51 It is much easier to prove using integers!*) |
|
52 Goal "int (fib (Suc (Suc n)) * fib n) = \ |
|
53 \ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ |
|
54 \ else int (fib(Suc n) * fib(Suc n)) + #1)"; |
|
55 by (induct_thm_tac fib.induct "n" 1); |
|
56 by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); |
|
57 by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1); |
|
58 by (asm_full_simp_tac |
|
59 (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, |
|
60 mod_Suc, zmult_int RS sym] @ zmult_ac) 1); |
|
61 qed "fib_Cassini"; |
|
62 |
|
63 |
|
64 |
|
65 (** Towards Law 6.111 of Concrete Mathematics **) |
|
66 |
|
67 val gcd_induct = thm "gcd_induct"; |
|
68 val gcd_commute = thm "gcd_commute"; |
|
69 val gcd_add2 = thm "gcd_add2"; |
|
70 val gcd_non_0 = thm "gcd_non_0"; |
|
71 val gcd_mult_cancel = thm "gcd_mult_cancel"; |
|
72 |
|
73 |
|
74 Goal "gcd(fib n, fib (Suc n)) = 1"; |
|
75 by (induct_thm_tac fib.induct "n" 1); |
|
76 by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3); |
|
77 by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc]))); |
|
78 qed "gcd_fib_Suc_eq_1"; |
|
79 |
|
80 val gcd_fib_commute = |
|
81 read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute; |
|
82 |
|
83 Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; |
|
84 by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1); |
|
85 by (case_tac "m=0" 1); |
|
86 by (Asm_simp_tac 1); |
|
87 by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1); |
|
88 by (simp_tac (simpset() addsimps [fib_add]) 1); |
|
89 by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1); |
|
90 by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1); |
|
91 by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1); |
|
92 qed "gcd_fib_add"; |
|
93 |
|
94 Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)"; |
|
95 by (rtac (gcd_fib_add RS sym RS trans) 1); |
|
96 by (Asm_simp_tac 1); |
|
97 qed "gcd_fib_diff"; |
|
98 |
|
99 Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; |
|
100 by (induct_thm_tac nat_less_induct "n" 1); |
|
101 by (stac mod_if 1); |
|
102 by (Asm_simp_tac 1); |
|
103 by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, |
|
104 not_less_iff_le, diff_less]) 1); |
|
105 qed "gcd_fib_mod"; |
|
106 |
|
107 (*Law 6.111*) |
|
108 Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; |
|
109 by (induct_thm_tac gcd_induct "m n" 1); |
|
110 by (Asm_simp_tac 1); |
|
111 by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); |
|
112 by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1); |
|
113 qed "fib_gcd"; |