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

src/HOL/Isar_examples/Fibonacci.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 16417 | 9bc16273c2d4 |

child 18153 | a084aa91f701 |

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

Constant "If" is now local

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

2 ID: $Id$

3 Author: Gertrud Bauer

4 Copyright 1999 Technische Universitaet Muenchen

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

7 tactic script by Lawrence C Paulson.

9 Fibonacci numbers: proofs of laws taken from

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

12 Concrete Mathematics.

13 (Addison-Wesley, 1989)

14 *)

16 header {* Fib and Gcd commute *}

18 theory Fibonacci imports Primes begin

20 text_raw {*

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

22 Larry Paulson. A few proofs of laws taken from

23 \cite{Concrete-Math}.}

24 *}

27 subsection {* Fibonacci numbers *}

29 consts fib :: "nat => nat"

30 recdef fib less_than

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

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

47 subsection {* Fib and gcd commute *}

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

51 lemma fib_add:

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

53 (is "?P n")

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

55 proof (induct n rule: fib_induct)

56 show "?P 0" by simp

57 show "?P 1" by simp

58 fix n

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

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

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

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

63 (is " _ = ?R1")

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

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

66 (is " _ = ?R2")

67 also have "?R1 + ?R2

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

69 by (simp add: add_mult_distrib2)

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

71 qed

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

74 proof (induct n rule: fib_induct)

75 show "?P 0" by simp

76 show "?P 1" by simp

77 fix n

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

79 by simp

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

81 by (simp only: gcd_add2')

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

83 by (simp add: gcd_commute)

84 also assume "... = 1"

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

86 qed

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

89 proof -

90 assume "0 < n"

91 hence "gcd (n * k + m, n) = gcd (n, m mod n)"

92 by (simp add: gcd_non_0 add_commute)

93 also have "... = gcd (m, n)" by (simp! add: gcd_non_0)

94 finally show ?thesis .

95 qed

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

98 proof (cases m)

99 assume "m = 0"

100 thus ?thesis by simp

101 next

102 fix k assume "m = Suc k"

103 hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"

104 by (simp add: gcd_commute)

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

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

107 by (rule fib_add)

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

109 by (simp add: gcd_mult_add)

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

111 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)

112 also have "... = gcd (fib m, fib n)"

113 by (simp! add: gcd_commute)

114 finally show ?thesis .

115 qed

117 lemma gcd_fib_diff:

118 "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"

119 proof -

120 assume "m <= n"

121 have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"

122 by (simp add: gcd_fib_add)

123 also have "n - m + m = n" by (simp!)

124 finally show ?thesis .

125 qed

127 lemma gcd_fib_mod:

128 "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"

129 proof -

130 assume m: "0 < m"

131 show ?thesis

132 proof (induct n rule: nat_less_induct)

133 fix n

134 assume hyp: "ALL ma. ma < n

135 --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"

136 show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"

137 proof -

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

139 by (rule mod_if)

140 also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"

141 proof cases

142 assume "n < m" thus ?thesis by simp

143 next

144 assume not_lt: "~ n < m" hence le: "m <= n" by simp

145 have "n - m < n" by (simp!)

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

147 = gcd (fib m, fib (n - m))" by simp

148 also from le have "... = gcd (fib m, fib n)"

149 by (rule gcd_fib_diff)

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

151 gcd (fib m, fib n)" .

152 with not_lt show ?thesis by simp

153 qed

154 finally show ?thesis .

155 qed

156 qed

157 qed

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

161 proof (induct m n rule: gcd_induct)

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

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

164 hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)

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

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

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

168 finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .

169 qed

171 end