author haftmann Wed, 22 Aug 2018 12:32:58 +0000 changeset 68783 248e1678ce55 parent 68782 8ff34c1ad580 child 68784 c7ee984243fc
more theorems on fact
 src/HOL/Factorial.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Factorial.thy	Wed Aug 22 12:32:58 2018 +0000
+++ b/src/HOL/Factorial.thy	Wed Aug 22 12:32:58 2018 +0000
@@ -174,12 +174,30 @@
by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
qed

+lemma prod_Suc_fact: "prod Suc {0..<n} = fact n"
+  by (simp add: fact_prod_Suc)
+
+lemma prod_Suc_Suc_fact: "prod Suc {Suc 0..<n} = fact n"
+proof (cases "n = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  have "prod Suc {Suc 0..<n} = Suc 0 * prod Suc {Suc 0..<n}"
+    by simp
+  also have "\<dots> = prod Suc (insert 0 {Suc 0..<n})"
+    by simp
+  also have "insert 0 {Suc 0..<n} = {0..<n}"
+    using False by auto
+  finally show ?thesis
+    by (simp add: fact_prod_Suc)
+qed
+
lemma fact_numeral: "fact (numeral k) = numeral k * fact (pred_numeral k)"
\<comment> \<open>Evaluation for specific numerals\<close>
by (metis fact_Suc numeral_eq_Suc of_nat_numeral)

-
subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>

text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>```