src/HOL/Hyperreal/Fact.thy
author chaieb
Sat Oct 20 12:09:33 2007 +0200 (2007-10-20)
changeset 25112 98824cc791c0
parent 20503 503ac4c5ef91
child 25134 3d4953e88449
permissions -rw-r--r--
fixed proofs
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
nipkow@15131
     9
theory Fact
paulson@15241
    10
imports "../Real/Real"
nipkow@15131
    11
begin
paulson@15094
    12
paulson@15094
    13
consts fact :: "nat => nat"
paulson@15094
    14
primrec
wenzelm@19765
    15
  fact_0:     "fact 0 = 1"
wenzelm@19765
    16
  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
paulson@15094
    17
paulson@15094
    18
paulson@15094
    19
lemma fact_gt_zero [simp]: "0 < fact n"
wenzelm@19765
    20
  by (induct n) auto
paulson@15094
    21
paulson@15094
    22
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
chaieb@25112
    23
  by (simp add: neq0_conv)
paulson@15094
    24
paulson@15094
    25
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
wenzelm@19765
    26
  by auto
paulson@15094
    27
paulson@15094
    28
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
wenzelm@19765
    29
  by auto
paulson@15094
    30
paulson@15094
    31
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
wenzelm@19765
    32
  by simp
paulson@15094
    33
paulson@15094
    34
lemma fact_ge_one [simp]: "1 \<le> fact n"
wenzelm@19765
    35
  by (induct n) auto
paulson@12196
    36
paulson@15094
    37
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
wenzelm@19765
    38
  apply (drule le_imp_less_or_eq)
wenzelm@19765
    39
  apply (auto dest!: less_imp_Suc_add)
wenzelm@19765
    40
  apply (induct_tac k, auto)
wenzelm@19765
    41
  done
paulson@15094
    42
paulson@15094
    43
text{*Note that @{term "fact 0 = fact 1"}*}
paulson@15094
    44
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
wenzelm@19765
    45
  apply (drule_tac m = m in less_imp_Suc_add, auto)
wenzelm@19765
    46
  apply (induct_tac k, auto)
wenzelm@19765
    47
  done
paulson@15094
    48
paulson@15094
    49
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
wenzelm@19765
    50
  by (auto simp add: positive_imp_inverse_positive)
paulson@15094
    51
paulson@15094
    52
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
wenzelm@19765
    53
  by (auto intro: order_less_imp_le)
paulson@15094
    54
paulson@15094
    55
lemma fact_diff_Suc [rule_format]:
wenzelm@19765
    56
    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
wenzelm@20503
    57
  apply (induct n arbitrary: m)
wenzelm@19765
    58
  apply auto
wenzelm@19765
    59
  apply (drule_tac x = "m - 1" in meta_spec, auto)
wenzelm@19765
    60
  done
paulson@15094
    61
paulson@15094
    62
lemma fact_num0 [simp]: "fact 0 = 1"
wenzelm@19765
    63
  by auto
paulson@15094
    64
paulson@15094
    65
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
wenzelm@19765
    66
  by (cases m) auto
paulson@15094
    67
paulson@15094
    68
lemma fact_add_num_eq_if:
wenzelm@19765
    69
    "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
wenzelm@19765
    70
  by (cases "m + n") auto
paulson@15094
    71
paulson@15094
    72
lemma fact_add_num_eq_if2:
wenzelm@19765
    73
    "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
wenzelm@19765
    74
  by (cases m) auto
paulson@12196
    75
nipkow@15131
    76
end