(* 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