diff --git a/thys/Complex_Geometry/Chordal_Metric.thy b/thys/Complex_Geometry/Chordal_Metric.thy index 10a747d1aed6a941cf8d95f01209004bb6af9af0..27336fc9f4357af51d3eda34c176b3ae79099578 100644 --- a/thys/Complex_Geometry/Chordal_Metric.thy +++ b/thys/Complex_Geometry/Chordal_Metric.thy @@ -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) \ 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 *: "\ a b c d b' d'. \b \ b'; d \ d'; a \ (0::real); c \ 0\ \ a*b + c*d \ 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) \ 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 \ 0" proof- have "0 \ Re ((D - A)\<^sup>2) + 4 * Re ((cor (cmod B))\<^sup>2)" - using \is_real A\ \is_real D\ - by (subst cor_squared, subst Re_complex_of_real) (simp add: power2_eq_square) + using \is_real A\ \is_real D\ by simp thus ?thesis using \dsc = sqrt(Re ((D-A)\<^sup>2 + 4*(B*cnj B)))\ 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 \ 0 \ (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 \\<^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 \Re ((4*A)/(A-D)) \ 0\ \is_real A\ \is_real D\ \A \ D\ - by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real Re_mult_real minus_divide_right) + using \is_real A\ \is_real D\ \A \ D\ \Re ((4*A)/(A-D)) \ 0\ + 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 \A \ D\ - 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\A \ D\ + 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 \Re ((4*A)/(A-D)) \ 0\ \is_real A\ \is_real D\ \A \ D\ - 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 \\<^sub>v r)" using * \is_real A\ \is_real D\ \A \ D\ \r = sqrt(Re ((4*A)/(A-D)))\ @@ -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 \is_real A\ \is_real D\ \A \ D\ - by (subst Re_divide_real, auto) + using \is_real A\ \is_real D\ \A \ D\ 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 \A \ D\ - 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: \A \ D\ minus_mult_right) hence **: "4 - (cor (sqrt (Re ((4*D)/(D-A)))))\<^sup>2 = cor (Re (4 / (A - D))) * A" using \is_real A\ \is_real D\ \A \ D\ \Re (4 * D / (D - A)) \ 0\ - 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 \is_real A\ \is_real D\ \A \ D\ \Re ((4*D)/(D-A)) \ 0\ - by (subst cor_squared, subst real_sqrt_power[symmetric], simp) (simp add: Re_divide_real minus_divide_right) - + using \is_real A\ \is_real D\ \A \ D\ \Re (4 * D / (D - A)) \ 0\ + 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 \is_real A\ \is_real D\ \A \ 0 \ D \ 0\ \r = sqrt (Re ((4*D)/(D-A)))\ @@ -1655,7 +1645,7 @@ proof (transfer, transfer) by (simp, simp add: field_simps) moreover have "1 + a * cnj a \ 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) \ -1" @@ -1680,8 +1670,7 @@ proof (transfer, transfer) using \is_real ?k\ \is_real A\ \1 + a * cnj a \ 0\ by (subst Re_divide_real, auto) hence "(cor r)\<^sup>2 = (4 - ?k * A) / (1 + a * cnj a)" - using \is_real ?k\ \is_real A\ - using mult_reals[of ?k A] + using \is_real ?k\ \is_real A\ 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 \is_real (-4*a/B)\] @@ -1696,8 +1685,7 @@ proof (transfer, transfer) have "?k\<^sup>2 = cor ((cmod ?k)\<^sup>2)" using cor_cmod_real[OF \is_real ?k\] - 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 diff --git a/thys/Complex_Geometry/Circlines.thy b/thys/Complex_Geometry/Circlines.thy index 06dc59a204f7c1c640057b3cdbf63b5d1ada88fd..f8ef5924573fc3d613d1fd11b8293bc62c1f1062 100644 --- a/thys/Complex_Geometry/Circlines.thy +++ b/thys/Complex_Geometry/Circlines.thy @@ -474,7 +474,7 @@ proof transfer show "euclidean_line_cmat H1 = euclidean_line_cmat H2" using HH1 HH2 * \k \ 0\ - 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: diff --git a/thys/Complex_Geometry/Hermitean_Matrices.thy b/thys/Complex_Geometry/Hermitean_Matrices.thy index cdda002372978861b8bf2fd0edd797b41b7e80e3..75fc68de228a120b84ea1cb95c4c759ce49f3851 100644 --- a/thys/Complex_Geometry/Hermitean_Matrices.thy +++ b/thys/Complex_Geometry/Hermitean_Matrices.thy @@ -112,7 +112,7 @@ proof- by (simp add: power2_eq_square) hence "- (Re a)\<^sup>2 \ 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 \cnj a = a\ eq_cnj_iff_real[of a] diff --git a/thys/Complex_Geometry/Matrices.thy b/thys/Complex_Geometry/Matrices.thy index 075f3b5222b65f65711a955be58dd3afbaf46ff0..1a2cfc8659a1db99152c8084a5cd138e25834479 100644 --- a/thys/Complex_Geometry/Matrices.thy +++ b/thys/Complex_Geometry/Matrices.thy @@ -91,7 +91,7 @@ lemma scalsquare_vv_zero: shows "(vec_cnj v) *\<^sub>v\<^sub>v v = 0 \ 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 (* ---------------------------------------------------------------------------- *) diff --git a/thys/Complex_Geometry/Moebius.thy b/thys/Complex_Geometry/Moebius.thy index 5c756d6d50a2551ee3db7aa86768fd9a1fce3e26..10a0df2089d61f8b89566bb527bac9171ea30d85 100644 --- a/thys/Complex_Geometry/Moebius.thy +++ b/thys/Complex_Geometry/Moebius.thy @@ -687,7 +687,7 @@ lemma moebius_rotation_preserve_cmod [simp]: shows "cmod (to_complex (moebius_pt (moebius_rotation \) u)) = cmod (to_complex u)" using assms using inf_or_of_complex[of u] - by auto + by (auto simp: norm_mult) (* -------------------------------------------------------------------------- *) subsubsection \Dilatation\ diff --git a/thys/Complex_Geometry/More_Complex.thy b/thys/Complex_Geometry/More_Complex.thy index 29f0c73a442660752cf968b02fa95c036fa01e1b..64ccd4a0c5a7af33f4178f8c2897119e9516afb2 100644 --- a/thys/Complex_Geometry/More_Complex.thy +++ b/thys/Complex_Geometry/More_Complex.thy @@ -9,7 +9,7 @@ theory More_Complex begin text \Conjugation and @{term cis}\ - + declare cis_cnj[simp] lemma rcis_cnj: @@ -24,14 +24,6 @@ formalization we abbreviate it to @{term cor}.\ abbreviation cor :: "real \ complex" where "cor \ 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 \ 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 \A\" - 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 + \ * cor y = 0 \ x = 0 \ 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 \ 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 / \k\" - 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 \ 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 \ + cis (-\) = 2 * cos \" -proof- - have "2 * cos \ = (cis \ + cnj (cis \))" - using Re_express_cnj[of "cis \"] - by (simp add: field_simps) - thus ?thesis - by simp -qed + by (metis cis.sel(1) cis_cnj complex_add_cnj) text \@{term cis} equal to 1 or -1\ lemma cis_one [simp]: @@ -419,19 +365,11 @@ lemma is_real_arg2: assumes "is_real z" shows "arg z = 0 \ 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 \k < 0\ 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 \ 0" shows "arg z = pi/2 \ 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 \k < 0\ 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 * \"] using arg_zero complex_of_real_i[of k] @@ -527,16 +457,7 @@ lemma arg_minus_pi2_iff: lemma arg_ii [simp]: shows "arg \ = pi/2" -proof- - have "\ = cis (arg \)" - using rcis_cmod_arg[of \] - by (simp add: rcis_def) - hence "cos (arg \) = 0" "sin (arg \) = 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 \"] arg_bounded[of \] - by auto -qed + by (metis arg_pi2_iff imaginary_unit.sel zero_less_one) lemma arg_minus_ii [simp]: shows "arg (-\) = -pi/2" @@ -561,21 +482,7 @@ lemma canon_ang_arg: lemma arg_cis: shows "arg (cis \) = \\\" -proof (rule canon_ang_eqI[symmetric]) - show "- pi < arg (cis \) \ arg (cis \) \ pi" - using arg_bounded - by simp -next - show "\ k::int. arg (cis \) - \ = 2*k*pi" - proof- - have "cis (arg (cis \)) = cis \" - using cis_arg[of "cis \"] - 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 \Cosine and sine of @{term arg}\ @@ -594,24 +501,7 @@ text \Argument of product\ lemma cis_arg_mult: assumes "z1 * z2 \ 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 \ 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 \ 0" and "z * z2 \ 0" assumes "arg (z * z1) = arg (z * z2)" shows "arg z1 = arg z2" -proof- - from assms have "\arg z + arg z1\ = \arg z + arg z2\" - 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 \Argument of conjugate\ 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 \ 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 \ 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 \ arg(cnj z) = -arg z" + have "arg (cnj z) = arg z \ 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) \ arg z" + have "arg (cnj z) \ 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 \ 0" shows "arg (1 / z) = \- arg z\" -proof- - obtain k::int where "arg(1 / z) = - arg z + 2*k*pi" - using arg_inv_2kpi[of z] - using assms - by auto - hence "\arg(1 / z)\ = \- arg z\" - 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 \Argument of quotient\ @@ -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: diff --git a/thys/Complex_Geometry/More_Transcendental.thy b/thys/Complex_Geometry/More_Transcendental.thy index ae1d3b39e12cf6f34fcc4205fadbd9e8fc39f1b5..41494749f3af464b45171fb0aa6f3477a531071b 100644 --- a/thys/Complex_Geometry/More_Transcendental.thy +++ b/thys/Complex_Geometry/More_Transcendental.thy @@ -57,7 +57,7 @@ subsection \Library Additions for Trigonometric Functions\ (* -------------------------------------------------------------------------- *) theory More_Transcendental - imports Complex_Main + imports Complex_Main "HOL-Library.Periodic_Fun" begin text \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 \ 0") - case True - hence "odd (nat k)" - using \odd k\ - by (auto simp add: even_nat_iff) - thus ?thesis - using \k \ 0\ cos_npi[of "nat k"] - by auto -next - case False - hence "-k \ 0" "odd (nat (-k))" - using \odd k\ - 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 \ 0") - case True - hence "even (nat k)" - using \even k\ - by (simp add: even_nat_iff) - thus ?thesis - using \k \ 0\ cos_npi[of "nat k"] - by auto -next - case False - hence "-k \ 0" "even (nat (-k))" - using \even k\ - 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 \Solving trigonometric equations and systems with special values (0, lemma cos_0_iff_canon: assumes "cos \ = 0" and "-pi < \" and "\ \ pi" shows "\ = pi/2 \ \ = -pi/2" -proof- - obtain k::int where "odd k" "\ = k * pi/2" - using cos_zero_iff_int[of \] assms(1) - by auto - thus ?thesis - proof (cases "k > 1 \ k < -1") - case True - hence "k \ 3 \ k \ -3" - using \odd k\ - by (smt dvd_refl even_minus) - hence "\ \ 3*pi/2 \ \ \ -3*pi/2" - using mult_right_mono[of k "-3" "pi / 2"] - using \\ = k * pi/2\ - by auto - thus ?thesis - using \- pi < \\ \\ \ pi\ - by auto - next - case False - hence "k = -1 \ k = 0 \ k = 1" - by auto - hence "k = -1 \ k = 1" - using \odd k\ - by auto - thus ?thesis - using \\ = k * pi/2\ - by auto - qed -qed + by (smt (verit, best) arccos_0 arccos_cos assms cos_minus divide_minus_left) lemma sin_0_iff_canon: assumes "sin \ = 0" and "-pi < \" and "\ \ pi" shows "\ = 0 \ \ = pi" -proof- - obtain k::int where "even k" "\ = k * pi/2" - using sin_zero_iff_int[of \] assms(1) - by auto - thus ?thesis - proof (cases "k > 2 \ k < 0") - case True - hence "k \ 4 \ k \ -2" - using \even k\ - by (smt evenE) - hence "\ \ 2*pi \ \ \ -pi" - proof - assume "4 \ k" - hence "4 * pi/2 \ \" - using mult_right_mono[of "4" "k" "pi/2"] - by (subst \\ = k * pi/2\) auto - thus ?thesis - by simp - next - assume "k \ -2" - hence "-2*pi/2 \ \" - using mult_right_mono[of "k" "-2" "pi/2"] - by (subst \\ = k * pi/2\, auto) - thus ?thesis - by simp - qed - thus ?thesis - using \- pi < \\ \\ \ pi\ - by auto - next - case False - hence "k = 0 \ k = 1 \ k = 2" - by auto - hence "k = 0 \ k = 2" - using \even k\ - by auto - thus ?thesis - using \\ = k * pi/2\ - by auto - qed -qed + using assms sin_eq_0_pi by force lemma cos0_sin1: - assumes "cos \ = 0" and "sin \ = 1" + assumes "sin \ = 1" shows "\ k::int. \ = pi/2 + 2*k*pi" -proof- - from \cos \ = 0\ - obtain k::int where "odd k" "\ = k * (pi / 2)" - using cos_zero_iff_int[of "\"] - by auto - then obtain k'::int where "k = 2*k' + 1" - using oddE by blast - hence "\ = pi/2 + (k' * pi)" - using \\ = k * (pi / 2)\ - by (auto simp add: field_simps) - hence "even k'" - using \sin \ = 1\ sin_pi2_plus_odd_kpi[of k'] - by auto - thus ?thesis - using \\ = pi /2 + (k' * pi)\ - unfolding even_iff_mod_2_eq_zero - by auto -qed - -lemma cos1_sin0: - assumes "cos \ = 1" and "sin \ = 0" - shows "\ k::int. \ = 2*k*pi" -proof- - from \sin \ = 0\ - obtain k::int where "even k" "\ = k * (pi / 2)" - using sin_zero_iff_int[of "\"] - by auto - then obtain k'::int where "k = 2*k'" - using evenE by blast - hence "\ = k' * pi" - using \\ = k * (pi / 2)\ - by (auto simp add: field_simps) - hence "even k'" - using \cos \ = 1\ cos_odd_kpi[of k'] - by auto - thus ?thesis - using \\ = k' * pi\ - using assms(1) cos_one_2pi_int by auto -qed + by (smt (verit, ccfv_threshold) assms cos_diff cos_one_2pi_int cos_pi_half mult_cancel_right1 sin_pi_half sin_plus_pi) (* TODO: add lemmas for cos = -1, sin = 0 and cos = 0, sin = -1 *) @@ -268,9 +130,7 @@ lemma sin_inj: assumes "-pi/2 \ \ \ \ \ pi/2" and "-pi/2 \ \' \ \' \ pi/2" assumes "\ \ \'" shows "sin \ \ sin \'" - using assms - using sin_monotone_2pi[of \ \'] sin_monotone_2pi[of \' \] - by (cases "\ < \'") auto + by (metis assms divide_minus_left sin_inj_pi) text \Periodicity of trigonometric functions\ @@ -280,56 +140,22 @@ that dependency\ lemma sin_periodic_nat [simp]: fixes n :: nat shows "sin (x + n * (2 * pi)) = sin x" -proof (induct n arbitrary: x) - case (Suc n) - have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi" - unfolding Suc_eq_plus1 distrib_right - by (auto simp add: field_simps) - show ?case unfolding split_pi_off using Suc by auto -qed auto + by (metis (no_types, hide_lams) add.commute add.left_neutral cos_2npi cos_one_2pi_int mult.assoc mult.commute mult.left_neutral mult_zero_left sin_add sin_int_2pin) lemma sin_periodic_int [simp]: fixes i :: int shows "sin (x + i * (2 * pi)) = sin x" -proof(cases "0 \ i") - case True - thus ?thesis - using sin_periodic_nat[of x "nat i"] - by auto -next - case False hence i_nat: "i = - real (nat (-i))" by auto - have "sin x = sin (x + i * (2 * pi) - i * (2 * pi))" by auto - also have "\ = sin (x + i * (2 * pi))" - unfolding i_nat mult_minus_left diff_minus_eq_add by (rule sin_periodic_nat) - finally show ?thesis by auto -qed + by (metis add.right_neutral cos_int_2pin mult.commute mult.right_neutral mult_zero_right sin_add sin_int_2pin) lemma cos_periodic_nat [simp]: fixes n :: nat shows "cos (x + n * (2 * pi)) = cos x" -proof (induct n arbitrary: x) - case (Suc n) - have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi" - unfolding Suc_eq_plus1 distrib_right - by (auto simp add: field_simps) - show ?case unfolding split_pi_off using Suc by auto -qed auto + by (metis add.left_neutral cos_2npi cos_add cos_periodic mult.assoc mult_2 mult_2_right of_nat_numeral sin_periodic sin_periodic_nat) lemma cos_periodic_int [simp]: fixes i :: int shows "cos (x + i * (2 * pi)) = cos x" -proof(cases "0 \ i") - case True - thus ?thesis - using cos_periodic_nat[of x "nat i"] - by auto -next - case False hence i_nat: "i = - real (nat (-i))" by auto - have "cos x = cos (x + i * (2 * pi) - i * (2 * pi))" by auto - also have "\ = cos (x + i * (2 * pi))" - unfolding i_nat mult_minus_left diff_minus_eq_add by (rule cos_periodic_nat) - finally show ?thesis by auto -qed + by (metis cos_add cos_int_2pin diff_zero mult.commute mult.right_neutral mult_zero_right sin_int_2pin) text \Values of both sine and cosine are repeated only after multiples of $2\cdot \pi$\ @@ -337,14 +163,7 @@ lemma sin_cos_eq: fixes a b :: real assumes "cos a = cos b" and "sin a = sin b" shows "\ k::int. a - b = 2*k*pi" -proof- - from assms have "sin (a - b) = 0" "cos (a - b) = 1" - using sin_diff[of a b] cos_diff[of a b] - by auto - thus ?thesis - using cos1_sin0 - by auto -qed + by (metis assms cos_diff cos_one_2pi_int mult.commute sin_cos_squared_add3) text \The following two lemmas are consequences of surjectivity of cosine for the range $[-1, 1]$.\ @@ -377,12 +196,8 @@ lemma ex_cos_gt: assumes "a < 1" shows "\ \'. -pi/2 \ \' \ \' \ pi/2 \ \' \ \ \ cos (\ - \') > a" proof- - have "\ a'. a' \ 0 \ a' > a \ a' < 1" - using \a < 1\ - using divide_strict_right_mono[of "2*a + (1 - a)" 2 2] - by (rule_tac x="if a < 0 then 0 else a + (1-a)/2" in exI) (auto simp add: field_simps) - then obtain a' where "a' \ 0" "a' > a" "a' < 1" - by auto + obtain a' where "a' \ 0" "a' > a" "a' < 1" + by (metis assms(2) dense_le_bounded linear not_one_le_zero) thus ?thesis using ex_cos_eq[of \ a'] assms by auto diff --git a/thys/Complex_Geometry/Riemann_Sphere.thy b/thys/Complex_Geometry/Riemann_Sphere.thy index 42b7084cafb73d2e75c4421a615e917daf798c15..d770c0610254618ac07f71277df489d6aefc0bfe 100644 --- a/thys/Complex_Geometry/Riemann_Sphere.thy +++ b/thys/Complex_Geometry/Riemann_Sphere.thy @@ -183,7 +183,7 @@ proof transfer case False thus ?thesis using * ** inv_stereographic_on_sphere[of x "v1 / v2" y z] - by simp + by (simp add: norm_divide) qed moreover have "inv_stereographic_cvec_r3 v = inv_stereographic_cvec_r3 v'" diff --git a/thys/Complex_Geometry/Unitary11_Matrices.thy b/thys/Complex_Geometry/Unitary11_Matrices.thy index 89d18977302c3fd63008a2024221cbbe67025a2a..f1f0794b8a16bab493989dfb0b62d677bd29cf08 100644 --- a/thys/Complex_Geometry/Unitary11_Matrices.thy +++ b/thys/Complex_Geometry/Unitary11_Matrices.thy @@ -365,7 +365,7 @@ proof unfolding unitary11_def by (auto simp add: mat_adj_def mat_cnj_def) (simp add: field_simps) hence ***: "(cmod k)\<^sup>2 * ((cmod a)\<^sup>2 - (cmod b)\<^sup>2) = 1" - by (subst (asm) complex_mult_cnj_cmod, subst (asm) md, subst (asm) cor_mult[symmetric]) (metis of_real_1 of_real_eq_iff) + by (metis complex_mult_cnj_cmod md of_real_1 of_real_eq_iff of_real_mult) hence "((cmod a)\<^sup>2 - (cmod b)\<^sup>2) = 1 / (cmod k)\<^sup>2" by (cases "k=0") (auto simp add: field_simps) hence "cmod a ^ 2 = cmod b ^ 2 + 1 / cmod k ^ 2" diff --git a/thys/Complex_Geometry/Unitary_Matrices.thy b/thys/Complex_Geometry/Unitary_Matrices.thy index e3c1bc8df80fb8206b7a07950a82ed95d58a9d3c..1fc074a4663fb47725e02100d9c794e9bbca37b1 100644 --- a/thys/Complex_Geometry/Unitary_Matrices.thy +++ b/thys/Complex_Geometry/Unitary_Matrices.thy @@ -307,7 +307,7 @@ proof unfolding unitary_def by (auto simp add: mat_adj_def mat_cnj_def field_simps) hence "(cmod k)\<^sup>2 * ((cmod a)\<^sup>2 + (cmod b)\<^sup>2) = 1" - by (subst (asm) complex_mult_cnj_cmod, subst (asm) md, subst (asm) cor_mult[symmetric]) (metis of_real_1 of_real_eq_iff) + by (metis (mono_tags, lifting) complex_norm_square md of_real_1 of_real_eq_iff of_real_mult) thus ?rhs using * mat_eye_l apply (rule_tac x="a" in exI, rule_tac x="b" in exI, rule_tac x="k" in exI)