Theory Chord_Segments

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Intersecting Chord Theorem›

theory Chord_Segments
imports Triangle.Triangle
begin

subsection ‹Preliminaries›

lemma betweenE_if_dist_leq:
  fixes A B X :: "'a::euclidean_space"
  assumes "between (A, B) X"
  assumes "dist A X ≤ dist B X"
  obtains u where "1 / 2 ≤ u" "u ≤ 1" and "X = u *R A + (1 - u) *R B"
proof (cases "A = B")
  assume "A ≠ B"
  from ‹between (A, B) X› obtain u where u: "u ≥ 0" "u ≤ 1" and X: "X = u *R A + (1 - u) *R B"
    by (metis add.commute betweenE between_commute)
  from X have "X = B + u *R (A - B)" and "X = A + (u - 1) *R (A - B)"
    by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib)+
  from ‹X = B + u *R (A - B)› have dist_B: "dist B X = norm (u *R (A - B))"
    by (auto simp add: dist_norm)
  from ‹X = A + (u - 1) *R (A - B)› have dist_A: "dist A X = norm ((u - 1) *R (A - B))"
    by (auto simp add: dist_norm)
  from ‹A ≠ B› have "norm (A - B) > 0" by auto
  from this ‹dist A X ≤ dist B X› have "u ≥ 1 / 2"
    using dist_A dist_B by simp
  from this ‹u ≤ 1› X that show thesis by blast
next
  assume "A = B"
  define u :: real where "u = 1"
  from ‹between (A, B) X› ‹A = B› have "1 / 2 ≤ u" "u ≤ 1" "X = u *R A + (1 - u) *R B"
    unfolding u_def by auto
  with that show thesis by blast
qed

lemma dist_geq_iff_midpoint_in_between:
  fixes A B X :: "'a::euclidean_space"
  assumes "between (A, B) X"
  shows "dist A X ≤ dist B X ⟷ between (X, B) (midpoint A B)"
proof
  assume "dist A X ≤ dist B X"
  from ‹between (A, B) X› this obtain u
    where u: "1 / 2 ≤ u" "u ≤ 1" and X: "X = u *R A + (1 - u) *R B"
    using betweenE_if_dist_leq by blast
  have M: "midpoint A B = (1 / 2) *R A + (1 / 2) *R B"
    unfolding midpoint_def by (simp add: scaleR_add_right)
  from ‹1 / 2 ≤ u› have 1: "midpoint A B = (1 / (2 * u)) *R X + (1 - (1 / (2 * u))) *R B"
  proof -
    have "(2 - u * 2) / (2 * u) = 1 / u - u / u"
      using u(1) by (simp add: diff_divide_distrib)
    also have "… = 1 / u - 1" using u(1) by auto
    finally have "(2 - u * 2) / (2 * u) = 1 / u - 1" .
    from ‹1 / 2 ≤ u› this show ?thesis
      using X M by (simp add: scaleR_add_right scaleR_add_left[symmetric])
  qed
  moreover from u have 2: "(1 / (2 * u)) ≥ 0" "(1 / (2 * u)) ≤ 1" by auto
  ultimately show "between (X, B) (midpoint A B)"
    using betweenI [of concl: B X]  by (metis add.commute between_commute)
next
  assume "between (X, B) (midpoint A B)"
  then have "between (A, midpoint A B) X"
    using ‹between (A, B) X› between_midpoint(1) between_swap by blast
  then have "dist A X ≤ dist A (midpoint A B)"
    using between zero_le_dist by force
  also have "dist A (midpoint A B) ≤ dist B (midpoint A B)"
    by (simp add: dist_midpoint)
  also from ‹between (X, B) (midpoint A B)› have "dist B (midpoint A B) ≤ dist B X"
    using between zero_le_dist by (metis add.commute dist_commute le_add_same_cancel1)
  finally show "dist A X ≤ dist B X" .
qed

subsection ‹Properties of Chord Segments›

lemma chord_property:
  fixes S C :: "'a :: euclidean_space"
  assumes "dist C S = dist C T"
  assumes "between (S, T) X"
  shows "dist S X * dist X T = (dist C S) ^ 2 - (dist C X) ^ 2"
proof -
  define M where "M = midpoint S T"
  have "between (S, T) M"
    unfolding M_def by (simp add: between_midpoint(1))
  have "dist T M = dist S M"
    unfolding M_def by (simp add: dist_midpoint)

  have distances: "max (dist S X) (dist X T) = (dist S M) + (dist X M) ∧
    min (dist S X) (dist X T) = (dist S M) - (dist X M)"
  proof cases
    assume "dist S X ≤ dist X T"
    then have "between (X, T) M"
      using ‹between (S, T) X› M_def
      by (simp add: dist_geq_iff_midpoint_in_between dist_commute)
    then have "between (S, M) X"
      using ‹between (S, T) X› ‹between (S, T) M› between_swap by blast
    from ‹between (X, T) M› have "dist X T = dist X M + dist M T"
      using between by auto
    moreover from ‹between (S, M) X› have "dist S X = dist S M - dist M X"
      using between dist_commute by force
    ultimately show ?thesis
      using ‹dist S X ≤ dist X T› ‹dist T M = dist S M›
      by (simp add: add.commute dist_commute max_def min_def)
  next
    assume "¬ (dist S X ≤ dist X T)"
    then have "dist T X ≤ dist S X" by (simp add: dist_commute)
    then have "between (S, X) M"
      using ‹between (S, T) X› M_def
      by (simp add: dist_geq_iff_midpoint_in_between midpoint_sym between_commute)
    then have "between (T, M) X"
      using ‹between (S, T) X› ‹between (S, T) M› between_swap between_commute by metis
    from ‹between (S, X) M› have "dist S X = dist S M + dist M X"
      using between by auto
    moreover from ‹between (T, M) X› have "dist T X = dist T M - dist M X"
      using between dist_commute by force
    ultimately show ?thesis
      using ‹¬ dist S X ≤ dist X T› ‹dist T M = dist S M›
      by (metis dist_commute max_def min_def)
  qed

  have "orthogonal (C - M) (S - M)"
    using ‹dist C S = dist C T› M_def
    by (auto simp add: isosceles_triangle_orthogonal_on_midpoint)
  have "orthogonal (C - M) (X - M)"
  proof -
    have "between (S, T) M"
      using M_def between_midpoint(1) by blast
    obtain c where "(X - M) = c *R (S - M)"
    proof (cases "S = M")
      assume "S ≠ M"
      then obtain c where "(X - M) = c *R (S - M)"
        using between_implies_scaled_diff [OF ‹between (S, T) X› ‹between (S, T) M›] by metis
      from this that show thesis by blast
    next
      assume "S = M"
      from this ‹between (S, T) X› have "X = M"
        by (simp add: midpoint_between M_def)
      from ‹X = M› ‹S = M› have "(X - M) = 0 *R (S - M)" by simp
      from this that show thesis by blast
    qed
    from this ‹orthogonal (C - M) (S - M)› show ?thesis
      by (auto intro: orthogonal_clauses(2))
  qed
  from ‹orthogonal (C - M) (S - M)› ‹orthogonal (C - M) (X - M)› have
    "(dist S M) ^ 2 + (dist M C) ^ 2 = (dist C S) ^ 2"
    "(dist X M) ^ 2 + (dist M C) ^ 2 = (dist C X) ^ 2"
    by (auto simp only: Pythagoras)
  then have geometric_observation:
    "(dist S M) ^ 2 = (dist C S) ^ 2 - (dist M C) ^ 2"
    "(dist X M) ^ 2 = (dist C X) ^ 2 - (dist M C) ^ 2"
    by auto

  have "dist S X * dist X T = max (dist S X) (dist X T) * min (dist S X) (dist X T)"
    by (auto split: split_max)
  also have "… = ((dist S M) + (dist X M)) * ((dist S M) - (dist X M))"
    using distances by simp
  also have "… = (dist S M) ^ 2 - (dist X M) ^ 2"
    by (simp add: field_simps power2_eq_square)
  also have "… = ((dist C S) ^ 2 - (dist M C) ^ 2) - ((dist C X) ^ 2 - (dist M C) ^ 2)"
    using geometric_observation by simp
  also have "… = (dist C S) ^ 2 - (dist C X) ^ 2" by simp
  finally show ?thesis .
qed

theorem product_of_chord_segments:
  fixes S1 T1 S2 T2 X C :: "'a :: euclidean_space"
  assumes "between (S1, T1) X" "between (S2, T2) X"
  assumes "dist C S1 = r" "dist C T1 = r"
  assumes "dist C S2 = r" "dist C T2 = r"
  shows "dist S1 X * dist X T1 = dist S2 X * dist X T2"
proof -
  from ‹dist C S1 = r› ‹dist C T1 = r› ‹between (S1, T1) X›
  have "dist S1 X * dist X T1 = r ^ 2 - (dist C X) ^ 2"
    by (subst chord_property) auto
  also from ‹dist C S2 = r› ‹dist C T2 = r› ‹between (S2, T2) X›
  have "… = dist S2 X * dist X T2"
    by (subst chord_property) auto
  finally show ?thesis .
qed

end