# Theory Fact

Up to index of Isabelle/HOL/HOL-Complex

theory Fact
imports Real
begin

    (*  Title       : Fact.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 1998  University of Cambridge
        Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    *)

    header{*Factorial Function*}

    theory Fact
    imports "../Real/Real"
    begin

    consts fact :: "nat => nat"
    primrec
       fact_0:     "fact 0 = 1"
       fact_Suc:   "fact (Suc n) = (Suc n) * fact n"

    lemma fact_gt_zero [simp]: "0 < fact n"
    by (induct "n", auto)

    lemma fact_not_eq_zero [simp]: "fact n ≠ 0"
    by simp

    lemma real_of_nat_fact_not_zero [simp]: "real (fact n) ≠ 0"
    by auto

    lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    by auto

    lemma real_of_nat_fact_ge_zero [simp]: "0 ≤ real(fact n)"
    by simp

    lemma fact_ge_one [simp]: "1 ≤ fact n"
    by (induct "n", auto)

    lemma fact_mono: "m ≤ n ==> fact m ≤ fact n"
    apply (drule le_imp_less_or_eq)
    apply (auto dest!: less_imp_Suc_add)
    apply (induct_tac "k", auto)
    done

    text{*Note that @{term "fact 0 = fact 1"}*}
    lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    apply (drule_tac m = m in less_imp_Suc_add, auto)
    apply (induct_tac "k", auto)
    done

    lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    by (auto simp add: positive_imp_inverse_positive)

    lemma inv_real_of_nat_fact_ge_zero [simp]: "0 ≤ inverse (real (fact n))"
    by (auto intro: order_less_imp_le)

    lemma fact_diff_Suc [rule_format]:
         "∀m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    apply (induct n, auto)
    apply (drule_tac x = "m - 1" in spec, auto)
    done

    lemma fact_num0 [simp]: "fact 0 = 1"
    by auto

    lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    by (case_tac "m", auto)

    lemma fact_add_num_eq_if:
         "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
    by (case_tac "m+n", auto)

    lemma fact_add_num_eq_if2:
         "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
    by (case_tac "m", auto)

    end

lemma fact_gt_zero:

      0 < fact n

lemma fact_not_eq_zero:

      fact n ≠ 0

lemma real_of_nat_fact_not_zero:

      real (fact n) ≠ 0

lemma real_of_nat_fact_gt_zero:

      0 < real (fact n)

lemma real_of_nat_fact_ge_zero:

      0 ≤ real (fact n)

lemma fact_ge_one:

      1 ≤ fact n

lemma fact_mono:

      m ≤ n ==> fact m ≤ fact n

lemma fact_less_mono:

      [| 0 < m; m < n |] ==> fact m < fact n

lemma inv_real_of_nat_fact_gt_zero:

      0 < inverse (real (fact n))

lemma inv_real_of_nat_fact_ge_zero:

      0 ≤ inverse (real (fact n))

lemma fact_diff_Suc:

      n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)

lemma fact_num0:

      fact 0 = 1

lemma fact_num_eq_if:

      fact m = (if m = 0 then 1 else m * fact (m - 1))

lemma fact_add_num_eq_if:

      fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))

lemma fact_add_num_eq_if2:

      fact (m + n) = (if m = 0 then fact n else (m + n) * fact (m - 1 + n))