src/HOL/Fact.thy
 author huffman Tue Feb 24 11:12:58 2009 -0800 (2009-02-24) changeset 30082 43c5b7bfc791 parent 30073 a4ad0c08b7d9 child 30242 aea5d7fa7ef5 permissions -rw-r--r--
make more proofs work whether or not One_nat_def is a simp rule
```     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
```
```    10 imports Main
```
```    11 begin
```
```    12
```
```    13 consts fact :: "nat => nat"
```
```    14 primrec
```
```    15   fact_0:     "fact 0 = 1"
```
```    16   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
```
```    17
```
```    18
```
```    19 lemma fact_gt_zero [simp]: "0 < fact n"
```
```    20 by (induct n) auto
```
```    21
```
```    22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
```
```    23 by simp
```
```    24
```
```    25 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
```
```    26 by auto
```
```    27
```
```    28 class ordered_semiring_1 = ordered_semiring + semiring_1
```
```    29 class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
```
```    30
```
```    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)"
```
```    34 by simp
```
```    35
```
```    36 lemma fact_ge_one [simp]: "1 \<le> fact n"
```
```    37 by (induct n) auto
```
```    38
```
```    39 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
```
```    40 apply (drule le_imp_less_or_eq)
```
```    41 apply (auto dest!: less_imp_Suc_add)
```
```    42 apply (induct_tac k, auto)
```
```    43 done
```
```    44
```
```    45 text{*Note that @{term "fact 0 = fact 1"}*}
```
```    46 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
```
```    47 apply (drule_tac m = m in less_imp_Suc_add, auto)
```
```    48 apply (induct_tac k, auto)
```
```    49 done
```
```    50
```
```    51 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
```
```    52 by (auto simp add: positive_imp_inverse_positive)
```
```    53
```
```    54 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
```
```    55 by (auto intro: order_less_imp_le)
```
```    56
```
```    57 lemma fact_diff_Suc [rule_format]:
```
```    58   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
```
```    59 apply (induct n arbitrary: m)
```
```    60 apply auto
```
```    61 apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
```
```    62 done
```
```    63
```
```    64 lemma fact_num0: "fact 0 = 1"
```
```    65 by auto
```
```    66
```
```    67 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
```
```    68 by (cases m) auto
```
```    69
```
```    70 lemma fact_add_num_eq_if:
```
```    71   "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
```
```    72 by (cases "m + n") auto
```
```    73
```
```    74 lemma fact_add_num_eq_if2:
```
```    75   "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
```
```    76 by (cases m) auto
```
```    77
```
```    78 end
```