# Theory Affine_Arithmetic.Intersection

section ‹Intersection›
theory Intersection
imports
Polygon
Counterclockwise_2D_Arbitrary
Affine_Form
begin
text ‹\label{sec:intersection}›

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

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

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

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

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

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

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

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

subsection ‹Orient all entries›

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

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

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

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

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

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

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

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

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

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

subsection ‹Lowest Vertex›

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

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

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

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

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

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

subsection ‹Collinear Generators›

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Independent Generators›

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

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

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

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

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

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

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

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

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

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

from 2 have "x ≠ 0" by simp

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

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

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

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

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

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

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

ultimately show ?case by blast
qed

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

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

from 2 have "x ≠ 0" by simp

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

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

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

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

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

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

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

ultimately show ?case by blast
qed

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

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

subsection ‹Independent Oriented Generators›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Half Segments›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma distinct_snd_half_segments:
"distinct (map snd (half_segments_of_aform X)`