src/HOL/Fact.thy
changeset 29693 708dcf7dec9f
parent 28952 15a4b2cf8c34
child 30073 a4ad0c08b7d9
child 30240 5b25fee0362c
equal deleted inserted replaced
29692:121289b1ae27 29693:708dcf7dec9f
     5 *)
     5 *)
     6 
     6 
     7 header{*Factorial Function*}
     7 header{*Factorial Function*}
     8 
     8 
     9 theory Fact
     9 theory Fact
    10 imports RealDef
    10 imports Nat
    11 begin
    11 begin
    12 
    12 
    13 consts fact :: "nat => nat"
    13 consts fact :: "nat => nat"
    14 primrec
    14 primrec
    15   fact_0:     "fact 0 = 1"
    15   fact_0:     "fact 0 = 1"
    20 by (induct n) auto
    20 by (induct n) auto
    21 
    21 
    22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    23 by simp
    23 by simp
    24 
    24 
    25 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    25 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
    26 by auto
    26 by auto
    27 
    27 
    28 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    28 class ordered_semiring_1 = ordered_semiring + semiring_1
    29 by auto
    29 class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
    30 
    30 
    31 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    31 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
       
    32 
       
    33 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
    32 by simp
    34 by simp
    33 
    35 
    34 lemma fact_ge_one [simp]: "1 \<le> fact n"
    36 lemma fact_ge_one [simp]: "1 \<le> fact n"
    35 by (induct n) auto
    37 by (induct n) auto
    36 
    38 
    44 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    46 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    45 apply (drule_tac m = m in less_imp_Suc_add, auto)
    47 apply (drule_tac m = m in less_imp_Suc_add, auto)
    46 apply (induct_tac k, auto)
    48 apply (induct_tac k, auto)
    47 done
    49 done
    48 
    50 
    49 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    51 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
    50 by (auto simp add: positive_imp_inverse_positive)
    52 by (auto simp add: positive_imp_inverse_positive)
    51 
    53 
    52 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    54 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
    53 by (auto intro: order_less_imp_le)
    55 by (auto intro: order_less_imp_le)
    54 
    56 
    55 lemma fact_diff_Suc [rule_format]:
    57 lemma fact_diff_Suc [rule_format]:
    56   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    58   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    57 apply (induct n arbitrary: m)
    59 apply (induct n arbitrary: m)
    58 apply auto
    60 apply auto
    59 apply (drule_tac x = "m - 1" in meta_spec, auto)
    61 apply (drule_tac x = "m - 1" in meta_spec, auto)
    60 done
    62 done
    61 
    63 
    62 lemma fact_num0 [simp]: "fact 0 = 1"
    64 lemma fact_num0: "fact 0 = 1"
    63 by auto
    65 by auto
    64 
    66 
    65 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    67 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    66 by (cases m) auto
    68 by (cases m) auto
    67 
    69