section {* CCW Vector Space *}
theory Counterclockwise_Vector
imports Counterclockwise
begin

locale ccw_vector_space = ccw_system12 ccw S for ccw::"'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" and S +
  assumes translate_plus[simp]: "ccw (a + x) (b + x) (c + x) \<longleftrightarrow> ccw a b c"
  assumes scaleR1_eq[simp]: "0 < e \<Longrightarrow> ccw 0 (e*\<^sub>Ra) b = ccw 0 a b"
  assumes uminus1[simp]: "ccw 0 (-a) b = ccw 0 b a"
  assumes add1: "ccw 0 a b \<Longrightarrow> ccw 0 c b \<Longrightarrow> ccw 0 (a + c) b"
begin

lemma translate_plus'[simp]:
  "ccw (x + a) (x + b) (x + c) \<longleftrightarrow> ccw a b c"
  by (auto simp: ac_simps)

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

lemma uminus_all[simp]: "ccw (-a) (-b) (-c) \<longleftrightarrow> ccw a b c"
proof -
  have f1: "\<forall>a aa. (aa\<Colon>'a) + - a = - (a + - aa)"
    by force
  have f2: "\<forall>a. (a\<Colon>'a) + - a = 0"
    by auto
  have f3: "\<forall>a aa. ccw 0 a aa \<or> \<not> ccw 0 aa (- a)"
    by auto
  hence "(\<exists>aa. ccw (aa + - a) (aa + - b) (aa + - c)) \<or> (\<exists>aa ab. \<not> ccw (aa + - a) (aa + - b) (aa + - c) \<and> \<not> ccw (ab + a) (ab + b) (ab + c))"
    using f2 f1 by (metis add.commute)
  moreover
  { assume "\<exists>aa. ccw (aa + - a) (aa + - b) (aa + - c)"
    moreover
    { assume "\<exists>aa ab. ccw (aa + - a) (aa + - b) (aa + - c) \<and> \<not> ccw (ab + a) (ab + b) (ab + c)"
      moreover
      { assume "\<exists>aa. ccw 0 (a + - b) (a + - c) \<and> ccw (aa + - a) (aa + - b) (aa + - c)"
        hence "\<exists>aa. ccw 0 (c + - a) (a + - b) \<and> ccw (aa + - a) (aa + - b) (aa + - c)"
          using f3 f1 by (metis (no_types))
        hence "\<exists>aa ab. ccw (aa + a) (aa + b) (aa + c) \<and> ccw (ab + - a) (ab + - b) (ab + - c)"
          using f3 f2 f1 by (metis (no_types) add.commute) }
      ultimately have "(\<exists>aa ab. \<not> ccw (aa + - a) (aa + - b) (aa + - c) \<and> \<not> ccw (ab + a) (ab + b) (ab + c)) \<or> (\<exists>aa ab. ccw (aa + a) (aa + b) (aa + c) \<and> ccw (ab + - a) (ab + - b) (ab + - c))"
        using f2 by metis }
    ultimately have "(\<exists>aa ab. \<not> ccw (aa + - a) (aa + - b) (aa + - c) \<and> \<not> ccw (ab + a) (ab + b) (ab + c)) \<or> ccw (- a) (- b) (- c) = ccw a b c"
      using translate_plus' by blast }
  ultimately show ?thesis
    using translate_plus' by blast
qed

lemma translate_origin: "NO_MATCH 0 p \<Longrightarrow> ccw p q r \<longleftrightarrow> 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) \<longleftrightarrow> ccw 0 b c"
  by (simp add: translate_origin)

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

lemma
  scaleR2_eq[simp]:
  "0 < e \<Longrightarrow> ccw 0 xr (e *\<^sub>R P) \<longleftrightarrow> ccw 0 xr P"
  using scaleR1_eq[of e "-P" xr]
  by simp

lemma scaleR1_nonzero_eq:
  "e \<noteq> 0 \<Longrightarrow> ccw 0 (e *\<^sub>R a) b = (if e > 0 then ccw 0 a b else ccw 0 b a)"
proof cases
  assume "e < 0"
  def e' \<equiv> "- e"
  hence "e = -e'" "e' > 0" using `e < 0` by simp_all
  thus ?thesis by simp
qed simp

lemma neg_scaleR[simp]: "x < 0 \<Longrightarrow> ccw 0 (x *\<^sub>R b) c \<longleftrightarrow> ccw 0 c b"
  using scaleR1_nonzero_eq by auto

lemma
  scaleR1:
  "0 < e \<Longrightarrow> ccw 0 xr P \<Longrightarrow> ccw 0 (e *\<^sub>R xr) P"
  by simp

lemma
  add3: "ccw 0 a b \<and> ccw 0 a c \<Longrightarrow> 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) \<longleftrightarrow> ccw 0 p q"
  using translate[of "-p" p "p + q"]
  apply simp
  apply (metis cyclic uminus2)
  done

lemma add2_self[simp]: "ccw 0 (p + q) p \<longleftrightarrow> 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 *\<^sub>R a + b) \<longleftrightarrow> 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"
    def x' \<equiv> "-x"
    hence "x = -x'" "x' > 0" using `x < 0` by simp_all
    hence "ccw 0 a (x *\<^sub>R a + b) = ccw 0 (x' *\<^sub>R a + - b) (x' *\<^sub>R a)"
      by (subst uminus1[symmetric]) simp
    also have "\<dots> = ccw 0 (- b) a"
      unfolding add2_self by (simp add: `x' > 0`)
    also have "\<dots> = ccw 0 a b"
      by simp
    finally have ?thesis .
  } ultimately show ?thesis by arith
qed

lemma scale_add3'[simp]: "ccw 0 a (b + x *\<^sub>R a) \<longleftrightarrow> ccw 0 a b"
  and scale_minus3[simp]: "ccw 0 a (x *\<^sub>R a - b) \<longleftrightarrow> ccw 0 b a"
  and scale_minus3'[simp]: "ccw 0 a (b - x *\<^sub>R a) \<longleftrightarrow> 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 setsum:
  assumes fin: "finite X"
  assumes ne: "X\<noteq>{}"
  assumes ncoll: "(\<And>x. x \<in> X \<Longrightarrow> ccw 0 a (f x))"
  shows "ccw 0 a (setsum f X)"
proof -
  from ne obtain x where "x \<in> X" by auto
  hence "insert x X = X"
    by auto
  have "ccw 0 a (setsum f (insert x X))"
    using fin ncoll
    apply (induct X rule: finite_induct)
    using `x \<in> X` ncoll
    apply (auto intro!: )
  proof -
    case (goal1 y)
    have "ccw 0 a (setsum f (insert y (insert x F)))"
      apply (cases "y = x")
      apply (simp add: goal1)
      apply (subst setsum.insert)
      using goal1 apply simp
      using goal1 apply simp
      using goal1
      apply (auto intro!: add3)
      done
    thus ?case
      by (simp add: insert_commute)
  qed
  thus ?thesis using `insert x X = X` by simp
qed

lemma setsum2:
  assumes fin: "finite X"
  assumes ne: "X\<noteq>{}"
  assumes ncoll: "(\<And>x. x \<in> X \<Longrightarrow> ccw 0 (f x) a)"
  shows "ccw 0 (setsum f X) a"
  using setsum[OF assms(1,2), of "-a" f] ncoll
  by simp

end

locale ccw_convex = ccw_system ccw S for ccw and S::"'a::real_vector set" +
  fixes oriented
  assumes convex2: "u \<ge> 0 \<Longrightarrow> v \<ge> 0 \<Longrightarrow> u + v = 1 \<Longrightarrow> ccw a b c \<Longrightarrow> ccw a b d \<Longrightarrow> oriented a b \<Longrightarrow> ccw a b (u *\<^sub>R c + v *\<^sub>R d)"
begin

lemma convex_hull:
  assumes [intro, simp]: "finite C"
  assumes ccw: "\<And>c. c \<in> C \<Longrightarrow> ccw a b c"
  assumes ch: "x \<in> convex hull C"
  assumes oriented: "oriented a b"
  shows "ccw a b x"
proof -
  def D\<equiv>C
  have D: "C \<subseteq> D" "\<And>c. c \<in> D \<Longrightarrow> 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 \<subseteq> D" by simp
    {
      assume "C = {}"
      hence ?case
        using insert
        by simp
    } moreover {
      assume "C \<noteq> {}"
      from convex_hull_insert[OF this, of c] insert(6)
      obtain u v d where "u \<ge> 0" "v \<ge> 0" "d \<in> convex hull C" "u + v = 1" and x: "x = u *\<^sub>R c + v *\<^sub>R d"
        by blast
      have "ccw a b d"
        by (auto intro: insert.hyps(3)[OF `C \<subseteq> D`] insert.prems `d \<in> convex hull C`)
      from insert
      have "ccw a b c"
        by simp
      from convex2[OF `0 \<le> u` `0 \<le> 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

