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 "b2 * m + c2 * n = a * (d2 + 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 "c2 = m2 + d2 - 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 "b2 = n2 + d2 + 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 "b2 * m + c2 * n = n * m2 + n2 * m + (m + n) * d2" by algebra
  also have " = (m + n) * (m * n + d2)" by algebra
  also from m + n = a have " = a * (d2 + 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 "b2 + c2 = 2 * (m2 + d2)"
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 "b2 * m + c2 * m = (2 * m) * (m2 + d2)"
    by (auto dest!: Stewart[where a="2 * m"] simp add: power2_eq_square)
  from this have "m * (b2 + c2) = m * (2 * (m2 + d2))"
    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