src/HOL/Fact.thy
author blanchet
Wed Mar 04 10:45:52 2009 +0100 (2009-03-04)
changeset 30240 5b25fee0362c
parent 29693 708dcf7dec9f
child 30242 aea5d7fa7ef5
permissions -rw-r--r--
Merge.
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
blanchet@30240
    10
imports Main
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"
nipkow@25134
    20
by (induct n) auto
paulson@15094
    21
paulson@15094
    22
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
nipkow@25162
    23
by simp
paulson@15094
    24
chaieb@29693
    25
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
nipkow@25134
    26
by auto
paulson@15094
    27
chaieb@29693
    28
class ordered_semiring_1 = ordered_semiring + semiring_1
chaieb@29693
    29
class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
paulson@15094
    30
chaieb@29693
    31
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
chaieb@29693
    32
chaieb@29693
    33
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
nipkow@25134
    34
by simp
paulson@15094
    35
paulson@15094
    36
lemma fact_ge_one [simp]: "1 \<le> fact n"
nipkow@25134
    37
by (induct n) auto
paulson@12196
    38
paulson@15094
    39
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
nipkow@25134
    40
apply (drule le_imp_less_or_eq)
nipkow@25134
    41
apply (auto dest!: less_imp_Suc_add)
nipkow@25134
    42
apply (induct_tac k, auto)
nipkow@25134
    43
done
paulson@15094
    44
paulson@15094
    45
text{*Note that @{term "fact 0 = fact 1"}*}
paulson@15094
    46
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
nipkow@25134
    47
apply (drule_tac m = m in less_imp_Suc_add, auto)
nipkow@25134
    48
apply (induct_tac k, auto)
nipkow@25134
    49
done
paulson@15094
    50
chaieb@29693
    51
lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
nipkow@25134
    52
by (auto simp add: positive_imp_inverse_positive)
paulson@15094
    53
chaieb@29693
    54
lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
nipkow@25134
    55
by (auto intro: order_less_imp_le)
paulson@15094
    56
paulson@15094
    57
lemma fact_diff_Suc [rule_format]:
nipkow@25134
    58
  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
nipkow@25134
    59
apply (induct n arbitrary: m)
nipkow@25134
    60
apply auto
blanchet@30240
    61
apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
nipkow@25134
    62
done
paulson@15094
    63
chaieb@29693
    64
lemma fact_num0: "fact 0 = 1"
nipkow@25134
    65
by auto
paulson@15094
    66
paulson@15094
    67
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
nipkow@25134
    68
by (cases m) auto
paulson@15094
    69
paulson@15094
    70
lemma fact_add_num_eq_if:
nipkow@25134
    71
  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
nipkow@25134
    72
by (cases "m + n") auto
paulson@15094
    73
paulson@15094
    74
lemma fact_add_num_eq_if2:
nipkow@25134
    75
  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
nipkow@25134
    76
by (cases m) auto
paulson@12196
    77
nipkow@15131
    78
end