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

4385

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

3300

29 
by (ALLGOALS

4089

30 
(asm_simp_tac (simpset() addsimps

3300

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);

4089

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

3300

39 
qed "fib_Suc_neq_0";


40 
Addsimps [fib_Suc_neq_0];


41 

4379

42 
goal thy "0 < fib (Suc n)";


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


44 
by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));


45 
qed "fib_Suc_gr_0";


46 
Addsimps [fib_Suc_gr_0];


47 

3300

48 


49 


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


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

4710

52 
\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n))  1 \

3300

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


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


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


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

4089

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

3300

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


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

4089

60 
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2,

4686

61 
mod_less, mod_Suc])));

3300

62 
by (ALLGOALS


63 
(asm_full_simp_tac

4089

64 
(simpset() addsimps (fib.rules @ add_ac @ mult_ac @

3300

65 
[add_mult_distrib, add_mult_distrib2,


66 
mod_less, mod_Suc]))));


67 
qed "fib_Cassini";


68 


69 


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