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