author | paulson |
Wed, 23 Sep 1998 10:12:01 +0200 | |
changeset 5537 | c2bd39a2c0ee |
parent 5143 | b94cd208f073 |
child 6916 | 4957978b6f9e |
permissions | -rw-r--r-- |
3300 | 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 |
||
4809 | 20 |
val [fib_0, fib_1, fib_Suc_Suc] = fib.rules; |
3300 | 21 |
|
4809 | 22 |
Addsimps [fib_0, fib_1]; |
23 |
||
24 |
||
25 |
val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; |
|
3300 | 26 |
|
27 |
(*Concrete Mathematics, page 280*) |
|
5069 | 28 |
Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; |
3300 | 29 |
by (res_inst_tac [("u","n")] fib.induct 1); |
30 |
(*Simplify the LHS just enough to apply the induction hypotheses*) |
|
31 |
by (asm_full_simp_tac |
|
4385 | 32 |
(simpset() addsimps [read_instantiate[("x","Suc(?m+?n)")] fib_Suc_Suc]) 3); |
3300 | 33 |
by (ALLGOALS |
4089 | 34 |
(asm_simp_tac (simpset() addsimps |
4809 | 35 |
([] @ add_ac @ mult_ac @ |
36 |
[fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); |
|
3300 | 37 |
qed "fib_add"; |
38 |
||
39 |
||
5069 | 40 |
Goal "fib (Suc n) ~= 0"; |
3300 | 41 |
by (res_inst_tac [("u","n")] fib.induct 1); |
4809 | 42 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); |
3300 | 43 |
qed "fib_Suc_neq_0"; |
44 |
||
4809 | 45 |
(* Also add 0 < fib (Suc n) *) |
46 |
Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; |
|
4379 | 47 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
48 |
Goal "0<n ==> 0 < fib n"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
49 |
by (rtac (not0_implies_Suc RS exE) 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
50 |
by Auto_tac; |
4809 | 51 |
qed "fib_gr_0"; |
3300 | 52 |
|
53 |
||
54 |
(*Concrete Mathematics, page 278: Cassini's identity*) |
|
5069 | 55 |
Goal "fib (Suc (Suc n)) * fib n = \ |
4710 | 56 |
\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \ |
3300 | 57 |
\ else Suc (fib(Suc n) * fib(Suc n)))"; |
58 |
by (res_inst_tac [("u","n")] fib.induct 1); |
|
59 |
by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3); |
|
60 |
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3); |
|
4089 | 61 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 3); |
4809 | 62 |
by (stac fib_Suc3 3); |
63 |
by (ALLGOALS (*using [fib_Suc_Suc] here results in a longer proof!*) |
|
4089 | 64 |
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, |
4686 | 65 |
mod_less, mod_Suc]))); |
3300 | 66 |
by (ALLGOALS |
67 |
(asm_full_simp_tac |
|
5537 | 68 |
(simpset() addsimps add_ac @ mult_ac @ |
4809 | 69 |
[fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, |
5537 | 70 |
mod_less, mod_Suc]))); |
3300 | 71 |
qed "fib_Cassini"; |
72 |
||
73 |
||
4809 | 74 |
(** Towards Law 6.111 of Concrete Mathematics **) |
75 |
||
5069 | 76 |
Goal "gcd(fib n, fib (Suc n)) = 1"; |
4809 | 77 |
by (res_inst_tac [("u","n")] fib.induct 1); |
78 |
by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3); |
|
79 |
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc]))); |
|
80 |
qed "gcd_fib_Suc_eq_1"; |
|
81 |
||
82 |
val gcd_fib_commute = |
|
83 |
read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute; |
|
84 |
||
5069 | 85 |
Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; |
4809 | 86 |
by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1); |
87 |
by (case_tac "m=0" 1); |
|
88 |
by (Asm_simp_tac 1); |
|
89 |
by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1); |
|
90 |
by (simp_tac (simpset() addsimps [fib_add]) 1); |
|
91 |
by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1); |
|
92 |
by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1); |
|
93 |
by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1); |
|
94 |
qed "gcd_fib_add"; |
|
95 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
96 |
Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
97 |
by (rtac (gcd_fib_add RS sym RS trans) 1); |
4809 | 98 |
by (Asm_simp_tac 1); |
99 |
qed "gcd_fib_diff"; |
|
100 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
101 |
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; |
4809 | 102 |
by (res_inst_tac [("n","n")] less_induct 1); |
103 |
by (stac mod_if 1); |
|
104 |
by (Asm_simp_tac 1); |
|
105 |
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_less, mod_geq, |
|
106 |
not_less_iff_le, diff_less]) 1); |
|
107 |
qed "gcd_fib_mod"; |
|
108 |
||
109 |
(*Law 6.111*) |
|
5069 | 110 |
Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
111 |
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
4809 | 112 |
by (Asm_simp_tac 1); |
113 |
by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); |
|
114 |
by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1); |
|
115 |
qed "fib_gcd"; |