# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID 248e1678ce556c3b7878d6d2bd5cb1aed454655f
# Parent  8ff34c1ad580630a640b0101e5e21ee90c709c18
more theorems on fact

diff -r 8ff34c1ad580 -r 248e1678ce55 src/HOL/Factorial.thy
--- 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>