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

src/HOL/Isar_Examples/Fibonacci.thy

author | haftmann |

Sat Nov 11 18:41:08 2017 +0000 (19 months ago) | |

changeset 67051 | e7e54a0b9197 |

parent 66453 | cc19f7ca2ed6 |

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

dedicated definition for coprimality

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

2 Author: Gertrud Bauer

3 Copyright 1999 Technische Universitaet Muenchen

5 The Fibonacci function. 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 section \<open>Fib and Gcd commute\<close>

17 theory Fibonacci

18 imports "HOL-Computational_Algebra.Primes"

19 begin

21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry

22 Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>

24 subsection \<open>Fibonacci numbers\<close>

26 fun fib :: "nat \<Rightarrow> nat"

27 where

28 "fib 0 = 0"

29 | "fib (Suc 0) = 1"

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

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

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

36 text \<open>Alternative induction rule.\<close>

38 theorem fib_induct: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"

39 for n :: nat

40 by (induct rule: fib.induct) simp_all

43 subsection \<open>Fib and gcd commute\<close>

45 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>

47 lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"

48 (is "?P n")

49 \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>

50 proof (induct n rule: fib_induct)

51 show "?P 0" by simp

52 show "?P 1" by simp

53 fix n

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

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

56 also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")

57 also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"

58 (is " _ = ?R2")

59 also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"

60 by (simp add: add_mult_distrib2)

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

62 qed

64 lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"

65 (is "?P n")

66 proof (induct n rule: fib_induct)

67 show "?P 0" by simp

68 show "?P 1" by simp

69 fix n

70 assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"

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

72 by simp

73 also have "\<dots> = fib (n + 2) + fib (n + 1)"

74 by simp

75 also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"

76 by (rule gcd_add2)

77 also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"

78 by (simp add: gcd.commute)

79 also have "\<dots> = 1"

80 using P by simp

81 finally show "?P (n + 2)"

82 by (simp add: coprime_iff_gcd_eq_1)

83 qed

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

86 proof -

87 assume "0 < n"

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

89 by (simp add: gcd_non_0_nat add.commute)

90 also from \<open>0 < n\<close> have "\<dots> = gcd m n"

91 by (simp add: gcd_non_0_nat)

92 finally show ?thesis .

93 qed

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

96 proof (cases m)

97 case 0

98 then show ?thesis by simp

99 next

100 case (Suc k)

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

102 by (simp add: gcd.commute)

103 also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"

104 by (rule fib_add)

105 also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"

106 by (simp add: gcd_mult_add)

107 also have "\<dots> = gcd (fib n) (fib (k + 1))"

108 using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]

109 by (simp add: ac_simps)

110 also have "\<dots> = gcd (fib m) (fib n)"

111 using Suc by (simp add: gcd.commute)

112 finally show ?thesis .

113 qed

115 lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m \<le> n"

116 proof -

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

118 by (simp add: gcd_fib_add)

119 also from \<open>m \<le> n\<close> have "n - m + m = n"

120 by simp

121 finally show ?thesis .

122 qed

124 lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"

125 proof (induct n rule: nat_less_induct)

126 case hyp: (1 n)

127 show ?case

128 proof -

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

130 by (rule mod_if)

131 also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"

132 proof (cases "n < m")

133 case True

134 then show ?thesis by simp

135 next

136 case False

137 then have "m \<le> n" by simp

138 from \<open>0 < m\<close> and False have "n - m < n"

139 by simp

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

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

142 also have "\<dots> = gcd (fib m) (fib n)"

143 using \<open>m \<le> n\<close> by (rule gcd_fib_diff)

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

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

146 with False show ?thesis by simp

147 qed

148 finally show ?thesis .

149 qed

150 qed

152 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"

153 (is "?P m n")

154 proof (induct m n rule: gcd_nat_induct)

155 fix m n :: nat

156 show "fib (gcd m 0) = gcd (fib m) (fib 0)"

157 by simp

158 assume n: "0 < n"

159 then have "gcd m n = gcd n (m mod n)"

160 by (simp add: gcd_non_0_nat)

161 also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"

162 also from n have "\<dots> = gcd (fib n) (fib m)"

163 by (rule gcd_fib_mod)

164 also have "\<dots> = gcd (fib m) (fib n)"

165 by (rule gcd.commute)

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

167 qed

169 end