author | nipkow |
Wed, 06 Sep 2000 08:04:41 +0200 | |
changeset 9870 | 2374ba026fc6 |
parent 9826 | 5b5d9ee742ca |
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 |
||
8658 | 20 |
Delsimps fib.Suc_Suc; |
4809 | 21 |
|
8658 | 22 |
val [fib_Suc_Suc] = fib.Suc_Suc; |
4809 | 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"; |
9747 | 27 |
by (induct_thm_tac fib.induct "n" 1); |
3300 | 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"; |
9747 | 38 |
by (induct_thm_tac fib.induct "n" 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 |
|
8778
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
50 |
(*Concrete Mathematics, page 278: Cassini's identity. |
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
51 |
It is much easier to prove using integers!*) |
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
52 |
Goal "int (fib (Suc (Suc n)) * fib n) = \ |
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
53 |
\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ |
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
54 |
\ else int (fib(Suc n) * fib(Suc n)) + #1)"; |
9747 | 55 |
by (induct_thm_tac fib.induct "n" 1); |
8778
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
56 |
by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); |
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
57 |
by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1); |
6916 | 58 |
by (asm_full_simp_tac |
59 |
(simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, |
|
8778
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
60 |
mod_Suc, zmult_int RS sym] @ zmult_ac) 1); |
3300 | 61 |
qed "fib_Cassini"; |
62 |
||
63 |
||
8778
268195e8c017
Cassini identity is easier to prove using INTEGERS
paulson
parents:
8658
diff
changeset
|
64 |
|
4809 | 65 |
(** Towards Law 6.111 of Concrete Mathematics **) |
66 |
||
9826 | 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 |
||
5069 | 74 |
Goal "gcd(fib n, fib (Suc n)) = 1"; |
9747 | 75 |
by (induct_thm_tac fib.induct "n" 1); |
9826 | 76 |
by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3); |
4809 | 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 |
||
5069 | 83 |
Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; |
4809 | 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 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
94 |
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
|
95 |
by (rtac (gcd_fib_add RS sym RS trans) 1); |
4809 | 96 |
by (Asm_simp_tac 1); |
97 |
qed "gcd_fib_diff"; |
|
98 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
99 |
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; |
9870 | 100 |
by (induct_thm_tac nat_less_induct "n" 1); |
4809 | 101 |
by (stac mod_if 1); |
102 |
by (Asm_simp_tac 1); |
|
8395 | 103 |
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, |
4809 | 104 |
not_less_iff_le, diff_less]) 1); |
105 |
qed "gcd_fib_mod"; |
|
106 |
||
107 |
(*Law 6.111*) |
|
5069 | 108 |
Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; |
9747 | 109 |
by (induct_thm_tac gcd_induct "m n" 1); |
4809 | 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"; |