src/HOL/Factorial.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 66589 b884c42694e0
child 66806 a4e82b58d833
permissions -rw-r--r--
tuned;
wenzelm@66589
     1
(*  Title:      HOL/Factorial.thy
haftmann@65812
     2
    Author:     Jacques D. Fleuriot
haftmann@65812
     3
    Author:     Lawrence C Paulson
haftmann@65812
     4
    Author:     Jeremy Avigad
haftmann@65812
     5
    Author:     Chaitanya Mangla
haftmann@65812
     6
    Author:     Manuel Eberl
haftmann@65812
     7
*)
haftmann@65812
     8
haftmann@65812
     9
section \<open>Factorial Function, Rising Factorials\<close>
haftmann@65812
    10
haftmann@65812
    11
theory Factorial
haftmann@65813
    12
  imports Groups_List
haftmann@65812
    13
begin
haftmann@65812
    14
haftmann@65812
    15
subsection \<open>Factorial Function\<close>
haftmann@65812
    16
haftmann@65812
    17
context semiring_char_0
haftmann@65812
    18
begin
haftmann@65812
    19
haftmann@65812
    20
definition fact :: "nat \<Rightarrow> 'a"
haftmann@65812
    21
  where fact_prod: "fact n = of_nat (\<Prod>{1..n})"
haftmann@65812
    22
haftmann@65812
    23
lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
haftmann@65812
    24
  by (cases n)
haftmann@65812
    25
    (simp_all add: fact_prod prod.atLeast_Suc_atMost_Suc_shift
haftmann@65812
    26
      atLeastLessThanSuc_atLeastAtMost)
haftmann@65812
    27
haftmann@65812
    28
lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
haftmann@65812
    29
  using prod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
haftmann@65812
    30
  by (cases n)
haftmann@65812
    31
    (simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
haftmann@65812
    32
      atLeastLessThanSuc_atLeastAtMost)
haftmann@65812
    33
haftmann@65812
    34
lemma fact_0 [simp]: "fact 0 = 1"
haftmann@65812
    35
  by (simp add: fact_prod)
haftmann@65812
    36
haftmann@65812
    37
lemma fact_1 [simp]: "fact 1 = 1"
haftmann@65812
    38
  by (simp add: fact_prod)
haftmann@65812
    39
haftmann@65812
    40
lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
haftmann@65812
    41
  by (simp add: fact_prod)
haftmann@65812
    42
haftmann@65812
    43
lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
haftmann@65812
    44
  by (simp add: fact_prod atLeastAtMostSuc_conv algebra_simps)
haftmann@65812
    45
haftmann@65812
    46
lemma fact_2 [simp]: "fact 2 = 2"
haftmann@65812
    47
  by (simp add: numeral_2_eq_2)
haftmann@65812
    48
haftmann@65812
    49
lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (prod Suc {n - k..<n}) * fact (n - k)"
haftmann@65812
    50
  by (simp add: fact_prod_Suc prod.union_disjoint [symmetric]
haftmann@65812
    51
    ivl_disj_un ac_simps of_nat_mult [symmetric])
haftmann@65812
    52
haftmann@65812
    53
end
haftmann@65812
    54
haftmann@65812
    55
lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
haftmann@65812
    56
  by (simp add: fact_prod)
haftmann@65812
    57
haftmann@65812
    58
lemma of_int_fact [simp]: "of_int (fact n) = fact n"
haftmann@65812
    59
  by (simp only: fact_prod of_int_of_nat_eq)
haftmann@65812
    60
haftmann@65812
    61
lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
haftmann@65812
    62
  by (cases n) auto
haftmann@65812
    63
haftmann@65812
    64
lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
haftmann@65812
    65
  apply (induct n)
haftmann@65812
    66
  apply auto
haftmann@65812
    67
  using of_nat_eq_0_iff
haftmann@65812
    68
  apply fastforce
haftmann@65812
    69
  done
haftmann@65812
    70
haftmann@65812
    71
lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
haftmann@65812
    72
  by (induct n) (auto simp: le_Suc_eq)
haftmann@65812
    73
haftmann@65812
    74
lemma fact_in_Nats: "fact n \<in> \<nat>"
haftmann@65812
    75
  by (induct n) auto
haftmann@65812
    76
haftmann@65812
    77
lemma fact_in_Ints: "fact n \<in> \<int>"
haftmann@65812
    78
  by (induct n) auto
haftmann@65812
    79
haftmann@65812
    80
context
haftmann@65812
    81
  assumes "SORT_CONSTRAINT('a::linordered_semidom)"
haftmann@65812
    82
begin
haftmann@65812
    83
haftmann@65812
    84
lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
haftmann@65812
    85
  by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
haftmann@65812
    86
haftmann@65812
    87
lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
haftmann@65812
    88
  by (metis le0 fact_0 fact_mono)
haftmann@65812
    89
haftmann@65812
    90
lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
haftmann@65812
    91
  using fact_ge_1 less_le_trans zero_less_one by blast
haftmann@65812
    92
haftmann@65812
    93
lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
haftmann@65812
    94
  by (simp add: less_imp_le)
haftmann@65812
    95
haftmann@65812
    96
lemma fact_not_neg [simp]: "\<not> fact n < (0 :: 'a)"
haftmann@65812
    97
  by (simp add: not_less_iff_gr_or_eq)
haftmann@65812
    98
haftmann@65812
    99
lemma fact_le_power: "fact n \<le> (of_nat (n^n) :: 'a)"
haftmann@65812
   100
proof (induct n)
haftmann@65812
   101
  case 0
haftmann@65812
   102
  then show ?case by simp
haftmann@65812
   103
next
haftmann@65812
   104
  case (Suc n)
haftmann@65812
   105
  then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
haftmann@65812
   106
    by (rule order_trans) (simp add: power_mono del: of_nat_power)
haftmann@65812
   107
  have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
haftmann@65812
   108
    by (simp add: algebra_simps)
haftmann@65812
   109
  also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n ^ n)"
haftmann@65812
   110
    by (simp add: * ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)
haftmann@65812
   111
  also have "\<dots> \<le> of_nat (Suc n ^ Suc n)"
haftmann@65812
   112
    by (metis of_nat_mult order_refl power_Suc)
haftmann@65812
   113
  finally show ?case .
haftmann@65812
   114
qed
haftmann@65812
   115
haftmann@65812
   116
end
haftmann@65812
   117
haftmann@65812
   118
lemma fact_less_mono_nat: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: nat)"
haftmann@65812
   119
  by (induct n) (auto simp: less_Suc_eq)
haftmann@65812
   120
haftmann@65812
   121
lemma fact_less_mono: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)"
haftmann@65812
   122
  by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
haftmann@65812
   123
haftmann@65812
   124
lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
haftmann@65812
   125
  by (metis One_nat_def fact_ge_1)
haftmann@65812
   126
haftmann@65812
   127
lemma dvd_fact: "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
haftmann@65812
   128
  by (induct n) (auto simp: dvdI le_Suc_eq)
haftmann@65812
   129
haftmann@65812
   130
lemma fact_ge_self: "fact n \<ge> n"
haftmann@65812
   131
  by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
haftmann@65812
   132
haftmann@65812
   133
lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})"
haftmann@65812
   134
  by (induct m) (auto simp: le_Suc_eq)
haftmann@65812
   135
haftmann@65812
   136
lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0"
haftmann@65812
   137
  by (auto simp add: fact_dvd)
haftmann@65812
   138
haftmann@65812
   139
lemma fact_div_fact:
haftmann@65812
   140
  assumes "m \<ge> n"
haftmann@65812
   141
  shows "fact m div fact n = \<Prod>{n + 1..m}"
haftmann@65812
   142
proof -
haftmann@65812
   143
  obtain d where "d = m - n"
haftmann@65812
   144
    by auto
haftmann@65812
   145
  with assms have "m = n + d"
haftmann@65812
   146
    by auto
haftmann@65812
   147
  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
haftmann@65812
   148
  proof (induct d)
haftmann@65812
   149
    case 0
haftmann@65812
   150
    show ?case by simp
haftmann@65812
   151
  next
haftmann@65812
   152
    case (Suc d')
haftmann@65812
   153
    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
haftmann@65812
   154
      by simp
haftmann@65812
   155
    also from Suc.hyps have "\<dots> = Suc (n + d') * \<Prod>{n + 1..n + d'}"
haftmann@65812
   156
      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
haftmann@65812
   157
    also have "\<dots> = \<Prod>{n + 1..n + Suc d'}"
haftmann@65812
   158
      by (simp add: atLeastAtMostSuc_conv)
haftmann@65812
   159
    finally show ?case .
haftmann@65812
   160
  qed
haftmann@65812
   161
  with \<open>m = n + d\<close> show ?thesis by simp
haftmann@65812
   162
qed
haftmann@65812
   163
haftmann@65812
   164
lemma fact_num_eq_if: "fact m = (if m = 0 then 1 else of_nat m * fact (m - 1))"
haftmann@65812
   165
  by (cases m) auto
haftmann@65812
   166
haftmann@65812
   167
lemma fact_div_fact_le_pow:
haftmann@65812
   168
  assumes "r \<le> n"
haftmann@65812
   169
  shows "fact n div fact (n - r) \<le> n ^ r"
haftmann@65812
   170
proof -
haftmann@65812
   171
  have "r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" for r
haftmann@65812
   172
    by (subst prod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
haftmann@65812
   173
  with assms show ?thesis
haftmann@65812
   174
    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
haftmann@65812
   175
qed
haftmann@65812
   176
haftmann@65812
   177
lemma fact_numeral: "fact (numeral k) = numeral k * fact (pred_numeral k)"
haftmann@65812
   178
  \<comment> \<open>Evaluation for specific numerals\<close>
haftmann@65812
   179
  by (metis fact_Suc numeral_eq_Suc of_nat_numeral)
haftmann@65812
   180
haftmann@65812
   181
haftmann@65812
   182
haftmann@65812
   183
subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
haftmann@65812
   184
haftmann@65812
   185
text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
haftmann@65812
   186
haftmann@65812
   187
context comm_semiring_1
haftmann@65812
   188
begin
haftmann@65812
   189
haftmann@65812
   190
definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
haftmann@65812
   191
  where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"
haftmann@65812
   192
haftmann@65812
   193
lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
haftmann@65812
   194
  using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
haftmann@65812
   195
  by (simp add: pochhammer_prod)
haftmann@65812
   196
haftmann@65812
   197
lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
haftmann@65812
   198
  by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)
haftmann@65812
   199
haftmann@65812
   200
lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
haftmann@65812
   201
  by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift)
haftmann@65812
   202
haftmann@65812
   203
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
haftmann@65812
   204
  by (simp add: pochhammer_prod)
haftmann@65812
   205
haftmann@65812
   206
lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
haftmann@65812
   207
  by (simp add: pochhammer_prod lessThan_Suc)
haftmann@65812
   208
haftmann@65812
   209
lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
haftmann@65812
   210
  by (simp add: pochhammer_prod lessThan_Suc)
haftmann@65812
   211
haftmann@65812
   212
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
haftmann@65812
   213
  by (simp add: pochhammer_prod atLeast0_lessThan_Suc ac_simps)
haftmann@65812
   214
haftmann@65812
   215
end
haftmann@65812
   216
haftmann@65812
   217
lemma pochhammer_nonneg:
haftmann@65812
   218
  fixes x :: "'a :: linordered_semidom"
haftmann@65812
   219
  shows "x > 0 \<Longrightarrow> pochhammer x n \<ge> 0"
haftmann@65812
   220
  by (induction n) (auto simp: pochhammer_Suc intro!: mult_nonneg_nonneg add_nonneg_nonneg)
haftmann@65812
   221
haftmann@65812
   222
lemma pochhammer_pos:
haftmann@65812
   223
  fixes x :: "'a :: linordered_semidom"
haftmann@65812
   224
  shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
haftmann@65812
   225
  by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
haftmann@65812
   226
haftmann@65812
   227
lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
haftmann@65812
   228
  by (simp add: pochhammer_prod)
haftmann@65812
   229
haftmann@65812
   230
lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
haftmann@65812
   231
  by (simp add: pochhammer_prod)
haftmann@65812
   232
haftmann@65812
   233
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
haftmann@65812
   234
  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
haftmann@65812
   235
haftmann@65812
   236
lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
haftmann@65812
   237
  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)
haftmann@65812
   238
haftmann@65812
   239
lemma pochhammer_fact: "fact n = pochhammer 1 n"
haftmann@65812
   240
  by (simp add: pochhammer_prod fact_prod_Suc)
haftmann@65812
   241
haftmann@65812
   242
lemma pochhammer_of_nat_eq_0_lemma: "k > n \<Longrightarrow> pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
haftmann@65812
   243
  by (auto simp add: pochhammer_prod)
haftmann@65812
   244
haftmann@65812
   245
lemma pochhammer_of_nat_eq_0_lemma':
haftmann@65812
   246
  assumes kn: "k \<le> n"
haftmann@65812
   247
  shows "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k \<noteq> 0"
haftmann@65812
   248
proof (cases k)
haftmann@65812
   249
  case 0
haftmann@65812
   250
  then show ?thesis by simp
haftmann@65812
   251
next
haftmann@65812
   252
  case (Suc h)
haftmann@65812
   253
  then show ?thesis
haftmann@65812
   254
    apply (simp add: pochhammer_Suc_prod)
haftmann@65812
   255
    using Suc kn
haftmann@65812
   256
    apply (auto simp add: algebra_simps)
haftmann@65812
   257
    done
haftmann@65812
   258
qed
haftmann@65812
   259
haftmann@65812
   260
lemma pochhammer_of_nat_eq_0_iff:
haftmann@65812
   261
  "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
haftmann@65812
   262
  (is "?l = ?r")
haftmann@65812
   263
  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
haftmann@65812
   264
    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
haftmann@65812
   265
  by (auto simp add: not_le[symmetric])
haftmann@65812
   266
eberlm@66394
   267
lemma pochhammer_0_left:
eberlm@66394
   268
  "pochhammer 0 n = (if n = 0 then 1 else 0)"
eberlm@66394
   269
  by (induction n) (simp_all add: pochhammer_rec)
eberlm@66394
   270
haftmann@65812
   271
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
haftmann@65812
   272
  by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)
haftmann@65812
   273
haftmann@65812
   274
lemma pochhammer_eq_0_mono:
haftmann@65812
   275
  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
haftmann@65812
   276
  unfolding pochhammer_eq_0_iff by auto
haftmann@65812
   277
haftmann@65812
   278
lemma pochhammer_neq_0_mono:
haftmann@65812
   279
  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
haftmann@65812
   280
  unfolding pochhammer_eq_0_iff by auto
haftmann@65812
   281
haftmann@65812
   282
lemma pochhammer_minus:
haftmann@65812
   283
  "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
haftmann@65812
   284
proof (cases k)
haftmann@65812
   285
  case 0
haftmann@65812
   286
  then show ?thesis by simp
haftmann@65812
   287
next
haftmann@65812
   288
  case (Suc h)
haftmann@65812
   289
  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
haftmann@65812
   290
    using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
haftmann@65812
   291
    by auto
haftmann@65812
   292
  with Suc show ?thesis
haftmann@65812
   293
    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
haftmann@65812
   294
    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
haftmann@65812
   295
qed
haftmann@65812
   296
haftmann@65812
   297
lemma pochhammer_minus':
haftmann@65812
   298
  "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
haftmann@65812
   299
  apply (simp only: pochhammer_minus [where b = b])
haftmann@65812
   300
  apply (simp only: mult.assoc [symmetric])
haftmann@65812
   301
  apply (simp only: power_add [symmetric])
haftmann@65812
   302
  apply simp
haftmann@65812
   303
  done
haftmann@65812
   304
haftmann@65812
   305
lemma pochhammer_same: "pochhammer (- of_nat n) n =
haftmann@65812
   306
    ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"
haftmann@65812
   307
  unfolding pochhammer_minus
haftmann@65812
   308
  by (simp add: of_nat_diff pochhammer_fact)
haftmann@65812
   309
haftmann@65812
   310
lemma pochhammer_product': "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
haftmann@65812
   311
proof (induct n arbitrary: z)
haftmann@65812
   312
  case 0
haftmann@65812
   313
  then show ?case by simp
haftmann@65812
   314
next
haftmann@65812
   315
  case (Suc n z)
haftmann@65812
   316
  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
haftmann@65812
   317
      z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
haftmann@65812
   318
    by (simp add: pochhammer_rec ac_simps)
haftmann@65812
   319
  also note Suc[symmetric]
haftmann@65812
   320
  also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
haftmann@65812
   321
    by (subst pochhammer_rec) simp
haftmann@65812
   322
  finally show ?case
haftmann@65812
   323
    by simp
haftmann@65812
   324
qed
haftmann@65812
   325
haftmann@65812
   326
lemma pochhammer_product:
haftmann@65812
   327
  "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
haftmann@65812
   328
  using pochhammer_product'[of z m "n - m"] by simp
haftmann@65812
   329
haftmann@65812
   330
lemma pochhammer_times_pochhammer_half:
haftmann@65812
   331
  fixes z :: "'a::field_char_0"
haftmann@65812
   332
  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
haftmann@65812
   333
proof (induct n)
haftmann@65812
   334
  case 0
haftmann@65812
   335
  then show ?case
haftmann@65812
   336
    by (simp add: atLeast0_atMost_Suc)
haftmann@65812
   337
next
haftmann@65812
   338
  case (Suc n)
haftmann@65812
   339
  define n' where "n' = Suc n"
haftmann@65812
   340
  have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
haftmann@65812
   341
      (pochhammer z n' * pochhammer (z + 1 / 2) n') * ((z + of_nat n') * (z + 1/2 + of_nat n'))"
haftmann@65812
   342
    (is "_ = _ * ?A")
haftmann@65812
   343
    by (simp_all add: pochhammer_rec' mult_ac)
haftmann@65812
   344
  also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
haftmann@65812
   345
    (is "_ = ?B")
haftmann@65812
   346
    by (simp add: field_simps n'_def)
haftmann@65812
   347
  also note Suc[folded n'_def]
haftmann@65812
   348
  also have "(\<Prod>k=0..2 * n + 1. z + of_nat k / 2) * ?B = (\<Prod>k=0..2 * Suc n + 1. z + of_nat k / 2)"
haftmann@65812
   349
    by (simp add: atLeast0_atMost_Suc)
haftmann@65812
   350
  finally show ?case
haftmann@65812
   351
    by (simp add: n'_def)
haftmann@65812
   352
qed
haftmann@65812
   353
haftmann@65812
   354
lemma pochhammer_double:
haftmann@65812
   355
  fixes z :: "'a::field_char_0"
haftmann@65812
   356
  shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
haftmann@65812
   357
proof (induct n)
haftmann@65812
   358
  case 0
haftmann@65812
   359
  then show ?case by simp
haftmann@65812
   360
next
haftmann@65812
   361
  case (Suc n)
haftmann@65812
   362
  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
haftmann@65812
   363
      (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
haftmann@65812
   364
    by (simp add: pochhammer_rec' ac_simps)
haftmann@65812
   365
  also note Suc
haftmann@65812
   366
  also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *
haftmann@65812
   367
        (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
haftmann@65812
   368
      of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
haftmann@65812
   369
    by (simp add: field_simps pochhammer_rec')
haftmann@65812
   370
  finally show ?case .
haftmann@65812
   371
qed
haftmann@65812
   372
haftmann@65812
   373
lemma fact_double:
haftmann@65812
   374
  "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a::field_char_0)"
haftmann@65812
   375
  using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
haftmann@65812
   376
haftmann@65812
   377
lemma pochhammer_absorb_comp: "(r - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
haftmann@65812
   378
  (is "?lhs = ?rhs")
haftmann@65812
   379
  for r :: "'a::comm_ring_1"
haftmann@65812
   380
proof -
haftmann@65812
   381
  have "?lhs = - pochhammer (- r) (Suc k)"
haftmann@65812
   382
    by (subst pochhammer_rec') (simp add: algebra_simps)
haftmann@65812
   383
  also have "\<dots> = ?rhs"
haftmann@65812
   384
    by (subst pochhammer_rec) simp
haftmann@65812
   385
  finally show ?thesis .
haftmann@65812
   386
qed
haftmann@65812
   387
haftmann@65812
   388
haftmann@65812
   389
subsection \<open>Misc\<close>
haftmann@65812
   390
haftmann@65812
   391
lemma fact_code [code]:
haftmann@65812
   392
  "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)"
haftmann@65812
   393
proof -
haftmann@65812
   394
  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
haftmann@65812
   395
    by (simp add: fact_prod)
haftmann@65812
   396
  also have "\<Prod>{1..n} = \<Prod>{2..n}"
haftmann@65812
   397
    by (intro prod.mono_neutral_right) auto
haftmann@65812
   398
  also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
haftmann@65812
   399
    by (simp add: prod_atLeastAtMost_code)
haftmann@65812
   400
  finally show ?thesis .
haftmann@65812
   401
qed
haftmann@65812
   402
haftmann@65812
   403
lemma pochhammer_code [code]:
haftmann@65812
   404
  "pochhammer a n =
haftmann@65812
   405
    (if n = 0 then 1
haftmann@65812
   406
     else fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
haftmann@65812
   407
  by (cases n)
haftmann@65812
   408
    (simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
haftmann@65812
   409
      atLeastLessThanSuc_atLeastAtMost)
haftmann@65812
   410
haftmann@65812
   411
end