Theory Counterclockwise_2D_Strict

section ‹CCW for Nonaligned Points in the Plane›
theory Counterclockwise_2D_Strict
  imports
    Counterclockwise_Vector
    Affine_Arithmetic_Auxiliarities
begin
text ‹\label{sec:counterclockwise2d}›

subsection ‹Determinant›

type_synonym point = "real*real"

fun det3::"point  point  point  real" where "det3 (xp, yp) (xq, yq) (xr, yr) =
  xp * yq + yp * xr + xq * yr - yq * xr - yp * xq - xp * yr"

lemma det3_def':
  "det3 p q r = fst p * snd q + snd p * fst r + fst q * snd r -
    snd q * fst r - snd p * fst q - fst p * snd r"
  by (cases p q r rule: prod.exhaust[case_product prod.exhaust[case_product prod.exhaust]]) auto

lemma det3_eq_det: "det3 (xa, ya) (xb, yb) (xc, yc) =
  det (vector [vector [xa, ya, 1], vector [xb, yb, 1], vector [xc, yc, 1]]::real^3^3)"
  unfolding Determinants.det_def UNIV_3
  by (auto simp: sum_over_permutations_insert
    vector_3 sign_swap_id permutation_swap_id sign_compose)

declare det3.simps[simp del]

lemma det3_self23[simp]: "det3 a b b = 0"
  and det3_self12[simp]: "det3 b b a = 0"
  by (auto simp: det3_def')

lemma
  coll_ex_scaling:
  assumes "b  c"
  assumes d: "det3 a b c = 0"
  shows "r. a = b + r *R (c - b)"
proof -
  from assms have "fst b  fst c  snd b  snd c" by (auto simp: prod_eq_iff)
  thus ?thesis
  proof
    assume neq: "fst b  fst c"
    with d have "snd a = ((fst a - fst b) * snd c + (fst c - fst a) * snd b) / (fst c - fst b)"
      by (auto simp: det3_def' field_simps)
    hence "snd a = ((fst a - fst b)/ (fst c - fst b)) * snd c +
      ((fst c - fst a)/ (fst c - fst b)) * snd b"
      by (simp add: add_divide_distrib)
    hence "snd a = snd b + (fst a - fst b) * snd c / (fst c - fst b) +
      ((fst c - fst a) - (fst c - fst b)) * snd b / (fst c - fst b)"
      using neq
      by (simp add: field_simps)
    hence "snd a = snd b + ((fst a - fst b) * snd c + (- fst a + fst b) * snd b) / (fst c - fst b)"
      unfolding add_divide_distrib
      by (simp add: algebra_simps)
    also
    have "(fst a - fst b) * snd c + (- fst a + fst b) * snd b = (fst a - fst b) * (snd c - snd b)"
      by (simp add: algebra_simps)
    finally have "snd a = snd b + (fst a - fst b) / (fst c - fst b) * (snd c - snd b)"
      by simp
    moreover
    hence "fst a = fst b + (fst a - fst b) / (fst c - fst b) * (fst c - fst b)"
      using neq by simp
    ultimately have "a = b + ((fst a - fst b) / (fst c - fst b)) *R (c - b)"
      by (auto simp: prod_eq_iff)
    thus ?thesis by blast
  next
    assume neq: "snd b  snd c"
    with d have "fst a = ((snd a - snd b) * fst c + (snd c - snd a) * fst b) / (snd c - snd b)"
      by (auto simp: det3_def' field_simps)
    hence "fst a = ((snd a - snd b)/ (snd c - snd b)) * fst c +
      ((snd c - snd a)/ (snd c - snd b)) * fst b"
      by (simp add: add_divide_distrib)
    hence "fst a = fst b + (snd a - snd b) * fst c / (snd c - snd b) +
      ((snd c - snd a) - (snd c - snd b)) * fst b / (snd c - snd b)"
      using neq
      by (simp add: field_simps)
    hence "fst a = fst b + ((snd a - snd b) * fst c + (- snd a + snd b) * fst b) / (snd c - snd b)"
      unfolding add_divide_distrib
      by (simp add: algebra_simps)
    also
    have "(snd a - snd b) * fst c + (- snd a + snd b) * fst b = (snd a - snd b) * (fst c - fst b)"
      by (simp add: algebra_simps)
    finally have "fst a = fst b + (snd a - snd b) / (snd c - snd b) * (fst c - fst b)"
      by simp
    moreover
    hence "snd a = snd b + (snd a - snd b) / (snd c - snd b) * (snd c - snd b)"
      using neq by simp
    ultimately have "a = b + ((snd a - snd b) / (snd c - snd b)) *R (c - b)"
      by (auto simp: prod_eq_iff)
    thus ?thesis by blast
  qed
qed

lemma cramer: "¬det3 s t q = 0 
  (det3 t p r) = ((det3 t q r) * (det3 s t p) + (det3 t p q) * (det3 s t r))/(det3 s t q)"
  by (auto simp: det3_def' field_simps)

lemma convex_comb_dets:
  assumes "det3 p q r > 0"
  shows "s = (det3 s q r / det3 p q r) *R p + (det3 p s r /  det3 p q r) *R q +
      (det3 p q s / det3 p q r) *R r"
    (is "?lhs = ?rhs")
proof -
  from assms have "det3 p q r *R ?lhs = det3 p q r *R ?rhs"
    by (simp add: field_simps prod_eq_iff scaleR_add_right) (simp add: algebra_simps det3_def')
  thus ?thesis using assms by simp
qed

lemma four_points_aligned:
  assumes c: "det3 t p q = 0" "det3 t q r = 0"
  assumes distinct: "distinct5 t s p q r"
  shows "det3 t r p = 0" "det3 p q r = 0"
proof -
  from distinct have d: "p  q" "q  r" by (auto)
  from coll_ex_scaling[OF d(1) c(1)] obtain s1 where s1: "t = p + s1 *R (q - p)" by auto
  from coll_ex_scaling[OF d(2) c(2)] obtain s2 where s2: "t = q + s2 *R (r - q)" by auto
  from distinct s1 have ne: "1 - s1  0" by auto
  from s1 s2 have "(1 - s1) *R p = (1 - s1 - s2) *R q + s2 *R r"
    by (simp add: algebra_simps)
  hence "(1 - s1) *R p /R (1 - s1)= ((1 - s1 - s2) *R q + s2 *R r) /R (1 - s1)"
    by simp
  with ne have p: "p = ((1 - s1 - s2) / (1 - s1)) *R q + (s2 / (1 - s1)) *R r"
    using ne
    by (simp add: prod_eq_iff inverse_eq_divide add_divide_distrib)
  define k1 where "k1 = (1 - s1 - s2) / (1 - s1)"
  define k2 where "k2 = s2 / (1 - s1)"
  have "det3 t r p = det3 0 (k1 *R q + (k2 - 1) *R r)
    (k1 *R q + (k2 - 1) *R r + (- s1 * (k1 - 1)) *R q - (s1 * k2) *R r)"
    unfolding s1 p k1_def[symmetric] k2_def[symmetric]
    by (simp add: algebra_simps det3_def')
  also have "- s1 * (k1 - 1) = s1 * k2"
    using ne by (auto simp: k1_def field_simps k2_def)
  also
  have "1 - k1 = k2"
    using ne
    by (auto simp: k2_def k1_def field_simps)
  have k21: "k2 - 1 = -k1"
    using ne
    by (auto simp: k2_def k1_def field_simps)
  finally have "det3 t r p = det3 0 (k1 *R (q - r)) ((k1 + (s1 * k2)) *R (q - r))"
    by (auto simp: algebra_simps)
  also have " = 0"
    by (simp add: algebra_simps det3_def')
  finally show "det3 t r p = 0" .
  have "det3 p q r = det3 (k1 *R q + k2 *R r) q r"
    unfolding p k1_def[symmetric] k2_def[symmetric] ..
  also have " = det3 0 (r - q) (k1 *R q + (-k1) *R r)"
    unfolding k21[symmetric]
    by (auto simp: algebra_simps det3_def')
  also have " = det3 0 (r - q) (-k1 *R (r - q))"
    by (auto simp: det3_def' algebra_simps)
  also have " = 0"
    by (auto simp: det3_def')
  finally show "det3 p q r = 0" .
qed

lemma det_identity:
  "det3 t p q * det3 t s r + det3 t q r * det3 t s p + det3 t r p * det3 t s q = 0"
  by (auto simp: det3_def' algebra_simps)

lemma det3_eq_zeroI:
  assumes "p = q + x *R (t - q)"
  shows "det3 q t p = 0"
  unfolding assms
  by (auto simp: det3_def' algebra_simps)

lemma det3_rotate: "det3 a b c = det3 c a b"
  by (auto simp: det3_def')

lemma det3_switch: "det3 a b c = - det3 a c b"
  by (auto simp: det3_def')

lemma det3_switch': "det3 a b c = - det3 b a c"
  by (auto simp: det3_def')

lemma det3_pos_transitive_coll:
  "det3 t s p > 0  det3 t s r  0  det3 t p q  0 
  det3 t q r > 0  det3 t s q = 0  det3 t p r > 0"
  using det_identity[of t p q s r]
  by (metis add.commute add_less_same_cancel1 det3_switch det3_switch' less_eq_real_def
    less_not_sym monoid_add_class.add.left_neutral mult_pos_pos mult_zero_left mult_zero_right)

lemma det3_pos_transitive:
  "det3 t s p > 0  det3 t s q  0  det3 t s r  0  det3 t p q  0 
  det3 t q r > 0  det3 t p r > 0"
  apply (cases "det3 t s q  0")
   using cramer[of q t s p r]
   apply (force simp: det3_rotate[of q t p] det3_rotate[of p q t] det3_switch[of t p s]
     det3_switch'[of q t r] det3_rotate[of q t s] det3_rotate[of s q t]
     intro!: divide_pos_pos add_nonneg_pos)
  apply (metis det3_pos_transitive_coll)
  done

lemma det3_zero_translate_plus[simp]: "det3 (a + x) (b + x) (c + x) = 0  det3 a b c = 0"
  by (auto simp: algebra_simps det3_def')

lemma det3_zero_translate_plus'[simp]: "det3 (a) (a + b) (a + c) = 0  det3 0 b c = 0"
  by (auto simp: algebra_simps det3_def')

lemma
  det30_zero_scaleR1:
  "0 < e  det3 0 xr P = 0  det3 0 (e *R xr) P = 0"
  by (auto simp: zero_prod_def algebra_simps det3_def')

lemma det3_same[simp]: "det3 a x x = 0"
  by (auto simp: det3_def')

lemma
  det30_zero_scaleR2:
  "0 < e  det3 0 P xr = 0  det3 0 P (e *R xr) = 0"
  by (auto simp: zero_prod_def algebra_simps det3_def')

lemma det3_eq_zero: "e  0  det3 0 xr (e *R Q) = 0  det3 0 xr Q = 0"
  by (auto simp: det3_def')

lemma det30_plus_scaled3[simp]: "det3 0 a (b + x *R a) = 0  det3 0 a b = 0"
  by (auto simp: det3_def' algebra_simps)

lemma det30_plus_scaled2[simp]:
  shows "det3 0 (a + x *R a) b = 0  (if x = -1 then True else det3 0 a b = 0)"
    (is "?lhs = ?rhs")
proof
  assume "det3 0 (a + x *R a) b = 0"
  hence "fst a * snd b * (1 + x) = fst b * snd a * (1 + x)"
    by (simp add: algebra_simps det3_def')
  thus ?rhs
    by (auto simp add: det3_def')
qed (auto simp: det3_def' algebra_simps split: if_split_asm)

lemma det30_uminus2[simp]: "det3 0 (-a) (b) = 0  det3 0 a b = 0"
  and det30_uminus3[simp]: "det3 0 a (-b) = 0  det3 0 a b = 0"
  by (auto simp: det3_def' algebra_simps)

lemma det30_minus_scaled3[simp]: "det3 0 a (b - x *R a) = 0  det3 0 a b = 0"
  using det30_plus_scaled3[of a b "-x"] by simp

lemma det30_scaled_minus3[simp]: "det3 0 a (e *R a - b) = 0  det3 0 a b = 0"
  using det30_plus_scaled3[of a "-b" e]
  by (simp add: algebra_simps)

lemma det30_minus_scaled2[simp]:
  "det3 0 (a - x *R a) b = 0  (if x = 1 then True else det3 0 a b = 0)"
  using det30_plus_scaled2[of a  "-x" b] by simp

lemma det3_nonneg_scaleR1:
  "0 < e  det3 0 xr P  0  det3 0 (e*Rxr) P  0"
  by (auto simp add: det3_def' algebra_simps)

lemma det3_nonneg_scaleR1_eq:
  "0 < e  det3 0 (e*Rxr) P  0  det3 0 xr P  0"
  by (auto simp add: det3_def' algebra_simps)

lemma det3_translate_origin: "NO_MATCH 0 p  det3 p q r = det3 0 (q - p) (r - p)"
  by (auto simp: det3_def' algebra_simps)

lemma det3_nonneg_scaleR_segment2:
  assumes "det3 x y z  0"
  assumes "a > 0"
  shows "det3 x ((1 - a) *R x + a *R y) z  0"
proof -
  from assms have "0  det3 0 (a *R (y - x)) (z - x)"
    by (intro det3_nonneg_scaleR1) (simp_all add: det3_translate_origin)
  thus ?thesis
    by (simp add: algebra_simps det3_translate_origin)
qed

lemma det3_nonneg_scaleR_segment1:
  assumes "det3 x y z  0"
  assumes "0  a" "a < 1"
  shows "det3 ((1 - a) *R x + a *R y) y z  0"
proof -
  from assms have "det3 0 ((1 - a) *R (y - x)) (z - x + (- a) *R (y - x))  0"
    by (subst det3_nonneg_scaleR1_eq) (auto simp add: det3_def' algebra_simps)
  thus ?thesis
    by (auto simp: algebra_simps det3_translate_origin)
qed


subsection ‹Strict CCW Predicate›

definition "ccw' p q r  0 < det3 p q r"

interpretation ccw': ccw_vector_space ccw'
  by unfold_locales (auto simp: ccw'_def det3_def' algebra_simps)

interpretation ccw': linorder_list0 "ccw' x" for x .

lemma ccw'_contra: "ccw' t r q  ccw' t q r = False"
  by (auto simp: ccw'_def det3_def' algebra_simps)

lemma not_ccw'_eq: "¬ ccw' t p s  ccw' t s p  det3 t s p = 0"
  by (auto simp: ccw'_def det3_def' algebra_simps)

lemma neq_left_right_of: "ccw' a b c  ccw' a c d  b  d"
  by (auto simp: ccw'_def det3_def' algebra_simps)

lemma ccw'_subst_collinear:
  assumes "det3 t r s = 0"
  assumes "s  t"
  assumes "ccw' t r p"
  shows "ccw' t s p  ccw' t p s"
proof cases
  assume "r  s"
  from assms have "det3 r s t = 0"
    by (auto simp: algebra_simps det3_def')
  from coll_ex_scaling[OF assms(2) this]
  obtain x where s: "r = s + x *R (t - s)" by auto
  from assms(3)[simplified ccw'_def s]
  have "0 < det3 0 (s + x *R (t - s) - t) (p - t)"
    by (auto simp: algebra_simps det3_def')
  also have "s + x *R (t - s) - t = (1 - x) *R (s - t)"
    by (simp add: algebra_simps)
  finally have ccw': "ccw' 0 ((1 - x) *R (s - t)) (p - t)"
    by (simp add: ccw'_def)
  hence "x  1" by (auto simp add: det3_def' ccw'_def)
  {
    assume "x < 1"
    hence ?thesis using ccw'
      by (auto simp: not_ccw'_eq ccw'.translate_origin)
  } moreover {
    assume "x > 1"
    hence ?thesis using ccw'
      by (auto simp: not_ccw'_eq ccw'.translate_origin)
  } ultimately show ?thesis using x  1 by arith
qed (insert assms, simp)

lemma ccw'_sorted_scaleR: "ccw'.sortedP 0 xs  r > 0  ccw'.sortedP 0 (map ((*R) r) xs)"
  by (induct xs) (auto intro!: ccw'.sortedP.Cons  elim!: ccw'.sortedP_Cons simp del: scaleR_Pair)


subsection ‹Collinearity›

abbreviation "coll a b c  det3 a b c = 0"

lemma coll_zero[intro, simp]: "coll 0 z 0"
  by (auto simp: det3_def')

lemma coll_zero1[intro, simp]: "coll 0 0 z"
  by (auto simp: det3_def')

lemma coll_self[intro, simp]: "coll 0 z z"
  by auto

lemma ccw'_not_coll:
  "ccw' a b c  ¬coll a b c"
  "ccw' a b c  ¬coll a c b"
  "ccw' a b c  ¬coll b a c"
  "ccw' a b c  ¬coll b c a"
  "ccw' a b c  ¬coll c a b"
  "ccw' a b c  ¬coll c b a"
  by (auto simp: det3_def' ccw'_def algebra_simps)

lemma coll_add: "coll 0 x y  coll 0 x z  coll 0 x (y + z)"
  by (auto simp: det3_def' algebra_simps)

lemma coll_scaleR_left_eq[simp]: "coll 0 (r *R x) y  r = 0  coll 0 x y"
  by (auto simp: det3_def' algebra_simps)

lemma coll_scaleR_right_eq[simp]: "coll 0 y (r *R x)  r = 0  coll 0 y x"
  by (auto simp: det3_def' algebra_simps)

lemma coll_scaleR: "coll 0 x y  coll 0 (r *R x) y"
  by (auto simp: det3_def' algebra_simps)

lemma coll_sum_list: "(y. y  set ys  coll 0 x y)  coll 0 x (sum_list ys)"
  by (induct ys) (auto intro!: coll_add)

lemma scaleR_left_normalize:
  fixes a ::real and b c::"'a::real_vector"
  shows "a *R b = c  (if a = 0 then c = 0 else b = c /R a)"
  by (auto simp: field_simps)

lemma coll_scale_pair: "coll 0 (a, b) (c, d)  (a, b)  0  (x. (c, d) = x *R (a, b))"
  by (auto intro: exI[where x="c/a"] exI[where x="d/b"] simp: det3_def' field_simps prod_eq_iff)

lemma coll_scale: "coll 0 r q  r  0  (x. q = x *R r)"
  using coll_scale_pair[of "fst r" "snd r" "fst q" "snd q"]
  by simp

lemma coll_add_trans:
  assumes "coll 0 x (y + z)"
  assumes "coll 0 y z"
  assumes "x  0"
  assumes "y  0"
  assumes "z  0"
  assumes "y + z  0"
  shows "coll 0 x z"
proof (cases "snd z = 0")
  case True
  hence "snd y = 0"
    using assms
    by (cases z) (auto simp add: zero_prod_def det3_def')
  with True assms have "snd x = 0"
    by (cases y, cases z) (auto simp add: zero_prod_def det3_def')
  from snd x = 0 snd y = 0 snd z = 0
  show ?thesis
    by (auto simp add: zero_prod_def det3_def')
next
  case False
  note z = False
  hence "snd y  0"
    using assms
    by (cases y) (auto simp add: zero_prod_def det3_def')
  with False assms have "snd x  0"
    apply (cases x)
    apply (cases y)
    apply (cases z)
    apply (auto simp add: zero_prod_def det3_def')
    apply (metis mult.commute mult_eq_0_iff ring_class.ring_distribs(1))
    done
  with False assms snd y  0 have yz: "snd (y + z)  0"
    by (cases x; cases y; cases z) (auto simp add: det3_def' zero_prod_def)
  from coll_scale[OF assms(1) assms(3)] coll_scale[OF assms(2) assms(4)]
  obtain r s where rs: "y + z = r *R x" "z = s *R y"
    by auto
  with z have "s  0"
    by (cases x; cases y; cases z) (auto simp: zero_prod_def)
  with rs z yz have "r  0"
    by (cases x; cases y; cases z) (auto simp: zero_prod_def)
  from s  0 rs have "y = r *R x - z" "y = z /R s"
    by (auto simp: inverse_eq_divide algebra_simps)
  hence "r *R x - z = z /R s" by simp
  hence "r *R x = (1 + inverse s) *R z"
    by (auto simp: inverse_eq_divide algebra_simps)
  hence "x = (inverse r * (1 + inverse s)) *R z"
    using r  0 s  0
    by (auto simp: field_simps scaleR_left_normalize)
  from this
  show ?thesis
    by (auto intro: coll_scaleR)
qed

lemma coll_commute: "coll 0 a b  coll 0 b a"
  by (metis det3_rotate det3_switch' diff_0 diff_self)

lemma coll_add_cancel: "coll 0 a (a + b)  coll 0 a b"
  by (cases a, cases b) (auto simp: det3_def' algebra_simps)

lemma coll_trans:
  "coll 0 a b  coll 0 a c  a  0  coll 0 b c"
  by (metis coll_scale coll_scaleR)

lemma sum_list_posI:
  fixes xs::"'a::ordered_comm_monoid_add list"
  shows "(x. x  set xs  x > 0)  xs  []  sum_list xs > 0"
proof (induct xs)
  case (Cons x xs)
  thus ?case
    by (cases "xs = []") (auto intro!: add_pos_pos)
qed simp

lemma nonzero_fstI[intro, simp]: "fst x  0  x  0"
  and nonzero_sndI[intro, simp]: "snd x  0  x  0"
  by auto

lemma coll_sum_list_trans:
  "xs  []  coll 0 a (sum_list xs)  (x. x  set xs  coll 0 x y) 
    (x. x  set xs  coll 0 x (sum_list xs)) 
    (x. x  set xs  snd x > 0)  a  0  coll 0 a y"
proof (induct xs rule: list_nonempty_induct)
  case (single x)
  from single(1) single(2)[of x] single(4)[of x] have "coll 0 x a" "coll 0 x y" "x  0"
    by (auto simp: coll_commute)
  thus ?case by (rule coll_trans)
next
  case (cons x xs)
  from cons(5)[of x] a  0 cons(6)[of x]
  have *: "coll 0 x (sum_list xs)" "a  0" "x  0" by (force simp add: coll_add_cancel)+
  have "0 < snd (sum_list (x#xs))"
    unfolding snd_sum_list
    by (rule sum_list_posI) (auto intro!: add_pos_pos cons simp: snd_sum_list)
  hence "x + sum_list xs  0" by simp
  from coll_add_trans[OF cons(3)[simplified] * _ this]
  have cH: "coll 0 a (sum_list xs)"
    by (cases "sum_list xs = 0") auto
  from cons(4) have cy: "(x. x  set xs  coll 0 x y)" by simp
  {
    fix y assume "y  set xs"
    hence "snd (sum_list xs) > 0"
      unfolding snd_sum_list
      by (intro sum_list_posI) (auto intro!: add_pos_pos cons simp: snd_sum_list)
    hence "sum_list xs  0" by simp
    from cons(5)[of x] have "coll 0 x (sum_list xs)"
      by (simp add: coll_add_cancel)
    from cons(5)[of y]
    have "coll 0 y (sum_list xs)"
      using y  set xs cons(6)[of y] x + sum_list xs  0
      apply (cases "y = x")
      subgoal by (force simp add: coll_add_cancel)
      subgoal by (force simp: dest!: coll_add_trans[OF _ *(1) _ *(3)])
      done
  } note cl = this
  show ?case
    by (rule cons(2)[OF cH cy cl cons(6) a  0]) auto
qed

lemma sum_list_coll_ex_scale:
  assumes coll: "x. x  set xs  coll 0 z x"
  assumes nz: "z  0"
  shows "r. sum_list xs = r *R z"
proof -
  {
    fix i assume i: "i < length xs"
    hence nth: "xs ! i  set xs" by simp
    note coll_scale[OF coll[OF nth] z  0]
  } then obtain r where r: "i. i < length xs  r i *R z = xs ! i"
    by metis
  have "xs = map ((!) xs) [0..<length xs]" by (simp add: map_nth)
  also have " = map (λi. r i *R z) [0..<length xs]"
    by (auto simp: r)
  also have "sum_list  = (i[0..<length xs]. r i) *R z"
    by (simp add: sum_list_sum_nth scaleR_sum_left)
  finally show ?thesis ..
qed

lemma sum_list_filter_coll_ex_scale: "z  0  r. sum_list (filter (coll 0 z) zs) = r *R z"
  by (rule sum_list_coll_ex_scale) simp

end