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 
(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 
bind_thm ("fib_Suc_Suc", hd(rev fib.rules));


21 


22 


23 
(*Concrete Mathematics, page 280*)


24 
goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";


25 
by (res_inst_tac [("u","n")] fib.induct 1);


26 
(*Simplify the LHS just enough to apply the induction hypotheses*)


27 
by (asm_full_simp_tac


28 
(!simpset addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);


29 
by (ALLGOALS


30 
(asm_simp_tac (!simpset addsimps


31 
(fib.rules @ add_ac @ mult_ac @


32 
[add_mult_distrib, add_mult_distrib2]))));


33 
qed "fib_add";


34 


35 


36 
goal thy "fib (Suc n) ~= 0";


37 
by (res_inst_tac [("u","n")] fib.induct 1);


38 
by (ALLGOALS (asm_simp_tac (!simpset addsimps fib.rules)));


39 
qed "fib_Suc_neq_0";


40 
Addsimps [fib_Suc_neq_0];


41 


42 


43 


44 
(*Concrete Mathematics, page 278: Cassini's identity*)


45 
goal thy "fib (Suc (Suc n)) * fib n = \


46 
\ (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \


47 
\ else Suc (fib(Suc n) * fib(Suc n)))";


48 
by (res_inst_tac [("u","n")] fib.induct 1);


49 
by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);


50 
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);


51 
by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3);


52 
by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);


53 
by (ALLGOALS (*using fib.rules here results in a longer proof!*)


54 
(asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2,


55 
mod_less, mod_Suc]

3919

56 
addsplits [expand_if])));

3724

57 
by (safe_tac (!claset addSDs [mod2_neq_0]));

3300

58 
by (ALLGOALS


59 
(asm_full_simp_tac


60 
(!simpset addsimps (fib.rules @ add_ac @ mult_ac @


61 
[add_mult_distrib, add_mult_distrib2,


62 
mod_less, mod_Suc]))));


63 
qed "fib_Cassini";


64 


65 


66 
(** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **)
