src/HOL/Fact.thy
author haftmann
Wed, 03 Dec 2008 15:58:44 +0100
changeset 28952 15a4b2cf8c34
parent 28944 src/HOL/Hyperreal/Fact.thy@e27abf0db984
child 29693 708dcf7dec9f
permissions -rw-r--r--
made repository layout more coherent with logical distribution structure; stripped some $Id$s
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
     1
(*  Title       : Fact.thy
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     5
*)
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     6
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
     7
header{*Factorial Function*}
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15094
diff changeset
     9
theory Fact
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
    10
imports RealDef
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15094
diff changeset
    11
begin
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    12
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    13
consts fact :: "nat => nat"
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    14
primrec
19765
dfe940911617 misc cleanup;
wenzelm
parents: 15241
diff changeset
    15
  fact_0:     "fact 0 = 1"
dfe940911617 misc cleanup;
wenzelm
parents: 15241
diff changeset
    16
  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    17
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    18
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    19
lemma fact_gt_zero [simp]: "0 < fact n"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    20
by (induct n) auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    21
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    22
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    23
by simp
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    24
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    25
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    26
by auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    27
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    28
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    29
by auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    30
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    31
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    32
by simp
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    33
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    34
lemma fact_ge_one [simp]: "1 \<le> fact n"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    35
by (induct n) auto
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    36
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    37
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    38
apply (drule le_imp_less_or_eq)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    39
apply (auto dest!: less_imp_Suc_add)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    40
apply (induct_tac k, auto)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    41
done
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    42
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    43
text{*Note that @{term "fact 0 = fact 1"}*}
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    44
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    45
apply (drule_tac m = m in less_imp_Suc_add, auto)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    46
apply (induct_tac k, auto)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    47
done
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    48
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    49
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    50
by (auto simp add: positive_imp_inverse_positive)
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    51
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    52
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    53
by (auto intro: order_less_imp_le)
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    54
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    55
lemma fact_diff_Suc [rule_format]:
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    56
  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    57
apply (induct n arbitrary: m)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    58
apply auto
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    59
apply (drule_tac x = "m - 1" in meta_spec, auto)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    60
done
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    61
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    62
lemma fact_num0 [simp]: "fact 0 = 1"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    63
by auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    64
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    65
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    66
by (cases m) auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    67
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    68
lemma fact_add_num_eq_if:
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    69
  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    70
by (cases "m + n") auto
15094
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    71
a7d1a3fdc30d conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents: 12196
diff changeset
    72
lemma fact_add_num_eq_if2:
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    73
  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
    74
by (cases m) auto
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
    75
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15094
diff changeset
    76
end