Theory 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