src/HOL/Number_Theory/Fib.thy
changeset 60526 fad653acf58f
parent 60141 833adf7db7d8
child 60527 eb431a5651fe
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:33:03 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:41:33 2015 +0200
     1.3 @@ -8,14 +8,14 @@
     1.4  Jeremy Avigad.
     1.5  *)
     1.6  
     1.7 -section {* Fib *}
     1.8 +section \<open>Fib\<close>
     1.9  
    1.10  theory Fib
    1.11  imports Main "../GCD" "../Binomial"
    1.12  begin
    1.13  
    1.14  
    1.15 -subsection {* Fibonacci numbers *}
    1.16 +subsection \<open>Fibonacci numbers\<close>
    1.17  
    1.18  fun fib :: "nat \<Rightarrow> nat"
    1.19  where
    1.20 @@ -23,7 +23,7 @@
    1.21    | fib1: "fib (Suc 0) = 1"
    1.22    | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
    1.23  
    1.24 -subsection {* Basic Properties *}
    1.25 +subsection \<open>Basic Properties\<close>
    1.26  
    1.27  lemma fib_1 [simp]: "fib (1::nat) = 1"
    1.28    by (metis One_nat_def fib1)
    1.29 @@ -41,12 +41,12 @@
    1.30  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
    1.31    by (induct n rule: fib.induct) (auto simp add: )
    1.32  
    1.33 -subsection {* A Few Elementary Results *}
    1.34 +subsection \<open>A Few Elementary Results\<close>
    1.35  
    1.36 -text {*
    1.37 +text \<open>
    1.38    \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
    1.39    much easier using integers, not natural numbers!
    1.40 -*}
    1.41 +\<close>
    1.42  
    1.43  lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
    1.44    by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
    1.45 @@ -57,7 +57,7 @@
    1.46  using fib_Cassini_int [of n] by auto
    1.47  
    1.48  
    1.49 -subsection {* Law 6.111 of Concrete Mathematics *}
    1.50 +subsection \<open>Law 6.111 of Concrete Mathematics\<close>
    1.51  
    1.52  lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
    1.53    apply (induct n rule: fib.induct)
    1.54 @@ -86,13 +86,13 @@
    1.55      case True
    1.56      then have "m \<le> n" by auto
    1.57      with pos_m have pos_n: "0 < n" by auto
    1.58 -    with pos_m `m < n` have diff: "n - m < n" by auto
    1.59 +    with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
    1.60      have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
    1.61 -      by (simp add: mod_if [of n]) (insert `m < n`, auto)
    1.62 +      by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
    1.63      also have "\<dots> = gcd (fib m)  (fib (n - m))"
    1.64        by (simp add: less.hyps diff pos_m)
    1.65      also have "\<dots> = gcd (fib m) (fib n)"
    1.66 -      by (simp add: gcd_fib_diff `m \<le> n`)
    1.67 +      by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
    1.68      finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
    1.69    next
    1.70      case False
    1.71 @@ -102,14 +102,14 @@
    1.72  qed
    1.73  
    1.74  lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
    1.75 -    -- {* Law 6.111 *}
    1.76 +    -- \<open>Law 6.111\<close>
    1.77    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
    1.78  
    1.79  theorem fib_mult_eq_setsum_nat:
    1.80      "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
    1.81    by (induct n rule: nat.induct) (auto simp add:  field_simps)
    1.82  
    1.83 -subsection {* Fibonacci and Binomial Coefficients *}
    1.84 +subsection \<open>Fibonacci and Binomial Coefficients\<close>
    1.85  
    1.86  lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
    1.87    by (induct n) auto