Theory Complex_Trigonometry

theory Complex_Trigonometry

imports  "HOL-Analysis.Convex"  Complex_Angles Complex_Triangles_Definitions

begin 

section ‹Complex trigonometry›
text ‹In this section we add some trigonometric results, especially the law of sines›
lemma ang_sin:
  shows‹Im ((b-a)*cnj(c-a)) = cmod (c-a) *cmod (b-a) * sin (angle_c c a b)›
proof -
  have f0:‹sin (Arg (cnj c - cnj a)) = - sin (Arg ( c - a))›
    by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff neg_0_equal_iff_equal sin_minus
        sin_pi)
  have f1:‹cos (Arg (cnj c - cnj a)) = cos (Arg (c - a))›
    by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff cos_minus)
  then have ‹b-a = cmod (b-a) * cis (Arg (b-a)) ∧ cnj (c-a) = cmod (c-a) * cis (Arg (cnj (c-a)))›
    using rcis_cmod_Arg rcis_def 
    by (metis complex_mod_cnj)
  then have ‹Im(cis (Arg (b-a)) * cis (Arg (cnj(c-a)))) = sin (angle_c c a b)›
    unfolding ang_vec_def angle_c_def using f1 f0 by(auto simp:cis.code sin_diff) 
  then have ‹Im (cmod (b-a) * cis (Arg (b-a)) * cmod (c-a) * cis (Arg (cnj (c-a)))) =
      cmod (c-a) *cmod (b-a) * sin (angle_c c a b) ›
    by (metis Im_complex_of_real[of "cmod (c - a)"] Im_complex_of_real[of "cmod (b - a)"]
        Im_mult_real[of "cor (cmod (c - a))"
          "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"]
        Im_mult_real[of "cor (cmod (b - a))" "cis (Arg (b - a)) * cis (Arg (cnj (c - a)))"]
        Re_complex_of_real[of "cmod (c - a)"] Re_complex_of_real[of "cmod (b - a)"]
        ab_semigroup_mult_class.mult_ac(1)[of "cor (cmod (b - a))" "cis (Arg (b - a))"
          "cis (Arg (cnj (c - a)))"]
        ab_semigroup_mult_class.mult_ac(1)[of "cis (Arg (cnj (c - a)))"
          "cor (cmod (b - a)) * cis (Arg (b - a))" "cor (cmod (c - a))"]
        ab_semigroup_mult_class.mult_ac(1)[of "cmod (c - a)" "cmod (b - a)"
          "Im (cis (Arg (b - a)) * cis (Arg (cnj (c - a))))"]
        mult.commute[of "cis (Arg (cnj (c - a)))" "cor (cmod (b - a)) * cis (Arg (b - a))"]
        mult.commute[of "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"
          "cor (cmod (c - a))"]
        mult.commute[of "cor (cmod (b - a)) * cis (Arg (b - a)) * cor (cmod (c - a))"
          "cis (Arg (cnj (c - a)))"])
  then show ‹Im ((b - a) * cnj (c - a)) = cmod (c - a) * cmod (b - a) * sin (angle_c c a b)› 
    by (metis ‹b - a = cor (cmod (b - a)) * cis (Arg (b - a)) ∧ cnj (c - a) = cor (cmod (c - a)) * cis (Arg (cnj (c - a)))› 
ab_semigroup_mult_class.mult_ac(1))
qed

lemma ang_cos:
  shows‹Re ((b-a)*cnj(c-a)) = cmod (c-a) *cmod (b-a) * cos (angle_c c a b)›
proof -
  have f0:‹sin (Arg (cnj c - cnj a)) = - sin (Arg ( c - a))›
    by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff neg_0_equal_iff_equal sin_minus
        sin_pi)
  have f1:‹cos (Arg (cnj c - cnj a)) = cos (Arg (c - a))›
    by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff cos_minus)
  then have f2:‹b-a = cmod (b-a) * cis (Arg (b-a)) ∧ cnj (c-a) = cmod (c-a) * cis (Arg (cnj (c-a)))›
    using rcis_cmod_Arg rcis_def 
    by (metis complex_mod_cnj)
  then have ‹Re(cis (Arg (b-a)) * cis (Arg (cnj(c-a)))) = cos (angle_c c a b)›
    unfolding ang_vec_def angle_c_def using f1 f0 by(auto simp:cis.code cos_diff) 
  then have ‹Re (cmod (b-a) * cmod (c-a)* cis (Arg (b-a))  * cis (Arg (cnj (c-a)))) =
      Re (cmod (c-a) *cmod (b-a)) * cos (angle_c c a b) ›
  proof -
    have f1: "cor (cmod (b - a) * cmod (c - a)) * cis (Arg (b - a)) * cis (Arg (cnj (c - a)))
 = cor (cmod (b - a) * cmod (c - a)) * (cis (Arg (b - a)) * cis (Arg (cnj (c - a))))"
      using ab_semigroup_mult_class.mult_ac(1) by blast
    have "cmod (b - a) * cmod (c - a) = cmod (c - a) * cmod (b - a)"
      by argo
    then show ?thesis
      using f1 Im_complex_of_real Re_mult_real ‹Re (cis (Arg (b - a)) * cis (Arg (cnj (c - a)))) 
          = cos (angle_c c a b)› by presburger
  qed
  then show ‹Re ((b-a)*cnj(c-a)) = cmod (c-a) *cmod (b-a) * cos (angle_c c a b)› 
    by (metis Re_complex_of_real f2 mult.assoc mult.commute of_real_mult)
   
qed

lemma law_of_cosines':
  assumes h:‹A≠C› ‹A≠B›
  shows "((cdist B C)⇧2 - (cdist A C)⇧2 - (cdist A B)⇧2 ) / (- 2*(cdist A C)*(cdist A B)) = (cos (∠ (C-A) (B-A)))"
  using law_of_cosines[of B C A] h by(auto simp:field_simps)

lemma law_of_cosines'':
  shows "(cdist A C)⇧2 = (cdist B C)⇧2 - (cdist A B)⇧2 + 2*(cdist A C)*(cdist A B)*(cos (∠ (C-A) (B-A)))"
  using law_of_cosines[of B C A]  by(auto simp:field_simps)

lemma law_of_cosines''':
  shows " (cdist A B)⇧2 = (cdist B C)⇧2 - (cdist A C)⇧2 + 2*(cdist A C)*(cdist A B)*(cos (∠ (C-A) (B-A)))"
  using law_of_cosines[of B C A]  by(auto simp:field_simps)


subsection ‹The law of sines›
theorem law_of_sines:
  assumes h1:‹b ≠ a› ‹a ≠ c› ‹b ≠ c›
  shows  "sin (angle_c a b c) * cdist b c = sin (angle_c c a b) * cdist a c" (is "?A = ?B") 
proof - 
  {fix a b c ::complex
    have f0:‹sin (Arg (cnj c - cnj a)) = - sin (Arg ( c - a))›
      by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff neg_0_equal_iff_equal sin_minus
          sin_pi)
    have f1:‹cos (Arg (cnj c - cnj a)) = cos (Arg (c - a))›
      by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff cos_minus)
    assume ‹b-a ≠ 0› ‹c-a ≠ 0 ›
    then have f2: ‹b-a = cmod (b-a) * cis (Arg (b-a)) ∧ cnj (c-a) = cmod (c-a) * cis (Arg (cnj (c-a)))›
      using rcis_cmod_Arg rcis_def 
      by (metis complex_mod_cnj)
    then have ‹Im(cis (Arg (b-a)) * cis (Arg (cnj(c-a)))) = sin (angle_c c a b)›
      unfolding ang_vec_def angle_c_def using f1 f0 by(auto simp:cis.code sin_diff) 
    then have ‹Im (cmod (b-a) * cis (Arg (b-a)) * cmod (c-a) * cis (Arg (cnj (c-a)))) =
      cmod (c-a) *cmod (b-a) * sin (angle_c c a b) ›
      by (metis Im_complex_of_real[of "cmod (c - a)"] Im_complex_of_real[of "cmod (b - a)"]
          Im_mult_real[of "cor (cmod (c - a))"
            "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"]
          Im_mult_real[of "cor (cmod (b - a))" "cis (Arg (b - a)) * cis (Arg (cnj (c - a)))"]
          Re_complex_of_real[of "cmod (c - a)"] Re_complex_of_real[of "cmod (b - a)"]
          ab_semigroup_mult_class.mult_ac(1)[of "cor (cmod (b - a))" "cis (Arg (b - a))"
            "cis (Arg (cnj (c - a)))"]
          ab_semigroup_mult_class.mult_ac(1)[of "cis (Arg (cnj (c - a)))"
            "cor (cmod (b - a)) * cis (Arg (b - a))" "cor (cmod (c - a))"]
          ab_semigroup_mult_class.mult_ac(1)[of "cmod (c - a)" "cmod (b - a)"
            "Im (cis (Arg (b - a)) * cis (Arg (cnj (c - a))))"]
          mult.commute[of "cis (Arg (cnj (c - a)))" "cor (cmod (b - a)) * cis (Arg (b - a))"]
          mult.commute[of "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"
            "cor (cmod (c - a))"]
          mult.commute[of "cor (cmod (b - a)) * cis (Arg (b - a)) * cor (cmod (c - a))"
            "cis (Arg (cnj (c - a)))"])
    then have ‹Im ((b-a)*cnj(c-a)) = cmod (c-a) *cmod (b-a) * sin (angle_c c a b)› 
      using ang_sin by presburger
  }note ang=this
  have i2:‹sin (angle_c c a b) = Im((b-a)*cnj(c-a))/ (cmod(b-a)*cmod(c-a))›
    using ang[of b a c] h1 by(auto)
  have ‹sin (angle_c a b c) = Im((c-b)*cnj(a-b)) / (cmod (c-b)*cmod (a-b))›
    using ang h1 by(auto)
  then have imp1:‹cmod (c-b) * sin (angle_c a b c) = Im((c-b)*cnj(a-b)) / (cmod (a-b)) ›
    by auto
  from i2 have imp2:‹cmod (c-a) * sin (angle_c c a b) = Im((b-a)*cnj(c-a))/ (cmod(b-a)) ›
    by auto
  show ?thesis using imp1 imp2 by(auto simp:field_simps norm_minus_commute) 
qed

lemma law_of_sines':  assumes h1:‹b ≠ a› ‹a ≠ c› ‹b ≠ c›
  shows "sin (angle_c a b c) * cdist b a = sin (angle_c b c a) * cdist a c"
proof - 
  {fix a b c ::complex
    have f0:‹sin (Arg (cnj c - cnj a)) = - sin (Arg ( c - a))›
      by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff neg_0_equal_iff_equal sin_minus
          sin_pi)
    have f1:‹cos (Arg (cnj c - cnj a)) = cos (Arg (c - a))›
      by (metis arg_cnj_not_pi arg_cnj_pi complex_cnj_diff cos_minus)
    assume ‹b-a ≠ 0› ‹c-a ≠ 0 ›
    then have f2:‹b-a = cmod (b-a) * cis (Arg (b-a)) ∧ cnj (c-a) = cmod (c-a) * cis (Arg (cnj (c-a)))›
      using rcis_cmod_Arg rcis_def 
      by (metis complex_mod_cnj)
    then have ‹Im(cis (Arg (b-a)) * cis (Arg (cnj(c-a)))) = sin (angle_c c a b)›
      unfolding ang_vec_def angle_c_def using f0 f1 by(auto simp:cis.code sin_diff) 
    then have ‹Im (cmod (b-a) * cis (Arg (b-a)) * cmod (c-a) * cis (Arg (cnj (c-a)))) =
      cmod (c-a) *cmod (b-a) * sin (angle_c c a b) ›
      by (metis Im_complex_of_real[of "cmod (c - a)"] Im_complex_of_real[of "cmod (b - a)"]
          Im_mult_real[of "cor (cmod (c - a))"
            "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"]
          Im_mult_real[of "cor (cmod (b - a))" "cis (Arg (b - a)) * cis (Arg (cnj (c - a)))"]
          Re_complex_of_real[of "cmod (c - a)"] Re_complex_of_real[of "cmod (b - a)"]
          ab_semigroup_mult_class.mult_ac(1)[of "cor (cmod (b - a))" "cis (Arg (b - a))"
            "cis (Arg (cnj (c - a)))"]
          ab_semigroup_mult_class.mult_ac(1)[of "cis (Arg (cnj (c - a)))"
            "cor (cmod (b - a)) * cis (Arg (b - a))" "cor (cmod (c - a))"]
          ab_semigroup_mult_class.mult_ac(1)[of "cmod (c - a)" "cmod (b - a)"
            "Im (cis (Arg (b - a)) * cis (Arg (cnj (c - a))))"]
          mult.commute[of "cis (Arg (cnj (c - a)))" "cor (cmod (b - a)) * cis (Arg (b - a))"]
          mult.commute[of "cis (Arg (cnj (c - a))) * (cor (cmod (b - a)) * cis (Arg (b - a)))"
            "cor (cmod (c - a))"]
          mult.commute[of "cor (cmod (b - a)) * cis (Arg (b - a)) * cor (cmod (c - a))"
            "cis (Arg (cnj (c - a)))"])
    then have ‹Im ((b-a)*cnj(c-a)) = cmod (c-a) *cmod (b-a) * sin (angle_c c a b)› 
      using ang_sin by presburger
  }note ang=this
  have i2:‹sin (angle_c b c a) = Im((a-c)*cnj(b - c))/ (cmod(b-c)*cmod(a-c))›
    using ang[of a c b] h1 by(auto)
  have ‹sin (angle_c a b c) = Im((c-b)*cnj(a-b)) / (cmod (c-b)*cmod (a-b))›
    using ang h1 by(auto)
  then have imp1:‹cmod (a-b) * sin (angle_c a b c) = Im((c-b)*cnj(a-b)) / (cmod (c-b)) ›
    by auto
  from i2 have imp2:‹cmod (a-c) * sin (angle_c b c a) = Im((a-c)*cnj(b-c))/ (cmod(b-c)) ›
    by auto
  show ?thesis using imp1 imp2 
    by (metis cdist_commute h1(1,2,3) law_of_sines)
qed


lemma ang_pos_pos:‹q≠p ⟹ p≠ r ⟹ r ≠ q ⟹ angle_c q r p ≥ 0 ⟹ angle_c r p q ≥0›
  using law_of_sines'[of r q p] 
  by (smt (verit) ang_vec_bounded angle_c_def cdist_def mult_neg_pos mult_nonneg_nonneg 
right_minus_eq sin_ge_zero sin_gt_zero sin_minus zero_less_norm_iff)

lemma cmod_pos:‹cmod a ≥ 0›
  by simp

lemma ang_neg_neg:‹q≠p ⟹ p≠ r ⟹ r ≠ q ⟹ angle_c q r p < 0 ⟹ angle_c r p q < 0›
proof -
  assume ‹q≠p› ‹p≠ r› ‹r ≠ q› ‹angle_c q r p < 0›
  then have ‹sin (angle_c q r p) < 0›
    using ang_c_in 
    by (metis ang_vec_def angle_c_def canon_ang(1) minus_less_iff neg_0_less_iff_less sin_gt_zero sin_minus)
  then have ‹sin (angle_c q r p) * cdist r q < 0›
    using ‹r ≠ q› mult_neg_pos by fastforce
  from law_of_sines'[of r q p] have  ‹sin (angle_c r p q)<0›
    by (metis ‹p ≠ r› ‹q ≠ p› ‹r ≠ q› ‹sin (angle_c q r p) * cdist r q < 0› 
        cdist_def linorder_not_less mult_less_0_iff norm_ge_zero)
  then show ?thesis
    using ang_c_in[of r p q] 
    by (metis ang_vec_def angle_c_def canon_ang(2) linorder_not_less sin_ge_zero) 
qed

lemma collinear_sin_neq_0:
  ‹¬collinear a2 b2 c2 ⟹ sin (angle_c a2 c2 b2) ≠ 0›
  unfolding collinear_def angle_c_def 
  by (metis Im_complex_div_eq_0 ang_sin angle_c_def collinear_def
 collinear_sym1 collinear_sym2' mult_eq_0_iff)


lemma collinear_sin_neq_pi:
  ‹¬collinear a2 b2 c2 ⟹ sin (angle_c a2 c2 b2) ≠ pi›
  unfolding collinear_def angle_c_def 
  by (metis add_cancel_right_left dual_order.antisym dual_order.trans le_add_same_cancel1 
linordered_nonzero_semiring_class.zero_le_one one_add_one one_neq_zero pi_ge_two sin_le_one)


lemma collinear_iff:
  assumes ‹a≠b ∧ b≠c ∧ c≠a› 
  shows ‹collinear a b c ⟷ (angle_c a b c = pi ∨ angle_c a b c = 0)›
  apply(rule iffI)
  using assms unfolding collinear_def using collinear_angle collinear_def apply(fastforce) 
  by (metis collinear_def collinear_sin_neq_0 collinear_sym1 sin_pi sin_zero)



definition ‹innerprod a b ≡ cnj a * b›


lemma left_lin_innerprod:‹innerprod (x + y) z = innerprod x z + innerprod y z›
  unfolding innerprod_def  
  by (simp add: mult.commute ring_class.ring_distribs(1))

lemma right_lin_innerprod:‹innerprod x (y+z) = innerprod x y + innerprod x z›
  unfolding innerprod_def 
  by (simp add: ring_class.ring_distribs(1))

lemma leftlin_innerprod:‹innerprod x (t*y) = t * innerprod x y›
  unfolding innerprod_def by(auto)

lemma rightsesqlin_innerprod:‹innerprod (t*x) (y) = cnj t * innerprod x y›
  unfolding innerprod_def by(auto)

lemma norm_eq_csqrt_inner:‹norm x = csqrt (innerprod x x)›
  using complex_mod_sqrt_Re_mult_cnj innerprod_def by force

lemma abs2_eq_inner:‹abs (innerprod x y)^2 = innerprod x y * cnj (innerprod x y)›
  unfolding innerprod_def abs_complex_def apply(rule complex_eqI)
  by (metis comp_apply complex_mult_cnj_cmod of_real_power)+

lemma complex_add_inner_cnj:‹t*innerprod x y + cnj (t*innerprod x y) = 2* Re (t*innerprod x y)›
  using complex_add_cnj by blast

lemma Re_innerprod_inner:‹Re (innerprod (a-b) (c-b)) = (a-b)∙(c-b)›
  unfolding innerprod_def inner_complex_def by(auto simp:field_simps) 

lemma angle_c_arccos_pos: 
  assumes h:‹a≠b ∧ b≠ c› ‹angle_c a b c ≥ 0›
  shows ‹angle_c a b c = arccos ((Re (innerprod (a-b) (c - b)))/(cmod(a-b)*cmod(c-b)))›
proof - 
  have ‹Re ((a-b)*cnj(c-b)) = (Re (innerprod (a-b) (c - b)))›
    unfolding innerprod_def by(auto simp:field_simps) 
  then have ‹((Re (innerprod (a-b) (c - b)))/(cmod(a-b)*cmod(c-b))) = cos (angle_c a b c)›
    by (metis (no_types, lifting) ang_cos angle_c_commute cos_minus divisors_zero
 h(1) mult.commute nonzero_mult_div_cancel_left norm_eq_zero right_minus_eq)
  then show ?thesis 
    using ang_vec_bounded angle_c_def arccos_cos h(2) by presburger
qed


lemma angle_c_arccos_neg: 
  assumes h:‹a≠b ∧ b≠ c› ‹angle_c a b c ≤ 0 ›
  shows ‹- angle_c a b c = arccos ((Re (innerprod (a-b) (c - b)))/(cmod(a-b)*cmod(c-b)))›
proof - 
  have ‹Re ((a-b)*cnj(c-b)) = (Re (innerprod (a-b) (c - b)))›
    unfolding innerprod_def by(auto simp:field_simps) 
  then have ‹((Re (innerprod (a-b) (c - b)))/(cmod(a-b)*cmod(c-b))) = cos (angle_c a b c)›
    by (metis (no_types, lifting) ang_cos angle_c_commute cos_minus divisors_zero
 h(1) mult.commute nonzero_mult_div_cancel_left norm_eq_zero right_minus_eq)
  then show ?thesis 
    using ang_vec_bounded angle_c_def arccos_cos h(2) 
    by (metis arccos_cos2 less_le_not_le)
qed

end