misc tuning and modernization;
authorwenzelm
Wed Jul 13 21:23:05 2016 +0200 (2016-07-13)
changeset 634876e29fb72e659
parent 63486 a4668ec480ad
child 63488 a7c5074a0251
misc tuning and modernization;
src/HOL/Library/Stirling.thy
     1.1 --- a/src/HOL/Library/Stirling.thy	Wed Jul 13 20:48:18 2016 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Wed Jul 13 21:23:05 2016 +0200
     1.3 @@ -1,5 +1,9 @@
     1.4 -(* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen
     1.5 -            with contributions by Lukas Bulwahn and Manuel Eberl*)
     1.6 +(*  Title:      HOL/Library/Stirling.thy
     1.7 +    Author:     Amine Chaieb
     1.8 +    Author:     Florian Haftmann
     1.9 +    Author:     Lukas Bulwahn
    1.10 +    Author:     Manuel Eberl
    1.11 +*)
    1.12  
    1.13  section \<open>Stirling numbers of first and second kind\<close>
    1.14  
    1.15 @@ -10,102 +14,105 @@
    1.16  subsection \<open>Stirling numbers of the second kind\<close>
    1.17  
    1.18  fun Stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.19 -where
    1.20 -  "Stirling 0 0 = 1"
    1.21 -| "Stirling 0 (Suc k) = 0"
    1.22 -| "Stirling (Suc n) 0 = 0"
    1.23 -| "Stirling (Suc n) (Suc k) = Suc k * Stirling n (Suc k) + Stirling n k"
    1.24 +  where
    1.25 +    "Stirling 0 0 = 1"
    1.26 +  | "Stirling 0 (Suc k) = 0"
    1.27 +  | "Stirling (Suc n) 0 = 0"
    1.28 +  | "Stirling (Suc n) (Suc k) = Suc k * Stirling n (Suc k) + Stirling n k"
    1.29  
    1.30 -lemma Stirling_1 [simp]:
    1.31 -  "Stirling (Suc n) (Suc 0) = 1"
    1.32 +lemma Stirling_1 [simp]: "Stirling (Suc n) (Suc 0) = 1"
    1.33    by (induct n) simp_all
    1.34  
    1.35 -lemma Stirling_less [simp]:
    1.36 -  "n < k \<Longrightarrow> Stirling n k = 0"
    1.37 +lemma Stirling_less [simp]: "n < k \<Longrightarrow> Stirling n k = 0"
    1.38    by (induct n k rule: Stirling.induct) simp_all
    1.39  
    1.40 -lemma Stirling_same [simp]:
    1.41 -  "Stirling n n = 1"
    1.42 +lemma Stirling_same [simp]: "Stirling n n = 1"
    1.43    by (induct n) simp_all
    1.44  
    1.45 -lemma Stirling_2_2:
    1.46 -  "Stirling (Suc (Suc n)) (Suc (Suc 0)) = 2 ^ Suc n - 1"
    1.47 +lemma Stirling_2_2: "Stirling (Suc (Suc n)) (Suc (Suc 0)) = 2 ^ Suc n - 1"
    1.48  proof (induct n)
    1.49 -  case 0 then show ?case by simp
    1.50 +  case 0
    1.51 +  then show ?case by simp
    1.52  next
    1.53    case (Suc n)
    1.54    have "Stirling (Suc (Suc (Suc n))) (Suc (Suc 0)) =
    1.55 -    2 * Stirling (Suc (Suc n)) (Suc (Suc 0)) + Stirling (Suc (Suc n)) (Suc 0)" by simp
    1.56 +      2 * Stirling (Suc (Suc n)) (Suc (Suc 0)) + Stirling (Suc (Suc n)) (Suc 0)"
    1.57 +    by simp
    1.58    also have "\<dots> = 2 * (2 ^ Suc n - 1) + 1"
    1.59      by (simp only: Suc Stirling_1)
    1.60    also have "\<dots> = 2 ^ Suc (Suc n) - 1"
    1.61    proof -
    1.62 -    have "(2::nat) ^ Suc n - 1 > 0" by (induct n) simp_all
    1.63 -    then have "2 * ((2::nat) ^ Suc n - 1) > 0" by simp
    1.64 -    then have "2 \<le> 2 * ((2::nat) ^ Suc n)" by simp
    1.65 +    have "(2::nat) ^ Suc n - 1 > 0"
    1.66 +      by (induct n) simp_all
    1.67 +    then have "2 * ((2::nat) ^ Suc n - 1) > 0"
    1.68 +      by simp
    1.69 +    then have "2 \<le> 2 * ((2::nat) ^ Suc n)"
    1.70 +      by simp
    1.71      with add_diff_assoc2 [of 2 "2 * 2 ^ Suc n" 1]
    1.72 -      have "2 * 2 ^ Suc n - 2 + (1::nat) = 2 * 2 ^ Suc n + 1 - 2" .
    1.73 -    then show ?thesis by (simp add: nat_distrib)
    1.74 +    have "2 * 2 ^ Suc n - 2 + (1::nat) = 2 * 2 ^ Suc n + 1 - 2" .
    1.75 +    then show ?thesis
    1.76 +      by (simp add: nat_distrib)
    1.77    qed
    1.78    finally show ?case by simp
    1.79  qed
    1.80  
    1.81 -lemma Stirling_2:
    1.82 -  "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1"
    1.83 +lemma Stirling_2: "Stirling (Suc n) (Suc (Suc 0)) = 2 ^ n - 1"
    1.84    using Stirling_2_2 by (cases n) simp_all
    1.85  
    1.86 +
    1.87  subsection \<open>Stirling numbers of the first kind\<close>
    1.88  
    1.89  fun stirling :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.90 -where
    1.91 -  "stirling 0 0 = 1"
    1.92 -| "stirling 0 (Suc k) = 0"
    1.93 -| "stirling (Suc n) 0 = 0"
    1.94 -| "stirling (Suc n) (Suc k) = n * stirling n (Suc k) + stirling n k"
    1.95 +  where
    1.96 +    "stirling 0 0 = 1"
    1.97 +  | "stirling 0 (Suc k) = 0"
    1.98 +  | "stirling (Suc n) 0 = 0"
    1.99 +  | "stirling (Suc n) (Suc k) = n * stirling n (Suc k) + stirling n k"
   1.100  
   1.101  lemma stirling_0 [simp]: "n > 0 \<Longrightarrow> stirling n 0 = 0"
   1.102    by (cases n) simp_all
   1.103  
   1.104 -lemma stirling_less [simp]:
   1.105 -  "n < k \<Longrightarrow> stirling n k = 0"
   1.106 +lemma stirling_less [simp]: "n < k \<Longrightarrow> stirling n k = 0"
   1.107    by (induct n k rule: stirling.induct) simp_all
   1.108  
   1.109 -lemma stirling_same [simp]:
   1.110 -  "stirling n n = 1"
   1.111 +lemma stirling_same [simp]: "stirling n n = 1"
   1.112    by (induct n) simp_all
   1.113  
   1.114 -lemma stirling_Suc_n_1:
   1.115 -  "stirling (Suc n) (Suc 0) = fact n"
   1.116 +lemma stirling_Suc_n_1: "stirling (Suc n) (Suc 0) = fact n"
   1.117    by (induct n) auto
   1.118  
   1.119 -lemma stirling_Suc_n_n:
   1.120 -  shows "stirling (Suc n) n = Suc n choose 2"
   1.121 -by (induct n) (auto simp add: numerals(2))
   1.122 +lemma stirling_Suc_n_n: "stirling (Suc n) n = Suc n choose 2"
   1.123 +  by (induct n) (auto simp add: numerals(2))
   1.124  
   1.125  lemma stirling_Suc_n_2:
   1.126    assumes "n \<ge> Suc 0"
   1.127    shows "stirling (Suc n) 2 = (\<Sum>k=1..n. fact n div k)"
   1.128 -using assms
   1.129 +  using assms
   1.130  proof (induct n)
   1.131 -  case 0 from this show ?case by simp
   1.132 +  case 0
   1.133 +  then show ?case by simp
   1.134  next
   1.135    case (Suc n)
   1.136    show ?case
   1.137    proof (cases n)
   1.138 -    case 0 from this show ?thesis by (simp add: numerals(2))
   1.139 +    case 0
   1.140 +    then show ?thesis
   1.141 +      by (simp add: numerals(2))
   1.142    next
   1.143      case Suc
   1.144 -    from this have geq1: "Suc 0 \<le> n" by simp
   1.145 +    then have geq1: "Suc 0 \<le> n"
   1.146 +      by simp
   1.147      have "stirling (Suc (Suc n)) 2 = Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0)"
   1.148        by (simp only: stirling.simps(4)[of "Suc n"] numerals(2))
   1.149 -    also have "... = Suc n * (\<Sum>k=1..n. fact n div k) + fact n"
   1.150 +    also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + fact n"
   1.151        using Suc.hyps[OF geq1]
   1.152        by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult)
   1.153 -    also have "... = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
   1.154 +    also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
   1.155        by (metis nat.distinct(1) nonzero_mult_divide_cancel_left)
   1.156 -    also have "... = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
   1.157 +    also have "\<dots> = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
   1.158        by (simp add: setsum_right_distrib div_mult_swap dvd_fact)
   1.159 -    also have "... = (\<Sum>k=1..Suc n. fact (Suc n) div k)" by simp
   1.160 +    also have "\<dots> = (\<Sum>k=1..Suc n. fact (Suc n) div k)"
   1.161 +      by simp
   1.162      finally show ?thesis .
   1.163    qed
   1.164  qed
   1.165 @@ -113,52 +120,60 @@
   1.166  lemma of_nat_stirling_Suc_n_2:
   1.167    assumes "n \<ge> Suc 0"
   1.168    shows "(of_nat (stirling (Suc n) 2)::'a::field_char_0) = fact n * (\<Sum>k=1..n. (1 / of_nat k))"
   1.169 -using assms
   1.170 +  using assms
   1.171  proof (induct n)
   1.172 -  case 0 from this show ?case by simp
   1.173 +  case 0
   1.174 +  then show ?case by simp
   1.175  next
   1.176    case (Suc n)
   1.177    show ?case
   1.178    proof (cases n)
   1.179 -    case 0 from this show ?thesis by (auto simp add: numerals(2))
   1.180 +    case 0
   1.181 +    then show ?thesis
   1.182 +      by (auto simp add: numerals(2))
   1.183    next
   1.184      case Suc
   1.185 -    from this have geq1: "Suc 0 \<le> n" by simp
   1.186 +    then have geq1: "Suc 0 \<le> n"
   1.187 +      by simp
   1.188      have "(of_nat (stirling (Suc (Suc n)) 2)::'a) =
   1.189 -      of_nat (Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0))"
   1.190 +        of_nat (Suc n * stirling (Suc n) 2 + stirling (Suc n) (Suc 0))"
   1.191        by (simp only: stirling.simps(4)[of "Suc n"] numerals(2))
   1.192 -    also have "... = of_nat (Suc n) * (fact n * (\<Sum>k = 1..n. 1 / of_nat k)) + fact n"
   1.193 +    also have "\<dots> = of_nat (Suc n) * (fact n * (\<Sum>k = 1..n. 1 / of_nat k)) + fact n"
   1.194        using Suc.hyps[OF geq1]
   1.195        by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult)
   1.196 -    also have "... = fact (Suc n) * (\<Sum>k = 1..n. 1 / of_nat k) + fact (Suc n) * (1 / of_nat (Suc n))"
   1.197 +    also have "\<dots> = fact (Suc n) * (\<Sum>k = 1..n. 1 / of_nat k) + fact (Suc n) * (1 / of_nat (Suc n))"
   1.198        using of_nat_neq_0 by auto
   1.199 -    also have "... = fact (Suc n) * (\<Sum>k = 1..Suc n. 1 / of_nat k)"
   1.200 +    also have "\<dots> = fact (Suc n) * (\<Sum>k = 1..Suc n. 1 / of_nat k)"
   1.201        by (simp add: distrib_left)
   1.202      finally show ?thesis .
   1.203    qed
   1.204  qed
   1.205  
   1.206 -lemma setsum_stirling:
   1.207 -  "(\<Sum>k\<le>n. stirling n k) = fact n"
   1.208 +lemma setsum_stirling: "(\<Sum>k\<le>n. stirling n k) = fact n"
   1.209  proof (induct n)
   1.210    case 0
   1.211 -  from this show ?case by simp
   1.212 +  then show ?case by simp
   1.213  next
   1.214    case (Suc n)
   1.215    have "(\<Sum>k\<le>Suc n. stirling (Suc n) k) = stirling (Suc n) 0 + (\<Sum>k\<le>n. stirling (Suc n) (Suc k))"
   1.216      by (simp only: setsum_atMost_Suc_shift)
   1.217 -  also have "\<dots> = (\<Sum>k\<le>n. stirling (Suc n) (Suc k))" by simp
   1.218 -  also have "\<dots> = (\<Sum>k\<le>n. n * stirling n (Suc k) + stirling n k)" by simp
   1.219 +  also have "\<dots> = (\<Sum>k\<le>n. stirling (Suc n) (Suc k))"
   1.220 +    by simp
   1.221 +  also have "\<dots> = (\<Sum>k\<le>n. n * stirling n (Suc k) + stirling n k)"
   1.222 +    by simp
   1.223    also have "\<dots> = n * (\<Sum>k\<le>n. stirling n (Suc k)) + (\<Sum>k\<le>n. stirling n k)"
   1.224      by (simp add: setsum.distrib setsum_right_distrib)
   1.225    also have "\<dots> = n * fact n + fact n"
   1.226    proof -
   1.227      have "n * (\<Sum>k\<le>n. stirling n (Suc k)) = n * ((\<Sum>k\<le>Suc n. stirling n k) - stirling n 0)"
   1.228        by (metis add_diff_cancel_left' setsum_atMost_Suc_shift)
   1.229 -    also have "\<dots> = n * (\<Sum>k\<le>n. stirling n k)" by (cases n) simp+
   1.230 -    also have "\<dots> = n * fact n" using Suc.hyps by simp
   1.231 +    also have "\<dots> = n * (\<Sum>k\<le>n. stirling n k)"
   1.232 +      by (cases n) simp_all
   1.233 +    also have "\<dots> = n * fact n"
   1.234 +      using Suc.hyps by simp
   1.235      finally have "n * (\<Sum>k\<le>n. stirling n (Suc k)) = n * fact n" .
   1.236 -    moreover have "(\<Sum>k\<le>n. stirling n k) = fact n" using Suc.hyps .
   1.237 +    moreover have "(\<Sum>k\<le>n. stirling n k) = fact n"
   1.238 +      using Suc.hyps .
   1.239      ultimately show ?thesis by simp
   1.240    qed
   1.241    also have "\<dots> = fact (Suc n)" by simp
   1.242 @@ -166,26 +181,29 @@
   1.243  qed
   1.244  
   1.245  lemma stirling_pochhammer:
   1.246 -  "(\<Sum>k\<le>n. of_nat (stirling n k) * x ^ k) = (pochhammer x n :: 'a :: comm_semiring_1)"
   1.247 -proof (induction n)
   1.248 +  "(\<Sum>k\<le>n. of_nat (stirling n k) * x ^ k) = (pochhammer x n :: 'a::comm_semiring_1)"
   1.249 +proof (induct n)
   1.250 +  case 0
   1.251 +  then show ?case by simp
   1.252 +next
   1.253    case (Suc n)
   1.254    have "of_nat (n * stirling n 0) = (0 :: 'a)" by (cases n) simp_all
   1.255 -  hence "(\<Sum>k\<le>Suc n. of_nat (stirling (Suc n) k) * x ^ k) =
   1.256 -            (of_nat (n * stirling n 0) * x ^ 0 +
   1.257 -            (\<Sum>i\<le>n. of_nat (n * stirling n (Suc i)) * (x ^ Suc i))) +
   1.258 -            (\<Sum>i\<le>n. of_nat (stirling n i) * (x ^ Suc i))"
   1.259 +  then have "(\<Sum>k\<le>Suc n. of_nat (stirling (Suc n) k) * x ^ k) =
   1.260 +      (of_nat (n * stirling n 0) * x ^ 0 +
   1.261 +      (\<Sum>i\<le>n. of_nat (n * stirling n (Suc i)) * (x ^ Suc i))) +
   1.262 +      (\<Sum>i\<le>n. of_nat (stirling n i) * (x ^ Suc i))"
   1.263      by (subst setsum_atMost_Suc_shift) (simp add: setsum.distrib ring_distribs)
   1.264    also have "\<dots> = pochhammer x (Suc n)"
   1.265      by (subst setsum_atMost_Suc_shift [symmetric])
   1.266 -       (simp add: algebra_simps setsum.distrib setsum_right_distrib pochhammer_Suc Suc [symmetric])
   1.267 +      (simp add: algebra_simps setsum.distrib setsum_right_distrib pochhammer_Suc Suc [symmetric])
   1.268    finally show ?case .
   1.269 -qed simp_all
   1.270 +qed
   1.271  
   1.272  
   1.273  text \<open>A row of the Stirling number triangle\<close>
   1.274  
   1.275 -definition stirling_row :: "nat \<Rightarrow> nat list" where
   1.276 -  "stirling_row n = [stirling n k. k \<leftarrow> [0..<Suc n]]"
   1.277 +definition stirling_row :: "nat \<Rightarrow> nat list"
   1.278 +  where "stirling_row n = [stirling n k. k \<leftarrow> [0..<Suc n]]"
   1.279  
   1.280  lemma nth_stirling_row: "k \<le> n \<Longrightarrow> stirling_row n ! k = stirling n k"
   1.281    by (simp add: stirling_row_def del: upt_Suc)
   1.282 @@ -200,82 +218,109 @@
   1.283  lemma list_ext:
   1.284    assumes "length xs = length ys"
   1.285    assumes "\<And>i. i < length xs \<Longrightarrow> xs ! i = ys ! i"
   1.286 -  shows   "xs = ys"
   1.287 -using assms
   1.288 +  shows "xs = ys"
   1.289 +  using assms
   1.290  proof (induction rule: list_induct2)
   1.291 +  case Nil
   1.292 +  then show ?case by simp
   1.293 +next
   1.294    case (Cons x xs y ys)
   1.295 -  from Cons.prems[of 0] have "x = y" by simp
   1.296 -  moreover from Cons.prems[of "Suc i" for i] have "xs = ys" by (intro Cons.IH) simp
   1.297 +  from Cons.prems[of 0] have "x = y"
   1.298 +    by simp
   1.299 +  moreover from Cons.prems[of "Suc i" for i] have "xs = ys"
   1.300 +    by (intro Cons.IH) simp
   1.301    ultimately show ?case by simp
   1.302 -qed simp_all
   1.303 +qed
   1.304  
   1.305  
   1.306  subsubsection \<open>Efficient code\<close>
   1.307  
   1.308  text \<open>
   1.309 -  Naively using the defining equations of the Stirling numbers of the first kind to
   1.310 -  compute them leads to exponential run time due to repeated computations.
   1.311 -  We can use memoisation to compute them row by row without repeating computations, at
   1.312 -  the cost of computing a few unneeded values.
   1.313 +  Naively using the defining equations of the Stirling numbers of the first
   1.314 +  kind to compute them leads to exponential run time due to repeated
   1.315 +  computations. We can use memoisation to compute them row by row without
   1.316 +  repeating computations, at the cost of computing a few unneeded values.
   1.317  
   1.318    As a bonus, this is very efficient for applications where an entire row of
   1.319 -  Stirling numbers is needed..
   1.320 +  Stirling numbers is needed.
   1.321  \<close>
   1.322  
   1.323 -definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   1.324 -  "zip_with_prev f x xs = map (\<lambda>(x,y). f x y) (zip (x # xs) xs)"
   1.325 +definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list"
   1.326 +  where "zip_with_prev f x xs = map (\<lambda>(x,y). f x y) (zip (x # xs) xs)"
   1.327  
   1.328  lemma zip_with_prev_altdef:
   1.329    "zip_with_prev f x xs =
   1.330 -     (if xs = [] then [] else f x (hd xs) # [f (xs!i) (xs!(i+1)). i \<leftarrow> [0..<length xs - 1]])"
   1.331 +    (if xs = [] then [] else f x (hd xs) # [f (xs!i) (xs!(i+1)). i \<leftarrow> [0..<length xs - 1]])"
   1.332  proof (cases xs)
   1.333 +  case Nil
   1.334 +  then show ?thesis
   1.335 +    by (simp add: zip_with_prev_def)
   1.336 +next
   1.337    case (Cons y ys)
   1.338 -  hence "zip_with_prev f x xs = f x (hd xs) # zip_with_prev f y ys"
   1.339 +  then have "zip_with_prev f x xs = f x (hd xs) # zip_with_prev f y ys"
   1.340      by (simp add: zip_with_prev_def)
   1.341    also have "zip_with_prev f y ys = map (\<lambda>i. f (xs ! i) (xs ! (i + 1))) [0..<length xs - 1]"
   1.342      unfolding Cons
   1.343 -    by (induction ys arbitrary: y)
   1.344 -       (simp_all add: zip_with_prev_def upt_conv_Cons map_Suc_upt [symmetric] del: upt_Suc)
   1.345 -  finally show ?thesis using Cons by simp
   1.346 -qed (simp add: zip_with_prev_def)
   1.347 +    by (induct ys arbitrary: y)
   1.348 +      (simp_all add: zip_with_prev_def upt_conv_Cons map_Suc_upt [symmetric] del: upt_Suc)
   1.349 +  finally show ?thesis
   1.350 +    using Cons by simp
   1.351 +qed
   1.352  
   1.353  
   1.354 -primrec stirling_row_aux where
   1.355 -  "stirling_row_aux n y [] = [1]"
   1.356 -| "stirling_row_aux n y (x#xs) = (y + n * x) # stirling_row_aux n x xs"
   1.357 +primrec stirling_row_aux
   1.358 +  where
   1.359 +    "stirling_row_aux n y [] = [1]"
   1.360 +  | "stirling_row_aux n y (x#xs) = (y + n * x) # stirling_row_aux n x xs"
   1.361  
   1.362  lemma stirling_row_aux_correct:
   1.363    "stirling_row_aux n y xs = zip_with_prev (\<lambda>a b. a + n * b) y xs @ [1]"
   1.364 -  by (induction xs arbitrary: y) (simp_all add: zip_with_prev_def)
   1.365 +  by (induct xs arbitrary: y) (simp_all add: zip_with_prev_def)
   1.366  
   1.367  lemma stirling_row_code [code]:
   1.368    "stirling_row 0 = [1]"
   1.369    "stirling_row (Suc n) = stirling_row_aux n 0 (stirling_row n)"
   1.370 -proof -
   1.371 +proof goal_cases
   1.372 +  case 1
   1.373 +  show ?case by (simp add: stirling_row_def)
   1.374 +next
   1.375 +  case 2
   1.376    have "stirling_row (Suc n) =
   1.377 -          0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \<leftarrow> [0..<n]] @ [1]"
   1.378 +    0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \<leftarrow> [0..<n]] @ [1]"
   1.379    proof (rule list_ext, goal_cases length nth)
   1.380      case (nth i)
   1.381 -    from nth have "i \<le> Suc n" by simp
   1.382 -    then consider "i = 0" | j where "i > 0" "i \<le> n" | "i = Suc n" by linarith
   1.383 -    thus ?case
   1.384 +    from nth have "i \<le> Suc n"
   1.385 +      by simp
   1.386 +    then consider "i = 0 \<or> i = Suc n" | "i > 0" "i \<le> n"
   1.387 +      by linarith
   1.388 +    then show ?case
   1.389      proof cases
   1.390 -      assume i: "i > 0" "i \<le> n"
   1.391 -      from this show ?thesis by (cases i) (simp_all add: nth_append nth_stirling_row)
   1.392 -    qed (simp_all add: nth_stirling_row nth_append)
   1.393 -  qed simp
   1.394 +      case 1
   1.395 +      then show ?thesis
   1.396 +        by (auto simp: nth_stirling_row nth_append)
   1.397 +    next
   1.398 +      case 2
   1.399 +      then show ?thesis
   1.400 +        by (cases i) (simp_all add: nth_append nth_stirling_row)
   1.401 +    qed
   1.402 +  next
   1.403 +    case length
   1.404 +    then show ?case by simp
   1.405 +  qed
   1.406    also have "0 # [stirling_row n ! i + stirling_row n ! (i+1) * n. i \<leftarrow> [0..<n]] @ [1] =
   1.407 -               zip_with_prev (\<lambda>a b. a + n * b) 0 (stirling_row n) @ [1]"
   1.408 +      zip_with_prev (\<lambda>a b. a + n * b) 0 (stirling_row n) @ [1]"
   1.409      by (cases n) (auto simp add: zip_with_prev_altdef stirling_row_def hd_map simp del: upt_Suc)
   1.410    also have "\<dots> = stirling_row_aux n 0 (stirling_row n)"
   1.411      by (simp add: stirling_row_aux_correct)
   1.412 -  finally show "stirling_row (Suc n) = stirling_row_aux n 0 (stirling_row n)" .
   1.413 -qed (simp add: stirling_row_def)
   1.414 +  finally show ?case .
   1.415 +qed
   1.416  
   1.417  lemma stirling_code [code]:
   1.418 -  "stirling n k = (if k = 0 then if n = 0 then 1 else 0
   1.419 -                   else if k > n then 0 else if k = n then 1
   1.420 -                   else stirling_row n ! k)"
   1.421 +  "stirling n k =
   1.422 +    (if k = 0 then (if n = 0 then 1 else 0)
   1.423 +     else if k > n then 0
   1.424 +     else if k = n then 1
   1.425 +     else stirling_row n ! k)"
   1.426    by (simp add: nth_stirling_row)
   1.427  
   1.428  end