Theory Stewart_Apollonius

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

section ‹Stewart's Theorem and Apollonius' Theorem›

theory Stewart_Apollonius
imports
  Triangle.Triangle
begin

subsection ‹Stewart's Theorem›

theorem Stewart:
  fixes A B C D :: "'a::euclidean_space"
  assumes "between (B, C) D"
  assumes "a = dist B C"
  assumes "b = dist A C"
  assumes "c = dist B A"
  assumes "d = dist A D"
  assumes "m = dist B D"
  assumes "n = dist C D"
  shows "b⇧2 * m + c⇧2 * n = a * (d⇧2 + m * n)"
proof (cases)
  assume "B ≠ D ∧ C ≠ D"
  let ?θ = "angle B D A"
  let ?θ' = "angle A D C"
  from ‹B ≠ D ∧ C ≠ D› ‹between _ _› have cos: "cos ?θ' = - cos ?θ"
    by (auto simp add: angle_inverse[of B C D] angle_commute[of A D C])
  from ‹between _ _› have "m + n = a"
    unfolding ‹a = _› ‹m = _› ‹n = _›
    by (metis (no_types) between dist_commute)
  have "c⇧2 = m⇧2 + d⇧2 - 2 * d * m * cos ?θ"
    unfolding ‹c = _› ‹m = _› ‹d = _›
    by (simp add: cosine_law_triangle[of B A D] dist_commute[of D A] dist_commute[of D B])
  moreover have "b⇧2 = n⇧2 + d⇧2 + 2 * d * n * cos ?θ"
    unfolding ‹b = _› ‹n = _› ‹d = _›
    by (simp add: cosine_law_triangle[of A C D] cos dist_commute[of D A] dist_commute[of D C])
  ultimately have "b⇧2 * m + c⇧2 * n = n * m⇧2 + n⇧2 * m + (m + n) * d⇧2" by algebra
  also have "… = (m + n) * (m * n + d⇧2)" by algebra
  also from ‹m + n = a› have "… = a * (d⇧2 + m * n)" by simp
  finally show ?thesis .
next
  assume "¬ (B ≠ D ∧ C ≠ D)"
  from this assms show ?thesis by (auto simp add: dist_commute)
qed

text ‹
Here is an equivalent formulation that is probably more suitable for further use
in other geometry theories in Isabelle.
›

theorem Stewart':
  fixes A B C D :: "'a::euclidean_space"
  assumes "between (B, C) D"
  shows "(dist A C)⇧2 * dist B D + (dist B A)⇧2 * dist C D = dist B C * ((dist A D)⇧2 + dist B D * dist C D)"
using assms by (auto intro: Stewart)

subsection ‹Apollonius' Theorem›

text ‹
Apollonius' theorem is a simple specialisation of Stewart's theorem,
but historically predated Stewart's theorem by many centuries.
›

lemma Apollonius:
  fixes A B C :: "'a::euclidean_space"
  assumes "B ≠ C"
  assumes "b = dist A C"
  assumes "c = dist B A"
  assumes "d = dist A (midpoint B C)"
  assumes "m = dist B (midpoint B C)"
  shows "b⇧2 + c⇧2 = 2 * (m⇧2 + d⇧2)"
proof -
  from ‹B ≠ C› have "m ≠ 0"
    unfolding ‹m = _› using midpoint_eq_endpoint(1) by fastforce
  have "between (B, C) (midpoint B C)"
    by (simp add: between_midpoint)
  moreover have "dist C (midpoint B C) = dist B (midpoint B C)"
    by (simp add: dist_midpoint)
  moreover have "dist B C = 2 * dist B (midpoint B C)"
    by (simp add: dist_midpoint)
  moreover note assms(2-5)
  ultimately have "b⇧2 * m + c⇧2 * m = (2 * m) * (m⇧2 + d⇧2)"
    by (auto dest!: Stewart[where a="2 * m"] simp add: power2_eq_square)
  from this have "m * (b⇧2 + c⇧2) = m * (2 * (m⇧2 + d⇧2))"
    by (simp add: distrib_left semiring_normalization_rules(7))
  from this ‹m ≠ 0› show ?thesis by auto
qed

text ‹
Here is the equivalent formulation that is probably more suitable for further use
in other geometry theories in Isabelle.
›

lemma Apollonius':
  fixes A B C :: "'a::euclidean_space"
  assumes "B ≠ C"
  shows "(dist A C)⇧2 + (dist B A)⇧2 = 2 * ((dist B (midpoint B C))⇧2 + (dist A (midpoint B C))⇧2)"
using assms by (rule Apollonius) auto

end