author  paulson 
Wed, 15 Jul 1998 10:15:13 +0200  
changeset 5143  b94cd208f073 
parent 5069  3ea049f7979d 
child 5537  c2bd39a2c0ee 
permissions  rwrr 
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 

4809  20 
val [fib_0, fib_1, fib_Suc_Suc] = fib.rules; 
3300  21 

4809  22 
Addsimps [fib_0, fib_1]; 
23 

24 

25 
val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; 

3300  26 

27 
(*Concrete Mathematics, page 280*) 

5069  28 
Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; 
3300  29 
by (res_inst_tac [("u","n")] fib.induct 1); 
30 
(*Simplify the LHS just enough to apply the induction hypotheses*) 

31 
by (asm_full_simp_tac 

4385  32 
(simpset() addsimps [read_instantiate[("x","Suc(?m+?n)")] fib_Suc_Suc]) 3); 
3300  33 
by (ALLGOALS 
4089  34 
(asm_simp_tac (simpset() addsimps 
4809  35 
([] @ add_ac @ mult_ac @ 
36 
[fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); 

3300  37 
qed "fib_add"; 
38 

39 

5069  40 
Goal "fib (Suc n) ~= 0"; 
3300  41 
by (res_inst_tac [("u","n")] fib.induct 1); 
4809  42 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); 
3300  43 
qed "fib_Suc_neq_0"; 
44 

4809  45 
(* Also add 0 < fib (Suc n) *) 
46 
Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; 

4379  47 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

48 
Goal "0<n ==> 0 < fib n"; 
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset

49 
by (rtac (not0_implies_Suc RS exE) 1); 
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset

50 
by Auto_tac; 
4809  51 
qed "fib_gr_0"; 
3300  52 

53 

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

5069  55 
Goal "fib (Suc (Suc n)) * fib n = \ 
4710  56 
\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n))  1 \ 
3300  57 
\ else Suc (fib(Suc n) * fib(Suc n)))"; 
58 
by (res_inst_tac [("u","n")] fib.induct 1); 

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

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

4089  61 
by (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 3); 
4809  62 
by (stac fib_Suc3 3); 
63 
by (ALLGOALS (*using [fib_Suc_Suc] here results in a longer proof!*) 

4089  64 
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
4686  65 
mod_less, mod_Suc]))); 
3300  66 
by (ALLGOALS 
67 
(asm_full_simp_tac 

4809  68 
(simpset() addsimps ([] @ add_ac @ mult_ac @ 
69 
[fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 

3300  70 
mod_less, mod_Suc])))); 
71 
qed "fib_Cassini"; 

72 

73 

4809  74 
(** Towards Law 6.111 of Concrete Mathematics **) 
75 

5069  76 
Goal "gcd(fib n, fib (Suc n)) = 1"; 
4809  77 
by (res_inst_tac [("u","n")] fib.induct 1); 
78 
by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3); 

79 
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc]))); 

80 
qed "gcd_fib_Suc_eq_1"; 

81 

82 
val gcd_fib_commute = 

83 
read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute; 

84 

5069  85 
Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; 
4809  86 
by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1); 
87 
by (case_tac "m=0" 1); 

88 
by (Asm_simp_tac 1); 

89 
by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1); 

90 
by (simp_tac (simpset() addsimps [fib_add]) 1); 

91 
by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1); 

92 
by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1); 

93 
by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1); 

94 
qed "gcd_fib_add"; 

95 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

96 
Goal "m <= n ==> gcd(fib m, fib (nm)) = gcd(fib m, fib n)"; 
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset

97 
by (rtac (gcd_fib_add RS sym RS trans) 1); 
4809  98 
by (Asm_simp_tac 1); 
99 
qed "gcd_fib_diff"; 

100 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

101 
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; 
4809  102 
by (res_inst_tac [("n","n")] less_induct 1); 
103 
by (stac mod_if 1); 

104 
by (Asm_simp_tac 1); 

105 
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_less, mod_geq, 

106 
not_less_iff_le, diff_less]) 1); 

107 
qed "gcd_fib_mod"; 

108 

109 
(*Law 6.111*) 

5069  110 
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

111 
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); 
4809  112 
by (Asm_simp_tac 1); 
113 
by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); 

114 
by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1); 

115 
qed "fib_gcd"; 