Theory Complex_Axial_Symmetry

theory Complex_Axial_Symmetry

imports Complex_Angles Complex_Triangles

begin
section ‹Axial symmetry in complex field›

text ‹In the following we define the axial symmetry and prove basics properties.›
context
  fixes z1 z2 :: complex and α β :: complex
  assumes neq0:‹z1≠z2›
  defines ‹α ≡ (z1-z2)/(cnj z1 - cnj z2)›
  defines ‹β  ≡ (z2*cnj z1 - z1*cnj z2)/(cnj z1 - cnj z2)›
begin

definition axial_symmetry::‹complex ⇒ complex› where
  ‹axial_symmetry z ≡ cnj z*(z1 - z2)/(cnj z1 - cnj z2) + (z2*cnj z1 - z1*cnj z2)/(cnj z1 - cnj z2)›

lemma norm_α_eq_1:‹cmod (α) = 1›
  by (auto simp: neq0 α_def β_def)

lemma z1_inv:‹axial_symmetry z1 = z1›
  unfolding axial_symmetry_def 
  by (metis (mono_tags, lifting) add_diff_eq add_divide_distrib complex_cnj_cancel_iff 
      diff_add_cancel eq_iff_diff_eq_0 mult.commute neq0 nonzero_eq_divide_eq right_diff_distrib') 

lemma z2_inv:‹axial_symmetry z2 = z2›
  unfolding axial_symmetry_def 
  by (smt (z3) add_diff_cancel_left add_diff_cancel_left' add_divide_distrib axial_symmetry_def 
      complex_cnj_cancel_iff diff_add_cancel divide_divide_eq_right eq_divide_imp mult_commute_abs right_minus_eq z1_inv)

lemma cmod_axial:‹cmod (axial_symmetry z - axial_symmetry z') = cmod (α*(cnj z - cnj z'))›
  unfolding axial_symmetry_def 
  by (auto simp: α_def β_def) (simp add: diff_divide_distrib mult.commute right_diff_distrib')

lemma cmod_axial_inv:‹cmod (axial_symmetry z - axial_symmetry z') = cmod (z - z')›
  by (metis cmod_axial complex_cnj_diff complex_mod_cnj mult.commute 
      mult.right_neutral norm_α_eq_1 norm_mult)

lemma axial_symmetry_dist1:‹cdist z1 z = cdist z1 (axial_symmetry z)›
  by (metis cdist_def cmod_axial_inv z1_inv)

lemma axial_symmetry_dist2:‹cdist z2 z = dist z2 (axial_symmetry z)›
  by (metis cdist_def cmod_axial_inv dist_commute dist_norm z2_inv)

lemma αβ: ‹α*cnj β + β = 0›
  by (simp add: add_divide_eq_iff  α_def β_def)

lemma involution_symmetry:‹axial_symmetry (axial_symmetry z) = z›
proof -
  have ‹α*cnj(α*cnj z + β) + β = α*cnj α*z + α*cnj β +β›
    by (simp add: ring_class.ring_distribs(1))
  then show ?thesis unfolding axial_symmetry_def
    by (smt (verit, best) αβ add.right_neutral cmod_eq_one group_cancel.add1 
        mult.commute mult_cancel_right2 norm_α_eq_1 times_divide_eq_left α_def β_def)
qed

lemma arg_α:‹Arg α = ⇂2*Arg (z1-z2)⇃›
  unfolding α_def β_def
  by (smt (verit, del_insts) arg_cnj_not_pi arg_div arg_pi_iff canon_ang_id canon_ang_pi_3pi 
      complex_cnj_cancel_iff complex_cnj_diff eq_cnj_iff_real eq_iff_diff_eq_0 neq0 pi_ge_two)

lemma Arg_invol:‹Arg (axial_symmetry (axial_symmetry z)) =  Arg z›
  by (simp add: involution_symmetry)


lemma angle_sum_symmetry:‹z≠z1 ⟹ ⇂angle_c z z1 z2 + angle_c z2 z1 (axial_symmetry z)⇃ = angle_c z z1 (axial_symmetry z)›
proof -
  assume ‹z≠z1›
  have ‹z2-z1 ≠ 0› using angle_c_sum neq0 by auto
  have ‹z1 - (axial_symmetry z) ≠ 0› 
    by (metis ‹z ≠ z1› eq_iff_diff_eq_0 involution_symmetry z1_inv)
  then show ?thesis
    using angle_c_sum 
    by (metis ‹z2 - z1 ≠ 0› right_minus_eq z1_inv)
qed

lemma angle_symmetry_eq_imp:
  assumes h:‹z1≠z› ‹z2≠z›
  shows‹angle_c z z1 z2 = - angle_c (axial_symmetry z) z1 z2 ∨ angle_c z z1 z2 = angle_c (axial_symmetry z) z1 z2›
  by (metis (mono_tags, lifting) axial_symmetry_dist1 cdist_def cmod_axial_inv
            congruent_ctriangle_sss(22) h(1) neq0 z2_inv)

lemma angle_symmetry:
  assumes h:‹z1≠z› ‹z2≠z›
    and ‹angle_c z z1 z2 = angle_c (axial_symmetry z) z1 z2›
  shows ‹z = axial_symmetry z›
proof -
  have ‹cmod (z - z1) = cmod (axial_symmetry z - z1)›
    using axial_symmetry_dist1 by auto
  have ‹cmod (z - z2) = cmod (axial_symmetry z - z2)›
    by (metis axial_symmetry_dist2 cdist_def dist_commute dist_complex_def)
  have ‹z-z1 = axial_symmetry z-z1›
    by (metis ‹cmod (z - z1) = cmod (local.axial_symmetry z - z1)› ang_cos ang_sin assms(3) 
        complex_cnj_cnj complex_eq_iff eq_iff_diff_eq_0 mult_cancel_left neq0)
  then show ?thesis 
    by simp
qed

lemma line_is_inv:‹z∈ line z1 z2 ∧ z≠z2 ∧ z≠z1 ⟹ z = axial_symmetry z›
proof -
  assume ‹z∈ line z1 z2 ∧ z≠z2 ∧ z≠z1›
  then have ‹angle_c z z1 z2 = 0 ∨ angle_c z z1 z2 = pi›
    unfolding line_def using neq0 collinear_angle
    using collinear_sym1 collinear_sym2' by blast
  then show ?thesis 
    by (smt (verit) ‹z ∈ line z1 z2 ∧ z ≠ z2 ∧ z ≠ z1› 
        angle_c_commute angle_c_commute_pi angle_symmetry angle_symmetry_eq_imp)
qed

lemma dist_inv:‹cdist a b = cdist (axial_symmetry a) (axial_symmetry b)›
  by (simp add: cmod_axial_inv)

lemma collinear_inv: assumes ‹collinear a b c› and ‹a ≠ b∧ b ≠ c ∧ c≠a› 
  shows ‹collinear (axial_symmetry a) (axial_symmetry b) (axial_symmetry c)›
proof -
  have ‹angle_c a b c = pi ∨ angle_c a b c = 0›
    using assms(1) assms(2) collinear_angle by blast
  then have ‹angle_c (axial_symmetry a) (axial_symmetry b) (axial_symmetry c) = angle_c a b c 
          ∨ angle_c (axial_symmetry a) (axial_symmetry b) (axial_symmetry c) = - angle_c a b c›
    by (metis congruent_ctriangle_sss(24) assms(2) dist_inv minus_equation_iff)
  then show ?thesis 
    using ‹angle_c a b c = pi ∨ angle_c a b c = 0› collinear_sin_neq_0 collinear_sym1 by fastforce
qed

lemma axial_symmetry_eq_line:‹z≠z1 ∧ z≠z2 ⟹ z = axial_symmetry z ⟹ z ∈ line z1 z2›
proof -
  assume ‹z≠z1 ∧ z≠z2› ‹z = axial_symmetry z›
  then have g0:‹z = α*cnj z + β› unfolding axial_symmetry_def 
    by (simp add: mult.commute α_def β_def)
  then have g1:‹cnj z = (z-β)*cnj α ›
    by (smt (verit, ccfv_threshold) add_diff_cancel complex_cnj_cnj complex_cnj_diff α_def β_def
        complex_cnj_divide mult.commute neq0 nonzero_eq_divide_eq right_minus_eq times_divide_eq_left)
  also have g2:‹z = (cnj z - cnj β)*α›
    by (metis calculation complex_cnj_cnj complex_cnj_diff complex_cnj_mult)
  have ‹α/(z1-z2) = 1 /(cnj z1 - cnj z2)›
    by (auto simp: α_def β_def)
  have ‹Im w = (w-cnj w)/(2*𝗂)› for w
    using Im_express_cnj by blast
  then have ‹Im (z2*cnj z1) = (z2*cnj z1 - cnj (z2*cnj z1))/(2*𝗂)›
    by presburger
  then have ‹Im (z2*cnj z1)*2*𝗂 = (z2*cnj z1 - cnj z2* z1)›
    by (metis complex_cnj_cnj complex_cnj_mult complex_diff_cnj mult.commute)
  have f0:‹(cnj z1 - cnj z2)*(z1-z2) = cmod z1^2 + cmod z2^2 - cnj z1 * z2 - cnj z2 * z1›
    by (smt (verit) cancel_ab_semigroup_add_class.diff_right_commute complex_mult_cnj_cmod 
        diff_diff_eq2 left_diff_distrib mult.assoc mult.commute norm_minus_commute norm_mult of_real_add of_real_eq_iff)
  have f1:‹cmod z1^2 + cmod z2^2 - cnj z1 * z2 - cnj z2 * z1 = cmod z1^2 + cmod z2^2 - 2*Re z1*Re z2 - 2*Im z1*Im z2›
    by(auto simp:field_simps intro:complex_eqI) 
  have ‹β = 2*𝗂*Im (z2*cnj z1) / (cnj z1-cnj z2)›
    using ‹cor (Im (z2 * cnj z1)) = (z2 * cnj z1 - cnj (z2 * cnj z1)) / (2 * 𝗂)›
    unfolding α_def β_def by auto
  then have f2:‹β/(z1-z2) = 2*𝗂*Im (z2*cnj z1) / ((cnj z1-cnj z2)*(z1-z2))›
    by simp
  then have ‹β/(z1-z2) = 2*𝗂*Im (z2*cnj z1) /(cmod z1^2 + cmod z2^2 - 2*Re z1*Re z2 - 2*Im z1*Im z2)›
    using f0 f1 by presburger
  then have ‹is_real ((z - z1)/(z1-z2))›
    unfolding axial_symmetry_def using g2 
    by (smt (verit, del_insts) add_diff_cancel_right axial_symmetry_def complex_cnj_cnj
        complex_cnj_diff complex_cnj_divide diff_divide_distrib divide_divide_eq_right eq_cnj_iff_real
        g0 g2 mult.commute times_divide_eq_right z1_inv z2_inv α_def β_def)
  then show ‹z ∈ line z1 z2› 
    unfolding line_def collinear_def 
    by (metis (mono_tags, lifting) Im_i_times Re_i_times cnj.simps(2) complex_i_mult_minus 
        eq_cnj_iff_real mem_Collect_eq minus_diff_eq minus_divide_right)
qed  

lemma angle_symmetry_eq:
  assumes h:‹z1≠z› ‹z2≠z› ‹z∉line z1 z2›
  shows‹angle_c z z1 z2 = - angle_c (axial_symmetry z) z1 z2›
proof -
  have f0:‹angle_c z z1 z2 = - angle_c (axial_symmetry z) z1 z2 ∨
           angle_c z z1 z2 = angle_c (axial_symmetry z) z1 z2›
    using angle_symmetry_eq_imp h(1) h(2) by blast
  have f1:‹angle_c z z2 z1 = - angle_c (axial_symmetry z) z2 z1 
          ∨ angle_c z z2 z1 = angle_c (axial_symmetry z) z2 z1›
    by (metis axial_symmetry_dist1 congruent_ctriangle_sss(24) dist_inv h(1) neq0 z2_inv)
  show ?thesis 
    using angle_symmetry axial_symmetry_eq_line f0 h(1) h(2) h(3) by presburger
qed

end
end