src/HOL/Fact.thy
 changeset 40033 84200d970bf0 parent 35644 d20cf282342e child 41550 efa734d9b221
```     1.1 --- a/src/HOL/Fact.thy	Tue Oct 19 12:26:37 2010 +0200
1.2 +++ b/src/HOL/Fact.thy	Tue Oct 19 12:26:38 2010 +0200
1.3 @@ -183,6 +183,35 @@
1.4    apply auto
1.5  done
1.6
1.7 +lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
1.8 +  by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
1.9 +
1.10 +lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
1.11 +  by (auto simp add: dvd_imp_mod_0 fact_dvd)
1.12 +
1.13 +lemma fact_div_fact:
1.14 +  assumes "m \<ge> (n :: nat)"
1.15 +  shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
1.16 +proof -
1.17 +  obtain d where "d = m - n" by auto
1.18 +  from assms this have "m = n + d" by auto
1.19 +  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
1.20 +  proof (induct d)
1.21 +    case 0
1.22 +    show ?case by simp
1.23 +  next
1.24 +    case (Suc d')
1.25 +    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
1.26 +      by simp
1.27 +    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
1.28 +      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
1.29 +    also have "... = \<Prod>{n + 1..n + Suc d'}"
1.30 +      by (simp add: atLeastAtMostSuc_conv setprod_insert)
1.31 +    finally show ?case .
1.32 +  qed
1.33 +  from this `m = n + d` show ?thesis by simp
1.34 +qed
1.35 +
1.36  lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
1.37  apply (drule le_imp_less_or_eq)