added some facts about factorial and dvd, div and mod
authorbulwahn
Tue Oct 19 12:26:38 2010 +0200 (2010-10-19)
changeset 4003384200d970bf0
parent 40032 5f78dfb2fa7d
child 40034 767a28027b68
added some facts about factorial and dvd, div and mod
src/HOL/Fact.thy
     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)
    1.38  apply (auto dest!: less_imp_Suc_add)