section {* Intersection *}
theory Intersection
imports
  Polygon
  Counterclockwise_2D_Arbitrary
  Affine_Code
  Float_Rat_Real
begin
text {*\label{sec:intersection}*}

subsection {* from the very beginning?! *}

lift_definition nlex_pdevs::"point pdevs \<Rightarrow> point pdevs"
  is "\<lambda>x n. if lex 0 (x n) then - x n else x n" by simp

lift_definition nlex_slist::"(nat, point) slist \<Rightarrow> (nat, point) slist" is
  "map (\<lambda>(i, x). (i, if lex 0 x then - x else x))"
  apply (auto simp: o_def split_beta' if_distrib)
  apply (smt fstI list.map_cong0)
  apply (smt fstI list.map_cong0)
  done

lemma Pdevs_raw_map: "f 0 = 0 \<Longrightarrow> Pdevs_raw (map (\<lambda>(i, x). (i, f x)) xs) i = f (Pdevs_raw xs i)"
  by (auto simp: Pdevs_raw_def map_of_map split: option.split)

lemma compute_nlex_pdevs[code]: "nlex_pdevs (Pdevs x) = Pdevs (nlex_slist x)"
  by transfer (auto simp: Pdevs_raw_map)

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 \<in> UNIV \<rightarrow> I" "uminus ` I = I"
  obtains e' where "e' \<in> UNIV \<rightarrow> I" "pdevs_val e x = pdevs_val e' (nlex_pdevs x)"
  using assms
  by (atomize_elim, intro exI[where x="\<lambda>n. if lex 0 (pdevs_apply x n) then - e n else e n"])
    (force simp: pdevs_val_pdevs_domain intro!: setsum.cong)

lemma
  pdevs_val_nlex_pdevs2:
  assumes "e \<in> UNIV \<rightarrow> I" "uminus ` I = I"
  obtains e' where "e' \<in> UNIV \<rightarrow> I" "pdevs_val e (nlex_pdevs x) = pdevs_val e' x"
  using assms
  by (atomize_elim, intro exI[where x="\<lambda>n. (if lex 0 (pdevs_apply x n) then - e n else e n)"])
    (force simp: pdevs_val_pdevs_domain intro!: setsum.cong)

definition lowest_vertex::"'a::ordered_euclidean_space aform \<Rightarrow> 'a" where
  "lowest_vertex X = fst X - listsum (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 \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes "\<And>i. snd (pdevs_apply (snd X) i) \<ge> 0"
  assumes "\<And>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) \<le> snd (aform_val e Y)"
proof -
  from abs_pdevs_val_le_tdev[OF assms(1), of "snd Y"]
  have "snd \<bar>pdevs_val e (snd Y)\<bar> \<le> (\<Sum>i<degree_aform Y. \<bar>snd (pdevs_apply (snd X) i)\<bar>)"
    unfolding lowest_vertex_def
    by (auto simp: aform_val_def tdev_def less_eq_prod_def snd_setsum snd_abs assms)
  also have "\<dots> = (\<Sum>i<degree_aform X. snd (pdevs_apply (snd X) i))"
    by (simp add: assms)
  also have "\<dots> \<le> snd (listsum (map snd (list_of_pdevs (snd X))))"
    by (simp add: listsum_list_of_pdevs dense_list_of_pdevs_def listsum_distinct_conv_setsum_set
      snd_setsum atLeast0LessThan)
  finally show ?thesis
    by (auto simp: aform_val_def lowest_vertex_def minus_le_iff snd_abs abs_real_def assms
      split: split_if_asm)
qed

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

lemma Affine_pdevs_of_list_ConsE:
  assumes "p \<in> Affine (x0, pdevs_of_list (x # xs))"
  obtains e where "e \<in> UNIV \<rightarrow> {-1 .. 1}" "p = e 0 *\<^sub>R x + aform_val e ((x0, pdevs_of_list (0#xs)))"
  using assms
  by (auto simp: Affine_def valuate_def aform_val_def )

lemma in_set_independent_pdevsE:
  assumes "y \<in> set (independent_pdevs xs)"
  obtains x where "x\<in>set xs" "coll 0 x y"
proof atomize_elim
  show "\<exists>x. x \<in> set xs \<and> 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 `y \<in> set (independent_pdevs (z # zs))`
    show ?case
      apply (simp add: Let_def split: split_if_asm)
      defer
    proof (erule disjE)
      case goal2
      hence "y \<in> set (independent_pdevs (snd (partition (coll 0 z) zs)))"
        by simp
      from 2(1)[OF refl pair_collapse refl this]
      show ?case
        by auto
    next
      case goal1
      show ?case
        unfolding goal1
        apply (rule exI[where x="fst z"])
        apply (rule exI[where x="snd z"])
        apply (auto intro!: coll_add coll_listsum)
        done
    next
      case goal3
      show ?case
        using 2(1)[OF refl pair_collapse refl, simplified, OF goal3(2)]
        by auto
    qed
  qed
qed

lemma distinct_independent_pdevs[simp]:
  shows "distinct (independent_pdevs xs)"
  using assms
proof (induct xs rule: independent_pdevs.induct)
  case 1 thus ?case by simp
next
  case (2 x xs)
  have "distinct (independent_pdevs (snd (partition (coll 0 x) xs)))"
    by (rule 2) (auto intro!: 2)
  thus ?case
  proof (auto elim!: in_set_independent_pdevsE simp: Let_def)
    case goal1
    {
      assume "(a, b) = 0"
      hence ?case using goal1 by simp
    } moreover {
      assume "x = 0"
      hence ?case using goal1 by simp
    } moreover {
      assume "listsum (filter (coll 0 x) xs) = 0"
      hence ?case using goal1 by (simp add: coll_commute)
    } moreover {
      assume abnz: "(a, b) \<noteq> 0" "x \<noteq> 0" "listsum (filter (coll 0 x) xs) \<noteq> 0"
        "x + listsum (filter (coll 0 x) xs) \<noteq> 0"
      have *: "coll 0 x (listsum (filter (coll 0 x) xs))"
        by (auto intro!: coll_listsum)
      have "coll 0 x (a, b)"
        apply (subst coll_commute)
        apply (rule coll_add_trans)
        defer
        apply (subst coll_commute)
        apply (rule *)
        apply fact apply fact apply fact apply (subst add.commute) apply fact
        using goal1(3) apply (simp add: add.commute)
        done
      hence ?case using goal1 by simp
    } ultimately show ?case using goal1 by blast
  qed
qed

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

interpretation ccw!: linorder_list0 "ccw x" for x .

definition half_segments_of_aform::"point aform \<Rightarrow> (point*point) list"
  where "half_segments_of_aform X =
    (let
      x0 = lowest_vertex (fst X, nlex_pdevs (snd X))
    in
      polychain_of x0 (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X)))))"

lemma polychain_of_eq_empty_iff[simp]: "polychain_of p xs = [] \<longleftrightarrow> xs = []"
  by (cases xs) (auto simp: Let_def)

lemma (in linorder_list0) selsort_eq_empty_iff[simp]: "selsort xs = [] \<longleftrightarrow> xs = []"
  by (cases xs) (auto simp: Let_def)

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
  apply (auto simp: half_segments_of_aform_def Let_def)
  defer
  apply (cases i)
  apply (auto simp: polychain_of_subsequent_eq )
  done

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 \<noteq> [] \<Longrightarrow>
    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 ccw_translate: "ccw p (p + q) (p + r) = ccw 0 q r"
  by (auto simp: ccw_def psi_def lex_def)

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

lemma "lex 0 x \<Longrightarrow> lex 0 y \<Longrightarrow> ccw 0 x y \<Longrightarrow> ccw 0 x (x + y)"
  by (auto simp add: ccw_def psi_def ccw'_not_coll det3_def' algebra_simps ccw'_def lex_def)

lemma subsequent_polychain_of_ccw':
  assumes "Suc i < length (polychain_of p xs)"
  assumes "linorder_list0.sortedP (ccw' 0) xs"
  shows "ccw' (fst (polychain_of p xs ! i)) (snd (polychain_of p xs ! i)) (snd (polychain_of p xs ! Suc i))"
  using assms
proof (induct xs arbitrary: p i)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  from Cons.hyps[of _ "p + x"]
  show ?case using Cons.prems
    by (cases i)
      (auto elim!: linorder_list0.sortedP_Nil linorder_list0.sortedP_Cons
        simp: neq_Nil_conv ac_simps ccw'.translate)
qed

lemma in_set_polychain_of_imp_listsum:
  assumes "z \<in> set (polychain_of Pc Ps)"
  obtains d where "z = (Pc + listsum (take d Ps), Pc + listsum (take (Suc d) Ps))"
  using assms
  apply atomize_elim
proof (induction Ps arbitrary: Pc z)
  case Nil thus ?case by simp
next
  case (Cons P Ps)
  hence "z = (Pc, Pc + P) \<or> z \<in> set (polychain_of (Pc + P) Ps)"
    by auto
  thus ?case
  proof
    assume "z \<in> set ((polychain_of (Pc + P) Ps))"
    from Cons.IH[OF this]
    obtain d
    where "z = (Pc + P + listsum (take d Ps), Pc + P + listsum (take (Suc d) Ps))"
      by auto
    thus ?case
      by (auto intro!: exI[where x="Suc d"])
  qed (auto intro!: exI[where x=0])
qed

lemma ccw'_imp_ccw: "ccw' a b c \<Longrightarrow> ccw a b c"
  by (simp add: ccw_def)

lemma ccw_ncoll_imp_ccw: "ccw a b c \<Longrightarrow> \<not>coll a b c \<Longrightarrow> ccw' a b c"
  by (simp add: ccw_def)

lemma ccw_sorted_implies_ccw'_sortedP:
  assumes nonaligned: "\<And>y z. y \<in> set Ps \<Longrightarrow> z \<in> set Ps \<Longrightarrow> y \<noteq> z \<Longrightarrow> \<not> coll 0 y z"
  assumes sorted: "linorder_list0.sortedP (ccw 0) Ps"
  assumes "distinct Ps"
  shows "linorder_list0.sortedP (ccw' 0 ) Ps"
  using assms
proof (induction Ps)
  case Nil
  thus ?case
    by (auto intro: linorder_list0.Nil)
next
  case (Cons P Ps)
  from Cons.prems(2)
  show ?case
    apply (auto intro!: linorder_list0.Cons elim!: linorder_list0.sortedP_Cons)
    defer
    apply (intro Cons) apply force apply force apply force apply force using Cons.prems(3) apply force
    apply (intro ccw_ncoll_imp_ccw) apply force
    using Cons.prems
    apply (intro Cons) apply force+
    done
qed

interpretation ccw'!: linorder_list0 "ccw' x" for x .

lemma polychain_of_ccw_evtl_unnecessary: --"TODO: evtl unnötig!"
  assumes sorted: "ccw'.sortedP 0 Ps"
  assumes z: "z \<in> set (polychain_of Pc Ps)"
  shows "list_all (\<lambda>(xi, xj). ccw xi xj (fst z) \<and> 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 \<noteq> {}"
    hence "Ps \<noteq> []" by simp
    {
      fix a assume "a \<in> 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_listsum[OF Cons(3)]
    obtain d
    where d: "z = (Pc + listsum (take d (P # Ps)), Pc + listsum (take (Suc d) (P # Ps)))" .

    from Cons(3)
    have disj: "z = (Pc, Pc + P) \<or> z \<in> set (polychain_of (Pc + P) Ps)"
      by auto

    have la: "list_all (\<lambda>(xi, xj). ccw xi xj Pc \<and> ccw xi xj (Pc + P)) (polychain_of (Pc + P) Ps)"
    proof (rule list_allI)
      fix x assume "x \<in> set (polychain_of (Pc + P) Ps)"
      from in_set_polychain_of_imp_listsum[OF this]
      obtain e
      where e: "x = (Pc + P + listsum (take e Ps), Pc + P + listsum (take (Suc e) Ps))"
        by auto
      thus "case x of (xi, xj) \<Rightarrow> ccw xi xj Pc \<and> ccw xi xj (Pc + P)"
        apply (auto simp add: e)
        apply (rule cyclic)
        apply (cases "e \<ge> length Ps")
        apply simp
        apply (cases "e = 0")
        apply (simp add: take_Suc_eq)
        apply (auto simp add: ccw_translate_origin take_Suc_eq add.assoc[symmetric]
          intro!: ccw'_imp_ccw)[2]
        apply (rule ccw') apply simp
        apply (rule ccw'.add1)
        apply (rule ccw')
        apply simp
        apply (simp add: listsum_setsum_nth)
        apply (rule ccw'.setsum2)
        apply (simp add: )
        apply (simp add: `Ps \<noteq> []`)
        apply (simp )
        apply (rule linorder_list0.sorted_nth_less)
        apply (rule sorted')
        apply auto
        apply (cases "e \<ge> length Ps")
        apply simp
        apply (cases "e = 0")
        apply (simp add: take_Suc_eq)
        apply (simp add: take_Suc_eq)
        apply (auto simp add: ccw_translate_origin take_Suc_eq add.assoc[symmetric]
          intro!: ccw'_imp_ccw)
        apply (simp add: listsum_setsum_nth)
        apply (rule ccw'.setsum2)
        apply (simp add: )
        apply (simp add: `Ps \<noteq> []`)
        apply (simp )
        apply (rule linorder_list0.sorted_nth_less)
        apply (rule sorted')
        apply auto
        done
    qed
    from disj have ?case
      apply rule
      apply (simp add: la)
      apply simp
      apply rule
      defer
      apply rule
      defer
      apply (rule Cons.IH)
        using Cons.prems apply (force elim!: linorder_list0.sortedP_Cons)
       using Cons.prems apply force

      apply (simp add: d ccw_translate_origin)
      apply (cases d, simp)
      apply (rename_tac e)
      apply (case_tac e) apply simp
      apply simp
      apply (rule ccw'_imp_ccw)
      apply (simp)
      apply (simp add: listsum_setsum_nth)
      apply (rule ccw'.setsum)
      apply (auto intro!: ccw')[3]

      apply (simp add: d ccw_translate_origin)
      apply (cases d, simp)
      apply (rename_tac e)
      apply (case_tac e) apply simp
      apply (rule ccw'_imp_ccw)
      apply (simp)
      apply (simp add: listsum_setsum_nth)
      apply (rule ccw'.setsum)
      apply (auto intro!: ccw')

      apply (rule ccw'_imp_ccw)
      apply (simp)
      apply (simp add: listsum_setsum_nth)
      apply (rule ccw'.setsum)
      apply (auto intro!: ccw')
      done
  } ultimately show ?case by blast
qed simp

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

lemma listsum_coll_ex_scale:
  assumes coll: "\<And>x. x \<in> set xs \<Longrightarrow> coll 0 z x"
  assumes nz: "z \<noteq> 0"
  shows "\<exists>r. listsum xs = r *\<^sub>R z"
proof -
  {
    fix i assume i: "i < length xs"
    hence nth: "xs ! i \<in> set xs" by simp
    note coll_scale[OF coll[OF nth] `z \<noteq> 0`]
  } then obtain r where r: "\<And>i. i < length xs \<Longrightarrow> xs ! i = r i *\<^sub>R z"
    by metis
  have "xs = map (op ! xs) [0..<length xs]" by (simp add: map_nth)
  also have "\<dots> = map (\<lambda>i. r i *\<^sub>R z) [0..<length xs]" by (simp add: r)
  also have "listsum \<dots> = (\<Sum>i\<leftarrow>[0..<length xs]. r i) *\<^sub>R z"
    by (simp add: listsum_setsum_nth scaleR_setsum_left)
  finally show ?thesis ..
qed

lemma listsum_filter_coll_ex_scale: "z \<noteq> 0 \<Longrightarrow> \<exists>r. listsum (filter (coll 0 z) zs) = r *\<^sub>R z"
  by (rule listsum_coll_ex_scale) simp

lemma in_set_independent_pdevs_nonzero: "x \<in> set (independent_pdevs xs) \<Longrightarrow> x \<noteq> 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: split_if_asm)
qed simp

lemma independent_pdevs_pairwise_non_coll:
  assumes "x \<in> set (independent_pdevs xs)"
  assumes "y \<in> set (independent_pdevs xs)"
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> x \<noteq> 0"
  assumes "x \<noteq> y"
  shows "\<not> 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 \<noteq> 0" by simp
  from 2(2) have "x \<noteq> 0" by (rule in_set_independent_pdevs_nonzero)
  from 2(3) have "y \<noteq> 0" by (rule in_set_independent_pdevs_nonzero)
  from 2(2,3,4,5)
  show ?case
    apply (auto simp: Let_def split: split_if_asm)
  proof -
    case goal1
    hence "\<not>coll 0 x y"
      by (intro 2(1)[OF refl prod.collapse refl _ _ 2(4) 2(5)]) auto
    thus False using goal1 by simp
  next
    case goal4
    hence "\<not>coll 0 x y"
      by (intro 2(1)[OF refl prod.collapse refl _ _ 2(4) 2(5)]) auto
    thus False using goal4 by simp
  next
    case goal2
    thus ?case
      using listsum_filter_coll_ex_scale[OF `z \<noteq> 0`, of "z#zs"]
      apply (auto elim!: in_set_independent_pdevsE  simp: coll_commute)
      by (metis (no_types) `x \<noteq> 0` coll_scale coll_scaleR)
  next
    case goal3
    thus ?case
      using listsum_filter_coll_ex_scale[OF `z \<noteq> 0`, of "z#zs"]
      apply (auto elim!: in_set_independent_pdevsE simp: coll_commute)
      by (metis (no_types) `y \<noteq> 0` coll_scale coll_scaleR)
  qed
qed

lemma list_of_pdevs_nonzero: "x \<in> set (map snd (list_of_pdevs xs)) \<Longrightarrow> x \<noteq> 0"
  by (auto simp: list_of_pdevs_def)

lemma in_set_inl_nonzero: "x \<in> set (inl xs) \<Longrightarrow> x \<noteq> 0"
  by (auto simp: inl_def in_set_independent_pdevs_nonzero)

lemma
  inl_ncoll: "y \<in> set (inl (snd X)) \<Longrightarrow> z \<in> set (inl (snd X)) \<Longrightarrow> y \<noteq> z \<Longrightarrow> \<not>coll 0 y z"
  unfolding inl_def
  by (rule independent_pdevs_pairwise_non_coll, assumption+)
    (auto simp: inl_def list_of_pdevs_nonzero)

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

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

lemma nlex_setsum:
  assumes "finite X"
  assumes "\<And>x. x \<in> X \<Longrightarrow> lex (f x) 0"
  shows "lex (setsum f X) 0"
  using assms
  by induction (auto intro!: nlex_sum)

lemma in_set_independent_pdevs_invariant_nlex:
  "x \<in> set (independent_pdevs xs) \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> lex x 0) \<Longrightarrow>
  (\<And>x. x \<in> set xs \<Longrightarrow> x \<noteq> 0) \<Longrightarrow> 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 \<noteq> 0" by auto
  from 2(2)
  have "x \<in> set (independent_pdevs (filter (Not \<circ> coll 0 y) ys)) \<or>
    x = y + listsum (filter (coll 0 y) ys)"
    by (auto simp: Let_def split: split_if_asm)
  thus ?case
  proof
    assume "x \<in> set (independent_pdevs (filter (Not \<circ> 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 + listsum (filter (coll 0 y) ys)"
    also have "lex \<dots> 0"
      by (force intro: nlex_sum nlex_setsum simp: listsum_setsum_nth
        dest: nth_mem intro: 2(3))
    finally show ?case .
  qed
qed

lemma in_set_inl_lex: "x \<in> set (inl xs) \<Longrightarrow> lex x 0"
  apply (auto simp: inl_def list_of_pdevs_def dest!: in_set_independent_pdevs_invariant_nlex
    split: split_if_asm)
  apply (simp add: lex_def)
  by (meson not_lex_eq)

lemma nlex_half_segments_of_aform: "(a, b) \<in> set (half_segments_of_aform X) \<Longrightarrow> lex b a"
  apply (auto simp: half_segments_of_aform_def dest!: in_set_polychain_ofD in_set_inl_lex)
  apply (auto simp add: lex_def prod_eq_iff)
  done

lemma distinct_map_scaleRI:
  fixes xs::"'a::real_vector list"
  shows "distinct xs \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> distinct (map (op *\<^sub>R c) xs)"
  by (induct xs) auto

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

lemma ccw_scale23: "ccw 0 a b \<Longrightarrow> r > 0 \<Longrightarrow> ccw 0 (r *\<^sub>R a) (r *\<^sub>R b)"
  by (auto simp: ccw_def psi_scale)

lemma ccw0_sorted_scaleR: "ccw.sortedP 0 xs \<Longrightarrow> r > 0 \<Longrightarrow> ccw.sortedP 0 (map (op *\<^sub>R r) xs)"
  by (induct xs) (auto intro!: ccw.sortedP.Cons ccw_scale23 elim!: ccw.sortedP_Cons simp del: scaleR_Pair)

interpretation ccw0!: linorder_list "ccw 0" "set (inl (snd X))"
  apply unfold_locales
  apply (meson ccw_self(2))
proof -
  case goal1
  thus ?case
    apply (cases "a = (0, 1)" "b = (0, 1)" "c = (0, 1)"
      rule: bool.exhaust[case_product bool.exhaust[case_product bool.exhaust]])
    apply simp_all
    apply (simp add: nlex_ccw_left in_set_inl_lex)
    using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left apply blast
    using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left apply blast
    apply (rule ccw.transitive[where S=UNIV and s="(0, 1)"])
    prefer 6 apply assumption
    prefer 6 apply assumption
    defer
    apply simp
    apply (simp_all add: nlex_ccw_left in_set_inl_lex)
    apply (metis (no_types) coll_zero inl_ncoll)
    done
next
  case goal2
  thus ?case
    by (metis ccw_self(1) in_set_inl_nonzero mem_Collect_eq not_ccw_eq)
next
  case goal3
  thus ?case
    by (metis UNIV_I ccw_self(1) nondegenerate)
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 (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X))))"
  using sorted_inl
  by (rule ccw0_sorted_scaleR) simp

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

lemma distinct_scaled_inl: "distinct (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X))))"
  using distinct_selsort_inl
  by (rule distinct_map_scaleRI) simp

lemma ccw'_sortedP_scaled_inl:
  "linorder_list0.sortedP (ccw' 0) (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X))))"
  using _ sorted_scaled_inl distinct_scaled_inl
  apply (rule ccw_sorted_implies_ccw'_sortedP)
  apply (auto simp del: scaleR_Pair)
  using inl_ncoll
  apply force+
  done

lemma ccw_half_segments_of_aform_all:
  assumes cd: "(c, d) \<in> set (half_segments_of_aform X)"
  shows "list_all (\<lambda>(xi, xj). ccw xi xj c \<and> ccw xi xj d) (half_segments_of_aform X)"
proof -
  have
    "list_all (\<lambda>(xi, xj). ccw xi xj (fst (c, d)) \<and> ccw xi xj (snd (c, d)))
      (polychain_of (lowest_vertex (fst X, nlex_pdevs (snd X)))
        ((map (op *\<^sub>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_evtl_unnecessary)
  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) \<in> set (half_segments_of_aform X)"
  assumes c: "(c, d) \<in> 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 \<in> convex hull set (map fst (half_segments_of_aform X))"
  assumes ab: "(a, b) \<in> set (half_segments_of_aform X)"
  shows "ccw a b x"
  using _ _ ch
  apply (rule ccw.convex_hull)
    apply auto
   apply (rule ccw_half_segments_of_aform(1))
    apply (rule ab)
   apply assumption
  apply (rule nlex_half_segments_of_aform)
  apply fact
  done

lemma half_segments_of_aform2:
  assumes ch: "x \<in> convex hull set (map snd (half_segments_of_aform X))"
  assumes ab: "(a, b) \<in> set (half_segments_of_aform X)"
  shows "ccw a b x"
  using _ _ ch
  apply (rule ccw.convex_hull)
    apply auto
   apply (rule ccw_half_segments_of_aform(2))
    apply (rule ab)
   apply assumption
  apply (rule nlex_half_segments_of_aform)
  apply fact
  done

lemma scaleR_listsum: fixes xs::"'a::real_vector list" shows "a *\<^sub>R listsum xs = listsum (map (scaleR a) xs)"
  by (induct xs) (auto simp: algebra_simps)

lemma pdevs_val_const_pdevs_of_list: "pdevs_val (\<lambda>_. c) (pdevs_of_list xs) = c *\<^sub>R listsum xs"
  unfolding pdevs_val_zip split_beta' scaleR_listsum
  by (rule arg_cong) (auto intro!: nth_equalityI)

lemma pdevs_val_listsum: "pdevs_val (\<lambda>_. c) X = c *\<^sub>R listsum (map snd (list_of_pdevs X))"
  by (auto simp: pdevs_val_setsum listsum_list_of_pdevs pdevs_val_const_pdevs_of_list[symmetric]
    pdevs_of_list_dense_list_of_pdevs)

lemma inner_listsum_left: "listsum xs \<bullet> b = listsum (map (\<lambda>x. x \<bullet> b) xs)"
  by (induct xs) (auto simp: algebra_simps)

lemma listsum_eq_0_iff_nonneg:
  fixes xs::"'a::ordered_ab_group_add list"
  shows "list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> (\<forall>n\<in>set xs. n = 0)"
  apply (auto simp: list_all_iff listsum_setsum_nth setsum_nonneg_eq_0_iff )
  apply (auto simp: in_set_conv_nth)
  done

lemma (in ordered_ab_group_add) add_nonpos_eq_0_iff:
  assumes x: "0 \<ge> x" and y: "0 \<ge> y"
  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
proof -
  from add_nonneg_eq_0_iff[of "-x" "-y"] assms
  have "- (x + y) = 0 \<longleftrightarrow> - x = 0 \<and> - y = 0"
    by simp
  also have "(- (x + y) = 0) = (x + y = 0)" unfolding neg_equal_0_iff_equal ..
  finally show ?thesis by simp
qed

lemma setsum_nonpos_eq_0_iff:
  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
  shows "\<lbrakk>finite A; \<forall>x\<in>A. f x \<le> 0\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
  apply (induct set: finite, simp)
  apply (simp add: add_nonpos_eq_0_iff setsum_nonpos)
  done

lemma listsum_eq_0_iff_nonpos:
  fixes xs::"'a::ordered_ab_group_add list"
  shows "list_all (\<lambda>x. x \<le> 0) xs \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> (\<forall>n\<in>set xs. n = 0)"
  apply (auto simp: list_all_iff listsum_setsum_nth setsum_nonpos_eq_0_iff )
  apply (auto simp: in_set_conv_nth)
  done

lemma listsum_eq0I: "(\<forall>x\<in>set xs. x = 0) \<Longrightarrow> listsum xs = 0"
  by (induct xs) auto

lemma mult_to_eq:
  fixes a b c d::real
  shows
    "a \<noteq> 0 \<Longrightarrow> a * b = c * d \<longleftrightarrow> b = c * d / a"
    "b \<noteq> 0 \<Longrightarrow> a * b = c * d \<longleftrightarrow> a = c * d / b"
    "c \<noteq> 0 \<Longrightarrow> a * b = c * d \<longleftrightarrow> d = a * b / c"
    "d \<noteq> 0 \<Longrightarrow> a * b = c * d \<longleftrightarrow> c = a * b / d"
  by (auto simp add: field_simps)

lemma
  mult_out:
  fixes x y z::real
  shows "0 \<le> x + y / z \<longleftrightarrow> (if z > 0 then 0 \<le> x * z + y else if z < 0 then x * z + y \<le> 0 else 0\<le>x)"
    and "0 < x/y + z \<longleftrightarrow> (if y > 0 then 0 < x + z * y else if y < 0 then x + z * y < 0 else 0<z)"
  by (auto simp add: field_simps)

lemma
  cancel_mult_nonpos:
  fixes a b c d e :: real
  shows "a * b * c + d * a * e \<le> 0 \<longleftrightarrow> (if a < 0 then 0 \<le> b * c + d * e else if a > 0 then 0 \<ge> b * c + d * e else True)"
  apply auto
  apply (metis add_le_less_mono distrib_left less_add_same_cancel1 monoid_add_class.add.left_neutral
    monoid_add_class.add.right_neutral mult.commute mult_le_0_iff mult.left_commute mult_zero_left
    not_real_square_gt_zero)
  apply (metis distrib_left less_eq_real_def mult.commute mult_le_0_iff mult.left_commute)
  apply (metis distrib_left mult.commute mult.left_commute mult_le_0_iff not_less)
  by (metis distrib_left less_eq_real_def mult.commute mult_le_0_iff mult.left_commute)

lemma
  cancel_mult_nonneg:
  fixes a b c d e :: real
  shows "0 \<le> a * b * c + d * a * e \<longleftrightarrow> (if a > 0 then 0 \<le> b * c + d * e else if a < 0 then 0 \<ge> b * c + d * e else True)"
  apply auto
  apply (metis (full_types) add_strict_increasing2 distrib_left less_add_same_cancel1 mult.commute mult_eq_0_iff mult.left_commute not_real_square_gt_zero zero_le_mult_iff)
  apply (metis distrib_left less_eq_real_def mult.commute mult.left_commute zero_le_mult_iff)
  apply (metis (erased, hide_lams) distrib_left less_eq_real_def mult.commute mult_eq_0_iff mult.left_commute zero_less_mult_pos)
  by (metis distrib_left less_eq_real_def mult.commute mult.left_commute zero_le_mult_iff)

lemma abs_add_coll:
  assumes "coll 0 a b"
  assumes "a \<bullet> n > 0"
  assumes "b \<bullet> n \<ge> 0"
  shows "abs (a + b) = abs a + abs b"
proof (rule antisym[OF abs_triangle_ineq])
  show "\<bar>a\<bar> + \<bar>b\<bar> \<le> \<bar>a + b\<bar>"
    unfolding less_eq_prod_def
  proof
    show "fst (\<bar>a\<bar> + \<bar>b\<bar>) \<le> fst \<bar>a + b\<bar>"
      using assms
      apply (simp add: not_le det3_def' abs_prod_def inner_prod_def)
      apply (cases a) apply (cases b) apply (cases n)
      apply (auto simp: det3_def' abs_prod_def algebra_simps not_less abs_real_def inner_prod_def
        split: split_if_asm)
      apply (rule ccontr)
      defer defer
      apply (rule ccontr)
      apply (simp_all add: mult_to_eq)
      apply auto
      apply (auto simp:  mult_out cancel_mult_nonpos cancel_mult_nonneg)
      apply (simp_all add: ac_simps)
      done
  next
    show "snd (\<bar>a\<bar> + \<bar>b\<bar>) \<le> snd \<bar>a + b\<bar>"
      using assms
      apply (simp add: not_le det3_def' abs_prod_def inner_prod_def)
      apply (cases a) apply (cases b) apply (cases n)
      apply (auto simp: det3_def' abs_prod_def algebra_simps not_less abs_real_def inner_prod_def
        split: split_if_asm)
      apply (rule ccontr)
      defer defer
      apply (rule ccontr)
      apply (simp_all add: mult_to_eq)
      apply auto
      apply (auto simp:  mult_out cancel_mult_nonpos cancel_mult_nonneg)
      apply (simp_all add: ac_simps distrib_left[symmetric] zero_less_mult_iff mult_less_0_iff)
      done
  qed
qed

lemma abs_add_nlex:
  assumes "coll 0 a b"
  assumes "lex a 0"
  assumes "lex b 0"
  shows "abs (a + b) = abs a + abs b"
proof (rule antisym[OF abs_triangle_ineq])
  show "\<bar>a\<bar> + \<bar>b\<bar> \<le> \<bar>a + b\<bar>"
    unfolding less_eq_prod_def
  proof
    show "fst (\<bar>a\<bar> + \<bar>b\<bar>) \<le> fst \<bar>a + b\<bar>"
      using assms
      by (auto simp add: det3_def' abs_prod_def lex_def)
  next
    show "snd (\<bar>a\<bar> + \<bar>b\<bar>) \<le> snd \<bar>a + b\<bar>"
      using assms
      apply (auto simp add: det3_def' abs_prod_def lex_def)
    proof -
      case goal1
      hence "snd b \<le> 0 \<longleftrightarrow> snd a \<le> 0"
        apply (auto )
        apply (metis less_eq_real_def not_le zero_le_mult_iff)
        apply (metis less_eq_real_def not_le zero_le_mult_iff)
        done
      thus ?case using goal1
        by auto
    qed
  qed
qed

lemma lex_listsum: "(\<And>x. x \<in> set xs \<Longrightarrow> lex x 0) \<Longrightarrow> lex (listsum xs) 0"
  by (induct xs) (auto simp: nlex_sum)

lemma
  abs_listsum_coll:
  assumes coll: "list_all (coll 0 x) xs"
  assumes "x \<noteq> 0"
  assumes up: "list_all (\<lambda>x. lex x 0) xs"
  shows "abs (listsum xs) = listsum (map abs xs)"
  using assms
  apply (induct xs)
  apply simp
  apply clarsimp
  apply (subst abs_add_nlex)
  apply auto
  apply (rule coll_trans)
  apply assumption
  apply (rule coll_listsum)
  apply (auto simp: list_all_iff lex_listsum)
  done

lemma scaleR_le_cancel_right:
  fixes c::"'a::ordered_real_vector"
  shows "a *\<^sub>R c \<le> c \<longleftrightarrow> (1 < a \<and> c \<le> 0 \<or> a < 1 \<and> 0 \<le> c \<or> a = 1)"
  using scaleR_le_0_iff[of "a - 1" c]
  by (simp add: algebra_simps)

lemma scaleR_cancel_right1:
  fixes x::"'a::real_vector"
  shows "a *\<^sub>R x = x \<longleftrightarrow> a = 1 \<or> x = 0"
  using scaleR_cancel_right[of a x 1]
  by simp

lemma listsum_nlex_eq_zeroI:
  assumes nlex: "list_all (\<lambda>x. lex x 0) xs"
  assumes "listsum xs = 0"
  shows "list_all (op = 0) xs"
proof -
  from assms(2) have z1: "listsum (map fst xs) = 0" and z2: "listsum (map snd xs) = 0"
    by (auto simp: prod_eq_iff fst_listsum snd_listsum)
  from nlex have "list_all (\<lambda>x. x \<le> 0) (map fst xs)"
    by (auto simp: lex_def list_all_iff)
  from listsum_eq_0_iff_nonpos[OF this] z1 nlex
  have
    z1': "list_all (\<lambda>x. x = 0) (map fst xs)"
    and "list_all (\<lambda>x. x \<le> 0) (map snd xs)"
    by (auto simp: list_all_iff lex_def)
  from listsum_eq_0_iff_nonpos[OF this(2)] z2
  have "list_all (\<lambda>x. x = 0) (map snd xs)" by (simp add: list_all_iff)
  with z1' show "list_all (op = 0) xs" by (auto simp: list_all_iff zero_prod_def)
qed

lemma listsum_nlex_eq_zero_iff:
  assumes nlex: "list_all (\<lambda>x. lex x 0) xs"
  shows "listsum xs = 0 \<longleftrightarrow> list_all (op = 0) xs"
  using assms
  by (auto intro!: listsum_nlex_eq_zeroI )
    (auto simp: list_all_iff intro!: listsum_eq0I)

lemma pdevs_val_coll:
  assumes coll: "list_all (coll 0 x) xs"
  assumes nlex: "list_all (\<lambda>x. lex x 0) xs"
  assumes "x \<noteq> 0"
  assumes "f \<in> UNIV \<rightarrow> {-1 .. 1}"
  obtains e where "e \<in> {-1 .. 1}" "pdevs_val f (pdevs_of_list xs) = e *\<^sub>R (listsum xs)"
proof cases
  assume "listsum xs = 0"
  from listsum_nlex_eq_zeroI[OF nlex this]
  have "pdevs_of_list xs = zero_pdevs"
    by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem)
  hence "0 \<in> {-1 .. 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *\<^sub>R listsum xs"
    by simp_all
  thus ?thesis ..
next
  assume "listsum xs \<noteq> 0"
  have "listsum (map abs xs) \<ge> 0"
    by (auto intro!: listsum_nonneg)
  hence [simp]: "\<not>listsum (map abs xs) \<le> 0"
    by (metis `listsum xs \<noteq> 0` abs_le_zero_iff antisym_conv listsum_abs)

  have "\<exists>x \<in> set xs. x \<noteq> 0"
    by (rule ccontr) (auto dest!: listsum_eq0I simp: `listsum xs \<noteq> 0`)
  then obtain i where i: "i < length xs" "xs ! i \<noteq> 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 (listsum xs)) xs"
  proof (rule list_allI)
    fix y assume "y \<in> set xs"
    hence "coll 0 x y"
      using coll by (auto simp: list_all_iff)
    also have "coll 0 x (listsum xs)"
      using coll by (auto simp: list_all_iff intro!: coll_listsum)
    finally (coll_trans)
    show "coll 0 (listsum xs) y"
      by (simp add: coll_commute `x \<noteq> 0`)
  qed

  {
    fix i assume "i < length xs"
    hence "\<exists>r. xs ! i = r *\<^sub>R (listsum xs)"
      by (metis (mono_tags) coll_scale nth_mem `listsum xs \<noteq> 0` list_all_iff collist)
  } then obtain r where r: "\<And>i. i < length xs \<Longrightarrow> (xs ! i) = r i *\<^sub>R (listsum xs)"
    by metis
  let ?coll = "pdevs_of_list xs"
  have "pdevs_val f (pdevs_of_list xs) =
      (\<Sum>i<degree (pdevs_of_list xs). f i *\<^sub>R xs ! i)"
    unfolding pdevs_val_setsum by (simp add: pdevs_apply_pdevs_of_list less_degree_pdevs_of_list_imp_less_length)
  also have "\<dots> = (\<Sum>i<degree ?coll. (f i * r i) *\<^sub>R (listsum xs))"
    by (simp add: r less_degree_pdevs_of_list_imp_less_length)
  also have "\<dots> = (\<Sum>i<degree ?coll. f i * r i) *\<^sub>R (listsum xs)"
    by (simp add: algebra_simps scaleR_setsum_left)
  finally have eq: "pdevs_val f ?coll = (\<Sum>i<degree ?coll. f i * r i) *\<^sub>R (listsum xs)"
    (is "_ = ?e *\<^sub>R _")
    .

  have "abs (pdevs_val f ?coll) \<le> tdev ?coll"
    using assms(4)
    by (intro abs_pdevs_val_le_tdev) (auto simp: Pi_iff less_imp_le deg_pos)
  also have "\<dots> = listsum (map abs xs)" using assms by simp
  also note eq
  finally have less: "\<bar>?e\<bar> *\<^sub>R abs (listsum xs) \<le> listsum (map abs xs)" by (simp add: abs_scaleR)
  also have "\<bar>listsum xs\<bar> = listsum (map abs xs)"
    using coll `x \<noteq> 0` nlex
    by (rule abs_listsum_coll)
  finally have "?e \<in> {-1 .. 1}"
    by (auto simp add: less_le scaleR_le_cancel_right)
  thus ?thesis using eq ..
qed

lemma abs_pdevs_val_less_tdev: "e \<in> UNIV \<rightarrow> {-1 <..< 1} \<Longrightarrow> degree x > 0 \<Longrightarrow> \<bar>pdevs_val e x\<bar> < tdev x"
  apply (auto simp: pdevs_val_setsum tdev_def abs_scaleR Pi_iff
    intro!: le_less_trans[OF setsum_abs] setsum_strict_mono_ex1 scaleR_left_le_one_le
    intro: abs_leI)
  apply (metis (poly_guards_query) abs_less_iff minus_less_iff order.strict_implies_order)
  apply (rule bexI[where x="degree x - 1"])
  apply (rule neq_le_trans)
  using degree_least_nonzero[of x]
  apply (simp add: scaleR_cancel_right1)
  apply (metis abs_less_iff less_numeral_extra(4) minus_less_iff)
  apply (auto simp: less_imp_le intro!: scaleR_left_le_one_le intro!: abs_leI)
  done

lemma pdevs_val_coll_strict:
  assumes coll: "list_all (coll 0 x) xs"
  assumes nlex: "list_all (\<lambda>x. lex x 0) xs"
  assumes "x \<noteq> 0"
  assumes "f \<in> UNIV \<rightarrow> {-1 <..< 1}"
  obtains e where "e \<in> {-1 <..< 1}" "pdevs_val f (pdevs_of_list xs) = e *\<^sub>R (listsum xs)"
proof cases
  assume "listsum xs = 0"
  from listsum_nlex_eq_zeroI[OF nlex this]
  have "pdevs_of_list xs = zero_pdevs"
    by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem)
  hence "0 \<in> {-1 <..< 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *\<^sub>R listsum xs"
    by simp_all
  thus ?thesis ..
next
  assume "listsum xs \<noteq> 0"
  have "listsum (map abs xs) \<ge> 0"
    by (auto intro!: listsum_nonneg)
  hence [simp]: "\<not>listsum (map abs xs) \<le> 0"
    by (metis `listsum xs \<noteq> 0` abs_le_zero_iff antisym_conv listsum_abs)

  have "\<exists>x \<in> set xs. x \<noteq> 0"
    by (rule ccontr) (auto dest!: listsum_eq0I simp: `listsum xs \<noteq> 0`)
  then obtain i where i: "i < length xs" "xs ! i \<noteq> 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 (listsum xs)) xs"
  proof (rule list_allI)
    fix y assume "y \<in> set xs"
    hence "coll 0 x y"
      using coll by (auto simp: list_all_iff)
    also have "coll 0 x (listsum xs)"
      using coll by (auto simp: list_all_iff intro!: coll_listsum)
    finally (coll_trans)
    show "coll 0 (listsum xs) y"
      by (simp add: coll_commute `x \<noteq> 0`)
  qed

  {
    fix i assume "i < length xs"
    hence "\<exists>r. xs ! i = r *\<^sub>R (listsum xs)"
      by (metis (mono_tags, lifting) `listsum xs \<noteq> 0` coll_scale collist list_all_iff nth_mem)
  } then obtain r where r: "\<And>i. i < length xs \<Longrightarrow> (xs ! i) = r i *\<^sub>R (listsum xs)"
    by metis
  let ?coll = "pdevs_of_list xs"
  have "pdevs_val f (pdevs_of_list xs) =
      (\<Sum>i<degree (pdevs_of_list xs). f i *\<^sub>R xs ! i)"
    unfolding pdevs_val_setsum
    by (simp add: less_degree_pdevs_of_list_imp_less_length pdevs_apply_pdevs_of_list)
  also have "\<dots> = (\<Sum>i<degree ?coll. (f i * r i) *\<^sub>R (listsum xs))"
    by (simp add: r less_degree_pdevs_of_list_imp_less_length)
  also have "\<dots> = (\<Sum>i<degree ?coll. f i * r i) *\<^sub>R (listsum xs)"
    by (simp add: algebra_simps scaleR_setsum_left)
  finally have eq: "pdevs_val f ?coll = (\<Sum>i<degree ?coll. f i * r i) *\<^sub>R (listsum xs)"
    (is "_ = ?e *\<^sub>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 "\<dots> = listsum (map abs xs)" using assms by simp
  also note eq
  finally have less: "\<bar>?e\<bar> *\<^sub>R abs (listsum xs) < listsum (map abs xs)" by (simp add: abs_scaleR)
  also have "\<bar>listsum xs\<bar> = listsum (map abs xs)"
    using coll `x \<noteq> 0` nlex
    by (rule abs_listsum_coll)
  finally have "?e \<in> {-1 <..< 1}"
    by (auto simp add: less_le scaleR_le_cancel_right)
  thus ?thesis using eq ..
qed

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

lemma
  pdevs_val_independent_pdevs2:
  assumes "e \<in> UNIV \<rightarrow> I"
  shows "\<exists>e'. e' \<in> UNIV \<rightarrow> I \<and> 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 listsum ?coll = 0 then e else e \<circ> op + (Suc 0)"
  have "pdevs_val e (pdevs_of_list (independent_pdevs (x#xs))) =
    e 0 *\<^sub>R (listsum ?coll) + pdevs_val ?e0 (pdevs_of_list (independent_pdevs ?ncoll))"
    (is "_ = ?vc + ?vnc")
    by (simp add: Let_def)
  also
  have e_split: "(\<lambda>_. e 0) \<in> UNIV \<rightarrow> I" "?e0 \<in> UNIV \<rightarrow> I"
    using 2(2) by auto
  from 2(1)[OF refl pair_collapse refl e_split(2)]
  obtain e' where e': "e' \<in> UNIV \<rightarrow> I" and "?vnc = pdevs_val e' (pdevs_of_list ?ncoll)"
    by (auto simp add: o_def)
  note this(2)
  also
  have "?vc = pdevs_val (\<lambda>_. 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'' \<in> UNIV \<rightarrow> I"
    and "pdevs_val (\<lambda>_. 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''' \<in> UNIV \<rightarrow> I"
    and "\<dots> = pdevs_val e''' (pdevs_of_list (x # xs))"
    by metis
  note this(2)
  finally show ?case using e''' by auto
qed

lemma
  pdevs_val_independent_pdevs:
  assumes "list_all (\<lambda>x. lex x 0) xs"
  assumes "list_all (\<lambda>x. x \<noteq> 0) xs"
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  shows "\<exists>e'. e' \<in> UNIV \<rightarrow> {-1 .. 1} \<and> 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 \<noteq> 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 \<in> UNIV \<rightarrow> {-1 .. 1}" and g: "g \<in> UNIV \<rightarrow> {-1 .. 1}"
    by blast
  note part
  also

  have "list_all (\<lambda>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 \<noteq> 0` f]
  obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *\<^sub>R listsum (filter (coll 0 x) (x#xs))"
    and f': "f' \<in> {-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 (\<lambda>x. lex x 0) ?ncoll" "list_all (\<lambda>x. x \<noteq> 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' \<in> UNIV \<rightarrow> {-1 .. 1}"
    by metis
  note this(1)
  also

  def h \<equiv> "if listsum ?coll \<noteq> 0 then rec_nat f' (\<lambda>i _. g' i) else g'"
  have "f' *\<^sub>R listsum ?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 \<in> UNIV \<rightarrow> {-1 .. 1}"
  proof
    fix i show "h i \<in> {-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 (\<lambda>x. lex x 0) xs"
  assumes "list_all (\<lambda>x. x \<noteq> 0) xs"
  assumes "e \<in> UNIV \<rightarrow> {-1 <..< 1}"
  shows "\<exists>e'. e' \<in> UNIV \<rightarrow> {-1 <..< 1} \<and> 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 \<noteq> 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 \<in> UNIV \<rightarrow> {-1 <..< 1}" and g: "g \<in> UNIV \<rightarrow> {-1 <..< 1}"
    by blast
  note part
  also

  have "list_all (\<lambda>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 \<noteq> 0` f]
  obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *\<^sub>R listsum (filter (coll 0 x) (x#xs))"
    and f': "f' \<in> {-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 (\<lambda>x. lex x 0) ?ncoll" "list_all (\<lambda>x. x \<noteq> 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' \<in> UNIV \<rightarrow> {-1 <..< 1}"
    by metis
  note this(1)
  also

  def h \<equiv> "if listsum ?coll \<noteq> 0 then rec_nat f' (\<lambda>i _. g' i) else g'"
  have "f' *\<^sub>R listsum ?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 \<in> UNIV \<rightarrow> {-1 <..< 1}"
  proof
    fix i show "h i \<in> {-1 <..< 1}"
      using f' g'
      by (cases i) (auto simp: h_def)
  qed

  ultimately show ?case by blast
qed

lemma
  pdevs_val_selsort_ccw:
  assumes "distinct xs"
  assumes "e \<in> UNIV \<rightarrow> I"
  obtains e' where "e' \<in> UNIV \<rightarrow> 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' \<in> UNIV \<rightarrow> 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 \<in> UNIV \<rightarrow> I"
  obtains e' where "e' \<in> UNIV \<rightarrow> 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' \<in> UNIV \<rightarrow> 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
  length_sorted_list_of_set:
  shows "length (sorted_list_of_set X) = card X"
  by (induction X rule: infinite_finite_induct) auto

lemma sorted_list_of_pdevs_domain_eq: "sorted_list_of_set (pdevs_domain X) = filter (op \<noteq> 0 o pdevs_apply X) [0..<degree X]"
  by (auto simp: degree_gt  intro!: sorted_distinct_set_unique sorted_filter[of "\<lambda>x. x", simplified])

lemma list_of_pdevs_eq:
  "rev (list_of_pdevs X) = (filter (op \<noteq> 0 o snd) (map (\<lambda>i. (i, pdevs_apply X i)) [0..<degree X]))"
  (is "_ = filter ?P (map ?f ?xs)")
  using map_filter[of ?f ?P ?xs]
  by (auto simp: list_of_pdevs_def o_def sorted_list_of_pdevs_domain_eq rev_map)

lemma
  map_permI:
  assumes "xs <~~> ys"
  shows "map f xs <~~> map f ys"
  using assms by induct auto

lemma rev_perm: "rev xs <~~> ys \<longleftrightarrow> xs <~~> ys"
  using perm_rev[of xs]
  apply auto
  by (metis perm.trans perm_rev rev_rev_ident)

lemma list_of_pdevs_perm_filter_nonzero:
  "map snd (list_of_pdevs X) <~~> (filter (op \<noteq> 0) (dense_list_of_pdevs X))"
proof -
  have zip_map:
    "zip [0..<degree X] (dense_list_of_pdevs X) = map (\<lambda>i. (i, pdevs_apply X i)) [0..<degree X]"
    by (auto simp: dense_list_of_pdevs_def intro!: nth_equalityI)
  have "rev (list_of_pdevs X) <~~>
      filter (op \<noteq> 0 o snd) (zip [0..<degree X] (dense_list_of_pdevs X))"
    by (auto simp: list_of_pdevs_eq o_def zip_map)
  from map_permI[OF this, of snd]
  have "map snd (list_of_pdevs X) <~~>
      map snd (filter (op \<noteq> 0 \<circ> snd) (zip [0..<degree X] (dense_list_of_pdevs X)))"
    by (simp add: rev_map[symmetric] rev_perm)
  also have "map snd (filter (op \<noteq> 0 \<circ> snd) (zip [0..<degree X] (dense_list_of_pdevs X))) =
      filter (op \<noteq> 0) (dense_list_of_pdevs X)"
    using map_filter[of snd "op \<noteq> 0" "(zip [0..<degree X] (dense_list_of_pdevs X))"]
    by (simp add: o_def dense_list_of_pdevs_def)
   finally
   show ?thesis .
qed

lemma
  pdevs_val_of_list_of_pdevs:
  assumes "e \<in> UNIV \<rightarrow> I"
  assumes "0 \<in> I"
  obtains e' where
    "pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) = pdevs_val e' X"
    "e' \<in> UNIV \<rightarrow> I"
proof -
  obtain e' where "e' \<in> UNIV \<rightarrow> I"
    and "pdevs_val e (pdevs_of_list (map snd (list_of_pdevs X))) =
      pdevs_val e' (pdevs_of_list (filter (op \<noteq> 0) (dense_list_of_pdevs X)))"
    by (rule pdevs_val_perm[OF list_of_pdevs_perm_filter_nonzero assms(1)])
  note this(2)
  also from pdevs_val_filter[OF `e' \<in> _` `0 \<in> I`, of "op \<noteq> 0" "dense_list_of_pdevs X"]
  obtain e'' where "e'' \<in> UNIV \<rightarrow> I"
    and "\<dots> = pdevs_val e'' (pdevs_of_list (dense_list_of_pdevs X))"
    by metis
  note this(2)
  also have "\<dots> = pdevs_val e'' X" by (simp add: pdevs_of_list_dense_list_of_pdevs)
  finally show ?thesis using `e'' \<in> UNIV \<rightarrow> I` ..
qed

lemma
  pdevs_val_of_list_of_pdevs2:
  assumes "e \<in> UNIV \<rightarrow> I"
  obtains e' where
    "pdevs_val e X = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))"
    "e' \<in> UNIV \<rightarrow> I"
proof -
  from list_of_pdevs_perm_filter_nonzero[of X]
  have perm: "(filter (op \<noteq> 0) (dense_list_of_pdevs X)) <~~> map snd (list_of_pdevs X)"
    by (simp add: perm_sym)
  have "pdevs_val e X = pdevs_val e (pdevs_of_list (dense_list_of_pdevs X))"
    by (simp add: pdevs_of_list_dense_list_of_pdevs)
  also from pdevs_val_partition[OF `e \<in> _`, of "dense_list_of_pdevs X" "op \<noteq> 0"]
  obtain f g where "f \<in> UNIV \<rightarrow> I" "g \<in> UNIV \<rightarrow> I"
    "\<dots> = pdevs_val f (pdevs_of_list (filter (op \<noteq> 0) (dense_list_of_pdevs X))) +
      pdevs_val g (pdevs_of_list (filter (Not \<circ> op \<noteq> 0) (dense_list_of_pdevs X)))"
    (is "_ = ?f + ?g")
    by metis
  note this(3)
  also
  have "pdevs_of_list [x\<leftarrow>dense_list_of_pdevs X . x = 0] = zero_pdevs"
    by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list dest!: nth_mem)
  hence "?g = 0" by (auto simp: o_def )
  also
  obtain e' where "e' \<in> UNIV \<rightarrow> I"
    and "?f = pdevs_val e' (pdevs_of_list (map snd (list_of_pdevs X)))"
    by (rule pdevs_val_perm[OF perm `f \<in> _`])
  note this(2)
  finally show ?thesis using `e' \<in> UNIV \<rightarrow> I` by (auto intro!: that)
qed

lemma listsum_take_pdevs_val_eq:
  "listsum (take d xs) = pdevs_val (\<lambda>i. if i < d then 1 else 0) (pdevs_of_list xs)"
proof -
  have "listsum (take d xs) = 1 *\<^sub>R listsum (take d xs)" by simp
  also note pdevs_val_const_pdevs_of_list[symmetric]
  also have "pdevs_val (\<lambda>_. 1) (pdevs_of_list (take d xs)) =
      pdevs_val (\<lambda>i. if i < d then 1 else 0) (pdevs_of_list xs)"
    by (auto simp: pdevs_apply_pdevs_of_list split: split_if_asm intro!: pdevs_val_eqI)
  finally show ?thesis .
qed

lemma pdevs_of_list_scaleR_0[simp]:
  fixes xs::"'a::real_vector list"
  shows "pdevs_of_list (map (op *\<^sub>R 0) xs) = zero_pdevs"
  by (auto simp: pdevs_apply_pdevs_of_list intro!: pdevs_eqI)

lemma degree_pdevs_of_list_scaleR:
  "degree (pdevs_of_list (map (op *\<^sub>R c) xs)) = (if c \<noteq> 0 then degree (pdevs_of_list xs) else 0)"
  by (auto simp: pdevs_apply_pdevs_of_list intro!: degree_cong)

lemma pdevs_val_pdevs_of_list_inlE:
  assumes "e \<in> UNIV \<rightarrow> I" "uminus ` I = I" "0 \<in> I"
  obtains e' where "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e' X" "e' \<in> UNIV \<rightarrow> 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 \<in> _`]
  obtain e'
  where "pdevs_val e (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e' (pdevs_of_list ?l)"
    and "e' \<in> UNIV \<rightarrow> I"
    by auto
  note this(1)
  also
  from pdevs_val_of_list_of_pdevs[OF `e' \<in> _` `0 \<in> I`, of "nlex_pdevs X"]
  obtain e'' where "pdevs_val e' (pdevs_of_list ?l) = pdevs_val e'' (nlex_pdevs X)"
    and "e'' \<in> UNIV \<rightarrow> I"
    by metis
  note this(1)
  also
  from pdevs_val_nlex_pdevs2[OF `e'' \<in> _` `_ = I`]
  obtain e''' where "pdevs_val e'' (nlex_pdevs X) = pdevs_val e''' X" "e''' \<in> UNIV \<rightarrow> I"
    by metis
  note this(1)
  finally have "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e''' X" .
  thus ?thesis using `e''' \<in> UNIV \<rightarrow> I` ..
qed

lemma lex_uminus_iff: "lex (- x) 0 \<longleftrightarrow> lex 0 x"
  by (simp add: lex_def)

lemma pdevs_val_pdevs_of_list_inl2E:
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  obtains e' where "pdevs_val e X = pdevs_val e' (pdevs_of_list (inl X))" "e' \<in> UNIV \<rightarrow> {-1 .. 1}"
proof -
  let ?l = "map snd (list_of_pdevs (nlex_pdevs X))"
  have l: "list_all (\<lambda>x. Counterclockwise_2D_Arbitrary.lex x 0) ?l"
    "list_all (\<lambda>x. x \<noteq> 0) (map snd (list_of_pdevs (nlex_pdevs X)))"
    by (auto simp: list_all_iff list_of_pdevs_def lex_uminus_iff)

  from pdevs_val_nlex_pdevs[OF assms(1)]
  obtain e' where "e' \<in> UNIV \<rightarrow> {-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' \<in> _`]
  obtain e'' where "e'' \<in> UNIV \<rightarrow> {-1 .. 1}" "\<dots> = pdevs_val e'' (pdevs_of_list ?l)"
    by metis
  note this(2)
  also from pdevs_val_independent_pdevs[OF l `e'' \<in> _`]
  obtain e'''
  where "e''' \<in> UNIV \<rightarrow> {-1 .. 1}"
    and "\<dots> = pdevs_val e''' (pdevs_of_list (independent_pdevs ?l))"
    by metis
  note this(2)
  also have "\<dots> = 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''' \<in> _` ..
qed

lemma
  in_set_half_segments_of_aform_aform_valE:
  assumes "(x2, y2) \<in> set (half_segments_of_aform X)"
  obtains e where "y2 = aform_val e X" "e \<in> UNIV \<rightarrow> {-1 .. 1}"
proof -
  from assms obtain d where
    "y2 = lowest_vertex (fst X, nlex_pdevs (snd X)) +
      listsum (take (Suc d) (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X)))))"
    by (auto simp: half_segments_of_aform_def elim!: in_set_polychain_of_imp_listsum)
  also have "lowest_vertex (fst X, nlex_pdevs (snd X)) =
      fst X - listsum (map snd (list_of_pdevs (nlex_pdevs (snd X))))"
    by (simp add: lowest_vertex_def)
  also have "listsum (map snd (list_of_pdevs (nlex_pdevs (snd X)))) =
      pdevs_val (\<lambda>_. 1) (nlex_pdevs (snd X))"
    by (auto simp: pdevs_val_listsum)
  also

  have "listsum (take (Suc d) (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X))))) =
      pdevs_val (\<lambda>i. if i \<le> d then 2 else 0) (pdevs_of_list (ccw.selsort 0 (inl (snd X))))"
    (is "_ = pdevs_val ?e _")
    by (subst listsum_take_pdevs_val_eq)
      (auto simp: pdevs_val_setsum if_distrib pdevs_apply_pdevs_of_list
        degree_pdevs_of_list_scaleR intro!: setsum.cong )
  also
  from pdevs_val_selsort_ccw2[of "inl (snd X)" ?e "{0 .. 2}"]
  obtain e'' where "\<dots> = pdevs_val e'' (pdevs_of_list (inl (snd X)))" "e'' \<in> UNIV \<rightarrow> {0..2}"
    by auto
  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'' \<in> _`]
  obtain e'''
  where "pdevs_val e'' (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e''' (pdevs_of_list ?l)"
    and "e''' \<in> UNIV \<rightarrow> {0..2}"
    by auto
  note this(1)
  also
  have "0 \<in> {0 .. 2::real}" by simp
  from pdevs_val_of_list_of_pdevs[OF `e''' \<in> _` 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'''' \<in> UNIV \<rightarrow> {0 .. 2}"
    by metis
  note this(1)
  finally have
    "y2 = fst X + (pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (\<lambda>_. 1) (nlex_pdevs (snd X)))"
    by simp
  also have "pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (\<lambda>_. 1) (nlex_pdevs (snd X)) =
      pdevs_val (\<lambda>i. e'''' i - 1) (nlex_pdevs (snd X))"
    by (simp add: pdevs_val_minus)
  also
  have "(\<lambda>i. e'''' i - 1) \<in> UNIV \<rightarrow> {-1 .. 1}" using `e'''' \<in> _` by auto
  from pdevs_val_nlex_pdevs2[OF this]
  obtain f where "f \<in> UNIV \<rightarrow>  {-1 .. 1}"
    and "pdevs_val (\<lambda>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 \<in> _` ..
qed

lemma fst_hd_polychain_of: "xs \<noteq> [] \<Longrightarrow> fst (hd (polychain_of x xs)) = x"
  by (cases xs) (auto simp: )

lemma fst_hd_half_segments_of_aform:
  assumes "half_segments_of_aform X \<noteq> []"
  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 ccw'_sortedP_translate_comp[simp]:
  "linorder_list0.sortedP (ccw' x0) (map (op + x \<circ> g) xs) \<longleftrightarrow>
    linorder_list0.sortedP (ccw' (x0 - x)) (map g xs)"
  apply (induct xs arbitrary: x0 x)
  apply (auto elim!: linorder_list0.sortedP_Cons intro!: linorder_list0.sortedP.Cons
    linorder_list0.sortedP.Nil)
  apply (metis add.commute add_diff_cancel ccw'.translate_plus3 diff_Pair)
  by (smt add.commute add_Pair ccw'.translate_plus' diff_add_cancel)

lemma polychain_of_add: "polychain_of (x + y) xs = map ((op + (y, y))) (polychain_of x xs)"
  by (induct xs arbitrary: x y) (auto simp: algebra_simps)

lemma snd_plus_commute: "snd \<circ> op + (x0, x0) = op + x0 o snd"
  by auto

lemma ccw'_sortedP_renormalize:
  "linorder_list0.sortedP (ccw' a) (map snd (polychain_of (x0 + x) xs)) \<longleftrightarrow>
  linorder_list0.sortedP (ccw' (a - x0)) (map snd (polychain_of x xs))"
  unfolding polychain_of_add add.commute
  by (simp add: snd_plus_commute)

lemma ccw'_sortedP_polychain_of01:
  shows "linorder_list0.sortedP (ccw' 0) [u] \<Longrightarrow> linorder_list0.sortedP (ccw' x0) (map snd (polychain_of x0 [u]))"
    and "linorder_list0.sortedP (ccw' 0) [] \<Longrightarrow> linorder_list0.sortedP (ccw' x0) (map snd (polychain_of x0 []))"
  by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons  simp: ac_simps)

lemma ccw'_sortedP_polychain_of2:
  assumes "linorder_list0.sortedP (ccw' 0) [u, v]"
  shows "linorder_list0.sortedP (ccw' x0) (map snd (polychain_of x0 [u, v]))"
  using assms
  by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
    elim!: linorder_list0.sortedP_Cons simp: ac_simps ccw'.translate_origin)

lemma ccw'_sortedP_polychain_of3:
  assumes "linorder_list0.sortedP (ccw' 0) (u#v#w#xs)"
  shows "linorder_list0.sortedP (ccw' x0) (map snd (polychain_of x0 (u#v#w#xs)))"
  using assms
proof (induct xs arbitrary: x0 u v w)
  case Nil
  hence "ccw' 0 u v" "ccw' 0 v w" "ccw' 0 u w"
    by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ac_simps)
  thus ?case
    apply (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ac_simps ccw'.translate_origin)
    unfolding ccw'_def
    apply (auto intro!: disjI1 simp: det3_def' algebra_simps)
    done
next
  case (Cons y ys)
  have s1: "linorder_list0.sortedP (ccw' 0)  ((u + v)#w#y#ys)" using Cons.prems
    by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ccw'.add1)
  have s2: "linorder_list0.sortedP (ccw' 0)  (u#(v + w)#y#ys)" using Cons.prems
    by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ccw'.add3 ccw'.add1)
  have s3: "linorder_list0.sortedP (ccw' 0)  (u#v#(w + y)#ys)" using Cons.prems
    by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ccw'.add3 ccw'.add1)
  show ?case
    using Cons.hyps[OF s1, of x0] Cons.hyps[OF s2, of x0] Cons.hyps[OF s3, of x0] Cons.prems
    by (auto intro!: linorder_list0.sortedP.Nil linorder_list0.sortedP.Cons
      elim!: linorder_list0.sortedP_Cons simp: ac_simps)
qed

lemma ccw'_sortedP_polychain_of_snd:
  assumes "linorder_list0.sortedP (ccw' 0) xs"
  shows "linorder_list0.sortedP (ccw' x0) (map snd (polychain_of x0 xs))"
  using assms
  by (metis ccw'_sortedP_polychain_of01 ccw'_sortedP_polychain_of2 ccw'_sortedP_polychain_of3
    list.exhaust)

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 ccw'_sortedPP_implies_distinct:
  assumes "ccw'.sortedP x qs"
  shows "distinct qs"
  using assms
  apply induct
   apply auto
  using ccw'_contra
  apply blast
  done

lemma ccw'_sortedPP_implies_nonaligned:
  assumes "ccw'.sortedP x qs"
  assumes "y \<in> set qs" "z \<in> set qs" "y \<noteq> z"
  shows "\<not> coll x y z"
  using assms
  by induct (force simp: ccw'_def det3_def' algebra_simps)+

lemma polychain_of_ccw_convex:
  assumes "e \<in> UNIV \<rightarrow> {0 <..< 1}"
  assumes sorted: "linorder_list0.sortedP (ccw' 0) (P#Q#Ps)"
  shows "list_all (\<lambda>(xi, xj). ccw' xi xj (Pc + (\<Sum>P \<in> set (P#Q#Ps). e P *\<^sub>R P))) (polychain_of Pc (P#Q#Ps))"
  using assms(1) ccw'_sortedPP_implies_nonaligned[OF assms(2)] assms(2)
  --"TODO: clean up proof, not feed in stupid additional assumption"
proof (induct Ps arbitrary: P Q Pc)
  case Nil
  have eq: "e P *\<^sub>R P + e Q *\<^sub>R Q - P = (1 - e P) *\<^sub>R (- P) + e Q *\<^sub>R Q"
    using `e \<in> _`
    by (auto simp add: algebra_simps)
  from Nil ccw'_sortedPP_implies_distinct[OF Nil(3)] have "P \<noteq> Q" "e P < 1" "0 < e Q" "ccw' 0 P Q"
    by (auto elim!: linorder_list0.sortedP_Cons)
  thus ?case
    by (auto simp: ccw'_not_coll ccw'.translate_origin eq)
next
  case (Cons R Rs)
  hence "ccw' 0 P Q" "P \<noteq> Q" using ccw'_sortedPP_implies_distinct[OF Cons(4)]
    by (auto elim!: linorder_list0.sortedP_Cons)
  have "list_all (\<lambda>(xi, xj). ccw' xi xj ((Pc + P) + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P)))
    (polychain_of (Pc + P) (Q # R # Rs))"
    using Cons(2-)
    by (intro Cons(1)) (auto elim: linorder_list0.sortedP_Cons)
  also have "polychain_of (Pc + P) (Q # R # Rs) = tl (polychain_of Pc (P # Q # R # Rs))"
    by simp
  finally have "list_all (\<lambda>(xi, xj). ccw' xi xj (Pc + P + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P)))
    (tl (polychain_of Pc (P # Q # R # Rs)))" .
  moreover
  have "list_all (\<lambda>(xi, xj). ccw' xi xj (P + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P))) (polychain_of P (Q # R # Rs))"
    using Cons(2-)
    by (intro Cons(1)) (auto elim: linorder_list0.sortedP_Cons)
  have "(\<lambda>(xi, xj). ccw' xi xj (Pc + P + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P)))
    (hd (polychain_of Pc (P # Q # R # Rs)))"
    using Cons(4) Cons(2) Cons(3)[of P Q] Cons(3)[of Q R] Cons(3)[of P R]
    by (auto simp add: Pi_iff add.assoc simp del: scaleR_Pair intro!: ccw'.setsum
        elim!: linorder_list0.sortedP_Cons)
  ultimately
  have "list_all (\<lambda>(xi, xj). ccw' xi xj (P + (Pc + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P)))) (polychain_of Pc (P # Q # R # Rs))"
    by (simp add: ac_simps)
  hence "list_all (\<lambda>(xi, xj). ccw' xi xj (e P *\<^sub>R P + (Pc + (\<Sum>P\<in>set (Q # R # Rs). e P *\<^sub>R P)))) (polychain_of Pc (P # Q # R # Rs))"
    apply (rule list_all_mp)
    apply (simp del: polychain_of.simps add: split_beta)
    apply (subst ccw'.translate_origin, simp)
    apply (subst (asm) ccw'.translate_origin)
  proof auto
    case goal1
    have e: "1 - e P > 0" using Cons(2)
      apply (auto simp: Pi_iff algebra_simps)
      by (metis prod.collapse)
    from `ccw' 0 P Q`
    have "ccw' 0 Q (-P)"
      by simp
    hence "ccw' 0 Q ((1 - e P) *\<^sub>R - P)" using e
      by simp
    hence "ccw' 0 Q (- (1 - e P) *\<^sub>R P)"
      by (auto simp: algebra_simps)
    hence "ccw' 0 Q (-(1 - e P) *\<^sub>R P + (\<Sum>P\<in>insert Q (insert R (set Rs)). e P *\<^sub>R P))"
      using goal1
      by (intro ccw'.add3) (simp_all add: algebra_simps)
    thus ?case
      by (auto simp: algebra_simps)
  next
    case goal2
    have e: "1 - e P > 0" using Cons(2)
      apply (auto simp: Pi_iff algebra_simps)
      by (metis prod.collapse)
    have "ccw' 0 P R" using Cons
      by (auto elim!: linorder_list0.sortedP_Cons)
    hence "ccw' 0 ((1 - e P) *\<^sub>R P) R"
      by (simp add: e)
    hence "ccw' 0 R ((1 - e P) *\<^sub>R (- P) + ((\<Sum>P\<in>insert Q (insert R (set Rs)). e P *\<^sub>R P) - Q))"
      using Cons(2) goal2
      by (intro ccw'.add3) simp_all
    thus ?case by (simp add: algebra_simps)
  next
    case goal3
    have e: "1 - e P > 0" using Cons(2)
      by (cases P) (auto simp: Pi_iff algebra_simps split: prod.split)
    from goal3(2)[THEN  in_set_polychain_ofD] Cons(4)
    have "ccw' 0 P (aa - a, ba - b)"
      by (auto elim!: linorder_list0.sortedP_Cons)
    hence "ccw' 0 (aa - a, ba - b) (-P)"
      by simp
    hence "ccw' 0 (aa - a, ba - b) ((1 - e P) *\<^sub>R - P)"
      by (simp_all add: e)
    hence "ccw' 0 (aa - a, ba - b) ((1 - e P) *\<^sub>R (- P) + (P + (Pc + (\<Sum>P\<in>insert Q (insert R (set Rs)). e P *\<^sub>R P)) - (a, b)))"
      using Cons(2) goal3
      by (intro ccw'.add3) (auto simp: algebra_simps)
    thus ?case by (simp add: algebra_simps)
  qed
  thus ?case
    using ccw'_sortedPP_implies_distinct[OF Cons(4)]
    using Cons by (simp add: ac_simps)
qed

lemma polychain_of_ccw:
  assumes "e \<in> UNIV \<rightarrow> {0 <..< 1}"
  assumes sorted: "ccw'.sortedP 0 qs"
  assumes qs: "length qs \<noteq> 1"
  shows "list_all (\<lambda>(xi, xj). ccw' xi xj (Pc + (\<Sum>P \<in> set qs. e P *\<^sub>R P))) (polychain_of Pc qs)"
  using assms
proof (cases qs)
  case Nil
  thus ?thesis by simp
next
  case (Cons Q Qs)
  note CQ = this
  show ?thesis
  proof (cases Qs)
    case Nil
    thus ?thesis
      using assms
      unfolding CQ
      by (cases Q, cases Pc) simp
  next
    case (Cons R Rs)
    show ?thesis
      unfolding CQ Cons
      apply (intro polychain_of_ccw_convex)
      apply fact
      using assms defer
      using assms unfolding CQ Cons apply auto
      done
  qed
qed

lemma in_polychain_of_ccw:
  assumes "e \<in> UNIV \<rightarrow> {0 <..< 1}"
  assumes "ccw'.sortedP 0 qs"
  assumes "length qs \<noteq> 1"
  assumes "seg \<in> set (polychain_of Pc qs)"
  shows "ccw' (fst seg) (snd seg) (Pc + (\<Sum>P \<in> set qs. e P *\<^sub>R P))"
  using polychain_of_ccw[OF assms(1,2,3)] assms(4)
  by (simp add: list_all_iff split_beta)

lemma list_all_list_of_pdevsI:
  assumes "\<And>i. i \<in> pdevs_domain X \<Longrightarrow> P (pdevs_apply X i)"
  shows "list_all (\<lambda>x. P x) (map snd (list_of_pdevs X))"
  using assms by (auto simp: list_all_iff list_of_pdevs_def)

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

lemma list_of_pdevs_all_nonzero: "list_all (\<lambda>x. x \<noteq> 0) (map snd (list_of_pdevs xs))"
  by (auto simp: list_of_pdevs_def list_all_iff)

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

lemma (in comm_monoid_add) listsum_distinct_selsort:
  assumes "distinct xs"
  shows "listsum (linorder_list0.selsort LE xs) = listsum xs"
  using assms
  apply (simp add: distinct_listsum_conv_Setsum linorder_list0.distinct_selsort)
  apply (rule setsum.cong)
  apply (simp add: linorder_list0.set_selsort)
  apply simp
  done

lemma pdevs_of_list_map_scaleR: "pdevs_of_list (map (scaleR r) xs) = scaleR_pdevs r (pdevs_of_list xs)"
  by (auto intro!: pdevs_eqI simp: pdevs_apply_pdevs_of_list)

lemma half_segments_of_aform_strict:
  assumes "e \<in> UNIV \<rightarrow> {-1 <..< 1}"
  assumes "seg \<in> set (half_segments_of_aform X)"
  assumes "length (half_segments_of_aform X) \<noteq> 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 (op *\<^sub>R 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))) \<noteq> 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' \<in> UNIV \<rightarrow> {-1 <..< 1}" "pdevs_val e (snd X) = pdevs_val e' (nlex_pdevs (snd X))"
    using pdevs_val_nlex_pdevs[OF `e \<in> _`]
    by auto
  note this(2)
  also obtain e'' where "e'' \<in> UNIV \<rightarrow> {-1 <..< 1}"
    "\<dots> = 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' \<in> _`])
  note this(2)
  also
  obtain e''' where "e''' \<in> UNIV \<rightarrow> {-1 <..< 1}" "\<dots> = 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'' \<in> _`]
    by metis
  note this(2)
  also
  from pdevs_val_selsort_ccw[OF distinct_inl `e''' \<in> _`]
  obtain f where "f \<in> UNIV \<rightarrow> {-1 <..< 1}"
    "\<dots> = 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 "\<dots> = pdevs_val (\<lambda>i. f i + 1) (pdevs_of_list ?sl) +
      lowest_vertex (fst X, nlex_pdevs (snd X)) - fst X"
    apply (simp add: pdevs_val_add lowest_vertex_def algebra_simps pdevs_val_listsum
      inl_def listsum_list_of_pdevs )
    apply (subst dense_list_of_pdevs_pdevs_of_list)
    apply (auto simp: in_set_independent_pdevs_nonzero)[1]
    apply (subst listsum_distinct_selsort)
    apply simp
    apply (simp add: listsum_independent_pdevs listsum_list_of_pdevs)
    done
  also have "pdevs_val (\<lambda>i. f i + 1) (pdevs_of_list ?sl) =
      pdevs_val (\<lambda>i. 1/2 * (f i + 1)) (pdevs_of_list (map (op *\<^sub>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' \<in> UNIV \<rightarrow> {0<..<1}" using `f \<in> _`
    by (auto simp: distinct_map_scaleRI Pi_iff algebra_simps real_0_less_add_iff)
  from pdevs_of_list_setsum[OF this]
  obtain g where "g \<in> UNIV \<rightarrow> {0<..<1}"
    "pdevs_val ?f' (pdevs_of_list ?ssl) = (\<Sum>P\<in>set ?ssl. g P *\<^sub>R P)"
    by blast
  note this(2)
  finally have "aform_val e X = lowest_vertex (fst X, nlex_pdevs (snd X)) + (\<Sum>P\<in>set ?ssl. g P *\<^sub>R P)"
    by simp
  also
  have "ccw' (fst seg) (snd seg) \<dots>"
    apply (rule in_polychain_of_ccw[OF `g \<in> _` _
        len
        `seg \<in> _`[unfolded half_segments_of_aform_def Let_def]])
    by (simp add: ccw'_sortedP_scaled_inl)
  finally show ?thesis .
qed

definition "mirror_point x y = 2 *\<^sub>R x - y"

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

lemma list_allD: "list_all P xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> P x"
  by (auto simp: list_all_iff)

lemma minus_one_less_multI:
  fixes e x::real
  shows "- 1 \<le> e \<Longrightarrow> 0 < x \<Longrightarrow> x < 1 \<Longrightarrow> - 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 \<le> 1 \<Longrightarrow> 0 < x \<Longrightarrow> x < 1 \<Longrightarrow> e * x < 1"
  by (metis (erased, hide_lams) less_eq_real_def monoid_mult_class.mult.left_neutral
    mult_strict_mono zero_less_one)

definition segments_of_aform::"point aform \<Rightarrow> (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 mirror_half_segments_of_aform:
  assumes "e \<in> UNIV \<rightarrow> {-1 <..< 1}"
  assumes "length (half_segments_of_aform X) \<noteq> 1"
  shows "list_all (\<lambda>seg. ccw' (fst seg) (snd seg) (aform_val e X)) (map (pairself (mirror_point (fst X))) (half_segments_of_aform X))"
proof -
  have "- e \<in> UNIV \<rightarrow> {-1 <..< 1}" using assms by auto
  show ?thesis
    unfolding list_all_length
  proof safe
    case goal1
    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 *\<^sub>R fst X - aform_val e X"
      by (auto simp: aform_val_def pdevs_val_setsum algebra_simps scaleR_2 setsum_negf)
    finally have le:
      "ccw' (fst (half_segments_of_aform X ! n)) (snd (half_segments_of_aform X ! n))
        (2 *\<^sub>R fst X - aform_val e X)"
      .

    have eq: "(map (pairself (mirror_point (fst X))) (half_segments_of_aform X) ! n) =
      (2 *\<^sub>R fst X - fst ((half_segments_of_aform X) ! n),
       2 *\<^sub>R fst X - snd ((half_segments_of_aform X) ! n))"
      apply (cases "half_segments_of_aform X ! n")
      apply (cases "2 *\<^sub>R fst X")
      using goal1
      by (auto simp add: mirror_point_def )
    show ?case
      using le
      unfolding eq
      by (auto simp: algebra_simps ccw'_def det3_def')
  qed
qed

lemma segments_of_aform_strict:
  assumes "e \<in> UNIV \<rightarrow> {-1 <..< 1}"
  assumes "length (half_segments_of_aform X) \<noteq> 1"
  shows "list_all (\<lambda>seg. ccw' (fst seg) (snd seg) (aform_val e X)) (segments_of_aform X)"
  using assms
  apply -
  apply (auto simp: segments_of_aform_def Let_def mirror_half_segments_of_aform)
  apply (auto intro!: half_segments_of_aform_strict simp: list_all_iff)
  done

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_setsum algebra_simps scaleR_2 setsum_negf)

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

subsection {* now generalize continuously *}

lemma LIMSEQ_minus_fract_mult:
  "(\<lambda>n. r * (1 - 1 / real (Suc (Suc n)))) ----> r"
  apply (rule tendsto_eq_rhs)
  apply (rule tendsto_mult)
  apply (auto simp: inverse_eq_divide[symmetric]
    intro: filterlim_compose[OF LIMSEQ_inverse_real_of_nat filterlim_Suc] tendsto_intros)
  done

lemma ccw_coll_segments_of_aform:
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes "length (half_segments_of_aform X) \<noteq> 1"
  shows "list_all (\<lambda>seg. det3 (fst seg) (snd seg) (aform_val e X) \<ge> 0) (segments_of_aform X)"
  unfolding list_all_iff
proof safe
  fix a b c d
  assume seg: "((a, b), c, d) \<in> set (segments_of_aform X)" (is "?seg \<in> _")
  --{* TODO: get rid of normal-of-segment / support-of-segment*}
  def normal_of_segment\<equiv>"\<lambda>((a0, a1), b0, b1). (b1 - a1, a0 - b0)::real*real"
  def support_of_segment\<equiv>"\<lambda>(a, b). normal_of_segment (a, b) \<bullet> a"
  have "closed ((\<lambda>x. x \<bullet> normal_of_segment ?seg) -` {..support_of_segment ?seg})" (is "closed ?cl")
    by (auto intro!: continuous_intros closed_vimage)
  moreover
  def f \<equiv> "\<lambda>n i. e i * ( 1 - 1 / (Suc (Suc n)))"
  have "\<forall>n. aform_val (f n) X \<in> ?cl"
  proof
    fix n
    have "f n \<in> UNIV \<rightarrow> {-1 <..< 1}"
      using assms
      by (auto simp: f_def Pi_iff diff_less_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 \<in> (\<lambda>x. x \<bullet> 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 "\<And>i. (\<lambda>n. f n i) ----> e i"
    unfolding f_def
    by (rule LIMSEQ_minus_fract_mult)
  hence "(\<lambda>n. aform_val (f n) X) ----> aform_val e X"
    by (auto simp: aform_val_def pdevs_val_setsum intro!: tendsto_intros)
  ultimately have "aform_val e X \<in> ?cl"
    by (rule closed_sequentially)
  thus "det3 (fst ?seg) (snd ?seg) (aform_val e X) \<ge> 0"
    by (auto simp: list_all_iff normal_of_segment_def support_of_segment_def det3_def' field_simps
      inner_prod_def)
qed

lemma ccw_coll_segments_of_aformI:
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes "length (half_segments_of_aform X) \<noteq> 1"
  assumes "seg \<in> set (segments_of_aform X)"
  shows "det3 (fst seg) (snd seg) (aform_val e X) \<ge> 0"
  using assms ccw_coll_segments_of_aform by (auto simp: list_all_iff)

lemma ccw_half_segments_of_aform_strictI:
  assumes "e \<in> UNIV \<rightarrow> {-1 <..< 1}"
  assumes "(s1, s2) \<in> set (half_segments_of_aform X)"
  assumes "length (half_segments_of_aform X) \<noteq> 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

primrec dirvec where "dirvec (x, y) = (y - x)"
lemma dirvec_minus: "dirvec x = snd x - fst x"
  by (cases x) simp

lemma dirvec_nth_polychain_of: "n < length xs \<Longrightarrow> dirvec ((polychain_of p xs) ! n ) = (xs ! n)"
  apply (induct xs arbitrary: p n)
  apply simp
  apply (case_tac n)
  apply auto
  done

lemma
  ccw'_renormalize:
  "ccw' 0 (a - b) (c - a) \<Longrightarrow> ccw' b a c"
  by (auto simp: ccw'_def det3_def' algebra_simps)

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
    apply (auto simp: nth_Cons dirvec_minus split: nat.split elim!: ccw'.sortedP_Cons)
    apply (metis (erased, hide_lams) ccw'_renormalize in_set_conv_nth length_greater_0_conv)
    done
qed

lemma map_dirvec_polychain_of[simp]: "map dirvec (polychain_of x xs) = xs"
  by (induct xs arbitrary: x) simp_all

lemma ccw'_sortedP_scaleR: "ccw'.sortedP 0 xs \<Longrightarrow> r > 0 \<Longrightarrow> ccw'.sortedP 0 (map (op *\<^sub>R r) xs)"
  by (induct xs) (auto intro!: ccw'.sortedP.Cons elim!: ccw'.sortedP_Cons simp del: scaleR_Pair)

lemma ccw'_sortedP_uminus: "ccw'.sortedP 0 xs \<Longrightarrow> 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
  apply (intro ccw'_sortedP_subsequent )
  apply (auto simp: subsequent_half_segments half_segments_of_aform_def intro!: ccw'_sortedP_scaleR)
  apply (rule ccw_sorted_implies_ccw'_sortedP[OF inl_ncoll])
  apply force apply force apply force
  apply (simp add: sorted_inl)
  apply (simp add:)
  apply (simp add: polychain_of_subsequent_eq)
  done

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) \<noteq> 1"
  show ?thesis
    by (rule convex_polychainI)
      (simp_all add: polychain_half_segments_of_aform subsequent_half_segments_ccw
        ccw'_def[symmetric])
qed

lemma last_polychain_of: "length xs > 0 \<Longrightarrow> snd (last (polychain_of p xs)) = p + listsum xs"
  by (induct xs arbitrary: p) simp_all

lemma last_half_segments:
  assumes "half_segments_of_aform X \<noteq> []"
  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_listsum[symmetric] last_polychain_of listsum_distinct_selsort inl_def
    listsum_independent_pdevs listsum_list_of_pdevs)

lemma polychain_segments_of_aform: "polychain (segments_of_aform X)"
  apply (auto simp: segments_of_aform_def Let_def intro!: polychain_appendI)
  apply (auto simp: polychain_half_segments_of_aform polychain_map_pairself)
  by (metis (no_types, hide_lams) fst_conv fst_half_segments hd_conv_nth hd_map last_half_segments
    pairself_apply)

lemma segments_of_aform_closed:
  assumes "segments_of_aform X \<noteq> []"
  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 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 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 dirvec_hd_polychain_of: "xs \<noteq> [] \<Longrightarrow> dirvec (hd (polychain_of p xs)) = (hd xs)"
  by (simp add: hd_conv_nth dirvec_nth_polychain_of)

lemma dirvec_last_polychain_of: "xs \<noteq> [] \<Longrightarrow> dirvec (last (polychain_of p xs)) = (last xs)"
  by (simp add: last_conv_nth dirvec_nth_polychain_of)

lemma ccw'_hd_last_sorted:
  assumes "ccw'.sortedP p xs" "length xs > 1"
  shows "ccw' p (hd xs) (last xs)"
proof (cases xs)
  case (Cons y ys)
  note ys = this
  thus ?thesis
    using ys assms
    by (auto elim!: ccw'.sortedP_Cons)
qed (insert assms, simp)

lemma ccw_hd_last_sorted:
  assumes "ccw.sortedP 0 xs" "length xs > 1"
  shows "ccw 0 (hd xs) (last xs)"
proof (cases xs)
  case (Cons y ys)
  note ys = this
  thus ?thesis
    using ys assms
    by (auto elim!: ccw.sortedP_Cons)
qed (insert assms, simp)

lemma hd_distinct_neq_last: "distinct xs \<Longrightarrow> length xs > 1 \<Longrightarrow> hd xs \<noteq> 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)))"
  using assms
  apply (auto simp add: half_segments_of_aform_def Let_def
    dirvec_hd_polychain_of dirvec_last_polychain_of
    simp del: polychain_of.simps split: split_if_asm)
  apply (subst dirvec_hd_polychain_of) apply force
  apply (subst dirvec_last_polychain_of) apply force
  apply (rule ccw_ncoll_imp_ccw)
  apply (rule ccw_hd_last_sorted)
  apply (rule ccw0_sorted_scaleR)
  apply (rule sorted_inl)
  apply simp
  apply simp
  apply (subst hd_map) apply force
  apply (subst last_map) apply force
  apply simp
  apply (rule inl_ncoll[of _ X])
  apply (metis ccw.length_selsort ccw.set_selsort gr_implies_not0 hd_in_set list.size(3))
  apply (metis Suc_lessD ccw.length_selsort ccw.set_selsort last_in_set length_greater_0_conv)
  apply (auto simp: hd_distinct_neq_last)
  done

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
proof (rule convex_polychain_appendI)
  case goal4
  thus ?case
    using ccw_hd_last_half_segments_dirvec[OF assms, simplified dirvec_minus]
    apply (auto simp: dirvec_minus hd_map pairself_apply last_half_segments mirror_point_def
      fst_hd_half_segments_of_aform )
    apply (simp add: det3_def' algebra_simps ccw'_def)
    done
qed (auto
  simp: convex_polychain_half_segments_of_aform convex_polychain_map_mirror last_half_segments
    hd_map pairself_apply fst_hd_half_segments_of_aform
  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 \<noteq> []"
    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) \<in> set (segments_of_aform X)"
  obtains x where "(x, y) \<in> set (segments_of_aform X)"
proof -
  from assms have ne[simp]: "segments_of_aform X \<noteq> []"
    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) \<in> 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)) \<in> set (segments_of_aform X)"
      apply (simp )
      by (metis Suc Suc_lessD i(1) in_set_conv_nth)
    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) \<in> set (segments_of_aform X)" .
    thus ?thesis ..
  qed
qed

subsection {* Encompassing *}
text {* TODO: should not be necessary anymore... *}
definition "encompasses x seg \<longleftrightarrow> det3 (fst seg) (snd seg) x \<ge> 0"

lemma encompasses_algebra: "encompasses x seg \<longleftrightarrow>
    fst x * (snd (snd seg) - snd (fst seg)) + snd x * (fst (fst seg) - fst (snd seg))
    \<le> (snd (snd seg) - snd (fst seg)) * fst (fst seg) + (fst (fst seg) - fst (snd seg)) * snd (fst seg)"
  by (auto simp: encompasses_def inner_prod_def det3_def' algebra_simps)

lemma encompasses_cases:
  "encompasses x seg \<or> encompasses x (snd seg, fst seg)"
  by (auto simp: encompasses_algebra 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_det3_equality:
  shows "det3 i j k *\<^sub>R p = det3 j k p *\<^sub>R i + det3 k i p *\<^sub>R j + det3 i j p *\<^sub>R k"
  by (cases p, cases i, cases j, cases k) (auto simp: det3_def' algebra_simps)

lemma triangle_encompassing_polychain_of:
  assumes "encompasses p (a, b)" "encompasses p (b, c)" "encompasses p (c, a)"
  assumes "ccw' a b c"
  shows "p \<in> convex hull {a, b, c}"
proof -
  from assms have nn: "det3 b c p \<ge> 0" "det3 c a p \<ge> 0" "det3 a b p \<ge> 0" "det3 a b c \<ge> 0"
    by (auto simp: encompasses_algebra det3_def' algebra_simps)
  have "det3 a b c *\<^sub>R p = det3 b c p *\<^sub>R a + det3 c a p *\<^sub>R b + det3 a b p *\<^sub>R c"
    by (rule triangle_det3_equality)
  hence "inverse (det3 a b c) *\<^sub>R (det3 a b c *\<^sub>R p) = inverse (det3 a b c) *\<^sub>R (det3 b c p *\<^sub>R a + det3 c a p *\<^sub>R b + det3 a b p *\<^sub>R c)"
    by simp
  with assms have p_eq: "p =
    (det3 b c p / det3 a b c) *\<^sub>R a + (det3 c a p / det3 a b c) *\<^sub>R b + (det3 a b p / det3 a b c) *\<^sub>R c"
    (is "_ = scaleR ?u _ + scaleR ?v _ + scaleR ?w _")
    by (simp add: inverse_eq_divide algebra_simps ccw'_def)
  show ?thesis
    unfolding convex_hull_3
    apply rule
    apply (rule exI[where x="?u"])
    apply (rule exI[where x="?v"])
    apply (rule exI[where x="?w"])
    apply (safe intro!: p_eq divide_nonneg_nonneg nn)
    apply (simp add: add_divide_distrib[symmetric])
    using assms(4)
    apply (auto simp: det3_def' algebra_simps ccw'_def)
    done
qed

lemma ccw_coll_cyclic: "det3 p q r \<ge> 0 \<Longrightarrow> det3 q r p \<ge> 0"
  by (auto simp: algebra_simps zero_prod_def det3_def')

lemma convex_polygon_skip:
  assumes "convex_polygon (x # y # z # w # ws)"
  assumes "ccw'.sortedP (fst x) (map snd (butlast (x # y # z # w # ws)))"
  shows "convex_polygon ((fst x, snd y) # z # w # ws)"
  using assms by (auto elim!: ccw'.sortedP_Cons simp: ccw'_def[symmetric])

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 \<in> convex hull (set (map fst (x#y#z#zs)))"
  using assms
proof (induct zs arbitrary: x y z p)
  case Nil
  hence "p \<in> convex hull {fst x, fst y, fst z}"
    by (cases x, cases y)
      (auto intro!: triangle_encompassing_polychain_of simp: ccw'_def[symmetric])
  thus ?case
    by simp
next
  case (Cons w ws)
  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 \<in> convex hull {fst x, fst y, snd y}"
      using Cons.prems
      by (cases x, cases y)
        (auto intro!: triangle_encompassing_polychain_of simp: ccw'_def[symmetric])
    thus ?case
      apply (rule set_rev_mp)
      apply (rule hull_mono)
      using Cons.prems
      apply auto
      done
  next
    assume *: "list_all (encompasses p) ((fst x, snd y) # z # w # ws)"
    from Cons.prems
    have enc: "ws \<noteq> [] \<Longrightarrow> encompasses p (last ws)"
      by (auto simp: list_all_iff)
    from * have "p \<in> convex hull set (map fst ((fst x, snd y)#z#w#ws))"
      apply (rule Cons.hyps)
      apply (rule convex_polygon_skip)
      apply (metis Cons.prems(2))
      using Cons.prems
      apply (cases ws)
      defer
      apply (auto elim!: ccw'.sortedP_Cons intro!: ccw'.sortedP.Cons ccw'.sortedP.Nil split: split_if_asm)[1]
      using Cons.prems
      apply (cases ws)
      defer
      apply (auto elim!: ccw'.sortedP_Cons intro!: ccw'.sortedP.Cons ccw'.sortedP.Nil split: split_if_asm)
      done
    have "set (map fst ((fst x, snd y)#z#w#ws)) \<subseteq> set (map fst (x # y # z # w # ws))"
      by auto
    show "p \<in> convex hull set (map fst (x # y # z # w # ws))"
      apply (rule set_mp)
      apply (rule hull_mono)
      apply fact
      apply fact
      done
  qed
qed

lemma ccw'_sortedP_mirror:
  "ccw'.sortedP x0 (map (mirror_point p0) xs) \<longleftrightarrow> ccw'.sortedP (mirror_point p0 x0) xs"
  apply (induct xs)
  apply (auto simp: ccw'_def[symmetric] intro!: ccw'.sortedP.Nil ccw'.sortedP.Cons elim!: ccw'.sortedP_Cons)
  apply (metis ccw'_mirror_point3 mirror_point_self_inverse)
  by (metis ccw'_mirror_point3 mirror_point_self_inverse)

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

lemma map_fst_half_segments_aux_eq: "[] \<noteq> half_segments_of_aform X \<Longrightarrow>
    map fst (half_segments_of_aform X) =
      fst (hd (half_segments_of_aform X))#butlast (map snd (half_segments_of_aform X))"
  apply (rule nth_equalityI)
  apply simp
  apply (auto simp: nth_Cons hd_conv_nth nth_butlast split: nat.split)
  by (metis subsequent_half_segments)

lemma map_snd_half_segments_aux_eq: "half_segments_of_aform X \<noteq> [] \<Longrightarrow>
    map snd (half_segments_of_aform X) =
      tl (map fst (half_segments_of_aform X)) @ [snd (last (half_segments_of_aform X))]"
  apply (rule nth_equalityI)
  apply simp
  apply (auto simp: nth_Cons hd_conv_nth nth_append nth_tl subsequent_half_segments split: nat.split)
  apply (simp add: not_less last_conv_nth algebra_simps)
  using le_less_Suc_eq by fastforce

lemma ccw'_sortedP_butlast[intro, simp]: "ccw'.sortedP x xs \<Longrightarrow> ccw'.sortedP x (butlast xs)"
  by (induct xs) (auto simp: intro!: ccw'.sortedP.Nil ccw'.sortedP.Cons elim!: ccw'.sortedP_Cons
    dest!: in_set_butlastD)

lemma ccw'_sortedP_right_of_append1:
  assumes "ccw'.sortedP x (zs@[z])"
  assumes "y \<in> set zs"
  shows "ccw' x y z"
  using assms
  by (induct zs arbitrary: x y z) (auto elim!: ccw'.sortedP_Cons)

lemma ccw'_sortedP_right_of_appendD:
  assumes "ccw'.sortedP x (zs@[z])"
  shows "\<forall>y \<in> set zs. ccw' z x y"
  using ccw'_sortedP_right_of_append1[OF assms]
  by (auto simp: det3_def' algebra_simps ccw'_def)

lemma ccw'_sortedP_right_of_last:
  assumes "ccw'.sortedP x zs"
  assumes "y \<in> set zs" "y \<noteq> last zs"
  shows "ccw' x y (last zs)"
  using assms
  apply (intro ccw'_sortedP_right_of_append1[of x "butlast zs" "last zs" y])
  apply (metis append_is_Nil_conv list.distinct(1) snoc_eq_iff_butlast split_list)
  by (metis List.insert_def append_butlast_last_id insert_Nil list.distinct(1) rotate1.simps(2)
    set_ConsD set_rotate1)

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

lemma ccw'_pos_cyclic: "ccw' p q r \<Longrightarrow> ccw' q r p"
  by (auto simp: det3_def' algebra_simps ccw'_def)

lemma ccw'_sortedP_append:
  "ccw'.sortedP p (xs@ys) = (ccw'.sortedP p xs & ccw'.sortedP p ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. ccw' p x y))"
  by (induct xs) (auto intro!: ccw'.sortedP.Cons ccw'.sortedP.Nil elim!: ccw'.sortedP_Cons)

lemma
  ccw'_sortedP_convex_rotate_aux:
  assumes "ccw'.sortedP 0 (zs)" "ccw'.sortedP x (map snd (polychain_of x (zs)))"
  shows "ccw'.sortedP (snd (last (polychain_of x (zs)))) (map snd (butlast (polychain_of x (zs))))"
  using assms
proof (induct zs arbitrary: x rule: list.induct)
  case Nil thus ?case
    apply (simp add: ccw'.sortedP.Nil)
    done
next
  case (Cons z zs)
  have *: "ccw'.sortedP (snd (last (polychain_of (x + z) zs))) (map snd (butlast (polychain_of (x + z) zs)))"
    using Cons(2-)
    apply (intro Cons) apply (auto elim!: ccw'.sortedP_Cons)
    apply (metis ccw'_sortedP_polychain_of_snd)
    done
  from Cons show ?case
    apply (auto intro!: ccw'.sortedP.Cons ccw'.sortedP.Nil elim!: ccw'.sortedP_Cons)
    apply (rule ccw'_pos_cyclic)
    apply (rule ccw'_pos_cyclic)
    apply (subst last_map[symmetric, where f= snd])
    apply simp
    apply (rule ccw'_sortedP_right_of_last)
    apply (metis ccw'_sortedP_polychain_of_snd)
    apply (drule in_set_butlastD) apply force
    using *
    apply (cases "polychain_of (x + z) zs" rule: rev_exhaust)
    apply simp
    apply auto[1] defer
    apply (rule *)
    using *
    apply (auto simp: ccw'_sortedP_append ccw'_def[symmetric])
    apply (metis ccw'_contra snd_conv)
    done
qed

lemma
  ccw'_sortedP_polychain_of_snd_arbitraryI:
  assumes "ccw'.sortedP 0 xs"
  assumes "\<And>z. z \<in> set xs \<Longrightarrow> ccw' x y (z + x)"
  shows "ccw'.sortedP x (map snd (polychain_of y xs))"
proof -
  have "ccw'.sortedP x (map snd (polychain_of x ((y - x)#xs)))"
    using assms(1,2)
    by (intro ccw'_sortedP_polychain_of_snd)
      (auto intro!: ccw'.sortedP.Cons simp: ccw'.translate_origin)
  thus ?thesis
    by (auto elim!: ccw'.sortedP_Cons)
qed

lemma pdevs_val_zero[simp]: "pdevs_val (\<lambda>_. 0) x = 0"
  by (auto simp: pdevs_val_setsum)

lemma snd_last: "xs \<noteq> [] \<Longrightarrow> snd (last xs) = last (map snd xs)"
  by (induct xs) auto

lemma distinct_in_set_butlastD:
  assumes "x \<in> set (butlast xs)"
  assumes "distinct xs"
  shows "x \<noteq> last xs"
  using assms
  by (induct xs) auto

lemma distinct_in_set_tlD:
  assumes "x \<in> set (tl xs)"
  assumes "distinct xs"
  shows "x \<noteq> hd xs"
  using assms
  by (induct xs) auto

lemma pair_in_set_map_sndD: "(a, b) \<in> set xs \<Longrightarrow> b \<in> set (map snd xs)"
  by force

lemma polychain_of_rebase_snd: "snd q = 0 \<Longrightarrow> map (snd o snd) (polychain_of p xs) = map (snd o snd) (polychain_of (p + q) xs)"
proof (induct xs arbitrary: p q)
  case (Cons x xs)
  show ?case
    apply (auto simp: Cons)
    apply (subst (3) add.commute)
    apply (subst add.assoc[symmetric])
    apply (subst (2) add.commute)
    apply (rule Cons[simplified o_def])
    apply (simp add: Cons)
    done
qed simp

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)

context linorder_list0
begin

lemma sorted_butlastI: "sortedP xs \<Longrightarrow> sortedP (butlast xs)"
  by (induct xs) (auto simp: elim!: sortedP_Cons intro!: sortedP.Cons dest!: in_set_butlastD)

end

lemma map_mirror_o_snd_polychain_of_eq: "map (mirror_point x0 \<circ> 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 \<noteq> [] \<Longrightarrow>
    (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 mirror_point_snd_last_eq_lowest:
  "half_segments_of_aform X \<noteq> [] \<Longrightarrow>
    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 listsum_nonnegI:
  fixes xs::"'a::ordered_comm_monoid_add list"
  shows "list_all (\<lambda>x. x \<le> 0) xs \<Longrightarrow> listsum xs \<le> 0"
  by (induct xs) (auto simp: intro!: add_nonpos_nonpos)

lemma listsum_negI:
  fixes xs::"'a::ordered_comm_monoid_add list"
  assumes "xs \<noteq> []"
  assumes "list_all (\<lambda>x. x \<le> 0) (butlast xs)"
  assumes "last xs < 0"
  shows "listsum xs < 0"
proof -
  from assms have "xs = butlast xs @ [last xs]"
    by simp
  also have "listsum \<dots> = listsum (butlast xs) + last xs"
    by simp
  also have "\<dots> < 0"
    by (intro add_nonpos_neg assms listsum_nonnegI)
  finally show ?thesis .
qed

lemma center_le_lowest:
  "fst (fst X) \<le> fst (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  by (auto simp: lowest_vertex_def fst_listsum intro!: listsum_nonnegI)
    (auto simp: lex_def list_all_iff list_of_pdevs_def dest!: in_set_butlastD split: split_if_asm)

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

lemma
  lex_fst_zero_imp:
  "fst x = 0 \<Longrightarrow> lex x 0 \<Longrightarrow> lex y 0 \<Longrightarrow> \<not>coll 0 x y \<Longrightarrow> ccw' 0 y x"
  by (auto simp: ccw'_def det3_def' lex_def sign_simps)

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

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

lemma
  lex_polychain_of_center:
  "(c, d) \<in> set (polychain_of x0 xs) \<Longrightarrow> list_all (\<lambda>x. lex x 0) xs \<Longrightarrow> lex 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) \<in> set (polychain_of x0 xs) \<Longrightarrow> list_all (\<lambda>x. lex x 0) xs \<Longrightarrow> lex (snd (last (polychain_of x0 xs))) d"
proof (induction xs arbitrary: x0 c d)
  case (Cons x xs)
  from Cons(2)
  show ?case
    apply auto
    defer
    apply (drule Cons.IH)
    using Cons.prems apply simp
    using Cons.prems apply simp
    apply (rule lex_polychain_of_center)
    apply (subst prod.collapse)
    apply (rule last_in_set) apply simp
    using Cons.prems apply simp
    done
qed (auto simp: lex_translate_origin)

lemma
  lex_half_segments_lowest_vertex:
  assumes "(c, d) \<in> set (half_segments_of_aform X)"
  shows "lex d (lowest_vertex (fst X, nlex_pdevs (snd X)))"
  using assms
  unfolding half_segments_of_aform_def Let_def
  by (rule lex_polychain_of_center) (auto simp: list_all_iff lex_def dest!: in_set_inl_lex)

lemma
  lex_half_segments_last:
  assumes "(c, d) \<in> 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_mirror_point: "lex (mirror_point x0 a) (mirror_point x0 b) \<Longrightarrow> 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) \<Longrightarrow> ccw' a b c"
  by (auto simp: mirror_point_def)

lemma ccw'_polychain_of_sorted_center_last:
  assumes set_butlast: "(c, d) \<in> set (butlast (polychain_of x0 xs))"
  assumes sorted: "ccw'.sortedP 0 xs"
  assumes ne: "xs \<noteq> []"
  shows "ccw' x0 d (snd (last (polychain_of x0 xs)))"
proof -
  from ccw'_sortedP_polychain_of_snd[OF sorted, of x0]
  have "ccw'.sortedP x0 (map snd (polychain_of x0 xs))" .
  also
  from set_butlast obtain ys zs where "butlast (polychain_of x0 xs) = ys@((c, d)#zs)"
    by (auto simp add: in_set_conv_decomp)
  hence "polychain_of x0 xs = ys @ (c, d) # zs @ [last (polychain_of x0 xs)]"
    by (metis append_Cons append_assoc append_butlast_last_id ne polychain_of_eq_empty_iff)
  finally show ?thesis by (auto elim!: ccw'.sortedP_Cons simp: ccw'.sortedP_append_iff)
qed

lemma in_set_butlastI: "xs \<noteq> [] \<Longrightarrow> x \<in> set xs \<Longrightarrow> x \<noteq> last xs \<Longrightarrow> x \<in> set (butlast xs)"
  by (induct xs) auto

lemma
  ccw'_half_segments_lowest_last:
  assumes set_butlast: "(c, d) \<in> set (butlast (half_segments_of_aform X))"
  assumes ne: "inl (snd X) \<noteq> []"
  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
  neq_left_right_of: "ccw' a b c \<Longrightarrow> ccw' a c d \<Longrightarrow> b \<noteq> d"
  by (auto simp: ccw'_def det3_def' algebra_simps)

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

lemma lowest_vertex_eq_center_iff: "lowest_vertex (x0, nlex_pdevs (snd X)) = x0 \<longleftrightarrow> snd X = zero_pdevs"
  apply (auto simp: lowest_vertex_def )
  apply (subst (asm) listsum_nlex_eq_zero_iff)
  apply (auto simp: list_all_iff list_of_pdevs_def split: split_if_asm intro!: pdevs_eqI)
  done

lemma
  not_coll_lemma_omg:
  "l \<noteq> x0 \<Longrightarrow> lex x1 r \<Longrightarrow> lex x1 l \<Longrightarrow> lex r x0 \<Longrightarrow> lex l x0 \<Longrightarrow>
  ccw' x0 l x1 \<Longrightarrow> ccw' x0 x1 r \<Longrightarrow> \<not>coll x0 l r"
proof
  case goal1
  from `coll x0 l r` have 1: "coll 0 (l - x0) (r - x0)" by (simp add: det3_def' algebra_simps)
  from `lex r x0` have 2: "lex (r - x0) 0" by (auto simp add: lex_def)
  from `lex l x0` have 3: "lex (l - x0) 0" by (auto simp add: lex_def)
  from `ccw' x0 l x1` have 4: "ccw' 0 (l - x0) (x1 - x0)" by (simp add: det3_def' ccw'_def algebra_simps)
  from `ccw' x0 x1 r` have 5: "ccw' 0 (x1 - x0) (r - x0)" by (simp add: det3_def' ccw'_def algebra_simps)
  from `lex x1 r` have 6: "lex 0 (r - x0 - (x1 - x0))" by (auto simp: lex_def)
  from `lex x1 l` have 7: "lex 0 (l - x0 - (x1 - x0))" by (auto simp: lex_def)
  def r' \<equiv> "r - x0"
  def l' \<equiv> "l - x0"
  def x0' \<equiv> "x1 - x0"
  from 1 2 3 4 5 6 7
  have rs: "coll 0 l' r'" "Counterclockwise_2D_Arbitrary.lex r' 0"
    "Counterclockwise_2D_Arbitrary.lex l' 0"
    "ccw' 0 l' x0'"
    "ccw' 0 x0' r'"
    "Counterclockwise_2D_Arbitrary.lex 0 (r' - x0')"
    "Counterclockwise_2D_Arbitrary.lex 0 (l' - x0')"
    unfolding r'_def[symmetric] l'_def[symmetric] x0'_def[symmetric]
    by auto
  from goal1 have "l' \<noteq> 0"
    by (auto simp: l'_def)
  from coll_scale[OF `coll 0 l' _` this]
  obtain y where y: "r' = y *\<^sub>R l'" by auto
  from rs
  show False
    unfolding y
    apply (cases "y = 0")
    apply (simp add: ccw'_def)
    apply (cases "y > 0")
    apply (simp add: ccw'_def)
    apply (auto simp: )
  proof -
    case goal2
    from goal2(1,7,8) have "lex 0 l'"
      by (auto simp: lex_def not_less sign_simps)
    with goal2 have "l' = 0"
      by simp
    thus ?case using goal2 by (auto simp: ccw'_def)
  next
    case goal1
    from goal1 have "0 < det3 0 x0' l'"
      by (auto simp: det3_def' algebra_simps)
    with goal1(3) show False by (auto simp: det3_def' algebra_simps)
  qed
qed

lemma distinct_fst_polychain_of:
  assumes "list_all (\<lambda>x. x \<noteq> 0) xs"
  assumes "list_all (\<lambda>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)
  show ?case
    apply (cases "xs = []", simp)
    apply (auto simp: )
    defer
    apply (rule Cons.IH)
    using Cons.prems apply simp
    using Cons.prems apply simp
    apply (auto elim!: in_set_polychain_of_imp_listsum)
    apply (subst (asm) listsum.Cons[symmetric])
    apply (subst (asm) listsum_nlex_eq_zero_iff)
    using Cons.prems(2) apply (auto simp add: list_all_iff dest!: in_set_takeD)[1]
    using Cons.prems(1) set_take_subset[of _ xs]
    apply (auto simp: neq_Nil_conv)
    done
qed

lemma distinct_snd_polychain_of:
  assumes "list_all (\<lambda>x. x \<noteq> 0) xs"
  assumes "list_all (\<lambda>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)
  show ?case
    apply (cases "xs = []", simp)
    apply (auto simp: )
    defer
    apply (rule Cons.IH)
    using Cons.prems apply simp
    using Cons.prems apply simp
    apply (auto elim!: in_set_polychain_of_imp_listsum)
    apply (subst (asm) listsum_nlex_eq_zero_iff)
    using Cons.prems(2) apply (auto simp add: list_all_iff dest!: in_set_takeD)[1]
    using Cons.prems(1) set_take_subset[of _ xs]
    apply (auto simp: neq_Nil_conv)
    done
qed

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"
  apply (auto simp: distinct_map )
  apply (rule subset_inj_on)
  apply (rule inj_mirror_point)
  apply simp
  done

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)

lemma ccw'_sortedP_snd_segments_of_aform:
  "length (inl (snd X)) > 1 \<Longrightarrow> ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X))) (butlast (map snd (segments_of_aform X)))"
  apply (cases "[] = half_segments_of_aform X")
  apply (simp add: segments_of_aform_def Let_def ccw'.sortedP.Nil)
  apply (auto simp: segments_of_aform_def Let_def ccw'_sortedP_append butlast_append
    lowest_vertex_eq_mirror_last snd_last
    ccw'_sortedP_snd_half_segments_of_aform intro!: )
  apply (simp add: mirror_point_snd_last_eq_lowest ccw'_sortedP_snd_half_segments_of_aform)
  defer
  apply (simp add: mirror_point_snd_last_eq_lowest)
  defer
proof -
  case goal1
  hence ne: "inl (snd X) \<noteq> []" by auto
  have "butlast (map (mirror_point (fst X) \<circ> snd) (half_segments_of_aform X)) =
    butlast
     (map (mirror_point (fst X) \<circ> snd) (polychain_of (lowest_vertex (fst X, nlex_pdevs (snd X)))
       (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X))))))"
    by (simp add: half_segments_of_aform_def)
  also have "\<dots> =
     map snd (butlast (polychain_of (mirror_point (fst X) (lowest_vertex (fst X, nlex_pdevs (snd X))))
         (map uminus (map (op *\<^sub>R 2) (linorder_list0.selsort (ccw 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"
      apply (rule ccw'_sortedP_uminus)
      apply (rule ccw'_sortedP_scaled_inl)
      done
    moreover
    have "ccw'.sortedP ?x (map snd (polychain_of ?x ?xs))"
      apply (subst ccw'_sortedP_mirror[symmetric])
      apply (simp add: map_mirror_o_snd_polychain_of_eq)
      apply (simp add: o_def)
      apply (rule ccw'_sortedP_polychain_of_snd)
      apply (rule ccw'_sortedP_scaled_inl)
      done
    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 (mirror_point (fst X) (lowest_vertex (fst X, nlex_pdevs (snd X))))
      (map uminus (map (op *\<^sub>R 2) (ccw.selsort 0 (inl (snd X)))))))) =
      mirror_point (fst X) (last (map snd (half_segments_of_aform X)))"
    apply (simp add: half_segments_of_aform_def)
    apply (subst last_map[symmetric, where f="mirror_point (fst X)"])
    apply (simp add: ne)
    apply (simp add: map_mirror_o_snd_polychain_of_eq)
    apply (subst last_map)
    apply (simp add: ne)
    apply simp
    done
  finally show ?case .
next
  case (goal2 a b c d e f)
  from goal2 have neq_Nil: "inl (snd X) \<noteq> []" "half_segments_of_aform X \<noteq> []"
    by auto

  from goal2(4) obtain foo where mirror_ef:
    "(foo, mirror_point (fst X) (e, f)) \<in> 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 = "mirror_point (fst X) ?l"

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

  def r \<equiv> "?l + (0, abs (d - snd ?l) + abs (f - snd ?l) + abs (snd ?ml - snd ?l) + 1)"

  have d1: "(c, d) \<noteq> r" "(e, f) \<noteq> r" "?l \<noteq> r" "?ml \<noteq> r"
    by (auto simp: r_def plus_prod_def prod_eq_iff)
  have "distinct (map (mirror_point (fst X) \<circ> 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 `(e, f) \<in> _` this]
  have "?l \<noteq> (e, f)"
    by (simp add: neq_Nil lowest_vertex_eq_mirror_last last_map)
  moreover have "?l \<noteq> ?ml"
    apply (simp add: eq_self_mirror_iff lowest_vertex_eq_center_iff)
    using neq_Nil apply (auto simp add: inl_def)
    done
  ultimately
  have d2: "?l \<noteq> (e, f)" "?l \<noteq> ?ml"
    by auto

  have *: "ccw' ?l (mirror_point (fst X) (e, f)) ?ml"
    unfolding mirror_eq_last
    apply (rule ccw'_half_segments_lowest_last)
    apply (rule mirror_ef)
    apply (rule neq_Nil)
    done
  have "ccw' ?ml (e, f) ?l"
    by (rule ccw'_mirror_point[of "fst X"]) (simp add: *)
  hence lmef: "ccw' ?l ?ml (e, f)"
    by (simp add: ccw'_def det3_def' algebra_simps)

  {
    assume "(c, d) \<noteq> ?ml"
    hence cd_butlast: "((a, b), c, d) \<in> set (butlast (half_segments_of_aform X))"
      unfolding mirror_eq_last
      using goal2(3)
      by (auto intro!: in_set_butlastI simp: prod_eq_iff)
    have "ccw' ?l (c, d) ?ml"
      unfolding mirror_eq_last
      apply (rule ccw'_half_segments_lowest_last)
      apply (rule cd_butlast)
      apply (rule neq_Nil)
      done
  } note lcdml = this
  {
    assume "(c, d) = ?ml"
    hence ?case
      by (simp add: lmef)
  } moreover {
    assume "(c, d) \<noteq> ?ml" "(e, f) = ?ml"
    hence ?case
      by (simp add: lcdml)
  } moreover {
    assume d3: "(c, d) \<noteq> ?ml" "(e, f) \<noteq> ?ml"

    from `(_, (c, d)) \<in> set _`
    have "(c, d) \<in> set (map snd (half_segments_of_aform X))" by force
    hence "(c, d) \<in> 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 \<noteq> (c, d)"
      by (simp add: fst_hd_half_segments_of_aform neq_Nil hd_map)

    note _ _
    moreover
    have "lex (c, d) ?l"
      by (rule lex_half_segments_lowest_vertex) fact
    hence "ccw ?l r (c, d)"
      unfolding r_def by (rule lex_ccw_left) simp
    moreover
    have "lex ?ml ?l"
      apply (rule lex_half_segments_lowest_vertex)
      unfolding mirror_eq_last
      using last_in_set[OF goal2(2)[symmetric]]
      apply (subst prod.collapse)
      apply assumption
      done
    hence "ccw ?l r ?ml"
      unfolding r_def by (rule lex_ccw_left) simp
    moreover
    have "lex (e, f) ?l"
      apply (rule lex_mirror_point[of "fst X"])
      unfolding mirror_eq_last
      apply (rule lex_half_segments_last)
      using mirror_ef
      apply (rule in_set_butlastD)
      done
    hence "ccw ?l r (e, f)"
      unfolding r_def by (rule lex_ccw_left) simp
    moreover
    from `(c, d) \<noteq> ?ml` have "ccw ?l (c, d) ?ml"
      by (simp add: ccw_def lcdml)
    moreover
    have d4: "(c, d) \<noteq> (e, f)"
      apply (rule neq_left_right_of lcdml)
      apply (rule lcdml)
      apply fact apply fact
      done
    from lmef have "ccw ?l ?ml (e, f)"
      by (simp add: ccw_def)
    ultimately
    have ccw: "ccw ?l (c, d) (e, f)"
      apply (rule ccw.transitive[where S=UNIV])
      using d1 d2 `?l \<noteq> (c, d)` d3 d4
      apply simp_all
      done
    have ncoll: "\<not> coll ?l (c, d) (e, f)"
      apply (rule not_coll_lemma_omg)
      using d2 `?l \<noteq> (c, d)` apply simp
      defer defer
      apply fact
      apply fact
      apply (rule lcdml)
      apply fact
      apply (rule lmef)
      defer
      apply (subst mirror_eq_last)
      apply (rule lex_half_segments_last)
      apply fact
      apply (rule lex_mirror_point[of "fst X"])
      apply simp
      apply (rule lex_half_segments_lowest_vertex)
      using mirror_ef
      apply (rule in_set_butlastD)
      done
    with ccw have ?case
      by (simp add: ccw_def)
  } ultimately show ?case by blast
qed

lemma polychain_of_segments_of_aform:
  assumes "2 < length (segments_of_aform X)"
  assumes "list_all (encompasses p) (segments_of_aform X)"
  shows "p \<in> convex hull set (map fst (segments_of_aform X))"
proof -
  from assms have len_half: "length (half_segments_of_aform X) > 1"
    by (auto simp: numeral_2_eq_2 segments_of_aform_def Let_def)
  then obtain x y ys where 2: "half_segments_of_aform X = x # y # ys"
    apply (cases "half_segments_of_aform X")
    defer
    apply (rename_tac x xs)
    apply (case_tac xs)
    apply auto
    done
  hence "3 < length (segments_of_aform X)"
    by (auto simp: segments_of_aform_def)
  then obtain w z zs where 4: "segments_of_aform X = x#y#w#z#zs"
    apply (cases "segments_of_aform X")
    defer
    apply (rename_tac x xs)
    apply (case_tac xs)
    defer
    apply (rename_tac x xs)
    apply (case_tac xs)
    defer
    apply (rename_tac x xs)
    apply (case_tac xs)
    apply (auto simp: segments_of_aform_def Let_def 2)
    done
  from assms have "1 < length (inl (snd X))"
    by (auto simp: half_segments_of_aform_def Let_def segments_of_aform_def split: split_if_asm)
  from ccw'_sortedP_snd_segments_of_aform[OF this] have sorted: "ccw'.sortedP (fst x) (map snd (butlast (x # y # w # z # zs)))"
    apply (auto simp: 4 )
    apply (subst (asm) fst_hd_half_segments_of_aform[symmetric])
    apply (auto simp add: 2 split: split_if_asm)
    by (metis (erased, lifting) "2" fst_hd_half_segments_of_aform list.distinct(1) list.sel(1) map_butlast)
  from
     encompasses_convex_polygon3[OF assms(2)[unfolded 4] convex_polygon_segments_of_aform[OF len_half, simplified 4] sorted]
  show ?thesis by (simp add: 4)
qed

lemma
  between_prodI:
  assumes "coll x y p"
  assumes "x \<le> p" "p \<le> y"
  shows "between (x, y) p"
proof cases
  assume ne: "y - x \<noteq> 0"
  from assms have "coll 0 (y - x) (p - x)"
    by (simp add: det3_def' algebra_simps)
  from coll_scale[OF this ne] obtain r where r: "p - x = r *\<^sub>R (y - x)" ..
  with ne have r_eq: "r = fst (p - x)/fst(y - x) \<or> r = snd (p - x)/snd(y - x)"
    by (auto simp: field_simps less_eq_prod_def prod_eq_iff)
  hence "0 \<le> r" "r \<le> 1"
    using assms(2,3) ne
    by (auto simp: field_simps less_eq_prod_def prod_eq_iff divide_le_eq_1)
  thus ?thesis using r
    by (auto simp: between_def closed_segment_def algebra_simps)
qed (insert assms, simp add: between dist_commute)

lemma polychain_of_segments_of_aform2:
  assumes "segments_of_aform X = [x, y]"
  assumes "between (fst x, snd x) p"
  shows "p \<in> 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 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: split_if_asm)

value "segments_of_aform (aform_of_ivl (1, 2) (3, 4))"

subsection {* Intersection *}

fun intersect_segment_xline'::"nat \<Rightarrow> point * point \<Rightarrow> real \<Rightarrow> point option"
  where "intersect_segment_xline' p ((x0, y0), (x1, y1)) xl =
    (if x0 \<le> xl \<and> xl \<le> 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 intersect_segment_xline':
  assumes "intersect_segment_xline' prec (p0, p1) x = Some (m, M)"
  shows "closed_segment p0 p1 \<inter> {p. fst p = x} \<subseteq> {(x, m) .. (x, M)}"
  using assms
  apply (cases p0)
  apply (rename_tac x0 y0)
  apply (cases p1)
  apply (rename_tac x1 y1)
  apply (auto simp: abs_le_iff split: split_if_asm)
  apply (auto simp add: min_def max_def split: split_if_asm simp add: algebra_simps not_le dest: segment_bound)[2]
  apply (auto 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]])
proof -
  case goal1
  then obtain u where u: "x = x0 *\<^sub>R (1 - u) + u * x1" "b = y0 *\<^sub>R (1 - u) + u * y1" "0 \<le> u" "u \<le> 1"
    by (auto simp: closed_segment_def algebra_simps)
  have "(y1 - y0) * (x - x0) / (x1 - x0) + y0 = b"
    using goal1 by (auto simp: closed_segment_def field_simps u)
  thus "(y1 - y0) * (x - x0) / (x1 - x0) + y0 \<le> b" "(y1 - y0) * (x - x0) / (x1 - x0) + y0 \<ge> b"
    by simp_all
qed

lemma intersect_segment_xline'_eq_None:
  assumes "intersect_segment_xline' prec (p0, p1) x = None"
  assumes "fst p0 \<le> fst p1"
  shows "closed_segment p0 p1 \<inter> {p. fst p = x} = {}"
  using assms
  apply (cases p0)
  apply (rename_tac x0 y0)
  apply (cases p1)
  apply (rename_tac x1 y1)
  apply (auto simp: abs_le_iff split: split_if_asm)
  apply (auto simp add: min_def max_def split: split_if_asm simp add: algebra_simps not_le closed_segment_def)[1]
  apply (metis add_le_imp_le_right add_less_cancel_left mult.commute not_less real_scaleR_def scaleR_le_cancel_left)
  apply (auto simp add: min_def max_def split: split_if_asm simp add: not_le closed_segment_def)
proof -
  case goal1
  hence "(1 - u) * x1 \<ge> (1 - u) * x0"
    apply (intro mult_left_mono)
    by auto
  thus ?case using goal1 by (auto simp: algebra_simps)
qed

fun intersect_segment_xline
  where "intersect_segment_xline prec ((a, b), (c, d)) x =
  (if a \<le> 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"
  apply (auto simp: closed_segment_def)
  apply (rule_tac x= "1 - u" in exI)
  apply simp
  apply (rule_tac x= "1 - u" in exI)
  apply simp
  done

lemma intersect_segment_xline:
  assumes "intersect_segment_xline prec (p0, p1) x = Some (m, M)"
  shows "closed_segment p0 p1 \<inter> {p. fst p = x} \<subseteq> {(x, m) .. (x, M)}"
  apply (cases p0)
  apply (rename_tac x0 y0)
  apply (cases p1)
  apply (rename_tac x1 y1)
  using assms
  by (auto simp: closed_segment_commute split: split_if_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) \<inter> {p. fst p = x} \<subseteq> {(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 \<inter> {p. fst p = x} = {}"
  apply (cases p0)
  apply (rename_tac x0 y0)
  apply (cases p1)
  apply (rename_tac x1 y1)
  using assms
  by (auto simp: closed_segment_commute split: split_if_asm simp del: intersect_segment_xline'.simps
    dest!: intersect_segment_xline'_eq_None)

lemma intersect_segment_xline_eq_empty:
  assumes "closed_segment p0 p1 \<inter> {p. fst p = x} = {}"
  shows "intersect_segment_xline prec (p0, p1) x = None"
  apply (cases p0)
  apply (rename_tac x0 y0)
  apply (cases p1)
  apply (rename_tac x1 y1)
  using assms
  apply (auto simp: closed_segment_commute closed_segment_def algebra_simps
    split: split_if_asm
    dest!: intersect_segment_xline'_eq_None)
proof -
  case goal1
  let "?t u" = "(x, y0 + y1 * u - y0 * u)"
  let ?s = "{?t u |u. 0 \<le> u \<and> u \<le> 1}"
  let ?h = "{p. fst p = x}"
  have "?t 0 \<in> ?s" "?t 0 \<in> ?h"
    by auto
  thus ?case using goal1 by blast
next
  case goal2
  let "?t u" = "(x0 + x1 * u - x0 * u, y0 + y1 * u - y0 * u)"
  let ?u = "(x - x0) / (x1 - x0)"
  let ?h = "{p. fst p = x}"
  from goal2 have "0 \<le> ?u \<and> ?u \<le> 1"
    by (auto simp add: field_simps)
  hence "?t ?u \<in> {?t u |u. 0 \<le> u \<and> u \<le> 1}"
    using goal2 by blast
  moreover
  have "?t ?u \<in> ?h"
    using `x0 \<noteq> _`
  proof (auto)
    have "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) =
      x0 + (x1 * (x - x0) - x0 * (x - x0)) / (x1 - x0)"
      by (subst diff_divide_distrib) simp
    also have "\<dots> = x"
      using `x0 \<noteq> _` by (simp add: field_simps)
    finally show "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) = x" .
  qed
  ultimately show False using goal2 by blast
next
  case goal3
  hence "x0 \<noteq> x1" by auto
  let "?t u" = "(x0 + x1 * u - x0 * u, y0 + y1 * u - y0 * u)"
  let ?u = "(x - x0) / (x1 - x0)"
  let ?h = "{p. fst p = x}"
  from goal3 have "0 \<le> ?u \<and> ?u \<le> 1"
    by (auto simp add: field_simps)
  hence "?t ?u \<in> {?t u |u. 0 \<le> u \<and> u \<le> 1}"
    using goal3 by blast
  moreover
  have "?t ?u \<in> ?h"
    using `x0 \<noteq> _`
  proof (auto)
    have "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) =
      x0 + (x1 * (x - x0) - x0 * (x - x0)) / (x1 - x0)"
      by (subst diff_divide_distrib) simp
    also have "\<dots> = x"
      using `x0 \<noteq> _` by (simp add: field_simps)
    finally show "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) = x" .
  qed
  ultimately show False using goal3 by blast
next
  case goal4
  hence "x0 \<noteq> x1" by auto
  let "?t u" = "(x0 + x1 * u - x0 * u, y0 + y1 * u - y0 * u)"
  let ?u = "(x - x0) / (x1 - x0)"
  let ?h = "{p. fst p = x}"
  from goal4 have "0 \<le> ?u \<and> ?u \<le> 1"
    by (auto simp add: field_simps)
  hence "?t ?u \<in> {?t u |u. 0 \<le> u \<and> u \<le> 1}"
    using goal4 by blast
  moreover
  have "?t ?u \<in> ?h"
    using `x0 \<noteq> _`
  proof (auto)
    have "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) =
      x0 + (x1 * (x - x0) - x0 * (x - x0)) / (x1 - x0)"
      by (subst diff_divide_distrib) simp
    also have "\<dots> = x"
      using `x0 \<noteq> _` by (simp add: field_simps)
    finally show "x0 + x1 * (x - x0) / (x1 - x0) - x0 * (x - x0) / (x1 - x0) = x" .
  qed
  ultimately show False using goal4 by blast
qed

value "intersect_segment_xline 20 ((10, 1),(4, 0)) (7)"

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 \<Rightarrow> intersect_segment_xline prec X xl
    | Some (m, M) \<Rightarrow>
      (case intersect_segment_xline prec X xl of
        None \<Rightarrow> Some (m, M)
      | Some (m', M') \<Rightarrow> Some (min m' m, max M' M)))"

lemma
  bound_intersect_2d_eq_None:
  assumes "bound_intersect_2d prec Xs x = None"
  assumes "X \<in> 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 \<in> set Xs" "intersect_segment_xline prec X x = Some (m', M)"
    "\<And>X m' M' . X \<in> set Xs \<Longrightarrow> intersect_segment_xline prec X x = Some (m', M') \<Longrightarrow> M' \<le> M"
proof atomize_elim
  show "\<exists>X m'. X \<in> set Xs \<and> intersect_segment_xline prec X x = Some (m', M) \<and>
    (\<forall>X m' M'. X \<in> set Xs \<longrightarrow> intersect_segment_xline prec X x = Some (m', M') \<longrightarrow> M' \<le> 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' \<in> set Xs" and m'': "intersect_segment_xline prec X' x = Some (m'', M')"
        and max: "\<And>X m' M'a. X \<in> set Xs \<Longrightarrow> intersect_segment_xline prec X x = Some (m', M'a) \<Longrightarrow> M'a \<le> 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'' max
          apply (cases mM''')
          apply (intro exI[where x= "if M' \<ge> snd mM''' then X' else X"] exI[where x= "if M' \<ge> snd mM''' then m'' else fst mM'''"])
          apply (auto simp: max_def min_def simp del: intersect_segment_xline.simps split: option.split_asm split_if_asm)
          apply (metis max linear order_trans)
          apply (metis max linear order_trans)
          done
      qed
    qed
  qed
qed

lemma bound_intersect_2d_lower:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  obtains X M' where "X \<in> set Xs" "intersect_segment_xline prec X x = Some (m, M')"
    "\<And>X m' M' . X \<in> set Xs \<Longrightarrow> intersect_segment_xline prec X x = Some (m', M') \<Longrightarrow> m \<le> m'"
proof atomize_elim
  show "\<exists>X M'. X \<in> set Xs \<and> intersect_segment_xline prec X x = Some (m, M') \<and>
    (\<forall>X m' M'. X \<in> set Xs \<longrightarrow> intersect_segment_xline prec X x = Some (m', M') \<longrightarrow> m \<le> 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' \<in> set Xs" and M'': "intersect_segment_xline prec X' x = Some (m', M'')"
        and min: "\<And>X m'a M'. X \<in> set Xs \<Longrightarrow> intersect_segment_xline prec X x = Some (m'a, M') \<Longrightarrow> m' \<le> 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
          apply (cases mM''')
          apply (intro exI[where x= "if m' \<le> fst mM''' then X' else X"] exI[where x= "if m' \<le> fst mM''' then M'' else snd mM'''"])
          apply (auto simp: max_def min_def simp del: intersect_segment_xline.simps split: option.split_asm split_if_asm)
          apply (metis min order_trans)
          apply (metis min order_trans)
          done
      qed
    qed
  qed
qed

lemma bound_intersect_2d:
  assumes "bound_intersect_2d prec Xs x = Some (m, M)"
  shows "(\<Union>(p1, p2) \<in> set Xs. closed_segment p1 p2) \<inter> {p. fst p = x} \<subseteq> {(x, m) .. (x, M)}"
proof -
  from bound_intersect_2d_upper[OF assms] guess X1 m1 . note upper = this
  from bound_intersect_2d_lower[OF assms] guess X2 M2 . note lower = this
  show ?thesis
    using upper(1,2) lower(1,2)
    apply (auto)
    apply (case_tac "intersect_segment_xline prec ((aa, ba), ab, bb) x")
    apply (force dest!: intersect_segment_xline_eq_None)
    apply (case_tac a)
    apply (simp only: )
    apply (rule order_trans)
    apply (rule lower)
    apply assumption back back
    apply assumption
    apply (drule intersect_segment_xline)
    apply force
    apply (case_tac "intersect_segment_xline prec ((aa, ba), ab, bb) x")
    apply (force dest!: intersect_segment_xline_eq_None)
    apply (case_tac a)
    apply (simp only: )
    apply (rule order_trans)
    defer
    apply (rule upper)
    apply assumption back back
    apply assumption
    defer defer
    apply (drule intersect_segment_xline)
    apply force
    done
qed

lemma
  singleton_contrE:
  assumes "\<And>x y. x \<noteq> y \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> False"
  assumes "X \<noteq> {}"
  obtains x where "X = {x}"
  using assms by blast

lemma ccw'_fst0: "det3 a b c = det3 0 (b - a) (c - a)"
  by (auto simp: det3_def' algebra_simps)

lemma ccw'_scaleR1_eq:
  "0 < e \<Longrightarrow> det3 0 (e*\<^sub>Rxr) P = 0 \<longleftrightarrow> det3 0 xr P = 0"
  by (auto simp add:  det3_def' algebra_simps)

lemma ccw'_coll_scaleR1:
  "0 < e \<Longrightarrow> det3 0 xr P \<ge> 0 \<Longrightarrow> det3 0 (e*\<^sub>Rxr) P \<ge> 0"
  by (auto simp add: det3_def' algebra_simps)

lemma ccw'_coll_scaleR1_eq:
  "0 < e \<Longrightarrow> det3 0 (e*\<^sub>Rxr) P \<ge> 0 \<longleftrightarrow> det3 0 xr P \<ge> 0"
  by (auto simp add: ccw_def det3_def' algebra_simps)

lemma ccw_coll_scaleR_segment:
  assumes "det3 x y z \<ge> 0"
  assumes "a > 0"
  shows "det3 x ((1 - a) *\<^sub>R x + a *\<^sub>R y) z \<ge> 0"
  using assms
  apply (subst ccw'_fst0)
  apply (subst (asm) ccw'_fst0)
  apply (simp add: algebra_simps)
  apply (subst scaleR_diff_right[symmetric])
  apply (rule ccw'_coll_scaleR1)
  apply assumption apply assumption
  done

lemma ccw_coll_scaleR_segment1:
  assumes "det3 x y z \<ge> 0"
  assumes "0 \<le> a" "a < 1"
  shows "det3 ((1 - a) *\<^sub>R x + a *\<^sub>R y) y z \<ge> 0"
  using assms
  apply (subst ccw'_fst0)
  apply (subst (asm) ccw'_fst0)
  apply (simp add: algebra_simps)
proof -
  case goal1
  have "det3 0 ((1 - a) *\<^sub>R (y - x)) (z - x + (- a) *\<^sub>R (y - x)) \<ge> 0"
    apply (subst ccw'_coll_scaleR1_eq)
    using assms
    apply (auto simp add: det3_def' algebra_simps)
    done
  thus ?case
    by (auto simp: algebra_simps)
qed

text {* convexity of zonotopes *}
lemma segment_in_aform_val:
  assumes "p \<in> closed_segment (aform_val e X) (aform_val f X)"
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes "f \<in> UNIV \<rightarrow> {-1 .. 1}"
  obtains g where "g \<in> UNIV \<rightarrow> {-1 .. 1}" "p = aform_val g X"
proof -
  from assms obtain u where u: "0 \<le> u" "u \<le> 1"
      "p = aform_val (\<lambda>i. (1 - u) * e i + u * f i) X"
    by (auto simp: closed_segment_def algebra_simps aform_val_def pdevs_val_cmul[symmetric]
      pdevs_val_add[symmetric])
  from u(1,2) assms(2,3) have "(\<lambda>i. (1 - u) * e i + u * f i) \<in> UNIV \<rightarrow> {-1 .. 1}"
    apply (auto simp: Pi_iff)
    apply (drule_tac x = i in spec)
    apply (drule_tac x = i in spec)
    apply (auto simp: Pi_iff)
  proof -
    case goal2
    have "(1 - u) * e i + u * f i \<le> 1"
      apply (rule convex_bound_le)
      using goal2 by auto
    thus ?case using goal2
      by (simp add: algebra_simps)
  next
    case goal1
    have "u * - f i + (1 - u) * - e i \<le> 1"
      apply (rule convex_bound_le)
      using goal1 by (auto )
    thus ?case using goal1
      by (simp add: algebra_simps)
  qed
  then show ?thesis using u(3) ..
qed

lemma append_eq_2: "length xs = length ys \<Longrightarrow> xs @ ys = [x, y] \<longleftrightarrow> xs = [x] \<and> ys = [y]"
  apply (cases xs, simp)
  apply (rename_tac z zs)
  apply (case_tac zs)
  apply (auto )
  done

lemma zero_in_range_pdevs_apply[intro, simp]:
  fixes X::"'a::real_vector pdevs" shows "0 \<in> range (pdevs_apply X)"
  by (metis degree_gt less_irrefl rangeI)

lemma dense_list_in_range: "x \<in> set (dense_list_of_pdevs X) \<Longrightarrow> x \<in> range (pdevs_apply X)"
  by (auto simp: dense_list_of_pdevs_def)

lemma not_in_dense_list_zeroD: "pdevs_apply X i \<notin> set (dense_list_of_pdevs X) \<Longrightarrow> pdevs_apply X i = 0"
  apply (auto simp: dense_list_of_pdevs_def)
proof (rule ccontr)
  case goal1
  assume "pdevs_apply X i \<noteq> 0"
  hence "i < degree X"
    by (rule degree_gt)
  thus False using goal1
    by force
qed

lemma add_scaleR_halves:
  fixes y::"'a::real_vector" shows "scaleR (x / 2) y + scaleR (x / 2) y = scaleR x y"
  by (metis real_sum_of_halves scaleR_left.add)

lemma polychain_of_singleton_iff: "polychain_of p xs = [a] \<longleftrightarrow> fst a = p \<and> xs = [(snd a - p)]"
  by (induct xs) auto

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

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

lemma
  bound_intersect_2d_ud_segments_of_aform_le:
  assumes "bound_intersect_2d_ud prec X xl = Some (m0, M0)"
  shows "m0 \<le> M0"
  using assms
  unfolding bound_intersect_2d_ud_def
  apply (cases "segments_of_aform X")
  apply (simp add: Let_def split: split_if_asm)
  apply (rename_tac y ys)
  apply (case_tac ys)
  apply (simp split: option.split_asm prod.split_asm split_if_asm add: min_def max_def)
  apply (rename_tac z zs)
  apply (case_tac zs)
  apply (simp split: option.split_asm prod.split_asm split_if_asm add: min_def max_def intersect_segment_xline_le)
  apply (auto split: option.split_asm)
  by (smt bound_intersect_2d_lower bound_intersect_2d_upper intersect_segment_xline_le)

lemma ccw_contr_on_line_left:
  assumes "det3 (a, b) (x, c) (x, d) \<ge> 0" "a > x"
  shows "d \<le> c"
  using assms
  apply (auto simp: det3_def' algebra_simps)
  apply (cases "x = a")
  apply (simp )
proof -
  case goal1
  hence "d * (a - x) \<le> c * (a - x)"
    by (auto simp: algebra_simps)
  thus "c \<ge> d"
    using goal1 by auto
qed

lemma ccw_contr_on_line_right:
  assumes "det3 (a, b) (x, c) (x, d) \<ge> 0" "a < x"
  shows "d \<ge> c"
  using assms
  apply (auto simp: det3_def')
  apply (cases "x = a")
  apply (auto simp: algebra_simps)
proof -
  case goal1
  hence "c * (x - a) \<le> d * (x - a)"
    by (auto simp: algebra_simps)
  thus "c \<le> d" using goal1 by auto
qed

lemma selsort_ccw_singleton_iff: "ccw.selsort c xs = [x] \<longleftrightarrow> xs = [x]"
  by (induct xs) (auto simp: Let_def)

lemma listsum_nlex_eq_listsum_inl:
  "listsum (map snd (list_of_pdevs (nlex_pdevs X))) = listsum (inl X)"
  by (auto simp: inl_def listsum_list_of_pdevs listsum_independent_pdevs)

lemma segments_of_aform_line_segment:
  assumes "segments_of_aform X = [x, y]"
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  shows "aform_val e X \<in> closed_segment (fst x) (snd x)"
proof -
  from pdevs_val_pdevs_of_list_inl2E[OF `e \<in> _`, of "snd X"]
  obtain e' where e': "pdevs_val e (snd X) = pdevs_val e' (pdevs_of_list (inl (snd X)))"
    "e' \<in> UNIV \<rightarrow> {- 1..1}" .
  from e' have "0 \<le> 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 selsort_ccw_singleton_iff lowest_vertex_def
        aform_val_def listsum_nlex_eq_listsum_inl closed_segment_def Pi_iff
      intro!: exI[where x="(1 + e' 0) / 2"])
      (auto simp: algebra_simps)
qed

lemma independent_pdevs_eq_Nil_iff:
  "list_all (\<lambda>x. lex x 0) xs \<Longrightarrow> list_all (\<lambda>x. x \<noteq> 0) xs \<Longrightarrow> independent_pdevs xs = [] \<longleftrightarrow> xs = []"
  apply (auto )
  apply (induct xs)
  apply (auto simp: Let_def split: split_if_asm)
  apply (subst (asm) listsum.Cons[symmetric])
  apply (subst (asm) listsum_nlex_eq_zero_iff)
  apply (auto simp: list_all_iff)
  done

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

lemma
  bound_intersect_2d_ud_segments_of_aform:
  assumes "bound_intersect_2d_ud prec X xl = Some (m0, M0)"
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  shows "{aform_val e X} \<inter> {x. fst x = xl} \<subseteq> {(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)\<leftarrow>segments_of_aform X . x1 < x2] xl = Some (m, M')"
      and ub: "bound_intersect_2d prec [((x1, y1), x2, y2)\<leftarrow>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] guess X1 m1 . note upper = this
    from bound_intersect_2d_lower[OF lb] guess X2 M2 . note lower = this
    from upper(1) lower(1)
    have X1: "X1 \<in> set (segments_of_aform X)" "fst (fst X1) > fst (snd X1)"
      and X2: "X2 \<in> 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) \<noteq> 1"
      by (auto simp: segments_of_aform_def Let_def)
    from X1 have ne1: "fst (fst X1) \<noteq> fst (snd X1)"
      by simp
    obtain p1 where p1: "closed_segment (fst X1) (snd X1) \<inter> {p. fst p = xl} = {p1}"
      apply (rule singleton_contrE)
      defer
      defer
      apply assumption
    proof -
      case goal1
      from goal1(2-) ne1
      show ?case
        apply (cases X1)
        apply (case_tac a)
        apply (auto )
        apply (auto simp: closed_segment_def field_simps)
      proof -
        case goal1
        hence "u = ua * (aa - ba) / (aa - ba)"
          by (auto simp: closed_segment_def field_simps)
        hence "u = ua"
          by (simp add: goal1)
        thus ?case using goal1 by simp
      qed
    next
      case goal2
      thus ?case
        using upper(2)
        by (auto dest!: intersect_segment_xline_eq_empty[where prec=prec])
    qed
    then obtain u where u: "p1 = (1 - u) *\<^sub>R fst X1 + u *\<^sub>R (snd X1)" "0 \<le> u" "u \<le> 1"
      by (auto simp: closed_segment_def algebra_simps)
    have coll1: "det3 (fst X1) p1 (aform_val e X) \<ge> 0"
      apply (cases "u = 0")
      unfolding u
      apply simp
      apply (rule ccw_coll_scaleR_segment)
      using u ccw_coll_segments_of_aformI[OF `e \<in> _` lh X1(1)]
      apply auto
      done
    have coll1': "det3 p1 (snd X1) (aform_val e X) \<ge> 0"
      apply (cases "u = 1")
      unfolding u
      apply simp
      apply (rule ccw_coll_scaleR_segment1)
      using u ccw_coll_segments_of_aformI[OF `e \<in> _` lh X1(1)]
      apply auto
      done

    from X2 have ne2: "fst (fst X2) \<noteq> fst (snd X2)" by simp
    obtain p2 where p2: "closed_segment (fst X2) (snd X2) \<inter> {p. fst p = xl} = {p2}"
      apply (rule singleton_contrE)
      defer
      defer
      apply assumption
    proof -
      case goal1
      from goal1(2-) ne2
      show ?case
        apply (cases X2)
        apply (case_tac a)
        apply (auto )
        apply (auto simp: closed_segment_def field_simps)
      proof -
        case goal1
        hence "u = ua * (aa - ba) / (aa - ba)"
          by (auto simp: closed_segment_def field_simps)
        hence "u = ua"
          by (simp add: goal1)
        thus ?case using goal1 by simp
      qed
    next
      case goal2
      thus ?case
        using lower
        by (auto dest!: intersect_segment_xline_eq_empty[where prec=prec])
    qed
    then obtain v where v: "p2 = (1 - v) *\<^sub>R fst X2 + v *\<^sub>R (snd X2)" "0 \<le> v" "v \<le> 1"
      by (auto simp: closed_segment_def algebra_simps)
    have coll2: "det3 (fst X2) p2 (aform_val e X) \<ge> 0"
      apply (cases "v = 0")
      unfolding v
      apply simp
      apply (rule ccw_coll_scaleR_segment)
      using v ccw_coll_segments_of_aformI[OF `e \<in> _` lh X2(1)]
      apply auto
      done
    have coll2': "det3 p2 (snd X2) (aform_val e X) \<ge> 0"
      apply (cases "v = 1")
      unfolding v
      apply simp
      apply (rule ccw_coll_scaleR_segment1)
      using v ccw_coll_segments_of_aformI[OF `e \<in> _` lh X2(1)]
      apply auto
      done

    from in_set_segments_of_aform_aform_valE[of "fst X1" "snd X1" X, unfolded pair_collapse, OF X1(1)]
      guess e1s . note e1s = this
    from previous_segments_of_aformE[of "fst X1" "snd X1" X, unfolded pair_collapse, OF X1(1)]
      guess fX0 .
    from in_set_segments_of_aform_aform_valE[OF this] guess e1f . note e1f = this
    have "p1 \<in> closed_segment (aform_val e1f X) (aform_val e1s X)"
      using p1 by (auto simp: e1s e1f)
    from segment_in_aform_val[of p1 e1f X e1s, OF this e1f(2) e1s(2)] guess ep1 . note ep1 = this

    from in_set_segments_of_aform_aform_valE[of "fst X2" "snd X2" X, unfolded pair_collapse, OF X2(1)]
      guess e2s . note e2s = this
    from previous_segments_of_aformE[of "fst X2" "snd X2" X, unfolded pair_collapse, OF X2(1)]
      guess fX02 .
    from in_set_segments_of_aform_aform_valE[OF this] guess e2f . note e2f = this
    have "p2 \<in> closed_segment (aform_val e2f X) (aform_val e2s X)"
      using p2 by (auto simp: e2s e2f)
    from segment_in_aform_val[of p2 e2f X e2s, OF this e2f(2) e2s(2)] guess ep2 . note ep2 = this

    from ccw_coll_segments_of_aformI[OF ep2(1), of X "(fst X1, snd X1)", unfolded pair_collapse, OF lh X1(1), unfolded ep2(2)[symmetric]]
    have c2: "det3 (fst X1) (snd X1) p2 \<ge> 0" .
    hence c12: "det3 (fst X1) p1 p2 \<ge> 0"
      apply (cases "u = 0")
      unfolding u
      apply (simp)
      apply (rule ccw_coll_scaleR_segment)
      using u
      apply auto
      done
    from ccw_coll_segments_of_aformI[OF ep1(1), of X "(fst X2, snd X2)", unfolded pair_collapse, OF lh X2(1), unfolded ep1(2)[symmetric]]
    have c1: "det3 (fst X2) (snd X2) p1 \<ge> 0" .
    hence c21: "det3 (fst X2) p2 p1 \<ge> 0"
      apply (cases "v = 0")
      unfolding v
      apply (simp)
      apply (rule ccw_coll_scaleR_segment)
      using v
      apply auto
      done
    from p1 p2 have p1p2xl: "fst p1 = xl" "fst p2 = xl"
      by (auto simp: det3_def')
    from upper_seg p1 have "snd p1 \<le> M" by (auto simp: less_eq_prod_def)
    from lower_seg p2 have "m \<le> 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)) \<ge> 0"
        and coll': "det3 (fst (snd X1), snd (snd X1)) (fst p1, snd (aform_val e X)) (fst p1, snd p1) \<ge> 0"
        using coll1 coll1'
        by (auto intro: ccw_coll_cyclic)
      have "snd (aform_val e X) \<le> M"
      proof (cases "fst (fst X1) = xl")
        case False
        have "fst (fst X1) \<ge> fst p1"
          unfolding u using X1
          by (auto simp: algebra_simps intro!: mult_left_mono u)
        moreover
        have "fst (fst X1) \<noteq> 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 \<le> M` by simp
      next
        case True
        have "fst (snd X1) * (1 - u) \<le> fst (fst X1) * (1 - u)"
          using X1 u
          by (auto simp: intro!: mult_right_mono)
        hence "fst (snd X1) \<le> fst p1"
          unfolding u by (auto simp: algebra_simps)
        moreover
        have "fst (snd X1) \<noteq> 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 \<le> M` by simp
      qed
    }
    {
      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)) \<ge> 0"
        and coll': "det3 (fst (snd X2), snd (snd X2)) (fst p2, snd (aform_val e X)) (fst p2, snd p2) \<ge> 0"
        using coll2 coll2'
        by (auto intro: ccw_coll_cyclic)
      have "m \<le> snd (aform_val e X)"
      proof (cases "fst (fst X2) = xl")
        case False
        have "fst (fst X2) \<le> fst p2"
          unfolding v using X2
          by (auto simp: algebra_simps intro!: mult_left_mono v)
        moreover
        have "fst (fst X2) \<noteq> 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 \<le> snd p2` by simp
      next
        case True
        have "(1 - v) * fst (snd X2) \<ge> (1 - v) * fst (fst X2)"
          using X2 v
          by (auto simp: intro!: mult_left_mono)
        hence "fst (snd X2) \<ge> fst p2"
          unfolding v by (auto simp: algebra_simps)
        moreover
        have "fst (snd X2) \<noteq> 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 \<le> snd p2` by simp
      qed
    }
    have "aform_val e X \<in> {(xl, m) .. (xl, M)}"
      apply (auto simp: less_eq_prod_def fst_aform_val)
      apply fact+
      done
    hence "aform_val e X \<in> {(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 \<in> 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 \<in> {(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 \<in> {(xl, m0) .. (xl, M0)}" by auto
  } moreover {
    assume len: "length (segments_of_aform X) = 0"
    hence "snd X = zero_pdevs"
      apply (auto simp add: segments_of_aform_def Let_def half_segments_of_aform_def inl_def)
      apply (subst (asm) independent_pdevs_eq_Nil_iff)
      apply (auto simp: list_all_iff list_of_pdevs_def dest: )
      done
    hence "aform_val e X = fst X"
      by (simp add: aform_val_def)
    with len assms have "aform_val e X \<in> {(xl, m0) .. (xl, M0)}"
      by (auto simp: bound_intersect_2d_ud_def Let_def split: split_if_asm)
  } ultimately have "aform_val e X \<in> {(xl, m0)..(xl, M0)}"
    by arith
  thus "(a, b) \<in> {(fst (a, b), m0)..(fst (a, b), M0)}"
    using safeassms
    by simp
qed

definition inter_aform_plane_ortho::"nat \<Rightarrow> 'a::executable_euclidean_space aform \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a aform option"
  where
  "inter_aform_plane_ortho p Z n g = do {
    mMs \<leftarrow> those (map (\<lambda>b. bound_intersect_2d_ud p (inner2_aform Z n b) g) Basis_list);
    let l = (\<Sum>(b, m)\<leftarrow>zip Basis_list (map fst mMs). m *\<^sub>R b);
    let u = (\<Sum>(b, M)\<leftarrow>zip Basis_list (map snd mMs). M *\<^sub>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 \<and> (\<forall>i.\<exists>y. i < length xs \<longrightarrow> 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 nth_Basis_list_nonneg:
  "n < length (Basis_list::'a::executable_euclidean_space list) \<Longrightarrow> 0 \<le> (Basis_list::'a list) ! n"
  by (auto dest!: nth_mem)

lemma
  listsum_zip_map:
  assumes "distinct xs"
  shows "(\<Sum>(x, y)\<leftarrow>zip xs (map g xs). f x y) = (\<Sum>x\<in>set xs. f x (g x))"
  apply (simp add: listsum_distinct_conv_setsum_set assms distinct_zipI1 split_beta')
  apply (rule setsum.reindex_cong[where l="\<lambda>x. (x, g x)"])
  apply (auto simp: in_set_zip in_set_conv_nth assms)
  defer
  defer
  apply (rule_tac x = i in exI)
  apply (auto simp: assms)
  by (metis inj_on_convol_ident)

lemma pdevs_domain_unop_linear:
  assumes "linear f"
  shows "pdevs_domain (unop_pdevs f x) \<subseteq> pdevs_domain x"
proof -
  interpret f: linear f by fact
  print_theorems
  show ?thesis
    by (auto simp: f.zero)
qed

lemma
  pdevs_val_unop_linear:
  assumes "linear f"
  shows "pdevs_val e (unop_pdevs f x) = f (pdevs_val e x)"
proof -
  interpret f: linear f by fact
  have *: "\<And>i. (if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i)) = f (pdevs_apply x i)"
    by (auto simp: f.zero)
  show ?thesis
    apply (simp add: pdevs_val_pdevs_domain * f.setsum f.scaleR cong: if_cong)
    apply (rule setsum.mono_neutral_cong_left)
    apply (auto )
    done
qed

lemma linear_inner2[intro, simp]: "linear (\<lambda>x. inner2 x n i)"
  apply unfold_locales
  apply (auto simp: inner2_def algebra_simps)
  done

lemma inner2_image_aform: "(\<lambda>x. (x \<bullet> n, x \<bullet> i)) ` Affine Z = Affine (inner2_aform Z n i)"
  apply (auto simp: inner2_aform_def Affine_def valuate_def aform_val_def pdevs_inner2_def
    pdevs_val_unop_linear prod_eq_iff)
  apply (rule_tac x= e in image_eqI)
  apply (auto simp: inner2_def algebra_simps)
  apply (rule_tac x= "fst Z + pdevs_val e (snd Z)" in image_eqI)
  apply (auto simp add: algebra_simps)
  done

lemma
  aform_val_aform_of_ivl_innerE:
  assumes "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes "a \<le> b" "c \<in> Basis"
  obtains f where "aform_val e (aform_of_ivl a b) \<bullet> c = aform_val f (aform_of_ivl (a \<bullet> c) (b \<bullet> c))"
    "f \<in> UNIV \<rightarrow> {-1 .. 1}"
proof -
  have [simp]: "a \<bullet> c \<le> b \<bullet> c"
    using assms by (auto simp: eucl_le[where 'a='a])
  have "(\<lambda>x. x \<bullet> c) ` Affine (aform_of_ivl a b) = Affine (aform_of_ivl (a \<bullet> c) (b \<bullet> c))"
    using assms
    by (auto simp: Affine_aform_of_ivl eucl_le[where 'a='a]
      image_eqI[where x="\<Sum>i\<in>Basis. (if i = c then x else a \<bullet> i) *\<^sub>R i" for x])
  then obtain f where
      "aform_val e (aform_of_ivl a b) \<bullet> c = aform_val f (aform_of_ivl (a \<bullet> c) (b \<bullet> c))"
      "f \<in> UNIV \<rightarrow> {-1 .. 1}"
    using assms
    by (force simp: Affine_def valuate_def)
  thus ?thesis ..
qed

lemma aform_val_inner2_aform[simp]: "aform_val e (inner2_aform Z n i) = inner2 (aform_val e Z) n i"
  apply (auto simp: aform_val_def inner2_aform_def pdevs_inner2_def pdevs_val_unop_linear)
  apply (simp add: inner2_def algebra_simps)
  done

lemma
  inter_aform_plane_ortho_overappr:
  assumes "inter_aform_plane_ortho p Z n g = Some X"
  shows "{x. \<forall>i \<in> Basis. x \<bullet> i \<in> {y. (g, y) \<in> (\<lambda>x. (x \<bullet> n, x \<bullet> i)) ` Affine Z}} \<subseteq> Affine X"
proof -
  from assms show ?thesis
    apply (cases "those (map (\<lambda>b. bound_intersect_2d_ud p (inner2_aform Z n b) g) Basis_list)")
    apply (auto simp: inter_aform_plane_ortho_def listsum_zip_map dest!: those_eq_SomeD simp: )
    apply (subst Affine_aform_of_ivl)
    apply (auto simp: eucl_le[where 'a='a])
  proof -
    case goal1
    from `i \<in> Basis` obtain j where "i = (Basis_list::'a list) ! j" "j < length (Basis_list::'a list)"
      by (metis in_set_conv_nth Basis_list)
    then obtain m M where "bound_intersect_2d_ud p (inner2_aform Z n i) g = Some (m, M)"
      using goal1 by auto
    thus ?case
      by (auto simp: bound_intersect_2d_ud_segments_of_aform_le)
  next
    case goal2
    hence x_in2: "(g, x \<bullet> i) \<in> (\<lambda>x. (x \<bullet> n, x \<bullet> i)) ` Affine Z"
      by auto
    from x_in2 obtain e
    where e: "e \<in> UNIV \<rightarrow> {- 1..1}"
      and g: "g = aform_val e Z \<bullet> n"
      and x: "x \<bullet> i = aform_val e Z \<bullet> 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)} \<inter> {x. fst x = g}"
      by (auto simp: g inner2_def)
    also
    from `i \<in> Basis` obtain j where "i = (Basis_list::'a list) ! j" "j < length (Basis_list::'a list)"
      by (metis in_set_conv_nth Basis_list)
    then obtain m M where mM: "bound_intersect_2d_ud p (inner2_aform Z n i) g = Some (m, M)"
      using goal2 by auto
    note bound_intersect_2d_ud_segments_of_aform[OF this e]
    finally have "x \<bullet> i \<in> {m .. M}" using goal2
      by (auto simp: x inner2_def)
    thus ?case "x \<bullet> i \<le> snd (the (bound_intersect_2d_ud p (inner2_aform Z n i) g))"
      by (auto simp: mM)
  qed
qed

lemma inter_proj_eq:
  fixes n g l
  defines "G \<equiv> {x. x \<bullet> n = g}"
  shows "(\<lambda>x. x \<bullet> l) ` (Z \<inter> G) = {y. (g, y) \<in> (\<lambda>x. (x \<bullet> n, x \<bullet> l)) ` Z}"
  by (auto simp: G_def)

lemma
  inter_overappr:
  fixes n \<gamma> l
  shows "Z \<inter> {x. x \<bullet> n = g} \<subseteq> {x. \<forall>i \<in> Basis. x \<bullet> i \<in> {y. (g, y) \<in> (\<lambda>x. (x \<bullet> n, x \<bullet> i)) ` Z}}"
  by auto

lemma inter_inter_aform_plane_ortho:
  assumes "inter_aform_plane_ortho p Z n g = Some X"
  shows "Affine Z \<inter> {x. x \<bullet> n = g} \<subseteq> Affine X"
proof -
  note inter_overappr[of "Affine Z" n g]
  also note inter_aform_plane_ortho_overappr[OF assms]
  finally show ?thesis .
qed

end
