# HG changeset patch # User paulson # Date 1675092257 0 # Node ID c8597292cd412ce2828a3be798dc2bdc621248bd # Parent 5bf9a1b78f932b80afff45567bf90295ff7ec537 Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Algebra/QuotRing.thy --- a/src/HOL/Algebra/QuotRing.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Algebra/QuotRing.thy Mon Jan 30 15:24:17 2023 +0000 @@ -805,17 +805,15 @@ using h unfolding ring_iso_def bij_betw_def inj_on_def by auto have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)" - using bij_betw_inv_into h ring_iso_def by fastforce + by (simp add: bij_betw_inv_into h ring_iso_memE(5)) - show "inv_into (carrier R) h \ ring_iso S R" - apply (rule ring_iso_memI) - apply (simp add: h_surj inv_into_into) - apply (auto simp add: h_inv_bij) - using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] - apply (simp_all add: \ring R\ bij_betw_def bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules(5)) - using ring_iso_memE [OF h] bij_betw_inv_into_right [of h "carrier R" "carrier S"] - apply (simp add: \ring R\ inv_into_f_eq ring.ring_simprules(1)) - by (simp add: \ring R\ inv_into_f_eq ring.ring_simprules(6)) + have "inv_into (carrier R) h \ ring_hom S R" + using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] \ring R\ + by (simp add: bij_betw_imp_inj_on bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules ring_hom_memI) + moreover have "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)" + using h_inv_bij by force + ultimately show "inv_into (carrier R) h \ ring_iso S R" + by (simp add: ring_iso_def) qed corollary ring_iso_sym: diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy Mon Jan 30 15:24:17 2023 +0000 @@ -318,12 +318,26 @@ unfolding constant_on_def by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) +lemma constant_on_compose: + assumes "f constant_on A" + shows "g \ f constant_on A" + using assms by (auto simp: constant_on_def) + +lemma not_constant_onI: + "f x \ f y \ x \ A \ y \ A \ \f constant_on A" + unfolding constant_on_def by metis + +lemma constant_onE: + assumes "f constant_on S" and "\x. x\S \ f x = g x" + shows "g constant_on S" + using assms unfolding constant_on_def by simp + lemma constant_on_closureI: fixes f :: "_ \ 'b::t1_space" assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f" - shows "f constant_on (closure S)" -using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def -by metis + shows "f constant_on (closure S)" + using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def + by metis subsection\<^marker>\tag unimportant\ \Continuity relative to a union.\ diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Complex.thy Mon Jan 30 15:24:17 2023 +0000 @@ -521,6 +521,12 @@ lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" by (simp add: complex_eq_iff) +lemma in_image_cnj_iff: "z \ cnj ` A \ cnj z \ A" + by (metis complex_cnj_cnj image_iff) + +lemma image_cnj_conv_vimage_cnj: "cnj ` A = cnj -` A" + using in_image_cnj_iff by blast + lemma complex_cnj_zero [simp]: "cnj 0 = 0" by (simp add: complex_eq_iff) @@ -835,6 +841,15 @@ lemma cis_divide: "cis a / cis b = cis (a - b)" by (simp add: divide_complex_def cis_mult) +lemma divide_conv_cnj: "norm z = 1 \ x / z = x * cnj z" + by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square) + +lemma i_not_in_Reals [simp, intro]: "\ \ \" + by (auto simp: complex_is_Real_iff) + +lemma powr_power_complex: "z \ 0 \ n \ 0 \ (z powr u :: complex) ^ n = z powr (of_nat n * u)" + by (induction n) (auto simp: algebra_simps powr_add) + lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)" by (auto simp add: DeMoivre) @@ -853,6 +868,11 @@ lemma cis_multiple_2pi[simp]: "n \ \ \ cis (2 * pi * n) = 1" by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr) +lemma minus_cis: "-cis x = cis (x + pi)" + by (simp flip: cis_mult) + +lemma minus_cis': "-cis x = cis (x - pi)" + by (simp flip: cis_divide) subsubsection \$r(\cos \theta + i \sin \theta)$\ @@ -1246,6 +1266,9 @@ field_simps real_sqrt_mult[symmetric] real_sqrt_divide) qed +lemma norm_csqrt [simp]: "norm (csqrt z) = sqrt (norm z)" + by (metis abs_of_nonneg norm_ge_zero norm_mult power2_csqrt power2_eq_square real_sqrt_abs) + lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" by auto (metis power2_csqrt power_eq_0_iff) diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Deriv.thy Mon Jan 30 15:24:17 2023 +0000 @@ -82,9 +82,12 @@ lemma has_derivative_ident[derivative_intros, simp]: "((\x. x) has_derivative (\x. x)) F" by (simp add: has_derivative_def) -lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)" +lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) F" by (metis eq_id_iff has_derivative_ident) +lemma shift_has_derivative_id: "((+) d has_derivative (\x. x)) F" + using has_derivative_def by fastforce + lemma has_derivative_const[derivative_intros, simp]: "((\x. c) has_derivative (\x. 0)) F" by (simp add: has_derivative_def) diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Fun.thy Mon Jan 30 15:24:17 2023 +0000 @@ -353,6 +353,17 @@ lemma inj_on_imp_bij_betw: "inj_on f A \ bij_betw f A (f ` A)" unfolding bij_betw_def by simp +lemma bij_betw_DiffI: + assumes "bij_betw f A B" "bij_betw f C D" "C \ A" "D \ B" + shows "bij_betw f (A - C) (B - D)" + using assms unfolding bij_betw_def inj_on_def by auto + +lemma bij_betw_singleton_iff [simp]: "bij_betw f {x} {y} \ f x = y" + by (auto simp: bij_betw_def) + +lemma bij_betw_singletonI [intro]: "f x = y \ bij_betw f {x} {y}" + by auto + lemma bij_betw_apply: "\bij_betw f A B; a \ A\ \ f a \ B" unfolding bij_betw_def by auto diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Library/Countable_Set.thy Mon Jan 30 15:24:17 2023 +0000 @@ -72,7 +72,7 @@ lemma countable_infiniteE': assumes "countable A" "infinite A" obtains g where "bij_betw g (UNIV :: nat set) A" - using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast + by (meson assms bij_betw_inv countableE_infinite) lemma countable_enum_cases: assumes "countable S" diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Library/Product_Order.thy Mon Jan 30 15:24:17 2023 +0000 @@ -35,6 +35,9 @@ lemma Pair_le [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" unfolding less_eq_prod_def by simp +lemma atLeastAtMost_prod_eq: "{a..b} = {fst a..fst b} \ {snd a..snd b}" + by (auto simp: less_eq_prod_def) + instance prod :: (preorder, preorder) preorder proof fix x y z :: "'a \ 'b" diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Power.thy Mon Jan 30 15:24:17 2023 +0000 @@ -654,9 +654,18 @@ lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \ x < b ^ w" by (metis of_nat_less_iff of_nat_power) +lemma power2_nonneg_ge_1_iff: + assumes "x \ 0" + shows "x ^ 2 \ 1 \ x \ 1" + using assms by (auto intro: power2_le_imp_le) + +lemma power2_nonneg_gt_1_iff: + assumes "x \ 0" + shows "x ^ 2 > 1 \ x > 1" + using assms by (auto intro: power_less_imp_less_base) + end - text \Some @{typ nat}-specific lemmas:\ lemma mono_ge2_power_minus_self: @@ -822,12 +831,14 @@ end - subsection \Miscellaneous rules\ lemma (in linordered_semidom) self_le_power: "1 \ a \ 0 < n \ a \ a ^ n" using power_increasing [of 1 n a] power_one_right [of a] by auto +lemma power2_ge_1_iff: "x ^ 2 \ 1 \ x \ 1 \ x \ (-1 :: 'a :: linordered_idom)" + using abs_le_square_iff[of 1 x] by (auto simp: abs_if split: if_splits) + lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" unfolding One_nat_def by (cases m) simp_all diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Mon Jan 30 15:24:17 2023 +0000 @@ -159,6 +159,11 @@ by simp qed +lemma shift_zero_ident [simp]: + fixes f :: "'a \ 'b::real_vector" + shows "(+)0 \ f = f" + by force + lemma linear_scale_real: fixes r::real shows "linear f \ f (r * b) = r * f b" using linear_scale by fastforce diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Topological_Spaces.thy Mon Jan 30 15:24:17 2023 +0000 @@ -535,6 +535,16 @@ "eventually P (at a within s) \ (\S. open S \ a \ S \ (\x\S. x \ a \ x \ s \ P x))" by (simp add: eventually_nhds eventually_at_filter) +lemma eventually_at_in_open: + assumes "open A" "x \ A" + shows "eventually (\y. y \ A - {x}) (at x)" + using assms eventually_at_topological by blast + +lemma eventually_at_in_open': + assumes "open A" "x \ A" + shows "eventually (\y. y \ A) (at x)" + using assms eventually_at_topological by blast + lemma (in topological_space) at_within_open: "a \ S \ open S \ at a within S = at a" unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) @@ -569,6 +579,10 @@ unfolding trivial_limit_def eventually_at_topological by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff) +lemma (in t1_space) eventually_neq_at_within: + "eventually (\w. w \ x) (at z within A)" + by (smt (verit, ccfv_threshold) eventually_True eventually_at_topological separation_t1) + lemma (in perfect_space) at_neq_bot [simp]: "at a \ bot" by (simp add: at_eq_bot_iff not_open_singleton) diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Jan 30 10:15:01 2023 +0100 +++ b/src/HOL/Transcendental.thy Mon Jan 30 15:24:17 2023 +0000 @@ -1928,9 +1928,9 @@ proof - have "suminf (\n. inverse(fact (n+2)) * (x ^ (n + 2))) \ x\<^sup>2" proof - - have "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" + have "(\n. x\<^sup>2 / 2 * (1/2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1/2)))" by (intro sums_mult geometric_sums) simp - then have sumsx: "(\n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" + then have sumsx: "(\n. x\<^sup>2 / 2 * (1/2) ^ n) sums x\<^sup>2" by simp have "suminf (\n. inverse(fact (n+2)) * (x ^ (n + 2))) \ suminf (\n. (x\<^sup>2/2) * ((1/2)^n))" proof (intro suminf_le allI) @@ -1953,7 +1953,7 @@ qed show "summable (\n. inverse (fact (n + 2)) * x ^ (n + 2))" by (rule summable_exp [THEN summable_ignore_initial_segment]) - show "summable (\n. x\<^sup>2 / 2 * (1 / 2) ^ n)" + show "summable (\n. x\<^sup>2 / 2 * (1/2) ^ n)" by (rule sums_summable [OF sumsx]) qed also have "\ = x\<^sup>2" @@ -2066,7 +2066,7 @@ lemma ln_one_minus_pos_lower_bound: fixes x :: real - assumes a: "0 \ x" and b: "x \ 1 / 2" + assumes a: "0 \ x" and b: "x \ 1/2" shows "- x - 2 * x\<^sup>2 \ ln (1 - x)" proof - from b have c: "x < 1" by auto @@ -2120,7 +2120,7 @@ lemma abs_ln_one_plus_x_minus_x_bound_nonpos: fixes x :: real - assumes a: "-(1 / 2) \ x" and b: "x \ 0" + assumes a: "-(1/2) \ x" and b: "x \ 0" shows "\ln (1 + x) - x\ \ 2 * x\<^sup>2" proof - have *: "- (-x) - 2 * (-x)\<^sup>2 \ ln (1 - (- x))" @@ -2134,7 +2134,7 @@ lemma abs_ln_one_plus_x_minus_x_bound: fixes x :: real - assumes "\x\ \ 1 / 2" + assumes "\x\ \ 1/2" shows "\ln (1 + x) - x\ \ 2 * x\<^sup>2" proof (cases "0 \ x") case True @@ -3532,9 +3532,10 @@ lemma cos_minus [simp]: "cos (-x) = cos x" for x :: "'a::{real_normed_algebra_1,banach}" - using cos_minus_converges [of x] - by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel] - suminf_minus sums_iff equation_minus_iff) + using cos_minus_converges [of x] by (metis cos_def sums_unique) + +lemma cos_abs_real [simp]: "cos \x :: real\ = cos x" + by (simp add: abs_if) lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" for x :: "'a::{real_normed_field,banach}" @@ -4009,12 +4010,12 @@ lemma sin_pi_divide_n_ge_0 [simp]: assumes "n \ 0" - shows "0 \ sin (pi / real n)" + shows "0 \ sin (pi/real n)" by (rule sin_ge_zero) (use assms in \simp_all add: field_split_simps\) lemma sin_pi_divide_n_gt_0: assumes "2 \ n" - shows "0 < sin (pi / real n)" + shows "0 < sin (pi/real n)" by (rule sin_gt_zero) (use assms in \simp_all add: field_split_simps\) text\Proof resembles that of \cos_is_zero\ but with \<^term>\pi\ for the upper bound\ @@ -4101,7 +4102,7 @@ proof - obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0" using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add) - then have "x = real (n - 1) * (pi / 2)" + then have "x = real (n - 1) * (pi/2)" by (simp add: algebra_simps of_nat_diff) then show ?thesis by (simp add: \odd n\) @@ -4182,9 +4183,9 @@ lemma sin_zero_iff_int2: "sin x = 0 \ (\i::int. x = of_int i * pi)" proof - - have "sin x = 0 \ (\i. even i \ x = real_of_int i * (pi / 2))" + have "sin x = 0 \ (\i. even i \ x = real_of_int i * (pi/2))" by (auto simp: sin_zero_iff_int) - also have "... = (\j. x = real_of_int (2*j) * (pi / 2))" + also have "... = (\j. x = real_of_int (2*j) * (pi/2))" using dvd_triv_left by blast also have "... = (\i::int. x = of_int i * pi)" by auto @@ -4421,15 +4422,15 @@ finally show ?thesis . qed -lemma cos_45: "cos (pi / 4) = sqrt 2 / 2" -proof - - let ?c = "cos (pi / 4)" - let ?s = "sin (pi / 4)" +lemma cos_45: "cos (pi/4) = sqrt 2 / 2" +proof - + let ?c = "cos (pi/4)" + let ?s = "sin (pi/4)" have nonneg: "0 \ ?c" by (simp add: cos_ge_zero) - have "0 = cos (pi / 4 + pi / 4)" + have "0 = cos (pi/4 + pi/4)" by simp - also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2" + also have "cos (pi/4 + pi/4) = ?c\<^sup>2 - ?s\<^sup>2" by (simp only: cos_add power2_eq_square) also have "\ = 2 * ?c\<^sup>2 - 1" by (simp add: sin_squared_eq) @@ -4439,13 +4440,13 @@ using nonneg by (rule power2_eq_imp_eq) simp qed -lemma cos_30: "cos (pi / 6) = sqrt 3/2" -proof - - let ?c = "cos (pi / 6)" - let ?s = "sin (pi / 6)" +lemma cos_30: "cos (pi/6) = sqrt 3/2" +proof - + let ?c = "cos (pi/6)" + let ?s = "sin (pi/6)" have pos_c: "0 < ?c" by (rule cos_gt_zero) simp_all - have "0 = cos (pi / 6 + pi / 6 + pi / 6)" + have "0 = cos (pi/6 + pi/6 + pi/6)" by simp also have "\ = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s" by (simp only: cos_add sin_add) @@ -4458,23 +4459,34 @@ by (rule power2_eq_imp_eq) simp qed -lemma sin_45: "sin (pi / 4) = sqrt 2 / 2" +lemma sin_45: "sin (pi/4) = sqrt 2 / 2" by (simp add: sin_cos_eq cos_45) -lemma sin_60: "sin (pi / 3) = sqrt 3/2" +lemma sin_60: "sin (pi/3) = sqrt 3/2" by (simp add: sin_cos_eq cos_30) -lemma cos_60: "cos (pi / 3) = 1 / 2" -proof - - have "0 \ cos (pi / 3)" +lemma cos_60: "cos (pi/3) = 1/2" +proof - + have "0 \ cos (pi/3)" by (rule cos_ge_zero) (use pi_half_ge_zero in \linarith+\) then show ?thesis by (simp add: cos_squared_eq sin_60 power_divide power2_eq_imp_eq) qed -lemma sin_30: "sin (pi / 6) = 1 / 2" +lemma sin_30: "sin (pi/6) = 1/2" by (simp add: sin_cos_eq cos_60) +lemma cos_120: "cos (2 * pi/3) = -1/2" + and sin_120: "sin (2 * pi/3) = sqrt 3 / 2" + using sin_double[of "pi/3"] cos_double[of "pi/3"] + by (simp_all add: power2_eq_square sin_60 cos_60) + +lemma cos_120': "cos (pi * 2 / 3) = -1/2" + using cos_120 by (subst mult.commute) + +lemma sin_120': "sin (pi * 2 / 3) = sqrt 3 / 2" + using sin_120 by (subst mult.commute) + lemma cos_integer_2pi: "n \ \ \ cos(2 * pi * n) = 1" by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute) @@ -4563,13 +4575,13 @@ unfolding tan_def sin_double cos_double sin_squared_eq by (simp add: power2_eq_square) -lemma tan_30: "tan (pi / 6) = 1 / sqrt 3" +lemma tan_30: "tan (pi/6) = 1 / sqrt 3" unfolding tan_def by (simp add: sin_30 cos_30) -lemma tan_45: "tan (pi / 4) = 1" +lemma tan_45: "tan (pi/4) = 1" unfolding tan_def by (simp add: sin_45 cos_45) -lemma tan_60: "tan (pi / 3) = sqrt 3" +lemma tan_60: "tan (pi/3) = sqrt 3" unfolding tan_def by (simp add: sin_60 cos_60) lemma DERIV_tan [simp]: "cos x \ 0 \ DERIV tan x :> inverse ((cos x)\<^sup>2)" @@ -4667,7 +4679,7 @@ by (meson less_le_trans minus_pi_half_less_zero tan_total_pos) next case ge - with tan_total_pos [of "-y"] obtain x where "0 \ x" "x < pi / 2" "tan x = - y" + with tan_total_pos [of "-y"] obtain x where "0 \ x" "x < pi/2" "tan x = - y" by force then show ?thesis by (rule_tac x="-x" in exI) auto @@ -4675,7 +4687,7 @@ proposition tan_total: "\! x. -(pi/2) < x \ x < (pi/2) \ tan x = y" proof - - have "u = v" if u: "- (pi / 2) < u" "u < pi / 2" and v: "- (pi / 2) < v" "v < pi / 2" + have "u = v" if u: "- (pi/2) < u" "u < pi/2" and v: "- (pi/2) < v" "v < pi/2" and eq: "tan u = tan v" for u v proof (cases u v rule: linorder_cases) case less @@ -4706,8 +4718,8 @@ ultimately show ?thesis using DERIV_unique [OF _ DERIV_tan] by fastforce qed auto - then have "\!x. - (pi / 2) < x \ x < pi / 2 \ tan x = y" - if x: "- (pi / 2) < x" "x < pi / 2" "tan x = y" for x + then have "\!x. - (pi/2) < x \ x < pi/2 \ tan x = y" + if x: "- (pi/2) < x" "x < pi/2" "tan x = y" for x using that by auto then show ?thesis using lemma_tan_total1 [where y = y] @@ -4984,6 +4996,10 @@ unfolding arcsin_def using the1_equality [OF sin_total] by simp +lemma arcsin_unique: + assumes "-pi/2 \ x" and "x \ pi/2" and "sin x = y" shows "arcsin y = x" + using arcsin_sin[of x] assms by force + lemma arcsin_0 [simp]: "arcsin 0 = 0" using arcsin_sin [of 0] by simp @@ -4996,6 +5012,13 @@ lemma arcsin_minus: "- 1 \ x \ x \ 1 \ arcsin (- x) = - arcsin x" by (metis (no_types, opaque_lifting) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus) +lemma arcsin_one_half [simp]: "arcsin (1/2) = pi / 6" + and arcsin_minus_one_half [simp]: "arcsin (-(1/2)) = -pi / 6" + by (intro arcsin_unique; simp add: sin_30 field_simps)+ + +lemma arcsin_one_over_sqrt_2: "arcsin (1 / sqrt 2) = pi / 4" + by (rule arcsin_unique) (auto simp: sin_45 field_simps) + lemma arcsin_eq_iff: "\x\ \ 1 \ \y\ \ 1 \ arcsin x = arcsin y \ x = y" by (metis abs_le_iff arcsin minus_le_iff) @@ -5036,6 +5059,10 @@ lemma arccos_cos2: "x \ 0 \ - pi \ x \ arccos (cos x) = -x" by (auto simp: arccos_def intro!: the1_equality cos_total) +lemma arccos_unique: + assumes "0 \ x" and "x \ pi" and "cos x = y" shows "arccos y = x" + using arccos_cos assms by blast + lemma cos_arcsin: assumes "- 1 \ x" "x \ 1" shows "cos (arcsin x) = sqrt (1 - x\<^sup>2)" @@ -5061,8 +5088,7 @@ qed lemma arccos_0 [simp]: "arccos 0 = pi/2" - by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero - pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One) + using arccos_cos pi_half_ge_zero by fastforce lemma arccos_1 [simp]: "arccos 1 = 0" using arccos_cos by force @@ -5071,8 +5097,14 @@ by (metis arccos_cos cos_pi order_refl pi_ge_zero) lemma arccos_minus: "-1 \ x \ x \ 1 \ arccos (- x) = pi - arccos x" - by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1 - minus_diff_eq uminus_add_conv_diff) + by (smt (verit, ccfv_threshold) arccos arccos_cos cos_minus cos_minus_pi) + +lemma arccos_one_half [simp]: "arccos (1/2) = pi / 3" + and arccos_minus_one_half [simp]: "arccos (-(1/2)) = 2 * pi / 3" + by (intro arccos_unique; simp add: cos_60 cos_120)+ + +lemma arccos_one_over_sqrt_2: "arccos (1 / sqrt 2) = pi / 4" + by (rule arccos_unique) (auto simp: cos_45 field_simps) corollary arccos_minus_abs: assumes "\x\ \ 1" @@ -5211,9 +5243,9 @@ lemma isCont_arctan: "isCont arctan x" proof - - obtain u where u: "- (pi / 2) < u" "u < arctan x" + obtain u where u: "- (pi/2) < u" "u < arctan x" by (meson arctan arctan_less_iff linordered_field_no_lb) - obtain v where v: "arctan x < v" "v < pi / 2" + obtain v where v: "arctan x < v" "v < pi/2" by (meson arctan_less_iff arctan_ubound linordered_field_no_ub) have "isCont arctan (tan (arctan x))" proof (rule isCont_inverse_function2 [of u "arctan x" v]) @@ -5442,6 +5474,9 @@ lemma arcsin_le_arcsin: "- 1 \ x \ x \ y \ y \ 1 \ arcsin x \ arcsin y" using arcsin_le_mono by auto +lemma arcsin_nonneg: "x \ {0..1} \ arcsin x \ 0" + using arcsin_le_arcsin[of 0 x] by simp + lemma arccos_less_mono: "\x\ \ 1 \ \y\ \ 1 \ arccos x < arccos y \ y < x" by (rule trans [OF cos_mono_less_eq [symmetric]]) (use arccos_ubound arccos_lbound in auto) @@ -5490,15 +5525,15 @@ proof - have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0" proof (rule sin_eq_0_pi) - show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)" + show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x)" using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms by (simp add: algebra_simps) next - show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi" + show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x) < pi" using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms by (simp add: algebra_simps) next - show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0" + show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x)) = 0" using assms by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan power2_eq_square square_eq_1_iff) @@ -5574,14 +5609,14 @@ subsection \Machin's formula\ -lemma arctan_one: "arctan 1 = pi / 4" +lemma arctan_one: "arctan 1 = pi/4" by (rule arctan_unique) (simp_all add: tan_45 m2pi_less_pi) lemma tan_total_pi4: assumes "\x\ < 1" - shows "\z. - (pi / 4) < z \ z < pi / 4 \ tan z = x" + shows "\z. - (pi/4) < z \ z < pi/4 \ tan z = x" proof - show "- (pi / 4) < arctan x \ arctan x < pi / 4 \ tan (arctan x) = x" + show "- (pi/4) < arctan x \ arctan x < pi/4 \ tan (arctan x) = x" unfolding arctan_one [symmetric] arctan_minus [symmetric] unfolding arctan_less_iff using assms by (auto simp: arctan) @@ -5591,13 +5626,13 @@ assumes "\x\ \ 1" "\y\ < 1" shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))" proof (rule arctan_unique [symmetric]) - have "- (pi / 4) \ arctan x" "- (pi / 4) < arctan y" + have "- (pi/4) \ arctan x" "- (pi/4) < arctan y" unfolding arctan_one [symmetric] arctan_minus [symmetric] unfolding arctan_le_iff arctan_less_iff using assms by auto from add_le_less_mono [OF this] show 1: "- (pi/2) < arctan x + arctan y" by simp - have "arctan x \ pi / 4" "arctan y < pi / 4" + have "arctan x \ pi/4" "arctan y < pi/4" unfolding arctan_one [symmetric] unfolding arctan_le_iff arctan_less_iff using assms by auto @@ -5610,7 +5645,7 @@ lemma arctan_double: "\x\ < 1 \ 2 * arctan x = arctan ((2 * x) / (1 - x\<^sup>2))" by (metis arctan_add linear mult_2 not_less power2_eq_square) -theorem machin: "pi / 4 = 4 * arctan (1 / 5) - arctan (1 / 239)" +theorem machin: "pi/4 = 4 * arctan (1 / 5) - arctan (1/239)" proof - have "\1 / 5\ < (1 :: real)" by auto @@ -5622,17 +5657,17 @@ from arctan_add[OF less_imp_le[OF this] this] have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto moreover - have "\1\ \ (1::real)" and "\1 / 239\ < (1::real)" + have "\1\ \ (1::real)" and "\1/239\ < (1::real)" by auto - from arctan_add[OF this] have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" + from arctan_add[OF this] have "arctan 1 + arctan (1/239) = arctan (120 / 119)" by auto - ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)" + ultimately have "arctan 1 + arctan (1/239) = 4 * arctan (1 / 5)" by auto then show ?thesis unfolding arctan_one by algebra qed -lemma machin_Euler: "5 * arctan (1 / 7) + 2 * arctan (3 / 79) = pi / 4" +lemma machin_Euler: "5 * arctan (1 / 7) + 2 * arctan (3 / 79) = pi/4" proof - have 17: "\1 / 7\ < (1 :: real)" by auto with arctan_double have "2 * arctan (1 / 7) = arctan (7 / 24)" @@ -6007,11 +6042,11 @@ have c_minus_minus: "?c (- 1) i = - ?c 1 i" for i by auto - have "arctan (- 1) = arctan (tan (-(pi / 4)))" + have "arctan (- 1) = arctan (tan (-(pi/4)))" unfolding tan_45 tan_minus .. - also have "\ = - (pi / 4)" + also have "\ = - (pi/4)" by (rule arctan_tan) (auto simp: order_less_trans[OF \- (pi/2) < 0\ pi_gt_zero]) - also have "\ = - (arctan (tan (pi / 4)))" + also have "\ = - (arctan (tan (pi/4)))" unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric]) (auto simp: order_less_trans[OF \- (2 * pi) < 0\ pi_gt_zero]) also have "\ = - (arctan 1)" @@ -6089,10 +6124,10 @@ by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff) qed -theorem pi_series: "pi / 4 = (\k. (-1)^k * 1 / real (k * 2 + 1))" +theorem pi_series: "pi/4 = (\k. (-1)^k * 1 / real (k * 2 + 1))" (is "_ = ?SUM") proof - - have "pi / 4 = arctan 1" + have "pi/4 = arctan 1" using arctan_one by auto also have "\ = ?SUM" using arctan_series[of 1] by auto @@ -6597,7 +6632,7 @@ lemma sinh_plus_cosh: "sinh x + cosh x = exp x" proof - - have "sinh x + cosh x = (1 / 2) *\<^sub>R (exp x + exp x)" + have "sinh x + cosh x = (1/2) *\<^sub>R (exp x + exp x)" by (simp add: sinh_def cosh_def algebra_simps) also have "\ = exp x" by (rule scaleR_half_double) finally show ?thesis . @@ -6608,7 +6643,7 @@ lemma cosh_minus_sinh: "cosh x - sinh x = exp (-x)" proof - - have "cosh x - sinh x = (1 / 2) *\<^sub>R (exp (-x) + exp (-x))" + have "cosh x - sinh x = (1/2) *\<^sub>R (exp (-x) + exp (-x))" by (simp add: sinh_def cosh_def algebra_simps) also have "\ = exp (-x)" by (rule scaleR_half_double) finally show ?thesis . @@ -6895,10 +6930,10 @@ proof - have *: "((\x. - exp (- x)) \ (-0::real)) at_top" by (intro tendsto_minus filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top) - have "filterlim (\x. (1 / 2) * (-exp (-x) + exp x) :: real) at_top at_top" + have "filterlim (\x. (1/2) * (-exp (-x) + exp x) :: real) at_top at_top" by (rule filterlim_tendsto_pos_mult_at_top[OF _ _ filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top) - also have "(\x. (1 / 2) * (-exp (-x) + exp x) :: real) = sinh" + also have "(\x. (1/2) * (-exp (-x) + exp x) :: real) = sinh" by (simp add: fun_eq_iff sinh_def) finally show ?thesis . qed @@ -6915,10 +6950,10 @@ proof - have *: "((\x. exp (- x)) \ (0::real)) at_top" by (intro filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top) - have "filterlim (\x. (1 / 2) * (exp (-x) + exp x) :: real) at_top at_top" + have "filterlim (\x. (1/2) * (exp (-x) + exp x) :: real) at_top at_top" by (rule filterlim_tendsto_pos_mult_at_top[OF _ _ filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top) - also have "(\x. (1 / 2) * (exp (-x) + exp x) :: real) = cosh" + also have "(\x. (1/2) * (exp (-x) + exp x) :: real) = cosh" by (simp add: fun_eq_iff cosh_def) finally show ?thesis . qed