# 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)"
moreover have "dist C (midpoint B C) = dist B (midpoint B C)"
moreover have "dist B C = 2 * dist B (midpoint B C)"
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))"
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
```