9944

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 
(AddisonWesley, 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 (nm)) = 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";
