Theory Affine_Arithmetic.Intersection

section ‹Intersection›
theory Intersection
imports
  "HOL-Library.Monad_Syntax"
  Polygon
  Counterclockwise_2D_Arbitrary
  Affine_Form
begin
text ‹\label{sec:intersection}›

subsection ‹Polygons and @{term ccw}, @{term lex}, @{term psi}, @{term coll}›

lemma polychain_of_ccw_conjunction:
  assumes sorted: "ccw'.sortedP 0 Ps"
  assumes z: "z ∈ set (polychain_of Pc Ps)"
  shows "list_all (λ(xi, xj). ccw xi xj (fst z) ∧ ccw xi xj (snd z)) (polychain_of Pc Ps)"
  using assms
proof (induction Ps arbitrary: Pc z rule: list.induct)
  case (Cons P Ps)
  {
    assume "set Ps = {}"
    hence ?case using Cons by simp
  } moreover {
    assume "set Ps ≠ {}"
    hence "Ps ≠ []" by simp
    {
      fix a assume "a ∈ set Ps"
      hence "ccw' 0 P a"
        using Cons.prems
        by (auto elim!: linorder_list0.sortedP_Cons)
    } note ccw' = this
    have sorted': "linorder_list0.sortedP (ccw' 0) Ps"
      using Cons.prems
      by (auto elim!: linorder_list0.sortedP_Cons)
    from in_set_polychain_of_imp_sum_list[OF Cons(3)]
    obtain d
    where d: "z = (Pc + sum_list (take d (P # Ps)), Pc + sum_list (take (Suc d) (P # Ps)))" .

    from Cons(3)
    have disj: "z = (Pc, Pc + P) ∨ z ∈ set (polychain_of (Pc + P) Ps)"
      by auto

    let ?th = "λ(xi, xj). ccw xi xj Pc ∧ ccw xi xj (Pc + P)"
    have la: "list_all ?th (polychain_of (Pc + P) Ps)"
    proof (rule list_allI)
      fix x assume x: "x ∈ set (polychain_of (Pc + P) Ps)"
      from in_set_polychain_of_imp_sum_list[OF this]
      obtain e where e: "x = (Pc + P + sum_list (take e Ps), Pc + P + sum_list (take (Suc e) Ps))"
        by auto
      {
        assume "e ≥ length Ps"
        hence "?th x" by (auto simp: e)
      } moreover {
        assume "e < length Ps"
        have 0: "⋀e. e < length Ps ⟹ ccw' 0 P (Ps ! e)"
          by (rule ccw') simp
        have 2: "0 < e ⟹ ccw' 0 (P + sum_list (take e Ps)) (Ps ! e)"
          using ‹e < length Ps›
          by (auto intro!: ccw'.add1 0 ccw'.sum2 sorted' ccw'.sorted_nth_less
            simp: sum_list_sum_nth)
        have "ccw Pc (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps))"
          by (cases "e = 0")
            (auto simp add: ccw_translate_origin take_Suc_eq add.assoc[symmetric] 0 2
              intro!: ccw'_imp_ccw intro: cyclic)
        hence "ccw (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps)) Pc"
          by (rule cyclic)
        moreover
        have "0 < e ⟹ ccw 0 (Ps ! e) (- sum_list (take e Ps))"
          using ‹e < length Ps›
          by (auto simp add: take_Suc_eq add.assoc[symmetric]
              sum_list_sum_nth
            intro!: ccw'_imp_ccw ccw'.sum2 sorted' ccw'.sorted_nth_less)
        hence "ccw (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps)) (Pc + P)"
          by (cases "e = 0") (simp_all add: ccw_translate_origin take_Suc_eq)
        ultimately have "?th x"
          by (auto simp add: e)
      } ultimately show "?th x" by arith
    qed
    from disj have ?case
    proof
      assume z: "z ∈ set (polychain_of (Pc + P) Ps)"
      have "ccw 0 P (sum_list (take d (P # Ps)))"
      proof (cases d)
        case (Suc e) note e = this
        show ?thesis
        proof (cases e)
          case (Suc f)
          have "ccw 0 P (P + sum_list (take (Suc f) Ps))"
            using z
            by (force simp add: sum_list_sum_nth intro!: ccw'.sum intro: ccw' ccw'_imp_ccw)
          thus ?thesis
            by (simp add: e Suc)
        qed (simp add: e)
      qed simp
      hence "ccw Pc (Pc + P) (fst z)"
        by (simp add: d ccw_translate_origin)
      moreover
      from z have "ccw 0 P (P + sum_list (take d Ps))"
        by (cases d, force)
          (force simp add: sum_list_sum_nth intro!: ccw'_imp_ccw ccw'.sum intro: ccw')+
      hence "ccw Pc (Pc + P) (snd z)"
        by (simp add: d ccw_translate_origin)
      moreover
      from z Cons.prems have "list_all (λ(xi, xj). ccw xi xj (fst z) ∧ ccw xi xj (snd z))
        (polychain_of (Pc + P) Ps)"
        by (intro Cons.IH) (auto elim!: linorder_list0.sortedP_Cons)
      ultimately show ?thesis by simp
    qed (simp add: la)
  } ultimately show ?case by blast
qed simp

lemma lex_polychain_of_center:
  "d ∈ set (polychain_of x0 xs) ⟹ list_all (λx. lex x 0) xs ⟹ lex (snd d) x0"
proof (induction xs arbitrary: x0)
  case (Cons x xs) thus ?case
    by (auto simp add: lex_def lex_translate_origin dest!: Cons.IH)
qed (auto simp: lex_translate_origin)

lemma lex_polychain_of_last:
  "(c, d) ∈ set (polychain_of x0 xs) ⟹ list_all (λx. lex x 0) xs ⟹
    lex (snd (last (polychain_of x0 xs))) d"
proof (induction xs arbitrary: x0 c d)
  case (Cons x xs)
  let ?c1 = "c = x0 ∧ d = x0 + x"
  let ?c2 = "(c, d) ∈ set (polychain_of (x0 + x) xs)"
  from Cons(2) have "?c1 ∨ ?c2" by auto
  thus ?case
  proof
    assume ?c1
    with Cons.prems show ?thesis
      by (auto intro!: lex_polychain_of_center)
  next
    assume ?c2
    from Cons.IH[OF this] Cons.prems
    show ?thesis
      by auto
  qed
qed (auto simp: lex_translate_origin)

lemma distinct_fst_polychain_of:
  assumes "list_all (λx. x ≠ 0) xs"
  assumes "list_all (λx. lex x 0) xs"
  shows "distinct (map fst (polychain_of x0 xs))"
  using assms
proof (induction xs arbitrary: x0)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  hence "⋀d. list_all (λx. lex x 0) (x # take d xs)"
    by (auto simp: list_all_iff dest!: in_set_takeD)
  from sum_list_nlex_eq_zero_iff[OF this] Cons.prems
  show ?case
    by (cases "xs = []") (auto intro!: Cons.IH elim!: in_set_polychain_of_imp_sum_list)
qed

lemma distinct_snd_polychain_of:
  assumes "list_all (λx. x ≠ 0) xs"
  assumes "list_all (λx. lex x 0) xs"
  shows "distinct (map snd (polychain_of x0 xs))"
  using assms
proof (induction xs arbitrary: x0)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  have contra:
    "⋀d. xs ≠ [] ⟹ list_all (λx. x ≠ 0) xs ⟹ list_all ((=) 0) (take (Suc d) xs) ⟹ False"
    by (auto simp: neq_Nil_conv)
  from Cons have "⋀d. list_all (λx. lex x 0) (take (Suc d) xs)"
    by (auto simp: list_all_iff dest!: in_set_takeD)
  from sum_list_nlex_eq_zero_iff[OF this] Cons.prems contra
  show ?case
    by (cases "xs = []") (auto intro!: Cons.IH elim!: in_set_polychain_of_imp_sum_list dest!: contra)
qed


subsection ‹Orient all entries›

lift_definition nlex_pdevs::"point pdevs ⇒ point pdevs"
  is "λx n. if lex 0 (x n) then - x n else x n" by simp

lemma pdevs_apply_nlex_pdevs[simp]: "pdevs_apply (nlex_pdevs x) n =
  (if lex 0 (pdevs_apply x n) then - pdevs_apply x n else pdevs_apply x n)"
  by transfer simp

lemma nlex_pdevs_zero_pdevs[simp]: "nlex_pdevs zero_pdevs = zero_pdevs"
  by (auto intro!: pdevs_eqI)

lemma pdevs_domain_nlex_pdevs[simp]: "pdevs_domain (nlex_pdevs x) = pdevs_domain x"
  by (auto simp: pdevs_domain_def)

lemma degree_nlex_pdevs[simp]: "degree (nlex_pdevs x) = degree x"
  by (rule degree_cong) auto

lemma
  pdevs_val_nlex_pdevs:
  assumes "e ∈ UNIV → I" "uminus ` I = I"
  obtains e' where "e' ∈ UNIV → I" "pdevs_val e x = pdevs_val e' (nlex_pdevs x)"
  using assms
  by (atomize_elim, intro exI[where x="λn. if lex 0 (pdevs_apply x n) then - e n else e n"])
    (force simp: pdevs_val_pdevs_domain intro!: sum.cong)

lemma
  pdevs_val_nlex_pdevs2:
  assumes "e ∈ UNIV → I" "uminus ` I = I"
  obtains e' where "e' ∈ UNIV → I" "pdevs_val e (nlex_pdevs x) = pdevs_val e' x"
  using assms
  by (atomize_elim, intro exI[where x="λn. (if lex 0 (pdevs_apply x n) then - e n else e n)"])
    (force simp: pdevs_val_pdevs_domain intro!: sum.cong)

lemma
  pdevs_val_selsort_ccw:
  assumes "distinct xs"
  assumes "e ∈ UNIV → I"
  obtains e' where "e' ∈ UNIV → I"
    "pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (ccw.selsort 0 xs))"
proof -
  have "set xs = set (ccw.selsort 0 xs)" "distinct xs" "distinct (ccw.selsort 0 xs)"
    by (simp_all add: assms)
  from this assms(2) obtain e'
  where "e' ∈ UNIV → I"
    "pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (ccw.selsort 0 xs))"
    by (rule pdevs_val_permute)
  thus thesis ..
qed

lemma
  pdevs_val_selsort_ccw2:
  assumes "distinct xs"
  assumes "e ∈ UNIV → I"
  obtains e' where "e' ∈ UNIV → I"
    "pdevs_val e (pdevs_of_list (ccw.selsort 0 xs)) = pdevs_val e' (pdevs_of_list xs)"
proof -
  have "set (ccw.selsort 0 xs) = set xs" "distinct (ccw.selsort 0 xs)" "distinct xs"
    by (simp_all add: assms)
  from this assms(2) obtain e'
  where "e' ∈ UNIV → I"
    "pdevs_val e (pdevs_of_list (ccw.selsort 0 xs)) = pdevs_val e' (pdevs_of_list xs)"
    by (rule pdevs_val_permute)
  thus thesis ..
qed

lemma lex_nlex_pdevs: "lex (pdevs_apply (nlex_pdevs x) i) 0"
  by (auto simp: lex_def algebra_simps prod_eq_iff)


subsection ‹Lowest Vertex›

definition lowest_vertex::"'a::ordered_euclidean_space aform ⇒ 'a" where
  "lowest_vertex X = fst X - sum_list (map snd (list_of_pdevs (snd X)))"

lemma snd_abs: "snd (abs x) = abs (snd x)"
  by (metis abs_prod_def snd_conv)

lemma lowest_vertex:
  fixes X Y::"(real*real) aform"
  assumes "e ∈ UNIV → {-1 .. 1}"
  assumes "⋀i. snd (pdevs_apply (snd X) i) ≥ 0"
  assumes "⋀i. abs (snd (pdevs_apply (snd Y) i)) = abs (snd (pdevs_apply (snd X) i))"
  assumes "degree_aform Y = degree_aform X"
  assumes "fst Y = fst X"
  shows "snd (lowest_vertex X) ≤ snd (aform_val e Y)"
proof -
  from abs_pdevs_val_le_tdev[OF assms(1), of "snd Y"]
  have "snd ¦pdevs_val e (snd Y)¦ ≤ (∑i<degree_aform Y. ¦snd (pdevs_apply (snd X) i)¦)"
    unfolding lowest_vertex_def
    by (auto simp: aform_val_def tdev_def less_eq_prod_def snd_sum snd_abs assms)
  also have "… = (∑i<degree_aform X. snd (pdevs_apply (snd X) i))"
    by (simp add: assms)
  also have "… ≤ snd (sum_list (map snd (list_of_pdevs (snd X))))"
    by (simp add: sum_list_list_of_pdevs dense_list_of_pdevs_def sum_list_distinct_conv_sum_set
      snd_sum atLeast0LessThan)
  finally show ?thesis
    by (auto simp: aform_val_def lowest_vertex_def minus_le_iff snd_abs abs_real_def assms
      split: if_split_asm)
qed

lemma sum_list_nonposI:
  fixes xs::"'a::ordered_comm_monoid_add list"
  shows "list_all (λx. x ≤ 0) xs ⟹ sum_list xs ≤ 0"
  by (induct xs) (auto simp: intro!: add_nonpos_nonpos)

lemma center_le_lowest:
  "fst (fst X) ≤ fst (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  by (auto simp: lowest_vertex_def fst_sum_list intro!: sum_list_nonposI)
    (auto simp: lex_def list_all_iff list_of_pdevs_def dest!: in_set_butlastD split: if_split_asm)

lemma lowest_vertex_eq_center_iff:
  "lowest_vertex (x0, nlex_pdevs (snd X)) = x0 ⟷ snd X = zero_pdevs"
proof
  assume "lowest_vertex (x0, nlex_pdevs (snd X)) = x0"
  then have "sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))) = 0"
    by (simp add: lowest_vertex_def)
  moreover have "list_all (λx. Counterclockwise_2D_Arbitrary.lex x 0)
    (map snd (list_of_pdevs (nlex_pdevs (snd X))))"
    by (auto simp add: list_all_iff list_of_pdevs_def)
  ultimately have "∀x∈set (list_of_pdevs (nlex_pdevs (snd X))). snd x = 0"
    by (simp add: sum_list_nlex_eq_zero_iff list_all_iff)
  then have "pdevs_apply (snd X) i = pdevs_apply zero_pdevs i" for i
    by (simp add: list_of_pdevs_def split: if_splits)
  then show "snd X = zero_pdevs"
    by (rule pdevs_eqI)
qed (simp add: lowest_vertex_def)


subsection ‹Collinear Generators›

lemma scaleR_le_self_cancel:
  fixes c::"'a::ordered_real_vector"
  shows "a *⇩R c ≤ c ⟷ (1 < a ∧ c ≤ 0 ∨ a < 1 ∧ 0 ≤ c ∨ a = 1)"
  using scaleR_le_0_iff[of "a - 1" c]
  by (simp add: algebra_simps)

lemma pdevs_val_coll:
  assumes coll: "list_all (coll 0 x) xs"
  assumes nlex: "list_all (λx. lex x 0) xs"
  assumes "x ≠ 0"
  assumes "f ∈ UNIV → {-1 .. 1}"
  obtains e where "e ∈ {-1 .. 1}" "pdevs_val f (pdevs_of_list xs) = e *⇩R (sum_list xs)"
proof cases
  assume "sum_list xs = 0"
  have "pdevs_of_list xs = zero_pdevs"
    by (auto intro!: pdevs_eqI sum_list_nlex_eq_zeroI[OF nlex ‹sum_list xs = 0›]
      simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem)
  hence "0 ∈ {-1 .. 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *⇩R sum_list xs"
    by simp_all
  thus ?thesis ..
next
  assume "sum_list xs ≠ 0"
  have "sum_list (map abs xs) ≥ 0"
    by (auto intro!: sum_list_nonneg)
  hence [simp]: "¬sum_list (map abs xs) ≤ 0"
    by (metis ‹sum_list xs ≠ 0› abs_le_zero_iff antisym_conv sum_list_abs)

  have collist: "list_all (coll 0 (sum_list xs)) xs"
  proof (rule list_allI)
    fix y assume "y ∈ set xs"
    hence "coll 0 x y"
      using coll by (auto simp: list_all_iff)
    also have "coll 0 x (sum_list xs)"
      using coll by (auto simp: list_all_iff intro!: coll_sum_list)
    finally (coll_trans)
    show "coll 0 (sum_list xs) y"
      by (simp add: coll_commute ‹x ≠ 0›)
  qed

  {
    fix i assume "i < length xs"
    hence "∃r. xs ! i = r *⇩R (sum_list xs)"
      by (metis (mono_tags) coll_scale nth_mem ‹sum_list xs ≠ 0› list_all_iff collist)
  } then obtain r where r: "⋀i. i < length xs ⟹ (xs ! i) = r i *⇩R (sum_list xs)"
    by metis
  let ?coll = "pdevs_of_list xs"
  have "pdevs_val f (pdevs_of_list xs) =
      (∑i<degree (pdevs_of_list xs). f i *⇩R xs ! i)"
    unfolding pdevs_val_sum
    by (simp add: pdevs_apply_pdevs_of_list less_degree_pdevs_of_list_imp_less_length)
  also have "… = (∑i<degree ?coll. (f i * r i) *⇩R (sum_list xs))"
    by (simp add: r less_degree_pdevs_of_list_imp_less_length)
  also have "… = (∑i<degree ?coll. f i * r i) *⇩R (sum_list xs)"
    by (simp add: algebra_simps scaleR_sum_left)
  finally have eq: "pdevs_val f ?coll = (∑i<degree ?coll. f i * r i) *⇩R (sum_list xs)"
    (is "_ = ?e *⇩R _")
    .

  have "abs (pdevs_val f ?coll) ≤ tdev ?coll"
    using assms(4)
    by (intro abs_pdevs_val_le_tdev) (auto simp: Pi_iff less_imp_le)
  also have "… = sum_list (map abs xs)" using assms by simp
  also note eq
  finally have less: "¦?e¦ *⇩R abs (sum_list xs) ≤ sum_list (map abs xs)" by (simp add: abs_scaleR)
  also have "¦sum_list xs¦ = sum_list (map abs xs)"
    using coll ‹x ≠ 0› nlex
    by (rule abs_sum_list_coll)
  finally have "?e ∈ {-1 .. 1}"
    by (auto simp add: less_le scaleR_le_self_cancel)
  thus ?thesis using eq ..
qed

lemma scaleR_eq_self_cancel:
  fixes x::"'a::real_vector"
  shows "a *⇩R x = x ⟷ a = 1 ∨ x = 0"
  using scaleR_cancel_right[of a x 1]
  by simp

lemma abs_pdevs_val_less_tdev:
  assumes "e ∈ UNIV → {-1 <..< 1}" "degree x > 0"
  shows "¦pdevs_val e x¦ < tdev x"
proof -
  have bnds: "⋀i. ¦e i¦ < 1" "⋀i. ¦e i¦ ≤ 1"
    using assms
    by (auto simp: Pi_iff abs_less_iff order.strict_implies_order)
  moreover
  let ?w = "degree x - 1"
  have witness: "¦e ?w¦ *⇩R ¦pdevs_apply x ?w¦ < ¦pdevs_apply x ?w¦"
    using degree_least_nonzero[of x] assms bnds
    by (intro neq_le_trans) (auto simp: scaleR_eq_self_cancel Pi_iff
      intro!: scaleR_left_le_one_le neq_le_trans
      intro: abs_leI less_imp_le dest!: order.strict_implies_not_eq)
  ultimately
  show ?thesis
    using assms witness bnds
    by (auto simp: pdevs_val_sum tdev_def abs_scaleR
      intro!: le_less_trans[OF sum_abs] sum_strict_mono_ex1 scaleR_left_le_one_le)
qed

lemma pdevs_val_coll_strict:
  assumes coll: "list_all (coll 0 x) xs"
  assumes nlex: "list_all (λx. lex x 0) xs"
  assumes "x ≠ 0"
  assumes "f ∈ UNIV → {-1 <..< 1}"
  obtains e where "e ∈ {-1 <..< 1}" "pdevs_val f (pdevs_of_list xs) = e *⇩R (sum_list xs)"
proof cases
  assume "sum_list xs = 0"
  have "pdevs_of_list xs = zero_pdevs"
    by (auto intro!: pdevs_eqI sum_list_nlex_eq_zeroI[OF nlex ‹sum_list xs = 0›]
      simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem)
  hence "0 ∈ {-1 <..< 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *⇩R sum_list xs"
    by simp_all
  thus ?thesis ..
next
  assume "sum_list xs ≠ 0"
  have "sum_list (map abs xs) ≥ 0"
    by (auto intro!: sum_list_nonneg)
  hence [simp]: "¬sum_list (map abs xs) ≤ 0"
    by (metis ‹sum_list xs ≠ 0› abs_le_zero_iff antisym_conv sum_list_abs)

  have "∃x ∈ set xs. x ≠ 0"
  proof (rule ccontr)
    assume "¬ (∃x∈set xs. x ≠ 0)"
    hence "⋀x. x ∈ set xs ⟹ x = 0" by auto
    hence "sum_list xs = 0"
      by (auto simp: sum_list_eq_0_iff_nonpos list_all_iff less_eq_prod_def prod_eq_iff fst_sum_list
        snd_sum_list)
    thus False using ‹sum_list xs ≠ 0› by simp
  qed
  then obtain i where i: "i < length xs" "xs ! i ≠ 0"
    by (metis in_set_conv_nth)
  hence "i < degree (pdevs_of_list xs)"
    by (auto intro!: degree_gt simp: pdevs_apply_pdevs_of_list)
  hence deg_pos: "0 < degree (pdevs_of_list xs)" by simp

  have collist: "list_all (coll 0 (sum_list xs)) xs"
  proof (rule list_allI)
    fix y assume "y ∈ set xs"
    hence "coll 0 x y"
      using coll by (auto simp: list_all_iff)
    also have "coll 0 x (sum_list xs)"
      using coll by (auto simp: list_all_iff intro!: coll_sum_list)
    finally (coll_trans)
    show "coll 0 (sum_list xs) y"
      by (simp add: coll_commute ‹x ≠ 0›)
  qed

  {
    fix i assume "i < length xs"
    hence "∃r. xs ! i = r *⇩R (sum_list xs)"
      by (metis (mono_tags, lifting) ‹sum_list xs ≠ 0› coll_scale collist list_all_iff nth_mem)
  } then obtain r where r: "⋀i. i < length xs ⟹ (xs ! i) = r i *⇩R (sum_list xs)"
    by metis
  let ?coll = "pdevs_of_list xs"
  have "pdevs_val f (pdevs_of_list xs) =
      (∑i<degree (pdevs_of_list xs). f i *⇩R xs ! i)"
    unfolding pdevs_val_sum
    by (simp add: less_degree_pdevs_of_list_imp_less_length pdevs_apply_pdevs_of_list)
  also have "… = (∑i<degree ?coll. (f i * r i) *⇩R (sum_list xs))"
    by (simp add: r less_degree_pdevs_of_list_imp_less_length)
  also have "… = (∑i<degree ?coll. f i * r i) *⇩R (sum_list xs)"
    by (simp add: algebra_simps scaleR_sum_left)
  finally have eq: "pdevs_val f ?coll = (∑i<degree ?coll. f i * r i) *⇩R (sum_list xs)"
    (is "_ = ?e *⇩R _")
    .

  have "abs (pdevs_val f ?coll) < tdev ?coll"
    using assms(4)
    by (intro abs_pdevs_val_less_tdev) (auto simp: Pi_iff less_imp_le deg_pos)
  also have "… = sum_list (map abs xs)" using assms by simp
  also note eq
  finally have less: "¦?e¦ *⇩R abs (sum_list xs) < sum_list (map abs xs)" by (simp add: abs_scaleR)
  also have "¦sum_list xs¦ = sum_list (map abs xs)"
    using coll ‹x ≠ 0› nlex
    by (rule abs_sum_list_coll)
  finally have "?e ∈ {-1 <..< 1}"
    by (auto simp add: less_le scaleR_le_self_cancel)
  thus ?thesis using eq ..
qed


subsection ‹Independent Generators›

fun independent_pdevs::"point list ⇒ point list"
  where
  "independent_pdevs [] = []"
| "independent_pdevs (x#xs) =
    (let
      (cs, is) = List.partition (coll 0 x) xs;
      s = x + sum_list cs
    in (if s = 0 then [] else [s]) @ independent_pdevs is)"

lemma in_set_independent_pdevsE:
  assumes "y ∈ set (independent_pdevs xs)"
  obtains x where "x∈set xs" "coll 0 x y"
proof atomize_elim
  show "∃x. x ∈ set xs ∧ coll 0 x y"
    using assms
  proof (induct xs rule: independent_pdevs.induct)
    case 1 thus ?case by simp
  next
    case (2 z zs)
    let ?c1 = "y = z + sum_list (filter (coll 0 z) zs)"
    let ?c2 = "y ∈ set (independent_pdevs (filter (Not ∘ coll 0 z) zs))"
    from 2
    have "?c1 ∨ ?c2"
      by (auto simp: Let_def split: if_split_asm)
    thus ?case
    proof
      assume ?c2
      hence "y ∈ set (independent_pdevs (snd (partition (coll 0 z) zs)))"
        by simp
      from 2(1)[OF refl prod.collapse refl this]
      show ?case
        by auto
    next
      assume y: ?c1
      show ?case
        unfolding y
        by (rule exI[where x="z"]) (auto intro!: coll_add coll_sum_list )
    qed
  qed
qed

lemma in_set_independent_pdevs_nonzero: "x ∈ set (independent_pdevs xs) ⟹ x ≠ 0"
proof (induct xs rule: independent_pdevs.induct)
  case (2 y ys)
  from 2(1)[OF refl prod.collapse refl] 2(2)
  show ?case
    by (auto simp: Let_def split: if_split_asm)
qed simp

lemma independent_pdevs_pairwise_non_coll:
  assumes "x ∈ set (independent_pdevs xs)"
  assumes "y ∈ set (independent_pdevs xs)"
  assumes "⋀x. x ∈ set xs ⟹ x ≠ 0"
  assumes "x ≠ y"
  shows "¬ coll 0 x y"
using assms
proof (induct xs rule: independent_pdevs.induct)
  case 1 thus ?case by simp
next
  case (2 z zs)
  from 2 have "z ≠ 0" by simp
  from 2(2) have "x ≠ 0" by (rule in_set_independent_pdevs_nonzero)
  from 2(3) have "y ≠ 0" by (rule in_set_independent_pdevs_nonzero)
  let ?c = "filter (coll 0 z) zs"
  let ?nc = "filter (Not ∘ coll 0 z) zs"
  {
    assume "x ∈ set (independent_pdevs ?nc)" "y ∈ set (independent_pdevs ?nc)"
    hence "¬coll 0 x y"
      by (intro 2(1)[OF refl prod.collapse refl _ _ 2(4) 2(5)]) auto
  } note IH = this
  {
    fix x assume "x ≠ 0" "z + sum_list ?c ≠ 0"
      "coll 0 x (z + sum_list ?c)"
    hence "x ∉ set (independent_pdevs ?nc)"
      using sum_list_filter_coll_ex_scale[OF ‹z ≠ 0›, of "z#zs"]
      by (auto elim!: in_set_independent_pdevsE  simp: coll_commute)
        (metis (no_types) ‹x ≠ 0› coll_scale coll_scaleR)
  } note nc = this
  from 2(2,3,4,5) nc[OF ‹x ≠ 0›] nc[OF ‹y ≠ 0›]
  show ?case
    by (auto simp: Let_def IH coll_commute split: if_split_asm)
qed

lemma distinct_independent_pdevs[simp]:
  shows "distinct (independent_pdevs xs)"
proof (induct xs rule: independent_pdevs.induct)
  case 1 thus ?case by simp
next
  case (2 x xs)
  let ?is = "independent_pdevs (filter (Not ∘ coll 0 x) xs)"
  have "distinct ?is"
    by (rule 2) (auto intro!: 2)
  thus ?case
  proof (clarsimp simp add: Let_def)
    let ?s = "x + sum_list (filter (coll 0 x) xs)"
    assume s: "?s ≠ 0" "?s ∈ set ?is"
    from in_set_independent_pdevsE[OF s(2)]
    obtain y where y:
      "y ∈ set (filter (Not ∘ coll 0 x) xs)"
      "coll 0 y (x + sum_list (filter (coll 0 x) xs))"
      by auto
    {
      assume "y = 0 ∨ x = 0 ∨ sum_list (filter (coll 0 x) xs) = 0"
      hence False using s y by (auto simp: coll_commute)
    } moreover {
      assume "y ≠ 0" "x ≠ 0" "sum_list (filter (coll 0 x) xs) ≠ 0"
        "sum_list (filter (coll 0 x) xs) + x ≠ 0"
      have *: "coll 0 (sum_list (filter (coll 0 x) xs)) x"
        by (auto intro!: coll_sum_list simp: coll_commute)
      have "coll 0 y (sum_list (filter (coll 0 x) xs) + x)"
        using s y by (simp add: add.commute)
      hence "coll 0 y x" using *
        by (rule coll_add_trans) fact+
      hence False using s y by (simp add: coll_commute)
    } ultimately show False using s y by (auto simp: add.commute)
  qed
qed

lemma in_set_independent_pdevs_invariant_nlex:
  "x ∈ set (independent_pdevs xs) ⟹ (⋀x. x ∈ set xs ⟹ lex x 0) ⟹
  (⋀x. x ∈ set xs ⟹ x ≠ 0) ⟹ Counterclockwise_2D_Arbitrary.lex x 0"
proof (induction xs arbitrary: x rule: independent_pdevs.induct )
  case 1 thus ?case by simp
next
  case (2 y ys)
  from 2 have "y ≠ 0" by auto
  from 2(2)
  have "x ∈ set (independent_pdevs (filter (Not ∘ coll 0 y) ys)) ∨
    x = y + sum_list (filter (coll 0 y) ys)"
    by (auto simp: Let_def split: if_split_asm)
  thus ?case
  proof
    assume "x ∈ set (independent_pdevs (filter (Not ∘ coll 0 y) ys))"
    from 2(1)[OF refl prod.collapse refl, simplified, OF this 2(3,4)]
    show ?case by simp
  next
    assume "x = y + sum_list (filter (coll 0 y) ys)"
    also have "lex … 0"
      by (force intro: nlex_add nlex_sum simp: sum_list_sum_nth
        dest: nth_mem intro: 2(3))
    finally show ?case .
  qed
qed

lemma
  pdevs_val_independent_pdevs2:
  assumes "e ∈ UNIV → I"
  shows "∃e'. e' ∈ UNIV → I ∧
    pdevs_val e (pdevs_of_list (independent_pdevs xs)) = pdevs_val e' (pdevs_of_list xs)"
  using assms
proof (induct xs arbitrary: e rule: independent_pdevs.induct)
  case 1 thus ?case by force
next
  case (2 x xs)
  let ?coll = "(filter (coll 0 x) (x#xs))"
  let ?ncoll = "(filter (Not o coll 0 x) (x#xs))"
  let ?e0 = "if sum_list ?coll = 0 then e else e ∘ (+) (Suc 0)"
  have "pdevs_val e (pdevs_of_list (independent_pdevs (x#xs))) =
    e 0 *⇩R (sum_list ?coll) + pdevs_val ?e0 (pdevs_of_list (independent_pdevs ?ncoll))"
    (is "_ = ?vc + ?vnc")
    by (simp add: Let_def)
  also
  have e_split: "(λ_. e 0) ∈ UNIV → I" "?e0 ∈ UNIV → I"
    using 2(2) by auto
  from 2(1)[OF refl prod.collapse refl e_split(2)]
  obtain e' where e': "e' ∈ UNIV → I" and "?vnc = pdevs_val e' (pdevs_of_list ?ncoll)"
    by (auto simp add: o_def)
  note this(2)
  also
  have "?vc = pdevs_val (λ_. e 0) (pdevs_of_list ?coll)"
    by (simp add: pdevs_val_const_pdevs_of_list)
  also
  from pdevs_val_pdevs_of_list_append[OF e_split(1) e'] obtain e'' where
    e'': "e'' ∈ UNIV → I"
    and "pdevs_val (λ_. e 0) (pdevs_of_list ?coll) + pdevs_val e' (pdevs_of_list ?ncoll) =
      pdevs_val e'' (pdevs_of_list (?coll @ ?ncoll))"
    by metis
  note this(2)
  also
  from pdevs_val_perm[OF partition_permI e'', of "coll 0 x" "x#xs"]
  obtain e''' where e''': "e''' ∈ UNIV → I"
    and "… = pdevs_val e''' (pdevs_of_list (x # xs))"
    by metis
  note this(2)
  finally show ?case using e''' by auto
qed

lemma list_all_filter: "list_all p (filter p xs)"
  by (induct xs) auto

lemma pdevs_val_independent_pdevs:
  assumes "list_all (λx. lex x 0) xs"
  assumes "list_all (λx. x ≠ 0) xs"
  assumes "e ∈ UNIV → {-1 .. 1}"
  shows "∃e'. e' ∈ UNIV → {-1 .. 1} ∧ pdevs_val e (pdevs_of_list xs) =
    pdevs_val e' (pdevs_of_list (independent_pdevs xs))"
  using assms(1,2,3)
proof (induct xs arbitrary: e rule: independent_pdevs.induct)
  case 1 thus ?case by force
next
  case (2 x xs)

  let ?coll = "(filter (coll 0 x) (x#xs))"
  let ?ncoll = "(filter (Not o coll 0 x) xs)"

  from 2 have "x ≠ 0" by simp

  from pdevs_val_partition[OF 2(4), of "x#xs" "coll 0 x"]
  obtain f g where part: "pdevs_val e (pdevs_of_list (x # xs)) =
      pdevs_val f (pdevs_of_list ?coll) +
      pdevs_val g (pdevs_of_list (filter (Not o coll 0 x) (x#xs)))"
    and f: "f ∈ UNIV → {-1 .. 1}" and g: "g ∈ UNIV → {-1 .. 1}"
    by blast
  note part
  also

  have "list_all (λx. lex x 0) (filter (coll 0 x) (x#xs))"
    using 2(2) by (auto simp: inner_prod_def list_all_iff)
  from pdevs_val_coll[OF list_all_filter this ‹x ≠ 0› f]
  obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *⇩R sum_list (filter (coll 0 x) (x#xs))"
    and f': "f' ∈ {-1 .. 1}"
    by blast
  note this(1)
  also

  have "filter (Not o coll 0 x) (x#xs) = ?ncoll"
    by simp
  also

  from 2(2) have "list_all (λx. lex x 0) ?ncoll" "list_all (λx. x ≠ 0) ?ncoll"
    by (auto simp: list_all_iff)
  from 2(1)[OF refl partition_filter_conv[symmetric] refl this g]
  obtain g'
  where "pdevs_val g (pdevs_of_list ?ncoll) =
      pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))"
    and g': "g' ∈ UNIV → {-1 .. 1}"
    by metis
  note this(1)
  also

  define h where "h = (if sum_list ?coll ≠ 0 then rec_nat f' (λi _. g' i) else g')"
  have "f' *⇩R sum_list ?coll + pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))
      = pdevs_val h (pdevs_of_list (independent_pdevs (x#xs)))"
    by (simp add: h_def o_def Let_def)

  finally
  have "pdevs_val e (pdevs_of_list (x # xs)) =
      pdevs_val h (pdevs_of_list (independent_pdevs (x # xs)))" .

  moreover have "h ∈ UNIV → {-1 .. 1}"
  proof
    fix i show "h i ∈ {-1 .. 1}"
      using f' g'
      by (cases i) (auto simp: h_def)
  qed

  ultimately show ?case by blast
qed

lemma
  pdevs_val_independent_pdevs_strict:
  assumes "list_all (λx. lex x 0) xs"
  assumes "list_all (λx. x ≠ 0) xs"
  assumes "e ∈ UNIV → {-1 <..< 1}"
  shows "∃e'. e' ∈ UNIV → {-1 <..< 1} ∧ pdevs_val e (pdevs_of_list xs) =
    pdevs_val e' (pdevs_of_list (independent_pdevs xs))"
  using assms(1,2,3)
proof (induct xs arbitrary: e rule: independent_pdevs.induct)
  case 1 thus ?case by force
next
  case (2 x xs)

  let ?coll = "(filter (coll 0 x) (x#xs))"
  let ?ncoll = "(filter (Not o coll 0 x) xs)"

  from 2 have "x ≠ 0" by simp

  from pdevs_val_partition[OF 2(4), of "x#xs" "coll 0 x"]
  obtain f g
  where part: "pdevs_val e (pdevs_of_list (x # xs)) =
      pdevs_val f (pdevs_of_list ?coll) +
      pdevs_val g (pdevs_of_list (filter (Not o coll 0 x) (x#xs)))"
    and f: "f ∈ UNIV → {-1 <..< 1}" and g: "g ∈ UNIV → {-1 <..< 1}"
    by blast
  note part
  also

  have "list_all (λx. lex x 0) (filter (coll 0 x) (x#xs))"
    using 2(2) by (auto simp: inner_prod_def list_all_iff)
  from pdevs_val_coll_strict[OF list_all_filter this ‹x ≠ 0› f]
  obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *⇩R sum_list (filter (coll 0 x) (x#xs))"
    and f': "f' ∈ {-1 <..< 1}"
    by blast
  note this(1)
  also

  have "filter (Not o coll 0 x) (x#xs) = ?ncoll"
    by simp
  also

  from 2(2) have "list_all (λx. lex x 0) ?ncoll" "list_all (λx. x ≠ 0) ?ncoll"
    by (auto simp: list_all_iff)
  from 2(1)[OF refl partition_filter_conv[symmetric] refl this g]
  obtain g'
  where "pdevs_val g (pdevs_of_list ?ncoll) =
      pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))"
    and g': "g' ∈ UNIV → {-1 <..< 1}"
    by metis
  note this(1)
  also

  define h where "h = (if sum_list ?coll ≠ 0 then rec_nat f' (λi _. g' i) else g')"
  have "f' *⇩R sum_list ?coll + pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))
      = pdevs_val h (pdevs_of_list (independent_pdevs (x#xs)))"
    by (simp add: h_def o_def Let_def)

  finally
  have "pdevs_val e (pdevs_of_list (x # xs)) =
      pdevs_val h (pdevs_of_list (independent_pdevs (x # xs)))" .

  moreover have "h ∈ UNIV → {-1 <..< 1}"
  proof
    fix i show "h i ∈ {-1 <..< 1}"
      using f' g'
      by (cases i) (auto simp: h_def)
  qed

  ultimately show ?case by blast
qed

lemma sum_list_independent_pdevs: "sum_list (independent_pdevs xs) = sum_list xs"
proof (induct xs rule: independent_pdevs.induct)
  case (2 y ys)
  from 2[OF refl prod.collapse refl]
  show ?case
    using sum_list_partition[of "coll 0 y" ys, symmetric]
    by (auto simp: Let_def)
qed simp

lemma independent_pdevs_eq_Nil_iff:
  "list_all (λx. lex x 0) xs ⟹ list_all (λx. x ≠ 0) xs ⟹ independent_pdevs xs = [] ⟷ xs = []"
proof (induct xs)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  from Cons(2) have "list_all (λx. lex x 0) (x # filter (coll 0 x) xs)"
    by (auto simp: list_all_iff)
  from sum_list_nlex_eq_zero_iff[OF this] Cons(3)
  show ?case
    by (auto simp: list_all_iff)
qed


subsection ‹Independent Oriented Generators›

definition "inl p = independent_pdevs (map snd (list_of_pdevs (nlex_pdevs p)))"

lemma distinct_inl[simp]: "distinct (inl (snd X))"
  by (auto simp: inl_def)

lemma in_set_inl_nonzero: "x ∈ set (inl xs) ⟹ x ≠ 0"
  by (auto simp: inl_def in_set_independent_pdevs_nonzero)

lemma
  inl_ncoll: "y ∈ set (inl (snd X)) ⟹ z ∈ set (inl (snd X)) ⟹ y ≠ z ⟹ ¬coll 0 y z"
  unfolding inl_def
  by (rule independent_pdevs_pairwise_non_coll, assumption+)
    (auto simp: inl_def list_of_pdevs_nonzero)

lemma in_set_inl_lex: "x ∈ set (inl xs) ⟹ lex x 0"
  by (auto simp: inl_def list_of_pdevs_def dest!: in_set_independent_pdevs_invariant_nlex
    split: if_split_asm)

interpretation ccw0: linorder_list "ccw 0" "set (inl (snd X))"
proof unfold_locales
  fix a b c
  show "a ≠ b ⟹ ccw 0 a b ∨ ccw 0 b a"
    by (metis UNIV_I ccw_self(1) nondegenerate)
  assume a: "a ∈ set (inl (snd X))"
  show "ccw 0 a a"
    by simp
  assume b: "b ∈ set (inl (snd X))"
  show "ccw 0 a b ⟹ ccw 0 b a ⟹ a = b"
    by (metis ccw_self(1) in_set_inl_nonzero mem_Collect_eq not_ccw_eq a b)
  assume c: "c ∈ set (inl (snd X))"
  assume distinct: "a ≠ b" "b ≠ c" "a ≠ c"
  assume ab: "ccw 0 a b" and bc: "ccw 0 b c"
  show "ccw 0 a c"
    using a b c ab bc
  proof (cases "a = (0, 1)" "b = (0, 1)" "c = (0, 1)"
      rule: case_split[case_product case_split[case_product case_split]])
    assume nu: "a ≠ (0, 1)" "b ≠ (0, 1)" "c ≠ (0, 1)"
    have "distinct5 a b c (0, 1) 0" "in5 UNIV a b c (0, 1) 0"
      using a b c distinct nu by (simp_all add: in_set_inl_nonzero)
    moreover have "ccw 0 (0, 1) a" "ccw 0 (0, 1) b" "ccw 0 (0, 1) c"
      by (auto intro!: nlex_ccw_left in_set_inl_lex a b c)
    ultimately show ?thesis using ab bc
      by (rule ccw.transitive[where S=UNIV and s="(0, 1)"])
  next
    assume "a ≠ (0, 1)" "b = (0, 1)" "c ≠ (0, 1)"
    thus ?thesis
      using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left a b ab
      by blast
  next
    assume "a ≠ (0, 1)" "b ≠ (0, 1)" "c = (0, 1)"
    thus ?thesis
      using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left b c bc
      by blast
  qed (auto simp add: nlex_ccw_left in_set_inl_lex)
qed

lemma sorted_inl: "ccw.sortedP 0 (ccw.selsort 0 (inl (snd X)))"
  by (rule ccw0.sortedP_selsort) auto

lemma sorted_scaled_inl: "ccw.sortedP 0 (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X))))"
  using sorted_inl
  by (rule ccw_sorted_scaleR) simp

lemma distinct_selsort_inl: "distinct (ccw.selsort 0 (inl (snd X)))"
  by simp

lemma distinct_map_scaleRI:
  fixes xs::"'a::real_vector list"
  shows "distinct xs ⟹ c ≠ 0 ⟹ distinct (map ((*⇩R) c) xs)"
  by (induct xs) auto

lemma distinct_scaled_inl: "distinct (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X))))"
  using distinct_selsort_inl
  by (rule distinct_map_scaleRI) simp

lemma ccw'_sortedP_scaled_inl:
  "ccw'.sortedP 0 (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X))))"
  using ccw_sorted_implies_ccw'_sortedP
  by (rule ccw'_sorted_scaleR) (auto simp: sorted_inl inl_ncoll)

lemma pdevs_val_pdevs_of_list_inl2E:
  assumes "e ∈ UNIV → {-1 .. 1}"
  obtains e' where "pdevs_val e X = pdevs_val e' (pdevs_of_list (inl X))" "e' ∈ UNIV → {-1 .. 1}"
proof -
  let ?l = "map snd (list_of_pdevs (nlex_pdevs X))"
  have l: "list_all (λx. Counterclockwise_2D_Arbitrary.lex x 0) ?l"
    "list_all (λx. x ≠ 0) (map snd (list_of_pdevs (nlex_pdevs X)))"
    by (auto simp: list_all_iff list_of_pdevs_def)

  from pdevs_val_nlex_pdevs[OF assms(1)]
  obtain e' where "e' ∈ UNIV → {-1 .. 1}" "pdevs_val e X = pdevs_val e' (nlex_pdevs X)"
    by auto
  note this(2)
  also from pdevs_val_of_list_of_pdevs2[OF ‹e' ∈ _›]
  obtain e'' where "e'' ∈ UNIV → {-1 .. 1}" "… = pdevs_val e'' (pdevs_of_list ?l)"
    by metis
  note this(2)
  also from pdevs_val_independent_pdevs[OF l ‹e'' ∈ _›]
  obtain e'''
  where "e''' ∈ UNIV → {-1 .. 1}"
    and "… = pdevs_val e''' (pdevs_of_list (independent_pdevs ?l))"
    by metis
  note this(2)
  also have "… = pdevs_val e''' (pdevs_of_list (inl X))"
    by (simp add: inl_def)
  finally have "pdevs_val e X = pdevs_val e''' (pdevs_of_list (inl X))" .
  thus thesis using ‹e''' ∈ _› ..
qed

lemma pdevs_val_pdevs_of_list_inlE:
  assumes "e ∈ UNIV → I" "uminus ` I = I" "0 ∈ I"
  obtains e' where "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e' X" "e' ∈ UNIV → I"
proof -
  let ?l = "map snd (list_of_pdevs (nlex_pdevs X))"
  have "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e (pdevs_of_list (independent_pdevs ?l))"
    by (simp add: inl_def)
  also
  from pdevs_val_independent_pdevs2[OF ‹e ∈ _›]
  obtain e'
  where "pdevs_val e (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e' (pdevs_of_list ?l)"
    and "e' ∈ UNIV → I"
    by auto
  note this(1)
  also
  from pdevs_val_of_list_of_pdevs[OF ‹e' ∈ _› ‹0 ∈ I›, of "nlex_pdevs X"]
  obtain e'' where "pdevs_val e' (pdevs_of_list ?l) = pdevs_val e'' (nlex_pdevs X)"
    and "e'' ∈ UNIV → I"
    by metis
  note this(1)
  also
  from pdevs_val_nlex_pdevs2[OF ‹e'' ∈ _› ‹_ = I›]
  obtain e''' where "pdevs_val e'' (nlex_pdevs X) = pdevs_val e''' X" "e''' ∈ UNIV → I"
    by metis
  note this(1)
  finally have "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e''' X" .
  thus ?thesis using ‹e''' ∈ UNIV → I› ..
qed

lemma sum_list_nlex_eq_sum_list_inl:
  "sum_list (map snd (list_of_pdevs (nlex_pdevs X))) = sum_list (inl X)"
  by (auto simp: inl_def sum_list_list_of_pdevs sum_list_independent_pdevs)

lemma Affine_inl: "Affine (fst X, pdevs_of_list (inl (snd X))) = Affine X"
  by (auto simp: Affine_def valuate_def aform_val_def
    elim: pdevs_val_pdevs_of_list_inlE[of _ _ "snd X"] pdevs_val_pdevs_of_list_inl2E[of _ "snd X"])


subsection ‹Half Segments›

definition half_segments_of_aform::"point aform ⇒ (point*point) list"
  where "half_segments_of_aform X =
    (let
      x0 = lowest_vertex (fst X, nlex_pdevs (snd X))
    in
      polychain_of x0 (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X)))))"

lemma subsequent_half_segments:
  fixes X
  assumes "Suc i < length (half_segments_of_aform X)"
  shows "snd (half_segments_of_aform X ! i) = fst (half_segments_of_aform X ! Suc i)"
  using assms
  by (cases i) (auto simp: half_segments_of_aform_def Let_def polychain_of_subsequent_eq)

lemma polychain_half_segments_of_aform: "polychain (half_segments_of_aform X)"
  by (auto simp: subsequent_half_segments intro!: polychainI)

lemma fst_half_segments:
  "half_segments_of_aform X ≠ [] ⟹
    fst (half_segments_of_aform X ! 0) = lowest_vertex (fst X, nlex_pdevs (snd X))"
  by (auto simp: half_segments_of_aform_def Let_def o_def split_beta')

lemma nlex_half_segments_of_aform: "(a, b) ∈ set (half_segments_of_aform X) ⟹ lex b a"
  by (auto simp: half_segments_of_aform_def prod_eq_iff lex_def
    dest!: in_set_polychain_ofD in_set_inl_lex)

lemma ccw_half_segments_of_aform_all:
  assumes cd: "(c, d) ∈ set (half_segments_of_aform X)"
  shows "list_all (λ(xi, xj). ccw xi xj c ∧ ccw xi xj d) (half_segments_of_aform X)"
proof -
  have
    "list_all (λ(xi, xj). ccw xi xj (fst (c, d)) ∧ ccw xi xj (snd (c, d)))
      (polychain_of (lowest_vertex (fst X, nlex_pdevs (snd X)))
        ((map ((*⇩R) 2) (linorder_list0.selsort (ccw 0) (inl (snd X))))))"
    using ccw'_sortedP_scaled_inl cd[unfolded half_segments_of_aform_def Let_def]
    by (rule polychain_of_ccw_conjunction)
  thus ?thesis
    unfolding half_segments_of_aform_def[unfolded Let_def, symmetric] fst_conv snd_conv .
qed

lemma ccw_half_segments_of_aform:
  assumes ij: "(xi, xj) ∈ set (half_segments_of_aform X)"
  assumes c: "(c, d) ∈ set (half_segments_of_aform X)"
  shows "ccw xi xj c" "ccw xi xj d"
  using ccw_half_segments_of_aform_all[OF c] ij
  by (auto simp add: list_all_iff)

lemma half_segments_of_aform1:
  assumes ch: "x ∈ convex hull set (map fst (half_segments_of_aform X))"
  assumes ab: "(a, b) ∈ set (half_segments_of_aform X)"
  shows "ccw a b x"
  using finite_set _ ch
proof (rule ccw.convex_hull)
  fix c assume "c ∈ set (map fst (half_segments_of_aform X))"
  then obtain d where "(c, d) ∈ set (half_segments_of_aform X)" by auto
  with ab show "ccw a b c"
    by (rule ccw_half_segments_of_aform(1))
qed (insert ab, simp add: nlex_half_segments_of_aform)

lemma half_segments_of_aform2:
  assumes ch: "x ∈ convex hull set (map snd (half_segments_of_aform X))"
  assumes ab: "(a, b) ∈ set (half_segments_of_aform X)"
  shows "ccw a b x"
  using finite_set _ ch
proof (rule ccw.convex_hull)
  fix d assume "d ∈ set (map snd (half_segments_of_aform X))"
  then obtain c where "(c, d) ∈ set (half_segments_of_aform X)" by auto
  with ab show "ccw a b d"
    by (rule ccw_half_segments_of_aform(2))
qed (insert ab, simp add: nlex_half_segments_of_aform)

lemma
  in_set_half_segments_of_aform_aform_valE:
  assumes "(x2, y2) ∈ set (half_segments_of_aform X)"
  obtains e where "y2 = aform_val e X" "e ∈ UNIV → {-1 .. 1}"
proof -
  from assms obtain d where
    "y2 = lowest_vertex (fst X, nlex_pdevs (snd X)) +
      sum_list (take (Suc d) (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X)))))"
    by (auto simp: half_segments_of_aform_def elim!: in_set_polychain_of_imp_sum_list)
  also have "lowest_vertex (fst X, nlex_pdevs (snd X)) =
      fst X - sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X))))"
    by (simp add: lowest_vertex_def)
  also have "sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))) =
      pdevs_val (λ_. 1) (nlex_pdevs (snd X))"
    by (auto simp: pdevs_val_sum_list)
  also

  have "sum_list (take (Suc d) (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X))))) =
      pdevs_val (λi. if i ≤ d then 2 else 0) (pdevs_of_list (ccw.selsort 0 (inl (snd X))))"
    (is "_ = pdevs_val ?e _")
    by (subst sum_list_take_pdevs_val_eq)
      (auto simp: pdevs_val_sum if_distrib pdevs_apply_pdevs_of_list
        degree_pdevs_of_list_scaleR intro!: sum.cong )
  also
  obtain e'' where "… = pdevs_val e'' (pdevs_of_list (inl (snd X)))" "e'' ∈ UNIV → {0..2}"
    by (auto intro: pdevs_val_selsort_ccw2[of "inl (snd X)" ?e "{0 .. 2}"])
  note this(1)
  also note inl_def
  also
  let ?l = "map snd (list_of_pdevs (nlex_pdevs (snd X)))"
  from pdevs_val_independent_pdevs2[OF ‹e'' ∈ _›]
  obtain e'''
  where "pdevs_val e'' (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e''' (pdevs_of_list ?l)"
    and "e''' ∈ UNIV → {0..2}"
    by auto
  note this(1)
  also
  have "0 ∈ {0 .. 2::real}" by simp
  from pdevs_val_of_list_of_pdevs[OF ‹e''' ∈ _› this, of "nlex_pdevs (snd X)"]
  obtain e'''' where "pdevs_val e''' (pdevs_of_list ?l) = pdevs_val e'''' (nlex_pdevs (snd X))"
    and "e'''' ∈ UNIV → {0 .. 2}"
    by metis
  note this(1)
  finally have
    "y2 = fst X + (pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (λ_. 1) (nlex_pdevs (snd X)))"
    by simp
  also have "pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (λ_. 1) (nlex_pdevs (snd X)) =
      pdevs_val (λi. e'''' i - 1) (nlex_pdevs (snd X))"
    by (simp add: pdevs_val_minus)
  also
  have "(λi. e'''' i - 1) ∈ UNIV → {-1 .. 1}" using ‹e'''' ∈ _› by auto
  from pdevs_val_nlex_pdevs2[OF this]
  obtain f where "f ∈ UNIV →  {-1 .. 1}"
    and "pdevs_val (λi. e'''' i - 1) (nlex_pdevs (snd X)) = pdevs_val f (snd X)"
    by auto
  note this(2)
  finally have "y2 = aform_val f X" by (simp add: aform_val_def)
  thus ?thesis using ‹f ∈ _› ..
qed

lemma fst_hd_half_segments_of_aform:
  assumes "half_segments_of_aform X ≠ []"
  shows "fst (hd (half_segments_of_aform X)) = lowest_vertex (fst X, (nlex_pdevs (snd X)))"
  using assms
  by (auto simp: half_segments_of_aform_def Let_def fst_hd_polychain_of)

lemma
  "linorder_list0.sortedP (ccw' (lowest_vertex (fst X, nlex_pdevs (snd X))))
    (map snd (half_segments_of_aform X))"
  (is "linorder_list0.sortedP (ccw' ?x0) ?ms")
  unfolding half_segments_of_aform_def Let_def
  by (rule ccw'_sortedP_polychain_of_snd) (rule ccw'_sortedP_scaled_inl)

lemma rev_zip: "length xs = length ys ⟹ rev (zip xs ys) = zip (rev xs) (rev ys)"
  by (induct xs ys rule: list_induct2) auto

lemma zip_upt_self_aux: "zip [0..<length xs] xs = map (λi. (i, xs ! i)) [0..<length xs]"
  by (auto intro!: nth_equalityI)

lemma half_segments_of_aform_strict:
  assumes "e ∈ UNIV → {-1 <..< 1}"
  assumes "seg ∈ set (half_segments_of_aform X)"
  assumes "length (half_segments_of_aform X) ≠ 1"
  shows "ccw' (fst seg) (snd seg) (aform_val e X)"
  using assms unfolding half_segments_of_aform_def Let_def
proof -
  have len: "length (map ((*⇩R) 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))) ≠ 1"
    using assms by (auto simp: half_segments_of_aform_def)

  have "aform_val e X = fst X + pdevs_val e (snd X)"
    by (simp add: aform_val_def)
  also
  obtain e' where "e' ∈ UNIV → {-1 <..< 1}"
    "pdevs_val e (snd X) = pdevs_val e' (nlex_pdevs (snd X))"
    using pdevs_val_nlex_pdevs[OF ‹e ∈ _›]
    by auto
  note this(2)
  also obtain e'' where "e'' ∈ UNIV → {-1 <..< 1}"
    "… = pdevs_val e'' (pdevs_of_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))))"
    by (metis pdevs_val_of_list_of_pdevs2[OF ‹e' ∈ _›])
  note this(2)
  also
  obtain e''' where "e''' ∈ UNIV → {-1 <..< 1}" "… = pdevs_val e''' (pdevs_of_list (inl (snd X)))"
    unfolding inl_def
    using
      pdevs_val_independent_pdevs_strict[OF list_all_list_of_pdevsI,
        OF lex_nlex_pdevs list_of_pdevs_all_nonzero ‹e'' ∈ _›]
    by metis
  note this(2)
  also
  from pdevs_val_selsort_ccw[OF distinct_inl ‹e''' ∈ _›]
  obtain f where "f ∈ UNIV → {-1 <..< 1}"
    "… = pdevs_val f (pdevs_of_list (linorder_list0.selsort (ccw 0) (inl (snd X))))"
    (is "_ = pdevs_val _ (pdevs_of_list ?sl)")
    by metis
  note this(2)
  also have "… = pdevs_val (λi. f i + 1) (pdevs_of_list ?sl) +
      lowest_vertex (fst X, nlex_pdevs (snd X)) - fst X"
  proof -
    have "sum_list (dense_list_of_pdevs (nlex_pdevs (snd X))) =
        sum_list (dense_list_of_pdevs (pdevs_of_list (ccw.selsort 0 (inl (snd X)))))"
      by (subst dense_list_of_pdevs_pdevs_of_list)
        (auto simp: in_set_independent_pdevs_nonzero dense_list_of_pdevs_pdevs_of_list inl_def
          sum_list_distinct_selsort sum_list_independent_pdevs sum_list_list_of_pdevs)
    thus ?thesis
      by (auto simp add: pdevs_val_add lowest_vertex_def algebra_simps pdevs_val_sum_list
        sum_list_list_of_pdevs in_set_inl_nonzero dense_list_of_pdevs_pdevs_of_list)
  qed
  also have "pdevs_val (λi. f i + 1) (pdevs_of_list ?sl) =
      pdevs_val (λi. 1/2 * (f i + 1)) (pdevs_of_list (map ((*⇩R) 2) ?sl))"
    (is "_ = pdevs_val ?f' (pdevs_of_list ?ssl)")
    by (subst pdevs_val_cmul) (simp add: pdevs_of_list_map_scaleR)
  also
  have "distinct ?ssl" "?f' ∈ UNIV → {0<..<1}" using ‹f ∈ _›
    by (auto simp: distinct_map_scaleRI Pi_iff algebra_simps real_0_less_add_iff)
  from pdevs_of_list_sum[OF this]
  obtain g where "g ∈ UNIV → {0<..<1}"
    "pdevs_val ?f' (pdevs_of_list ?ssl) = (∑P∈set ?ssl. g P *⇩R P)"
    by blast
  note this(2)
  finally
  have "aform_val e X = lowest_vertex (fst X, nlex_pdevs (snd X)) + (∑P∈set ?ssl. g P *⇩R P)"
    by simp
  also
  have "ccw' (fst seg) (snd seg) …"
    using ‹g ∈ _› _ len ‹seg ∈ _›[unfolded half_segments_of_aform_def Let_def]
    by (rule in_polychain_of_ccw) (simp add: ccw'_sortedP_scaled_inl)
  finally show ?thesis .
qed

lemma half_segments_of_aform_strict_all:
  assumes "e ∈ UNIV → {-1 <..< 1}"
  assumes "length (half_segments_of_aform X) ≠ 1"
  shows "list_all (λseg. ccw' (fst seg) (snd seg) (aform_val e X)) (half_segments_of_aform X)"
  using assms
  by (auto intro!: half_segments_of_aform_strict simp: list_all_iff)

lemma list_allD: "list_all P xs ⟹ x ∈ set xs ⟹ P x"
  by (auto simp: list_all_iff)

lemma minus_one_less_multI:
  fixes e x::real
  shows "- 1 ≤ e ⟹ 0 < x ⟹ x < 1 ⟹ - 1 < e * x"
  by (metis abs_add_one_gt_zero abs_real_def le_less_trans less_not_sym mult_less_0_iff
    mult_less_cancel_left1 real_0_less_add_iff)

lemma less_one_multI:
  fixes e x::real
  shows "e ≤ 1 ⟹ 0 < x ⟹ x < 1 ⟹ e * x < 1"
  by (metis (erased, opaque_lifting) less_eq_real_def monoid_mult_class.mult.left_neutral
    mult_strict_mono zero_less_one)

lemma ccw_half_segments_of_aform_strictI:
  assumes "e ∈ UNIV → {-1 <..< 1}"
  assumes "(s1, s2) ∈ set (half_segments_of_aform X)"
  assumes "length (half_segments_of_aform X) ≠ 1"
  assumes "x = (aform_val e X)"
  shows "ccw' s1 s2 x"
  using half_segments_of_aform_strict[OF assms(1-3)] assms(4) by simp

lemma
  ccw'_sortedP_subsequent:
  assumes "Suc i < length xs" "ccw'.sortedP 0 (map dirvec xs)" "fst (xs ! Suc i) = snd (xs ! i)"
  shows "ccw' (fst (xs ! i)) (snd (xs ! i)) (snd (xs ! Suc i))"
  using assms
proof (induct xs arbitrary: i)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
    by (auto simp: nth_Cons dirvec_minus split: nat.split elim!: ccw'.sortedP_Cons)
      (metis (no_types, lifting) ccw'.renormalize length_greater_0_conv nth_mem prod.case_eq_if)
qed

lemma ccw'_sortedP_uminus: "ccw'.sortedP 0 xs ⟹ ccw'.sortedP 0 (map uminus xs)"
  by (induct xs) (auto intro!: ccw'.sortedP.Cons elim!: ccw'.sortedP_Cons simp del: uminus_Pair)

lemma subsequent_half_segments_ccw:
  fixes X
  assumes "Suc i < length (half_segments_of_aform X)"
  shows "ccw' (fst (half_segments_of_aform X ! i)) (snd (half_segments_of_aform X ! i))
    (snd (half_segments_of_aform X ! Suc i))"
  using assms
  by (intro ccw'_sortedP_subsequent )
    (auto simp: subsequent_half_segments half_segments_of_aform_def
      sorted_inl polychain_of_subsequent_eq intro!: ccw_sorted_implies_ccw'_sortedP[OF inl_ncoll]
      ccw'_sorted_scaleR)

lemma convex_polychain_half_segments_of_aform: "convex_polychain (half_segments_of_aform X)"
proof cases
  assume "length (half_segments_of_aform X) = 1"
  thus ?thesis
    by (auto simp: length_Suc_conv convex_polychain_def polychain_def)
next
  assume len: "length (half_segments_of_aform X) ≠ 1"
  show ?thesis
    by (rule convex_polychainI)
      (simp_all add: polychain_half_segments_of_aform subsequent_half_segments_ccw
        ccw'_def[symmetric])
qed

lemma hd_distinct_neq_last: "distinct xs ⟹ length xs > 1 ⟹ hd xs ≠ last xs"
  by (metis One_nat_def add_Suc_right distinct.simps(2) last.simps last_in_set less_irrefl
    list.exhaust list.sel(1) list.size(3) list.size(4) add.right_neutral nat_neq_iff not_less0)

lemma ccw_hd_last_half_segments_dirvec:
  assumes "length (half_segments_of_aform X) > 1"
  shows "ccw' 0 (dirvec (hd (half_segments_of_aform X))) (dirvec (last (half_segments_of_aform X)))"
proof -
  let ?i = "ccw.selsort 0 (inl (snd X))"
  let ?s = "map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X)))"
  from assms have l: "1 < length (inl (snd X))" "inl (snd X) ≠ []"
    using assms by (auto simp add: half_segments_of_aform_def)
  hence "hd ?i ∈ set ?i" "last ?i ∈ set ?i"
    by (auto intro!: hd_in_set last_in_set simp del: ccw.set_selsort)
  hence "¬coll 0 (hd ?i) (last ?i)" using l
    by (intro inl_ncoll[of _ X]) (auto simp: hd_distinct_neq_last)
  hence "¬coll 0 (hd ?s) (last ?s)" using l
    by (auto simp: hd_map last_map)
  hence "ccw' 0 (hd (map ((*⇩R) 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))))
     (last (map ((*⇩R) 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))))"
    using assms
    by (auto simp add: half_segments_of_aform_def
      intro!: sorted_inl ccw_sorted_scaleR ccw.hd_last_sorted ccw_ncoll_imp_ccw)
  with assms show ?thesis
    by (auto simp add: half_segments_of_aform_def Let_def
        dirvec_hd_polychain_of dirvec_last_polychain_of length_greater_0_conv[symmetric]
      simp del: polychain_of.simps length_greater_0_conv
      split: if_split_asm)
qed

lemma map_fst_half_segments_aux_eq: "[] ≠ half_segments_of_aform X ⟹
    map fst (half_segments_of_aform X) =
      fst (hd (half_segments_of_aform X))#butlast (map snd (half_segments_of_aform X))"
  by (rule nth_equalityI)
    (auto simp: nth_Cons hd_conv_nth nth_butlast subsequent_half_segments split: nat.split)

lemma le_less_Suc_eq: "x - Suc 0 ≤ (i::nat) ⟹ i < x ⟹ x - Suc 0 = i"
  by simp

lemma map_snd_half_segments_aux_eq: "half_segments_of_aform X ≠ [] ⟹
    map snd (half_segments_of_aform X) =
      tl (map fst (half_segments_of_aform X)) @ [snd (last (half_segments_of_aform X))]"
  by (rule nth_equalityI)
    (auto simp: nth_Cons hd_conv_nth nth_append nth_tl subsequent_half_segments
      not_less last_conv_nth algebra_simps dest!: le_less_Suc_eq
    split: nat.split)

lemma ccw'_sortedP_snd_half_segments_of_aform:
  "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X))) (map snd (half_segments_of_aform X))"
  by (auto simp: half_segments_of_aform_def Let_def
    intro!: ccw'.sortedP.Cons ccw'_sortedP_polychain_of_snd ccw'_sortedP_scaled_inl)

lemma
  lex_half_segments_lowest_vertex:
  assumes "(c, d) ∈ set (half_segments_of_aform X)"
  shows "lex d (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  unfolding half_segments_of_aform_def Let_def
  by (rule lex_polychain_of_center[OF assms[unfolded half_segments_of_aform_def Let_def],
      unfolded snd_conv])
    (auto simp: list_all_iff lex_def dest!: in_set_inl_lex)

lemma
  lex_half_segments_lowest_vertex':
  assumes "d ∈ set (map snd (half_segments_of_aform X))"
  shows "lex d (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  using assms
  by (auto intro: lex_half_segments_lowest_vertex)

lemma
  lex_half_segments_last:
  assumes "(c, d) ∈ set (half_segments_of_aform X)"
  shows "lex (snd (last (half_segments_of_aform X))) d"
  using assms
  unfolding half_segments_of_aform_def Let_def
  by (rule lex_polychain_of_last) (auto simp: list_all_iff lex_def dest!: in_set_inl_lex)

lemma
  lex_half_segments_last':
  assumes "d ∈ set (map snd (half_segments_of_aform X))"
  shows "lex (snd (last (half_segments_of_aform X))) d"
  using assms
  by (auto intro: lex_half_segments_last)

lemma
  ccw'_half_segments_lowest_last:
  assumes set_butlast: "(c, d) ∈ set (butlast (half_segments_of_aform X))"
  assumes ne: "inl (snd X) ≠ []"
  shows "ccw' (lowest_vertex (fst X, nlex_pdevs (snd X))) d (snd (last (half_segments_of_aform X)))"
  using set_butlast
  unfolding half_segments_of_aform_def Let_def
  by (rule ccw'_polychain_of_sorted_center_last) (auto simp: ne ccw'_sortedP_scaled_inl)

lemma distinct_fst_half_segments:
  "distinct (map fst (half_segments_of_aform X))"
  by (auto simp: half_segments_of_aform_def list_all_iff lex_scale1_zero
    simp del: scaleR_Pair
    intro!: distinct_fst_polychain_of
    dest: in_set_inl_nonzero in_set_inl_lex)

lemma distinct_snd_half_segments:
  "distinct (map snd (half_segments_of_aform X))"
  by (auto simp: half_segments_of_aform_def list_all_iff lex_scale1_zero
    simp del: scaleR_Pair
    intro!: distinct_snd_polychain_of
    dest: in_set_inl_nonzero in_set_inl_lex)


subsection ‹Mirror›

definition "mirror_point x y = 2 *⇩R x - y"

lemma ccw'_mirror_point3[simp]:
  "ccw' (mirror_point x y) (mirror_point x z) (mirror_point x w) ⟷ ccw' y z w "
  by (auto simp: mirror_point_def det3_def' ccw'_def algebra_simps)

lemma mirror_point_self_inverse[simp]:
  fixes x::"'a::real_vector"
  shows "mirror_point p (mirror_point p x) = x"
  by (auto simp: mirror_point_def scaleR_2)

lemma mirror_half_segments_of_aform:
  assumes "e ∈ UNIV → {-1 <..< 1}"
  assumes "length (half_segments_of_aform X) ≠ 1"
  shows "list_all (λseg. ccw' (fst seg) (snd seg) (aform_val e X))
      (map (pairself (mirror_point (fst X))) (half_segments_of_aform X))"
  unfolding list_all_length
proof safe
  let ?m = "map (pairself (mirror_point (fst X))) (half_segments_of_aform X)"
  fix n assume "n < length ?m"
  hence "ccw' (fst (half_segments_of_aform X ! n)) (snd (half_segments_of_aform X ! n))
      (aform_val (- e) X)"
    using assms
    by (auto dest!: nth_mem intro!: half_segments_of_aform_strict)
  also have "aform_val (-e) X = 2 *⇩R fst X - aform_val e X"
    by (auto simp: aform_val_def pdevs_val_sum algebra_simps scaleR_2 sum_negf)
  finally have le:
    "ccw' (fst (half_segments_of_aform X ! n)) (snd (half_segments_of_aform X ! n))
      (2 *⇩R fst X - aform_val e X)"
    .

  have eq: "(map (pairself (mirror_point (fst X))) (half_segments_of_aform X) ! n) =
    (2 *⇩R fst X - fst ((half_segments_of_aform X) ! n),
     2 *⇩R fst X - snd ((half_segments_of_aform X) ! n))"
    using ‹n < length ?m›
    by (cases "half_segments_of_aform X ! n") (auto simp add: mirror_point_def)
  show "ccw' (fst (?m ! n)) (snd (?m ! n)) (aform_val e X)"
    using le
    unfolding eq
    by (auto simp: algebra_simps ccw'_def det3_def')
qed

lemma last_half_segments:
  assumes "half_segments_of_aform X ≠ []"
  shows "snd (last (half_segments_of_aform X)) =
    mirror_point (fst X) (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  using assms
  by (auto simp add: half_segments_of_aform_def Let_def lowest_vertex_def mirror_point_def scaleR_2
    scaleR_sum_list[symmetric] last_polychain_of sum_list_distinct_selsort inl_def
    sum_list_independent_pdevs sum_list_list_of_pdevs)

lemma convex_polychain_map_mirror:
  assumes "convex_polychain hs"
  shows "convex_polychain (map (pairself (mirror_point x)) hs)"
proof (rule convex_polychainI)
qed (insert assms, auto simp: convex_polychain_def polychain_map_pairself pairself_apply
  mirror_point_def det3_def' algebra_simps)

lemma ccw'_mirror_point0:
  "ccw' (mirror_point x y) z w ⟷ ccw' y (mirror_point x z) (mirror_point x w)"
  by (metis ccw'_mirror_point3 mirror_point_self_inverse)

lemma ccw'_sortedP_mirror:
  "ccw'.sortedP x0 (map (mirror_point p0) xs) ⟷ ccw'.sortedP (mirror_point p0 x0) xs"
  by (induct xs)
    (simp_all add: linorder_list0.sortedP.Nil linorder_list0.sortedP_Cons_iff ccw'_mirror_point0)

lemma ccw'_sortedP_mirror2:
  "ccw'.sortedP (mirror_point p0 x0) (map (mirror_point p0) xs) ⟷ ccw'.sortedP x0 xs"
  using ccw'_sortedP_mirror[of "mirror_point p0 x0" p0 xs]
  by simp

lemma map_mirror_o_snd_polychain_of_eq: "map (mirror_point x0 ∘ snd) (polychain_of y xs) =
  map snd (polychain_of (mirror_point x0 y) (map uminus xs))"
  by (induct xs arbitrary: x0 y) (auto simp: mirror_point_def o_def algebra_simps)

lemma lowest_vertex_eq_mirror_last:
  "half_segments_of_aform X ≠ [] ⟹
    (lowest_vertex (fst X, nlex_pdevs (snd X))) =
    mirror_point (fst X) (snd (last (half_segments_of_aform X)))"
  using last_half_segments[of X] by simp

lemma snd_last: "xs ≠ [] ⟹ snd (last xs) = last (map snd xs)"
  by (induct xs) auto

lemma mirror_point_snd_last_eq_lowest:
  "half_segments_of_aform X ≠ [] ⟹
    mirror_point (fst X) (last (map snd (half_segments_of_aform X))) =
      lowest_vertex (fst X, nlex_pdevs (snd X))"
  by (simp add: lowest_vertex_eq_mirror_last snd_last)

lemma lex_mirror_point: "lex (mirror_point x0 a) (mirror_point x0 b) ⟹ lex b a"
  by (auto simp: mirror_point_def lex_def)

lemma ccw'_mirror_point:
  "ccw' (mirror_point x0 a) (mirror_point x0 b)  (mirror_point x0 c) ⟹ ccw' a b c"
  by (auto simp: mirror_point_def)

lemma inj_mirror_point: "inj (mirror_point (x::'a::real_vector))"
  by (auto simp: mirror_point_def inj_on_def algebra_simps)

lemma
  distinct_map_mirror_point_eq:
  "distinct (map (mirror_point (x::'a::real_vector)) xs) = distinct xs"
  by (auto simp: distinct_map intro!: subset_inj_on[OF inj_mirror_point])

lemma eq_self_mirror_iff: fixes x::"'a::real_vector" shows "x = mirror_point y x ⟷ x = y"
  by (auto simp: mirror_point_def algebra_simps scaleR_2[symmetric])


subsection ‹Full Segments›

definition segments_of_aform::"point aform ⇒ (point * point) list"
  where "segments_of_aform X =
    (let hs = half_segments_of_aform X in hs @ map (pairself (mirror_point (fst X))) hs)"

lemma segments_of_aform_strict:
  assumes "e ∈ UNIV → {-1 <..< 1}"
  assumes "length (half_segments_of_aform X) ≠ 1"
  shows "list_all (λseg. ccw' (fst seg) (snd seg) (aform_val e X)) (segments_of_aform X)"
  using assms
  by (auto simp: segments_of_aform_def Let_def mirror_half_segments_of_aform
    half_segments_of_aform_strict_all)
  

lemma mirror_point_aform_val[simp]: "mirror_point (fst X) (aform_val e X) = aform_val (- e) X"
  by (auto simp: mirror_point_def aform_val_def pdevs_val_sum algebra_simps scaleR_2 sum_negf)

lemma
  in_set_segments_of_aform_aform_valE:
  assumes "(x2, y2) ∈ set (segments_of_aform X)"
  obtains e where "y2 = aform_val e X" "e ∈ UNIV → {-1 .. 1}"
  using assms
proof (auto simp: segments_of_aform_def Let_def)
  assume "(x2, y2) ∈ set (half_segments_of_aform X)"
  from in_set_half_segments_of_aform_aform_valE[OF this]
  obtain e where "y2 = aform_val e X" "e ∈ UNIV → {- 1..1}" by auto
  thus ?thesis ..
next
  fix a b aa ba
  assume "((a, b), aa, ba) ∈ set (half_segments_of_aform X)"
  from in_set_half_segments_of_aform_aform_valE[OF this]
  obtain e where e: "(aa, ba) = aform_val e X" "e ∈ UNIV → {- 1..1}" by auto
  assume "y2 = mirror_point (fst X) (aa, ba)"
  hence "y2 = aform_val (-e) X" "(-e) ∈ UNIV → {-1 .. 1}" using e by auto
  thus ?thesis ..
qed

lemma
  last_half_segments_eq_mirror_hd:
  assumes "half_segments_of_aform X ≠ []"
  shows "snd (last (half_segments_of_aform X)) = mirror_point (fst X) (fst (hd (half_segments_of_aform X)))"
  by (simp add: last_half_segments assms fst_hd_half_segments_of_aform)

lemma polychain_segments_of_aform: "polychain (segments_of_aform X)"
  by (auto simp: segments_of_aform_def Let_def polychain_half_segments_of_aform
    polychain_map_pairself last_half_segments_eq_mirror_hd hd_map pairself_apply
    intro!: polychain_appendI)

lemma segments_of_aform_closed:
  assumes "segments_of_aform X ≠ []"
  shows "fst (hd (segments_of_aform X)) = snd (last (segments_of_aform X))"
  using assms
  by (auto simp: segments_of_aform_def Let_def fst_hd_half_segments_of_aform last_map
    pairself_apply last_half_segments mirror_point_def)

lemma convex_polychain_segments_of_aform:
  assumes "1 < length (half_segments_of_aform X)"
  shows "convex_polychain (segments_of_aform X)"
  unfolding segments_of_aform_def Let_def
    using ccw_hd_last_half_segments_dirvec[OF assms]
  by (intro convex_polychain_appendI)
    (auto
      simp: convex_polychain_half_segments_of_aform convex_polychain_map_mirror dirvec_minus hd_map
        pairself_apply last_half_segments mirror_point_def fst_hd_half_segments_of_aform det3_def'
        algebra_simps ccw'_def
      intro!: polychain_appendI polychain_half_segments_of_aform polychain_map_pairself)

lemma convex_polygon_segments_of_aform:
  assumes "1 < length (half_segments_of_aform X)"
  shows "convex_polygon (segments_of_aform X)"
proof -
  from assms have hne: "half_segments_of_aform X ≠ []"
    by auto
  from convex_polychain_segments_of_aform[OF assms]
  have "convex_polychain (segments_of_aform X)" .
  thus ?thesis
    by (auto simp: convex_polygon_def segments_of_aform_closed)
qed

lemma
  previous_segments_of_aformE:
  assumes "(y, z) ∈ set (segments_of_aform X)"
  obtains x where "(x, y) ∈ set (segments_of_aform X)"
proof -
  from assms have ne[simp]: "segments_of_aform X ≠ []"
    by auto
  from assms
  obtain i where i: "i<length (segments_of_aform X)" "(segments_of_aform X) ! i = (y, z)"
    by (auto simp: in_set_conv_nth)
  show ?thesis
  proof (cases i)
    case 0
    with segments_of_aform_closed[of X] assms
    have "(fst (last (segments_of_aform X)), y) ∈ set (segments_of_aform X)"
      by (metis fst_conv hd_conv_nth i(2) last_in_set ne snd_conv surj_pair)
    thus ?thesis ..
  next
    case (Suc j)
    have "(fst (segments_of_aform X ! j), snd (segments_of_aform X ! j)) ∈
        set (segments_of_aform X)"
      using Suc i(1) by auto
    also
    from i have "y = fst (segments_of_aform X ! i)"
      by auto
    hence "snd (segments_of_aform X ! j) = y"
      using polychain_segments_of_aform[of X] i(1) Suc
      by (auto simp: polychain_def Suc)
    finally have "(fst (segments_of_aform X ! j), y) ∈ set (segments_of_aform X)" .
    thus ?thesis ..
  qed
qed

lemma fst_compose_pairself: "fst o pairself f = f o fst"
  and snd_compose_pairself: "snd o pairself f = f o snd"
  by (auto simp: pairself_apply)

lemma in_set_butlastI: "xs ≠ [] ⟹ x ∈ set xs ⟹ x ≠ last xs ⟹ x ∈ set (butlast xs)"
  by (induct xs) (auto split: if_splits)

lemma distinct_in_set_butlastD:
  "x ∈ set (butlast xs) ⟹ distinct xs ⟹ x ≠ last xs"
  by (induct xs) auto

lemma distinct_in_set_tlD:
  "x ∈ set (tl xs) ⟹ distinct xs ⟹ x ≠ hd xs"
  by (induct xs) auto

lemma ccw'_sortedP_snd_segments_of_aform:
  assumes "length (inl (snd X)) > 1"
  shows
    "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X)))
      (butlast (map snd (segments_of_aform X)))"
proof cases
  assume "[] = half_segments_of_aform X"
  from this show ?thesis
    by (simp add: segments_of_aform_def Let_def ccw'.sortedP.Nil)
next
  assume H: "[] ≠ half_segments_of_aform X"
  let ?m = "mirror_point (fst X)"
  have ne: "inl (snd X) ≠ []" using assms by auto
  have "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X)))
     (map snd (half_segments_of_aform X) @ butlast (map (?m ∘ snd)
    (half_segments_of_aform X)))"
  proof (rule ccw'.sortedP_appendI)
    show "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X))) (map snd (half_segments_of_aform X))"
      by (rule ccw'_sortedP_snd_half_segments_of_aform)
    have "butlast (map (?m ∘ snd) (half_segments_of_aform X)) =
      butlast
       (map (?m ∘ snd) (polychain_of (lowest_vertex (fst X, nlex_pdevs (snd X)))
         (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X))))))"
      by (simp add: half_segments_of_aform_def)
    also have "… =
       map snd
        (butlast
          (polychain_of (?m (lowest_vertex (fst X, nlex_pdevs (snd X))))
            (map uminus (map ((*⇩R) 2) (ccw.selsort 0 (inl (snd X)))))))"
      (is "_ = map snd (butlast (polychain_of ?x ?xs))")
      by (simp add: map_mirror_o_snd_polychain_of_eq map_butlast)
    also
    {
      have "ccw'.sortedP 0 ?xs"
        by (intro ccw'_sortedP_uminus ccw'_sortedP_scaled_inl)
      moreover
      have "ccw'.sortedP ?x (map snd (polychain_of ?x ?xs))"
        unfolding ccw'_sortedP_mirror[symmetric] map_map map_mirror_o_snd_polychain_of_eq
        by (auto simp add: o_def intro!: ccw'_sortedP_polychain_of_snd ccw'_sortedP_scaled_inl)
      ultimately
      have "ccw'.sortedP (snd (last (polychain_of ?x ?xs)))
          (map snd (butlast (polychain_of ?x ?xs)))"
        by (rule ccw'_sortedP_convex_rotate_aux)
    }
    also have "(snd (last (polychain_of ?x ?xs))) =
        ?m (last (map snd (half_segments_of_aform X)))"
      by (simp add: half_segments_of_aform_def ne map_mirror_o_snd_polychain_of_eq
         last_map[symmetric, where f="?m"]
         last_map[symmetric, where f="snd"])
    also have "… = lowest_vertex (fst X, nlex_pdevs (snd X))"
      using ne H
      by (auto simp: lowest_vertex_eq_mirror_last snd_last)
    finally show "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X)))
       (butlast (map (?m ∘ snd) (half_segments_of_aform X)))" .
  next
    fix x y
    assume seg: "x ∈ set (map snd (half_segments_of_aform X))"
      and mseg: "y ∈ set (butlast (map (?m ∘ snd) (half_segments_of_aform X)))"
    from seg assms have neq_Nil: "inl (snd X) ≠ []" "half_segments_of_aform X ≠ []"
      by auto

    from seg obtain a where a: "(a, x) ∈ set (half_segments_of_aform X)"
      by auto
    from mseg obtain b
    where mirror_y: "(b, ?m y) ∈ set (butlast (half_segments_of_aform X))"
      by (auto simp: map_butlast[symmetric])

    let ?l = "lowest_vertex (fst X, nlex_pdevs (snd X))"
    let ?ml = "?m ?l"

    have mirror_eq_last: "?ml = snd (last (half_segments_of_aform X))"
      using seg H
      by (intro last_half_segments[symmetric]) simp

    define r
      where "r = ?l + (0, abs (snd x - snd ?l) + abs (snd y - snd ?l) + abs (snd ?ml - snd ?l) + 1)"

    have d1: "x ≠ r" "y ≠ r" "?l ≠ r" "?ml ≠ r"
      by (auto simp: r_def plus_prod_def prod_eq_iff)
    have "distinct (map (?m ∘ snd) (half_segments_of_aform X))"
      unfolding map_comp_map[symmetric]
      unfolding o_def distinct_map_mirror_point_eq
      by (rule distinct_snd_half_segments)
    from distinct_in_set_butlastD[OF ‹y ∈ _› this]
    have "?l ≠ y"
      by (simp add: neq_Nil lowest_vertex_eq_mirror_last last_map)
    moreover have "?l ≠ ?ml"
      using neq_Nil by (auto simp add: eq_self_mirror_iff lowest_vertex_eq_center_iff inl_def)
    ultimately
    have d2: "?l ≠ y" "?l ≠ ?ml"
      by auto

    have *: "ccw' ?l (?m y) ?ml"
      by (metis mirror_eq_last ccw'_half_segments_lowest_last mirror_y neq_Nil(1))
    have "ccw' ?ml y ?l"
      by (rule ccw'_mirror_point[of "fst X"]) (simp add: *)
    hence lmy: "ccw' ?l ?ml y"
      by (simp add: ccw'_def det3_def' algebra_simps)
    let ?ccw = "ccw' (lowest_vertex (fst X, nlex_pdevs (snd X))) x y"
    {
      assume "x ≠ ?ml"
      hence x_butlast: "(a, x) ∈ set (butlast (half_segments_of_aform X))"
        unfolding mirror_eq_last
        using a
        by (auto intro!: in_set_butlastI simp: prod_eq_iff)
      have "ccw' ?l x ?ml"
        by (metis mirror_eq_last ccw'_half_segments_lowest_last x_butlast neq_Nil(1))
    } note lxml = this
    {
      assume "x = ?ml"
      hence ?ccw
        by (simp add: lmy)
    } moreover {
      assume "x ≠ ?ml" "y = ?ml"
      hence ?ccw
        by (simp add: lxml)
    } moreover {
      assume d3: "x ≠ ?ml" "y ≠ ?ml"

      from ‹x ∈ set _›
      have "x ∈ set (map snd (half_segments_of_aform X))" by force
      hence "x ∈ set (tl (map fst (half_segments_of_aform X)))"
        using d3
        unfolding map_snd_half_segments_aux_eq[OF neq_Nil(2)]
        by (auto simp: mirror_eq_last)
      from distinct_in_set_tlD[OF this distinct_fst_half_segments]
      have "?l ≠ x"
        by (simp add: fst_hd_half_segments_of_aform neq_Nil hd_map)

      from lxml[OF ‹x ≠ ?ml›] ‹ccw' ?l ?ml y›
      have d4: "x ≠ y"
        by (rule neq_left_right_of lxml)

      have "distinct5 x ?ml y r ?l"
        using d1 d2 ‹?l ≠ x› d3 d4
        by simp_all
      moreover
      note _
      moreover
      have "lex x ?l"
        by (rule lex_half_segments_lowest_vertex) fact
      hence "ccw ?l r x"
        unfolding r_def by (rule lex_ccw_left) simp
      moreover
      have "lex ?ml ?l"
        using last_in_set[OF H[symmetric]]
        by (auto simp: mirror_eq_last intro: lex_half_segments_lowest_vertex')
      hence "ccw ?l r ?ml"
        unfolding r_def by (rule lex_ccw_left) simp
      moreover
      have "lex (?m (lowest_vertex (fst X, nlex_pdevs (snd X)))) (?m y)"
        using mirror_y
        by (force dest!: in_set_butlastD intro: lex_half_segments_last' simp: mirror_eq_last )
      hence "lex y ?l"
        by (rule lex_mirror_point)
      hence "ccw ?l r y"
        unfolding r_def by (rule lex_ccw_left) simp
      moreover
      from ‹x ≠ ?ml› have "ccw ?l x ?ml"
        by (simp add: ccw_def lxml)
      moreover
      from lmy have "ccw ?l ?ml y"
        by (simp add: ccw_def)
      ultimately
      have "ccw ?l x y"
        by (rule ccw.transitive[where S=UNIV]) simp

      moreover
      {
        have "x ≠ ?l" using ‹?l ≠ x› by simp
        moreover
        have "lex (?m y) (?m ?ml)"
          using mirror_y
          by (force intro: lex_half_segments_lowest_vertex in_set_butlastD)
        hence "lex ?ml y"
          by (rule lex_mirror_point)
        moreover
        from a have "lex ?ml x"
          unfolding mirror_eq_last
          by (rule lex_half_segments_last)
        moreover note ‹lex y ?l› ‹lex x ?l› ‹ccw' ?l x ?ml› ‹ccw' ?l ?ml y›
        ultimately
        have ncoll: "¬ coll ?l x y"
          by (rule not_coll_ordered_lexI)
      }
      ultimately have ?ccw
        by (simp add: ccw_def)
    } ultimately show ?ccw
      by blast
  qed
  thus ?thesis using H
    by (simp add: segments_of_aform_def Let_def butlast_append snd_compose_pairself)
qed

lemma polychain_of_segments_of_aform1:
  assumes "length (segments_of_aform X) = 1"
  shows "False"
  using assms
  by (auto simp: segments_of_aform_def Let_def half_segments_of_aform_def add_is_1
    split: if_split_asm)

lemma polychain_of_segments_of_aform2:
  assumes "segments_of_aform X = [x, y]"
  assumes "between (fst x, snd x) p"
  shows "p ∈ convex hull set (map fst (segments_of_aform X))"
proof -
  from polychain_segments_of_aform[of X] segments_of_aform_closed[of X] assms
  have "fst y = snd x" "snd y = fst x" by (simp_all add: polychain_def)
  thus ?thesis
    using assms
    by (cases x) (auto simp: between_mem_convex_hull)
qed

lemma append_eq_2:
  assumes "length xs = length ys"
  shows "xs @ ys = [x, y] ⟷ xs = [x] ∧ ys = [y]"
  using assms
proof (cases xs)
  case (Cons z zs)
  thus ?thesis using assms by (cases zs) auto
qed simp

lemma segments_of_aform_line_segment:
  assumes "segments_of_aform X = [x, y]"
  assumes "e ∈ UNIV → {-1 .. 1}"
  shows "aform_val e X ∈ closed_segment (fst x) (snd x)"
proof -
  from pdevs_val_pdevs_of_list_inl2E[OF ‹e ∈ _›, of "snd X"]
  obtain e' where e': "pdevs_val e (snd X) = pdevs_val e' (pdevs_of_list (inl (snd X)))"
    "e' ∈ UNIV → {- 1..1}" .
  from e' have "0 ≤ 1 + e' 0" by (auto simp: Pi_iff dest!: spec[where x=0])
  with assms e' show ?thesis
    by (auto simp: segments_of_aform_def Let_def append_eq_2 half_segments_of_aform_def
        polychain_of_singleton_iff mirror_point_def ccw.selsort_singleton_iff lowest_vertex_def
        aform_val_def sum_list_nlex_eq_sum_list_inl closed_segment_def Pi_iff
      intro!: exI[where x="(1 + e' 0) / 2"])
      (auto simp: algebra_simps)
qed


subsection ‹Continuous Generalization›

lemma LIMSEQ_minus_fract_mult:
  "(λn. r * (1 - 1 / real (Suc (Suc n)))) ⇢ r"
  by (rule tendsto_eq_rhs[OF tendsto_mult[where a=r and b = 1]])
    (auto simp: inverse_eq_divide[symmetric] simp del: of_nat_Suc
      intro: filterlim_compose[OF LIMSEQ_inverse_real_of_nat filterlim_Suc] tendsto_eq_intros)

lemma det3_nonneg_segments_of_aform:
  assumes "e ∈ UNIV → {-1 .. 1}"
  assumes "length (half_segments_of_aform X) ≠ 1"
  shows "list_all (λseg. det3 (fst seg) (snd seg) (aform_val e X) ≥ 0) (segments_of_aform X)"
  unfolding list_all_iff
proof safe
  fix a b c d
  assume seg: "((a, b), c, d) ∈ set (segments_of_aform X)" (is "?seg ∈ _")
  define normal_of_segment
    where "normal_of_segment = (λ((a0, a1), b0, b1). (b1 - a1, a0 - b0)::real*real)"
  define support_of_segment
    where "support_of_segment = (λ(a, b). normal_of_segment (a, b) ∙ a)"
  have "closed ((λx. x ∙ normal_of_segment ?seg) -` {..support_of_segment ?seg})" (is "closed ?cl")
    by (auto intro!: continuous_intros closed_vimage)
  moreover
  define f where "f n i = e i * ( 1 - 1 / (Suc (Suc n)))" for n i
  have "∀n. aform_val (f n) X ∈ ?cl"
  proof
    fix n
    have "f n ∈ UNIV → {-1 <..< 1}"
      using assms
      by (auto simp: f_def Pi_iff intro!: less_one_multI minus_one_less_multI)
    from list_allD[OF segments_of_aform_strict[OF this assms(2)] seg]
    show "aform_val (f n) X ∈ (λx. x ∙ normal_of_segment ((a, b), c, d)) -`
        {..support_of_segment ((a, b), c, d)}"
      by (auto simp: list_all_iff normal_of_segment_def support_of_segment_def
        det3_def' field_simps inner_prod_def ccw'_def)
  qed
  moreover
  have "⋀i. (λn. f n i) ⇢ e i"
    unfolding f_def
    by (rule LIMSEQ_minus_fract_mult)
  hence "(λn. aform_val (f n) X) ⇢ aform_val e X"
    by (auto simp: aform_val_def pdevs_val_sum intro!: tendsto_intros)
  ultimately have "aform_val e X ∈ ?cl"
    by (meson closed_sequentially)
  thus "det3 (fst ?seg) (snd ?seg) (aform_val e X) ≥ 0"
    by (auto simp: list_all_iff normal_of_segment_def support_of_segment_def det3_def' field_simps
      inner_prod_def)
qed

lemma det3_nonneg_segments_of_aformI:
  assumes "e ∈ UNIV → {-1 .. 1}"
  assumes "length (half_segments_of_aform X) ≠ 1"
  assumes "seg ∈ set (segments_of_aform X)"
  shows "det3 (fst seg) (snd seg) (aform_val e X) ≥ 0"
  using assms det3_nonneg_segments_of_aform by (auto simp: list_all_iff)


subsection ‹Intersection of Vertical Line with Segment›

fun intersect_segment_xline'::"nat ⇒ point * point ⇒ real ⇒ point option"
  where "intersect_segment_xline' p ((x0, y0), (x1, y1)) xl =
    (if x0 ≤ xl ∧ xl ≤ x1 then
      if x0 = x1 then Some ((min y0 y1), (max y0 y1))
      else
        let
          yl = truncate_down p (truncate_down p (real_divl p (y1 - y0) (x1 - x0) * (xl - x0)) + y0);
          yr = truncate_up p (truncate_up p (real_divr p (y1 - y0) (x1 - x0) * (xl - x0)) + y0)
        in Some (yl, yr)
    else None)"

lemma norm_pair_fst0[simp]: "norm (0, x) = norm x"
  by (auto simp: norm_prod_def)

lemmas add_right_mono_le = order_trans[OF add_right_mono]
lemmas mult_right_mono_le = order_trans[OF mult_right_mono]

lemmas add_right_mono_ge = order_trans[OF _ add_right_mono]
lemmas mult_right_mono_ge = order_trans[OF _ mult_right_mono]

lemma dest_segment:
  fixes x b::real
  assumes "(x, b) ∈ closed_segment (x0, y0) (x1, y1)"
  assumes "x0 ≠ x1"
  shows "b = (y1 - y0) * (x - x0) / (x1 - x0) + y0"
proof -
  from assms obtain u where u: "x = x0 *⇩R (1 - u) + u * x1" "b = y0 *⇩R (1 - u) + u * y1" "0 ≤ u" "u ≤ 1"
    by (auto simp: closed_segment_def algebra_simps)
  show "b = (y1 - y0) * (x - x0) / (x1 - x0) + y0 "
    using assms by (auto simp: closed_segment_def field_simps u)
qed

lemma intersect_segment_xline':
  assumes "intersect_segment_xline' prec (p0, p1) x = Some (m, M)"
  shows "closed_segment p0 p1 ∩ {p. fst p = x} ⊆ {(x, m) .. (x, M)}"
  using assms
proof (cases p0)
  case (Pair x0 y0) note p0 = this
  show ?thesis
  proof (cases p1)
    case (Pair x1 y1) note p1 = this
    {
      assume "x0 = x1" "x = x1" "m = min y0 y1" "M = max y0 y1"
      hence ?thesis
        by (force simp: abs_le_iff p0 p1 min_def max_def algebra_simps dest: segment_bound
          split: if_split_asm)
    } thus ?thesis
      using assms
      by (auto simp: abs_le_iff p0 p1 split: if_split_asm
        intro!: truncate_up_le truncate_down_le
        add_right_mono_le[OF truncate_down]
        add_right_mono_le[OF real_divl]
        add_right_mono_le[OF mult_right_mono_le[OF real_divl]]
        add_right_mono_ge[OF _ truncate_up]
        add_right_mono_ge[OF _ mult_right_mono_ge[OF _ real_divr]]
        dest!: dest_segment)
  qed
qed

lemma
  in_segment_fst_le:
  fixes x0 x1 b::real
  assumes "x0 ≤ x1" "(x, b) ∈ closed_segment (x0, y0) (x1, y1)"
  shows "x ≤ x1"
  using assms using mult_left_mono[OF ‹x0 ≤ x1›, where c="1 - u" for u]
  by (force simp add: min_def max_def split: if_split_asm
    simp add: algebra_simps not_le closed_segment_def)

lemma
  in_segment_fst_ge:
  fixes x0 x1 b::real
  assumes "x0 ≤ x1" "(x, b) ∈ closed_segment (x0, y0) (x1, y1)"
  shows "x0 ≤ x"
  using assms using mult_left_mono[OF ‹x0 ≤ x1›]
  by (force simp add: min_def max_def split: if_split_asm
    simp add: algebra_simps not_le closed_segment_def)

lemma intersect_segment_xline'_eq_None:
  assumes "intersect_segment_xline' prec (p0, p1) x = None"
  assumes "fst p0 ≤ fst p1"
  shows "closed_segment p0 p1 ∩ {p. fst p = x} = {}"
  using assms
  by (cases p0, cases p1)
    (auto simp: abs_le_iff split: if_split_asm dest: in_segment_fst_le in_segment_fst_ge)

fun intersect_segment_xline
  where "intersect_segment_xline prec ((a, b), (c, d)) x =
  (if a ≤ c then intersect_segment_xline' prec ((a, b), (c, d)) x
  else intersect_segment_xline' prec ((c, d), (a, b)) x)"

lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
  by (meson convex_contains_segment convex_closed_segment dual_order.antisym ends_in_segment)

lemma intersect_segment_xline:
  assumes "intersect_segment_xline prec (p0, p1) x = Some (m, M)"
  shows "closed_segment p0 p1 ∩ {p. fst p = x} ⊆ {(x, m) .. (x, M)}"
  using assms
  by (cases p0, cases p1)
    (auto simp: closed_segment_commute split: if_split_asm simp del: intersect_segment_xline'.simps
      dest!: intersect_segment_xline')

lemma intersect_segment_xline_fst_snd:
  assumes "intersect_segment_xline prec seg x = Some (m, M)"
  shows "closed_segment (fst seg) (snd seg) ∩ {p. fst p = x} ⊆ {(x, m) .. (x, M)}"
  using intersect_segment_xline[of prec "fst seg" "snd seg" x m M] assms
  by simp

lemma intersect_segment_xline_eq_None:
  assumes "intersect_segment_xline prec (p0, p1) x = None"
  shows "closed_segment p0 p1 ∩ {p. fst p = x} = {}"
  using assms
  by (cases p0, cases p1)
     (auto simp: closed_segment_commute split: if_split_asm simp del: intersect_segment_xline'.simps
      dest!: intersect_segment_xline'_eq_None)

lemma inter_image_empty_iff: "(X ∩ {p. f p = x} = {}) ⟷ (x ∉ f ` X)"
  by auto

lemma fst_closed_segment[simp]: "fst ` closed_segment a b = closed_segment (fst a) (fst b)"
  by (force simp: closed_segment_def)

lemma intersect_segment_xline_eq_empty:
  fixes p0 p1::"real * real"
  assumes "closed_segment p0 p1 ∩ {p. fst p = x} = {}"
  shows "intersect_segment_xline prec (p0, p1) x = None"
  using assms
  by (cases p0, cases p1)
    (auto simp: inter_image_empty_iff closed_segment_eq_real_ivl split: if_split_asm)

lemma intersect_segment_xline_le:
  assumes "intersect_segment_xline prec y xl = Some (m0, M0)"
  shows "m0 ≤ M0"
  using assms
  by (cases y) (auto simp: min_def split: if_split_asm intro!: truncate_up_le truncate_down_le
    order_trans[OF real_divl] order_trans[OF _ real_divr] mult_right_mono)

lemma intersect_segment_xline_None_iff:
  fixes p0 p1::"real * real"
  shows "intersect_segment_xline prec (p0, p1) x = None ⟷ closed_segment p0 p1 ∩ {p. fst p = x} = {}"
  by (auto intro!: intersect_segment_xline_eq_empty dest!: intersect_segment_xline_eq_None)


subsection ‹Bounds on Vertical Intersection with Oriented List of Segments›

primrec bound_intersect_2d where
  "bound_intersect_2d prec [] x = None"
| "bound_intersect_2d prec (X # Xs) xl =
    (case bound_intersect_2d prec Xs xl of
      None ⇒ intersect_segment_xline prec X xl
    | Some (m, M) ⇒
      (case intersect_segment_xline prec X xl of
        None ⇒ Some (m, M)
      | Some (m', M') ⇒ Some (min m' m, max M' M)))"

lemma
  bound_intersect_2d_eq_None:
  assumes "bound_intersect_2d prec Xs x = None"
  assumes "X ∈ set Xs"
  shows "intersect_segment_xline prec X x = None"
  using assms by (induct Xs) (auto split: option.split_asm)

lemma bound_intersect_2d_upper:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  obtains X m' where "X ∈ set Xs" "intersect_segment_xline prec X x = Some (m', M)"
    "⋀X m' M' . X ∈ set Xs ⟹ intersect_segment_xline prec X x = Some (m', M') ⟹ M' ≤ M"
proof atomize_elim
  show "∃X m'. X ∈ set Xs ∧ intersect_segment_xline prec X x = Some (m', M) ∧
    (∀X m' M'. X ∈ set Xs ⟶ intersect_segment_xline prec X x = Some (m', M') ⟶ M' ≤ M)"
    using assms
  proof (induct Xs arbitrary: m M)
    case Nil thus ?case by (simp add: bound_intersect_2d_def)
  next
    case (Cons X Xs)
    show ?case
    proof (cases "bound_intersect_2d prec Xs x")
      case None
      thus ?thesis using Cons
        by (intro exI[where x=X] exI[where x=m])
          (simp del: intersect_segment_xline.simps add: bound_intersect_2d_eq_None)
    next
      case (Some mM)
      note Some1=this
      then obtain m' M' where mM: "mM = (m', M')" by (cases mM)
      from Cons(1)[OF Some[unfolded mM]]
      obtain X' m'' where X': "X' ∈ set Xs"
        and m'': "intersect_segment_xline prec X' x = Some (m'', M')"
        and max: "⋀X m' M'a. X ∈ set Xs ⟹ intersect_segment_xline prec X x = Some (m', M'a) ⟹
          M'a ≤ M'"
        by auto
      show ?thesis
      proof (cases "intersect_segment_xline prec X x")
        case None thus ?thesis using Some1 mM Cons(2) X' m'' max
          by (intro exI[where x= X'] exI[where x= m''])
            (auto simp del: intersect_segment_xline.simps split: option.split_asm)
      next
        case (Some mM''')
        thus ?thesis using Some1 mM Cons(2) X' m''
          by (cases mM''')
            (force simp: max_def min_def simp del: intersect_segment_xline.simps
              split: option.split_asm if_split_asm dest!: max
              intro!: exI[where x= "if M' ≥ snd mM''' then X' else X"]
              exI[where x= "if M' ≥ snd mM''' then m'' else fst mM'''"])
      qed
    qed
  qed
qed

lemma bound_intersect_2d_lower:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  obtains X M' where "X ∈ set Xs" "intersect_segment_xline prec X x = Some (m, M')"
    "⋀X m' M' . X ∈ set Xs ⟹ intersect_segment_xline prec X x = Some (m', M') ⟹ m ≤ m'"
proof atomize_elim
  show "∃X M'. X ∈ set Xs ∧ intersect_segment_xline prec X x = Some (m, M') ∧
    (∀X m' M'. X ∈ set Xs ⟶ intersect_segment_xline prec X x = Some (m', M') ⟶ m ≤ m')"
    using assms
  proof (induct Xs arbitrary: m M)
    case Nil thus ?case by (simp add: bound_intersect_2d_def)
  next
    case (Cons X Xs)
    show ?case
    proof (cases "bound_intersect_2d prec Xs x")
      case None
      thus ?thesis using Cons
        by (intro exI[where x= X])
          (simp del: intersect_segment_xline.simps add: bound_intersect_2d_eq_None)
    next
      case (Some mM)
      note Some1=this
      then obtain m' M' where mM: "mM = (m', M')" by (cases mM)
      from Cons(1)[OF Some[unfolded mM]]
      obtain X' M'' where X': "X' ∈ set Xs"
        and M'': "intersect_segment_xline prec X' x = Some (m', M'')"
        and min: "⋀X m'a M'. X ∈ set Xs ⟹ intersect_segment_xline prec X x = Some (m'a, M') ⟹
          m' ≤ m'a"
        by auto
      show ?thesis
      proof (cases "intersect_segment_xline prec X x")
        case None thus ?thesis using Some1 mM Cons(2) X' M'' min
          by (intro exI[where x= X'] exI[where x= M''])
            (auto simp del: intersect_segment_xline.simps split: option.split_asm)
      next
        case (Some mM''')
        thus ?thesis using Some1 mM Cons(2) X' M'' min
          by (cases mM''')
            (force simp: max_def min_def
              simp del: intersect_segment_xline.simps
              split: option.split_asm if_split_asm
              dest!: min
              intro!: exI[where x= "if m' ≤ fst mM''' then X' else X"]
                exI[where x= "if m' ≤ fst mM''' then M'' else snd mM'''"])
      qed
    qed
  qed
qed

lemma bound_intersect_2d:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  shows "(⋃(p1, p2) ∈ set Xs. closed_segment p1 p2) ∩ {p. fst p = x} ⊆ {(x, m) .. (x, M)}"
proof (clarsimp, safe)
  fix b x0 y0 x1 y1
  assume H: "((x0, y0), x1, y1) ∈ set Xs" "(x, b) ∈ closed_segment (x0, y0) (x1, y1)"
  hence "intersect_segment_xline prec ((x0, y0), x1, y1) x ≠ None"
    by (intro notI)
      (auto dest!: intersect_segment_xline_eq_None simp del: intersect_segment_xline.simps)
  then obtain e f where ef: "intersect_segment_xline prec ((x0, y0), x1, y1) x = Some (e, f)"
    by auto
  with H have "m ≤ e"
    by (auto intro: bound_intersect_2d_lower[OF assms])
  also have "… ≤ b"
    using intersect_segment_xline[OF ef] H
    by force
  finally show "m ≤ b" .
  have "b ≤ f"
    using intersect_segment_xline[OF ef] H
    by force
  also have "… ≤ M"
    using H ef by (auto intro: bound_intersect_2d_upper[OF assms])
  finally show "b ≤ M" .
qed

lemma bound_intersect_2d_eq_None_iff:
  "bound_intersect_2d prec Xs x = None ⟷ (∀X∈set Xs. intersect_segment_xline prec X x = None)"
  by (induct Xs) (auto simp: split: option.split_asm)

lemma bound_intersect_2d_nonempty:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  shows "(⋃(p1, p2) ∈ set Xs. closed_segment p1 p2) ∩ {p. fst p = x} ≠ {}"
proof -
  from assms have "bound_intersect_2d prec Xs x ≠ None" by simp
  then obtain p1 p2 where "(p1, p2) ∈ set Xs" "intersect_segment_xline prec (p1, p2) x ≠ None"
    unfolding bound_intersect_2d_eq_None_iff by auto
  hence "closed_segment p1 p2 ∩ {p. fst p = x} ≠ {}"
    by (simp add: intersect_segment_xline_None_iff)
  thus ?thesis using ‹(p1, p2) ∈ set Xs› by auto
qed

lemma bound_intersect_2d_le:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)" shows "m ≤ M"
proof -
  from bound_intersect_2d_nonempty[OF assms] bound_intersect_2d[OF assms]
  show "m ≤ M" by auto
qed


subsection ‹Bounds on Vertical Intersection with General List of Segments›

definition "bound_intersect_2d_ud prec X xl =
  (case segments_of_aform X of
    [] ⇒ if fst (fst X) = xl then let m = snd (fst X) in Some (m, m) else None
  | [x, y] ⇒ intersect_segment_xline prec x xl
  | xs ⇒
    (case bound_intersect_2d prec (filter (λ((x1, y1), x2, y2). x1 < x2) xs) xl of
      Some (m, M') ⇒
      (case bound_intersect_2d prec (filter (λ((x1, y1), x2, y2). x1 > x2) xs) xl of
        Some (m', M) ⇒ Some (min m m', max M M')
      | None ⇒ None)
    | None ⇒ None))"

lemma list_cases4:
  "⋀x P. (x = [] ⟹ P) ⟹ (⋀y. x = [y] ⟹ P) ⟹
    (⋀y z. x = [y, z] ⟹ P) ⟹
    (⋀w y z zs. x = w # y # z # zs ⟹ P) ⟹ P"
  by (metis list.exhaust)

lemma bound_intersect_2d_ud_segments_of_aform_le:
  "bound_intersect_2d_ud prec X xl = Some (m0, M0) ⟹ m0 ≤ M0"
  by (cases "segments_of_aform X" rule: list_cases4)
    (auto simp: Let_def bound_intersect_2d_ud_def min_def max_def intersect_segment_xline_le
      if_split_eq1 split: option.split_asm prod.split_asm list.split_asm
      dest!: bound_intersect_2d_le)

lemma pdevs_domain_eq_empty_iff[simp]: "pdevs_domain (snd X) = {} ⟷ snd X = zero_pdevs"
  by (auto simp: intro!: pdevs_eqI)

lemma ccw_contr_on_line_left:
  assumes "det3 (a, b) (x, c) (x, d) ≥ 0" "a > x"
  shows "d ≤ c"
proof -
  from assms have "d * (a - x) ≤ c * (a - x)"
    by (auto simp: det3_def' algebra_simps)
  with assms show "c ≥ d" by auto
qed

lemma ccw_contr_on_line_right:
  assumes "det3 (a, b) (x, c) (x, d) ≥ 0" "a < x"
  shows "d ≥ c"
proof -
  from assms have "c * (x - a) ≤ d * (x - a)"
    by (auto simp: det3_def' algebra_simps)
  with assms show "d ≥ c" by auto
qed

lemma singleton_contrE:
  assumes "⋀x y. x ≠ y ⟹ x ∈ X ⟹ y ∈ X ⟹ False"
  assumes "X ≠ {}"
  obtains x where "X = {x}"
  using assms by blast

lemma segment_intersection_singleton:
  fixes xl and a b::"real * real"
  defines "i ≡ closed_segment a b ∩ {p. fst p = xl}"
  assumes ne1: "fst a ≠ fst b"
  assumes upper: "i ≠ {}"
  obtains p1 where "i = {p1}"
proof (rule singleton_contrE[OF _ upper])
  fix x y assume H: "x ≠ y" "x ∈ i" "y ∈ i"
  then obtain u v where uv: "x = u *⇩R b + (1 - u) *⇩R a" "y = v *⇩R b + (1 - v) *⇩R a"
    "0 ≤ u" "u ≤ 1" "0 ≤ v" "v ≤ 1"
    by (auto simp add: closed_segment_def i_def field_simps)
  then have "x + u *⇩R a = a + u *⇩R b" "y + v *⇩R a = a + v *⇩R b"
    by simp_all
  then have "fst (x + u *⇩R a) = fst (a + u *⇩R b)" "fst (y + v *⇩R a) = fst (a + v *⇩R b)"
    by simp_all
  then have "u = v * (fst a - fst b) / (fst a - fst b)"
    using ne1 H(2,3) ‹0 ≤ u› ‹u ≤ 1› ‹0 ≤ v› ‹v ≤ 1›
    by (simp add: closed_segment_def i_def field_simps)
  then have "u = v"
    by (simp add: ne1)
  then show False using H uv
    by simp
qed

lemma bound_intersect_2d_ud_segments_of_aform:
  assumes "bound_intersect_2d_ud prec X xl = Some (m0, M0)"
  assumes "e ∈ UNIV → {-1 .. 1}"
  shows "{aform_val e X} ∩ {x. fst x = xl} ⊆ {(xl, m0) .. (xl, M0)}"
proof safe
  fix a b
  assume safeassms: "(a, b) = aform_val e X" "xl = fst (a, b)"
  hence fst_aform_val: "fst (aform_val e X) = xl"
    by simp
  {
    assume len: "length (segments_of_aform X) > 2"
    with assms obtain m M m' M'
    where lb: "bound_intersect_2d prec
        [((x1, y1), x2, y2)←segments_of_aform X . x1 < x2] xl = Some (m, M')"
      and ub: "bound_intersect_2d prec
        [((x1, y1), x2, y2)←segments_of_aform X . x2 < x1] xl = Some (m', M)"
      and minmax: "m0 = min m m'" "M0 = max M M'"
      by (auto simp: bound_intersect_2d_ud_def split: option.split_asm list.split_asm )
    from bound_intersect_2d_upper[OF ub] obtain X1 m1
    where upper:
      "X1 ∈ set [((x1, y1), x2, y2)←segments_of_aform X . x2 < x1]"
      "intersect_segment_xline prec X1 xl = Some (m1, M)"
      by metis
    from bound_intersect_2d_lower[OF lb] obtain X2 M2
    where lower:
      "X2 ∈ set [((x1, y1), x2, y2)←segments_of_aform X . x1 < x2]"
      "intersect_segment_xline prec X2 xl = Some (m, M2)"
      by metis
    from upper(1) lower(1)
    have X1: "X1 ∈ set (segments_of_aform X)" "fst (fst X1) > fst (snd X1)"
      and X2: "X2 ∈ set (segments_of_aform X)" "fst (fst X2) < fst (snd X2)"
      by auto
    note upper_seg = intersect_segment_xline_fst_snd[OF upper(2)]
    note lower_seg = intersect_segment_xline_fst_snd[OF lower(2)]
    from len have lh: "length (half_segments_of_aform X) ≠ 1"
      by (auto simp: segments_of_aform_def Let_def)
    from X1 have ne1: "fst (fst X1) ≠ fst (snd X1)"
      by simp
    moreover have "closed_segment (fst X1) (snd X1) ∩ {p. fst p = xl} ≠ {}"
      using upper(2)
      by (simp add: intersect_segment_xline_None_iff[of prec, symmetric])
    ultimately obtain p1 where p1: "closed_segment (fst X1) (snd X1) ∩ {p. fst p = xl} = {p1}"
      by (rule segment_intersection_singleton)
    then obtain u where u: "p1 = (1 - u) *⇩R fst X1 + u *⇩R (snd X1)" "0 ≤ u" "u ≤ 1"
      by (auto simp: closed_segment_def algebra_simps)
    have coll1: "det3 (fst X1) p1 (aform_val e X) ≥ 0"
      and coll1': "det3 p1 (snd X1) (aform_val e X) ≥ 0"
      unfolding atomize_conj
      using u
      by (cases "u = 0 ∨ u = 1")
        (auto simp: u(1) intro: det3_nonneg_scaleR_segment1 det3_nonneg_scaleR_segment2
          det3_nonneg_segments_of_aformI[OF ‹e ∈ _› lh X1(1)])

    from X2 have ne2: "fst (fst X2) ≠ fst (snd X2)" by simp
    moreover
    have "closed_segment (fst X2) (snd X2) ∩ {p. fst p = xl} ≠ {}"
      using lower(2)
      by (simp add: intersect_segment_xline_None_iff[of prec, symmetric])
    ultimately
    obtain p2 where p2: "closed_segment (fst X2) (snd X2) ∩ {p. fst p = xl} = {p2}"
      by (rule segment_intersection_singleton)
    then obtain v where v: "p2 = (1 - v) *⇩R fst X2 + v *⇩R (snd X2)" "0 ≤ v" "v ≤ 1"
      by (auto simp: closed_segment_def algebra_simps)
    have coll2: "det3 (fst X2) p2 (aform_val e X) ≥ 0"
      and coll2': "det3 p2 (snd X2) (aform_val e X) ≥ 0"
      unfolding atomize_conj
      using v
      by (cases "v = 0 ∨ v = 1")
        (auto simp: v(1) intro: det3_nonneg_scaleR_segment1 det3_nonneg_scaleR_segment2
          det3_nonneg_segments_of_aformI[OF ‹e ∈ _› lh X2(1)])

    from in_set_segments_of_aform_aform_valE
        [of "fst X1" "snd X1" X, unfolded prod.collapse, OF X1(1)]
    obtain e1s where e1s: "snd X1 = aform_val e1s X" "e1s ∈ UNIV → {- 1..1}" .
    from previous_segments_of_aformE
        [of "fst X1" "snd X1" X, unfolded prod.collapse, OF X1(1)]
    obtain fX0 where "(fX0, fst X1) ∈ set (segments_of_aform X)" .
    from in_set_segments_of_aform_aform_valE[OF this]
    obtain e1f where e1f: "fst X1 = aform_val e1f X" "e1f ∈ UNIV → {- 1..1}" .
    have "p1 ∈ closed_segment (aform_val e1f X) (aform_val e1s X)"
      using p1 by (auto simp: e1s e1f)
    with segment_in_aform_val[OF e1s(2) e1f(2), of X]
    obtain ep1 where ep1: "ep1 ∈ UNIV → {-1 .. 1}" "p1 = aform_val ep1 X"
      by (auto simp: Affine_def valuate_def closed_segment_commute)

    from in_set_segments_of_aform_aform_valE
        [of "fst X2" "snd X2" X, unfolded prod.collapse, OF X2(1)]
    obtain e2s where e2s: "snd X2 = aform_val e2s X" "e2s ∈ UNIV → {- 1..1}" .
    from previous_segments_of_aformE
        [of "fst X2" "snd X2" X, unfolded prod.collapse, OF X2(1)]
    obtain fX02 where "(fX02, fst X2) ∈ set (segments_of_aform X)" .
    from in_set_segments_of_aform_aform_valE[OF this]
    obtain e2f where e2f: "fst X2 = aform_val e2f X" "e2f ∈ UNIV → {- 1..1}" .
    have "p2 ∈ closed_segment (aform_val e2f X) (aform_val e2s X)"
      using p2 by (auto simp: e2s e2f)
    with segment_in_aform_val[OF e2f(2) e2s(2), of X]
    obtain ep2 where ep2: "ep2 ∈ UNIV → {-1 .. 1}" "p2 = aform_val ep2 X"
      by (auto simp: Affine_def valuate_def)

    from det3_nonneg_segments_of_aformI[OF ep2(1), of X "(fst X1, snd X1)", unfolded prod.collapse,
        OF lh X1(1), unfolded ep2(2)[symmetric]]
    have c2: "det3 (fst X1) (snd X1) p2 ≥ 0" .
    hence c12: "det3 (fst X1) p1 p2 ≥ 0"
      using u by (cases "u = 0") (auto simp: u(1) det3_nonneg_scaleR_segment2)
    from det3_nonneg_segments_of_aformI[OF ep1(1), of X "(fst X2, snd X2)", unfolded prod.collapse,
        OF lh X2(1), unfolded ep1(2)[symmetric]]
    have c1: "det3 (fst X2) (snd X2) p1 ≥ 0" .
    hence c21: "det3 (fst X2) p2 p1 ≥ 0"
      using v by (cases "v = 0") (auto simp: v(1) det3_nonneg_scaleR_segment2)
    from p1 p2 have p1p2xl: "fst p1 = xl" "fst p2 = xl"
      by (auto simp: det3_def')
    from upper_seg p1 have "snd p1 ≤ M" by (auto simp: less_eq_prod_def)
    from lower_seg p2 have "m ≤ snd p2" by (auto simp: less_eq_prod_def)

    {
      have *: "(fst p1, snd (aform_val e X)) = aform_val e X"
        by (simp add: prod_eq_iff p1p2xl fst_aform_val)
      hence coll:
        "det3 (fst (fst X1), snd (fst X1)) (fst p1, snd p1) (fst p1, snd (aform_val e X)) ≥ 0"
        and coll':
        "det3 (fst (snd X1), snd (snd X1)) (fst p1, snd (aform_val e X)) (fst p1, snd p1) ≥ 0"
        using coll1 coll1'
        by (auto simp: det3_rotate)
      have "snd (aform_val e X) ≤ M"
      proof (cases "fst (fst X1) = xl")
        case False
        have "fst (fst X1) ≥ fst p1"
          unfolding u using X1
          by (auto simp: algebra_simps intro!: mult_left_mono u)
        moreover
        have "fst (fst X1) ≠ fst p1"
          using False
          by (simp add: p1p2xl)
        ultimately
        have "fst (fst X1) > fst p1" by simp
        from ccw_contr_on_line_left[OF coll this]
        show ?thesis using ‹snd p1 ≤ M› by simp
      next
        case True
        have "fst (snd X1) * (1 - u) ≤ fst (fst X1) * (1 - u)"
          using X1 u
          by (auto simp: intro!: mult_right_mono)
        hence "fst (snd X1) ≤ fst p1"
          unfolding u by (auto simp: algebra_simps)
        moreover
        have "fst (snd X1) ≠ fst p1"
          using True ne1
          by (simp add: p1p2xl)
        ultimately
        have "fst (snd X1) < fst p1" by simp
        from ccw_contr_on_line_right[OF coll' this]
        show ?thesis using ‹snd p1 ≤ M› by simp
      qed
    } moreover {
      have "(fst p2, snd (aform_val e X)) = aform_val e X"
        by (simp add: prod_eq_iff p1p2xl fst_aform_val)
      hence coll:
        "det3 (fst (fst X2), snd (fst X2)) (fst p2, snd p2) (fst p2, snd (aform_val e X)) ≥ 0"
        and coll':
        "det3 (fst (snd X2), snd (snd X2)) (fst p2, snd (aform_val e X)) (fst p2, snd p2) ≥ 0"
        using coll2 coll2'
        by (auto simp: det3_rotate)
      have "m ≤ snd (aform_val e X)"
      proof (cases "fst (fst X2) = xl")
        case False
        have "fst (fst X2) ≤ fst p2"
          unfolding v using X2
          by (auto simp: algebra_simps intro!: mult_left_mono v)
        moreover
        have "fst (fst X2) ≠ fst p2"
          using False
          by (simp add: p1p2xl)
        ultimately
        have "fst (fst X2) < fst p2" by simp
        from ccw_contr_on_line_right[OF coll this]
        show ?thesis using ‹m ≤ snd p2› by simp
      next
        case True
        have "(1 - v) * fst (snd X2) ≥ (1 - v) * fst (fst X2)"
          using X2 v
          by (auto simp: intro!: mult_left_mono)
        hence "fst (snd X2) ≥ fst p2"
          unfolding v by (auto simp: algebra_simps)
        moreover
        have "fst (snd X2) ≠ fst p2"
          using True ne2
          by (simp add: p1p2xl)
        ultimately
        have "fst (snd X2) > fst p2" by simp
        from ccw_contr_on_line_left[OF coll' this]
        show ?thesis using ‹m ≤ snd p2› by simp
      qed
    } ultimately have "aform_val e X ∈ {(xl, m) .. (xl, M)}"
      by (auto simp: less_eq_prod_def fst_aform_val)
    hence "aform_val e X ∈ {(xl, m0) .. (xl, M0)}"
      by (auto simp: minmax less_eq_prod_def)
  } moreover {
    assume "length (segments_of_aform X) = 2"
    then obtain a b where s: "segments_of_aform X = [a, b]"
      by (auto simp: numeral_2_eq_2 length_Suc_conv)
    from segments_of_aform_line_segment[OF this assms(2)]
    have "aform_val e X ∈ closed_segment (fst a) (snd a)" .
    moreover
    from assms
    have "intersect_segment_xline prec a xl = Some (m0, M0)"
      by (auto simp: bound_intersect_2d_ud_def s)
    note intersect_segment_xline_fst_snd[OF this]
    ultimately
    have "aform_val e X ∈ {(xl, m0) .. (xl, M0)}"
      by (auto simp: less_eq_prod_def fst_aform_val)
  } moreover {
    assume "length (segments_of_aform X) = 1"
    from polychain_of_segments_of_aform1[OF this]
    have "aform_val e X ∈ {(xl, m0) .. (xl, M0)}" by auto
  } moreover {
    assume len: "length (segments_of_aform X) = 0"
    hence "independent_pdevs (map snd (list_of_pdevs (nlex_pdevs (snd X)))) = []"
      by (simp add: segments_of_aform_def Let_def half_segments_of_aform_def inl_def)
    hence "snd X = zero_pdevs"
      by (subst (asm) independent_pdevs_eq_Nil_iff) (auto simp: list_all_iff list_of_pdevs_def)
    hence "aform_val e X = fst X"
      by (simp add: aform_val_def)
    with len assms have "aform_val e X ∈ {(xl, m0) .. (xl, M0)}"
      by (auto simp: bound_intersect_2d_ud_def Let_def split: if_split_asm)
  } ultimately have "aform_val e X ∈ {(xl, m0)..(xl, M0)}"
    by arith
  thus "(a, b) ∈ {(fst (a, b), m0)..(fst (a, b), M0)}"
    using safeassms
    by simp
qed


subsection ‹Approximation from Orthogonal Directions›

definition inter_aform_plane_ortho::
  "nat ⇒ 'a::executable_euclidean_space aform ⇒ 'a ⇒ real ⇒ 'a aform option"
  where
  "inter_aform_plane_ortho p Z n g = do {
    mMs ← those (map (λb. bound_intersect_2d_ud p (inner2_aform Z n b) g) Basis_list);
    let l = (∑(b, m)←zip Basis_list (map fst mMs). m *⇩R b);
    let u = (∑(b, M)←zip Basis_list (map snd mMs). M *⇩R b);
    Some (aform_of_ivl l u)
  }"

lemma
  those_eq_SomeD:
  assumes "those (map f xs) = Some ys"
  shows "ys = map (the o f) xs ∧ (∀i.∃y. i < length xs ⟶ f (xs ! i) = Some y)"
  using assms
  by (induct xs arbitrary: ys) (auto split: option.split_asm simp: o_def nth_Cons split: nat.split)

lemma
  sum_list_zip_map:
  assumes "distinct xs"
  shows "(∑(x, y)←zip xs (map g xs). f x y) = (∑x∈set xs. f x (g x))"
  by (force simp add: sum_list_distinct_conv_sum_set assms distinct_zipI1 split_beta'
    in_set_zip in_set_conv_nth inj_on_convol_ident
    intro!: sum.reindex_cong[where l="λx. (x, g x)"])

lemma
  inter_aform_plane_ortho_overappr:
  assumes "inter_aform_plane_ortho p Z n g = Some X"
  shows "{x. ∀i ∈ Basis. x ∙ i ∈ {y. (g, y) ∈ (λx. (x ∙ n, x ∙ i)) ` Affine Z}} ⊆ Affine X"
proof -
  let ?inter = "(λb. bound_intersect_2d_ud p (inner2_aform Z n b) g)"
  obtain xs
  where xs: "those (map ?inter Basis_list) = Some xs"
    using assms by (cases "those (map ?inter Basis_list)") (auto simp: inter_aform_plane_ortho_def)

  from those_eq_SomeD[OF this]
  obtain y' where xs_eq: "xs = map (the ∘ ?inter) Basis_list"
    and y': "⋀i. i < length (Basis_list::'a list) ⟹ ?inter (Basis_list ! i) = Some (y' i)"
    by metis
  have "∀(i::'a) ∈ Basis. ∃j<length (Basis_list::'a list). i = Basis_list ! j"
    by (metis Basis_list in_set_conv_nth)
  then obtain j where j:
    "⋀i::'a. i∈Basis ⟹ j i < length (Basis_list::'a list)"
    "⋀i::'a. i∈Basis ⟹ i = Basis_list ! j i"
    by metis
  define y where "y = y' o j"
  with y' j have y: "⋀i. i ∈ Basis ⟹ ?inter i = Some (y i)"
    by (metis comp_def)
  hence y_le: "⋀i. i ∈ Basis ⟹ fst (y i) ≤ snd (y i)"
    by (auto intro!: bound_intersect_2d_ud_segments_of_aform_le)
  hence "(∑b∈Basis. fst (y b) *⇩R b) ≤ (∑b∈Basis. snd (y b) *⇩R b)"
    by (auto simp: eucl_le[where 'a='a])
  with assms have X: "Affine X = {∑b∈Basis. fst (y b) *⇩R b..∑b∈Basis. snd (y b) *⇩R b}"
    by (auto simp: inter_aform_plane_ortho_def sum_list_zip_map xs xs_eq y Affine_aform_of_ivl)

  show ?thesis
  proof safe
    fix x assume x: "∀i∈Basis. x ∙ i ∈ {y. (g, y) ∈ (λx. (x ∙ n, x ∙ i)) ` Affine Z}"
    {
      fix i::'a assume i: "i ∈ Basis"
      from x i have x_in2: "(g, x ∙ i) ∈ (λx. (x ∙ n, x ∙ i)) ` Affine Z"
        by auto
      from x_in2 obtain e
      where e: "e ∈ UNIV → {- 1..1}"
        and g: "g = aform_val e Z ∙ n"
        and x: "x ∙ i = aform_val e Z ∙ i"
        by (auto simp: Affine_def valuate_def)
      have "{aform_val e (inner2_aform Z n i)} = {aform_val e (inner2_aform Z n i)} ∩ {x. fst x = g}"
        by (auto simp: g inner2_def)
      also
      from y[OF ‹i ∈ Basis›]
      have "?inter i = Some (fst (y i), snd (y i))" by simp
      note bound_intersect_2d_ud_segments_of_aform[OF this e]
      finally have "x ∙ i ∈ {fst (y i) .. snd (y i)}"
        by (auto simp: x inner2_def)
    } thus "x ∈ Affine X"
      unfolding X
      by (auto simp: eucl_le[where 'a='a])
  qed
qed

lemma inter_proj_eq:
  fixes n g l
  defines "G ≡ {x. x ∙ n = g}"
  shows "(λx. x ∙ l) ` (Z ∩ G) =
    {y. (g, y) ∈ (λx. (x ∙ n, x ∙ l)) ` Z}"
  by (auto simp: G_def)

lemma
  inter_overappr:
  fixes n γ l
  shows "Z ∩ {x. x ∙ n = g} ⊆ {x. ∀i ∈ Basis. x ∙ i ∈ {y. (g, y) ∈ (λx. (x ∙ n, x ∙ i)) ` Z}}"
  by auto

lemma inter_inter_aform_plane_ortho:
  assumes "inter_aform_plane_ortho p Z n g = Some X"
  shows "Affine Z ∩ {x. x ∙ n = g} ⊆ Affine X"
proof -
  note inter_overappr[of "Affine Z" n g]
  also note inter_aform_plane_ortho_overappr[OF assms]
  finally show ?thesis .
qed

subsection ‹``Completeness'' of Intersection›

abbreviation "encompasses x seg ≡ det3 (fst seg) (snd seg) x ≥ 0"

lemma encompasses_cases:
  "encompasses x seg ∨ encompasses x (snd seg, fst seg)"
  by (auto simp: det3_def' algebra_simps)

lemma list_all_encompasses_cases:
  assumes "list_all (encompasses p) (x # y # zs)"
  obtains "list_all (encompasses p) [x, y, (snd y, fst x)]"
    | "list_all (encompasses p) ((fst x, snd y)#zs)"
  using encompasses_cases
proof
  assume "encompasses p (snd y, fst x)"
  hence "list_all (encompasses p) [x, y, (snd y, fst x)]"
    using assms by (auto simp: list_all_iff)
  thus ?thesis ..
next
  assume "encompasses p (snd (snd y, fst x), fst (snd y, fst x))"
  hence "list_all (encompasses p) ((fst x, snd y)#zs)"
    using assms by (auto simp: list_all_iff)
  thus ?thesis ..
qed

lemma triangle_encompassing_polychain_of:
  assumes "det3 p a b ≥ 0" "det3 p b c ≥ 0" "det3 p c a ≥ 0"
  assumes "ccw' a b c"
  shows "p ∈ convex hull {a, b, c}"
proof -
  from assms have nn: "det3 b c p ≥ 0" "det3 c a p ≥ 0" "det3 a b p ≥ 0" "det3 a b c ≥ 0"
    by (auto simp: det3_def' algebra_simps)
  have "det3 a b c *⇩R p = det3 b c p *⇩R a + det3 c a p *⇩R b + det3 a b p *⇩R c"
    by (auto simp: det3_def' algebra_simps prod_eq_iff)
  hence "inverse (det3 a b c) *⇩R (det3 a b c *⇩R p) =
      inverse (det3 a b c) *⇩R (det3 b c p *⇩R a + det3 c a p *⇩R b + det3 a b p *⇩R c)"
    by simp
  with assms have p_eq: "p =
    (det3 b c p / det3 a b c) *⇩R a + (det3 c a p / det3 a b c) *⇩R b + (det3 a b p / det3 a b c) *⇩R c"
    (is "_ = scaleR ?u _ + scaleR ?v _ + scaleR ?w _")
    by (simp add: inverse_eq_divide algebra_simps ccw'_def)
  have det_eq: "det3 b c p / det3 a b c + det3 c a p / det3 a b c + det3 a b p / det3 a b c = 1"
    using assms(4)
    by (simp add: add_divide_distrib[symmetric] det3_def' algebra_simps ccw'_def)
  show ?thesis
    unfolding convex_hull_3
    using assms(4)
    by (blast intro: exI[where x="?u"] exI[where x="?v"] exI[where x="?w"]
      intro!: p_eq divide_nonneg_nonneg nn det_eq)
qed

lemma encompasses_convex_polygon3:
  assumes "list_all (encompasses p) (x#y#z#zs)"
  assumes "convex_polygon (x#y#z#zs)"
  assumes "ccw'.sortedP (fst x) (map snd (butlast (x#y#z#zs)))"
  shows "p ∈ convex hull (set (map fst (x#y#z#zs)))"
  using assms
proof (induct zs arbitrary: x y z p)
  case Nil
  thus ?case
    by (auto simp: det3_def' algebra_simps
      elim!: ccw'.sortedP_Cons ccw'.sortedP_Nil
      intro!: triangle_encompassing_polychain_of)
next
  case (Cons w ws)
  from Cons.prems(2) have "snd y = fst z" by auto
  from Cons.prems(1)
  show ?case
  proof (rule list_all_encompasses_cases)
    assume "list_all (encompasses p) [x, y, (snd y, fst x)]"
    hence "p ∈ convex hull {fst x, fst y, snd y}"
      using Cons.prems
      by (auto simp: det3_def' algebra_simps
        elim!: ccw'.sortedP_Cons ccw'.sortedP_Nil
        intro!: triangle_encompassing_polychain_of)
    thus ?case
      by (rule rev_subsetD[OF _ hull_mono]) (auto simp: ‹snd y = fst z›)
  next
    assume *: "list_all (encompasses p) ((fst x, snd y) # z # w # ws)"
    from Cons.prems
    have enc: "ws ≠ [] ⟹ encompasses p (last ws)"
      by (auto simp: list_all_iff)
    have "set (map fst ((fst x, snd y)#z#w#ws)) ⊆ set (map fst (x # y # z # w # ws))"
      by auto
    moreover
    {
      note *
      moreover
      have "convex_polygon ((fst x, snd y) # z # w # ws)"
        by (metis convex_polygon_skip Cons.prems(2,3))
      moreover
      have "ccw'.sortedP (fst (fst x, snd y)) (map snd (butlast ((fst x, snd y) # z # w # ws)))"
        using Cons.prems(3)
        by (auto elim!: ccw'.sortedP_Cons intro!: ccw'.sortedP.Cons ccw'.sortedP.Nil
          split: if_split_asm)
      ultimately have "p ∈ convex hull set (map fst ((fst x, snd y)#z#w#ws))"
        by (rule Cons.hyps)
    }
    ultimately
    show "p ∈ convex hull set (map fst (x # y # z # w # ws))"
      by (rule subsetD[OF hull_mono])
  qed
qed

lemma segments_of_aform_empty_Affine_eq:
  assumes "segments_of_aform X = []"
  shows "Affine X = {fst X}"
proof -
  have "independent_pdevs (map snd (list_of_pdevs (nlex_pdevs (snd X)))) = [] ⟷
    (list_of_pdevs (nlex_pdevs (snd X))) = []"
    by (subst independent_pdevs_eq_Nil_iff) (auto simp: list_all_iff list_of_pdevs_def )
  with assms show ?thesis
    by (force simp: aform_val_def list_of_pdevs_def Affine_def valuate_def segments_of_aform_def
      Let_def half_segments_of_aform_def inl_def)
qed

lemma not_segments_of_aform_singleton: "segments_of_aform X ≠ [x]"
  by (auto simp: segments_of_aform_def Let_def add_is_1 dest!: arg_cong[where f=length])

lemma encompasses_segments_of_aform_in_AffineI:
  assumes "length (segments_of_aform X) > 2"
  assumes "list_all (encompasses p) (segments_of_aform X)"
  shows "p ∈ Affine X"
proof -
  from assms(1) obtain x y z zs where eq: "segments_of_aform X = x#y#z#zs"
    by (cases "segments_of_aform X" rule: list_cases4) auto
  hence "fst x = fst (hd (half_segments_of_aform X))"
    by (metis segments_of_aform_def hd_append list.map_disc_iff list.sel(1))
  also have "… = lowest_vertex (fst X, nlex_pdevs (snd X))"
    using assms
    by (intro fst_hd_half_segments_of_aform) (auto simp: segments_of_aform_def)
  finally have fstx: "fst x = lowest_vertex (fst X, nlex_pdevs (snd X))" .
  have "p ∈ convex hull (set (map fst (segments_of_aform X)))"
    using assms(2)
    unfolding eq
  proof (rule encompasses_convex_polygon3)
    show "convex_polygon (x # y # z # zs)"
      using assms(1) unfolding eq[symmetric]
      by (intro convex_polygon_segments_of_aform) (simp add: segments_of_aform_def Let_def)
    show "ccw'.sortedP (fst x) (map snd (butlast (x # y # z # zs)))"
      using assms(1)
      unfolding fstx map_butlast eq[symmetric]
      by (intro ccw'_sortedP_snd_segments_of_aform)
        (simp add: segments_of_aform_def Let_def half_segments_of_aform_def)
  qed
  also have "… ⊆ convex hull (Affine X)"
  proof (rule hull_mono, safe)
    fix a b assume "(a, b) ∈ set (map fst (segments_of_aform X))"
    then obtain c d where "((a, b), c, d) ∈ set (segments_of_aform X)" by auto
    from previous_segments_of_aformE[OF this]
    obtain x where "(x, a, b) ∈ set (segments_of_aform X)" by auto
    from in_set_segments_of_aform_aform_valE[OF this]
    obtain e where "(a, b) = aform_val e X" "e ∈ UNIV → {- 1..1}" by auto
    thus "(a, b) ∈ Affine X"
      by (auto simp: Affine_def valuate_def image_iff)
  qed
  also have "… = Affine X"
    by (simp add: convex_Affine convex_hull_eq)
  finally show ?thesis .
qed

end