author  chaieb 
Fri, 11 Nov 2005 10:50:43 +0100  
changeset 18156  5a971b272f78 
parent 16417  9bc16273c2d4 
child 20272  0ca998e83447 
permissions  rwrr 
15628  1 
(* ID: $Id$ 
9944  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1997 University of Cambridge 

4 
*) 

5 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

6 
header {* The Fibonacci function *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

7 

16417  8 
theory Fib imports Primes begin 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

9 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

10 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

11 
Fibonacci numbers: proofs of laws taken from: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

12 
R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

13 
(AddisonWesley, 1989) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

14 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

15 
\bigskip 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

16 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

17 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

18 
consts fib :: "nat => nat" 
15628  19 
recdef fib "measure (\<lambda>x. x)" 
20 
zero: "fib 0 = 0" 

21 
one: "fib (Suc 0) = Suc 0" 

22 
Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

23 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

24 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

25 
\medskip The difficulty in these proofs is to ensure that the 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

26 
induction hypotheses are applied before the definition of @{term 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

27 
fib}. Towards this end, the @{term fib} equations are not declared 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

28 
to the Simplifier and are applied very selectively at first. 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

29 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

30 

15628  31 
text{*We disable @{text fib.Suc_Suc} for simplification ...*} 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

32 
declare fib.Suc_Suc [simp del] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

33 

15628  34 
text{*...then prove a version that has a more restrictive pattern.*} 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

35 
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" 
15628  36 
by (rule fib.Suc_Suc) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

37 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

38 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

39 
text {* \medskip Concrete Mathematics, page 280 *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

40 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

41 
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

42 
apply (induct n rule: fib.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

43 
prefer 3 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

44 
txt {* simplify the LHS just enough to apply the induction hypotheses *} 
15628  45 
apply (simp add: fib_Suc3) 
46 
apply (simp_all add: fib.Suc_Suc add_mult_distrib2) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

47 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

48 

15628  49 
lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

50 
apply (induct n rule: fib.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

51 
apply (simp_all add: fib.Suc_Suc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

52 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

53 

15628  54 
lemma fib_Suc_gr_0: "0 < fib (Suc n)" 
55 
by (insert fib_Suc_neq_0 [of n], simp) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

56 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

57 
lemma fib_gr_0: "0 < n ==> 0 < fib n" 
15628  58 
by (case_tac n, auto simp add: fib_Suc_gr_0) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

59 

9944  60 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

61 
text {* 
15628  62 
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is 
63 
much easier using integers, not natural numbers! 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

64 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

65 

15628  66 
lemma fib_Cassini_int: 
15003  67 
"int (fib (Suc (Suc n)) * fib n) = 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11786
diff
changeset

68 
(if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n))  1 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11786
diff
changeset

69 
else int (fib (Suc n) * fib (Suc n)) + 1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

70 
apply (induct n rule: fib.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

71 
apply (simp add: fib.Suc_Suc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

72 
apply (simp add: fib.Suc_Suc mod_Suc) 
15628  73 
apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2 
74 
mod_Suc zmult_int [symmetric]) 

18156
5a971b272f78
a proof step corrected due to the changement in the presburger method.
chaieb
parents:
16417
diff
changeset

75 
apply (presburger (no_abs)) 
15628  76 
done 
77 

78 
text{*We now obtain a version for the natural numbers via the coercion 

79 
function @{term int}.*} 

80 
theorem fib_Cassini: 

81 
"fib (Suc (Suc n)) * fib n = 

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

83 
else fib (Suc n) * fib (Suc n) + 1)" 

84 
apply (rule int_int_eq [THEN iffD1]) 

85 
apply (simp add: fib_Cassini_int) 

86 
apply (subst zdiff_int [symmetric]) 

87 
apply (insert fib_Suc_gr_0 [of n], simp_all) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

88 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

89 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

90 

15628  91 
text {* \medskip Toward Law 6.111 of Concrete Mathematics *} 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

92 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset

93 
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

94 
apply (induct n rule: fib.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

95 
prefer 3 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

96 
apply (simp add: gcd_commute fib_Suc3) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

97 
apply (simp_all add: fib.Suc_Suc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

98 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

99 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

100 
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" 
15628  101 
apply (simp add: gcd_commute [of "fib m"]) 
102 
apply (case_tac m) 

103 
apply simp 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

104 
apply (simp add: fib_add) 
15628  105 
apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0]) 
106 
apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric]) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

107 
apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

108 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

109 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

110 
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n  m)) = gcd (fib m, fib n)" 
15628  111 
by (simp add: gcd_fib_add [symmetric, of _ "nm"]) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

112 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

113 
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

114 
apply (induct n rule: nat_less_induct) 
15628  115 
apply (simp add: mod_if gcd_fib_diff mod_geq) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

116 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

117 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

118 
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  {* Law 6.111 *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

119 
apply (induct m n rule: gcd_induct) 
15628  120 
apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

121 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

122 

15628  123 
theorem fib_mult_eq_setsum: 
11786  124 
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

125 
apply (induct n rule: fib.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

126 
apply (auto simp add: atMost_Suc fib.Suc_Suc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

127 
apply (simp add: add_mult_distrib add_mult_distrib2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

128 
done 
9944  129 

130 
end 