Commit 4e04ee80 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

a massive simplification, thanks to sledgehammer, etc.

parent 3ce2153720f3
......@@ -151,7 +151,7 @@ proof transfer
apply (subst norm_cvec_scale[OF **(2)])
apply (subst inprod_cvec_bilinear1[OF *(2)])
apply (subst inprod_cvec_bilinear2[OF **(2)])
by (simp add: power2_eq_square)
by (simp add: power2_eq_square norm_mult)
thus "dist_fs_cvec z1 z2 = dist_fs_cvec z1' z2'"
using 1 dist_fs_cvec_iff
by simp
......@@ -239,10 +239,10 @@ proof-
ultimately
have "cmod(a - b) * (1+(cmod c)\<^sup>2) \<le> cmod (a-c) * cmod (1+cnj c*b) + cmod (c-b) * cmod(1 + cnj c*a)"
using complex_mod_triangle_ineq2[of "(a-c)*(1+cnj c*b)" "(c-b)*(1 + cnj c*a)"]
by simp
by (simp add: norm_mult)
moreover
have *: "\<And> a b c d b' d'. \<lbrakk>b \<le> b'; d \<le> d'; a \<ge> (0::real); c \<ge> 0\<rbrakk> \<Longrightarrow> a*b + c*d \<le> a*b' + c*d'"
by (smt mult_left_mono)
by (simp add: add_mono_thms_linordered_semiring(1) mult_left_mono)
have "cmod (a-c) * cmod (1+cnj c*b) + cmod (c-b) * cmod(1 + cnj c*a) \<le> cmod (a - c) * (sqrt (1+(cmod c)\<^sup>2) * sqrt (1+(cmod b)\<^sup>2)) + cmod (c - b) * (sqrt (1+(cmod c)\<^sup>2) * sqrt (1+(cmod a)\<^sup>2))"
using *[OF cmod_1_plus_mult_le[of "cnj c" b] cmod_1_plus_mult_le[of "cnj c" a], of "cmod (a-c)" "cmod (c-b)"]
by (simp add: field_simps real_sqrt_mult[symmetric])
......@@ -1228,8 +1228,7 @@ proof-
have "dsc \<ge> 0"
proof-
have "0 \<le> Re ((D - A)\<^sup>2) + 4 * Re ((cor (cmod B))\<^sup>2)"
using \<open>is_real A\<close> \<open>is_real D\<close>
by (subst cor_squared, subst Re_complex_of_real) (simp add: power2_eq_square)
using \<open>is_real A\<close> \<open>is_real D\<close> by simp
thus ?thesis
using \<open>dsc = sqrt(Re ((D-A)\<^sup>2 + 4*(B*cnj B)))\<close>
by (subst (asm) complex_mult_cnj_cmod) simp
......@@ -1491,6 +1490,9 @@ next
by (metis zero_less_divide_iff)
qed
lemma cor_sqrt_squared: "x \<ge> 0 \<Longrightarrow> (cor (sqrt x))\<^sup>2 = cor x"
by (simp add: power2_eq_square)
lemma chordal_circle1:
assumes "is_real A" and "is_real D" and "Re (A * D) < 0" and "r = sqrt(Re ((4*A)/(A-D)))"
shows "mk_circline A 0 0 D = chordal_circle \<infinity>\<^sub>h r"
......@@ -1523,19 +1525,15 @@ proof (transfer, transfer)
qed
moreover
have "- (cor (sqrt (Re (4 * A / (A - D)))))\<^sup>2 = cor (Re (4 / (D - A))) * A"
using \<open>Re ((4*A)/(A-D)) \<ge> 0\<close> \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close>
by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real Re_mult_real minus_divide_right)
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> \<open>Re ((4*A)/(A-D)) \<ge> 0\<close>
by (simp add: cor_sqrt_squared field_simps)
moreover
have "4 * (A - D) - 4 * A = 4 * -D"
by (simp add: field_simps)
hence "4 - 4 * A / (A - D) = -4 * D / (A - D)"
using \<open>A \<noteq> D\<close>
by (smt ab_semigroup_mult_class.mult_ac(1) diff_divide_eq_iff eq_iff_diff_eq_0 mult_minus1 mult_minus1_right mult_numeral_1_right right_diff_distrib_numeral times_divide_eq_right)
hence "4 - 4 * A / (A - D) = 4 * D / (D - A)"
by (metis (hide_lams, no_types) minus_diff_eq minus_divide_left minus_divide_right minus_mult_left)
have "4 - 4 * A / (A - D) = 4 * D / (D - A)"
using\<open>A \<noteq> D\<close>
by (simp add: divide_simps split: if_split_asm) (simp add: minus_mult_right)
hence **: "4 - (cor (sqrt (Re (4 * A / (A - D)))))\<^sup>2 = cor (Re (4 / (D - A))) * D"
using \<open>Re ((4*A)/(A-D)) \<ge> 0\<close> \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close>
by (subst cor_squared, subst real_sqrt_power[symmetric], simp)
by (simp add: cor_sqrt_squared field_simps)
ultimately
show "circline_eq_cmat (mk_circline_cmat A 0 0 D) (chordal_circle_cvec_cmat \<infinity>\<^sub>v r)"
using * \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> \<open>r = sqrt(Re ((4*A)/(A-D)))\<close>
......@@ -1569,25 +1567,17 @@ proof (transfer, transfer)
using chordal_circle_det_positive[of "Re D" "Re A"]
by (simp add: field_simps)
thus ?thesis
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close>
by (subst Re_divide_real, auto)
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> Re_divide_real by force
qed
have "4 * (D - A) - 4 * D = 4 * -A"
by (simp add: field_simps)
hence "4 - 4 * D / (D - A) = -4 * A / (D - A)"
using \<open>A \<noteq> D\<close>
by (smt ab_semigroup_mult_class.mult_ac(1) diff_divide_eq_iff eq_iff_diff_eq_0 mult_minus1 mult_minus1_right mult_numeral_1_right right_diff_distrib_numeral times_divide_eq_right)
hence "4 - 4 * D / (D - A) = 4 * A / (A - D)"
by (metis (hide_lams, no_types) minus_diff_eq minus_divide_left minus_divide_right minus_mult_left)
have "4 - 4 * D / (D - A) = 4 * A / (A - D)"
by (simp add: divide_simps split: if_split_asm) (simp add: \<open>A \<noteq> D\<close> minus_mult_right)
hence **: "4 - (cor (sqrt (Re ((4*D)/(D-A)))))\<^sup>2 = cor (Re (4 / (A - D))) * A"
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> \<open>Re (4 * D / (D - A)) \<ge> 0\<close>
by (subst cor_squared, subst real_sqrt_power[symmetric], simp)
by (simp add: cor_sqrt_squared field_simps)
moreover
have "- (cor (sqrt (Re ((4*D)/(D-A)))))\<^sup>2 = cor (Re (4 / (A - D))) * D"
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> \<open>Re ((4*D)/(D-A)) \<ge> 0\<close>
by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real minus_divide_right)
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> D\<close> \<open>Re (4 * D / (D - A)) \<ge> 0\<close>
by (simp add: cor_sqrt_squared field_simps)
ultimately
show "circline_eq_cmat (mk_circline_cmat A 0 0 D) (chordal_circle_cvec_cmat 0\<^sub>v r)"
using \<open>is_real A\<close> \<open>is_real D\<close> \<open>A \<noteq> 0 \<or> D \<noteq> 0\<close> \<open>r = sqrt (Re ((4*D)/(D-A)))\<close>
......@@ -1655,7 +1645,7 @@ proof (transfer, transfer)
by (simp, simp add: field_simps)
moreover
have "1 + a * cnj a \<noteq> 0"
by (subst complex_mult_cnj_cmod) (smt cor_add of_real_0 of_real_1 of_real_eq_iff realpow_square_minus_le)
by (simp add: complex_mult_cnj_cmod)
have "r\<^sup>2 = (4 - Re (?k * A)) / (1 + Re (a * cnj a))"
proof-
have "Re (a / B * A) \<ge> -1"
......@@ -1680,8 +1670,7 @@ proof (transfer, transfer)
using \<open>is_real ?k\<close> \<open>is_real A\<close> \<open>1 + a * cnj a \<noteq> 0\<close>
by (subst Re_divide_real, auto)
hence "(cor r)\<^sup>2 = (4 - ?k * A) / (1 + a * cnj a)"
using \<open>is_real ?k\<close> \<open>is_real A\<close>
using mult_reals[of ?k A]
using \<open>is_real ?k\<close> \<open>is_real A\<close> mult_reals[of ?k A]
by (simp add: cor_squared)
hence "4 - (cor r)\<^sup>2 * (a * cnj a + 1) = cor (Re ?k) * A"
using complex_of_real_Re[OF \<open>is_real (-4*a/B)\<close>]
......@@ -1696,8 +1685,7 @@ proof (transfer, transfer)
have "?k\<^sup>2 = cor ((cmod ?k)\<^sup>2)"
using cor_cmod_real[OF \<open>is_real ?k\<close>]
unfolding power2_eq_square
by (subst cor_mult) (metis minus_mult_minus)
unfolding power2_eq_square by force
hence "?k\<^sup>2 = ?k * cnj ?k"
using complex_mult_cnj_cmod[of ?k]
by simp
......
......@@ -474,7 +474,7 @@ proof transfer
show "euclidean_line_cmat H1 = euclidean_line_cmat H2"
using HH1 HH2 * \<open>k \<noteq> 0\<close>
by (cases "k > 0") (auto simp add: Let_def, simp_all add: sgn_eq 1 2)
by (cases "k > 0") (auto simp add: Let_def, simp_all add: norm_mult sgn_eq 1 2)
qed
lemma classic_line:
......
......@@ -112,7 +112,7 @@ proof-
by (simp add: power2_eq_square)
hence "- (Re a)\<^sup>2 \<ge> 0"
using zero_le_power2[of "cmod c"]
by (metis Re_complex_of_real cor_squared of_real_minus)
by (metis Re_complex_of_real of_real_minus of_real_power)
hence "a = 0"
using zero_le_power2[of "Re a"]
using \<open>cnj a = a\<close> eq_cnj_iff_real[of a]
......
......@@ -91,7 +91,7 @@ lemma scalsquare_vv_zero:
shows "(vec_cnj v) *\<^sub>v\<^sub>v v = 0 \<longleftrightarrow> v = vec_zero"
apply (cases v)
apply (auto simp add: vec_cnj_def field_simps complex_mult_cnj_cmod power2_eq_square)
apply (simp only: cor_add[symmetric] cor_mult[symmetric] of_real_eq_0_iff, simp)+
apply (metis (no_types) norm_eq_zero of_real_0 of_real_add of_real_eq_iff of_real_mult sum_squares_eq_zero_iff)+
done
(* ---------------------------------------------------------------------------- *)
......
......@@ -687,7 +687,7 @@ lemma moebius_rotation_preserve_cmod [simp]:
shows "cmod (to_complex (moebius_pt (moebius_rotation \<phi>) u)) = cmod (to_complex u)"
using assms
using inf_or_of_complex[of u]
by auto
by (auto simp: norm_mult)
(* -------------------------------------------------------------------------- *)
subsubsection \<open>Dilatation\<close>
......
......@@ -9,7 +9,7 @@ theory More_Complex
begin
text \<open>Conjugation and @{term cis}\<close>
declare cis_cnj[simp]
lemma rcis_cnj:
......@@ -24,14 +24,6 @@ formalization we abbreviate it to @{term cor}.\<close>
abbreviation cor :: "real \<Rightarrow> complex" where
"cor \<equiv> complex_of_real"
lemma cor_neg_one [simp]:
shows "cor (-1) = -1"
by simp
lemma neg_cor_neg_one [simp]:
shows "- cor (-1) = 1"
by simp
lemma cmod_cis [simp]:
assumes "a \<noteq> 0"
shows "cor (cmod a) * cis (arg a) = a"
......@@ -44,21 +36,13 @@ lemma cis_cmod [simp]:
using assms cmod_cis[of a]
by (simp add: field_simps)
lemma cor_add:
shows "cor (a + b) = cor a + cor b"
by (rule of_real_add)
lemma cor_mult:
shows "cor (a * b) = cor a * cor b"
by (rule of_real_mult)
lemma cor_squared:
shows "(cor x)\<^sup>2 = cor (x\<^sup>2)"
by (simp add: power2_eq_square)
lemma cor_sqrt_mult_cor_sqrt [simp]:
shows "cor (sqrt A) * cor (sqrt A) = cor \<bar>A\<bar>"
by (metis cor_mult real_sqrt_abs2 real_sqrt_mult)
by (metis of_real_mult real_sqrt_mult_self)
lemma cor_eq_0: "cor x + \<i> * cor y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
by (metis Complex_eq Im_complex_of_real Im_i_times Re_complex_of_real add_cancel_left_left of_real_eq_0_iff plus_complex.sel(2) zero_complex.code)
......@@ -128,7 +112,7 @@ lemma cmod_square:
lemma cor_cmod_power_4 [simp]:
shows "cor (cmod z) ^ 4 = (z * cnj z)\<^sup>2"
by (metis complex_norm_square cor_squared numeral_times_numeral power2_eq_square semiring_norm(11) semiring_norm(13) semiring_normalization_rules(36))
by (simp add: complex_mult_cnj_cmod)
lemma cnjE:
assumes "x \<noteq> 0"
......@@ -136,21 +120,13 @@ lemma cnjE:
using complex_mult_cnj_cmod[of x] assms
by (auto simp add: field_simps)
lemma cmod_mult [simp]:
shows "cmod (a * b) = cmod a * cmod b"
by (rule norm_mult)
lemma cmod_divide [simp]:
shows "cmod (a / b) = cmod a / cmod b"
by (rule norm_divide)
lemma cmod_cor_divide [simp]:
shows "cmod (z / cor k) = cmod z / \<bar>k\<bar>"
by auto
by (simp add: norm_divide)
lemma cmod_mult_minus_left_distrib [simp]:
shows "cmod (z*z1 - z*z2) = cmod z * cmod(z1 - z2)"
by (metis bounded_bilinear.diff_right bounded_bilinear_mult cmod_mult)
by (metis norm_mult right_diff_distrib)
lemma cmod_eqI:
assumes "z1 * cnj z1 = z2 * cnj z2"
......@@ -161,13 +137,7 @@ lemma cmod_eqI:
lemma cmod_eqE:
assumes "cmod z1 = cmod z2"
shows "z1 * cnj z1 = z2 * cnj z2"
proof-
from assms have "cor ((cmod z1)\<^sup>2) = cor ((cmod z2)\<^sup>2)"
by auto
thus ?thesis
using complex_mult_cnj_cmod
by auto
qed
by (simp add: assms complex_mult_cnj_cmod)
lemma cmod_eq_one [simp]:
shows "cmod a = 1 \<longleftrightarrow> a*cnj a = 1"
......@@ -251,24 +221,6 @@ lemma Im_divide_real:
using assms
by (simp add: complex_is_Real_iff)
lemma Re_half [simp]:
shows "Re (x / 2) = Re x / 2"
by (rule Re_divide_numeral)
lemma Re_double [simp]:
shows "Re (2 * x) = 2 * Re x"
using Re_mult_real[of "2" x]
by simp
lemma Im_half [simp]:
shows "Im (z / 2) = Im z / 2"
by (subst Im_divide_real, auto)
lemma Im_double [simp]:
shows "Im (2 * z) = 2 * Im z"
using Im_mult_real[of "2" z]
by simp
lemma Re_sgn:
assumes "is_real R"
shows "Re (sgn R) = sgn (Re R)"
......@@ -381,13 +333,7 @@ lemma cis_opposite_diff_cis [simp]:
lemma cis_add_cis_opposite [simp]:
shows "cis \<phi> + cis (-\<phi>) = 2 * cos \<phi>"
proof-
have "2 * cos \<phi> = (cis \<phi> + cnj (cis \<phi>))"
using Re_express_cnj[of "cis \<phi>"]
by (simp add: field_simps)
thus ?thesis
by simp
qed
by (metis cis.sel(1) cis_cnj complex_add_cnj)
text \<open>@{term cis} equal to 1 or -1\<close>
lemma cis_one [simp]:
......@@ -419,19 +365,11 @@ lemma is_real_arg2:
assumes "is_real z"
shows "arg z = 0 \<or> arg z = pi"
proof (cases "z = 0")
case True
thus ?thesis
by (auto simp add: arg_zero)
next
case False
hence "sin (arg z) = 0"
using assms rcis_cmod_arg[of z] Im_rcis[of "cmod z" "arg z"]
by auto
thus ?thesis
using arg_bounded[of z]
using sin_0_iff_canon
by simp
qed
by (smt (verit, best) Im_sgn assms cis.simps(2) cis_arg div_0 sin_zero_pi_iff)
qed (auto simp add: arg_zero)
lemma arg_complex_of_real_positive [simp]:
assumes "k > 0"
......@@ -440,7 +378,7 @@ proof-
have "cos (arg (Complex k 0)) > 0"
using assms
using rcis_cmod_arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "arg (Complex k 0)"]
by (smt complex.sel(1) mult_nonneg_nonpos norm_ge_zero)
using cmod_eq_Re by force
thus ?thesis
using assms is_real_arg2[of "cor k"]
unfolding complex_of_real_def
......@@ -453,7 +391,7 @@ lemma arg_complex_of_real_negative [simp]:
proof-
have "cos (arg (Complex k 0)) < 0"
using \<open>k < 0\<close> rcis_cmod_arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "arg (Complex k 0)"]
by (smt complex.sel(1) mult_nonneg_nonneg norm_ge_zero)
by (metis complex.sel(1) mult_less_0_iff norm_not_less_zero)
thus ?thesis
using assms is_real_arg2[of "cor k"]
unfolding complex_of_real_def
......@@ -481,15 +419,7 @@ lemma is_imag_arg1:
lemma is_imag_arg2:
assumes "is_imag z" and "z \<noteq> 0"
shows "arg z = pi/2 \<or> arg z = -pi/2"
proof-
have "cos (arg z) = 0"
using assms
by (metis Re_rcis no_zero_divisors norm_eq_zero rcis_cmod_arg)
thus ?thesis
using arg_bounded[of z]
using cos_0_iff_canon[of "arg z"]
by simp
qed
using arg_bounded assms cos_0_iff_canon cos_arg_i_mult_zero by presburger
lemma arg_complex_of_real_times_i_positive [simp]:
assumes "k > 0"
......@@ -510,7 +440,7 @@ lemma arg_complex_of_real_times_i_negative [simp]:
proof-
have "sin (arg (Complex 0 k)) < 0"
using \<open>k < 0\<close> rcis_cmod_arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "arg (Complex 0 k)"]
by (smt complex.sel(2) mult_nonneg_nonneg norm_ge_zero)
by (metis complex.sel(2) mult_less_0_iff norm_not_less_zero)
thus ?thesis
using assms is_imag_arg2[of "cor k * \<i>"]
using arg_zero complex_of_real_i[of k]
......@@ -527,16 +457,7 @@ lemma arg_minus_pi2_iff:
lemma arg_ii [simp]:
shows "arg \<i> = pi/2"
proof-
have "\<i> = cis (arg \<i>)"
using rcis_cmod_arg[of \<i>]
by (simp add: rcis_def)
hence "cos (arg \<i>) = 0" "sin (arg \<i>) = 1"
by (metis cis.simps(1) imaginary_unit.simps(1), metis cis.simps(2) imaginary_unit.simps(2))
thus ?thesis
using cos_0_iff_canon[of "arg \<i>"] arg_bounded[of \<i>]
by auto
qed
by (metis arg_pi2_iff imaginary_unit.sel zero_less_one)
lemma arg_minus_ii [simp]:
shows "arg (-\<i>) = -pi/2"
......@@ -561,21 +482,7 @@ lemma canon_ang_arg:
lemma arg_cis:
shows "arg (cis \<phi>) = \<downharpoonright>\<phi>\<downharpoonleft>"
proof (rule canon_ang_eqI[symmetric])
show "- pi < arg (cis \<phi>) \<and> arg (cis \<phi>) \<le> pi"
using arg_bounded
by simp
next
show "\<exists> k::int. arg (cis \<phi>) - \<phi> = 2*k*pi"
proof-
have "cis (arg (cis \<phi>)) = cis \<phi>"
using cis_arg[of "cis \<phi>"]
by auto
thus ?thesis
using cis_eq
by auto
qed
qed
using arg_unique canon_ang canon_ang_cos canon_ang_sin cis.ctr sgn_cis by presburger
text \<open>Cosine and sine of @{term arg}\<close>
......@@ -594,24 +501,7 @@ text \<open>Argument of product\<close>
lemma cis_arg_mult:
assumes "z1 * z2 \<noteq> 0"
shows "cis (arg (z1 * z2)) = cis (arg z1 + arg z2)"
proof-
have "z1 * z2 = cor (cmod z1) * cor (cmod z2) * cis (arg z1) * cis (arg z2)"
using rcis_cmod_arg[of z1, symmetric] rcis_cmod_arg[of z2, symmetric]
unfolding rcis_def
by algebra
hence "z1 * z2 = cor (cmod (z1 * z2)) * cis (arg z1 + arg z2)"
using cis_mult[of "arg z1" "arg z2"]
by auto
hence "cor (cmod (z1 * z2)) * cis (arg z1 + arg z2) = cor (cmod (z1 * z2)) * cis (arg (z1 * z2))"
using assms
using rcis_cmod_arg[of "z1*z2"]
unfolding rcis_def
by auto
thus ?thesis
using mult_cancel_left[of "cor (cmod (z1 * z2))" "cis (arg z1 + arg z2)" "cis (arg (z1 * z2))"]
using assms
by auto
qed
by (metis assms cis_arg cis_mult mult_eq_0_iff sgn_mult)
lemma arg_mult_2kpi:
assumes "z1 * z2 \<noteq> 0"
......@@ -644,33 +534,20 @@ lemma arg_mult_real_positive [simp]:
assumes "k > 0"
shows "arg (cor k * z) = arg z"
proof (cases "z = 0")
case True
thus ?thesis
by (auto simp add: arg_zero)
next
case False
thus ?thesis
using assms
using arg_mult[of "cor k" z]
by (auto simp add: canon_ang_arg)
qed
using arg_mult assms canon_ang_arg by force
qed (auto simp: arg_zero)
lemma arg_mult_real_negative [simp]:
assumes "k < 0"
shows "arg (cor k * z) = arg (-z)"
proof (cases "z = 0")
case True
thus ?thesis
by (auto simp add: arg_zero)
next
case False
thus ?thesis
using assms
using arg_mult[of "cor k" z]
using arg_mult[of "-1" z]
using arg_complex_of_real_negative[of k] arg_complex_of_real_negative[of "-1"]
by auto
qed
by (metis arg_mult_real_positive minus_mult_commute neg_0_less_iff_less of_real_minus minus_minus)
qed (auto simp: arg_zero)
lemma arg_div_real_positive [simp]:
assumes "k > 0"
......@@ -706,45 +583,14 @@ lemma arg_mult_eq:
assumes "z * z1 \<noteq> 0" and "z * z2 \<noteq> 0"
assumes "arg (z * z1) = arg (z * z2)"
shows "arg z1 = arg z2"
proof-
from assms have "\<downharpoonright>arg z + arg z1\<downharpoonleft> = \<downharpoonright>arg z + arg z2\<downharpoonleft>"
by (simp add: arg_mult)
then obtain x::int where *: "arg z1 - arg z2 = 2 * x * pi"
using canon_ang_eqE[of "arg z + arg z1" "arg z + arg z2"]
by auto
moreover
have "arg z1 - arg z2 < 2*pi" "arg z1 - arg z2 > -2*pi"
using arg_bounded[of z1] arg_bounded[of z2]
by auto
ultimately
have "-1 < x" "x < 1"
using divide_strict_right_mono[of "-pi" "pi * x" pi]
by auto
hence "x = 0"
by auto
thus ?thesis
using *
by simp
qed
by (metis (no_types, lifting) arg_cis assms canon_ang_arg cis_arg mult_eq_0_iff nonzero_mult_div_cancel_left sgn_divide)
text \<open>Argument of conjugate\<close>
lemma arg_cnj_pi:
assumes "arg z = pi"
shows "arg (cnj z) = pi"
proof-
have "cos (arg (cnj z)) = cos (arg z)"
using rcis_cmod_arg[of z, symmetric] Re_rcis[of "cmod z" "arg z"]
using rcis_cmod_arg[of "cnj z", symmetric] Re_rcis[of "cmod (cnj z)" "arg (cnj z)"]
by auto
hence "arg (cnj z) = arg z \<or> arg(cnj z) = -arg z"
using arg_bounded[of z] arg_bounded[of "cnj z"]
by (metis arccos_cos arccos_cos2 less_eq_real_def linorder_le_cases minus_minus)
thus ?thesis
using assms
using arg_bounded[of "cnj z"]
by auto
qed
using arg_pi_iff assms by auto
lemma arg_cnj_not_pi:
assumes "arg z \<noteq> pi"
......@@ -755,22 +601,13 @@ proof(cases "arg z = 0")
using eq_cnj_iff_real[of z] is_real_arg1[of z] by force
next
case False
have "cos (arg (cnj z)) = cos (arg z)"
using rcis_cmod_arg[of z] Re_rcis[of "cmod z" "arg z"]
using rcis_cmod_arg[of "cnj z"] Re_rcis[of "cmod (cnj z)" "arg (cnj z)"]
by auto
hence "arg (cnj z) = arg z \<or> arg(cnj z) = -arg z"
have "arg (cnj z) = arg z \<or> arg(cnj z) = -arg z"
using arg_bounded[of z] arg_bounded[of "cnj z"]
by (metis arccos_cos arccos_cos2 less_eq_real_def linorder_le_cases minus_minus)
by (smt (verit, best) arccos_cos arccos_cos2 cnj.sel(1) complex_cnj_zero_iff complex_mod_cnj cos_arg)
moreover
have "sin (arg (cnj z)) = -sin (arg z)"
using rcis_cmod_arg[of z] Im_rcis[of "cmod z" "arg z"]
using rcis_cmod_arg[of "cnj z"] Im_rcis[of "cmod (cnj z)" "arg (cnj z)"]
using calculation eq_cnj_iff_real is_real_arg2
by force
hence "arg (cnj z) \<noteq> arg z"
have "arg (cnj z) \<noteq> arg z"
using sin_0_iff_canon[of "arg (cnj z)"] arg_bounded False assms
by auto
by (metis complex_mod_cnj eq_cnj_iff_real is_real_arg2 rcis_cmod_arg)
ultimately
show ?thesis
by auto
......@@ -814,18 +651,7 @@ lemma arg_inv_2kpi:
lemma arg_inv:
assumes "z \<noteq> 0"
shows "arg (1 / z) = \<downharpoonright>- arg z\<downharpoonleft>"
proof-
obtain k::int where "arg(1 / z) = - arg z + 2*k*pi"
using arg_inv_2kpi[of z]
using assms
by auto
hence "\<downharpoonright>arg(1 / z)\<downharpoonleft> = \<downharpoonright>- arg z\<downharpoonleft>"
using canon_ang_eq
by(simp add:field_simps)
thus ?thesis
using canon_ang_arg[of "1 / z"]
by auto
qed
by (metis arg_inv_not_pi arg_inv_pi assms canon_ang_arg canon_ang_uminus_pi)
text \<open>Argument of quotient\<close>
......@@ -1033,8 +859,7 @@ next
thus ?thesis
using False
unfolding ccsqrt_def
by (simp add: rcis_mult real_sqrt_mult arg_mult)
(auto simp add: rcis_def)
by (smt (verit, best) arg_mult mult_minus_left mult_minus_right no_zero_divisors norm_mult rcis_def rcis_mult real_sqrt_mult)
qed
lemma csqrt_real:
......
......@@ -57,7 +57,7 @@ subsection \<open>Library Additions for Trigonometric Functions\<close>
(* -------------------------------------------------------------------------- *)
theory More_Transcendental
imports Complex_Main
imports Complex_Main "HOL-Library.Periodic_Fun"
begin
text \<open>Additional properties of @{term sin} and @{term cos} functions that are later used in proving
......@@ -82,45 +82,13 @@ lemma cos_odd_kpi [simp]:
fixes k::int
assumes "odd k"
shows "cos (k * pi) = -1"
proof (cases "k \<ge> 0")
case True
hence "odd (nat k)"
using \<open>odd k\<close>
by (auto simp add: even_nat_iff)
thus ?thesis
using \<open>k \<ge> 0\<close> cos_npi[of "nat k"]
by auto
next
case False
hence "-k \<ge> 0" "odd (nat (-k))"
using \<open>odd k\<close>
by (auto simp add: even_nat_iff)
thus ?thesis
using cos_npi[of "nat (-k)"]
by auto
qed
by (simp add: assms mult.commute)
lemma cos_even_kpi [simp]:
fixes k::int
assumes "even k"
shows "cos (k * pi) = 1"
proof (cases "k \<ge> 0")
case True
hence "even (nat k)"
using \<open>even k\<close>
by (simp add: even_nat_iff)
thus ?thesis
using \<open>k \<ge> 0\<close> cos_npi[of "nat k"]
by auto
next
case False
hence "-k \<ge> 0" "even (nat (-k))"
using \<open>even k\<close>
by (auto simp add: even_nat_iff)
thus ?thesis
using cos_npi[of "nat (-k)"]
by auto
qed
by (simp add: assms mult.commute)
lemma sin_pi2_plus_odd_kpi [simp]:
fixes k::int
......@@ -141,123 +109,17 @@ text \<open>Solving trigonometric equations and systems with special values (0,
lemma cos_0_iff_canon:
assumes "cos \<phi> = 0" and "-pi < \<phi>" and "\<phi> \<le> pi"
shows "\<phi> = pi/2 \<or> \<phi> = -pi/2"
proof-
obtain k::int where "odd k" "\<phi> = k * pi/2"
using cos_zero_iff_int[of \<phi>] assms(1)
by auto
thus ?thesis
proof (cases "k > 1 \<or> k < -1")
case True
hence "k \<ge> 3 \<or> k \<le> -3"
using \<open>odd k\<close>
by (smt dvd_refl even_minus)
hence "\<phi> \<ge> 3*pi/2 \<or> \<phi> \<le> -3*pi/2"
using mult_right_mono[of k "-3" "pi / 2"]
using \<open>\<phi> = k * pi/2\<close>
by auto
thus ?thesis
using \<open>- pi < \<phi>\<close> \<open>\<phi> \<le> pi\<close>
by auto
next