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.6      Author:     Jeremy Avigad
     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.11 -Jeremy Avigad.
    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.65    apply (auto simp add: fib_add)
    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.68 +    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
    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.74    by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
    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)))"
   1.134      by (simp add: setsum.distrib)
   1.135 -  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
   1.136 +  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
   1.137                     (\<Sum>j = 0..n. n - j choose j)"
   1.138      by (metis setsum_choose_drop_zero)
   1.139    finally show ?case using 3