misc tuning and modernization;
authorwenzelm
Wed Apr 05 22:25:18 2017 +0200 (2017-04-05)
changeset 65393079a6f850c02
parent 65392 f365f61f2081
child 65394 faeccede9534
misc tuning and modernization;
src/HOL/Number_Theory/Fib.thy
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Wed Apr 05 22:00:44 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Wed Apr 05 22:25:18 2017 +0200
     1.3 @@ -14,29 +14,28 @@
     1.4  subsection \<open>Fibonacci numbers\<close>
     1.5  
     1.6  fun fib :: "nat \<Rightarrow> nat"
     1.7 -where
     1.8 -  fib0: "fib 0 = 0"
     1.9 -| fib1: "fib (Suc 0) = 1"
    1.10 -| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
    1.11 +  where
    1.12 +    fib0: "fib 0 = 0"
    1.13 +  | fib1: "fib (Suc 0) = 1"
    1.14 +  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
    1.15  
    1.16  
    1.17  subsection \<open>Basic Properties\<close>
    1.18  
    1.19 -lemma fib_1 [simp]: "fib (1::nat) = 1"
    1.20 +lemma fib_1 [simp]: "fib 1 = 1"
    1.21    by (metis One_nat_def fib1)
    1.22  
    1.23 -lemma fib_2 [simp]: "fib (2::nat) = 1"
    1.24 -  using fib.simps(3) [of 0]
    1.25 -  by (simp add: numeral_2_eq_2)
    1.26 +lemma fib_2 [simp]: "fib 2 = 1"
    1.27 +  using fib.simps(3) [of 0] by (simp add: numeral_2_eq_2)
    1.28  
    1.29  lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
    1.30    by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
    1.31  
    1.32 -lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
    1.33 +lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
    1.34    by (induct n rule: fib.induct) (auto simp add: field_simps)
    1.35  
    1.36  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
    1.37 -  by (induct n rule: fib.induct) (auto simp add: )
    1.38 +  by (induct n rule: fib.induct) auto
    1.39  
    1.40  
    1.41  subsection \<open>More efficient code\<close>
    1.42 @@ -45,21 +44,22 @@
    1.43    The naive approach is very inefficient since the branching recursion leads to many
    1.44    values of @{term fib} being computed multiple times. We can avoid this by ``remembering''
    1.45    the last two values in the sequence, yielding a tail-recursive version.
    1.46 -  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the 
    1.47 +  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
    1.48    time required to multiply two $n$-bit integers), but much better than the naive version,
    1.49    which is exponential.
    1.50  \<close>
    1.51  
    1.52 -fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.53 -  "gen_fib a b 0 = a"
    1.54 -| "gen_fib a b (Suc 0) = b"
    1.55 -| "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
    1.56 +fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    1.57 +  where
    1.58 +    "gen_fib a b 0 = a"
    1.59 +  | "gen_fib a b (Suc 0) = b"
    1.60 +  | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
    1.61  
    1.62  lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)"
    1.63 -  by (induction a b n rule: gen_fib.induct) simp_all
    1.64 -  
    1.65 +  by (induct a b n rule: gen_fib.induct) simp_all
    1.66 +
    1.67  lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)"
    1.68 -  by (induction m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
    1.69 +  by (induct m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
    1.70  
    1.71  lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n"
    1.72    using gen_fib_fib[of 0 n] by simp
    1.73 @@ -70,22 +70,22 @@
    1.74  subsection \<open>A Few Elementary Results\<close>
    1.75  
    1.76  text \<open>
    1.77 -  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
    1.78 +  \<^medskip> Concrete Mathematics, page 278: Cassini's identity.  The proof is
    1.79    much easier using integers, not natural numbers!
    1.80  \<close>
    1.81  
    1.82  lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
    1.83 -  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
    1.84 +  by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
    1.85  
    1.86  lemma fib_Cassini_nat:
    1.87    "fib (Suc (Suc n)) * fib n =
    1.88       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
    1.89 -  using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
    1.90 +  using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
    1.91  
    1.92  
    1.93  subsection \<open>Law 6.111 of Concrete Mathematics\<close>
    1.94  
    1.95 -lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
    1.96 +lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
    1.97    apply (induct n rule: fib.induct)
    1.98    apply auto
    1.99    apply (metis gcd_add1 add.commute)
   1.100 @@ -109,12 +109,12 @@
   1.101    proof (cases "m < n")
   1.102      case True
   1.103      then have "m \<le> n" by auto
   1.104 -    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
   1.105 -    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
   1.106 +    with \<open>0 < m\<close> have "0 < n" by auto
   1.107 +    with \<open>0 < m\<close> \<open>m < n\<close> have *: "n - m < n" by auto
   1.108      have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
   1.109 -      by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
   1.110 +      by (simp add: mod_if [of n]) (use \<open>m < n\<close> in auto)
   1.111      also have "\<dots> = gcd (fib m)  (fib (n - m))"
   1.112 -      by (simp add: less.hyps diff \<open>0 < m\<close>)
   1.113 +      by (simp add: less.hyps * \<open>0 < m\<close>)
   1.114      also have "\<dots> = gcd (fib m) (fib n)"
   1.115        by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
   1.116      finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   1.117 @@ -125,8 +125,7 @@
   1.118    qed
   1.119  qed
   1.120  
   1.121 -lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
   1.122 -    \<comment> \<open>Law 6.111\<close>
   1.123 +lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  \<comment> \<open>Law 6.111\<close>
   1.124    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
   1.125  
   1.126  theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   1.127 @@ -136,49 +135,55 @@
   1.128  subsection \<open>Closed form\<close>
   1.129  
   1.130  lemma fib_closed_form:
   1.131 -  defines "\<phi> \<equiv> (1 + sqrt 5) / (2::real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2::real)"
   1.132 -  shows   "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
   1.133 -proof (induction n rule: fib.induct)
   1.134 +  fixes \<phi> \<psi> :: real
   1.135 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.136 +    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
   1.137 +  shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
   1.138 +proof (induct n rule: fib.induct)
   1.139    fix n :: nat
   1.140    assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
   1.141    assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5"
   1.142    have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp
   1.143 -  also have "... = (\<phi>^n*(\<phi> + 1) - \<psi>^n*(\<psi> + 1)) / sqrt 5"
   1.144 +  also have "\<dots> = (\<phi>^n * (\<phi> + 1) - \<psi>^n * (\<psi> + 1)) / sqrt 5"
   1.145      by (simp add: IH1 IH2 field_simps)
   1.146    also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square)
   1.147    also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square)
   1.148 -  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"  
   1.149 +  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"
   1.150      by (simp add: power2_eq_square)
   1.151    finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" .
   1.152  qed (simp_all add: \<phi>_def \<psi>_def field_simps)
   1.153  
   1.154  lemma fib_closed_form':
   1.155 -  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
   1.156 +  fixes \<phi> \<psi> :: real
   1.157 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.158 +    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
   1.159    assumes "n > 0"
   1.160 -  shows   "fib n = round (\<phi> ^ n / sqrt 5)"
   1.161 +  shows "fib n = round (\<phi> ^ n / sqrt 5)"
   1.162  proof (rule sym, rule round_unique')
   1.163    have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5"
   1.164      by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs)
   1.165    also {
   1.166      from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1"
   1.167        by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt)
   1.168 -    also have "... < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
   1.169 +    also have "\<dots> < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
   1.170      finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps)
   1.171    }
   1.172    finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" .
   1.173  qed
   1.174  
   1.175  lemma fib_asymptotics:
   1.176 -  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)"
   1.177 -  shows   "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
   1.178 +  fixes \<phi> :: real
   1.179 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.180 +  shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
   1.181  proof -
   1.182 -  define \<psi> where "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
   1.183 +  define \<psi> :: real where "\<psi> \<equiv> (1 - sqrt 5) / 2"
   1.184    have "\<phi> > 1" by (simp add: \<phi>_def)
   1.185 -  hence A: "\<phi> \<noteq> 0" by auto
   1.186 +  then have *: "\<phi> \<noteq> 0" by auto
   1.187    have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0"
   1.188      by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos)
   1.189 -  hence "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" by (intro tendsto_diff tendsto_const)
   1.190 -  with A show ?thesis
   1.191 +  then have "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0"
   1.192 +    by (intro tendsto_diff tendsto_const)
   1.193 +  with * show ?thesis
   1.194      by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def])
   1.195  qed
   1.196  
   1.197 @@ -186,58 +191,72 @@
   1.198  subsection \<open>Divide-and-Conquer recurrence\<close>
   1.199  
   1.200  text \<open>
   1.201 -  The following divide-and-conquer recurrence allows for a more efficient computation 
   1.202 -  of Fibonacci numbers; however, it requires memoisation of values to be reasonably 
   1.203 +  The following divide-and-conquer recurrence allows for a more efficient computation
   1.204 +  of Fibonacci numbers; however, it requires memoisation of values to be reasonably
   1.205    efficient, cutting the number of values to be computed to logarithmically many instead of
   1.206 -  linearly many. The vast majority of the computation time is then actually spent on the 
   1.207 +  linearly many. The vast majority of the computation time is then actually spent on the
   1.208    multiplication, since the output number is exponential in the input number.
   1.209  \<close>
   1.210  
   1.211  lemma fib_rec_odd:
   1.212 -  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
   1.213 -  shows   "fib (Suc (2*n)) = fib n^2 + fib (Suc n)^2"
   1.214 +  fixes \<phi> \<psi> :: real
   1.215 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.216 +    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
   1.217 +  shows "fib (Suc (2 * n)) = fib n^2 + fib (Suc n)^2"
   1.218  proof -
   1.219    have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5"
   1.220      by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square)
   1.221 -  also have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = 
   1.222 -    \<phi>^(2*n) + \<psi>^(2*n) - 2*(\<phi>*\<psi>)^n + \<phi>^(2*n+2) + \<psi>^(2*n+2) - 2*(\<phi>*\<psi>)^(n+1)" (is "_ = ?A")
   1.223 -      by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
   1.224 -  also have "\<phi> * \<psi> = -1" by (simp add: \<phi>_def \<psi>_def field_simps)
   1.225 -  hence "?A = \<phi>^(2*n+1) * (\<phi> + inverse \<phi>) + \<psi>^(2*n+1) * (\<psi> + inverse \<psi>)" 
   1.226 +  also
   1.227 +  let ?A = "\<phi>^(2 * n) + \<psi>^(2 * n) - 2*(\<phi> * \<psi>)^n + \<phi>^(2 * n + 2) + \<psi>^(2 * n + 2) - 2*(\<phi> * \<psi>)^(n + 1)"
   1.228 +  have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = ?A"
   1.229 +    by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
   1.230 +  also have "\<phi> * \<psi> = -1"
   1.231 +    by (simp add: \<phi>_def \<psi>_def field_simps)
   1.232 +  then have "?A = \<phi>^(2 * n + 1) * (\<phi> + inverse \<phi>) + \<psi>^(2 * n + 1) * (\<psi> + inverse \<psi>)"
   1.233      by (auto simp: field_simps power2_eq_square)
   1.234 -  also have "1 + sqrt 5 > 0" by (auto intro: add_pos_pos)
   1.235 -  hence "\<phi> + inverse \<phi> = sqrt 5" by (simp add: \<phi>_def field_simps)
   1.236 -  also have "\<psi> + inverse \<psi> = -sqrt 5" by (simp add: \<psi>_def field_simps)
   1.237 -  also have "(\<phi> ^ (2*n+1) * sqrt 5 + \<psi> ^ (2*n+1)* - sqrt 5) / 5 =
   1.238 -               (\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * (sqrt 5 / 5)" by (simp add: field_simps)
   1.239 -  also have "sqrt 5 / 5 = inverse (sqrt 5)" by (simp add: field_simps)
   1.240 -  also have "(\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * ... = of_nat (fib (Suc (2*n)))"
   1.241 +  also have "1 + sqrt 5 > 0"
   1.242 +    by (auto intro: add_pos_pos)
   1.243 +  then have "\<phi> + inverse \<phi> = sqrt 5"
   1.244 +    by (simp add: \<phi>_def field_simps)
   1.245 +  also have "\<psi> + inverse \<psi> = -sqrt 5"
   1.246 +    by (simp add: \<psi>_def field_simps)
   1.247 +  also have "(\<phi> ^ (2 * n + 1) * sqrt 5 + \<psi> ^ (2 * n + 1) * - sqrt 5) / 5 =
   1.248 +    (\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * (sqrt 5 / 5)"
   1.249 +    by (simp add: field_simps)
   1.250 +  also have "sqrt 5 / 5 = inverse (sqrt 5)"
   1.251 +    by (simp add: field_simps)
   1.252 +  also have "(\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * \<dots> = of_nat (fib (Suc (2 * n)))"
   1.253      by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse)
   1.254 -  finally show ?thesis by (simp only: of_nat_eq_iff)
   1.255 +  finally show ?thesis
   1.256 +    by (simp only: of_nat_eq_iff)
   1.257  qed
   1.258  
   1.259 -lemma fib_rec_even: "fib (2*n) = (fib (n - 1) + fib (n + 1)) * fib n"
   1.260 -proof (induction n)
   1.261 +lemma fib_rec_even: "fib (2 * n) = (fib (n - 1) + fib (n + 1)) * fib n"
   1.262 +proof (induct n)
   1.263 +  case 0
   1.264 +  then show ?case by simp
   1.265 +next
   1.266    case (Suc n)
   1.267    let ?rfib = "\<lambda>x. real (fib x)"
   1.268 -  have "2 * (Suc n) = Suc (Suc (2*n))" by simp
   1.269 -  also have "real (fib ...) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n" 
   1.270 +  have "2 * (Suc n) = Suc (Suc (2 * n))" by simp
   1.271 +  also have "real (fib \<dots>) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n"
   1.272      by (simp add: fib_rec_odd Suc)
   1.273    also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n"
   1.274      by (cases n) simp_all
   1.275 -  also have "?rfib n^2 + ?rfib (Suc n)^2 + ... = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
   1.276 +  also have "?rfib n^2 + ?rfib (Suc n)^2 + \<dots> = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
   1.277      by (simp add: algebra_simps power2_eq_square)
   1.278 -  also have "... = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
   1.279 +  also have "\<dots> = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
   1.280    finally show ?case by (simp only: of_nat_eq_iff)
   1.281 -qed simp
   1.282 +qed
   1.283  
   1.284 -lemma fib_rec_even': "fib (2*n) = (2*fib (n - 1) + fib n) * fib n"
   1.285 +lemma fib_rec_even': "fib (2 * n) = (2 * fib (n - 1) + fib n) * fib n"
   1.286    by (subst fib_rec_even, cases n) simp_all
   1.287  
   1.288  lemma fib_rec:
   1.289 -  "fib n = (if n = 0 then 0 else if n = 1 then 1 else
   1.290 -            if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
   1.291 -            else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
   1.292 +  "fib n =
   1.293 +    (if n = 0 then 0 else if n = 1 then 1
   1.294 +     else if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
   1.295 +     else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
   1.296    by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def)
   1.297  
   1.298  
   1.299 @@ -247,7 +266,8 @@
   1.300    by (induct n) auto
   1.301  
   1.302  lemma sum_choose_drop_zero:
   1.303 -    "(\<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.304 +  "(\<Sum>k = 0..Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) =
   1.305 +    (\<Sum>j = 0..n. (n-j) choose j)"
   1.306    by (rule trans [OF sum.cong sum_drop_zero]) auto
   1.307  
   1.308  lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
   1.309 @@ -260,17 +280,16 @@
   1.310  next
   1.311    case (3 n)
   1.312    have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
   1.313 -        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
   1.314 +     (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k = 0 then 0 else (Suc n - k choose (k - 1))))"
   1.315      by (rule sum.cong) (simp_all add: choose_reduce_nat)
   1.316 -  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
   1.317 -                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
   1.318 +  also have "\<dots> =
   1.319 +    (\<Sum>k = 0..Suc n. Suc n - k choose k) +
   1.320 +    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
   1.321      by (simp add: sum.distrib)
   1.322 -  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
   1.323 -                   (\<Sum>j = 0..n. n - j choose j)"
   1.324 +  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) + (\<Sum>j = 0..n. n - j choose j)"
   1.325      by (metis sum_choose_drop_zero)
   1.326    finally show ?case using 3
   1.327      by simp
   1.328  qed
   1.329  
   1.330  end
   1.331 -