--- a/src/HOL/Complex.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Complex.thy Wed Mar 18 14:30:12 2015 +0000
@@ -215,6 +215,18 @@
lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
by (metis mult.commute power2_i power_mult)
+lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
+ by simp
+
+lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
+ by simp
+
+lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
+ by auto
+
+lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
+ by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
+
subsection {* Vector Norm *}
instantiation complex :: real_normed_field
@@ -309,6 +321,9 @@
apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
done
+lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
+ by (simp add: norm_complex_def divide_simps complex_eq_iff)
+
text {* Properties of complex signum. *}
@@ -508,10 +523,10 @@
(auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
simp del: of_real_power)
-lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
+lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
by (auto simp add: Re_divide)
-lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
+lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
by (auto simp add: Im_divide)
lemma complex_div_gt_0:
@@ -526,27 +541,27 @@
by (simp add: Re_divide Im_divide zero_less_divide_iff)
qed
-lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
- and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
+lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
+ and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
using complex_div_gt_0 by auto
-lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
- by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+ by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
-lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
- by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+ by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
-lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
- by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+ by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
-lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
- by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+ by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
-lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
- by (metis not_le re_complex_div_gt_0)
+lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+ by (metis not_le Re_complex_div_gt_0)
-lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
- by (metis im_complex_div_gt_0 not_le)
+lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+ by (metis Im_complex_div_gt_0 not_le)
lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
by (induct s rule: infinite_finite_induct) auto
@@ -807,7 +822,7 @@
lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
-lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
+lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
proof cases
assume "Im z = 0" then show ?thesis
using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 18 14:30:12 2015 +0000
@@ -1718,8 +1718,10 @@
by (auto simp: real_power_down_fl intro!: power_down_le)
next
case True
- have "power_down_fl prec (Float 1 (- 2)) ?num \<le> real (Float 1 (- 2)) ^ ?num"
- by (auto simp: real_power_down_fl power_down)
+ have "power_down_fl prec (Float 1 (- 2)) ?num \<le> (Float 1 (- 2)) ^ ?num"
+ by (metis Float_le_zero_iff less_imp_le linorder_not_less not_numeral_le_zero numeral_One power_down_fl)
+ then have "power_down_fl prec (Float 1 (- 2)) ?num \<le> real (Float 1 (- 2)) ^ ?num"
+ by simp
also
have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
@@ -1727,7 +1729,7 @@
from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
- by (auto intro!: power_mono)
+ by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
finally show ?thesis
unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Mar 18 14:30:12 2015 +0000
@@ -8,8 +8,6 @@
imports Complex_Main
begin
-lemmas fact_Suc = fact.simps(2)
-
subsection {* The type of formal power series*}
typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
@@ -594,7 +592,7 @@
fix n :: nat
assume nn0: "n \<ge> n0"
then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
- by (auto intro: power_decreasing)
+ by (simp add: divide_simps)
{
assume "?s n = a"
then have "dist (?s n) a < r"
@@ -612,9 +610,9 @@
by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
split: split_if_asm intro: LeastI2_ex)
then have "dist (?s n) a < (1/2)^n"
- unfolding dth by (auto intro: power_strict_decreasing)
+ unfolding dth by (simp add: divide_simps)
also have "\<dots> \<le> (1/2)^n0"
- using nn0 by (auto intro: power_decreasing)
+ using nn0 by (simp add: divide_simps)
also have "\<dots> < r"
using n0 by simp
finally have "dist (?s n) a < r" .
--- a/src/HOL/NthRoot.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/NthRoot.thy Wed Mar 18 14:30:12 2015 +0000
@@ -626,19 +626,24 @@
apply (simp add: zero_less_divide_iff)
done
+lemma sqrt2_less_2: "sqrt 2 < (2::real)"
+ by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
+
+
text{*Needed for the infinitely close relation over the nonstandard
complex numbers*}
lemma lemma_sqrt_hcomplex_capprox:
"[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
-apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
-apply (erule_tac [2] lemma_real_divide_sqrt_less)
-apply (rule power2_le_imp_le)
-apply (auto simp add: zero_le_divide_iff power_divide)
-apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
-apply (rule add_mono)
-apply (auto simp add: four_x_squared intro: power_mono)
-done
-
+ apply (rule real_sqrt_sum_squares_less)
+ apply (auto simp add: abs_if field_simps)
+ apply (rule le_less_trans [where y = "x*2"])
+ using less_eq_real_def sqrt2_less_2 apply force
+ apply assumption
+ apply (rule le_less_trans [where y = "y*2"])
+ using less_eq_real_def sqrt2_less_2 mult_le_cancel_left
+ apply auto
+ done
+
text "Legacy theorem names:"
lemmas real_root_pos2 = real_root_power_cancel
lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
--- a/src/HOL/Power.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Power.thy Wed Mar 18 14:30:12 2015 +0000
@@ -51,6 +51,10 @@
"a ^ 1 = a"
by simp
+lemma power_Suc0_right [simp]:
+ "a ^ Suc 0 = a"
+ by simp
+
lemma power_commutes:
"a ^ n * a = a * a ^ n"
by (induct n) (simp_all add: mult.assoc)
@@ -127,6 +131,9 @@
end
+declare power_mult_distrib [where a = "numeral w" for w, simp]
+declare power_mult_distrib [where b = "numeral w" for w, simp]
+
context semiring_numeral
begin
@@ -301,6 +308,8 @@
"b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+declare nonzero_power_divide [where b = "numeral w" for w, simp]
+
end
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 18 14:30:12 2015 +0000
@@ -502,13 +502,26 @@
end
lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
- unfolding UN_box_eq_UNIV[symmetric]
- apply (subst SUP_emeasure_incseq[symmetric])
- apply (auto simp: incseq_def subset_box inner_add_left setprod_constant intro!: SUP_PInfty)
- apply (rule_tac x="Suc n" in exI)
- apply (rule order_trans[OF _ self_le_power])
- apply (auto simp: card_gt_0_iff real_of_nat_Suc)
- done
+proof -
+ { fix n::nat
+ let ?Ba = "Basis :: 'a set"
+ have "real n \<le> (2::real) ^ card ?Ba * real n"
+ by (simp add: mult_le_cancel_right1)
+ also
+ have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
+ apply (rule mult_left_mono)
+ apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le real_of_nat_le_iff real_of_nat_power self_le_power zero_less_Suc)
+ apply (simp add: DIM_positive)
+ done
+ finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
+ } note [intro!] = this
+ show ?thesis
+ unfolding UN_box_eq_UNIV[symmetric]
+ apply (subst SUP_emeasure_incseq[symmetric])
+ apply (auto simp: incseq_def subset_box inner_add_left setprod_constant
+ intro!: SUP_PInfty)
+ done
+qed
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
using emeasure_lborel_cbox[of x x] nonempty_Basis
--- a/src/HOL/ROOT Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/ROOT Wed Mar 18 14:30:12 2015 +0000
@@ -689,6 +689,7 @@
Determinants
PolyRoots
Complex_Analysis_Basics
+ Complex_Transcendental
document_files
"root.tex"
--- a/src/HOL/Real_Vector_Spaces.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Mar 18 14:30:12 2015 +0000
@@ -444,7 +444,8 @@
then show thesis ..
qed
-lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+lemma setsum_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto
@@ -453,7 +454,8 @@
by (metis Reals_0 setsum.infinite)
qed
-lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+lemma setprod_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto
--- a/src/HOL/Series.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Series.thy Wed Mar 18 14:30:12 2015 +0000
@@ -434,7 +434,7 @@
have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
by auto
have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
- by simp
+ by (simp add: mult.commute)
thus ?thesis using sums_divide [OF 2, of 2]
by simp
qed
--- a/src/HOL/Transcendental.thy Wed Mar 18 15:23:12 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 18 14:30:12 2015 +0000
@@ -1512,6 +1512,10 @@
using exp_bound [of "1/2"]
by (simp add: field_simps)
+corollary exp_le: "exp 1 \<le> (3::real)"
+ using exp_bound [of 1]
+ by (simp add: field_simps)
+
lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
@@ -3071,6 +3075,84 @@
lemma sin_two_pi [simp]: "sin (2*pi) = 0"
by (simp add: sin_double)
+
+lemma sin_times_sin:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "sin(w) * sin(z) = (cos(w - z) - cos(w + z)) / 2"
+ by (simp add: cos_diff cos_add)
+
+lemma sin_times_cos:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "sin(w) * cos(z) = (sin(w + z) + sin(w - z)) / 2"
+ by (simp add: sin_diff sin_add)
+
+lemma cos_times_sin:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "cos(w) * sin(z) = (sin(w + z) - sin(w - z)) / 2"
+ by (simp add: sin_diff sin_add)
+
+lemma cos_times_cos:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
+ by (simp add: cos_diff cos_add)
+
+lemma sin_plus_sin: (*FIXME field_inverse_zero should not be necessary*)
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
+ apply (simp add: mult.assoc sin_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma sin_diff_sin:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
+ apply (simp add: mult.assoc sin_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_plus_cos:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
+ apply (simp add: mult.assoc cos_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_diff_cos:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
+ apply (simp add: mult.assoc sin_times_sin)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_double_cos:
+ fixes z :: "'a::{real_normed_field,banach}"
+ shows "cos(2 * z) = 2 * cos z ^ 2 - 1"
+by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin:
+ fixes z :: "'a::{real_normed_field,banach}"
+ shows "cos(2 * z) = 1 - 2 * sin z ^ 2"
+by (simp add: cos_double sin_squared_eq)
+
+lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
+ by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
+
+lemma cos_pi_minus [simp]: "cos (pi - x) = -(cos x)"
+ by (metis cos_minus cos_periodic_pi uminus_add_conv_diff)
+
+lemma sin_minus_pi [simp]: "sin (x - pi) = - (sin x)"
+ by (simp add: sin_diff)
+
+lemma cos_minus_pi [simp]: "cos (x - pi) = -(cos x)"
+ by (simp add: cos_diff)
+
+lemma sin_2pi_minus [simp]: "sin (2*pi - x) = -(sin x)"
+ by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
+
+lemma cos_2pi_minus [simp]: "cos (2*pi - x) = cos x"
+ by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi
+ diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
+
lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)