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 ⟷ (∀n∈set 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: "(∀x∈set 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 r›‹0 ≤ 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