The Fibonacci function. Original tactic script by Lawrence C Paulson.
Fibonacci numbers: proofs of laws taken from
R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. (Addison-Wesley, 1989)
*)
section \<open>Fib and Gcd commute\<close>
theory Fibonacci imports"HOL-Computational_Algebra.Primes" begin
text_raw\<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
Paulson. A few proofs of laws taken from\<^cite>\<open>"Concrete-Math"\<close>.\<close>\<close>
subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \ nat" where "fib 0 = 0"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "fib (Suc n) > 0" by (induct n rule: fib.induct) simp_all
text\<open>Alternative induction rule.\<close>
theorem fib_induct: "P 0 \ P 1 \ (\n. P (n + 1) \ P n \ P (n + 2)) \ P n" for n :: nat by (induct rule: fib.induct) simp_all
subsection \<open>Fib and gcd commute\<close>
text\<open>A few laws taken from \<^cite>\<open>"Concrete-Math"\<close>.\<close>
lemma gcd_mult_add: "(0::nat) < n \ gcd (n * k + m) n = gcd m n" proof - assume"0 < n" thenhave"gcd (n * k + m) n = gcd n (m mod n)" by (simp add: gcd_non_0_nat add.commute) alsofrom\<open>0 < n\<close> have "\<dots> = gcd m n" by (simp add: gcd_non_0_nat) finallyshow ?thesis . qed
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" proof (cases m) case 0 thenshow ?thesis by simp next case (Suc k) thenhave"gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" by (simp add: gcd.commute) alsohave"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" by (rule fib_add) alsohave"gcd \ (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" by (simp add: gcd_mult_add) alsohave"\ = gcd (fib n) (fib (k + 1))" using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)""fib k""fib n"] by (simp add: ac_simps) alsohave"\ = gcd (fib m) (fib n)" using Suc by (simp add: gcd.commute) finallyshow ?thesis . qed
lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"if"m \ n" proof - have"gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" by (simp add: gcd_fib_add) alsofrom\<open>m \<le> n\<close> have "n - m + m = n" by simp finallyshow ?thesis . qed
lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"if"0 < m" proof (induct n rule: nat_less_induct) case hyp: (1 n) show ?case proof - have"n mod m = (if n < m then n else (n - m) mod m)" by (rule mod_if) alsohave"gcd (fib m) (fib \) = gcd (fib m) (fib n)" proof (cases "n < m") case True thenshow ?thesis by simp next case False thenhave"m \ n" by simp from\<open>0 < m\<close> and False have "n - m < n" by simp with hyp have"gcd (fib m) (fib ((n - m) mod m))
= gcd (fib m) (fib (n - m))" by simp alsohave"\ = gcd (fib m) (fib n)" using\<open>m \<le> n\<close> by (rule gcd_fib_diff) finallyhave"gcd (fib m) (fib ((n - m) mod m)) =
gcd (fib m) (fib n)" . with False show ?thesis by simp qed finallyshow ?thesis . qed qed
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
(is"?P m n") proof (induct m n rule: gcd_nat_induct) fix m n :: nat show"fib (gcd m 0) = gcd (fib m) (fib 0)" by simp assume n: "0 < n" thenhave"gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat) alsoassume hyp: "fib \ = gcd (fib n) (fib (m mod n))" alsofrom n have"\ = gcd (fib n) (fib m)" by (rule gcd_fib_mod) alsohave"\ = gcd (fib m) (fib n)" by (rule gcd.commute) finallyshow"fib (gcd m n) = gcd (fib m) (fib n)" . qed
end
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
