--- a/src/HOL/Fact.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/Fact.thy Fri Jul 17 23:13:50 2009 +0200
@@ -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 {* @{term fact} and @{term 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 Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/GCD.thy Fri Jul 17 23:13:50 2009 +0200
@@ -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]
@@ -1777,4 +1780,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/Library/Binomial.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Fri Jul 17 23:13:50 2009 +0200
@@ -243,14 +243,8 @@
ultimately show ?thesis by blast
qed
-lemma fact_setprod: "fact n = setprod id {1 .. n}"
- apply (induct n, simp)
- apply (simp only: fact_Suc atLeastAtMostSuc_conv)
- apply (subst setprod_insert)
- by simp_all
-
lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
- unfolding fact_setprod
+ unfolding fact_altdef_nat
apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
apply (rule setprod_reindex_cong[where f=Suc])
@@ -347,7 +341,7 @@
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
using binomial_fact_lemma[OF kn]
- by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
+ by (simp add: field_simps of_nat_mult[symmetric])
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
proof-
@@ -377,7 +371,7 @@
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
- apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
+ apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult_assoc[symmetric]
unfolding setprod_timesf[symmetric]
@@ -404,7 +398,7 @@
proof-
have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
- pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
+ pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc
by (simp add: field_simps del: of_nat_Suc)
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
by (simp add: ring_simps)
@@ -420,7 +414,7 @@
lemma gbinomial_mult_fact:
"(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
unfolding gbinomial_Suc
- by (simp_all add: field_simps del: fact_Suc)
+ by (simp_all add: field_simps del: fact_Suc_nat)
lemma gbinomial_mult_fact':
"((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
@@ -438,9 +432,9 @@
have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
unfolding h
- apply (simp add: ring_simps del: fact_Suc)
+ apply (simp add: ring_simps del: fact_Suc_nat)
unfolding gbinomial_mult_fact'
- apply (subst fact_Suc)
+ apply (subst fact_Suc_nat)
unfolding of_nat_mult
apply (subst mult_commute)
unfolding mult_assoc
@@ -455,7 +449,7 @@
by simp
also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
unfolding gbinomial_mult_fact ..
- finally have ?thesis by (simp del: fact_Suc) }
+ finally have ?thesis by (simp del: fact_Suc_nat) }
ultimately show ?thesis by (cases k, auto)
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Jul 17 23:13:50 2009 +0200
@@ -2514,7 +2514,7 @@
proof-
{fix n
have "?l$n = ?r $ n"
- apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
+ apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
by (simp add: of_nat_mult ring_simps)}
then show ?thesis by (simp add: fps_eq_iff)
qed
@@ -2530,8 +2530,8 @@
apply (induct n)
apply simp
unfolding th
- using fact_gt_zero
- apply (simp add: field_simps del: of_nat_Suc fact.simps)
+ using fact_gt_zero_nat
+ apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
apply (drule sym)
by (simp add: ring_simps of_nat_mult power_Suc)}
note th' = this
@@ -2697,7 +2697,7 @@
also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
using en by (simp add: fps_sin_def)
also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
- unfolding fact_Suc of_nat_mult
+ unfolding fact_Suc_nat of_nat_mult
by (simp add: field_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2721,7 +2721,7 @@
also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
using en by (simp add: fps_cos_def)
also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
- unfolding fact_Suc of_nat_mult
+ unfolding fact_Suc_nat of_nat_mult
by (simp add: field_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2747,9 +2747,6 @@
finally show ?thesis .
qed
-lemma fact_1 [simp]: "fact 1 = 1"
-unfolding One_nat_def fact_Suc by simp
-
lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
by auto
@@ -2766,7 +2763,7 @@
"fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_sin_def
apply (cases n, simp)
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done
@@ -2779,7 +2776,7 @@
lemma fps_cos_nth_add_2:
"fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_cos_def
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done
--- a/src/HOL/Ln.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/Ln.thy Fri Jul 17 23:13:50 2009 +0200
@@ -31,13 +31,13 @@
qed
lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
- shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
+ shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
proof (induct n)
- show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <=
+ show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <=
x ^ 2 / 2 * (1 / 2) ^ 0"
by (simp add: real_of_nat_Suc power2_eq_square)
next
- fix n
+ fix n :: nat
assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
<= x ^ 2 / 2 * (1 / 2) ^ n"
show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
--- a/src/HOL/MacLaurin.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/MacLaurin.thy Fri Jul 17 23:13:50 2009 +0200
@@ -27,6 +27,10 @@
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
by arith
+lemma fact_diff_Suc [rule_format]:
+ "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+ by (subst fact_reduce_nat, auto)
+
lemma Maclaurin_lemma2:
assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
assumes n: "n = Suc k"
@@ -47,22 +51,24 @@
apply (rule_tac [2] DERIV_quotient)
apply (rule_tac [3] DERIV_const)
apply (rule_tac [2] DERIV_pow)
- prefer 3 apply (simp add: fact_diff_Suc)
+ prefer 3
+
+apply (simp add: fact_diff_Suc)
prefer 2 apply simp
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
apply (rule lemma_DERIV_subst)
apply (rule DERIV_add)
apply (rule_tac [2] DERIV_const)
apply (rule DERIV_sumr, clarify)
prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
+ apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
apply (rule DERIV_cmult)
apply (rule lemma_DERIV_subst)
apply (best intro!: DERIV_intros)
- apply (subst fact_Suc)
+ apply (subst fact_Suc_nat)
apply (subst real_of_nat_mult)
apply (simp add: mult_ac)
done
@@ -114,7 +120,7 @@
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
done
have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
@@ -174,7 +180,7 @@
(\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n"
using `difg (Suc m) t = 0`
- by (simp add: m f_h difg_def del: fact_Suc)
+ by (simp add: m f_h difg_def del: fact_Suc_nat)
qed
qed
--- a/src/HOL/NewNumberTheory/Binomial.thy Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/NewNumberTheory/Binomial.thy Fri Jul 17 23:13:50 2009 +0200
@@ -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 Fri Jul 17 23:11:40 2009 +0200
+++ b/src/HOL/Transcendental.thy Fri Jul 17 23:13:50 2009 +0200
@@ -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]