author chaieb Fri Jan 30 12:48:56 2009 +0000 (2009-01-30) changeset 29693 708dcf7dec9f parent 29692 121289b1ae27 child 29694 2f2558d7bc3e
moved upwards in thy graph, real related theorems moved to Transcendental.thy
 src/HOL/Fact.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Fact.thy	Thu Jan 29 22:29:44 2009 +0100
1.2 +++ b/src/HOL/Fact.thy	Fri Jan 30 12:48:56 2009 +0000
1.3 @@ -7,7 +7,7 @@
1.4  header{*Factorial Function*}
1.5
1.6  theory Fact
1.7 -imports RealDef
1.8 +imports Nat
1.9  begin
1.10
1.11  consts fact :: "nat => nat"
1.12 @@ -22,13 +22,15 @@
1.13  lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
1.14  by simp
1.15
1.16 -lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
1.17 +lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
1.18  by auto
1.19
1.20 -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
1.21 -by auto
1.22 +class ordered_semiring_1 = ordered_semiring + semiring_1
1.23 +class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
1.24
1.25 -lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
1.26 +lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
1.27 +
1.28 +lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
1.29  by simp
1.30
1.31  lemma fact_ge_one [simp]: "1 \<le> fact n"
1.32 @@ -46,10 +48,10 @@
1.33  apply (induct_tac k, auto)
1.34  done
1.35
1.36 -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
1.37 +lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
1.38  by (auto simp add: positive_imp_inverse_positive)
1.39
1.40 -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
1.41 +lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
1.42  by (auto intro: order_less_imp_le)
1.43
1.44  lemma fact_diff_Suc [rule_format]:
1.45 @@ -59,7 +61,7 @@
1.46  apply (drule_tac x = "m - 1" in meta_spec, auto)
1.47  done
1.48
1.49 -lemma fact_num0 [simp]: "fact 0 = 1"
1.50 +lemma fact_num0: "fact 0 = 1"
1.51  by auto
1.52
1.53  lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
```