summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Fibonacci.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 33026 | 8f35633c4922 |

child 37671 | fa53d267dab3 |

permissions | -rw-r--r-- |

more speaking names

1 (* Title: HOL/Isar_Examples/Fibonacci.thy

2 Author: Gertrud Bauer

3 Copyright 1999 Technische Universitaet Muenchen

5 The Fibonacci function. Demonstrates the use of recdef. Original

6 tactic script by Lawrence C Paulson.

8 Fibonacci numbers: proofs of laws taken from

10 R. L. Graham, D. E. Knuth, O. Patashnik.

11 Concrete Mathematics.

12 (Addison-Wesley, 1989)

13 *)

15 header {* Fib and Gcd commute *}

17 theory Fibonacci

18 imports Primes

19 begin

21 text_raw {*

22 \footnote{Isar version by Gertrud Bauer. Original tactic script by

23 Larry Paulson. A few proofs of laws taken from

24 \cite{Concrete-Math}.}

25 *}

28 subsection {* Fibonacci numbers *}

30 fun fib :: "nat \<Rightarrow> nat" where

31 "fib 0 = 0"

32 | "fib (Suc 0) = 1"

33 | "fib (Suc (Suc x)) = fib x + fib (Suc x)"

35 lemma [simp]: "0 < fib (Suc n)"

36 by (induct n rule: fib.induct) simp_all

39 text {* Alternative induction rule. *}

41 theorem fib_induct:

42 "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"

43 by (induct rule: fib.induct) simp_all

46 subsection {* Fib and gcd commute *}

48 text {* A few laws taken from \cite{Concrete-Math}. *}

50 lemma fib_add:

51 "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"

52 (is "?P n")

53 -- {* see \cite[page 280]{Concrete-Math} *}

54 proof (induct n rule: fib_induct)

55 show "?P 0" by simp

56 show "?P 1" by simp

57 fix n

58 have "fib (n + 2 + k + 1)

59 = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp

60 also assume "fib (n + k + 1)

61 = fib (k + 1) * fib (n + 1) + fib k * fib n"

62 (is " _ = ?R1")

63 also assume "fib (n + 1 + k + 1)

64 = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"

65 (is " _ = ?R2")

66 also have "?R1 + ?R2

67 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"

68 by (simp add: add_mult_distrib2)

69 finally show "?P (n + 2)" .

70 qed

72 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")

73 proof (induct n rule: fib_induct)

74 show "?P 0" by simp

75 show "?P 1" by simp

76 fix n

77 have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"

78 by simp

79 also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"

80 by (simp only: gcd_add2')

81 also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"

82 by (simp add: gcd_commute)

83 also assume "... = 1"

84 finally show "?P (n + 2)" .

85 qed

87 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n"

88 proof -

89 assume "0 < n"

90 then have "gcd (n * k + m) n = gcd n (m mod n)"

91 by (simp add: gcd_non_0 add_commute)

92 also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)

93 finally show ?thesis .

94 qed

96 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"

97 proof (cases m)

98 case 0

99 then show ?thesis by simp

100 next

101 case (Suc k)

102 then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"

103 by (simp add: gcd_commute)

104 also have "fib (n + k + 1)

105 = fib (k + 1) * fib (n + 1) + fib k * fib n"

106 by (rule fib_add)

107 also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"

108 by (simp add: gcd_mult_add)

109 also have "... = gcd (fib n) (fib (k + 1))"

110 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)

111 also have "... = gcd (fib m) (fib n)"

112 using Suc by (simp add: gcd_commute)

113 finally show ?thesis .

114 qed

116 lemma gcd_fib_diff:

117 assumes "m <= n"

118 shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"

119 proof -

120 have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"

121 by (simp add: gcd_fib_add)

122 also from `m <= n` have "n - m + m = n" by simp

123 finally show ?thesis .

124 qed

126 lemma gcd_fib_mod:

127 assumes "0 < m"

128 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"

129 proof (induct n rule: nat_less_induct)

130 case (1 n) note hyp = this

131 show ?case

132 proof -

133 have "n mod m = (if n < m then n else (n - m) mod m)"

134 by (rule mod_if)

135 also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"

136 proof (cases "n < m")

137 case True then show ?thesis by simp

138 next

139 case False then have "m <= n" by simp

140 from `0 < m` and False have "n - m < n" by simp

141 with hyp have "gcd (fib m) (fib ((n - m) mod m))

142 = gcd (fib m) (fib (n - m))" by simp

143 also have "... = gcd (fib m) (fib n)"

144 using `m <= n` by (rule gcd_fib_diff)

145 finally have "gcd (fib m) (fib ((n - m) mod m)) =

146 gcd (fib m) (fib n)" .

147 with False show ?thesis by simp

148 qed

149 finally show ?thesis .

150 qed

151 qed

154 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")

155 proof (induct m n rule: gcd_induct)

156 fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp

157 fix n :: nat assume n: "0 < n"

158 then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0)

159 also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"

160 also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)

161 also have "... = gcd (fib m) (fib n)" by (rule gcd_commute)

162 finally show "fib (gcd m n) = gcd (fib m) (fib n)" .

163 qed

165 end