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

src/HOL/Isar_Examples/Fibonacci.thy

author | nipkow |

Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) | |

changeset 46372 | 6fa9cdb8b850 |

parent 37672 | 645eb9fec794 |

child 54892 | 64c2d4f8d981 |

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

added "'a rel"

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 "../Number_Theory/Primes"

19 begin

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

22 script by Larry Paulson. A few proofs of laws taken from

23 \cite{Concrete-Math}.} *}

26 declare One_nat_def [simp]

29 subsection {* Fibonacci numbers *}

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

32 "fib 0 = 0"

33 | "fib (Suc 0) = 1"

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

36 lemma [simp]: "fib (Suc n) > 0"

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

40 text {* Alternative induction rule. *}

42 theorem fib_induct:

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

44 by (induct rule: fib.induct) simp_all

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 "... = fib (n + 2) + fib (n + 1)" by simp

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

82 by (rule gcd_add2_nat)

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

84 by (simp add: gcd_commute_nat)

85 also assume "... = 1"

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

87 qed

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

90 proof -

91 assume "0 < n"

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

93 by (simp add: gcd_non_0_nat add_commute)

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

95 finally show ?thesis .

96 qed

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

99 proof (cases m)

100 case 0

101 then show ?thesis by simp

102 next

103 case (Suc k)

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

105 by (simp add: gcd_commute_nat)

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

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

108 by (rule fib_add)

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

110 by (simp add: gcd_mult_add)

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

112 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)

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

114 using Suc by (simp add: gcd_commute_nat)

115 finally show ?thesis .

116 qed

118 lemma gcd_fib_diff:

119 assumes "m <= n"

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

121 proof -

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

123 by (simp add: gcd_fib_add)

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

125 finally show ?thesis .

126 qed

128 lemma gcd_fib_mod:

129 assumes "0 < m"

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

131 proof (induct n rule: nat_less_induct)

132 case (1 n) note hyp = this

133 show ?case

134 proof -

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

136 by (rule mod_if)

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

138 proof (cases "n < m")

139 case True then show ?thesis by simp

140 next

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

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

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

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

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

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

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

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

149 with False show ?thesis by simp

150 qed

151 finally show ?thesis .

152 qed

153 qed

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

156 proof (induct m n rule: gcd_nat_induct)

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

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

159 then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat)

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

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

162 also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)

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

164 qed

166 end