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

src/HOL/Isar_Examples/Fibonacci.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 57512 | cc97b347b301 |

child 58614 | 7338eb25226c |

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

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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 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 fixes n :: nat

44 shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"

45 by (induct rule: fib.induct) simp_all

48 subsection {* Fib and gcd commute *}

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

52 lemma fib_add:

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

54 (is "?P n")

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

56 proof (induct n rule: fib_induct)

57 show "?P 0" by simp

58 show "?P 1" by simp

59 fix n

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

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

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

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

64 (is " _ = ?R1")

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

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

67 (is " _ = ?R2")

68 also have "?R1 + ?R2

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

70 by (simp add: add_mult_distrib2)

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

72 qed

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

75 proof (induct n rule: fib_induct)

76 show "?P 0" by simp

77 show "?P 1" by simp

78 fix n

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

80 by simp

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

82 by simp

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

84 by (rule gcd_add2_nat)

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

86 by (simp add: gcd_commute_nat)

87 also assume "\<dots> = 1"

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

89 qed

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

92 proof -

93 assume "0 < n"

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

95 by (simp add: gcd_non_0_nat add.commute)

96 also from `0 < n` have "\<dots> = gcd m n"

97 by (simp add: gcd_non_0_nat)

98 finally show ?thesis .

99 qed

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

102 proof (cases m)

103 case 0

104 then show ?thesis by simp

105 next

106 case (Suc k)

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

108 by (simp add: gcd_commute_nat)

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

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

111 by (rule fib_add)

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

113 by (simp add: gcd_mult_add)

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

115 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)

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

117 using Suc by (simp add: gcd_commute_nat)

118 finally show ?thesis .

119 qed

121 lemma gcd_fib_diff:

122 assumes "m \<le> n"

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

124 proof -

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

126 by (simp add: gcd_fib_add)

127 also from `m \<le> n` have "n - m + m = n"

128 by simp

129 finally show ?thesis .

130 qed

132 lemma gcd_fib_mod:

133 assumes "0 < m"

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

135 proof (induct n rule: nat_less_induct)

136 case (1 n) note hyp = this

137 show ?case

138 proof -

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

140 by (rule mod_if)

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

142 proof (cases "n < m")

143 case True

144 then show ?thesis by simp

145 next

146 case False

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

148 from `0 < m` and False have "n - m < n"

149 by simp

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

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

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

153 using `m \<le> n` by (rule gcd_fib_diff)

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

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

156 with False show ?thesis by simp

157 qed

158 finally show ?thesis .

159 qed

160 qed

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

163 proof (induct m n rule: gcd_nat_induct)

164 fix m

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

166 by simp

167 fix n :: nat

168 assume n: "0 < n"

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

170 by (simp add: gcd_non_0_nat)

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

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

173 by (rule gcd_fib_mod)

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

175 by (rule gcd_commute_nat)

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

177 qed

179 end