--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Dec 05 12:14:36 2017 +0100
@@ -367,6 +367,10 @@
"(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
unfolding holomorphic_on_def by (metis field_differentiable_sum)
+lemma holomorphic_on_prod [holomorphic_intros]:
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
+ by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
+
lemma holomorphic_pochhammer [holomorphic_intros]:
"f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Dec 05 12:14:36 2017 +0100
@@ -1790,8 +1790,8 @@
shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
by (simp_all add: powr_def exp_eq_polar)
-lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
- by (metis linear not_le of_real_Re powr_of_real)
+lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
+ by (metis not_le of_real_Re powr_of_real)
lemma norm_powr_real_mono:
"\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
@@ -1943,6 +1943,32 @@
with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
qed
+lemma tendsto_neg_powr_complex_of_real:
+ assumes "filterlim f at_top F" and "Re s < 0"
+ shows "((\<lambda>x. complex_of_real (f x) powr s) \<longlongrightarrow> 0) F"
+proof -
+ have "((\<lambda>x. norm (complex_of_real (f x) powr s)) \<longlongrightarrow> 0) F"
+ proof (rule Lim_transform_eventually)
+ from assms(1) have "eventually (\<lambda>x. f x \<ge> 0) F"
+ by (auto simp: filterlim_at_top)
+ thus "eventually (\<lambda>x. f x powr Re s = norm (of_real (f x) powr s)) F"
+ by eventually_elim (simp add: norm_powr_real_powr)
+ from assms show "((\<lambda>x. f x powr Re s) \<longlongrightarrow> 0) F"
+ by (intro tendsto_neg_powr)
+ qed
+ thus ?thesis by (simp add: tendsto_norm_zero_iff)
+qed
+
+lemma tendsto_neg_powr_complex_of_nat:
+ assumes "filterlim f at_top F" and "Re s < 0"
+ shows "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F"
+proof -
+ have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2)
+ by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real]
+ filterlim_compose[OF _ assms(1)] filterlim_real_sequentially filterlim_ident) auto
+ thus ?thesis by simp
+qed
+
lemma continuous_powr_complex:
assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
shows "continuous F (\<lambda>z. f z powr g z :: complex)"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Dec 05 12:14:36 2017 +0100
@@ -2991,6 +2991,17 @@
by (auto elim!: no_isolated_singularity)
qed
+lemma not_is_pole_holomorphic:
+ assumes "open A" "x \<in> A" "f holomorphic_on A"
+ shows "\<not>is_pole f x"
+proof -
+ have "continuous_on A f" by (intro holomorphic_on_imp_continuous_on) fact
+ with assms have "isCont f x" by (simp add: continuous_on_eq_continuous_at)
+ hence "f \<midarrow>x\<rightarrow> f x" by (simp add: isCont_def)
+ thus "\<not>is_pole f x" unfolding is_pole_def
+ using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto
+qed
+
(*order of the zero of f at z*)
definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Dec 05 12:14:36 2017 +0100
@@ -279,7 +279,31 @@
by (auto simp: convex_bound_lt inner_add)
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
- using convex_halfspace_lt[of "-a" "-b"] by auto
+ using convex_halfspace_lt[of "-a" "-b"] by auto
+
+lemma convex_halfspace_Re_ge: "convex {x. Re x \<ge> b}"
+ using convex_halfspace_ge[of b "1::complex"] by simp
+
+lemma convex_halfspace_Re_le: "convex {x. Re x \<le> b}"
+ using convex_halfspace_le[of "1::complex" b] by simp
+
+lemma convex_halfspace_Im_ge: "convex {x. Im x \<ge> b}"
+ using convex_halfspace_ge[of b \<i>] by simp
+
+lemma convex_halfspace_Im_le: "convex {x. Im x \<le> b}"
+ using convex_halfspace_le[of \<i> b] by simp
+
+lemma convex_halfspace_Re_gt: "convex {x. Re x > b}"
+ using convex_halfspace_gt[of b "1::complex"] by simp
+
+lemma convex_halfspace_Re_lt: "convex {x. Re x < b}"
+ using convex_halfspace_lt[of "1::complex" b] by simp
+
+lemma convex_halfspace_Im_gt: "convex {x. Im x > b}"
+ using convex_halfspace_gt[of b \<i>] by simp
+
+lemma convex_halfspace_Im_lt: "convex {x. Im x < b}"
+ using convex_halfspace_lt[of \<i> b] by simp
lemma convex_real_interval [iff]:
fixes a b :: "real"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue Dec 05 12:14:36 2017 +0100
@@ -819,6 +819,11 @@
unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
qed
+lemma lebesgue_real_scale:
+ assumes "c \<noteq> 0"
+ shows "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)"
+ using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all
+
lemma divideR_right:
fixes x y :: "'a::real_normed_vector"
shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
--- a/src/HOL/Analysis/Winding_Numbers.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Tue Dec 05 12:14:36 2017 +0100
@@ -706,7 +706,7 @@
- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
- show "- complex_of_real d \<noteq> complex_of_real e"
+ show "- d \<noteq> e"
using ad_not_ae by auto
show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0"
using z1 by auto
--- a/src/HOL/Library/Nonpos_Ints.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy Tue Dec 05 12:14:36 2017 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Nonpos_Ints.thy
+ (* Title: HOL/Library/Nonpos_Ints.thy
Author: Manuel Eberl, TU München
*)
@@ -237,7 +237,6 @@
lemma uminus_nonneg_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<ge>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<le>\<^sub>0"
apply (auto simp: nonpos_Reals_def nonneg_Reals_def)
apply (metis nonpos_Reals_of_real_iff minus_minus neg_le_0_iff_le of_real_minus)
- apply (metis neg_0_le_iff_le of_real_minus)
done
lemma uminus_nonpos_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<ge>\<^sub>0"
--- a/src/HOL/Number_Theory/Prime_Powers.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy Tue Dec 05 12:14:36 2017 +0100
@@ -127,6 +127,12 @@
lemma primepow_not_unit [simp]: "primepow p \<Longrightarrow> \<not>is_unit p"
by (auto simp: primepow_def is_unit_power_iff)
+lemma not_primepow_Suc_0_nat [simp]: "\<not>primepow (Suc 0)"
+ using primepow_gt_Suc_0[of "Suc 0"] by auto
+
+lemma primepow_gt_0_nat: "primepow n \<Longrightarrow> n > (0::nat)"
+ using primepow_gt_Suc_0[of n] by simp
+
lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1"
by (auto simp: primepow_def unit_factor_power)
@@ -204,6 +210,10 @@
by (auto simp: primepow_def power_mult intro!: exI[of _ q] exI[of _ "k * n"])
qed
+lemma primepow_power_iff_nat:
+ "p > 0 \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> primepow (p :: nat) \<and> n > 0"
+ by (rule primepow_power_iff) (simp_all add: unit_factor_nat_def)
+
lemma primepow_prime [simp]: "prime n \<Longrightarrow> primepow n"
by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])
@@ -211,6 +221,51 @@
"prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
by (subst primepow_power_iff) auto
+lemma aprimedivisor_vimage:
+ assumes "prime (p :: 'a :: factorial_semiring)"
+ shows "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
+proof safe
+ fix q assume q: "q \<in> primepow_factors n"
+ hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
+ let ?n = "multiplicity (aprimedivisor q) q"
+ from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n"
+ by (auto simp: primepow_decompose primepow_factors_def prime_multiplicity_gt_zero_iff
+ prime_aprimedivisor' prime_imp_prime_elem aprimedivisor_dvd')
+ thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" ..
+next
+ fix k :: nat assume k: "p ^ k dvd n" "k > 0"
+ with assms show "p ^ k \<in> aprimedivisor -` {p}"
+ by (auto simp: aprimedivisor_prime_power)
+ with assms k show "p ^ k \<in> primepow_factors n"
+ by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
+qed
+
+lemma aprimedivisor_nat:
+ assumes "n \<noteq> (Suc 0::nat)"
+ shows "prime (aprimedivisor n)" "aprimedivisor n dvd n"
+proof -
+ from assms have "\<exists>p. prime p \<and> p dvd n" by (intro prime_factor_nat) auto
+ from someI_ex[OF this, folded aprimedivisor_def]
+ show "prime (aprimedivisor n)" "aprimedivisor n dvd n" by blast+
+qed
+
+lemma aprimedivisor_gt_Suc_0:
+ assumes "n \<noteq> Suc 0"
+ shows "aprimedivisor n > Suc 0"
+proof -
+ from assms have "prime (aprimedivisor n)" by (rule aprimedivisor_nat)
+ thus "aprimedivisor n > Suc 0" by (simp add: prime_nat_iff)
+qed
+
+lemma aprimedivisor_le_nat:
+ assumes "n > Suc 0"
+ shows "aprimedivisor n \<le> n"
+proof -
+ from assms have "aprimedivisor n dvd n" by (intro aprimedivisor_nat) simp_all
+ with assms show "aprimedivisor n \<le> n"
+ by (intro dvd_imp_le) simp_all
+qed
+
lemma bij_betw_primepows:
"bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring)
(Collect prime \<times> UNIV) (Collect primepow)"
@@ -260,28 +315,7 @@
by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
subst primepow_prime_power)
(insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
-
-lemma aprimedivisor_vimage:
- assumes "prime (p :: 'a :: factorial_semiring)"
- shows "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
-proof safe
- fix q assume q: "q \<in> primepow_factors n"
- hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
- let ?n = "multiplicity (aprimedivisor q) q"
- from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n"
- using prime_aprimedivisor'[of q] aprimedivisor_dvd'[of q]
- by (subst primepow_decompose [symmetric])
- (auto simp: primepow_factors_def multiplicity_gt_zero_iff unit_factor_primepow
- intro: dvd_trans[OF multiplicity_dvd])
- thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" ..
-next
- fix k :: nat assume k: "p ^ k dvd n" "k > 0"
- with assms show "p ^ k \<in> aprimedivisor -` {p}"
- by (auto simp: aprimedivisor_prime_power)
- with assms k show "p ^ k \<in> primepow_factors n"
- by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
-qed
-
+
lemma primepow_factors_altdef:
fixes x :: "'a :: factorial_semiring"
assumes "x \<noteq> 0"
@@ -307,6 +341,84 @@
finally show ?thesis .
qed
+lemma aprimedivisor_primepow_factors_conv_prime_factorization:
+ assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring)"
+ shows "image_mset aprimedivisor (mset_set (primepow_factors n)) = prime_factorization n"
+ (is "?lhs = ?rhs")
+proof (intro multiset_eqI)
+ fix p :: 'a
+ show "count ?lhs p = count ?rhs p"
+ proof (cases "prime p")
+ case False
+ have "p \<notin># image_mset aprimedivisor (mset_set (primepow_factors n))"
+ proof
+ assume "p \<in># image_mset aprimedivisor (mset_set (primepow_factors n))"
+ then obtain q where "p = aprimedivisor q" "q \<in> primepow_factors n"
+ by (auto simp: finite_primepow_factors)
+ with False prime_aprimedivisor'[of q] have "q = 0 \<or> is_unit q" by auto
+ with \<open>q \<in> primepow_factors n\<close> show False by (auto simp: primepow_factors_def primepow_def)
+ qed
+ hence "count ?lhs p = 0" by (simp only: Multiset.not_in_iff)
+ with False show ?thesis by (simp add: count_prime_factorization)
+ next
+ case True
+ hence p: "p \<noteq> 0" "\<not>is_unit p" by auto
+ have "count ?lhs p = card (aprimedivisor -` {p} \<inter> primepow_factors n)"
+ by (simp add: count_image_mset finite_primepow_factors)
+ also have "aprimedivisor -` {p} \<inter> primepow_factors n = {p^k |k. k > 0 \<and> p ^ k dvd n}"
+ using True by (rule aprimedivisor_vimage)
+ also from True have "\<dots> = (\<lambda>k. p ^ k) ` {0<..multiplicity p n}"
+ by (subst power_dvd_iff_le_multiplicity) auto
+ also from p True have "card \<dots> = multiplicity p n"
+ by (subst card_image) (auto intro!: inj_onI dest: prime_power_inj)
+ also from True have "\<dots> = count (prime_factorization n) p"
+ by (simp add: count_prime_factorization)
+ finally show ?thesis .
+ qed
+qed
+
+lemma prime_elem_aprimedivisor_nat: "d > Suc 0 \<Longrightarrow> prime_elem (aprimedivisor d)"
+ using prime_aprimedivisor'[of d] by simp
+
+lemma aprimedivisor_gt_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d > 0"
+ using prime_aprimedivisor'[of d] by (simp add: prime_gt_0_nat)
+
+lemma aprimedivisor_gt_Suc_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d > Suc 0"
+ using prime_aprimedivisor'[of d] by (simp add: prime_gt_Suc_0_nat)
+
+lemma aprimedivisor_not_Suc_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d \<noteq> Suc 0"
+ using aprimedivisor_gt_Suc_0[of d] by (intro notI) auto
+
+lemma multiplicity_aprimedivisor_gt_0_nat [simp]:
+ "d > Suc 0 \<Longrightarrow> multiplicity (aprimedivisor d) d > 0"
+ by (subst multiplicity_gt_zero_iff) (auto intro: aprimedivisor_dvd')
+
+lemma primepowI:
+ "prime p \<Longrightarrow> k > 0 \<Longrightarrow> p ^ k = n \<Longrightarrow> primepow n \<and> aprimedivisor n = p"
+ unfolding primepow_def by (auto simp: aprimedivisor_prime_power)
+
+lemma not_primepowI:
+ assumes "prime p" "prime q" "p \<noteq> q" "p dvd n" "q dvd n"
+ shows "\<not>primepow n"
+ using assms by (auto simp: primepow_def dest!: prime_dvd_power[rotated] dest: primes_dvd_imp_eq)
+
+lemma sum_prime_factorization_conv_sum_primepow_factors:
+ assumes "n \<noteq> 0"
+ shows "(\<Sum>q\<in>primepow_factors n. f (aprimedivisor q)) = (\<Sum>p\<in>#prime_factorization n. f p)"
+proof -
+ from assms have "prime_factorization n = image_mset aprimedivisor (mset_set (primepow_factors n))"
+ by (rule aprimedivisor_primepow_factors_conv_prime_factorization [symmetric])
+ also have "(\<Sum>p\<in>#\<dots>. f p) = (\<Sum>q\<in>primepow_factors n. f (aprimedivisor q))"
+ by (simp add: image_mset.compositionality sum_unfold_sum_mset o_def)
+ finally show ?thesis ..
+qed
+
+lemma multiplicity_aprimedivisor_Suc_0_iff:
+ assumes "primepow (n :: 'a :: factorial_semiring)"
+ shows "multiplicity (aprimedivisor n) n = Suc 0 \<longleftrightarrow> prime n"
+ by (subst (3) primepow_decompose [OF assms, symmetric])
+ (insert assms, auto simp add: prime_power_iff intro!: prime_aprimedivisor')
+
definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
"mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
@@ -342,5 +454,50 @@
also have "\<dots> = n" using assms by (intro prime_factorization_nat [symmetric]) simp
finally show ?thesis .
qed
-
+
+lemma mangoldt_primepow:
+ "prime p \<Longrightarrow> mangoldt (p ^ k) = (if k > 0 then of_real (ln (real p)) else 0)"
+ by (simp add: mangoldt_def aprimedivisor_prime_power)
+
+lemma mangoldt_primepow' [simp]: "prime p \<Longrightarrow> k > 0 \<Longrightarrow> mangoldt (p ^ k) = of_real (ln (real p))"
+ by (subst mangoldt_primepow) auto
+
+lemma mangoldt_prime [simp]: "prime p \<Longrightarrow> mangoldt p = of_real (ln (real p))"
+ using mangoldt_primepow[of p 1] by simp
+
+lemma mangoldt_nonneg: "0 \<le> (mangoldt d :: real)"
+ using aprimedivisor_gt_Suc_0_nat[of d]
+ by (auto simp: mangoldt_def of_nat_le_iff[of 1 x for x, unfolded of_nat_1] Suc_le_eq
+ intro!: ln_ge_zero dest: primepow_gt_Suc_0)
+
+lemma norm_mangoldt [simp]:
+ "norm (mangoldt n :: 'a :: real_normed_algebra_1) = mangoldt n"
+proof (cases "primepow n")
+ case True
+ hence "prime (aprimedivisor n)"
+ by (intro prime_aprimedivisor')
+ (auto simp: primepow_def prime_gt_0_nat)
+ hence "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
+ with True show ?thesis by (auto simp: mangoldt_def abs_if)
+qed (auto simp: mangoldt_def)
+
+lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
+ using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .
+
+lemma mangoldt_le:
+ assumes "n > 0"
+ shows "mangoldt n \<le> ln n"
+proof (cases "primepow n")
+ case True
+ from True have "prime (aprimedivisor n)"
+ by (intro prime_aprimedivisor')
+ (auto simp: primepow_def prime_gt_0_nat)
+ hence gt_1: "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
+ from True have "mangoldt n = ln (aprimedivisor n)"
+ by (simp add: mangoldt_def)
+ also have "\<dots> \<le> ln n" using True gt_1
+ by (subst ln_le_cancel_iff) (auto intro!: Nat.gr0I dvd_imp_le aprimedivisor_dvd')
+ finally show ?thesis .
+qed (insert assms, auto simp: mangoldt_def)
+
end
\ No newline at end of file
--- a/src/HOL/Real_Vector_Spaces.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Dec 05 12:14:36 2017 +0100
@@ -366,6 +366,12 @@
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
+lemma minus_of_real_eq_of_real_iff [simp]: "-of_real x = of_real y \<longleftrightarrow> -x = y"
+ using of_real_eq_iff[of "-x" y] by (simp only: of_real_minus)
+
+lemma of_real_eq_minus_of_real_iff [simp]: "of_real x = -of_real y \<longleftrightarrow> x = -y"
+ using of_real_eq_iff[of x "-y"] by (simp only: of_real_minus)
+
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
by (rule ext) (simp add: of_real_def)
@@ -445,10 +451,7 @@
done
lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
- apply (auto simp add: Reals_def)
- apply (rule range_eqI)
- apply (rule of_real_minus [symmetric])
- done
+ by (auto simp add: Reals_def)
lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
apply (auto simp add: Reals_def)