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 \Factorial Function, Rising Factorials\ ``` 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 \Factorial Function\ ``` haftmann@65812 ` 16` haftmann@65812 ` 17` ```context semiring_char_0 ``` haftmann@65812 ` 18` ```begin ``` haftmann@65812 ` 19` haftmann@65812 ` 20` ```definition fact :: "nat \ 'a" ``` haftmann@65812 ` 21` ``` where fact_prod: "fact n = of_nat (\{1..n})" ``` haftmann@65812 ` 22` haftmann@65812 ` 23` ```lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..i = 0..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 \ n \ fact n = of_nat (prod Suc {n - k.. 0 \ 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 \ (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 \ n \ fact m \ (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 \ \" ``` haftmann@65812 ` 75` ``` by (induct n) auto ``` haftmann@65812 ` 76` haftmann@65812 ` 77` ```lemma fact_in_Ints: "fact n \ \" ``` 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 \ n \ fact m \ (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 \ (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 \ (0 :: 'a)" ``` haftmann@65812 ` 94` ``` by (simp add: less_imp_le) ``` haftmann@65812 ` 95` haftmann@65812 ` 96` ```lemma fact_not_neg [simp]: "\ 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 \ (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 \ (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 "\ \ 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 "\ \ 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 \ m < n \ 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 \ m < n \ 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 \ Suc 0" ``` haftmann@65812 ` 125` ``` by (metis One_nat_def fact_ge_1) ``` haftmann@65812 ` 126` haftmann@65812 ` 127` ```lemma dvd_fact: "1 \ m \ m \ n \ 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 \ 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 \ m \ 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 \ n \ 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 \ n" ``` haftmann@65812 ` 141` ``` shows "fact m div fact n = \{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) = \{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 "\ = Suc (n + d') * \{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 "\ = \{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 \m = n + d\ 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 \ n" ``` haftmann@65812 ` 169` ``` shows "fact n div fact (n - r) \ n ^ r" ``` haftmann@65812 ` 170` ```proof - ``` haftmann@65812 ` 171` ``` have "r \ n \ \{n - r..n} = (n - r) * \{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` ``` \ \Evaluation for specific numerals\ ``` 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 \Pochhammer's symbol: generalized rising factorial\ ``` haftmann@65812 ` 184` haftmann@65812 ` 185` ```text \See \<^url>\http://en.wikipedia.org/wiki/Pochhammer_symbol\.\ ``` haftmann@65812 ` 186` haftmann@65812 ` 187` ```context comm_semiring_1 ``` haftmann@65812 ` 188` ```begin ``` haftmann@65812 ` 189` haftmann@65812 ` 190` ```definition pochhammer :: "'a \ nat \ 'a" ``` haftmann@65812 ` 191` ``` where pochhammer_prod: "pochhammer a n = prod (\i. a + of_nat i) {0..i. a + of_nat (n - i)) {1..n}" ``` haftmann@65812 ` 194` ``` using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\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 (\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 (\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 \ pochhammer x n \ 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 \ 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 \ 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 \ n" ``` haftmann@65812 ` 247` ``` shows "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k \ 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 \ 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) \ (\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) \ m \ n \ 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 \ (0::'a::field_char_0) \ m \ n \ pochhammer a n \ 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) = (\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 \ n \ 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) = (\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 "(\k=0..2 * n + 1. z + of_nat k / 2) * ?B = (\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 "\ = ?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 \Misc\ ``` 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 (\{1..n}) :: 'a)" ``` haftmann@65812 ` 395` ``` by (simp add: fact_prod) ``` haftmann@65812 ` 396` ``` also have "\{1..n} = \{2..n}" ``` haftmann@65812 ` 397` ``` by (intro prod.mono_neutral_right) auto ``` haftmann@65812 ` 398` ``` also have "\ = 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 (\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 ```