--- a/src/HOL/Number_Theory/Fib.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Fri Jun 19 21:41:33 2015 +0200
@@ -8,14 +8,14 @@
Jeremy Avigad.
*)
-section {* Fib *}
+section \<open>Fib\<close>
theory Fib
imports Main "../GCD" "../Binomial"
begin
-subsection {* Fibonacci numbers *}
+subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
where
@@ -23,7 +23,7 @@
| fib1: "fib (Suc 0) = 1"
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
lemma fib_1 [simp]: "fib (1::nat) = 1"
by (metis One_nat_def fib1)
@@ -41,12 +41,12 @@
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
by (induct n rule: fib.induct) (auto simp add: )
-subsection {* A Few Elementary Results *}
+subsection \<open>A Few Elementary Results\<close>
-text {*
+text \<open>
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
much easier using integers, not natural numbers!
-*}
+\<close>
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
by (induction n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
@@ -57,7 +57,7 @@
using fib_Cassini_int [of n] by auto
-subsection {* Law 6.111 of Concrete Mathematics *}
+subsection \<open>Law 6.111 of Concrete Mathematics\<close>
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
apply (induct n rule: fib.induct)
@@ -86,13 +86,13 @@
case True
then have "m \<le> n" by auto
with pos_m have pos_n: "0 < n" by auto
- with pos_m `m < n` have diff: "n - m < n" by auto
+ with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
- by (simp add: mod_if [of n]) (insert `m < n`, auto)
+ by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
also have "\<dots> = gcd (fib m) (fib (n - m))"
by (simp add: less.hyps diff pos_m)
also have "\<dots> = gcd (fib m) (fib n)"
- by (simp add: gcd_fib_diff `m \<le> n`)
+ by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
case False
@@ -102,14 +102,14 @@
qed
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
- -- {* Law 6.111 *}
+ -- \<open>Law 6.111\<close>
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
theorem fib_mult_eq_setsum_nat:
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
by (induct n rule: nat.induct) (auto simp add: field_simps)
-subsection {* Fibonacci and Binomial Coefficients *}
+subsection \<open>Fibonacci and Binomial Coefficients\<close>
lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
by (induct n) auto