# HG changeset patch
# User bulwahn
# Date 1287483998 -7200
# Node ID 84200d970bf061ca29972cbafff6fd8d2417491f
# Parent  5f78dfb2fa7d7f726aa896786bde8c5403fab0d5
added some facts about factorial and dvd, div and mod

diff -r 5f78dfb2fa7d -r 84200d970bf0 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Tue Oct 19 12:26:37 2010 +0200
+++ b/src/HOL/Fact.thy	Tue Oct 19 12:26:38 2010 +0200
@@ -183,6 +183,35 @@
   apply auto
 done
 
+lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
+  by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
+
+lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
+  by (auto simp add: dvd_imp_mod_0 fact_dvd)
+
+lemma fact_div_fact:
+  assumes "m \<ge> (n :: nat)"
+  shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
+proof -
+  obtain d where "d = m - n" by auto
+  from assms this have "m = n + d" by auto
+  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
+  proof (induct d)
+    case 0
+    show ?case by simp
+  next
+    case (Suc d')
+    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
+      by simp
+    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}" 
+      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
+    also have "... = \<Prod>{n + 1..n + Suc d'}"
+      by (simp add: atLeastAtMostSuc_conv setprod_insert)
+    finally show ?case .
+  qed
+  from this `m = n + d` show ?thesis by simp
+qed
+
 lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
 apply (drule le_imp_less_or_eq)
 apply (auto dest!: less_imp_Suc_add)