--- a/src/HOL/Binomial.thy Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Binomial.thy Wed Feb 17 21:51:57 2016 +0100
@@ -25,9 +25,19 @@
lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
by simp
-lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
+lemma of_nat_fact [simp]:
+ "of_nat (fact n) = fact n"
by (induct n) (auto simp add: algebra_simps of_nat_mult)
+lemma of_int_fact [simp]:
+ "of_int (fact n) = fact n"
+proof -
+ have "of_int (of_nat (fact n)) = fact n"
+ unfolding of_int_of_nat_eq by simp
+ then show ?thesis
+ by simp
+qed
+
lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
by (cases n) auto