--- a/NEWS Tue Mar 17 16:38:09 2015 +0100
+++ b/NEWS Wed Mar 18 13:31:52 2015 +0100
@@ -80,6 +80,12 @@
type, so in particular on "real" and "complex" uniformly.
Minor INCOMPATIBILITY: type constraints may be needed.
+* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
+ numeric types including nat, int, real and complex. INCOMPATIBILITY:
+ an expression such as "fact 3 = 6" may require a type constraint, and the combination
+ "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
+ then use "of_nat (fact k)".
+
* removed functions "natfloor" and "natceiling",
use "nat o floor" and "nat o ceiling" instead.
A few of the lemmas have been retained and adapted: in their names
--- a/src/HOL/Binomial.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Binomial.thy Wed Mar 18 13:31:52 2015 +0100
@@ -11,182 +11,99 @@
imports Main
begin
-class fact =
- fixes fact :: "'a \<Rightarrow> 'a"
+subsection {* Factorial *}
+
+fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)"
+ where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
-instantiation nat :: fact
-begin
+lemmas fact_Suc = fact.simps(2)
+
+lemma fact_1 [simp]: "fact 1 = 1"
+ by simp
+
+lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
+ by simp
-fun
- fact_nat :: "nat \<Rightarrow> nat"
-where
- fact_0_nat: "fact_nat 0 = Suc 0"
-| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
+lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
+ by (induct n) (auto simp add: algebra_simps of_nat_mult)
+
+lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
+ by (cases n) auto
-instance ..
+lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
+ apply (induct n)
+ apply auto
+ using of_nat_eq_0_iff by fastforce
+
+lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
+ by (induct n) (auto simp: le_Suc_eq)
-end
-
-(* definitions for the integers *)
-
-instantiation int :: fact
-
+context
+ fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
begin
+
+ lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
+ by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
+
+ lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
+ by (metis le0 fact.simps(1) fact_mono)
+
+ lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
+ using fact_ge_1 less_le_trans zero_less_one by blast
+
+ lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
+ by (simp add: less_imp_le)
-definition
- fact_int :: "int \<Rightarrow> int"
-where
- "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
-
-instance proof qed
+ lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))"
+ by (simp add: not_less_iff_gr_or_eq)
+
+ lemma fact_le_power:
+ "fact n \<le> (of_nat (n^n) ::'a)"
+ proof (induct n)
+ case (Suc n)
+ then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
+ by (rule order_trans) (simp add: power_mono)
+ have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
+ by (simp add: algebra_simps)
+ also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)"
+ by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono)
+ also have "... \<le> (of_nat (Suc n ^ Suc n) ::'a)"
+ by (metis of_nat_mult order_refl power_Suc)
+ finally show ?case .
+ qed simp
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 transfer_morphism_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 transfer_morphism_int_nat[transfer add return:
- transfer_int_nat_factorial transfer_int_nat_factorial_closure]
-
-
-subsection {* Factorial *}
-
-lemma fact_0_int [simp]: "fact (0::int) = 1"
- by (simp add: fact_int_def)
+text{*Note that @{term "fact 0 = fact 1"}*}
+lemma fact_less_mono_nat: "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: nat)"
+ by (induct n) (auto simp: less_Suc_eq)
-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 assms unfolding fact_int_def
- by (simp add: nat_add_distrib algebra_simps int_mult)
+lemma fact_less_mono:
+ fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
+ shows "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a)"
+ by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
-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)
- 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_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
+ by (metis One_nat_def fact_ge_1)
-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 dvd_fact:
+ shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
+ by (induct n) (auto simp: dvdI le_Suc_eq)
-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)
- apply (subgoal_tac "m = Suc n")
- apply (erule ssubst)
- apply (rule dvd_triv_left)
- apply auto
- done
+lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
+ by (induct n) (auto simp: atLeastAtMostSuc_conv)
-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_altdef: "fact n = setprod of_nat {1..n}"
+ by (induct n) (auto simp: atLeastAtMostSuc_conv)
-lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
- apply (induct n)
- apply force
- apply (subst fact_Suc)
- apply (subst interval_Suc)
- apply auto
-done
+lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
+ by (induct m) (auto simp: le_Suc_eq)
-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_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
- by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
-
-lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
- by (auto simp add: dvd_imp_mod_0 fact_dvd)
+lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a :: {semiring_div,linordered_semidom}) = 0"
+ by (auto simp add: fact_dvd)
lemma fact_div_fact:
- assumes "m \<ge> (n :: nat)"
+ assumes "m \<ge> n"
shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
proof -
obtain d where "d = m - n" by auto
@@ -202,107 +119,17 @@
also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
also have "... = \<Prod>{n + 1..n + Suc d'}"
- by (simp add: atLeastAtMostSuc_conv setprod.insert)
+ by (simp add: atLeastAtMostSuc_conv)
finally show ?case .
qed
from this `m = n + d` show ?thesis by simp
qed
-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 (2) fact_reduce_int)
- apply (auto simp add: ac_simps)
- apply (erule order_less_le_trans)
- apply auto
- 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))"
+lemma fact_num_eq_if:
+ "fact m = (if m=0 then 1 else of_nat 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
-
-lemma fact_le_power: "fact n \<le> n^n"
-proof (induct n)
- case (Suc n)
- then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
- then show ?case by (simp add: add_le_mono)
-qed simp
-
-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
-
-lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
-
-lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
-by simp
-
-lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
-by (auto simp add: positive_imp_inverse_positive)
-
-lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
-by (auto intro: order_less_imp_le)
-
-lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
+lemma fact_eq_rev_setprod_nat: "fact k = (\<Prod>i<k. k - i)"
unfolding fact_altdef_nat
by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
@@ -317,7 +144,7 @@
lemma fact_numeral: --{*Evaluation for specific numerals*}
"fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
- by (simp add: numeral_eq_Suc)
+ by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)
text {* This development is based on the work of Andy Gordon and
@@ -532,10 +359,11 @@
lemma binomial_fact:
assumes kn: "k \<le> n"
- shows "(of_nat (n choose k) :: 'a::{field,ring_char_0}) =
- of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
+ shows "(of_nat (n choose k) :: 'a::field_char_0) =
+ (fact n) / (fact k * fact(n - k))"
using binomial_fact_lemma[OF kn]
- by (simp add: field_simps of_nat_mult [symmetric])
+ apply (simp add: field_simps)
+ by (metis mult.commute of_nat_fact of_nat_mult)
lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
using binomial [of 1 "1" n]
@@ -626,8 +454,8 @@
done
qed
-lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
- unfolding fact_altdef_nat
+lemma pochhammer_fact: "fact n = pochhammer 1 n"
+ unfolding fact_altdef
apply (cases n)
apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
apply (rule setprod.reindex_cong [where l = Suc])
@@ -711,7 +539,7 @@
by simp
lemma pochhammer_same: "pochhammer (- of_nat n) n =
- ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
+ ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)"
unfolding pochhammer_minus[OF le_refl[of n]]
by (simp add: of_nat_diff pochhammer_fact)
@@ -720,7 +548,7 @@
definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
where "a gchoose n =
- (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
+ (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
apply (simp_all add: gbinomial_def)
@@ -729,7 +557,7 @@
apply simp
done
-lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
+lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
proof (cases "n = 0")
case True
then show ?thesis by simp
@@ -743,7 +571,8 @@
eq setprod.distrib[symmetric])
qed
-lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
+lemma binomial_gbinomial:
+ "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof -
{ assume kn: "k > n"
then have ?thesis
@@ -769,10 +598,10 @@
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_altdef_nat h
+ apply (simp add: pochhammer_Suc_setprod fact_altdef h
of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
- unfolding mult.assoc[symmetric]
+ unfolding mult.assoc
unfolding setprod.distrib[symmetric]
apply simp
apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
@@ -791,40 +620,46 @@
by (simp add: gbinomial_def)
lemma gbinomial_mult_1:
- "a * (a gchoose n) =
+ fixes a :: "'a :: field_char_0"
+ shows "a * (a gchoose n) =
of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r")
proof -
- have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
+ have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
- pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
- by (simp add: field_simps del: of_nat_Suc)
+ pochhammer_Suc of_nat_mult right_diff_distrib power_Suc
+ apply (simp del: of_nat_Suc fact.simps)
+ apply (auto simp add: field_simps simp del: of_nat_Suc)
+ done
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
by (simp add: field_simps)
finally show ?thesis ..
qed
lemma gbinomial_mult_1':
- "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
+ fixes a :: "'a :: field_char_0"
+ shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
by (simp add: mult.commute gbinomial_mult_1)
lemma gbinomial_Suc:
- "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
+ "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / (fact (Suc k))"
by (simp add: gbinomial_def)
lemma gbinomial_mult_fact:
- "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
+ fixes a :: "'a::field_char_0"
+ shows
+ "fact (Suc k) * (a gchoose (Suc k)) =
(setprod (\<lambda>i. a - of_nat i) {0 .. k})"
- by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
+ by (simp_all add: gbinomial_Suc field_simps del: fact.simps)
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})"
+ fixes a :: "'a::field_char_0"
+ shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
using gbinomial_mult_fact[of k a]
by (subst mult.commute)
-
lemma gbinomial_Suc_Suc:
- "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+ fixes a :: "'a :: field_char_0"
+ shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
proof (cases k)
case 0
then show ?thesis by simp
@@ -835,31 +670,42 @@
using Suc
apply auto
done
- 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)"
- apply (simp add: Suc field_simps del: fact_Suc)
+ have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
+ (a gchoose Suc h) * (fact (Suc (Suc h))) +
+ (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
+ by (simp add: Suc field_simps del: fact.simps)
+ also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
+ (\<Prod>i = 0..Suc h. a - of_nat i)"
+ by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
+ also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
+ (\<Prod>i = 0..Suc h. a - of_nat i)"
+ by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
+ also have "... = of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
+ (\<Prod>i = 0..Suc h. a - of_nat i)"
+ by (metis gbinomial_mult_fact mult.commute)
+ also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
+ (of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
+ by (simp add: field_simps)
+ also have "... =
+ ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
unfolding gbinomial_mult_fact'
- apply (subst fact_Suc)
- unfolding of_nat_mult
- apply (subst mult.commute)
- unfolding mult.assoc
- unfolding gbinomial_mult_fact
- apply (simp add: field_simps)
- done
+ by (simp add: comm_semiring_class.distrib field_simps Suc)
also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
by (simp add: field_simps Suc)
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
using eq0
by (simp add: Suc setprod_nat_ivl_1_Suc)
- also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
+ also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
unfolding gbinomial_mult_fact ..
- finally show ?thesis by (simp del: fact_Suc)
+ finally show ?thesis
+ by (metis fact_nonzero mult_cancel_left)
qed
lemma gbinomial_reduce_nat:
- "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
-by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
+ fixes a :: "'a :: field_char_0"
+ shows "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
+ by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
lemma binomial_symmetric:
@@ -947,19 +793,16 @@
n choose k = fact n div (fact k * fact (n - k))"
by (subst binomial_fact_lemma [symmetric]) auto
-lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
-by (metis binomial_fact_lemma dvd_def)
-
-lemma choose_dvd_int:
- assumes "(0::int) <= k" and "k <= n"
- shows "fact k * fact (n - k) dvd fact n"
- apply (subst tsub_eq [symmetric], rule assms)
- apply (rule choose_dvd_nat [transferred])
- using assms apply auto
+lemma choose_dvd: "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})"
+ unfolding dvd_def
+ apply (rule exI [where x="of_nat (n choose k)"])
+ using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
+ apply (auto simp: of_nat_mult)
done
-lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
-by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
+lemma fact_fact_dvd_fact:
+ "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"
+by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
lemma choose_mult_lemma:
"((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
@@ -969,18 +812,17 @@
by (simp add: assms binomial_altdef_nat)
also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
apply (subst div_mult_div_if_dvd)
- apply (auto simp: fact_fact_dvd_fact)
+ apply (auto simp: algebra_simps fact_fact_dvd_fact)
apply (metis add.assoc add.commute fact_fact_dvd_fact)
done
also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
apply (subst div_mult_div_if_dvd [symmetric])
- apply (auto simp: fact_fact_dvd_fact)
- apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
+ apply (auto simp add: algebra_simps)
+ apply (metis fact_fact_dvd_fact dvd.order.trans nat_mult_dvd_cancel_disj)
done
also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
apply (subst div_mult_div_if_dvd)
- apply (auto simp: fact_fact_dvd_fact)
- apply(metis mult.left_commute)
+ apply (auto simp: fact_fact_dvd_fact algebra_simps)
done
finally show ?thesis
by (simp add: binomial_altdef_nat mult.commute)
@@ -1009,7 +851,7 @@
apply auto
apply (case_tac "k = Suc n")
apply auto
- apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
+ apply (metis Suc_le_eq fact.cases le_Suc_eq le_eq_less_or_eq)
done
lemma card_UNION:
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 18 13:31:52 2015 +0100
@@ -905,11 +905,11 @@
float_round_up prec (x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)))"
lemma cos_aux:
- shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
- and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
+ shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i))) * x ^(2 * i))" (is "?lb")
+ and "(\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
proof -
have "0 \<le> real (x * x)" by auto
- let "?f n" = "fact (2 * n)"
+ let "?f n" = "fact (2 * n) :: nat"
{ fix n
have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
@@ -935,15 +935,15 @@
hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
have "0 < x * x" using `0 < x` by simp
- { fix x n have "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^ (2 * i))
- = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
+ { fix x n have "(\<Sum> i=0..<n. (-1::real) ^ i * (1/(fact (2 * i))) * x ^ (2 * i))
+ = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
proof -
have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
also have "\<dots> =
- (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
+ (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / ((fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / ((fact i)) * x ^ i else 0)"
unfolding sum_split_even_odd atLeast0LessThan ..
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / ((fact i)) else 0) * x ^ i)"
by (rule setsum.cong) auto
finally show ?thesis by assumption
qed } note morph_to_if_power = this
@@ -952,8 +952,8 @@
{ fix n :: nat assume "0 < n"
hence "0 < 2 * n" by auto
obtain t where "0 < t" and "t < real x" and
- cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
- + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
+ cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * (real x) ^ i)
+ + (cos (t + 1/2 * (2 * n) * pi) / (fact (2*n))) * (real x)^(2*n)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
unfolding cos_coeff_def atLeast0LessThan by auto
@@ -1020,22 +1020,22 @@
qed
lemma sin_aux: assumes "0 \<le> real x"
- shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
- and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
+ shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
+ and "(\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
proof -
have "0 \<le> real (x * x)" by auto
- let "?f n" = "fact (2 * n + 1)"
+ let "?f n" = "fact (2 * n + 1) :: nat"
{ fix n
have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
- unfolding F by auto } note f_eq = this
-
+ unfolding F by auto }
+ note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
show "?lb" and "?ub" using `0 \<le> real x`
unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
- unfolding mult.commute[where 'a=real]
+ unfolding mult.commute[where 'a=real] real_fact_nat
by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
qed
@@ -1046,14 +1046,15 @@
hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
have "0 < x * x" using `0 < x` by simp
- { fix x n have "(\<Sum> j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
- = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
+ { fix x::real and n
+ have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
+ = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * x ^ i)" (is "?SUM = _")
proof -
have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / ((fact i)) * x ^ i)"
unfolding sum_split_even_odd atLeast0LessThan ..
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / ((fact i))) * x ^ i)"
by (rule setsum.cong) auto
finally show ?thesis by assumption
qed } note setsum_morph = this
@@ -1061,8 +1062,8 @@
{ fix n :: nat assume "0 < n"
hence "0 < 2 * n + 1" by auto
obtain t where "0 < t" and "t < real x" and
- sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
- + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
+ sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)
+ + (sin (t + 1/2 * (2 * n + 1) * pi) / (fact (2*n + 1))) * (real x)^(2*n + 1)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
unfolding sin_coeff_def atLeast0LessThan by auto
@@ -1079,7 +1080,7 @@
{
assume "even n"
have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
- (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+ (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
also have "\<dots> \<le> ?SUM" by auto
also have "\<dots> \<le> sin x"
@@ -1100,7 +1101,7 @@
by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
thus ?thesis unfolding sin_eq by auto
qed
- also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+ also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
by auto
also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
@@ -1534,18 +1535,19 @@
proof -
{ fix n
have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
- have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^^ n) 1" unfolding F by auto } note f_eq = this
+ have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto
+ } note f_eq = this
note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
- { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / real (fact j) * real x ^ j)"
+ { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / (fact j) * real x ^ j)"
using bounds(1) by auto
also have "\<dots> \<le> exp x"
proof -
- obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
+ obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / (fact m)) + exp t / (fact (get_even n)) * (real x) ^ (get_even n)"
using Maclaurin_exp_le unfolding atLeast0LessThan by blast
- moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
+ moreover have "0 \<le> exp t / (fact (get_even n)) * (real x) ^ (get_even n)"
by (auto simp: zero_le_even_power)
ultimately show ?thesis using get_odd exp_gt_zero by auto
qed
@@ -1562,11 +1564,11 @@
show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`)
qed
- obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)"
+ obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / (fact m)) + exp t / (fact (get_odd n)) * (real x) ^ (get_odd n)"
using Maclaurin_exp_le unfolding atLeast0LessThan by blast
- moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
+ moreover have "exp t / (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero)
- ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
+ ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / (fact j) * real x ^ j)"
using get_odd exp_gt_zero by auto
also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x"
using bounds(2) by auto
@@ -3229,16 +3231,9 @@
qed
qed
-lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
-proof (induct k)
- case 0
- show ?case by simp
-next
- case (Suc k)
- have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
- hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
- thus ?case using Suc by auto
-qed
+lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
+ using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat
+ by presburger
lemma approx_tse:
assumes "bounded_by xs vs"
@@ -3258,10 +3253,11 @@
obtain n
where DERIV: "\<forall> m z. m < n \<and> real lx \<le> z \<and> z \<le> real ux \<longrightarrow> DERIV (F m) z :> F (Suc m) z"
and hyp: "\<And> (t::real). t \<in> {lx .. ux} \<Longrightarrow>
- (\<Sum> j = 0..<n. inverse (real (fact j)) * F j c * (xs!x - c)^j) +
- inverse (real (fact n)) * F n t * (xs!x - c)^n
+ (\<Sum> j = 0..<n. inverse(fact j) * F j c * (xs!x - c)^j) +
+ inverse ((fact n)) * F n t * (xs!x - c)^n
\<in> {l .. u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
- unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact by blast
+ unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact
+ by blast
have bnd_xs: "xs ! x \<in> { lx .. ux }"
using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
@@ -3284,8 +3280,8 @@
from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
- (\<Sum>m = 0..<Suc n'. F m c / real (fact m) * (xs ! x - c) ^ m) +
- F (Suc n') t / real (fact (Suc n')) * (xs ! x - c) ^ Suc n'"
+ (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
+ F (Suc n') t / (fact (Suc n')) * (xs ! x - c) ^ Suc n'"
unfolding atLeast0LessThan by blast
from t_bnd bnd_xs bnd_c have *: "t \<in> {lx .. ux}"
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Mar 18 13:31:52 2015 +0100
@@ -8,6 +8,7 @@
imports Complex_Main
begin
+lemmas fact_Suc = fact.simps(2)
subsection {* The type of formal power series*}
@@ -2866,7 +2867,7 @@
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)
+ simp del: fact.simps of_nat_Suc power_Suc)
apply (simp add: of_nat_mult field_simps)
done
}
@@ -2882,11 +2883,11 @@
by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
{
fix n
- have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
+ have "a$n = a$0 * c ^ n/ (fact n)"
apply (induct n)
apply simp
unfolding th
- using fact_gt_zero_nat
+ using fact_gt_zero
apply (simp add: field_simps del: of_nat_Suc fact_Suc)
apply (drule sym)
apply (simp add: field_simps of_nat_mult)
@@ -2985,33 +2986,6 @@
apply (simp add: cond_value_iff cond_application_beta setsum.delta' cong del: if_weak_cong)
done
-text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *}
-
-lemma gbinomial_theorem:
- "((a::'a::{field_char_0,field_inverse_zero})+b) ^ n =
- (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
-proof -
- from E_add_mult[of a b]
- have "(E (a + b)) $ n = (E a * E b)$n" by simp
- then have "(a + b) ^ n =
- (\<Sum>i::nat = 0::nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
- by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
- then show ?thesis
- apply simp
- apply (rule setsum.cong)
- apply simp_all
- apply (frule binomial_fact[where ?'a = 'a, symmetric])
- apply (simp add: field_simps of_nat_mult)
- done
-qed
-
-text{* And the nat-form -- also available from Binomial.thy *}
-lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
- using gbinomial_theorem[of "of_nat a" "of_nat b" n]
- unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric]
- of_nat_setsum[symmetric]
- by simp
-
subsubsection{* Logarithmic series *}
@@ -3290,7 +3264,7 @@
unfolding m1nk
unfolding m h pochhammer_Suc_setprod
apply (simp add: field_simps del: fact_Suc)
- unfolding fact_altdef_nat id_def
+ unfolding fact_altdef id_def
unfolding of_nat_setprod
unfolding setprod.distrib[symmetric]
apply auto
@@ -3823,7 +3797,7 @@
THEN spec, of "\<lambda>x. x < e"]
have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
apply safe
- apply (auto simp: eventually_nhds)
+ apply (auto simp: eventually_nhds) --{*slow*}
done
then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
--- a/src/HOL/Library/Permutations.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Library/Permutations.thy Wed Mar 18 13:31:52 2015 +0100
@@ -190,7 +190,7 @@
from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
using `finite F` by auto
then have "finite ?pF"
- using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
+ by (auto intro: card_ge_0_finite)
then have pF'f: "finite ?pF'"
using H0 `finite F`
apply (simp only: Collect_split Collect_mem_eq)
@@ -258,7 +258,7 @@
lemma finite_permutations:
assumes fS: "finite S"
shows "finite {p. p permutes S}"
- using card_permutations[OF refl fS] fact_gt_zero_nat
+ using card_permutations[OF refl fS]
by (auto intro: card_ge_0_finite)
@@ -280,26 +280,6 @@
by simp
qed
-lemma setsum_permute:
- assumes "p permutes S"
- shows "setsum f S = setsum (f \<circ> p) S"
- using assms by (fact setsum.permute)
-
-lemma setsum_permute_natseg:
- assumes pS: "p permutes {m .. n}"
- shows "setsum f {m .. n} = setsum (f \<circ> p) {m .. n}"
- using setsum_permute [OF pS, of f ] pS by blast
-
-lemma setprod_permute:
- assumes "p permutes S"
- shows "setprod f S = setprod (f \<circ> p) S"
- using assms by (fact setprod.permute)
-
-lemma setprod_permute_natseg:
- assumes pS: "p permutes {m .. n}"
- shows "setprod f {m .. n} = setprod (f \<circ> p) {m .. n}"
- using setprod_permute [OF pS, of f ] pS by blast
-
subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *}
--- a/src/HOL/MacLaurin.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/MacLaurin.thy Wed Mar 18 13:31:52 2015 +0100
@@ -17,47 +17,52 @@
lemma Maclaurin_lemma:
"0 < h ==>
- \<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) +
- (B * ((h^n) / real(fact n)))"
-by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(fact n) / (h^n)"]) simp
+ \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) +
+ (B * ((h^n) /(fact n)))"
+by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
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)
+ by (subst fact_reduce, auto)
lemma Maclaurin_lemma2:
fixes B
assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
- and INIT : "n = Suc k"
- defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
- B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
+ and INIT : "n = Suc k"
+ defines "difg \<equiv>
+ (\<lambda>m t::real. diff m t -
+ ((\<Sum>p<n - m. diff (m + p) 0 / (fact p) * t ^ p) + B * (t ^ (n - m) / (fact (n - m)))))"
+ (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
proof (rule allI impI)+
- fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
+ fix m and t::real
+ assume INIT2: "m < n & 0 \<le> t & t \<le> h"
have "DERIV (difg m) t :> diff (Suc m) t -
- ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
- real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
+ ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) +
+ real (n - m) * t ^ (n - Suc m) * B / (fact (n - m)))"
+ unfolding difg_def
by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
simp: real_of_nat_def[symmetric])
moreover
from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
unfolding atLeast0LessThan[symmetric] by auto
- have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
- (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
+ have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
+ (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
moreover
- have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
- by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)
- have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =
- diff (Suc m + x) 0 * t^x / real (fact x)"
- by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])
+ have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
+ by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff not_real_of_nat_less_zero)
+ have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)) =
+ diff (Suc m + x) 0 * t^x / (fact x)"
+ by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
moreover
- have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =
- B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"
- using `0 < n - m` by (simp add: fact_reduce_nat)
+ have "(n - m) * t ^ (n - Suc m) * B / (fact (n - m)) =
+ B * (t ^ (n - Suc m) / (fact (n - Suc m)))"
+ using `0 < n - m`
+ by (simp add: divide_simps fact_reduce)
ultimately show "DERIV (difg m) t :> difg (Suc m) t"
unfolding difg_def by simp
qed
@@ -69,29 +74,27 @@
assumes diff_Suc:
"\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
shows
- "\<exists>t. 0 < t & t < h &
+ "\<exists>t::real. 0 < t & t < h &
f h =
- setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} +
- (diff n t / real (fact n)) * h ^ n"
+ setsum (%m. (diff m 0 / (fact m)) * h ^ m) {..<n} +
+ (diff n t / (fact n)) * h ^ n"
proof -
from n obtain m where m: "n = Suc m"
by (cases n) (simp add: n)
obtain B where f_h: "f h =
- (\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
- B * (h ^ n / real (fact n))"
+ (\<Sum>m<n. diff m (0\<Colon>real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))"
using Maclaurin_lemma [OF h] ..
def g \<equiv> "(\<lambda>t. f t -
- (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n}
- + (B * (t^n / real(fact n)))))"
+ (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n)))))"
have g2: "g 0 = 0 & g h = 0"
by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
def difg \<equiv> "(%m t. diff m t -
- (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
- + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
+ (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
+ + (B * ((t ^ (n - m)) / (fact (n - m))))))"
have difg_0: "difg 0 = g"
unfolding difg_def g_def by (simp add: diff_0)
@@ -146,7 +149,6 @@
thus ?case
using `t < h` by auto
qed
-
then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
hence "difg (Suc m) t = 0"
@@ -156,30 +158,28 @@
proof (intro exI conjI)
show "0 < t" by fact
show "t < h" by fact
- show "f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n"
+ show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (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)
qed
qed
lemma Maclaurin_objl:
"0 < h & n>0 & diff 0 = f &
(\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
- --> (\<exists>t. 0 < t & t < h &
- f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n)"
+ --> (\<exists>t::real. 0 < t & t < h &
+ f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
+ diff n t / (fact n) * h ^ n)"
by (blast intro: Maclaurin)
lemma Maclaurin2:
assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
- and DERIV: "\<forall>m t.
+ and DERIV: "\<forall>m t::real.
m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n"
+ (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
+ diff n t / (fact n) * h ^ n"
proof (cases "n")
case 0 with INIT1 INIT2 show ?thesis by fastforce
next
@@ -187,28 +187,28 @@
hence "n > 0" by simp
from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
+ (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
by (rule Maclaurin)
thus ?thesis by fastforce
qed
lemma Maclaurin2_objl:
"0 < h & diff 0 = f &
- (\<forall>m t.
- m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
- --> (\<exists>t. 0 < t &
+ (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
+ --> (\<exists>t::real. 0 < t &
t \<le> h &
f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n)"
+ (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
+ diff n t / (fact n) * h ^ n)"
by (blast intro: Maclaurin2)
lemma Maclaurin_minus:
+ fixes h::real
assumes "h < 0" "0 < n" "diff 0 = f"
and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
shows "\<exists>t. h < t & t < 0 &
- f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n"
+ f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
+ diff n t / (fact n) * h ^ n"
proof -
txt "Transform @{text ABL'} into @{text derivative_intros} format."
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
@@ -216,33 +216,35 @@
have "\<exists>t>0. t < - h \<and>
f (- (- h)) =
(\<Sum>m<n.
- (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
- (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
+ (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
+ (- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
then guess t ..
moreover
- have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
+ have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
by (auto simp add: power_mult_distrib[symmetric])
moreover
- have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
+ have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
ultimately have " h < - t \<and>
- t < 0 \<and>
f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
+ (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
by auto
thus ?thesis ..
qed
lemma Maclaurin_minus_objl:
+ fixes h::real
+ shows
"(h < 0 & n > 0 & diff 0 = f &
(\<forall>m t.
m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
--> (\<exists>t. h < t &
t < 0 &
f h =
- (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
- diff n t / real (fact n) * h ^ n)"
+ (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
+ diff n t / (fact n) * h ^ n)"
by (blast intro: Maclaurin_minus)
@@ -250,20 +252,19 @@
(* not good for PVS sin_approx, cos_approx *)
-lemma Maclaurin_bi_le_lemma [rule_format]:
- "n>0 \<longrightarrow>
+lemma Maclaurin_bi_le_lemma:
+ "n>0 \<Longrightarrow>
diff 0 0 =
- (\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) +
- diff n 0 * 0 ^ n / real (fact n)"
+ (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
by (induct "n") auto
lemma Maclaurin_bi_le:
assumes "diff 0 = f"
- and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
+ and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
shows "\<exists>t. abs t \<le> abs x &
f x =
- (\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) +
- diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
+ (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
+ diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
proof cases
assume "n = 0" with `diff 0 = f` show ?thesis by force
next
@@ -291,11 +292,12 @@
qed
lemma Maclaurin_all_lt:
+ fixes x::real
assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
- (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
- (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
+ (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
+ (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
proof (cases rule: linorder_cases)
assume "x = 0" with INIT3 show "?thesis"..
next
@@ -314,28 +316,30 @@
lemma Maclaurin_all_lt_objl:
+ fixes x::real
+ shows
"diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
x ~= 0 & n > 0
--> (\<exists>t. 0 < abs t & abs t < abs x &
- f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
- (diff n t / real (fact n)) * x ^ n)"
+ f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
+ (diff n t / (fact n)) * x ^ n)"
by (blast intro: Maclaurin_all_lt)
lemma Maclaurin_zero [rule_format]:
"x = (0::real)
==> n \<noteq> 0 -->
- (\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) =
+ (\<Sum>m<n. (diff m (0::real) / (fact m)) * x ^ m) =
diff 0 0"
by (induct n, auto)
lemma Maclaurin_all_le:
assumes INIT: "diff 0 = f"
- and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
+ and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
shows "\<exists>t. abs t \<le> abs x & f x =
- (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
- (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
+ (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
+ (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
proof cases
assume "n = 0" with INIT show ?thesis by force
next
@@ -343,7 +347,7 @@
show ?thesis
proof cases
assume "x = 0"
- with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
+ with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
by (intro Maclaurin_zero) auto
with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
thus ?thesis ..
@@ -357,28 +361,32 @@
qed
qed
-lemma Maclaurin_all_le_objl: "diff 0 = f &
+lemma Maclaurin_all_le_objl:
+ "diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
- --> (\<exists>t. abs t \<le> abs x &
- f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
- (diff n t / real (fact n)) * x ^ n)"
+ --> (\<exists>t::real. abs t \<le> abs x &
+ f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
+ (diff n t / (fact n)) * x ^ n)"
by (blast intro: Maclaurin_all_le)
subsection{*Version for Exponential Function*}
-lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
+lemma Maclaurin_exp_lt:
+ fixes x::real
+ shows
+ "[| x ~= 0; n > 0 |]
==> (\<exists>t. 0 < abs t &
abs t < abs x &
- exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
- (exp t / real (fact n)) * x ^ n)"
+ exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
+ (exp t / (fact n)) * x ^ n)"
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
lemma Maclaurin_exp_le:
- "\<exists>t. abs t \<le> abs x &
- exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
- (exp t / real (fact n)) * x ^ n"
+ "\<exists>t::real. abs t \<le> abs x &
+ exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
+ (exp t / (fact n)) * x ^ n"
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
@@ -412,7 +420,7 @@
"\<exists>t. abs t \<le> abs x &
sin x =
(\<Sum>m<n. sin_coeff m * x ^ m)
- + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and x = x
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
@@ -431,7 +439,7 @@
lemma Maclaurin_sin_expansion:
"\<exists>t. sin x =
(\<Sum>m<n. sin_coeff m * x ^ m)
- + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (insert Maclaurin_sin_expansion2 [of x n])
apply (blast intro: elim:)
done
@@ -441,7 +449,7 @@
\<exists>t. 0 < t & t < x &
sin x =
(\<Sum>m<n. sin_coeff m * x ^ m)
- + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
+ + ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
@@ -458,7 +466,7 @@
\<exists>t. 0 < t & t \<le> x &
sin x =
(\<Sum>m<n. sin_coeff m * x ^ m)
- + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
apply simp
@@ -482,10 +490,10 @@
by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
lemma Maclaurin_cos_expansion:
- "\<exists>t. abs t \<le> abs x &
+ "\<exists>t::real. abs t \<le> abs x &
cos x =
(\<Sum>m<n. cos_coeff m * x ^ m)
- + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
@@ -505,7 +513,7 @@
\<exists>t. 0 < t & t < x &
cos x =
(\<Sum>m<n. cos_coeff m * x ^ m)
- + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
@@ -521,7 +529,7 @@
\<exists>t. x < t & t < 0 &
cos x =
(\<Sum>m<n. cos_coeff m * x ^ m)
- + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+ + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
apply simp
@@ -542,7 +550,7 @@
lemma Maclaurin_sin_bound:
"abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
- \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
+ \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
proof -
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
by (rule_tac mult_right_mono,simp_all)
@@ -557,8 +565,8 @@
done
from Maclaurin_all_le [OF diff_0 DERIV_diff]
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
- t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) +
- ?diff n t / real (fact n) * x ^ n" by fast
+ t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) +
+ ?diff n t / (fact n) * x ^ n" by fast
have diff_m_0:
"\<And>m. ?diff m 0 = (if even m then 0
else (- 1) ^ ((m - Suc 0) div 2))"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Mar 18 13:31:52 2015 +0100
@@ -8,6 +8,10 @@
imports "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
begin
+
+lemma cmod_fact [simp]: "cmod (fact n) = fact n"
+ by (metis norm_of_nat of_nat_fact)
+
subsection{*General lemmas*}
lemma has_derivative_mult_right:
@@ -26,7 +30,7 @@
lemma fact_cancel:
fixes c :: "'a::real_field"
- shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
+ shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
lemma linear_times:
@@ -985,7 +989,7 @@
and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
and w: "w \<in> s"
and z: "z \<in> s"
- shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / of_nat (fact i)))
+ shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
\<le> B * cmod(z - w)^(Suc n) / fact n"
proof -
have wzs: "closed_segment w z \<subseteq> s" using assms
@@ -994,48 +998,46 @@
assume "u \<in> closed_segment w z"
then have "u \<in> s"
by (metis wzs subsetD)
- have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / of_nat (fact i) +
- f (Suc i) u * (z-u)^i / of_nat (fact i)) =
- f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
+ have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
+ f (Suc i) u * (z-u)^i / (fact i)) =
+ f (Suc n) u * (z-u) ^ n / (fact n)"
proof (induction n)
case 0 show ?case by simp
next
case (Suc n)
- have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / of_nat (fact i) +
- f (Suc i) u * (z-u) ^ i / of_nat (fact i)) =
- f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
- f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
- f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
+ have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) +
+ f (Suc i) u * (z-u) ^ i / (fact i)) =
+ f (Suc n) u * (z-u) ^ n / (fact n) +
+ f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
+ f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
using Suc by simp
- also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
+ also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
proof -
- have "of_nat(fact(Suc n)) *
- (f(Suc n) u *(z-u) ^ n / of_nat(fact n) +
- f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / of_nat(fact(Suc n)) -
- f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / of_nat(fact(Suc n))) =
- (of_nat(fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / of_nat(fact n) +
- (of_nat(fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / of_nat(fact(Suc n))) -
- (of_nat(fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / of_nat(fact(Suc n))"
- by (simp add: algebra_simps del: fact_Suc)
- also have "... =
- (of_nat (fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / of_nat (fact n) +
- (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
- (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp del: fact_Suc)
- also have "... =
- (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
- (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
- (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp only: fact_Suc of_nat_mult ac_simps) simp
+ have "(fact(Suc n)) *
+ (f(Suc n) u *(z-u) ^ n / (fact n) +
+ f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / (fact(Suc n)) -
+ f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / (fact(Suc n))) =
+ ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
+ ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
+ ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
+ by (simp add: algebra_simps del: fact.simps)
+ also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
+ (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
+ (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
+ by (simp del: fact.simps)
+ also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
+ (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
+ (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
+ by (simp only: fact.simps of_nat_mult ac_simps) simp
also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
by (simp add: algebra_simps)
finally show ?thesis
- by (simp add: mult_left_cancel [where c = "of_nat (fact (Suc n))", THEN iffD1] del: fact_Suc)
+ by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
qed
finally show ?case .
qed
- then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / of_nat (fact i)))
- has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n))
+ then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
+ has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
(at u within s)"
apply (intro derivative_eq_intros)
apply (blast intro: assms `u \<in> s`)
@@ -1055,22 +1057,22 @@
by (metis norm_ge_zero zero_le_power mult_right_mono B [OF us])
finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> B * cmod (z - w) ^ n" .
} note cmod_bound = this
- have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (fact i)) = (\<Sum>i\<le>n. (f i z / of_nat (fact i)) * 0 ^ i)"
+ have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)) = (\<Sum>i\<le>n. (f i z / (fact i)) * 0 ^ i)"
by simp
- also have "\<dots> = f 0 z / of_nat (fact 0)"
+ also have "\<dots> = f 0 z / (fact 0)"
by (subst setsum_zero_power) simp
- finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / of_nat (fact i)))
- \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / of_nat (fact i)) -
- (\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (fact i)))"
+ finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
+ \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
+ (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
by (simp add: norm_minus_commute)
- also have "... \<le> B * cmod (z - w) ^ n / real_of_nat (fact n) * cmod (w - z)"
+ also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
apply (rule complex_differentiable_bound
- [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / of_nat(fact n)"
+ [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
and s = "closed_segment w z", OF convex_segment])
apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
done
- also have "... \<le> B * cmod (z - w) ^ Suc n / real (fact n)"
+ also have "... \<le> B * cmod (z - w) ^ Suc n / (fact n)"
by (simp add: algebra_simps norm_minus_commute real_of_nat_def)
finally show ?thesis .
qed
@@ -1102,40 +1104,40 @@
assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
shows "\<exists>u. u \<in> closed_segment w z \<and>
Re (f 0 z) =
- Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / of_nat (fact i)) +
- (f (Suc n) u * (z-u)^n / of_nat (fact n)) * (z - w))"
+ Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / (fact i)) +
+ (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))"
proof -
{ fix u
assume u: "u \<in> closed_segment w z"
have "(\<Sum>i = 0..n.
(f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) /
- of_nat (fact i)) =
+ (fact i)) =
f (Suc 0) u -
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
+ (fact (Suc n)) +
(\<Sum>i = 0..n.
(f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
- of_nat (fact (Suc i)))"
+ (fact (Suc i)))"
by (subst setsum_Suc_reindex) simp
also have "... = f (Suc 0) u -
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
+ (fact (Suc n)) +
(\<Sum>i = 0..n.
- f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i)) -
- f (Suc i) u * (z-u) ^ i / of_nat (fact i))"
+ f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) -
+ f (Suc i) u * (z-u) ^ i / (fact i))"
by (simp only: diff_divide_distrib fact_cancel ac_simps)
also have "... = f (Suc 0) u -
(f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
- f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n)) - f (Suc 0) u"
+ (fact (Suc n)) +
+ f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
by (subst setsum_Suc_diff) auto
- also have "... = f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
+ also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
by (simp only: algebra_simps diff_divide_distrib fact_cancel)
finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
- - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / of_nat (fact i)) =
- f (Suc n) u * (z - u) ^ n / of_nat (fact n)" .
- then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative
- f (Suc n) u * (z - u) ^ n / of_nat (fact n)) (at u)"
+ - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
+ f (Suc n) u * (z - u) ^ n / (fact n)" .
+ then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
+ f (Suc n) u * (z - u) ^ n / (fact n)) (at u)"
apply (intro derivative_eq_intros)+
apply (force intro: u assms)
apply (rule refl)+
@@ -1143,8 +1145,8 @@
done
}
then show ?thesis
- apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / of_nat (fact i)"
- "\<lambda>u. (f (Suc n) u * (z-u)^n / of_nat (fact n))"])
+ apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
+ "\<lambda>u. (f (Suc n) u * (z-u)^n / (fact n))"])
apply (auto simp add: intro: open_closed_segment)
done
qed
--- a/src/HOL/NSA/HTranscendental.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Wed Mar 18 13:31:52 2015 +0100
@@ -14,7 +14,7 @@
definition
exphr :: "real => hypreal" where
--{*define exponential function using standard part *}
- "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
+ "exphr x = st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
definition
sinhr :: "real => hypreal" where
@@ -213,7 +213,7 @@
done
lemma HFinite_exp [simp]:
- "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
+ "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \<in> HFinite"
unfolding sumhr_app
apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
apply (rule NSBseqD2)
--- a/src/HOL/NSA/NSComplex.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy Wed Mar 18 13:31:52 2015 +0100
@@ -654,5 +654,4 @@
"hIm(numeral v :: hcomplex) = 0"
by transfer (rule complex_Im_numeral)
-(* TODO: add neg_numeral rules above *)
end
--- a/src/HOL/Number_Theory/Primes.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Wed Mar 18 13:31:52 2015 +0100
@@ -226,7 +226,7 @@
lemma next_prime_bound: "\<exists>p. 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
+ have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
from prime_factor_nat [OF f1]
obtain p where "prime p" and "p dvd fact n + 1" by auto
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
@@ -234,7 +234,7 @@
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)
+ by (intro dvd_fact)
with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
by (rule dvd_diff_nat)
then have "p dvd 1" by simp
--- a/src/HOL/Number_Theory/Residues.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Wed Mar 18 13:31:52 2015 +0100
@@ -384,7 +384,7 @@
lemma (in residues_prime) wilson_theorem1:
assumes a: "p > 2"
- shows "[fact (p - 1) = - 1] (mod p)"
+ shows "[fact (p - 1) = (-1::int)] (mod p)"
proof -
let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
@@ -430,9 +430,9 @@
apply (subst res_prime_units_eq)
apply (simp add: int_setprod zmod_int setprod_int_eq)
done
- finally have "fact (p - 1) mod p = \<ominus> \<one>".
- then show ?thesis
- by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
+ finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
+ then show ?thesis
+ by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
qed
lemma wilson_theorem:
--- a/src/HOL/Probability/Distributions.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Probability/Distributions.thy Wed Mar 18 13:31:52 2015 +0100
@@ -78,12 +78,13 @@
proof -
let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
-
- have "?I * (inverse (fact k)) =
- (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
+ have "?I * (inverse (real_of_nat (fact k))) =
+ (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (real_of_nat (fact k))) \<partial>lborel)"
by (intro nn_integral_multc[symmetric]) auto
also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
- by (intro nn_integral_cong) (simp add: field_simps)
+ apply (intro nn_integral_cong)
+ apply (simp add: field_simps)
+ by (metis (no_types) divide_inverse mult.commute mult.left_commute mult.left_neutral times_ereal.simps(1))
also have "\<dots> = ereal (?F k a - ?F k 0)"
proof (rule nn_integral_FTC_Icc)
fix x assume "x \<in> {0..a}"
@@ -93,13 +94,13 @@
next
case (Suc k)
have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
- ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
+ ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k))"
by (intro DERIV_diff Suc)
(auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
by simp
- also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
+ also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k)) = ?f (Suc k) x"
by (auto simp: field_simps simp del: fact_Suc)
(simp_all add: real_of_nat_Suc field_simps)
finally show ?case .
@@ -112,7 +113,7 @@
qed
lemma nn_intergal_power_times_exp_Ici:
- shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k"
+ shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)"
proof (rule LIMSEQ_unique)
let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
@@ -122,9 +123,10 @@
apply (metis nat_ceiling_le_eq)
done
- have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
+ have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
+ (1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
by (intro tendsto_intros tendsto_power_div_exp_0) simp
- then show "?X ----> fact k"
+ then show "?X ----> real_of_nat (fact k)"
by (subst nn_intergal_power_times_exp_Icc)
(auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
qed
@@ -514,7 +516,7 @@
by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
- let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
+ let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))"
let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)"
@@ -919,10 +921,12 @@
lemma
fixes k :: nat
shows gaussian_moment_even_pos:
- "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
- ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" (is "?even")
+ "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
+ ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))"
+ (is "?even")
and gaussian_moment_odd_pos:
- "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" (is "?odd")
+ "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)"
+ (is "?odd")
proof -
let ?M = "\<lambda>k x. exp (- x\<^sup>2) * x^k :: real"
@@ -997,9 +1001,11 @@
proof (induct k)
case (Suc k)
note step[OF this]
- also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * (real (fact (2 * k)) / real (2 ^ (2 * k) * fact k)))) =
- sqrt pi / 2 * (real (fact (2 * Suc k)) / real (2 ^ (2 * Suc k) * fact (Suc k)))"
- by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
+ also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) =
+ sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))"
+ apply (simp add: field_simps del: fact_Suc)
+ apply (simp add: real_of_nat_def of_nat_mult field_simps)
+ done
finally show ?case
by simp
qed (insert gaussian_moment_0, simp)
@@ -1008,7 +1014,7 @@
proof (induct k)
case (Suc k)
note step[OF this]
- also have "(real (2 * k + 1 + 1) / 2 * (real (fact k) / 2)) = real (fact (Suc k)) / 2"
+ also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2"
by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
finally show ?case
by simp
@@ -1036,7 +1042,7 @@
by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult
real_sqrt_divide power_mult eq)
also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) =
- (inverse (sqrt 2 * \<sigma>) * (real (fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * real (fact k)))"
+ (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))"
by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult
power2_eq_square)
finally show ?thesis
@@ -1047,10 +1053,10 @@
lemma normal_moment_abs_odd:
"has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))"
proof -
- have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
+ have "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto
from has_bochner_integral_even_function[OF this]
- have "has_bochner_integral lborel (\<lambda>x. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
+ have "has_bochner_integral lborel (\<lambda>x::real. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
by simp
then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))
(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))"
@@ -1059,7 +1065,7 @@
(\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))"
by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult)
also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) =
- (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * real (fact k) * sqrt (2 / pi)))"
+ (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))"
by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide
real_sqrt_mult)
finally show ?thesis
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Mar 18 13:31:52 2015 +0100
@@ -1429,9 +1429,7 @@
begin
lift_definition poisson_pmf :: "nat pmf" is "\<lambda>k. rate ^ k / fact k * exp (-rate)"
-proof
- (* Proof by Manuel Eberl *)
-
+proof (* by Manuel Eberl *)
have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
by (simp add: field_simps divide_inverse [symmetric])
have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
@@ -1440,10 +1438,10 @@
also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
also have "... = exp rate" unfolding exp_def
- by (simp add: field_simps divide_inverse [symmetric] transfer_int_nat_factorial)
+ by (simp add: field_simps divide_inverse [symmetric])
also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
by (simp add: mult_exp_exp)
- finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
+ finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
qed (simp add: rate_pos[THEN less_imp_le])
lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)"
--- a/src/HOL/Proofs/Extraction/Euclid.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Wed Mar 18 13:31:52 2015 +0100
@@ -210,8 +210,8 @@
lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
proof -
- let ?k = "fact n + 1"
- have "1 < fact n + 1" by simp
+ let ?k = "fact n + (1::nat)"
+ have "1 < ?k" by simp
then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
have "n < p"
proof -
--- a/src/HOL/Proofs/Extraction/Util.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Util.thy Wed Mar 18 13:31:52 2015 +0100
@@ -5,7 +5,7 @@
section {* Auxiliary lemmas used in program extraction examples *}
theory Util
-imports Old_Datatype
+imports "~~/src/HOL/Library/Old_Datatype"
begin
text {*
--- a/src/HOL/Taylor.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Taylor.thy Wed Mar 18 13:31:52 2015 +0100
@@ -17,8 +17,8 @@
assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a \<le> c" "c < b"
- shows "\<exists> t. c < t & t < b &
- f b = (\<Sum>m<n. (diff m c / real (fact m)) * (b - c)^m) + (diff n t / real (fact n)) * (b - c)^n"
+ shows "\<exists>t::real. c < t & t < b &
+ f b = (\<Sum>m<n. (diff m c / (fact m)) * (b - c)^m) + (diff n t / (fact n)) * (b - c)^n"
proof -
from INTERV have "0 < b-c" by arith
moreover
@@ -35,31 +35,24 @@
by (rule DERIV_chain2)
thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
qed
- ultimately
- have EX:"EX t>0. t < b - c &
- f (b - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
- diff n (t + c) / real (fact n) * (b - c) ^ n"
- by (rule Maclaurin)
- show ?thesis
- proof -
- from EX obtain x where
- X: "0 < x & x < b - c &
- f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
- diff n (x + c) / real (fact n) * (b - c) ^ n" ..
- let ?H = "x + c"
- from X have "c<?H & ?H<b \<and> f b = (\<Sum>m<n. diff m c / real (fact m) * (b - c) ^ m) +
- diff n ?H / real (fact n) * (b - c) ^ n"
- by fastforce
- thus ?thesis by fastforce
- qed
+ ultimately obtain x where
+ "0 < x & x < b - c &
+ f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b - c) ^ m) +
+ diff n (x + c) / (fact n) * (b - c) ^ n"
+ by (rule Maclaurin [THEN exE])
+ then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b - c) ^ m) +
+ diff n (x+c) / (fact n) * (b - c) ^ n"
+ by fastforce
+ thus ?thesis by fastforce
qed
lemma taylor_down:
+ fixes a::real
assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a < c" "c \<le> b"
shows "\<exists> t. a < t & t < c &
- f a = (\<Sum>m<n. (diff m c / real (fact m)) * (a - c)^m) + (diff n t / real (fact n)) * (a - c)^n"
+ f a = (\<Sum>m<n. (diff m c / (fact m)) * (a - c)^m) + (diff n t / (fact n)) * (a - c)^n"
proof -
from INTERV have "a-c < 0" by arith
moreover
@@ -75,30 +68,24 @@
ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
qed
- ultimately
- have EX: "EX t>a - c. t < 0 &
- f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
- diff n (t + c) / real (fact n) * (a - c) ^ n"
- by (rule Maclaurin_minus)
- show ?thesis
- proof -
- from EX obtain x where X: "a - c < x & x < 0 &
- f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
- diff n (x + c) / real (fact n) * (a - c) ^ n" ..
- let ?H = "x + c"
- from X have "a<?H & ?H<c \<and> f a = (\<Sum>m<n. diff m c / real (fact m) * (a - c) ^ m) +
- diff n ?H / real (fact n) * (a - c) ^ n"
- by fastforce
- thus ?thesis by fastforce
- qed
+ ultimately obtain x where
+ "a - c < x & x < 0 &
+ f (a - c + c) = (SUM m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
+ diff n (x + c) / (fact n) * (a - c) ^ n"
+ by (rule Maclaurin_minus [THEN exE])
+ then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
+ diff n (x+c) / (fact n) * (a - c) ^ n"
+ by fastforce
+ thus ?thesis by fastforce
qed
lemma taylor:
+ fixes a::real
assumes INIT: "n>0" "diff 0 = f"
and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
- f x = (\<Sum>m<n. (diff m c / real (fact m)) * (x - c)^m) + (diff n t / real (fact n)) * (x - c)^n"
+ f x = (\<Sum>m<n. (diff m c / (fact m)) * (x - c)^m) + (diff n t / (fact n)) * (x - c)^n"
proof (cases "x<c")
case True
note INIT
@@ -107,8 +94,8 @@
by fastforce
moreover note True
moreover from INTERV have "c \<le> b" by simp
- ultimately have EX: "\<exists>t>x. t < c \<and> f x =
- (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n"
+ ultimately have "\<exists>t>x. t < c \<and> f x =
+ (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
by (rule taylor_down)
with True show ?thesis by simp
next
@@ -119,8 +106,8 @@
by fastforce
moreover from INTERV have "a \<le> c" by arith
moreover from False and INTERV have "c < x" by arith
- ultimately have EX: "\<exists>t>c. t < x \<and> f x =
- (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n"
+ ultimately have "\<exists>t>c. t < x \<and> f x =
+ (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
by (rule taylor_up)
with False show ?thesis by simp
qed
--- a/src/HOL/Transcendental.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 18 13:31:52 2015 +0100
@@ -10,6 +10,15 @@
imports Binomial Series Deriv NthRoot
begin
+lemma of_real_fact [simp]: "of_real (fact n) = fact n"
+ by (metis of_nat_fact of_real_of_nat_eq)
+
+lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
+ by (simp add: real_of_nat_def)
+
+lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
+ by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
+
lemma root_test_convergence:
fixes f :: "nat \<Rightarrow> 'a::banach"
assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
@@ -54,13 +63,13 @@
(x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
proof (induct n)
case (Suc n)
- have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
+ have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
by simp
- also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
+ also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
by (simp add: algebra_simps)
- also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
+ also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
by (simp only: Suc)
- also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
+ also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
by (simp only: mult.left_commute)
also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
@@ -100,40 +109,40 @@
lemma powser_insidea:
fixes x z :: "'a::real_normed_div_algebra"
- assumes 1: "summable (\<lambda>n. f n * x ^ n)"
+ assumes 1: "summable (\<lambda>n. f n * x^n)"
and 2: "norm z < norm x"
shows "summable (\<lambda>n. norm (f n * z ^ n))"
proof -
from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
- from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
+ from 1 have "(\<lambda>n. f n * x^n) ----> 0"
by (rule summable_LIMSEQ_zero)
- hence "convergent (\<lambda>n. f n * x ^ n)"
+ hence "convergent (\<lambda>n. f n * x^n)"
by (rule convergentI)
- hence "Cauchy (\<lambda>n. f n * x ^ n)"
+ hence "Cauchy (\<lambda>n. f n * x^n)"
by (rule convergent_Cauchy)
- hence "Bseq (\<lambda>n. f n * x ^ n)"
+ hence "Bseq (\<lambda>n. f n * x^n)"
by (rule Cauchy_Bseq)
- then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
+ then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
by (simp add: Bseq_def, safe)
have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
- K * norm (z ^ n) * inverse (norm (x ^ n))"
+ K * norm (z ^ n) * inverse (norm (x^n))"
proof (intro exI allI impI)
fix n::nat
assume "0 \<le> n"
- have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
- norm (f n * x ^ n) * norm (z ^ n)"
+ have "norm (norm (f n * z ^ n)) * norm (x^n) =
+ norm (f n * x^n) * norm (z ^ n)"
by (simp add: norm_mult abs_mult)
also have "\<dots> \<le> K * norm (z ^ n)"
by (simp only: mult_right_mono 4 norm_ge_zero)
- also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
+ also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
by (simp add: x_neq_0)
- also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
+ also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
by (simp only: mult.assoc)
finally show "norm (norm (f n * z ^ n)) \<le>
- K * norm (z ^ n) * inverse (norm (x ^ n))"
+ K * norm (z ^ n) * inverse (norm (x^n))"
by (simp add: mult_le_cancel_right x_neq_0)
qed
- moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
+ moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
proof -
from 2 have "norm (norm (z * inverse x)) < 1"
using x_neq_0
@@ -142,7 +151,7 @@
by (rule summable_geometric)
hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
by (rule summable_mult)
- thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
+ thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
using x_neq_0
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
power_inverse norm_power mult.assoc)
@@ -154,7 +163,7 @@
lemma powser_inside:
fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
shows
- "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
+ "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
summable (\<lambda>n. f n * (z ^ n))"
by (rule powser_insidea [THEN summable_norm_cancel])
@@ -581,7 +590,7 @@
fixes x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
and 2: "norm x < norm K"
- shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
+ shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
- of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
proof -
from dense [OF 2]
@@ -629,7 +638,7 @@
hence "norm x + norm h < r" by simp
with norm_triangle_ineq have xh: "norm (x + h) < r"
by (rule order_le_less_trans)
- show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
+ show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
\<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
apply (simp only: norm_mult mult.assoc)
apply (rule mult_left_mono [OF _ norm_ge_zero])
@@ -645,11 +654,11 @@
and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
and 4: "norm x < norm K"
- shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
+ shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
unfolding DERIV_def
proof (rule LIM_zero_cancel)
- show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
- - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
+ show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
+ - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
proof (rule LIM_equal2)
show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
next
@@ -658,18 +667,18 @@
hence "norm x + norm h < norm K" by simp
hence 5: "norm (x + h) < norm K"
by (rule norm_triangle_ineq [THEN order_le_less_trans])
- have "summable (\<lambda>n. c n * x ^ n)"
+ have "summable (\<lambda>n. c n * x^n)"
and "summable (\<lambda>n. c n * (x + h) ^ n)"
- and "summable (\<lambda>n. diffs c n * x ^ n)"
+ and "summable (\<lambda>n. diffs c n * x^n)"
using 1 2 4 5 by (auto elim: powser_inside)
- then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
- (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
+ then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
+ (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
- then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
- (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
+ then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
+ (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
by (simp add: algebra_simps)
next
- show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
+ show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
by (rule termdiffs_aux [OF 3 4])
qed
qed
@@ -889,7 +898,7 @@
fix n
have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
by (rule mult_left_mono) auto
- show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
+ show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
unfolding real_norm_def abs_mult
by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
@@ -925,14 +934,14 @@
subsection {* Exponential Function *}
definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
- where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
+ where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
lemma summable_exp_generic:
fixes x :: "'a::{real_normed_algebra_1,banach}"
- defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
+ defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
shows "summable S"
proof -
- have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
+ have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
unfolding S_def by (simp del: mult_Suc)
obtain r :: real where r0: "0 < r" and r1: "r < 1"
using dense [OF zero_less_one] by fast
@@ -959,26 +968,29 @@
lemma summable_norm_exp:
fixes x :: "'a::{real_normed_algebra_1,banach}"
- shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
+ shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
proof (rule summable_norm_comparison_test [OF exI, rule_format])
- show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
+ show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
by (rule summable_exp_generic)
fix n
- show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
+ show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
by (simp add: norm_power_ineq)
qed
-lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
- using summable_exp_generic [where x=x] by simp
-
-lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
+lemma summable_exp:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "summable (\<lambda>n. inverse (fact n) * x^n)"
+ using summable_exp_generic [where x=x]
+ by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
+
+lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
-
lemma exp_fdiffs:
- "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
- by (simp add: diffs_def mult.assoc [symmetric] real_of_nat_def of_nat_mult
- del: mult_Suc of_nat_Suc)
+ fixes XXX :: "'a::{real_normed_field,banach}"
+ shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
+ by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
+ del: mult_Suc of_nat_Suc)
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
by (simp add: diffs_def)
@@ -997,7 +1009,7 @@
lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
proof -
from summable_norm[OF summable_norm_exp, of x]
- have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
+ have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
by (simp add: exp_def)
also have "\<dots> \<le> exp (norm x)"
using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
@@ -1047,7 +1059,7 @@
lemma exp_series_add_commuting:
fixes x y :: "'a::{real_normed_algebra_1, banach}"
- defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
+ defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
assumes comm: "x * y = y * x"
shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
proof (induct n)
@@ -1182,9 +1194,9 @@
using order_le_imp_less_or_eq [OF assms]
proof
assume "0 < x"
- have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
+ have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
by (auto simp add: numeral_2_eq_2)
- also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
+ also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
apply (rule setsum_le_suminf [OF summable_exp])
using `0 < x`
apply (auto simp add: zero_le_mult_iff)
@@ -1297,7 +1309,7 @@
lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
by (rule ln_unique) (simp add: exp_diff)
-lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
+lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
by (rule ln_unique) (simp add: exp_real_of_nat_mult)
lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
@@ -1424,7 +1436,7 @@
fix x :: real
assume "x \<in> {- 1<..<1}"
hence "norm (-x) < 1" by auto
- show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+ show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
unfolding One_nat_def
by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
qed
@@ -1439,12 +1451,14 @@
thus ?thesis by auto
qed
-lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
+lemma exp_first_two_terms:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
proof -
- have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
- by (simp add: exp_def)
+ have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
+ by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
- (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
+ (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
by (rule suminf_split_initial_segment)
also have "?a = 1 + x"
by (simp add: numeral_2_eq_2)
@@ -1458,21 +1472,22 @@
assume b: "x <= 1"
{
fix n :: nat
- have "2 * 2 ^ n \<le> fact (n + 2)"
+ have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
by (induct n) simp_all
- hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
+ hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
by (simp only: real_of_nat_le_iff)
- hence "2 * 2 ^ n \<le> real (fact (n + 2))"
- by simp
- hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
+ hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
+ unfolding of_nat_fact real_of_nat_def
+ by (simp add: of_nat_mult of_nat_power)
+ hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
by (rule le_imp_inverse_le) simp
- hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
+ hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
by (simp add: power_inverse)
hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
by (rule mult_mono)
(rule mult_mono, simp_all add: power_le_one a b)
hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
- unfolding power_add by (simp add: ac_simps del: fact_Suc) }
+ unfolding power_add by (simp add: ac_simps del: fact.simps) }
note aux1 = this
have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
by (intro sums_mult geometric_sums, simp)
@@ -2140,7 +2155,7 @@
lemma log_powr: "log b (x powr y) = y * log b x"
by (simp add: log_def ln_powr)
-lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
+lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
by (simp add: log_powr powr_realpow [symmetric])
lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
@@ -2342,10 +2357,10 @@
subsection {* Sine and Cosine *}
definition sin_coeff :: "nat \<Rightarrow> real" where
- "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
+ "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / (fact n))"
definition cos_coeff :: "nat \<Rightarrow> real" where
- "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
+ "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / (fact n) else 0)"
definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
@@ -2377,7 +2392,7 @@
lemma summable_norm_cos:
fixes x :: "'a::{real_normed_algebra_1,banach}"
- shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
+ shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
unfolding cos_coeff_def
apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
@@ -2398,7 +2413,7 @@
have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R (of_real x)^n)"
proof
fix n
- show "of_real (sin_coeff n *\<^sub>R x ^ n) = sin_coeff n *\<^sub>R of_real x ^ n"
+ show "of_real (sin_coeff n *\<^sub>R x^n) = sin_coeff n *\<^sub>R of_real x^n"
by (simp add: scaleR_conv_of_real)
qed
also have "... sums (sin (of_real x))"
@@ -2416,7 +2431,7 @@
have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R (of_real x)^n)"
proof
fix n
- show "of_real (cos_coeff n *\<^sub>R x ^ n) = cos_coeff n *\<^sub>R of_real x ^ n"
+ show "of_real (cos_coeff n *\<^sub>R x^n) = cos_coeff n *\<^sub>R of_real x^n"
by (simp add: scaleR_conv_of_real)
qed
also have "... sums (cos (of_real x))"
@@ -2549,7 +2564,7 @@
fixes x :: "'a::{real_normed_field,banach}"
shows "(\<lambda>p. \<Sum>n\<le>p.
if even p \<and> even n
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
sums (cos x * cos y)"
proof -
{ fix n p::nat
@@ -2557,12 +2572,12 @@
then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
by (metis div_add power_add le_add_diff_inverse odd_add)
have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
- (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
+ (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
using `n\<le>p`
by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
}
then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
(\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
by simp
also have "... = (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n *\<^sub>R x^n) * (cos_coeff (p - n) *\<^sub>R y^(p-n)))"
@@ -2578,7 +2593,7 @@
fixes x :: "'a::{real_normed_field,banach}"
shows "(\<lambda>p. \<Sum>n\<le>p.
if even p \<and> odd n
- then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
+ then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
sums (sin x * sin y)"
proof -
{ fix n p::nat
@@ -2596,12 +2611,12 @@
} then
have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
(if even p \<and> odd n
- then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
+ then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
using `n\<le>p`
by (auto simp: algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
}
then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
- then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
+ then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
(\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
by simp
also have "... = (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n *\<^sub>R x^n) * (sin_coeff (p - n) *\<^sub>R y^(p-n)))"
@@ -2616,31 +2631,31 @@
fixes x :: "'a::{real_normed_field,banach}"
shows
"(\<lambda>p. \<Sum>n\<le>p. if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
else 0)
sums cos (x + y)"
proof -
{ fix p::nat
have "(\<Sum>n\<le>p. if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
else 0) =
(if even p
- then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
+ then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
else 0)"
by simp
also have "... = (if even p
- then of_real ((-1) ^ (p div 2) / of_nat (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
+ then of_real ((-1) ^ (p div 2) / (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
else 0)"
by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
by (simp add: cos_coeff_def binomial_ring [of x y] scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
finally have "(\<Sum>n\<le>p. if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
}
then have "(\<lambda>p. \<Sum>n\<le>p.
if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
else 0)
= (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
by simp
@@ -2656,15 +2671,15 @@
{ fix n p::nat
assume "n\<le>p"
then have "(if even p \<and> even n
- then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
+ then ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
(if even p \<and> odd n
- then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
+ then - ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
= (if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
by simp
}
then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
- then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
+ then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
sums (cos x * cos y - sin x * sin y)"
using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
by (simp add: setsum_subtractf [symmetric])
@@ -2701,7 +2716,6 @@
by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
suminf_minus sums_iff equation_minus_iff)
-
lemma sin_cos_squared_add [simp]:
fixes x :: "'a::{real_normed_field,banach}"
shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
@@ -2787,7 +2801,7 @@
lemma sin_paired:
fixes x :: real
- shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums sin x"
+ shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n + 1)) * x ^ (2 * n + 1)) sums sin x"
proof -
have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
apply (rule sums_group)
@@ -2801,7 +2815,7 @@
assumes "0 < x" and "x < 2"
shows "0 < sin x"
proof -
- let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
+ let ?f = "\<lambda>n::nat. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / (fact (2*k+1)) * x^(2*k+1)"
have pos: "\<forall>n. 0 < ?f n"
proof
fix n :: nat
@@ -2812,9 +2826,8 @@
hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
by (intro mult_strict_right_mono zero_less_power `0 < x`)
thus "0 < ?f n"
- by (simp del: mult_Suc,
- simp add: less_divide_eq field_simps del: mult_Suc)
- qed
+ by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
+qed
have sums: "?f sums sin x"
by (rule sin_paired [THEN sums_group], simp)
show "0 < sin x"
@@ -2830,7 +2843,7 @@
lemma cos_paired:
fixes x :: real
- shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
+ shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n)) * x ^ (2 * n)) sums cos x"
proof -
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
apply (rule sums_group)
@@ -2860,29 +2873,28 @@
lemma cos_two_less_zero [simp]:
"cos 2 < (0::real)"
proof -
- note fact_Suc [simp del]
- from cos_paired
- have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
- by (rule sums_minus)
- then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
+ note fact.simps(2) [simp del]
+ from sums_minus [OF cos_paired]
+ have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
by simp
- then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule sums_summable)
- have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
- by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
- moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))
- < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
+ by (simp add: fact_num_eq_if realpow_num_eq_if)
+ moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))
+ < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
proof -
{ fix d
- have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
- < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
- fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
- by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
- then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
- < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
- by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
- then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
- < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+ have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
+ < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
+ fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+ unfolding real_of_nat_mult
+ by (rule mult_strict_mono) (simp_all add: fact_less_mono)
+ then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
+ < (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
+ by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact)
+ then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
+ < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
by (simp add: inverse_eq_divide less_divide_eq)
}
note *** = this
@@ -2890,9 +2902,9 @@
from ** show ?thesis by (rule sumr_pos_lt_pair)
(simp add: divide_inverse mult.assoc [symmetric] ***)
qed
- ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule order_less_trans)
- moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ moreover from * have "- cos 2 = (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule sums_unique)
ultimately have "(0::real) < - cos 2" by simp
then show ?thesis by simp
--- a/src/HOL/ex/Birthday_Paradox.thy Tue Mar 17 16:38:09 2015 +0100
+++ b/src/HOL/ex/Birthday_Paradox.thy Wed Mar 18 13:31:52 2015 +0100
@@ -51,7 +51,7 @@
using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
by (simp add: fact_mod)
also have "... = fact (card T) div fact (card T - card (insert x S))"
- using insert by (simp add: fact_reduce_nat[of "card T"])
+ using insert by (simp add: fact_reduce[of "card T"])
finally show ?case .
qed