# 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 \ m \ fact n dvd fact (m::nat)" + by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset) + +lemma fact_mod: "m \ (n::nat) \ fact n mod fact m = 0" + by (auto simp add: dvd_imp_mod_0 fact_dvd) + +lemma fact_div_fact: + assumes "m \ (n :: nat)" + shows "(fact m) div (fact n) = \{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) = \{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') * \{n + 1..n + d'}" + unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod) + also have "... = \{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) \ n \ fact m \ fact n" apply (drule le_imp_less_or_eq) apply (auto dest!: less_imp_Suc_add)