moved upwards in thy graph, real related theorems moved to Transcendental.thy
authorchaieb
Fri Jan 30 12:48:56 2009 +0000 (2009-01-30)
changeset 29693708dcf7dec9f
parent 29692 121289b1ae27
child 29694 2f2558d7bc3e
moved upwards in thy graph, real related theorems moved to Transcendental.thy
src/HOL/Fact.thy
     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))"