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

src/HOL/Isar_examples/Fibonacci.thy

author | krauss |

Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) | |

changeset 21512 | 3786eb1b69d6 |

parent 18241 | afdba6b3e383 |

child 27366 | d0cda1ea705e |

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

Lemma "fundef_default_value" uses predicate instead of set.

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_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