src/HOL/Number_Theory/Fib.thy
 changeset 60527 eb431a5651fe parent 60526 fad653acf58f child 60688 01488b559910
```     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:41:33 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 23:40:46 2015 +0200
1.3 @@ -1,17 +1,12 @@
1.4  (*  Title:      HOL/Number_Theory/Fib.thy
1.5      Author:     Lawrence C. Paulson
1.7 -
1.8 -Defines the fibonacci function.
1.9 -
1.10 -The original "Fib" is due to Lawrence C. Paulson, and was adapted by
1.12  *)
1.13
1.14 -section \<open>Fib\<close>
1.15 +section \<open>The fibonacci function\<close>
1.16
1.17  theory Fib
1.18 -imports Main "../GCD" "../Binomial"
1.19 +imports Main GCD Binomial
1.20  begin
1.21
1.22
1.23 @@ -19,9 +14,10 @@
1.24
1.25  fun fib :: "nat \<Rightarrow> nat"
1.26  where
1.27 -    fib0: "fib 0 = 0"
1.28 -  | fib1: "fib (Suc 0) = 1"
1.29 -  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
1.30 +  fib0: "fib 0 = 0"
1.31 +| fib1: "fib (Suc 0) = 1"
1.32 +| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
1.33 +
1.34
1.35  subsection \<open>Basic Properties\<close>
1.36
1.37 @@ -41,6 +37,7 @@
1.38  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
1.39    by (induct n rule: fib.induct) (auto simp add: )
1.40
1.41 +
1.42  subsection \<open>A Few Elementary Results\<close>
1.43
1.44  text \<open>
1.45 @@ -49,12 +46,12 @@
1.46  \<close>
1.47
1.48  lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
1.49 -  by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
1.50 +  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
1.51
1.52  lemma fib_Cassini_nat:
1.53 -    "fib (Suc (Suc n)) * fib n =
1.54 -       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
1.55 -using fib_Cassini_int [of n] by auto
1.56 +  "fib (Suc (Suc n)) * fib n =
1.57 +     (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
1.58 +  using fib_Cassini_int [of n] by auto
1.59
1.60
1.61  subsection \<open>Law 6.111 of Concrete Mathematics\<close>
1.62 @@ -69,28 +66,26 @@
1.63    apply (simp add: gcd_commute_nat [of "fib m"])
1.64    apply (cases m)
1.66 -  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
1.67 +  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
1.69    done
1.70
1.71 -lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
1.72 -    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
1.73 +lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
1.75
1.76 -lemma gcd_fib_mod: "0 < m \<Longrightarrow>
1.77 -    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.78 +lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.79  proof (induct n rule: less_induct)
1.80    case (less n)
1.81 -  from less.prems have pos_m: "0 < m" .
1.82    show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.83    proof (cases "m < n")
1.84      case True
1.85      then have "m \<le> n" by auto
1.86 -    with pos_m have pos_n: "0 < n" by auto
1.87 -    with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
1.88 +    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
1.89 +    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
1.90      have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
1.91        by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
1.92      also have "\<dots> = gcd (fib m)  (fib (n - m))"
1.93 -      by (simp add: less.hyps diff pos_m)
1.94 +      by (simp add: less.hyps diff \<open>0 < m\<close>)
1.95      also have "\<dots> = gcd (fib m) (fib n)"
1.96        by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
1.97      finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
1.98 @@ -105,10 +100,10 @@
1.99      -- \<open>Law 6.111\<close>
1.100    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
1.101
1.102 -theorem fib_mult_eq_setsum_nat:
1.103 -    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.104 +theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.105    by (induct n rule: nat.induct) (auto simp add:  field_simps)
1.106
1.107 +
1.108  subsection \<open>Fibonacci and Binomial Coefficients\<close>
1.109
1.110  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.111 @@ -118,21 +113,22 @@
1.112      "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
1.113    by (rule trans [OF setsum.cong setsum_drop_zero]) auto
1.114
1.115 -lemma ne_diagonal_fib:
1.116 -   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
1.117 +lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
1.118  proof (induct n rule: fib.induct)
1.119 -  case 1 show ?case by simp
1.120 +  case 1
1.121 +  show ?case by simp
1.122  next
1.123 -  case 2 show ?case by simp
1.124 +  case 2
1.125 +  show ?case by simp
1.126  next
1.127    case (3 n)
1.128    have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
1.129          (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
1.130      by (rule setsum.cong) (simp_all add: choose_reduce_nat)
1.131 -  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.132 +  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.133                     (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"