Theory Angles
section ‹Definition of angles›
theory Angles
imports
"HOL-Analysis.Multivariate_Analysis"
begin
lemma collinear_translate_iff: "collinear (((+) a) ` A) ⟷ collinear A"
by (auto simp: collinear_def)
definition vangle where
"vangle u v = (if u = 0 ∨ v = 0 then pi / 2 else arccos (u ∙ v / (norm u * norm v)))"
definition angle where
"angle a b c = vangle (a - b) (c - b)"
lemma angle_altdef: "angle a b c = arccos ((a - b) ∙ (c - b) / (dist a b * dist c b))"
by (simp add: angle_def vangle_def dist_norm)
lemma vangle_0_left [simp]: "vangle 0 v = pi / 2"
and vangle_0_right [simp]: "vangle u 0 = pi / 2"
by (simp_all add: vangle_def)
lemma vangle_refl [simp]: "u ≠ 0 ⟹ vangle u u = 0"
by (simp add: vangle_def dot_square_norm power2_eq_square)
lemma angle_refl [simp]: "angle a a b = pi / 2" "angle a b b = pi / 2"
by (simp_all add: angle_def)
lemma angle_refl_mid [simp]: "a ≠ b ⟹ angle a b a = 0"
by (simp add: angle_def)
lemma cos_vangle: "cos (vangle u v) = u ∙ v / (norm u * norm v)"
unfolding vangle_def using Cauchy_Schwarz_ineq2[of u v] by (auto simp: field_simps)
lemma cos_angle: "cos (angle a b c) = (a - b) ∙ (c - b) / (dist a b * dist c b)"
by (simp add: angle_def cos_vangle dist_norm)
lemma inner_conv_angle: "(a - b) ∙ (c - b) = dist a b * dist c b * cos (angle a b c)"
by (simp add: cos_angle)
lemma vangle_commute: "vangle u v = vangle v u"
by (simp add: vangle_def inner_commute mult.commute)
lemma angle_commute: "angle a b c = angle c b a"
by (simp add: angle_def vangle_commute)
lemma vangle_nonneg: "vangle u v ≥ 0" and vangle_le_pi: "vangle u v ≤ pi"
using Cauchy_Schwarz_ineq2[of u v]
by (auto simp: vangle_def field_simps intro!: arccos_lbound arccos_ubound)
lemmas vangle_bounds = vangle_nonneg vangle_le_pi
lemma angle_nonneg: "angle a b c ≥ 0" and angle_le_pi: "angle a b c ≤ pi"
using vangle_bounds unfolding angle_def by blast+
lemmas angle_bounds = angle_nonneg angle_le_pi
lemma sin_vangle_nonneg: "sin (vangle u v) ≥ 0"
using vangle_bounds by (rule sin_ge_zero)
lemma sin_angle_nonneg: "sin (angle a b c) ≥ 0"
using angle_bounds by (rule sin_ge_zero)
lemma vangle_eq_0D:
assumes "vangle u v = 0"
shows "norm u *⇩R v = norm v *⇩R u"
proof -
from assms have "u ∙ v = norm u * norm v"
using arccos_eq_iff[of "(u ∙ v) / (norm u * norm v)" 1] Cauchy_Schwarz_ineq2[of u v]
by (fastforce simp: vangle_def split: if_split_asm)
thus ?thesis by (subst (asm) norm_cauchy_schwarz_eq) simp_all
qed
lemma vangle_eq_piD:
assumes "vangle u v = pi"
shows "norm u *⇩R v + norm v *⇩R u = 0"
proof -
from assms have "(-u) ∙ v = norm (-u) * norm v"
using arccos_eq_iff[of "(u ∙ v) / (norm u * norm v)" "-1"] Cauchy_Schwarz_ineq2[of u v]
by (simp add: field_simps vangle_def split: if_split_asm)
thus ?thesis by (subst (asm) norm_cauchy_schwarz_eq) simp_all
qed
lemma dist_triangle_eq:
fixes a b c :: "'a :: real_inner"
shows "(dist a c = dist a b + dist b c) ⟷ dist a b *⇩R (c - b) + dist b c *⇩R (a - b) = 0"
using norm_triangle_eq[of "b - a" "c - b"]
by (simp add: dist_norm norm_minus_commute algebra_simps)
lemma angle_eq_pi_imp_dist_additive:
assumes "angle a b c = pi"
shows "dist a c = dist a b + dist b c"
using vangle_eq_piD[OF assms[unfolded angle_def]]
by (subst dist_triangle_eq) (simp add: dist_norm norm_minus_commute)
lemma orthogonal_iff_vangle: "orthogonal u v ⟷ vangle u v = pi / 2"
using arccos_eq_iff[of "u ∙ v / (norm u * norm v)" 0] Cauchy_Schwarz_ineq2[of u v]
by (auto simp: vangle_def orthogonal_def)
lemma cos_minus1_imp_pi:
assumes "cos x = -1" "x ≥ 0" "x < 3 * pi"
shows "x = pi"
proof -
have "cos (x - pi) = 1" by (simp add: assms)
then obtain n :: int where n: "of_int n = (x / pi - 1) / 2"
by (subst (asm) cos_one_2pi_int) (auto simp: field_simps)
also from assms have "… ∈ {-1<..<1}" by (auto simp: field_simps)
finally have "n = 0" by simp
with n show ?thesis by simp
qed
lemma vangle_eqI:
assumes "u ≠ 0" "v ≠ 0" "w ≠ 0" "x ≠ 0"
assumes "(u ∙ v) * norm w * norm x = (w ∙ x) * norm u * norm v"
shows "vangle u v = vangle w x"
using assms Cauchy_Schwarz_ineq2[of u v] Cauchy_Schwarz_ineq2[of w x]
unfolding vangle_def by (auto simp: arccos_eq_iff field_simps)
lemma angle_eqI:
assumes "a ≠ b" "a ≠ c" "d ≠ e" "d ≠ f"
assumes "((b-a) ∙ (c-a)) * dist d e * dist d f = ((e-d) ∙ (f-d)) * dist a b * dist a c"
shows "angle b a c = angle e d f"
using assms unfolding angle_def
by (intro vangle_eqI) (simp_all add: dist_norm norm_minus_commute)
lemma cos_vangle_eqD: "cos (vangle u v) = cos (vangle w x) ⟹ vangle u v = vangle w x"
by (rule cos_inj_pi) (simp_all add: vangle_bounds)
lemma cos_angle_eqD: "cos (angle a b c) = cos (angle d e f) ⟹ angle a b c = angle d e f"
unfolding angle_def by (rule cos_vangle_eqD)
lemma sin_vangle_zero_iff: "sin (vangle u v) = 0 ⟷ vangle u v ∈ {0, pi}"
proof
assume "sin (vangle u v) = 0"
then obtain n :: int where n: "of_int n = vangle u v / pi"
by (subst (asm) sin_zero_iff_int2) auto
also have "… ∈ {0..1}" using vangle_bounds by (auto simp: field_simps)
finally have "n ∈ {0,1}" by auto
thus "vangle u v ∈ {0,pi}" using n by (auto simp: field_simps)
qed auto
lemma sin_angle_zero_iff: "sin (angle a b c) = 0 ⟷ angle a b c ∈ {0, pi}"
unfolding angle_def by (simp only: sin_vangle_zero_iff)
lemma vangle_collinear: "vangle u v ∈ {0, pi} ⟹ collinear {0, u, v}"
apply (subst norm_cauchy_schwarz_equal [symmetric])
apply (subst norm_cauchy_schwarz_abs_eq)
apply (auto dest!: vangle_eq_0D vangle_eq_piD simp: eq_neg_iff_add_eq_0)
done
lemma angle_collinear: "angle a b c ∈ {0, pi} ⟹ collinear {a, b, c}"
apply (unfold angle_def, drule vangle_collinear)
apply (subst collinear_translate_iff[symmetric, of _ "-b"])
apply (auto simp: insert_commute)
done
lemma not_collinear_vangle: "¬collinear {0,u,v} ⟹ vangle u v ∈ {0<..<pi}"
using vangle_bounds[of u v] vangle_collinear[of u v]
by (cases "vangle u v = 0 ∨ vangle u v = pi") auto
lemma not_collinear_angle: "¬collinear {a,b,c} ⟹ angle a b c ∈ {0<..<pi}"
using angle_bounds[of a b c] angle_collinear[of a b c]
by (cases "angle a b c = 0 ∨ angle a b c = pi") auto
subsection‹Contributions from Lukas Bulwahn›
lemma vangle_scales:
assumes "0 < c"
shows "vangle (c *⇩R v⇩1) v⇩2 = vangle v⇩1 v⇩2"
using assms unfolding vangle_def by auto
lemma vangle_inverse:
"vangle (- v⇩1) v⇩2 = pi - vangle v⇩1 v⇩2"
proof -
have "¦v⇩1 ∙ v⇩2 / (norm v⇩1 * norm v⇩2)¦ ≤ 1"
proof cases
assume "v⇩1 ≠ 0 ∧ v⇩2 ≠ 0"
from this show ?thesis by (simp add: Cauchy_Schwarz_ineq2)
next
assume "¬ (v⇩1 ≠ 0 ∧ v⇩2 ≠ 0)"
from this show ?thesis by auto
qed
from this show ?thesis
unfolding vangle_def
by (simp add: arccos_minus_abs)
qed
lemma orthogonal_iff_angle:
shows "orthogonal (A - B) (C - B) ⟷ angle A B C = pi / 2"
unfolding angle_def by (auto simp only: orthogonal_iff_vangle)
lemma angle_inverse:
assumes "between (A, C) B"
assumes "A ≠ B" "B ≠ C"
shows "angle A B D = pi - angle C B D"
proof -
from ‹between (A, C) B› obtain u where u: "u ≥ 0" "u ≤ 1"
and X: "B = u *⇩R A + (1 - u) *⇩R C"
by (metis add.commute betweenE between_commute)
from ‹A ≠ B› ‹B ≠ C› X have "u ≠ 0" "u ≠ 1" by auto
have "0 < ((1 - u) / u)"
using ‹u ≠ 0› ‹u ≠ 1› ‹u ≥ 0› ‹u ≤ 1› by simp
from X have "A - B = - (1 - u) *⇩R (C - A)"
by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib)
moreover from X have "C - B = u *⇩R (C - A)"
by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib)
ultimately have "A - B = - (((1 - u) / u) *⇩R (C - B))"
using ‹u ≠ 0› by simp (metis minus_diff_eq real_vector.scale_minus_left)
from this have "vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)"
using ‹0 < (1 - u) / u› by (simp add: vangle_inverse vangle_scales)
from this show ?thesis
unfolding angle_def by simp
qed
lemma strictly_between_implies_angle_eq_pi:
assumes "between (A, C) B"
assumes "A ≠ B" "B ≠ C"
shows "angle A B C = pi"
proof -
from ‹between (A, C) B› obtain u where u: "u ≥ 0" "u ≤ 1"
and X: "B = u *⇩R A + (1 - u) *⇩R C"
by (metis add.commute betweenE between_commute)
from ‹A ≠ B› ‹B ≠ C› X have "u ≠ 0" "u ≠ 1" by auto
from ‹A ≠ B› ‹B ≠ C› ‹between (A, C) B› have "A ≠ C" by auto
from X have "A - B = - (1 - u) *⇩R (C - A)"
by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib)
moreover from this have "dist A B = norm ((1 - u) *⇩R (C - A))"
using ‹u ≥ 0› ‹u ≤ 1› by (simp add: dist_norm)
moreover from X have "C - B = u *⇩R (C - A)"
by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib)
moreover from this have "dist C B = norm (u *⇩R (C - A))"
by (simp add: dist_norm)
ultimately have "(A - B) ∙ (C - B) / (dist A B * dist C B) = u * (u - 1) / (¦1 - u¦ * ¦u¦)"
using ‹A ≠ C› by (simp add: dot_square_norm power2_eq_square)
also have "… = - 1"
using ‹u ≠ 0› ‹u ≠ 1› ‹u ≥ 0› ‹u ≤ 1› by (simp add: divide_eq_minus_1_iff)
finally show ?thesis
unfolding angle_altdef by simp
qed
end