Theory Triangle.Angles

(*
  File:    Angles.thy
  Author:  Manuel Eberl <manuel@pruvisto.org>

  Definition of angles between vectors and between three points.
*)

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 v1) v2 = vangle v1 v2"
using assms unfolding vangle_def by auto

lemma vangle_inverse:
  "vangle (- v1) v2 = pi - vangle v1 v2"
proof -
  have "¦v1  v2 / (norm v1 * norm v2)¦  1"
  proof cases
    assume "v1  0  v2  0"
    from this show ?thesis by (simp add: Cauchy_Schwarz_ineq2)
  next
    assume "¬ (v1  0  v2  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