Theory Affine_Arithmetic.Counterclockwise_Vector

section ‹CCW Vector Space›
theory Counterclockwise_Vector
imports Counterclockwise
begin

locale ccw_vector_space = ccw_system12 ccw S for ccw::"'a::real_vector ⇒ 'a ⇒ 'a ⇒ bool" and S +
  assumes translate_plus[simp]: "ccw (a + x) (b + x) (c + x) ⟷ ccw a b c"
  assumes scaleR1_eq[simp]: "0 < e ⟹ ccw 0 (e*⇩Ra) b = ccw 0 a b"
  assumes uminus1[simp]: "ccw 0 (-a) b = ccw 0 b a"
  assumes add1: "ccw 0 a b ⟹ ccw 0 c b ⟹ ccw 0 (a + c) b"
begin

lemma translate_plus'[simp]:
  "ccw (x + a) (x + b) (x + c) ⟷ ccw a b c"
  by (auto simp: ac_simps)

lemma uminus2[simp]: "ccw 0 a (- b) = ccw 0 b a"
  by (metis minus_minus uminus1)

lemma uminus_all[simp]: "ccw (-a) (-b) (-c) ⟷ ccw a b c"
proof -
  have "ccw (-a) (-b) (-c) ⟷ ccw 0 (- (b - a)) (- (c - a))"
    using translate_plus[of "-a" a "-b" "-c"]
    by simp
  also have "… ⟷ ccw 0 (b - a) (c - a)"
    by (simp del: minus_diff_eq)
  also have "… ⟷ ccw a b c"
    using translate_plus[of a "-a" b c]
    by simp
  finally show ?thesis .
qed

lemma translate_origin: "NO_MATCH 0 p ⟹ ccw p q r ⟷ ccw 0 (q - p) (r - p)"
  using translate_plus[of p "- p" q r]
  by simp

lemma translate[simp]: "ccw a (a + b) (a + c) ⟷ ccw 0 b c"
  by (simp add: translate_origin)

lemma translate_plus3: "ccw (a - x) (b - x) c ⟷ ccw a b (c + x)"
  using translate_plus[of a "-x" b "c + x"] by simp

lemma renormalize:
  "ccw 0 (a - b) (c - a) ⟹ ccw b a c"
  by (metis diff_add_cancel diff_self cyclic minus_diff_eq translate_plus3 uminus1)

lemma cyclicI: "ccw p q r ⟹ ccw q r p"
  by (metis cyclic)

lemma
  scaleR2_eq[simp]:
  "0 < e ⟹ ccw 0 xr (e *⇩R P) ⟷ ccw 0 xr P"
  using scaleR1_eq[of e "-P" xr]
  by simp

lemma scaleR1_nonzero_eq:
  "e ≠ 0 ⟹ ccw 0 (e *⇩R a) b = (if e > 0 then ccw 0 a b else ccw 0 b a)"
proof cases
  assume "e < 0"
  define e' where "e' = - e"
  hence "e = -e'" "e' > 0" using ‹e < 0› by simp_all
  thus ?thesis by simp
qed simp

lemma neg_scaleR[simp]: "x < 0 ⟹ ccw 0 (x *⇩R b) c ⟷ ccw 0 c b"
  using scaleR1_nonzero_eq by auto

lemma
  scaleR1:
  "0 < e ⟹ ccw 0 xr P ⟹ ccw 0 (e *⇩R xr) P"
  by simp

lemma
  add3: "ccw 0 a b ∧ ccw 0 a c ⟹ ccw 0 a (b + c)"
  using add1[of "-b" a "-c"] uminus1[of "b + c" a]
  by simp

lemma add3_self[simp]: "ccw 0 p (p + q) ⟷ ccw 0 p q"
  using translate[of "-p" p "p + q"]
  apply (simp add: cyclic)
  apply (metis cyclic uminus2)
  done

lemma add2_self[simp]: "ccw 0 (p + q) p ⟷ ccw 0 q p"
  using translate[of "-p" "p + q" p]
  apply simp
  apply (metis cyclic uminus1)
  done

lemma scale_add3[simp]: "ccw 0 a (x *⇩R a + b) ⟷ ccw 0 a b"
proof -
  {
    assume "x = 0"
    hence ?thesis by simp
  } moreover {
    assume "x > 0"
    hence ?thesis using add3_self scaleR1_eq by blast
  } moreover {
    assume "x < 0"
    define x' where "x' = - x"
    hence "x = -x'" "x' > 0" using ‹x < 0› by simp_all
    hence "ccw 0 a (x *⇩R a + b) = ccw 0 (x' *⇩R a + - b) (x' *⇩R a)"
      by (subst uminus1[symmetric]) simp
    also have "… = ccw 0 (- b) a"
      unfolding add2_self by (simp add: ‹x' > 0›)
    also have "… = ccw 0 a b"
      by simp
    finally have ?thesis .
  } ultimately show ?thesis by arith
qed

lemma scale_add3'[simp]: "ccw 0 a (b + x *⇩R a) ⟷ ccw 0 a b"
  and scale_minus3[simp]: "ccw 0 a (x *⇩R a - b) ⟷ ccw 0 b a"
  and scale_minus3'[simp]: "ccw 0 a (b - x *⇩R a) ⟷ ccw 0 a b"
  using
    scale_add3[of a x b]
    scale_add3[of a "-x" b]
    scale_add3[of a x "-b"]
  by (simp_all add: ac_simps)

lemma sum:
  assumes fin: "finite X"
  assumes ne: "X≠{}"
  assumes ncoll: "(⋀x. x ∈ X ⟹ ccw 0 a (f x))"
  shows "ccw 0 a (sum f X)"
proof -
  from ne obtain x where "x ∈ X" "insert x X = X" by auto
  have "ccw 0 a (sum f (insert x X))"
    using fin ncoll
  proof (induction X)
    case empty thus ?case using ‹x ∈ X› ncoll
      by auto
  next
    case (insert y F)
    hence "ccw 0 a (sum f (insert y (insert x F)))"
      by (cases "y = x") (auto intro!: add3)
    thus ?case
      by (simp add: insert_commute)
  qed
  thus ?thesis using ‹insert x X = X› by simp
qed

lemma sum2:
  assumes fin: "finite X"
  assumes ne: "X≠{}"
  assumes ncoll: "(⋀x. x ∈ X ⟹ ccw 0 (f x) a)"
  shows "ccw 0 (sum f X) a"
  using sum[OF assms(1,2), of "-a" f] ncoll
  by simp

lemma translate_minus[simp]:
  "ccw (x - a) (x - b) (x - c) = ccw (-a) (-b) (-c)"
  using translate_plus[of "-a" x "-b" "-c"]
  by simp

end

locale ccw_convex = ccw_system ccw S for ccw and S::"'a::real_vector set" +
  fixes oriented
  assumes convex2:
    "u ≥ 0 ⟹ v ≥ 0 ⟹ u + v = 1 ⟹ ccw a b c ⟹ ccw a b d ⟹ oriented a b ⟹
      ccw a b (u *⇩R c + v *⇩R d)"
begin

lemma convex_hull:
  assumes [intro, simp]: "finite C"
  assumes ccw: "⋀c. c ∈ C ⟹ ccw a b c"
  assumes ch: "x ∈ convex hull C"
  assumes oriented: "oriented a b"
  shows "ccw a b x"
proof -
  define D where "D = C"
  have D: "C ⊆ D" "⋀c. c ∈ D ⟹ ccw a b c" by (simp_all add: D_def ccw)
  show "ccw a b x"
    using ‹finite C› D ch
  proof (induct arbitrary: x)
    case empty thus ?case by simp
  next
    case (insert c C)
    hence "C ⊆ D" by simp
    {
      assume "C = {}"
      hence ?case
        using insert
        by simp
    } moreover {
      assume "C ≠ {}"
      from convex_hull_insert[OF this, of c] insert(6)
      obtain u v d where "u ≥ 0" "v ≥ 0" "d ∈ convex hull C" "u + v = 1"
        and x: "x = u *⇩R c + v *⇩R d"
        by blast
      have "ccw a b d"
        by (auto intro: insert.hyps(3)[OF ‹C ⊆ D›] insert.prems ‹d ∈ convex hull C›)
      from insert
      have "ccw a b c"
        by simp
      from convex2[OF ‹0 ≤ u› ‹0 ≤ v› ‹u + v = 1› ‹ccw a b c› ‹ccw a b d› ‹oriented a b›]
      have ?case by (simp add: x)
    } ultimately show ?case by blast
  qed
qed

end

end