Theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary

section ‹CCW for Arbitrary Points in the Plane›
theory Counterclockwise_2D_Arbitrary
imports Counterclockwise_2D_Strict
begin

subsection ‹Interpretation of Knuth's axioms in the plane›

definition lex::"point  point  bool" where
  "lex p q  (fst p < fst q  fst p = fst q  snd p < snd q  p = q)"

definition psi::"point  point  point  bool" where
  "psi p q r  (lex p q  lex q r)"

definition ccw::"point  point  point  bool" where
  "ccw p q r  ccw' p q r  (det3 p q r = 0  (psi p q r  psi q r p  psi r p q))"

interpretation ccw: linorder_list0 "ccw x" for x .

lemma ccw'_imp_ccw: "ccw' a b c  ccw a b c"
  by (simp add: ccw_def)

lemma ccw_ncoll_imp_ccw: "ccw a b c  ¬coll a b c  ccw' a b c"
  by (simp add: ccw_def)

lemma ccw_translate: "ccw p (p + q) (p + r) = ccw 0 q r"
  by (auto simp: ccw_def psi_def lex_def)

lemma ccw_translate_origin: "NO_MATCH 0 p  ccw p q r = ccw 0 (q - p) (r - p)"
  using ccw_translate[of p "q - p" "r - p"]
  by simp

lemma psi_scale:
  "psi (r *R a) (r *R b) 0 = (if r > 0 then psi a b 0 else if r < 0 then psi 0 b a else True)"
  "psi (r *R a) 0 (r *R b) = (if r > 0 then psi a 0 b else if r < 0 then psi b 0 a else True)"
  "psi 0 (r *R a) (r *R b) = (if r > 0 then psi 0 a b else if r < 0 then psi b a 0 else True)"
  by (auto simp: psi_def lex_def det3_def' not_less algebra_split_simps)

lemma ccw_scale23: "ccw 0 a b  r > 0  ccw 0 (r *R a) (r *R b)"
  by (auto simp: ccw_def psi_scale)

lemma psi_notI: "distinct3 p q r  psi p q r  ¬ psi q p r"
  by (auto simp: algebra_simps psi_def lex_def)

lemma not_lex_eq: "¬ lex a b  lex b a  b  a"
  by (auto simp: algebra_simps lex_def prod_eq_iff)

lemma lex_trans: "lex a b  lex b c  lex a c"
  by (auto simp: lex_def)

lemma lex_sym_eqI: "lex a b  lex b a  a = b"
  and lex_sym_eq_iff: "lex a b  lex b a  a = b"
  by (auto simp: lex_def)

lemma lex_refl[simp]: "lex p p"
  by (metis not_lex_eq)

lemma psi_disjuncts:
  "distinct3 p q r  psi p q r  psi p r q  psi q r p  psi q p r  psi r p q  psi r q p"
  by (auto simp: psi_def not_lex_eq)

lemma nlex_ccw_left: "lex x 0  ccw 0 (0, 1) x"
  by (auto simp: ccw_def lex_def psi_def ccw'_def det3_def')

interpretation ccw_system123 ccw
  apply unfold_locales
  subgoal by (force simp: ccw_def ccw'_def det3_def' algebra_simps)
  subgoal by (force simp: ccw_def ccw'_def det3_def' psi_def algebra_simps lex_sym_eq_iff)
  subgoal by (drule psi_disjuncts) (force simp: ccw_def ccw'_def det3_def' algebra_simps)
  done

lemma lex_scaleR_nonneg: "lex a b  r  0  lex a (a + r *R (b - a))"
  by (auto simp: lex_def)

lemma lex_scale1_zero:
    "lex (v *R u) 0 = (if v > 0 then lex u 0 else if v < 0 then lex 0 u else True)"
  and lex_scale2_zero:
    "lex 0 (v *R u) = (if v > 0 then lex 0 u else if v < 0 then lex u 0 else True)"
  by (auto simp: lex_def prod_eq_iff less_eq_prod_def algebra_split_simps)

lemma nlex_add:
  assumes "lex a 0" "lex b 0"
  shows "lex (a + b) 0"
  using assms by (auto simp: lex_def)

lemma nlex_sum:
  assumes "finite X"
  assumes "x. x  X  lex (f x) 0"
  shows "lex (sum f X) 0"
  using assms
  by induction (auto intro!: nlex_add)

lemma abs_add_nlex:
  assumes "coll 0 a b"
  assumes "lex a 0"
  assumes "lex b 0"
  shows "abs (a + b) = abs a + abs b"
proof (rule antisym[OF abs_triangle_ineq])
  have "fst (¦a¦ + ¦b¦)  fst ¦a + b¦"
    using assms
    by (auto simp add: det3_def' abs_prod_def lex_def)
  moreover
  {
    assume H: "fst a < 0" "fst b < 0"
    hence "snd b  0  snd a  0"
      using assms
      by (auto simp: lex_def det3_def' mult.commute)
        (metis mult_le_cancel_left_neg mult_zero_right)+
    hence "¦snd a¦ + ¦snd b¦  ¦snd a + snd b¦"
      using H by auto
  } hence "snd (¦a¦ + ¦b¦)  snd ¦a + b¦"
    using assms
    by (auto simp add: det3_def' abs_prod_def lex_def)
  ultimately
  show "¦a¦ + ¦b¦  ¦a + b¦" unfolding less_eq_prod_def ..
qed

lemma lex_sum_list: "(x. x  set xs  lex x 0)  lex (sum_list xs) 0"
  by (induct xs) (auto simp: nlex_add)

lemma
  abs_sum_list_coll:
  assumes coll: "list_all (coll 0 x) xs"
  assumes "x  0"
  assumes up: "list_all (λx. lex x 0) xs"
  shows "abs (sum_list xs) = sum_list (map abs xs)"
  using assms
proof (induct xs)
  case (Cons y ys)
  hence "coll 0 x y" "coll 0 x (sum_list ys)"
    by (auto simp: list_all_iff intro!: coll_sum_list)
  hence "coll 0 y (sum_list ys)" using x  0
    by (rule coll_trans)
  hence "¦y + sum_list ys¦ = abs y + abs (sum_list ys)" using Cons
    by (subst abs_add_nlex) (auto simp: list_all_iff lex_sum_list)
  thus ?case using Cons by simp
qed simp

lemma lex_diff1: "lex (a - b) c = lex a (c + b)"
  and lex_diff2: "lex c (a - b) = lex (c + b) a"
  by (auto simp: lex_def)

lemma sum_list_eq_0_iff_nonpos:
  fixes xs::"'a::ordered_ab_group_add list"
  shows "list_all (λx. x  0) xs  sum_list xs = 0  (nset xs. n = 0)"
  by (auto simp: list_all_iff sum_list_sum_nth sum_nonpos_eq_0_iff)
    (auto simp add: in_set_conv_nth)

lemma sum_list_nlex_eq_zeroI:
  assumes nlex: "list_all (λx. lex x 0) xs"
  assumes "sum_list xs = 0"
  assumes "x  set xs"
  shows "x = 0"
proof -
  from assms(2) have z1: "sum_list (map fst xs) = 0" and z2: "sum_list (map snd xs) = 0"
    by (auto simp: prod_eq_iff fst_sum_list snd_sum_list)
  from nlex have "list_all (λx. x  0) (map fst xs)"
    by (auto simp: lex_def list_all_iff)
  from sum_list_eq_0_iff_nonpos[OF this] z1 nlex
  have
    z1': "list_all (λx. x = 0) (map fst xs)"
    and "list_all (λx. x  0) (map snd xs)"
    by (auto simp: list_all_iff lex_def)
  from sum_list_eq_0_iff_nonpos[OF this(2)] z2
  have "list_all (λx. x = 0) (map snd xs)" by (simp add: list_all_iff)
  with z1' show "x = 0" by (auto simp: list_all_iff zero_prod_def assms prod_eq_iff)
qed

lemma sum_list_eq0I: "(xset xs. x = 0)  sum_list xs = 0"
  by (induct xs) auto

lemma sum_list_nlex_eq_zero_iff:
  assumes nlex: "list_all (λx. lex x 0) xs"
  shows "sum_list xs = 0  list_all ((=) 0) xs"
  using assms
  by (auto intro: sum_list_nlex_eq_zeroI sum_list_eq0I simp: list_all_iff)

lemma
  assumes "lex p q" "lex q r" "0  a" "0  b" "0  c" "a + b + c = 1"
  assumes comb_def: "comb = a *R p + b *R q + c *R r"
  shows lex_convex3: "lex p comb" "lex comb r"
proof -
  from convex3_alt[OF assms(3-6), of p q r]
  obtain u v where
    uv: "a *R p + b *R q + c *R r = p + u *R (q - p) + v *R (r - p)" "0  u" "0  v" "u + v  1" .
  have "lex p r"
    using assms by (metis lex_trans)
  hence "lex (v *R (p - r)) 0" using uv
    by (simp add: lex_scale1_zero lex_diff1)
  also
  have "lex 0 (u *R (q - p))" using lex p q uv
    by (simp add: lex_scale2_zero lex_diff2)
  finally (lex_trans)
  show "lex p comb"
    unfolding comb_def uv
    by (simp add: lex_def prod_eq_iff algebra_simps)
  from comb_def have comb_def': "comb = c *R r + b *R q + a *R p" by simp
  from assms have "c + b + a = 1" by simp
  from convex3_alt[OF assms(5,4,3) this, of r q p]
  obtain u v where uv: "c *R r + b *R q + a *R p = r + u *R (q - r) + v *R (p - r)"
    "0  u" "0  v" "u + v  1"
    by auto
  have "lex (u *R (q - r)) 0"
    using uv lex q r
    by (simp add: lex_scale1_zero lex_diff1)
  also have "lex 0  (v *R (r - p))"
    using uv lex p r
    by (simp add: lex_scale2_zero lex_diff2)
  finally (lex_trans) show "lex comb r"
    unfolding comb_def' uv
    by (simp add: lex_def prod_eq_iff algebra_simps)
qed

lemma lex_convex_self2:
  assumes "lex p q" "0  a" "a  1"
  defines "r  a *R p + (1 - a) *R q"
  shows "lex p r" (is ?th1)
    and "lex r q" (is ?th2)
  using lex_convex3[OF lex p q, of q a "1 - a" 0 r]
      assms
  by (simp_all add: r_def)

lemma lex_uminus0[simp]: "lex (-a) 0 = lex 0 a"
  by (auto simp: lex_def)

lemma
  lex_fst_zero_imp:
  "fst x = 0  lex x 0  lex y 0  ¬coll 0 x y  ccw' 0 y x"
  by (auto simp: ccw'_def det3_def' lex_def algebra_split_simps)

lemma lex_ccw_left: "lex x y  r > 0  ccw y (y + (0, r)) x"
  by (auto simp: ccw_def ccw'_def det3_def' algebra_simps lex_def psi_def)

lemma lex_translate_origin: "NO_MATCH 0 a  lex a b = lex 0 (b - a)"
  by (auto simp: lex_def)


subsection ‹Order prover setup›

definition "lexs p q  (lex p q  p  q)"

lemma lexs_irrefl: "¬ lexs p p"
  and lexs_imp_lex: "lexs x y  lex x y"
  and not_lexs: "(¬ lexs x y) = (lex y x)"
  and not_lex: "(¬ lex x y) = (lexs y x)"
  and eq_lex_refl: "x = y  lex x y"
  by (auto simp: lexs_def lex_def prod_eq_iff)

lemma lexs_trans: "lexs x y  lexs y z  lexs x z"
  and lexs_lex_trans: "lexs x y  lex y z  lexs x z"
  and lex_lexs_trans: "lex x y  lexs y z  lexs x z"
  and lex_neq_trans: "lex a b  a  b  lexs a b"
  and neq_lex_trans: "a  b  lex a b  lexs a b"
  and lexs_imp_neq: "lexs a b  a  b"
  by (auto simp: lexs_def lex_def prod_eq_iff)

local_setup HOL_Order_Tac.declare_linorder {
    ops = {eq = @{term (=) :: point  point  bool}, le = @{term lex}, lt = @{term lexs}},
    thms = {trans = @{thm lex_trans}, refl = @{thm lex_refl}, eqD1 = @{thm eq_lex_refl},
            eqD2 = @{thm eq_lex_refl[OF sym]}, antisym = @{thm lex_sym_eqI}, contr = @{thm notE}},
    conv_thms = {less_le = @{thm eq_reflection[OF lexs_def]},
                 nless_le = @{thm eq_reflection[OF not_lexs]},
                 nle_le = @{thm eq_reflection[OF not_lex_eq]}}
  }

subsection ‹Contradictions›

lemma
  assumes d: "distinct4 s p q r"
  shows contra1: "¬(lex p q  lex q r  lex r s  indelta s p q r)" (is ?th1)
    and contra2: "¬(lex s p  lex p q  lex q r  indelta s p q r)" (is ?th2)
    and contra3: "¬(lex p r  lex p s  lex q r  lex q s  insquare p r q s)" (is ?th3)
proof -
  {
    assume "det3 s p q = 0" "det3 s q r = 0" "det3 s r p = 0" "det3 p q r = 0"
    hence ?th1 ?th2 ?th3 using d
      by (auto simp add: det3_def' ccw'_def ccw_def psi_def algebra_simps)
  } moreover {
    assume *: "¬(det3 s p q = 0  det3 s q r = 0  det3 s r p = 0  det3 p q r = 0)"
    {
      assume d0: "det3 p q r = 0"
      with d have "?th1  ?th2"
        by (force simp add: det3_def' ccw'_def ccw_def psi_def algebra_simps)
    } moreover {
      assume dp: "det3 p q r  0"
      have "?th1  ?th2"
        unfolding de_Morgan_disj[symmetric]
      proof (rule notI, goal_cases)
        case prems: 1
        hence **: "indelta s p q r" by auto
        hence nonnegs: "det3 p q r  0" "0  det3 s q r" "0  det3 p s r" "0  det3 p q s"
          by (auto simp: ccw_def ccw'_def det3_def' algebra_simps)
        hence det_pos: "det3 p q r > 0" using dp by simp
        have det_eq: "det3 s q r + det3 p s r + det3 p q s = det3 p q r"
          by (auto simp: ccw_def det3_def' algebra_simps)
        hence det_div_eq:
          "det3 s q r / det3 p q r + det3 p s r / det3 p q r + det3 p q s / det3 p q r = 1"
          using det_pos by (auto simp: field_simps)
        from lex_convex3[OF _ _ _ _ _ det_div_eq convex_comb_dets[OF det_pos, of s]]
        have "lex p s" "lex s r"
          using prems by (auto simp: nonnegs)
        with prems d show False by (simp add: lex_sym_eq_iff)
      qed
    } moreover have ?th3
    proof (safe, goal_cases)
      case prems: 1
      have nonnegs: "det3 p r q  0" "det3 r q s  0" "det3 s p r  0" "det3 q s p  0"
        using prems
        by (auto simp add: ccw_def ccw'_def less_eq_real_def)
      have dets_eq: "det3 p r q + det3 q s p = det3 r q s + det3 s p r"
        by (auto simp: det3_def')
      hence **: "det3 p r q = 0  det3 q s p = 0  det3 r q s = 0  det3 s p r = 0"
        using prems
        by (auto simp: ccw_def ccw'_def)
      moreover
      {
        fix p r q s
        assume det_pos: "det3 p r q > 0"
        assume dets_eq: "det3 p r q + det3 q s p = det3 r q s + det3 s p r"
        assume nonnegs:"det3 r q s  0" "det3 s p r  0" "det3 q s p  0"
        assume g14: "lex p r" "lex p s" "lex q r" "lex q s"
        assume d: "distinct4 s p q r"

        let ?sum = "(det3 p r q + det3 q s p) / det3 p r q"
        have eqs: "det3 s p r = det3 p r s" "det3 r q s = det3 s r q" "det3 q s p = - det3 p s q"
          by (auto simp: det3_def' algebra_simps)
        from convex_comb_dets[OF det_pos, of s]
        have "((det3 p r q / det3 p r q) *R s + (det3 q s p / det3 p r q) *R r) /R ?sum =
            ((det3 r q s / det3 p r q) *R p + (det3 s p r / det3 p r q) *R q) /R ?sum"
          unfolding eqs
          by (simp add: algebra_simps prod_eq_iff)
        hence srpq: "(det3 p r q / det3 p r q / ?sum) *R s + (det3 q s p / det3 p r q / ?sum) *R r =
          (det3 r q s / det3 p r q / ?sum) *R p + (det3 s p r / det3 p r q  / ?sum) *R q"
          (is "?s *R s + ?r *R r = ?p *R p + ?q *R q")
          using det_pos
          by (simp add: algebra_simps inverse_eq_divide)
        have eqs: "?s + ?r = 1" "?p + ?q = 1"
          and s: "?s  0" "?s  1"
          and r: "?r  0" "?r  1"
          and p: "?p  0" "?p  1"
          and q: "?q  0" "?q  1"
          unfolding add_divide_distrib[symmetric]
          using det_pos nonnegs dets_eq
          by (auto)
        from eqs have eqs': "1 - ?s = ?r" "1 - ?r = ?s" "1 - ?p = ?q" "1 - ?q = ?p"
          by auto
        have comm: "?r *R r + ?s *R s = ?s *R s + ?r *R r"
          "?q *R q + ?p *R p = ?p *R p + ?q *R q"
          by simp_all
        define K
          where "K = (det3 r q s / det3 p r q / ?sum) *R p + (det3 s p r / det3 p r q  / ?sum) *R q"
        note rewrs = eqs' comm srpq K_def[symmetric]
        from lex_convex_self2[OF _ s, of s r, unfolded rewrs]
           lex_convex_self2[OF _ r, of r s, unfolded rewrs]
           lex_convex_self2[OF _ p, of p q, unfolded rewrs]
           lex_convex_self2[OF _ q, of q p, unfolded rewrs]
        have False using g14 d det_pos
          by (metis lex_trans not_lex_eq)
      } note wlog = this
      from dets_eq have 1: "det3 q s p + det3 p r q = det3 s p r + det3 r q s"
        by simp
      from d have d': "distinct4 r q p s" by auto
      note wlog[of q s p r, OF _ 1 nonnegs(3,2,1) prems(4,3,2,1) d']
        wlog[of p r q s, OF _ dets_eq nonnegs(2,3,4) prems(1-4) d]
      ultimately show False using nonnegs d *
        by (auto simp: less_eq_real_def det3_def' algebra_simps)
    qed
    ultimately have ?th1 ?th2 ?th3 by blast+
  } ultimately show ?th1 ?th2 ?th3 by force+
qed

lemma ccw'_subst_psi_disj:
  assumes "det3 t r s = 0"
  assumes "psi t r s  psi t s r  psi s r t"
  assumes "s  t"
  assumes "ccw' t r p"
  shows "ccw' t s p"
proof cases
  assume "r  s"
  from assms have "r  t" by (auto simp: det3_def' ccw'_def algebra_simps)
  from assms have "det3 r s t = 0"
    by (auto simp: algebra_simps det3_def')
  from coll_ex_scaling[OF assms(3) this]
  obtain x where s: "r = s + x *R (t - s)" by auto
  from assms(4)[simplified s]
  have "0 < det3 0 (s + x *R (t - s) - t) (p - t)"
    by (auto simp: algebra_simps det3_def' ccw'_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 neq: "x  1" by (auto simp add: det3_def' ccw'_def)
  have tr: "fst s < fst r  fst t = fst s  snd t  snd r"
    by (simp add: s)
  from s have "fst (r - s) = fst (x *R (t - s))" "snd (r - s) = snd (x *R (t - s))"
    by auto
  hence "x = (if fst (t - s) = 0 then snd (r - s) / snd (t - s) else fst (r - s) / fst (t - s))"
    using s  t
    by (auto simp add: field_simps prod_eq_iff)
  also have "  1"
    using assms
    by (auto simp: lex_def psi_def tr)
  finally have "x < 1" using neq by simp
  thus ?thesis using ccw'
    by (auto simp: ccw'.translate_origin)
qed (insert assms, simp)

lemma lex_contr:
  assumes "distinct4 t s q r"
  assumes "lex t s" "lex s r"
  assumes "det3 t s r = 0"
  assumes "ccw' t s q"
  assumes "ccw' t q r"
  shows "False"
  using ccw'_subst_psi_disj[of t s r q] assms
  by (cases "r = t") (auto simp: det3_def' algebra_simps psi_def ccw'_def)

lemma contra4:
  assumes "distinct4 s r q p"
  assumes lex: "lex q p" "lex p r" "lex r s"
  assumes ccw: "ccw r q s" "ccw r s p" "ccw r q p"
  shows False
proof cases
  assume c: "ccw s q p"
  from c have *: "indelta s r q p"
    using assms by simp
  with contra1[OF assms(1)]
  have "¬ (lex r q  lex q p  lex p s)" by blast
  hence "¬ lex q p"
    using ccw s q p contra1 cyclic assms nondegenerate by blast
  thus False using assms by simp
next
  assume "¬ ccw s q p"
  with ccw have "ccw q s p  ccw s p r  ccw p r q  ccw r q s"
    by (metis assms(1) ccw'.cyclic ccw_def not_ccw'_eq psi_disjuncts)
  moreover
  from lex have "lex q r" "lex q s" "lex p r" "lex p s" by order+
  ultimately show False using contra3[of r q p s] distinct4 s r q p by blast
qed

lemma not_coll_ordered_lexI:
  assumes "l  x0"
    and "lex x1 r"
    and "lex x1 l"
    and "lex r x0"
    and "lex l x0"
    and "ccw' x0 l x1"
    and "ccw' x0 x1 r"
  shows "det3 x0 l r  0"
proof
  assume "coll x0 l r"
  from coll x0 l r have 1: "coll 0 (l - x0) (r - x0)"
    by (simp add: det3_def' algebra_simps)
  from lex r x0 have 2: "lex (r - x0) 0" by (auto simp add: lex_def)
  from lex l x0 have 3: "lex (l - x0) 0" by (auto simp add: lex_def)
  from ccw' x0 l x1 have 4: "ccw' 0 (l - x0) (x1 - x0)"
    by (simp add: det3_def' ccw'_def algebra_simps)
  from ccw' x0 x1 r have 5: "ccw' 0 (x1 - x0) (r - x0)"
    by (simp add: det3_def' ccw'_def algebra_simps)
  from lex x1 r have 6: "lex 0 (r - x0 - (x1 - x0))" by (auto simp: lex_def)
  from lex x1 l have 7: "lex 0 (l - x0 - (x1 - x0))" by (auto simp: lex_def)
  define r' where "r' = r - x0"
  define l' where "l' = l - x0"
  define x0' where "x0' = x1 - x0"
  from 1 2 3 4 5 6 7
  have rs: "coll 0 l' r'" "lex r' 0"
    "lex l' 0"
    "ccw' 0 l' x0'"
    "ccw' 0 x0' r'"
    "lex 0 (r' - x0')"
    "lex 0 (l' - x0')"
    unfolding r'_def[symmetric] l'_def[symmetric] x0'_def[symmetric]
    by auto
  from assms have "l'  0"
    by (auto simp: l'_def)
  from coll_scale[OF coll 0 l' _ this]
  obtain y where y: "r' = y *R l'" by auto
  {
    assume "y > 0"
    with rs have False
      by (auto simp: det3_def' algebra_simps y ccw'_def)
  } moreover {
    assume "y < 0"
    with rs have False
      by (auto simp: lex_def not_less algebra_simps algebra_split_simps y ccw'_def)
  } moreover {
    assume "y = 0"
    from this rs have False
      by (simp add: ccw'_def y)
  } ultimately show False by arith
qed

interpretation ccw_system4 ccw
proof unfold_locales
  fix p q r t
  assume ccw: "ccw t q r" "ccw p t r" "ccw p q t"
  show "ccw p q r"
  proof (cases "det3 t q r = 0  det3 p t r = 0  det3 p q t = 0")
    case True
    {
      assume "psi t q r  psi q r t  psi r t q"
        "psi p t r  psi t r p  psi r p t"
        "psi p q t  psi q t p  psi t p q"
      hence "psi p q r  psi q r p  psi r p q"
        using lex_sym_eq_iff psi_def by blast
    }
    with True ccw show ?thesis
      by (simp add: det3_def' algebra_simps ccw_def ccw'_def)
  next
    case False
    hence "0  det3 t q r" "0  det3 p t r" "0  det3 p q t"
      using ccw by (auto simp: less_eq_real_def ccw_def ccw'_def)
    with False show ?thesis
      by (auto simp: ccw_def det3_def' algebra_simps ccw'_def intro!: disjI1)
  qed
qed

lemma lex_total: "lex t q  t  q  lex q t  t  q  t = q"
  by auto

lemma
  ccw_two_up_contra:
  assumes c: "ccw' t p q" "ccw' t q r"
  assumes ccws: "ccw t s p" "ccw t s q" "ccw t s r" "ccw t p q" "ccw t q r" "ccw t r p"
  assumes distinct: "distinct5 t s p q r"
  shows False
proof -
  from ccws
  have nn: "det3 t s p  0" "det3 t s q  0" "det3 t s r  0" "det3 t r p  0"
    by (auto simp add: less_eq_real_def ccw_def ccw'_def)
  with c det_identity[of t p q s r]
  have tsr: "coll t s r" and tsp: "coll t s p"
    by (auto simp: add_nonneg_eq_0_iff ccw'_def)
  moreover
  have trp: "coll t r p"
    by (metis ccw'_subst_collinear distinct not_ccw'_eq tsr tsp)
  ultimately have tpr: "coll t p r"
    by (auto simp: det3_def' algebra_simps)
  moreover
  have psi: "psi t p r  psi t r p  psi r p t"
    unfolding psi_def
  proof -
    have ntsr: "¬ ccw' t s r" "¬ ccw' t r s"
      using tsr
      by (auto simp: not_ccw'_eq det3_def' algebra_simps)
    have f8: "¬ ccw' t r s"
      using tsr not_ccw'_eq by blast
    have f9: "¬ ccw' t r p"
      using tpr by (simp add: not_ccw'_eq)
    have f10: "(lex t r  lex r p  lex r p  lex p t  lex p t  lex t r)"
      using ccw_def ccws(6) psi_def f9 by auto

    have "¬ ccw' t r q"
      using c(2) not_ccw'_eq by blast
    moreover
    have "¬coll t q s"
      using ntsr ccw'_subst_collinear distinct c(2) by blast
    hence "ccw' t s q"
      by (meson ccw_def ccws(2) not_ccw'_eq)
    moreover
    from tsr tsp coll t r p have "coll t p s" "coll t p r" "coll t r s"
      by (auto simp add: det3_def' algebra_simps)
    ultimately
    show "lex t p  lex p r  lex t r  lex r p  lex r p  lex p t"
      by (metis ccw'_subst_psi_disj distinct ccw_def ccws(3) contra4 tsp ntsr(1) f10 lex_total
        psi_def trp)
  qed
  moreover
  from distinct have "r  t" by auto
  ultimately
  have "ccw' t r q" using c(1)
    by (rule ccw'_subst_psi_disj)
  thus False
    using c(2) by (simp add: ccw'_contra)
qed

lemma
  ccw_transitive_contr:
  fixes t s p q r
  assumes ccws: "ccw t s p" "ccw t s q" "ccw t s r" "ccw t p q" "ccw t q r" "ccw t r p"
  assumes distinct: "distinct5 t s p q r"
  shows False
proof -
  from ccws distinct have *: "ccw p t r" "ccw p q t" by (metis cyclic)+
  with distinct have "ccw r p q" using interior[OF _ _ ccws(5) *, of UNIV]
    by (auto intro: cyclic)

  from ccws have nonnegs: "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 r p  0"
    by (auto simp add: less_eq_real_def ccw_def ccw'_def)
  {
    assume "ccw' t p q" "ccw' t q r" "ccw' t r p"
    hence False
      using ccw_two_up_contra ccws distinct by blast
  } moreover {
    assume c: "coll t q r" "coll t r p"
    with distinct four_points_aligned(1)[OF c, of s]
    have "coll t p q"
      by auto
    hence "(psi t p q  psi p q t  psi q t p)"
      "psi t q r  psi q r t  psi r t q"
      "psi t r p  psi r p t  psi p t r"
      using ccws(4,5,6) c
      by (simp_all add: ccw_def ccw'_def)
    hence False
      using distinct
      by (auto simp: psi_def ccw'_def)
  } moreover {
    assume c: "det3 t p q = 0" "det3 t q r > 0" "det3 t r p = 0"
    have "x. det3 t q r = 0  t = x  r = q  q = x  r = p  p = x  r = x"
      by (meson c(1) c(3) distinct four_points_aligned(1))
    hence False
      by (metis (full_types) c(2) distinct less_irrefl)
  } moreover {
    assume c: "det3 t p q = 0" "det3 t q r = 0" "det3 t r p > 0"
    have "x. det3 t r p = 0  t = x  r = x  q = x  p = x"
      by (meson c(1) c(2) distinct four_points_aligned(1))
    hence False
      by (metis (no_types) c(3) distinct less_numeral_extra(3))
  } moreover {
    assume c: "ccw' t p q" "ccw' t q r"
    from ccw_two_up_contra[OF this ccws distinct]
    have False .
  } moreover {
    assume c: "ccw' t p q" "ccw' t r p"
    from ccw_two_up_contra[OF this(2,1), of s] ccws distinct
    have False by auto
  } moreover {
    assume c: "ccw' t q r" "ccw' t r p"
    from ccw_two_up_contra[OF this, of s] ccws distinct
    have False by auto
  } ultimately show "False"
    using 0  det3 t p q
    0  det3 t q r0  det3 t r p
    by (auto simp: less_eq_real_def ccw'_def)
qed

interpretation ccw: ccw_system ccw
  by unfold_locales (metis ccw_transitive_contr nondegenerate)

lemma ccw_scaleR1:
  "det3 0 xr P  0  0 < e  ccw 0 xr P  ccw 0 (e*Rxr) P"
  by (simp add: ccw_def)

lemma ccw_scaleR2:
  "det3 0 xr P  0  0 < e  ccw 0 xr P  ccw 0 xr (e*RP)"
  by (simp add: ccw_def)

lemma ccw_translate3_aux:
  assumes "¬coll 0 a b"
  assumes "x < 1"
  assumes "ccw 0 (a - x*Ra) (b - x *R a)"
  shows "ccw 0 a b"
proof -
  from assms have "¬ coll 0 (a - x*Ra) (b - x *R a)"
    by simp
  with assms have "ccw' 0 ((1 - x) *R a) (b - x *R a)"
    by (simp add: algebra_simps ccw_def)
  thus "ccw 0 a b"
    using x < 1
    by (simp add: ccw_def)
qed

lemma ccw_translate3_minus: "det3 0 a b  0  x < 1  ccw 0 a (b - x *R a)  ccw 0 a b"
  using ccw_translate3_aux[of a b x] ccw_scaleR1[of a "b - x *R a" "1-x" ]
  by (auto simp add: algebra_simps)

lemma ccw_translate3: "det3 0 a b  0  x < 1  ccw 0 a b  ccw 0 a (x *R a + b)"
  by (rule ccw_translate3_minus) (auto simp add: algebra_simps)

lemma ccw_switch23: "det3 0 P Q  0  (¬ ccw 0 Q P  ccw 0 P Q)"
  by (auto simp: ccw_def algebra_simps not_ccw'_eq ccw'_not_coll)

lemma ccw0_upward: "fst a > 0  snd a = 0  snd b > snd a  ccw 0 a b"
  by (auto simp: ccw_def det3_def' algebra_simps ccw'_def)

lemma ccw_uminus3[simp]: "det3 a b c  0  ccw (-a) (-b) (-c) = ccw a b c"
  by (auto simp: ccw_def ccw'_def algebra_simps det3_def')

lemma coll_minus_eq: "coll (x - a) (x - b) (x - c) = coll a b c"
  by (auto simp: det3_def' algebra_simps)

lemma ccw_minus3: "¬ coll a b c  ccw (x - a) (x - b) (x - c)  ccw a b c"
  by (simp add: ccw_def coll_minus_eq)

lemma ccw0_uminus[simp]: "¬ coll 0 a b  ccw 0 (-a) (-b)  ccw 0 a b"
  using ccw_uminus3[of 0 a b]
  by simp

lemma lex_convex2:
  assumes "lex p q" "lex p r" "0  u" "u  1"
  shows "lex p (u *R q + (1 - u) *R r)"
proof cases
  note lex p q
  also
  assume "lex q r"
  hence "lex q (u *R q + (1 - u) *R r)"
    using 0  u u  1
    by (rule lex_convex_self2)
  finally (lex_trans) show ?thesis .
next
  note lex p r
  also
  assume "¬ lex q r"
  hence "lex r q"
    by simp
  hence "lex r ((1 - u) *R r + (1 - (1 - u)) *R q)"
    using 0  u u  1
    by (intro lex_convex_self2) simp_all
  finally (lex_trans) show ?thesis by (simp add: ac_simps)
qed

lemma lex_convex2':
  assumes "lex q p" "lex r p" "0  u" "u  1"
  shows "lex (u *R q + (1 - u) *R r) p"
proof -
  have "lex (- p) (u *R (-q) + (1 - u) *R (-r))"
    using assms
    by (intro lex_convex2) (auto simp: lex_def)
  thus ?thesis
    by (auto simp: lex_def algebra_simps)
qed

lemma psi_convex1:
  assumes "psi c a b"
  assumes "psi d a b"
  assumes "0  u" "0  v" "u + v = 1"
  shows "psi (u *R c + v *R d) a b"
proof -
  from assms have v: "v = (1 - u)" by simp
  show ?thesis
    using assms
    by (auto simp: psi_def v intro!: lex_convex2' lex_convex2)
qed

lemma psi_convex2:
  assumes "psi a c b"
  assumes "psi a d b"
  assumes "0  u" "0  v" "u + v = 1"
  shows "psi a (u *R c + v *R d) b"
proof -
  from assms have v: "v = (1 - u)" by simp
  show ?thesis
    using assms
    by (auto simp: psi_def v intro!: lex_convex2' lex_convex2)
qed

lemma psi_convex3:
  assumes "psi a b c"
  assumes "psi a b d"
  assumes "0  u" "0  v" "u + v = 1"
  shows "psi a b (u *R c + v *R d)"
proof -
  from assms have v: "v = (1 - u)" by simp
  show ?thesis
    using assms
    by (auto simp: psi_def v intro!: lex_convex2)
qed

lemma coll_convex:
  assumes "coll a b c" "coll a b d"
  assumes "0  u" "0  v" "u + v = 1"
  shows "coll a b (u *R c + v *R d)"
proof cases
  assume "a  b"
  with assms(1, 2)
  obtain x y where xy: "c - a = x *R (b - a)" "d - a = y *R (b - a)"
    by (auto simp: det3_translate_origin dest!: coll_scale)
  from assms have "(u + v) *R a = a" by simp
  hence "u *R c + v *R d - a = u *R (c - a) + v *R (d - a)"
    by (simp add: algebra_simps)
  also have " = u *R x *R (b - a) + v *R y *R (b - a)"
    by (simp add: xy)
  also have " = (u * x + v * y) *R (b - a)" by (simp add: algebra_simps)
  also have "coll 0 (b - a) "
    by (simp add: coll_scaleR_right_eq)
  finally show ?thesis
    by (auto simp: det3_translate_origin)
qed simp

lemma (in ccw_vector_space) convex3:
  assumes "u  0" "v  0" "u + v = 1" "ccw a b d" "ccw a b c"
  shows "ccw a b (u *R c + v *R d)"
proof -
  have "v = 1 - u" using assms by simp
  hence "ccw 0 (b - a) (u *R (c - a) + v *R (d - a))"
    using assms
    by (cases "u = 0" "v = 0" rule: bool.exhaust[case_product bool.exhaust])
      (auto simp add: translate_origin intro!: add3)
  also
  have "(u + v) *R a = a" by (simp add: assms)
  hence "u *R (c - a) + v *R (d - a) = u *R c + v *R d - a"
    by (auto simp: algebra_simps)
  finally show ?thesis by (simp add: translate_origin)
qed

lemma ccw_self[simp]: "ccw a a b" "ccw b a a"
  by (auto simp: ccw_def psi_def intro: cyclic)

lemma ccw_sefl'[simp]: "ccw a b a"
  by (rule cyclic) simp

lemma ccw_convex':
  assumes uv: "u  0" "v  0" "u + v = 1"
  assumes "ccw a b c" and 1: "coll a b c"
  assumes "ccw a b d" and 2: "¬ coll a b d"
  shows "ccw a b (u *R c + v *R d)"
proof -
  from assms have u: "0  u" "u  1" and v: "v = 1 - u"
    by (auto simp: algebra_simps)
  let ?c = "u *R c + v *R d"
  from 1 have abd: "ccw' a b d"
    using assms by (auto simp: ccw_def)
  {
    assume 2: "¬ coll a b c"
    from 2 have "ccw' a b c"
      using assms by (auto simp: ccw_def)
    with abd have "ccw' a b ?c"
      using assms by (auto intro!: ccw'.convex3)
    hence ?thesis
      by (simp add: ccw_def)
  } moreover {
    assume 2: "coll a b c"
    {
      assume "a = b"
      hence ?thesis by simp
    } moreover {
      assume "v = 0"
      hence ?thesis
        by (auto simp: v assms)
    } moreover {
      assume "v  0" "a  b"
      have "coll c a b" using 2 by (auto simp: det3_def' algebra_simps)
      from coll_ex_scaling[OF a  b this]
      obtain r where c: "c = a + r *R (b - a)" by auto
      have *: "u *R (a + r *R (b - a)) + v *R d - a = (u * r) *R (b - a)  + (1 - u) *R (d - a)"
        by (auto simp: algebra_simps v)
      have "ccw' a b ?c"
        using v  0 uv abd
        by (simp add: ccw'.translate_origin c *)
      hence ?thesis by (simp add: ccw_def)
    } ultimately have ?thesis by blast
  } ultimately show ?thesis by blast
qed

lemma ccw_convex:
  assumes uv: "u  0" "v  0" "u + v = 1"
  assumes "ccw a b c"
  assumes "ccw a b d"
  assumes lex: "coll a b c  coll a b d  lex b a"
  shows "ccw a b (u *R c + v *R d)"
proof -
  from assms have u: "0  u" "u  1" and v: "v = 1 - u"
    by (auto simp: algebra_simps)
  let ?c = "u *R c + v *R d"
  {
    assume coll: "coll a b c  coll a b d"
    hence "coll a b ?c"
      by (auto intro!: coll_convex assms)
    moreover
    from coll have "psi a b c  psi b c a  psi c a b" "psi a b d  psi b d a  psi d a b"
      using assms by (auto simp add: ccw_def ccw'_not_coll)
    hence "psi a b ?c  psi b ?c a  psi ?c a b"
      using coll uv lex
      by (auto simp: psi_def ccw_def not_lex lexs_def v intro: lex_convex2 lex_convex2')
    ultimately have ?thesis
      by (simp add: ccw_def)
  } moreover {
    assume 1: "¬ coll a b d" and 2: "¬ coll a b c"
    from 1 have abd: "ccw' a b d"
      using assms by (auto simp: ccw_def)
    from 2 have "ccw' a b c"
      using assms by (auto simp: ccw_def)
    with abd have "ccw' a b ?c"
      using assms by (auto intro!: ccw'.convex3)
    hence ?thesis
      by (simp add: ccw_def)
  } moreover {
    assume "¬ coll a b d" "coll a b c"
    have ?thesis
      by (rule ccw_convex') fact+
  } moreover {
    assume 1: "coll a b d" and 2: "¬ coll a b c"
    have "0  1 - u" using assms by (auto )
    from ccw_convex'[OF this 0  u _ ccw a b d 1 ccw a b c 2]
    have ?thesis by (simp add: algebra_simps v)
  } ultimately show ?thesis by blast
qed

interpretation ccw: ccw_convex ccw S "λa b. lex b a" for S
  by unfold_locales (rule ccw_convex)

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 ccw_scale23 elim!: ccw.sortedP_Cons simp del: scaleR_Pair)

lemma ccw_sorted_implies_ccw'_sortedP:
  assumes nonaligned: "y z. y  set Ps  z  set Ps  y  z  ¬ coll 0 y z"
  assumes sorted: "linorder_list0.sortedP (ccw 0) Ps"
  assumes "distinct Ps"
  shows "linorder_list0.sortedP (ccw' 0 ) Ps"
  using assms
proof (induction Ps)
  case (Cons P Ps)
  {
    fix p assume p: "p  set Ps"
    moreover
    from p Cons.prems have "ccw 0 P p"
      by (auto elim!: linorder_list0.sortedP_Cons intro: Cons)
    ultimately
    have "ccw' 0 P p"
      using distinct (P#Ps)
      by (intro ccw_ncoll_imp_ccw Cons) auto
  }
  moreover
  have "linorder_list0.sortedP (ccw' 0) Ps"
    using Cons.prems
    by (intro Cons) (auto elim!: linorder_list0.sortedP_Cons intro: Cons)
  ultimately
  show ?case
    by (auto intro!: linorder_list0.Cons )
qed (auto intro: linorder_list0.Nil)

end