Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
--- a/src/HOL/Fact.thy Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Fact.thy Fri Jul 10 10:45:30 2009 -0400
@@ -2,25 +2,266 @@
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+ The integer version of factorial and other additions by Jeremy Avigad.
*)
header{*Factorial Function*}
theory Fact
-imports Main
+imports NatTransfer
begin
-consts fact :: "nat => nat"
-primrec
- fact_0: "fact 0 = 1"
- fact_Suc: "fact (Suc n) = (Suc n) * fact n"
+class fact =
+
+fixes
+ fact :: "'a \<Rightarrow> 'a"
+
+instantiation nat :: fact
+
+begin
+
+fun
+ fact_nat :: "nat \<Rightarrow> nat"
+where
+ fact_0_nat: "fact_nat 0 = Suc 0"
+| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
+
+instance proof qed
+
+end
+
+(* definitions for the integers *)
+
+instantiation int :: fact
+
+begin
+
+definition
+ fact_int :: "int \<Rightarrow> int"
+where
+ "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up Transfer *}
+
+lemma transfer_nat_int_factorial:
+ "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
+ unfolding fact_int_def
+ by auto
+
+
+lemma transfer_nat_int_factorial_closure:
+ "x >= (0::int) \<Longrightarrow> fact x >= 0"
+ by (auto simp add: fact_int_def)
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_factorial transfer_nat_int_factorial_closure]
+
+lemma transfer_int_nat_factorial:
+ "fact (int x) = int (fact x)"
+ unfolding fact_int_def by auto
+
+lemma transfer_int_nat_factorial_closure:
+ "is_nat x \<Longrightarrow> fact x >= 0"
+ by (auto simp add: fact_int_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_factorial transfer_int_nat_factorial_closure]
-lemma fact_gt_zero [simp]: "0 < fact n"
-by (induct n) auto
+subsection {* Factorial *}
+
+lemma fact_0_int [simp]: "fact (0::int) = 1"
+ by (simp add: fact_int_def)
+
+lemma fact_1_nat [simp]: "fact (1::nat) = 1"
+ by simp
+
+lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
+ by simp
+
+lemma fact_1_int [simp]: "fact (1::int) = 1"
+ by (simp add: fact_int_def)
+
+lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
+ by simp
+
+lemma fact_plus_one_int:
+ assumes "n >= 0"
+ shows "fact ((n::int) + 1) = (n + 1) * fact n"
+
+ using prems unfolding fact_int_def
+ by (simp add: nat_add_distrib algebra_simps int_mult)
+
+lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+ apply (subgoal_tac "n = Suc (n - 1)")
+ apply (erule ssubst)
+ apply (subst fact_Suc_nat)
+ apply simp_all
+done
+
+lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+ apply (subgoal_tac "n = (n - 1) + 1")
+ apply (erule ssubst)
+ apply (subst fact_plus_one_int)
+ apply simp_all
+done
+
+lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
+ apply (induct n)
+ apply (auto simp add: fact_plus_one_nat)
+done
+
+lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
+ by (simp add: fact_int_def)
+
+lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
+ by (insert fact_nonzero_nat [of n], arith)
+
+lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
+ by (auto simp add: fact_int_def)
+
+lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
+ by (insert fact_nonzero_nat [of n], arith)
+
+lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
+ by (insert fact_nonzero_nat [of n], arith)
+
+lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
+ apply (auto simp add: fact_int_def)
+ apply (subgoal_tac "1 = int 1")
+ apply (erule ssubst)
+ apply (subst zle_int)
+ apply auto
+done
+
+lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
+ apply (induct n)
+ apply force
+ apply (auto simp only: fact_Suc_nat)
+ apply (subgoal_tac "m = Suc n")
+ apply (erule ssubst)
+ apply (rule dvd_triv_left)
+ apply auto
+done
+
+lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
+ apply (case_tac "1 <= n")
+ apply (induct n rule: int_ge_induct)
+ apply (auto simp add: fact_plus_one_int)
+ apply (subgoal_tac "m = i + 1")
+ apply auto
+done
+
+lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
+ {i..j+1} = {i..j} Un {j+1}"
+ by auto
+
+lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
+ by auto
+
+lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
+ by auto
-lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by simp
+lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
+ apply (induct n)
+ apply force
+ apply (subst fact_Suc_nat)
+ apply (subst interval_Suc)
+ apply auto
+done
+
+lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
+ apply (induct n rule: int_ge_induct)
+ apply force
+ apply (subst fact_plus_one_int, assumption)
+ apply (subst interval_plus_one_int)
+ apply auto
+done
+
+lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k, auto)
+done
+
+lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
+ unfolding fact_int_def by auto
+
+lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
+ apply (case_tac "m >= 0")
+ apply auto
+ apply (frule fact_gt_zero_int)
+ apply arith
+done
+
+lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
+ fact (m + k) >= fact m"
+ apply (case_tac "m < 0")
+ apply auto
+ apply (induct k rule: int_ge_induct)
+ apply auto
+ apply (subst add_assoc [symmetric])
+ apply (subst fact_plus_one_int)
+ apply auto
+ apply (erule order_trans)
+ apply (subst mult_le_cancel_right1)
+ apply (subgoal_tac "fact (m + i) >= 0")
+ apply arith
+ apply auto
+done
+
+lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
+ apply (insert fact_mono_int_aux [of "n - m" "m"])
+ apply auto
+done
+
+text{*Note that @{term "fact 0 = fact 1"}*}
+lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac k, auto)
+done
+
+lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
+ fact m < fact ((m + 1) + k)"
+ apply (induct k rule: int_ge_induct)
+ apply (simp add: fact_plus_one_int)
+ apply (subst mult_less_cancel_right1)
+ apply (insert fact_gt_zero_int [of m], arith)
+ apply (subst (2) fact_reduce_int)
+ apply (auto simp add: add_ac)
+ apply (erule order_less_le_trans)
+ apply (subst mult_le_cancel_right1)
+ apply auto
+ apply (subgoal_tac "fact (i + (1 + m)) >= 0")
+ apply force
+ apply (rule fact_ge_zero_int)
+done
+
+lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
+ apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
+ apply auto
+done
+
+lemma fact_num_eq_if_nat: "fact (m::nat) =
+ (if m=0 then 1 else m * fact (m - 1))"
+by (cases m) auto
+
+lemma fact_add_num_eq_if_nat:
+ "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+by (cases "m + n") auto
+
+lemma fact_add_num_eq_if2_nat:
+ "fact ((m::nat) + n) =
+ (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+by (cases m) auto
+
+
+subsection {* fact and of_nat *}
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
by auto
@@ -33,46 +274,10 @@
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
by simp
-lemma fact_ge_one [simp]: "1 \<le> fact n"
-by (induct n) auto
-
-lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
-apply (drule le_imp_less_or_eq)
-apply (auto dest!: less_imp_Suc_add)
-apply (induct_tac k, auto)
-done
-
-text{*Note that @{term "fact 0 = fact 1"}*}
-lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
-apply (drule_tac m = m in less_imp_Suc_add, auto)
-apply (induct_tac k, auto)
-done
-
lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
by (auto simp add: positive_imp_inverse_positive)
lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
by (auto intro: order_less_imp_le)
-lemma fact_diff_Suc [rule_format]:
- "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-apply (induct n arbitrary: m)
-apply auto
-apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
-done
-
-lemma fact_num0: "fact 0 = 1"
-by auto
-
-lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
-by (cases m) auto
-
-lemma fact_add_num_eq_if:
- "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
-by (cases "m + n") auto
-
-lemma fact_add_num_eq_if2:
- "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
-by (cases m) auto
-
end
--- a/src/HOL/GCD.thy Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/GCD.thy Fri Jul 10 10:45:30 2009 -0400
@@ -20,6 +20,9 @@
the congruence relations on the integers. The notion was extended to
the natural numbers by Chiaeb.
+Jeremy Avigad combined all of these, made everything uniform for the
+natural numbers and the integers, and added a number of new theorems.
+
Tobias Nipkow cleaned up a lot.
*)
@@ -27,7 +30,7 @@
header {* GCD *}
theory GCD
-imports NatTransfer
+imports Fact
begin
declare One_nat_def [simp del]
@@ -1730,4 +1733,42 @@
ultimately show ?thesis by blast
qed
+subsection {* Infinitely many primes *}
+
+lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
+proof-
+ have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
+ from prime_factor_nat [OF f1]
+ obtain p where "prime p" and "p dvd fact n + 1" by auto
+ hence "p \<le> fact n + 1"
+ by (intro dvd_imp_le, auto)
+ {assume "p \<le> n"
+ from `prime p` have "p \<ge> 1"
+ by (cases p, simp_all)
+ with `p <= n` have "p dvd fact n"
+ by (intro dvd_fact_nat)
+ with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
+ by (rule dvd_diff_nat)
+ hence "p dvd 1" by simp
+ hence "p <= 1" by auto
+ moreover from `prime p` have "p > 1" by auto
+ ultimately have False by auto}
+ hence "n < p" by arith
+ with `prime p` and `p <= fact n + 1` show ?thesis by auto
+qed
+
+lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
+using next_prime_bound by auto
+
+lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
+proof
+ assume "finite {(p::nat). prime p}"
+ with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
+ by auto
+ then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
+ by auto
+ with bigger_prime [of b] show False by auto
+qed
+
+
end
--- a/src/HOL/NewNumberTheory/Binomial.thy Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/NewNumberTheory/Binomial.thy Fri Jul 10 10:45:30 2009 -0400
@@ -2,7 +2,7 @@
Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
-Defines factorial and the "choose" function, and establishes basic properties.
+Defines the "choose" function, and establishes basic properties.
The original theory "Binomial" was by Lawrence C. Paulson, based on
the work of Andy Gordon and Florian Kammueller. The approach here,
@@ -16,7 +16,7 @@
header {* Binomial *}
theory Binomial
-imports Cong
+imports Cong Fact
begin
@@ -25,7 +25,6 @@
class binomial =
fixes
- fact :: "'a \<Rightarrow> 'a" and
binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
(* definitions for the natural numbers *)
@@ -35,13 +34,6 @@
begin
fun
- fact_nat :: "nat \<Rightarrow> nat"
-where
- "fact_nat x =
- (if x = 0 then 1 else
- x * fact(x - 1))"
-
-fun
binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"binomial_nat n k =
@@ -60,11 +52,6 @@
begin
definition
- fact_int :: "int \<Rightarrow> int"
-where
- "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
-
-definition
binomial_int :: "int => int \<Rightarrow> int"
where
"binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
@@ -76,182 +63,29 @@
subsection {* Set up Transfer *}
-
lemma transfer_nat_int_binomial:
- "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
"(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) =
nat (binomial n k)"
- unfolding fact_int_def binomial_int_def
+ unfolding binomial_int_def
by auto
-
-lemma transfer_nat_int_binomial_closures:
- "x >= (0::int) \<Longrightarrow> fact x >= 0"
+lemma transfer_nat_int_binomial_closure:
"n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
- by (auto simp add: fact_int_def binomial_int_def)
+ by (auto simp add: binomial_int_def)
declare TransferMorphism_nat_int[transfer add return:
- transfer_nat_int_binomial transfer_nat_int_binomial_closures]
+ transfer_nat_int_binomial transfer_nat_int_binomial_closure]
lemma transfer_int_nat_binomial:
- "fact (int x) = int (fact x)"
"binomial (int n) (int k) = int (binomial n k)"
unfolding fact_int_def binomial_int_def by auto
-lemma transfer_int_nat_binomial_closures:
- "is_nat x \<Longrightarrow> fact x >= 0"
+lemma transfer_int_nat_binomial_closure:
"is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
- by (auto simp add: fact_int_def binomial_int_def)
+ by (auto simp add: binomial_int_def)
declare TransferMorphism_int_nat[transfer add return:
- transfer_int_nat_binomial transfer_int_nat_binomial_closures]
-
-
-subsection {* Factorial *}
-
-lemma fact_zero_nat [simp]: "fact (0::nat) = 1"
- by simp
-
-lemma fact_zero_int [simp]: "fact (0::int) = 1"
- by (simp add: fact_int_def)
-
-lemma fact_one_nat [simp]: "fact (1::nat) = 1"
- by simp
-
-lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
- by (simp add: One_nat_def)
-
-lemma fact_one_int [simp]: "fact (1::int) = 1"
- by (simp add: fact_int_def)
-
-lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
- by simp
-
-lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n"
- by (simp add: One_nat_def)
-
-lemma fact_plus_one_int:
- assumes "n >= 0"
- shows "fact ((n::int) + 1) = (n + 1) * fact n"
-
- using prems by (rule fact_plus_one_nat [transferred])
-
-lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
- by simp
-
-lemma fact_reduce_int:
- assumes "(n::int) > 0"
- shows "fact n = n * fact (n - 1)"
-
- using prems apply (subst tsub_eq [symmetric], auto)
- apply (rule fact_reduce_nat [transferred])
- using prems apply auto
-done
-
-declare fact_nat.simps [simp del]
-
-lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
- apply (induct n rule: induct'_nat)
- apply (auto simp add: fact_plus_one_nat)
-done
-
-lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
- by (simp add: fact_int_def)
-
-lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
- by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
- by (auto simp add: fact_int_def)
-
-lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
- by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
- by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
- apply (auto simp add: fact_int_def)
- apply (subgoal_tac "1 = int 1")
- apply (erule ssubst)
- apply (subst zle_int)
- apply auto
-done
-
-lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
- apply (induct n rule: induct'_nat)
- apply (auto simp add: fact_plus_one_nat)
- apply (subgoal_tac "m = n + 1")
- apply auto
-done
-
-lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
- apply (case_tac "1 <= n")
- apply (induct n rule: int_ge_induct)
- apply (auto simp add: fact_plus_one_int)
- apply (subgoal_tac "m = i + 1")
- apply auto
-done
-
-lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
- {i..j+1} = {i..j} Un {j+1}"
- by auto
-
-lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
- by auto
-
-lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
- apply (induct n rule: induct'_nat)
- apply force
- apply (subst fact_plus_one_nat)
- apply (subst interval_plus_one_nat)
- apply auto
-done
-
-lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
- apply (induct n rule: int_ge_induct)
- apply force
- apply (subst fact_plus_one_int, assumption)
- apply (subst interval_plus_one_int)
- apply auto
-done
-
-subsection {* Infinitely many primes *}
-
-lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
-proof-
- have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
- from prime_factor_nat [OF f1]
- obtain p where "prime p" and "p dvd fact n + 1" by auto
- hence "p \<le> fact n + 1"
- by (intro dvd_imp_le, auto)
- {assume "p \<le> n"
- from `prime p` have "p \<ge> 1"
- by (cases p, simp_all)
- with `p <= n` have "p dvd fact n"
- by (intro dvd_fact_nat)
- with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
- by (rule dvd_diff_nat)
- hence "p dvd 1" by simp
- hence "p <= 1" by auto
- moreover from `prime p` have "p > 1" by auto
- ultimately have False by auto}
- hence "n < p" by arith
- with `prime p` and `p <= fact n + 1` show ?thesis by auto
-qed
-
-lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
-using next_prime_bound by auto
-
-lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
-proof
- assume "finite {(p::nat). prime p}"
- with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
- by auto
- then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
- by auto
- with bigger_prime [of b] show False by auto
-qed
+ transfer_int_nat_binomial transfer_int_nat_binomial_closure]
subsection {* Binomial coefficients *}
--- a/src/HOL/Transcendental.thy Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Transcendental.thy Fri Jul 10 10:45:30 2009 -0400
@@ -621,19 +621,19 @@
subsection{* Some properties of factorials *}
-lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
+lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
by auto
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
+lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
by auto
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
+lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
by simp
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
+lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
by (auto simp add: positive_imp_inverse_positive)
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
+lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
by (auto intro: order_less_imp_le)
subsection {* Derivability of power series *}
@@ -1604,11 +1604,11 @@
apply (rotate_tac 2)
apply (drule sin_paired [THEN sums_unique, THEN ssubst])
unfolding One_nat_def
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
apply (frule sums_unique)
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
apply (erule sums_summable)
apply (case_tac "m=0")
apply (simp (no_asm_simp))
@@ -1617,24 +1617,24 @@
apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
apply (subgoal_tac "x*x < 2*3", simp)
apply (rule mult_strict_mono)
-apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
+apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse del: fact_Suc)
-apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
+apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
-apply (auto simp add: mult_assoc simp del: fact_Suc)
+apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
-apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
+apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
apply (erule ssubst)+
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
apply (subgoal_tac "0 < x ^ (4 * m) ")
prefer 2 apply (simp only: zero_less_power)
apply (simp (no_asm_simp) add: mult_less_cancel_left)
@@ -1670,24 +1670,24 @@
apply (rule_tac y =
"\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
in order_less_trans)
-apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc)
+apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
unfolding One_nat_def
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
- del: fact_Suc)
+ del: fact_Suc_nat)
apply (rule real_mult_inverse_cancel2)
apply (rule real_of_nat_fact_gt_zero)+
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
+apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
apply (subst fact_lemma)
-apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
apply (simp only: real_of_nat_mult)
apply (rule mult_strict_mono, force)
apply (rule_tac [3] real_of_nat_ge_zero)
prefer 2 apply force
apply (rule real_of_nat_less_iff [THEN iffD2])
-apply (rule fact_less_mono, auto)
+apply (rule fact_less_mono_nat, auto)
done
lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]