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 "xset (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 "¬ (xset 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 "xset 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) = (Pset ?ssl. g P *R P)"
    by blast
  note this(2)
  finally
  have "aform_val e X = lowest_vertex (fst X, nlex_pdevs (snd X)) + (Pset ?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)