--- a/src/HOL/GCD.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/GCD.thy Thu Apr 30 15:28:01 2015 +0100
@@ -755,24 +755,16 @@
done
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
- by (induct n, simp_all add: coprime_mult_nat)
+ by (induct n, simp_all add: power_Suc coprime_mult_nat)
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
- by (induct n, simp_all add: coprime_mult_int)
+ by (induct n, simp_all add: power_Suc coprime_mult_int)
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
- apply (rule coprime_exp_nat)
- apply (subst gcd_commute_nat)
- apply (rule coprime_exp_nat)
- apply (subst gcd_commute_nat, assumption)
-done
+ by (simp add: coprime_exp_nat gcd_nat.commute)
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
- apply (rule coprime_exp_int)
- apply (subst gcd_commute_int)
- apply (rule coprime_exp_int)
- apply (subst gcd_commute_int, assumption)
-done
+ by (simp add: coprime_exp_int gcd_int.commute)
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
proof (cases)
@@ -783,24 +775,11 @@
by (auto simp:div_gcd_coprime_nat)
hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
- apply (subst (1 2) mult.commute)
- apply (subst gcd_mult_distrib_nat [symmetric])
- apply simp
- done
+ by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
- apply (subst div_power)
- apply auto
- apply (rule dvd_div_mult_self)
- apply (rule dvd_power_same)
- apply auto
- done
+ by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
- apply (subst div_power)
- apply auto
- apply (rule dvd_div_mult_self)
- apply (rule dvd_power_same)
- apply auto
- done
+ by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
finally show ?thesis .
qed
@@ -908,7 +887,7 @@
have "a' dvd a'^n" by (simp add: m)
with th0 have "a' dvd b'^n"
using dvd_trans[of a' "a'^n" "b'^n"] by simp
- hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
+ hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute power_Suc)
from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
have "a' dvd b'" by (subst (asm) mult.commute, blast)
hence "a'*?g dvd b'*?g" by simp
@@ -947,21 +926,13 @@
qed
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
- apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
- apply force
- apply (rule dvd_diff_nat)
- apply auto
-done
+ by (simp add: gcd_nat.commute)
lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
using coprime_plus_one_nat by (simp add: One_nat_def)
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
- apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
- apply force
- apply (rule dvd_diff)
- apply auto
-done
+ by (simp add: gcd_int.commute)
lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
using coprime_plus_one_nat [of "n - 1"]
@@ -985,36 +956,23 @@
apply (auto simp add: gcd_mult_cancel_int)
done
-lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
- x dvd b \<Longrightarrow> x = 1"
- apply (subgoal_tac "x dvd gcd a b")
- apply simp
- apply (erule (1) gcd_greatest)
-done
+lemma coprime_common_divisor_nat:
+ "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+ by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
-lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
- x dvd b \<Longrightarrow> abs x = 1"
- apply (subgoal_tac "x dvd gcd a b")
- apply simp
- apply (erule (1) gcd_greatest)
-done
+lemma coprime_common_divisor_int:
+ "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
+ using gcd_greatest by fastforce
-lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
- coprime d e"
- apply (auto simp add: dvd_def)
- apply (frule coprime_lmult_int)
- apply (subst gcd_commute_int)
- apply (subst (asm) (2) gcd_commute_int)
- apply (erule coprime_lmult_int)
-done
+lemma coprime_divisors_nat:
+ "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
+ by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
-apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
-done
+by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
-apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
-done
+by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
subsection {* Bezout's theorem *}
--- a/src/HOL/Int.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Int.thy Thu Apr 30 15:28:01 2015 +0100
@@ -3,7 +3,7 @@
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
*)
-section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
+section {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
theory Int
imports Equiv_Relations Power Quotient Fun_Def
@@ -338,10 +338,10 @@
text{*An alternative condition is @{term "0 \<le> w"} *}
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
-by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
+by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
by transfer (clarsimp, arith)
@@ -355,7 +355,7 @@
lemma nat_eq_iff:
"nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
by transfer (clarsimp simp add: le_imp_diff_is_add)
-
+
corollary nat_eq_iff2:
"m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
using nat_eq_iff [of w m] by auto
@@ -378,7 +378,7 @@
lemma nat_2: "nat 2 = Suc (Suc 0)"
by simp
-
+
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
by transfer (clarsimp, arith)
@@ -404,7 +404,7 @@
lemma nat_diff_distrib':
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
by transfer clarsimp
-
+
lemma nat_diff_distrib:
"0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
by (rule nat_diff_distrib') auto
@@ -415,7 +415,7 @@
lemma le_nat_iff:
"k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
by transfer auto
-
+
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
by transfer (clarsimp simp add: less_diff_conv)
@@ -427,7 +427,7 @@
end
-lemma diff_nat_numeral [simp]:
+lemma diff_nat_numeral [simp]:
"(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
@@ -550,7 +550,7 @@
text {* Preliminaries *}
-lemma le_imp_0_less:
+lemma le_imp_0_less:
assumes le: "0 \<le> z"
shows "(0::int) < 1 + z"
proof -
@@ -565,7 +565,7 @@
proof (cases z)
case (nonneg n)
thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing
- le_imp_0_less [THEN order_less_imp_le])
+ le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
@@ -580,19 +580,19 @@
"1 + z + z \<noteq> (0::int)"
proof (cases z)
case (nonneg n)
- have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
+ have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
thus ?thesis using le_imp_0_less [OF le]
- by (auto simp add: add.assoc)
+ by (auto simp add: add.assoc)
next
case (neg n)
show ?thesis
proof
assume eq: "1 + z + z = 0"
have "(0::int) < 1 + (int n + int n)"
- by (simp add: le_imp_0_less add_increasing)
- also have "... = - (1 + z + z)"
- by (simp add: neg add.assoc [symmetric])
- also have "... = 0" by (simp add: eq)
+ by (simp add: le_imp_0_less add_increasing)
+ also have "... = - (1 + z + z)"
+ by (simp add: neg add.assoc [symmetric])
+ also have "... = 0" by (simp add: eq)
finally have "0<0" ..
thus False by blast
qed
@@ -699,12 +699,12 @@
hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
with odd_nonzero show False by blast
qed
-qed
+qed
lemma Nats_numeral [simp]: "numeral w \<in> Nats"
using of_nat_in_Nats [of "numeral w"] by simp
-lemma Ints_odd_less_0:
+lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
proof -
@@ -787,9 +787,7 @@
text{*Simplify the term @{term "w + - z"}*}
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
-apply (insert zless_nat_conj [of 1 z])
-apply auto
-done
+ using zless_nat_conj [of 1 z] by auto
text{*This simplifies expressions of the form @{term "int n = z"} where
z is an integer literal.*}
@@ -857,7 +855,7 @@
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
apply (cases "z=0 | w=0")
-apply (auto simp add: abs_if nat_mult_distrib [symmetric]
+apply (auto simp add: abs_if nat_mult_distrib [symmetric]
nat_mult_distrib_neg [symmetric] mult_less_0_iff)
done
@@ -867,9 +865,9 @@
done
lemma diff_nat_eq_if:
- "nat z - nat z' =
- (if z' < 0 then nat z
- else let d = z-z' in
+ "nat z - nat z' =
+ (if z' < 0 then nat z
+ else let d = z-z' in
if d < 0 then 0 else nat d)"
by (simp add: Let_def nat_diff_distrib [symmetric])
@@ -891,8 +889,8 @@
proof -
have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
by (auto simp add: int_ge_less_than_def)
- thus ?thesis
- by (rule wf_subset [OF wf_measure])
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
qed
text{*This variant looks odd, but is typical of the relations suggested
@@ -905,10 +903,10 @@
theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
proof -
- have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
+ have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
by (auto simp add: int_ge_less_than2_def)
- thus ?thesis
- by (rule wf_subset [OF wf_measure])
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
qed
(* `set:int': dummy construction *)
@@ -1009,7 +1007,7 @@
subsection{*Intermediate value theorems*}
lemma int_val_lemma:
- "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
+ "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
unfolding One_nat_def
apply (induct n)
@@ -1027,9 +1025,9 @@
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
lemma nat_intermed_int_val:
- "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
+ "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
-apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
+apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
in int_val_lemma)
unfolding One_nat_def
apply simp
@@ -1053,8 +1051,8 @@
proof
assume "2 \<le> \<bar>m\<bar>"
hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
- by (simp add: mult_mono 0)
- also have "... = \<bar>m*n\<bar>"
+ by (simp add: mult_mono 0)
+ also have "... = \<bar>m*n\<bar>"
by (simp add: abs_mult)
also have "... = 1"
by (simp add: mn)
@@ -1077,10 +1075,10 @@
qed
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
-apply (rule iffI)
+apply (rule iffI)
apply (frule pos_zmult_eq_1_iff_lemma)
- apply (simp add: mult.commute [of m])
- apply (frule pos_zmult_eq_1_iff_lemma, auto)
+ apply (simp add: mult.commute [of m])
+ apply (frule pos_zmult_eq_1_iff_lemma, auto)
done
lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
@@ -1226,14 +1224,14 @@
apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff)
done
-lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
+lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
proof cases
assume "a = 0" with assms show ?thesis by simp
next
assume "a \<noteq> 0"
- from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
- from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
+ from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
+ from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
from k k' have "a = a*k*k'" by simp
with mult_cancel_left1[where c="a" and b="k*k'"]
have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult.assoc)
@@ -1242,7 +1240,7 @@
qed
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
- using dvd_add_right_iff [of k "- n" m] by simp
+ using dvd_add_right_iff [of k "- n" m] by simp
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
@@ -1317,10 +1315,10 @@
then show "x dvd 1" by (auto intro: dvdI)
qed
-lemma zdvd_mult_cancel1:
+lemma zdvd_mult_cancel1:
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
proof
- assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
+ assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
by (cases "n >0") (auto simp add: minus_equation_iff)
next
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu Apr 30 15:28:01 2015 +0100
@@ -742,32 +742,28 @@
by (auto simp add: expand_fps_eq)
qed
-lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
- = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
- apply (rule fps_inverse_unique)
- apply simp
- apply (simp add: fps_eq_iff fps_mult_nth)
- apply clarsimp
+lemma setsum_zero_lemma:
+ fixes n::nat
+ assumes "0 < n"
+ shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
proof -
- fix n :: nat
- assume n: "n > 0"
- let ?f = "\<lambda>i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0"
- let ?g = "\<lambda>i. if i = n then 1 else if i=n - 1 then - 1 else 0"
+ let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
+ let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
have th1: "setsum ?f {0..n} = setsum ?g {0..n}"
by (rule setsum.cong) auto
have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}"
- apply (insert n)
apply (rule setsum.cong)
+ using assms
apply auto
done
have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
by auto
- from n have d: "{0.. n - 1} \<inter> {n} = {}"
+ from assms have d: "{0.. n - 1} \<inter> {n} = {}"
by auto
have f: "finite {0.. n - 1}" "finite {n}"
by auto
- show "setsum ?f {0..n} = 0"
+ show ?thesis
unfolding th1
apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
unfolding th2
@@ -775,6 +771,12 @@
done
qed
+lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
+ = Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
+ apply (rule fps_inverse_unique)
+ apply (simp_all add: fps_eq_iff fps_mult_nth setsum_zero_lemma)
+ done
+
subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *}
@@ -2885,8 +2887,7 @@
unfolding th
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)
+ apply simp
done
}
note th' = this
@@ -2894,11 +2895,7 @@
next
assume h: ?rhs
show ?lhs
- apply (subst h)
- apply simp
- apply (simp only: h[symmetric])
- apply simp
- done
+ by (metis E_deriv fps_deriv_mult_const_left h mult.left_commute)
qed
lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
@@ -2949,16 +2946,6 @@
apply auto
done
-lemma inverse_one_plus_X:
- "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::field)^n)"
- (is "inverse ?l = ?r")
-proof -
- have th: "?l * ?r = 1"
- by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
- have th': "?l $ 0 \<noteq> 0" by (simp add: )
- from fps_inverse_unique[OF th' th] show ?thesis .
-qed
-
lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
by (induct n) (auto simp add: field_simps E_add_mult)
@@ -2993,7 +2980,7 @@
where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
- unfolding inverse_one_plus_X
+ unfolding fps_inverse_X_plus1
by (simp add: L_def fps_eq_iff del: of_nat_Suc)
lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
@@ -3438,12 +3425,6 @@
finally show ?thesis .
qed
-lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
- by auto
-
-lemma eq_divide_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x = y / a \<longleftrightarrow> x * a = y"
- by auto
-
lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0"
unfolding fps_sin_def by simp
@@ -3454,7 +3435,7 @@
"fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_sin_def
apply (cases n, simp)
- apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+ apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done
@@ -3467,7 +3448,7 @@
lemma fps_cos_nth_add_2:
"fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_cos_def
- apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+ apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done
@@ -3500,7 +3481,7 @@
apply (simp add: nat_add_1_add_1 fps_sin_nth_add_2
del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
apply (subst minus_divide_left)
- apply (subst eq_divide_iff)
+ apply (subst nonzero_eq_divide_eq)
apply (simp del: of_nat_add of_nat_Suc)
apply (simp only: ac_simps)
done
@@ -3518,7 +3499,7 @@
apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2
del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
apply (subst minus_divide_left)
- apply (subst eq_divide_iff)
+ apply (subst nonzero_eq_divide_eq)
apply (simp del: of_nat_add of_nat_Suc)
apply (simp only: ac_simps)
done
@@ -3793,7 +3774,8 @@
THEN spec, of "\<lambda>x. x < e"]
have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
unfolding eventually_nhds
- apply safe
+ apply clarsimp
+ apply (rule FalseE)
apply auto --{*slow*}
done
then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
--- a/src/HOL/Library/Library.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Library/Library.thy Thu Apr 30 15:28:01 2015 +0100
@@ -54,6 +54,7 @@
Polynomial
Preorder
Product_Vector
+ Quadratic_Discriminant
Quotient_List
Quotient_Option
Quotient_Product
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quadratic_Discriminant.thy Thu Apr 30 15:28:01 2015 +0100
@@ -0,0 +1,182 @@
+(* Title: Roots of real quadratics
+ Author: Tim Makarios <tjm1983 at gmail.com>, 2012
+
+Originally from the AFP entry Tarskis_Geometry
+*)
+
+section "Roots of real quadratics"
+
+theory Quadratic_Discriminant
+imports Complex_Main
+begin
+
+definition discrim :: "[real,real,real] \<Rightarrow> real" where
+ "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
+
+lemma complete_square:
+ fixes a b c x :: "real"
+ assumes "a \<noteq> 0"
+ shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
+proof -
+ have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
+ by (simp add: algebra_simps power2_eq_square)
+ with `a \<noteq> 0`
+ have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0"
+ by simp
+ thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
+ unfolding discrim_def
+ by (simp add: power2_eq_square algebra_simps)
+qed
+
+lemma discriminant_negative:
+ fixes a b c x :: real
+ assumes "a \<noteq> 0"
+ and "discrim a b c < 0"
+ shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
+proof -
+ have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
+ with `discrim a b c < 0` have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
+ with complete_square and `a \<noteq> 0` show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
+qed
+
+lemma plus_or_minus_sqrt:
+ fixes x y :: real
+ assumes "y \<ge> 0"
+ shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
+proof
+ assume "x\<^sup>2 = y"
+ hence "sqrt (x\<^sup>2) = sqrt y" by simp
+ hence "sqrt y = \<bar>x\<bar>" by simp
+ thus "x = sqrt y \<or> x = - sqrt y" by auto
+next
+ assume "x = sqrt y \<or> x = - sqrt y"
+ hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
+ with `y \<ge> 0` show "x\<^sup>2 = y" by simp
+qed
+
+lemma divide_non_zero:
+ fixes x y z :: real
+ assumes "x \<noteq> 0"
+ shows "x * y = z \<longleftrightarrow> y = z / x"
+proof
+ assume "x * y = z"
+ with `x \<noteq> 0` show "y = z / x" by (simp add: field_simps)
+next
+ assume "y = z / x"
+ with `x \<noteq> 0` show "x * y = z" by simp
+qed
+
+lemma discriminant_nonneg:
+ fixes a b c x :: real
+ assumes "a \<noteq> 0"
+ and "discrim a b c \<ge> 0"
+ shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+ x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a)"
+proof -
+ from complete_square and plus_or_minus_sqrt and assms
+ have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+ (2 * a) * x + b = sqrt (discrim a b c) \<or>
+ (2 * a) * x + b = - sqrt (discrim a b c)"
+ by simp
+ also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
+ (2 * a) * x = (-b - sqrt (discrim a b c))"
+ by auto
+ also from `a \<noteq> 0` and divide_non_zero [of "2 * a" x]
+ have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a)"
+ by simp
+ finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+ x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a)" .
+qed
+
+lemma discriminant_zero:
+ fixes a b c x :: real
+ assumes "a \<noteq> 0"
+ and "discrim a b c = 0"
+ shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
+ using discriminant_nonneg and assms
+ by simp
+
+theorem discriminant_iff:
+ fixes a b c x :: real
+ assumes "a \<noteq> 0"
+ shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
+ discrim a b c \<ge> 0 \<and>
+ (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a))"
+proof
+ assume "a * x\<^sup>2 + b * x + c = 0"
+ with discriminant_negative and `a \<noteq> 0` have "\<not>(discrim a b c < 0)" by auto
+ hence "discrim a b c \<ge> 0" by simp
+ with discriminant_nonneg and `a * x\<^sup>2 + b * x + c = 0` and `a \<noteq> 0`
+ have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a)"
+ by simp
+ with `discrim a b c \<ge> 0`
+ show "discrim a b c \<ge> 0 \<and>
+ (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
+next
+ assume "discrim a b c \<ge> 0 \<and>
+ (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a))"
+ hence "discrim a b c \<ge> 0" and
+ "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
+ x = (-b - sqrt (discrim a b c)) / (2 * a)"
+ by simp_all
+ with discriminant_nonneg and `a \<noteq> 0` show "a * x\<^sup>2 + b * x + c = 0" by simp
+qed
+
+lemma discriminant_nonneg_ex:
+ fixes a b c :: real
+ assumes "a \<noteq> 0"
+ and "discrim a b c \<ge> 0"
+ shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
+ using discriminant_nonneg and assms
+ by auto
+
+lemma discriminant_pos_ex:
+ fixes a b c :: real
+ assumes "a \<noteq> 0"
+ and "discrim a b c > 0"
+ shows "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
+proof -
+ let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
+ let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
+ from `discrim a b c > 0` have "sqrt (discrim a b c) \<noteq> 0" by simp
+ hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
+ with `a \<noteq> 0` have "?x \<noteq> ?y" by simp
+ moreover
+ from discriminant_nonneg [of a b c ?x]
+ and discriminant_nonneg [of a b c ?y]
+ and assms
+ have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
+ ultimately
+ show "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0" by blast
+qed
+
+lemma discriminant_pos_distinct:
+ fixes a b c x :: real
+ assumes "a \<noteq> 0" and "discrim a b c > 0"
+ shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
+proof -
+ from discriminant_pos_ex and `a \<noteq> 0` and `discrim a b c > 0`
+ obtain w and z where "w \<noteq> z"
+ and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
+ by blast
+ show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
+ proof cases
+ assume "x = w"
+ with `w \<noteq> z` have "x \<noteq> z" by simp
+ with `a * z\<^sup>2 + b * z + c = 0`
+ show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+ next
+ assume "x \<noteq> w"
+ with `a * w\<^sup>2 + b * w + c = 0`
+ show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
+ qed
+qed
+
+end
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 30 15:28:01 2015 +0100
@@ -1200,7 +1200,7 @@
also have "... \<le> (e * norm z) * norm z ^ Suc n"
by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
- by (simp add: power_Suc)
+ by simp
qed
qed
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Apr 30 15:28:01 2015 +0100
@@ -458,9 +458,6 @@
subsection{* Taylor series for complex exponential, sine and cosine.*}
-context
-begin
-
declare power_Suc [simp del]
lemma Taylor_exp:
@@ -522,8 +519,9 @@
have *: "cmod (sin z -
(\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
- proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
-simplified])
+ proof (rule complex_taylor [of "closed_segment 0 z" n
+ "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
+ "exp\<bar>Im z\<bar>" 0 z, simplified])
show "convex (closed_segment 0 z)"
by (rule convex_segment [of 0 z])
next
@@ -600,7 +598,7 @@
done
qed
-end (* of context *)
+declare power_Suc [simp]
text{*32-bit Approximation to e*}
lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
@@ -2626,13 +2624,13 @@
lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
by (simp add: arccos_arctan arcsin_arccos_eq)
-lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
apply (subst Arcsin_Arccos_csqrt_pos)
- apply (auto simp: power_le_one zz)
+ apply (auto simp: power_le_one csqrt_1_diff_eq)
done
lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
@@ -2642,7 +2640,7 @@
lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
apply (subst Arccos_Arcsin_csqrt_pos)
- apply (auto simp: power_le_one zz)
+ apply (auto simp: power_le_one csqrt_1_diff_eq)
done
lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Apr 30 15:28:01 2015 +0100
@@ -575,9 +575,8 @@
by simp
also have "\<dots> \<le> (1 + x) ^ Suc n"
apply (subst diff_le_0_iff_le[symmetric])
+ using mult_left_mono[OF p Suc.prems]
apply (simp add: field_simps)
- using mult_left_mono[OF p Suc.prems]
- apply simp
done
finally show ?case
by (simp add: real_of_nat_Suc field_simps)
@@ -887,10 +886,8 @@
assumes "0 \<in> A"
shows "dependent A"
unfolding dependent_def
- apply (rule_tac x=0 in bexI)
using assms span_0
- apply auto
- done
+ by auto
lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"
by (metis subspace_add subspace_span)
--- a/src/HOL/Real.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Real.thy Thu Apr 30 15:28:01 2015 +0100
@@ -757,10 +757,7 @@
"of_nat n < (2::'a::linordered_idom) ^ n"
apply (induct n)
apply simp
-apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
-apply (drule (1) add_le_less_mono, simp)
-apply simp
-done
+by (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc)
lemma complete_real:
fixes S :: "real set"
@@ -807,7 +804,7 @@
have width: "\<And>n. B n - A n = (b - a) / 2^n"
apply (simp add: eq_divide_eq)
apply (induct_tac n, simp)
- apply (simp add: C_def avg_def algebra_simps)
+ apply (simp add: C_def avg_def power_Suc algebra_simps)
done
have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
@@ -1518,12 +1515,7 @@
by simp
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
-apply (induct "n")
-apply (auto simp add: real_of_nat_Suc)
-apply (subst mult_2)
-apply (erule add_less_le_mono)
-apply (rule two_realpow_ge_one)
-done
+ by (simp add: of_nat_less_two_power real_of_nat_def)
text {* TODO: no longer real-specific; rename and move elsewhere *}
lemma realpow_Suc_le_self:
@@ -1535,7 +1527,7 @@
lemma realpow_minus_mult:
fixes x :: "'a::monoid_mult"
shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
-by (simp add: power_commutes split add: nat_diff_split)
+by (simp add: power_Suc power_commutes split add: nat_diff_split)
text {* FIXME: declare this [simp] for all types, or not at all *}
lemma real_two_squares_add_zero_iff [simp]:
--- a/src/HOL/Set_Interval.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Set_Interval.thy Thu Apr 30 15:28:01 2015 +0100
@@ -1519,6 +1519,9 @@
using setsum_triangle_reindex [of f "Suc n"]
by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
+lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
+ by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
+
subsection{* Shifting bounds *}
lemma setsum_shift_bounds_nat_ivl:
@@ -1598,10 +1601,53 @@
proof -
from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
- by (induct n) (simp_all add: field_simps `y \<noteq> 0`)
+ by (induct n) (simp_all add: power_Suc field_simps `y \<noteq> 0`)
ultimately show ?thesis by simp
qed
+lemma diff_power_eq_setsum:
+ fixes y :: "'a::{comm_ring,monoid_mult}"
+ shows
+ "x ^ (Suc n) - y ^ (Suc n) =
+ (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)"
+ by (simp add: power_Suc)
+ also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
+ by (simp add: power_Suc algebra_simps)
+ 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)"
+ by (simp only: mult.left_commute)
+ also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
+ by (simp add: power_Suc field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
+ finally show ?case .
+qed simp
+
+corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
+using diff_power_eq_setsum[of x "n - 1" y]
+by (cases "n = 0") (simp_all add: field_simps)
+
+lemma power_diff_1_eq:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
+using diff_power_eq_setsum [of x _ 1]
+ by (cases n) auto
+
+lemma one_diff_power_eq':
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
+using diff_power_eq_setsum [of 1 _ x]
+ by (cases n) auto
+
+lemma one_diff_power_eq:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
+by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
+
subsection {* The formula for arithmetic sums *}
@@ -1665,9 +1711,6 @@
lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
by (subst setsum_subtractf_nat) auto
-lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
- by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
-
subsection {* Products indexed over intervals *}
syntax
--- a/src/HOL/Transcendental.thy Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Transcendental.thy Thu Apr 30 15:28:01 2015 +0100
@@ -53,63 +53,6 @@
subsection {* Properties of Power Series *}
-lemma lemma_realpow_diff:
- fixes y :: "'a::monoid_mult"
- shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
-proof -
- assume "p \<le> n"
- hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
- thus ?thesis by (simp add: power_commutes)
-qed
-
-lemma lemma_realpow_diff_sumr2:
- fixes y :: "'a::{comm_ring,monoid_mult}"
- shows
- "x ^ (Suc n) - y ^ (Suc n) =
- (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)"
- by simp
- 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)"
- by (simp only: Suc)
- 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)
- finally show ?case .
-qed simp
-
-corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
-using lemma_realpow_diff_sumr2[of x "n - 1" y]
-by (cases "n = 0") (simp_all add: field_simps)
-
-lemma lemma_realpow_rev_sumr:
- "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
- (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
- by (subst nat_diff_setsum_reindex[symmetric]) simp
-
-lemma power_diff_1_eq:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
-using lemma_realpow_diff_sumr2 [of x _ 1]
- by (cases n) auto
-
-lemma one_diff_power_eq':
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
-using lemma_realpow_diff_sumr2 [of 1 _ x]
- by (cases n) auto
-
-lemma one_diff_power_eq:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
-by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
-
lemma powser_zero:
fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1"
shows "(\<Sum>n. f n * 0 ^ n) = f 0"
@@ -533,6 +476,11 @@
"setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
by (simp add: setsum_subtractf)
+lemma lemma_realpow_rev_sumr:
+ "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
+ (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
+ by (subst nat_diff_setsum_reindex[symmetric]) simp
+
lemma lemma_termdiff2:
fixes h :: "'a :: {field}"
assumes h: "h \<noteq> 0"
@@ -544,7 +492,7 @@
apply (simp add: right_diff_distrib diff_divide_distrib h)
apply (simp add: mult.assoc [symmetric])
apply (cases "n", simp)
- apply (simp add: lemma_realpow_diff_sumr2 h
+ apply (simp add: diff_power_eq_setsum h
right_diff_distrib [symmetric] mult.assoc
del: power_Suc setsum_lessThan_Suc of_nat_Suc)
apply (subst lemma_realpow_rev_sumr)
@@ -554,7 +502,7 @@
apply (rule setsum.cong [OF refl])
apply (simp add: less_iff_Suc_add)
apply (clarify)
- apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
+ apply (simp add: setsum_right_distrib diff_power_eq_setsum ac_simps
del: setsum_lessThan_Suc power_Suc)
apply (subst mult.assoc [symmetric], subst power_add [symmetric])
apply (simp add: ac_simps)
@@ -1043,7 +991,7 @@
proof -
have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
(\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
- unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
+ unfolding right_diff_distrib[symmetric] diff_power_eq_setsum abs_mult
by auto
also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
proof (rule mult_left_mono)
@@ -1345,7 +1293,10 @@
lemma exp_of_nat_mult:
fixes x :: "'a::{real_normed_field,banach}"
shows "exp(of_nat n * x) = exp(x) ^ n"
- by (induct n) (auto simp add: distrib_left exp_add mult.commute)
+ by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute)
+
+corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
+ by (simp add: exp_of_nat_mult real_of_nat_def)
lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
@@ -1374,10 +1325,6 @@
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
by simp
-(*FIXME: superseded by exp_of_nat_mult*)
-lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
- by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
-
text {* Strict monotonicity of exponential. *}
lemma exp_ge_add_one_self_aux:
@@ -2361,10 +2308,7 @@
lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
apply (induct n)
apply simp
- apply (subgoal_tac "real(Suc n) = real n + 1")
- apply (erule ssubst)
- apply (subst powr_add, simp, simp)
- done
+ by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc)
lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
@@ -3159,7 +3103,7 @@
lemmas realpow_num_eq_if = power_eq_if
-lemma sumr_pos_lt_pair: (*FIXME A MESS, BUT THE REAL MESS IS THE NEXT THEOREM*)
+lemma sumr_pos_lt_pair:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>summable f;
\<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
@@ -3169,11 +3113,7 @@
apply (drule_tac k=k in summable_ignore_initial_segment)
apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
apply simp
-apply (frule sums_unique)
-apply (drule sums_summable, simp)
-apply (erule suminf_pos)
-apply (simp add: ac_simps)
-done
+by (metis (no_types, lifting) add.commute suminf_pos summable_def sums_unique)
lemma cos_two_less_zero [simp]:
"cos 2 < (0::real)"
@@ -3182,30 +3122,25 @@
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::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
+ then have sm: "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::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))))"
+ < (\<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))))))))
- < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
- fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
+ let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))"
+ have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))"
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))))))))"
+ then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))"
+ by (simp only: fact.simps(2) [of "Suc (?six4d)"] real_of_nat_def of_nat_mult of_nat_fact)
+ then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))"
by (simp add: inverse_eq_divide less_divide_eq)
- }
- note *** = this
- have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
- from ** show ?thesis by (rule sumr_pos_lt_pair)
- (simp add: divide_inverse mult.assoc [symmetric] ***)
+ }
+ then show ?thesis
+ by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps)
qed
ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule order_less_trans)