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