68 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" |
68 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" |
69 by (simp add: add_mult_distrib2) |
69 by (simp add: add_mult_distrib2) |
70 finally show "?P (n + 2)" . |
70 finally show "?P (n + 2)" . |
71 qed |
71 qed |
72 |
72 |
73 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n") |
73 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n") |
74 proof (induct n rule: fib_induct) |
74 proof (induct n rule: fib_induct) |
75 show "?P 0" by simp |
75 show "?P 0" by simp |
76 show "?P 1" by simp |
76 show "?P 1" by simp |
77 fix n |
77 fix n |
78 have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" |
78 have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" |
79 by simp |
79 by simp |
80 also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))" |
80 also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))" |
81 by (simp only: gcd_add2') |
81 by (simp only: gcd_add2') |
82 also have "... = gcd (fib (n + 1), fib (n + 1 + 1))" |
82 also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))" |
83 by (simp add: gcd_commute) |
83 by (simp add: gcd_commute) |
84 also assume "... = 1" |
84 also assume "... = 1" |
85 finally show "?P (n + 2)" . |
85 finally show "?P (n + 2)" . |
86 qed |
86 qed |
87 |
87 |
88 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)" |
88 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n" |
89 proof - |
89 proof - |
90 assume "0 < n" |
90 assume "0 < n" |
91 then have "gcd (n * k + m, n) = gcd (n, m mod n)" |
91 then have "gcd (n * k + m) n = gcd n (m mod n)" |
92 by (simp add: gcd_non_0 add_commute) |
92 by (simp add: gcd_non_0 add_commute) |
93 also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0) |
93 also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0) |
94 finally show ?thesis . |
94 finally show ?thesis . |
95 qed |
95 qed |
96 |
96 |
97 lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" |
97 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
98 proof (cases m) |
98 proof (cases m) |
99 case 0 |
99 case 0 |
100 then show ?thesis by simp |
100 then show ?thesis by simp |
101 next |
101 next |
102 case (Suc k) |
102 case (Suc k) |
103 then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))" |
103 then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" |
104 by (simp add: gcd_commute) |
104 by (simp add: gcd_commute) |
105 also have "fib (n + k + 1) |
105 also have "fib (n + k + 1) |
106 = fib (k + 1) * fib (n + 1) + fib k * fib n" |
106 = fib (k + 1) * fib (n + 1) + fib k * fib n" |
107 by (rule fib_add) |
107 by (rule fib_add) |
108 also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))" |
108 also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" |
109 by (simp add: gcd_mult_add) |
109 by (simp add: gcd_mult_add) |
110 also have "... = gcd (fib n, fib (k + 1))" |
110 also have "... = gcd (fib n) (fib (k + 1))" |
111 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
111 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
112 also have "... = gcd (fib m, fib n)" |
112 also have "... = gcd (fib m) (fib n)" |
113 using Suc by (simp add: gcd_commute) |
113 using Suc by (simp add: gcd_commute) |
114 finally show ?thesis . |
114 finally show ?thesis . |
115 qed |
115 qed |
116 |
116 |
117 lemma gcd_fib_diff: |
117 lemma gcd_fib_diff: |
118 assumes "m <= n" |
118 assumes "m <= n" |
119 shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" |
119 shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
120 proof - |
120 proof - |
121 have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))" |
121 have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" |
122 by (simp add: gcd_fib_add) |
122 by (simp add: gcd_fib_add) |
123 also from `m <= n` have "n - m + m = n" by simp |
123 also from `m <= n` have "n - m + m = n" by simp |
124 finally show ?thesis . |
124 finally show ?thesis . |
125 qed |
125 qed |
126 |
126 |
127 lemma gcd_fib_mod: |
127 lemma gcd_fib_mod: |
128 assumes "0 < m" |
128 assumes "0 < m" |
129 shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
129 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
130 proof (induct n rule: nat_less_induct) |
130 proof (induct n rule: nat_less_induct) |
131 case (1 n) note hyp = this |
131 case (1 n) note hyp = this |
132 show ?case |
132 show ?case |
133 proof - |
133 proof - |
134 have "n mod m = (if n < m then n else (n - m) mod m)" |
134 have "n mod m = (if n < m then n else (n - m) mod m)" |
135 by (rule mod_if) |
135 by (rule mod_if) |
136 also have "gcd (fib m, fib ...) = gcd (fib m, fib n)" |
136 also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)" |
137 proof (cases "n < m") |
137 proof (cases "n < m") |
138 case True then show ?thesis by simp |
138 case True then show ?thesis by simp |
139 next |
139 next |
140 case False then have "m <= n" by simp |
140 case False then have "m <= n" by simp |
141 from `0 < m` and False have "n - m < n" by simp |
141 from `0 < m` and False have "n - m < n" by simp |
142 with hyp have "gcd (fib m, fib ((n - m) mod m)) |
142 with hyp have "gcd (fib m) (fib ((n - m) mod m)) |
143 = gcd (fib m, fib (n - m))" by simp |
143 = gcd (fib m) (fib (n - m))" by simp |
144 also have "... = gcd (fib m, fib n)" |
144 also have "... = gcd (fib m) (fib n)" |
145 using `m <= n` by (rule gcd_fib_diff) |
145 using `m <= n` by (rule gcd_fib_diff) |
146 finally have "gcd (fib m, fib ((n - m) mod m)) = |
146 finally have "gcd (fib m) (fib ((n - m) mod m)) = |
147 gcd (fib m, fib n)" . |
147 gcd (fib m) (fib n)" . |
148 with False show ?thesis by simp |
148 with False show ?thesis by simp |
149 qed |
149 qed |
150 finally show ?thesis . |
150 finally show ?thesis . |
151 qed |
151 qed |
152 qed |
152 qed |
153 |
153 |
154 |
154 |
155 theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n") |
155 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") |
156 proof (induct m n rule: gcd_induct) |
156 proof (induct m n rule: gcd_induct) |
157 fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp |
157 fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp |
158 fix n :: nat assume n: "0 < n" |
158 fix n :: nat assume n: "0 < n" |
159 then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0) |
159 then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0) |
160 also assume hyp: "fib ... = gcd (fib n, fib (m mod n))" |
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) |
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) |
162 also have "... = gcd (fib m) (fib n)" by (rule gcd_commute) |
163 finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" . |
163 finally show "fib (gcd m n) = gcd (fib m) (fib n)" . |
164 qed |
164 qed |
165 |
165 |
166 end |
166 end |