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