src/HOL/Hyperreal/Fact.thy
author paulson
Sat Jul 31 20:54:23 2004 +0200 (2004-07-31)
changeset 15094 a7d1a3fdc30d
parent 12196 a3be6b3a9c0b
child 15131 c69542757a4d
permissions -rw-r--r--
conversion of Hyperreal/{Fact,Filter} to Isar scripts
     1 (*  Title       : Fact.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{*Factorial Function*}
     8 
     9 theory Fact = Real:
    10 
    11 consts fact :: "nat => nat"
    12 primrec
    13    fact_0:     "fact 0 = 1"
    14    fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
    15 
    16 
    17 lemma fact_gt_zero [simp]: "0 < fact n"
    18 by (induct "n", auto)
    19 
    20 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    21 by simp
    22 
    23 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    24 by auto
    25 
    26 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    27 by auto
    28 
    29 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    30 by simp
    31 
    32 lemma fact_ge_one [simp]: "1 \<le> fact n"
    33 by (induct "n", auto)
    34 
    35 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
    36 apply (drule le_imp_less_or_eq)
    37 apply (auto dest!: less_imp_Suc_add)
    38 apply (induct_tac "k", auto)
    39 done
    40 
    41 text{*Note that @{term "fact 0 = fact 1"}*}
    42 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    43 apply (drule_tac m = m in less_imp_Suc_add, auto)
    44 apply (induct_tac "k", auto)
    45 done
    46 
    47 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    48 by (auto simp add: positive_imp_inverse_positive)
    49 
    50 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    51 by (auto intro: order_less_imp_le)
    52 
    53 lemma fact_diff_Suc [rule_format]:
    54      "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    55 apply (induct n, auto)
    56 apply (drule_tac x = "m - 1" in spec, auto)
    57 done
    58 
    59 lemma fact_num0 [simp]: "fact 0 = 1"
    60 by auto
    61 
    62 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    63 by (case_tac "m", auto)
    64 
    65 lemma fact_add_num_eq_if:
    66      "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
    67 by (case_tac "m+n", auto)
    68 
    69 lemma fact_add_num_eq_if2:
    70      "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
    71 by (case_tac "m", auto)
    72 
    73 
    74 end