section ‹Intersection› theory Intersection imports "HOL-Library.Monad_Syntax" Polygon Counterclockwise_2D_Arbitrary Affine_Form begin text ‹\label{sec:intersection}› subsection ‹Polygons and @{term ccw}, @{term lex}, @{term psi}, @{term coll}› lemma polychain_of_ccw_conjunction: assumes sorted: "ccw'.sortedP 0 Ps" assumes z: "z ∈ set (polychain_of Pc Ps)" shows "list_all (λ(xi, xj). ccw xi xj (fst z) ∧ ccw xi xj (snd z)) (polychain_of Pc Ps)" using assms proof (induction Ps arbitrary: Pc z rule: list.induct) case (Cons P Ps) { assume "set Ps = {}" hence ?case using Cons by simp } moreover { assume "set Ps ≠ {}" hence "Ps ≠ []" by simp { fix a assume "a ∈ set Ps" hence "ccw' 0 P a" using Cons.prems by (auto elim!: linorder_list0.sortedP_Cons) } note ccw' = this have sorted': "linorder_list0.sortedP (ccw' 0) Ps" using Cons.prems by (auto elim!: linorder_list0.sortedP_Cons) from in_set_polychain_of_imp_sum_list[OF Cons(3)] obtain d where d: "z = (Pc + sum_list (take d (P # Ps)), Pc + sum_list (take (Suc d) (P # Ps)))" . from Cons(3) have disj: "z = (Pc, Pc + P) ∨ z ∈ set (polychain_of (Pc + P) Ps)" by auto let ?th = "λ(xi, xj). ccw xi xj Pc ∧ ccw xi xj (Pc + P)" have la: "list_all ?th (polychain_of (Pc + P) Ps)" proof (rule list_allI) fix x assume x: "x ∈ set (polychain_of (Pc + P) Ps)" from in_set_polychain_of_imp_sum_list[OF this] obtain e where e: "x = (Pc + P + sum_list (take e Ps), Pc + P + sum_list (take (Suc e) Ps))" by auto { assume "e ≥ length Ps" hence "?th x" by (auto simp: e) } moreover { assume "e < length Ps" have 0: "⋀e. e < length Ps ⟹ ccw' 0 P (Ps ! e)" by (rule ccw') simp have 2: "0 < e ⟹ ccw' 0 (P + sum_list (take e Ps)) (Ps ! e)" using ‹e < length Ps› by (auto intro!: ccw'.add1 0 ccw'.sum2 sorted' ccw'.sorted_nth_less simp: sum_list_sum_nth) have "ccw Pc (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps))" by (cases "e = 0") (auto simp add: ccw_translate_origin take_Suc_eq add.assoc[symmetric] 0 2 intro!: ccw'_imp_ccw intro: cyclic) hence "ccw (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps)) Pc" by (rule cyclic) moreover have "0 < e ⟹ ccw 0 (Ps ! e) (- sum_list (take e Ps))" using ‹e < length Ps› by (auto simp add: take_Suc_eq add.assoc[symmetric] sum_list_sum_nth intro!: ccw'_imp_ccw ccw'.sum2 sorted' ccw'.sorted_nth_less) hence "ccw (Pc + P + sum_list (take e Ps)) (Pc + P + sum_list (take (Suc e) Ps)) (Pc + P)" by (cases "e = 0") (simp_all add: ccw_translate_origin take_Suc_eq) ultimately have "?th x" by (auto simp add: e) } ultimately show "?th x" by arith qed from disj have ?case proof assume z: "z ∈ set (polychain_of (Pc + P) Ps)" have "ccw 0 P (sum_list (take d (P # Ps)))" proof (cases d) case (Suc e) note e = this show ?thesis proof (cases e) case (Suc f) have "ccw 0 P (P + sum_list (take (Suc f) Ps))" using z by (force simp add: sum_list_sum_nth intro!: ccw'.sum intro: ccw' ccw'_imp_ccw) thus ?thesis by (simp add: e Suc) qed (simp add: e) qed simp hence "ccw Pc (Pc + P) (fst z)" by (simp add: d ccw_translate_origin) moreover from z have "ccw 0 P (P + sum_list (take d Ps))" by (cases d, force) (force simp add: sum_list_sum_nth intro!: ccw'_imp_ccw ccw'.sum intro: ccw')+ hence "ccw Pc (Pc + P) (snd z)" by (simp add: d ccw_translate_origin) moreover from z Cons.prems have "list_all (λ(xi, xj). ccw xi xj (fst z) ∧ ccw xi xj (snd z)) (polychain_of (Pc + P) Ps)" by (intro Cons.IH) (auto elim!: linorder_list0.sortedP_Cons) ultimately show ?thesis by simp qed (simp add: la) } ultimately show ?case by blast qed simp lemma lex_polychain_of_center: "d ∈ set (polychain_of x0 xs) ⟹ list_all (λx. lex x 0) xs ⟹ lex (snd d) x0" proof (induction xs arbitrary: x0) case (Cons x xs) thus ?case by (auto simp add: lex_def lex_translate_origin dest!: Cons.IH) qed (auto simp: lex_translate_origin) lemma lex_polychain_of_last: "(c, d) ∈ set (polychain_of x0 xs) ⟹ list_all (λx. lex x 0) xs ⟹ lex (snd (last (polychain_of x0 xs))) d" proof (induction xs arbitrary: x0 c d) case (Cons x xs) let ?c1 = "c = x0 ∧ d = x0 + x" let ?c2 = "(c, d) ∈ set (polychain_of (x0 + x) xs)" from Cons(2) have "?c1 ∨ ?c2" by auto thus ?case proof assume ?c1 with Cons.prems show ?thesis by (auto intro!: lex_polychain_of_center) next assume ?c2 from Cons.IH[OF this] Cons.prems show ?thesis by auto qed qed (auto simp: lex_translate_origin) lemma distinct_fst_polychain_of: assumes "list_all (λx. x ≠ 0) xs" assumes "list_all (λx. lex x 0) xs" shows "distinct (map fst (polychain_of x0 xs))" using assms proof (induction xs arbitrary: x0) case Nil thus ?case by simp next case (Cons x xs) hence "⋀d. list_all (λx. lex x 0) (x # take d xs)" by (auto simp: list_all_iff dest!: in_set_takeD) from sum_list_nlex_eq_zero_iff[OF this] Cons.prems show ?case by (cases "xs = []") (auto intro!: Cons.IH elim!: in_set_polychain_of_imp_sum_list) qed lemma distinct_snd_polychain_of: assumes "list_all (λx. x ≠ 0) xs" assumes "list_all (λx. lex x 0) xs" shows "distinct (map snd (polychain_of x0 xs))" using assms proof (induction xs arbitrary: x0) case Nil thus ?case by simp next case (Cons x xs) have contra: "⋀d. xs ≠ [] ⟹ list_all (λx. x ≠ 0) xs ⟹ list_all ((=) 0) (take (Suc d) xs) ⟹ False" by (auto simp: neq_Nil_conv) from Cons have "⋀d. list_all (λx. lex x 0) (take (Suc d) xs)" by (auto simp: list_all_iff dest!: in_set_takeD) from sum_list_nlex_eq_zero_iff[OF this] Cons.prems contra show ?case by (cases "xs = []") (auto intro!: Cons.IH elim!: in_set_polychain_of_imp_sum_list dest!: contra) qed subsection ‹Orient all entries› lift_definition nlex_pdevs::"point pdevs ⇒ point pdevs" is "λx n. if lex 0 (x n) then - x n else x n" by simp lemma pdevs_apply_nlex_pdevs[simp]: "pdevs_apply (nlex_pdevs x) n = (if lex 0 (pdevs_apply x n) then - pdevs_apply x n else pdevs_apply x n)" by transfer simp lemma nlex_pdevs_zero_pdevs[simp]: "nlex_pdevs zero_pdevs = zero_pdevs" by (auto intro!: pdevs_eqI) lemma pdevs_domain_nlex_pdevs[simp]: "pdevs_domain (nlex_pdevs x) = pdevs_domain x" by (auto simp: pdevs_domain_def) lemma degree_nlex_pdevs[simp]: "degree (nlex_pdevs x) = degree x" by (rule degree_cong) auto lemma pdevs_val_nlex_pdevs: assumes "e ∈ UNIV → I" "uminus ` I = I" obtains e' where "e' ∈ UNIV → I" "pdevs_val e x = pdevs_val e' (nlex_pdevs x)" using assms by (atomize_elim, intro exI[where x="λn. if lex 0 (pdevs_apply x n) then - e n else e n"]) (force simp: pdevs_val_pdevs_domain intro!: sum.cong) lemma pdevs_val_nlex_pdevs2: assumes "e ∈ UNIV → I" "uminus ` I = I" obtains e' where "e' ∈ UNIV → I" "pdevs_val e (nlex_pdevs x) = pdevs_val e' x" using assms by (atomize_elim, intro exI[where x="λn. (if lex 0 (pdevs_apply x n) then - e n else e n)"]) (force simp: pdevs_val_pdevs_domain intro!: sum.cong) lemma pdevs_val_selsort_ccw: assumes "distinct xs" assumes "e ∈ UNIV → I" obtains e' where "e' ∈ UNIV → I" "pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (ccw.selsort 0 xs))" proof - have "set xs = set (ccw.selsort 0 xs)" "distinct xs" "distinct (ccw.selsort 0 xs)" by (simp_all add: assms) from this assms(2) obtain e' where "e' ∈ UNIV → I" "pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (ccw.selsort 0 xs))" by (rule pdevs_val_permute) thus thesis .. qed lemma pdevs_val_selsort_ccw2: assumes "distinct xs" assumes "e ∈ UNIV → I" obtains e' where "e' ∈ UNIV → I" "pdevs_val e (pdevs_of_list (ccw.selsort 0 xs)) = pdevs_val e' (pdevs_of_list xs)" proof - have "set (ccw.selsort 0 xs) = set xs" "distinct (ccw.selsort 0 xs)" "distinct xs" by (simp_all add: assms) from this assms(2) obtain e' where "e' ∈ UNIV → I" "pdevs_val e (pdevs_of_list (ccw.selsort 0 xs)) = pdevs_val e' (pdevs_of_list xs)" by (rule pdevs_val_permute) thus thesis .. qed lemma lex_nlex_pdevs: "lex (pdevs_apply (nlex_pdevs x) i) 0" by (auto simp: lex_def algebra_simps prod_eq_iff) subsection ‹Lowest Vertex› definition lowest_vertex::"'a::ordered_euclidean_space aform ⇒ 'a" where "lowest_vertex X = fst X - sum_list (map snd (list_of_pdevs (snd X)))" lemma snd_abs: "snd (abs x) = abs (snd x)" by (metis abs_prod_def snd_conv) lemma lowest_vertex: fixes X Y::"(real*real) aform" assumes "e ∈ UNIV → {-1 .. 1}" assumes "⋀i. snd (pdevs_apply (snd X) i) ≥ 0" assumes "⋀i. abs (snd (pdevs_apply (snd Y) i)) = abs (snd (pdevs_apply (snd X) i))" assumes "degree_aform Y = degree_aform X" assumes "fst Y = fst X" shows "snd (lowest_vertex X) ≤ snd (aform_val e Y)" proof - from abs_pdevs_val_le_tdev[OF assms(1), of "snd Y"] have "snd ¦pdevs_val e (snd Y)¦ ≤ (∑i<degree_aform Y. ¦snd (pdevs_apply (snd X) i)¦)" unfolding lowest_vertex_def by (auto simp: aform_val_def tdev_def less_eq_prod_def snd_sum snd_abs assms) also have "… = (∑i<degree_aform X. snd (pdevs_apply (snd X) i))" by (simp add: assms) also have "… ≤ snd (sum_list (map snd (list_of_pdevs (snd X))))" by (simp add: sum_list_list_of_pdevs dense_list_of_pdevs_def sum_list_distinct_conv_sum_set snd_sum atLeast0LessThan) finally show ?thesis by (auto simp: aform_val_def lowest_vertex_def minus_le_iff snd_abs abs_real_def assms split: if_split_asm) qed lemma sum_list_nonposI: fixes xs::"'a::ordered_comm_monoid_add list" shows "list_all (λx. x ≤ 0) xs ⟹ sum_list xs ≤ 0" by (induct xs) (auto simp: intro!: add_nonpos_nonpos) lemma center_le_lowest: "fst (fst X) ≤ fst (lowest_vertex (fst X, nlex_pdevs (snd X)))" by (auto simp: lowest_vertex_def fst_sum_list intro!: sum_list_nonposI) (auto simp: lex_def list_all_iff list_of_pdevs_def dest!: in_set_butlastD split: if_split_asm) lemma lowest_vertex_eq_center_iff: "lowest_vertex (x0, nlex_pdevs (snd X)) = x0 ⟷ snd X = zero_pdevs" proof assume "lowest_vertex (x0, nlex_pdevs (snd X)) = x0" then have "sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))) = 0" by (simp add: lowest_vertex_def) moreover have "list_all (λx. Counterclockwise_2D_Arbitrary.lex x 0) (map snd (list_of_pdevs (nlex_pdevs (snd X))))" by (auto simp add: list_all_iff list_of_pdevs_def) ultimately have "∀x∈set (list_of_pdevs (nlex_pdevs (snd X))). snd x = 0" by (simp add: sum_list_nlex_eq_zero_iff list_all_iff) then have "pdevs_apply (snd X) i = pdevs_apply zero_pdevs i" for i by (simp add: list_of_pdevs_def split: if_splits) then show "snd X = zero_pdevs" by (rule pdevs_eqI) qed (simp add: lowest_vertex_def) subsection ‹Collinear Generators› lemma scaleR_le_self_cancel: fixes c::"'a::ordered_real_vector" shows "a *⇩_{R}c ≤ c ⟷ (1 < a ∧ c ≤ 0 ∨ a < 1 ∧ 0 ≤ c ∨ a = 1)" using scaleR_le_0_iff[of "a - 1" c] by (simp add: algebra_simps) lemma pdevs_val_coll: assumes coll: "list_all (coll 0 x) xs" assumes nlex: "list_all (λx. lex x 0) xs" assumes "x ≠ 0" assumes "f ∈ UNIV → {-1 .. 1}" obtains e where "e ∈ {-1 .. 1}" "pdevs_val f (pdevs_of_list xs) = e *⇩_{R}(sum_list xs)" proof cases assume "sum_list xs = 0" have "pdevs_of_list xs = zero_pdevs" by (auto intro!: pdevs_eqI sum_list_nlex_eq_zeroI[OF nlex ‹sum_list xs = 0›] simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem) hence "0 ∈ {-1 .. 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *⇩_{R}sum_list xs" by simp_all thus ?thesis .. next assume "sum_list xs ≠ 0" have "sum_list (map abs xs) ≥ 0" by (auto intro!: sum_list_nonneg) hence [simp]: "¬sum_list (map abs xs) ≤ 0" by (metis ‹sum_list xs ≠ 0› abs_le_zero_iff antisym_conv sum_list_abs) have collist: "list_all (coll 0 (sum_list xs)) xs" proof (rule list_allI) fix y assume "y ∈ set xs" hence "coll 0 x y" using coll by (auto simp: list_all_iff) also have "coll 0 x (sum_list xs)" using coll by (auto simp: list_all_iff intro!: coll_sum_list) finally (coll_trans) show "coll 0 (sum_list xs) y" by (simp add: coll_commute ‹x ≠ 0›) qed { fix i assume "i < length xs" hence "∃r. xs ! i = r *⇩_{R}(sum_list xs)" by (metis (mono_tags) coll_scale nth_mem ‹sum_list xs ≠ 0› list_all_iff collist) } then obtain r where r: "⋀i. i < length xs ⟹ (xs ! i) = r i *⇩_{R}(sum_list xs)" by metis let ?coll = "pdevs_of_list xs" have "pdevs_val f (pdevs_of_list xs) = (∑i<degree (pdevs_of_list xs). f i *⇩_{R}xs ! i)" unfolding pdevs_val_sum by (simp add: pdevs_apply_pdevs_of_list less_degree_pdevs_of_list_imp_less_length) also have "… = (∑i<degree ?coll. (f i * r i) *⇩_{R}(sum_list xs))" by (simp add: r less_degree_pdevs_of_list_imp_less_length) also have "… = (∑i<degree ?coll. f i * r i) *⇩_{R}(sum_list xs)" by (simp add: algebra_simps scaleR_sum_left) finally have eq: "pdevs_val f ?coll = (∑i<degree ?coll. f i * r i) *⇩_{R}(sum_list xs)" (is "_ = ?e *⇩_{R}_") . have "abs (pdevs_val f ?coll) ≤ tdev ?coll" using assms(4) by (intro abs_pdevs_val_le_tdev) (auto simp: Pi_iff less_imp_le) also have "… = sum_list (map abs xs)" using assms by simp also note eq finally have less: "¦?e¦ *⇩_{R}abs (sum_list xs) ≤ sum_list (map abs xs)" by (simp add: abs_scaleR) also have "¦sum_list xs¦ = sum_list (map abs xs)" using coll ‹x ≠ 0› nlex by (rule abs_sum_list_coll) finally have "?e ∈ {-1 .. 1}" by (auto simp add: less_le scaleR_le_self_cancel) thus ?thesis using eq .. qed lemma scaleR_eq_self_cancel: fixes x::"'a::real_vector" shows "a *⇩_{R}x = x ⟷ a = 1 ∨ x = 0" using scaleR_cancel_right[of a x 1] by simp lemma abs_pdevs_val_less_tdev: assumes "e ∈ UNIV → {-1 <..< 1}" "degree x > 0" shows "¦pdevs_val e x¦ < tdev x" proof - have bnds: "⋀i. ¦e i¦ < 1" "⋀i. ¦e i¦ ≤ 1" using assms by (auto simp: Pi_iff abs_less_iff order.strict_implies_order) moreover let ?w = "degree x - 1" have witness: "¦e ?w¦ *⇩_{R}¦pdevs_apply x ?w¦ < ¦pdevs_apply x ?w¦" using degree_least_nonzero[of x] assms bnds by (intro neq_le_trans) (auto simp: scaleR_eq_self_cancel Pi_iff intro!: scaleR_left_le_one_le neq_le_trans intro: abs_leI less_imp_le dest!: order.strict_implies_not_eq) ultimately show ?thesis using assms witness bnds by (auto simp: pdevs_val_sum tdev_def abs_scaleR intro!: le_less_trans[OF sum_abs] sum_strict_mono_ex1 scaleR_left_le_one_le) qed lemma pdevs_val_coll_strict: assumes coll: "list_all (coll 0 x) xs" assumes nlex: "list_all (λx. lex x 0) xs" assumes "x ≠ 0" assumes "f ∈ UNIV → {-1 <..< 1}" obtains e where "e ∈ {-1 <..< 1}" "pdevs_val f (pdevs_of_list xs) = e *⇩_{R}(sum_list xs)" proof cases assume "sum_list xs = 0" have "pdevs_of_list xs = zero_pdevs" by (auto intro!: pdevs_eqI sum_list_nlex_eq_zeroI[OF nlex ‹sum_list xs = 0›] simp: pdevs_apply_pdevs_of_list list_all_iff dest!: nth_mem) hence "0 ∈ {-1 <..< 1::real}" "pdevs_val f (pdevs_of_list xs) = 0 *⇩_{R}sum_list xs" by simp_all thus ?thesis .. next assume "sum_list xs ≠ 0" have "sum_list (map abs xs) ≥ 0" by (auto intro!: sum_list_nonneg) hence [simp]: "¬sum_list (map abs xs) ≤ 0" by (metis ‹sum_list xs ≠ 0› abs_le_zero_iff antisym_conv sum_list_abs) have "∃x ∈ set xs. x ≠ 0" proof (rule ccontr) assume "¬ (∃x∈set xs. x ≠ 0)" hence "⋀x. x ∈ set xs ⟹ x = 0" by auto hence "sum_list xs = 0" by (auto simp: sum_list_eq_0_iff_nonpos list_all_iff less_eq_prod_def prod_eq_iff fst_sum_list snd_sum_list) thus False using ‹sum_list xs ≠ 0› by simp qed then obtain i where i: "i < length xs" "xs ! i ≠ 0" by (metis in_set_conv_nth) hence "i < degree (pdevs_of_list xs)" by (auto intro!: degree_gt simp: pdevs_apply_pdevs_of_list) hence deg_pos: "0 < degree (pdevs_of_list xs)" by simp have collist: "list_all (coll 0 (sum_list xs)) xs" proof (rule list_allI) fix y assume "y ∈ set xs" hence "coll 0 x y" using coll by (auto simp: list_all_iff) also have "coll 0 x (sum_list xs)" using coll by (auto simp: list_all_iff intro!: coll_sum_list) finally (coll_trans) show "coll 0 (sum_list xs) y" by (simp add: coll_commute ‹x ≠ 0›) qed { fix i assume "i < length xs" hence "∃r. xs ! i = r *⇩_{R}(sum_list xs)" by (metis (mono_tags, lifting) ‹sum_list xs ≠ 0› coll_scale collist list_all_iff nth_mem) } then obtain r where r: "⋀i. i < length xs ⟹ (xs ! i) = r i *⇩_{R}(sum_list xs)" by metis let ?coll = "pdevs_of_list xs" have "pdevs_val f (pdevs_of_list xs) = (∑i<degree (pdevs_of_list xs). f i *⇩_{R}xs ! i)" unfolding pdevs_val_sum by (simp add: less_degree_pdevs_of_list_imp_less_length pdevs_apply_pdevs_of_list) also have "… = (∑i<degree ?coll. (f i * r i) *⇩_{R}(sum_list xs))" by (simp add: r less_degree_pdevs_of_list_imp_less_length) also have "… = (∑i<degree ?coll. f i * r i) *⇩_{R}(sum_list xs)" by (simp add: algebra_simps scaleR_sum_left) finally have eq: "pdevs_val f ?coll = (∑i<degree ?coll. f i * r i) *⇩_{R}(sum_list xs)" (is "_ = ?e *⇩_{R}_") . have "abs (pdevs_val f ?coll) < tdev ?coll" using assms(4) by (intro abs_pdevs_val_less_tdev) (auto simp: Pi_iff less_imp_le deg_pos) also have "… = sum_list (map abs xs)" using assms by simp also note eq finally have less: "¦?e¦ *⇩_{R}abs (sum_list xs) < sum_list (map abs xs)" by (simp add: abs_scaleR) also have "¦sum_list xs¦ = sum_list (map abs xs)" using coll ‹x ≠ 0› nlex by (rule abs_sum_list_coll) finally have "?e ∈ {-1 <..< 1}" by (auto simp add: less_le scaleR_le_self_cancel) thus ?thesis using eq .. qed subsection ‹Independent Generators› fun independent_pdevs::"point list ⇒ point list" where "independent_pdevs [] = []" | "independent_pdevs (x#xs) = (let (cs, is) = List.partition (coll 0 x) xs; s = x + sum_list cs in (if s = 0 then [] else [s]) @ independent_pdevs is)" lemma in_set_independent_pdevsE: assumes "y ∈ set (independent_pdevs xs)" obtains x where "x∈set xs" "coll 0 x y" proof atomize_elim show "∃x. x ∈ set xs ∧ coll 0 x y" using assms proof (induct xs rule: independent_pdevs.induct) case 1 thus ?case by simp next case (2 z zs) let ?c1 = "y = z + sum_list (filter (coll 0 z) zs)" let ?c2 = "y ∈ set (independent_pdevs (filter (Not ∘ coll 0 z) zs))" from 2 have "?c1 ∨ ?c2" by (auto simp: Let_def split: if_split_asm) thus ?case proof assume ?c2 hence "y ∈ set (independent_pdevs (snd (partition (coll 0 z) zs)))" by simp from 2(1)[OF refl prod.collapse refl this] show ?case by auto next assume y: ?c1 show ?case unfolding y by (rule exI[where x="z"]) (auto intro!: coll_add coll_sum_list ) qed qed qed lemma in_set_independent_pdevs_nonzero: "x ∈ set (independent_pdevs xs) ⟹ x ≠ 0" proof (induct xs rule: independent_pdevs.induct) case (2 y ys) from 2(1)[OF refl prod.collapse refl] 2(2) show ?case by (auto simp: Let_def split: if_split_asm) qed simp lemma independent_pdevs_pairwise_non_coll: assumes "x ∈ set (independent_pdevs xs)" assumes "y ∈ set (independent_pdevs xs)" assumes "⋀x. x ∈ set xs ⟹ x ≠ 0" assumes "x ≠ y" shows "¬ coll 0 x y" using assms proof (induct xs rule: independent_pdevs.induct) case 1 thus ?case by simp next case (2 z zs) from 2 have "z ≠ 0" by simp from 2(2) have "x ≠ 0" by (rule in_set_independent_pdevs_nonzero) from 2(3) have "y ≠ 0" by (rule in_set_independent_pdevs_nonzero) let ?c = "filter (coll 0 z) zs" let ?nc = "filter (Not ∘ coll 0 z) zs" { assume "x ∈ set (independent_pdevs ?nc)" "y ∈ set (independent_pdevs ?nc)" hence "¬coll 0 x y" by (intro 2(1)[OF refl prod.collapse refl _ _ 2(4) 2(5)]) auto } note IH = this { fix x assume "x ≠ 0" "z + sum_list ?c ≠ 0" "coll 0 x (z + sum_list ?c)" hence "x ∉ set (independent_pdevs ?nc)" using sum_list_filter_coll_ex_scale[OF ‹z ≠ 0›, of "z#zs"] by (auto elim!: in_set_independent_pdevsE simp: coll_commute) (metis (no_types) ‹x ≠ 0› coll_scale coll_scaleR) } note nc = this from 2(2,3,4,5) nc[OF ‹x ≠ 0›] nc[OF ‹y ≠ 0›] show ?case by (auto simp: Let_def IH coll_commute split: if_split_asm) qed lemma distinct_independent_pdevs[simp]: shows "distinct (independent_pdevs xs)" proof (induct xs rule: independent_pdevs.induct) case 1 thus ?case by simp next case (2 x xs) let ?is = "independent_pdevs (filter (Not ∘ coll 0 x) xs)" have "distinct ?is" by (rule 2) (auto intro!: 2) thus ?case proof (clarsimp simp add: Let_def) let ?s = "x + sum_list (filter (coll 0 x) xs)" assume s: "?s ≠ 0" "?s ∈ set ?is" from in_set_independent_pdevsE[OF s(2)] obtain y where y: "y ∈ set (filter (Not ∘ coll 0 x) xs)" "coll 0 y (x + sum_list (filter (coll 0 x) xs))" by auto { assume "y = 0 ∨ x = 0 ∨ sum_list (filter (coll 0 x) xs) = 0" hence False using s y by (auto simp: coll_commute) } moreover { assume "y ≠ 0" "x ≠ 0" "sum_list (filter (coll 0 x) xs) ≠ 0" "sum_list (filter (coll 0 x) xs) + x ≠ 0" have *: "coll 0 (sum_list (filter (coll 0 x) xs)) x" by (auto intro!: coll_sum_list simp: coll_commute) have "coll 0 y (sum_list (filter (coll 0 x) xs) + x)" using s y by (simp add: add.commute) hence "coll 0 y x" using * by (rule coll_add_trans) fact+ hence False using s y by (simp add: coll_commute) } ultimately show False using s y by (auto simp: add.commute) qed qed lemma in_set_independent_pdevs_invariant_nlex: "x ∈ set (independent_pdevs xs) ⟹ (⋀x. x ∈ set xs ⟹ lex x 0) ⟹ (⋀x. x ∈ set xs ⟹ x ≠ 0) ⟹ Counterclockwise_2D_Arbitrary.lex x 0" proof (induction xs arbitrary: x rule: independent_pdevs.induct ) case 1 thus ?case by simp next case (2 y ys) from 2 have "y ≠ 0" by auto from 2(2) have "x ∈ set (independent_pdevs (filter (Not ∘ coll 0 y) ys)) ∨ x = y + sum_list (filter (coll 0 y) ys)" by (auto simp: Let_def split: if_split_asm) thus ?case proof assume "x ∈ set (independent_pdevs (filter (Not ∘ coll 0 y) ys))" from 2(1)[OF refl prod.collapse refl, simplified, OF this 2(3,4)] show ?case by simp next assume "x = y + sum_list (filter (coll 0 y) ys)" also have "lex … 0" by (force intro: nlex_add nlex_sum simp: sum_list_sum_nth dest: nth_mem intro: 2(3)) finally show ?case . qed qed lemma pdevs_val_independent_pdevs2: assumes "e ∈ UNIV → I" shows "∃e'. e' ∈ UNIV → I ∧ pdevs_val e (pdevs_of_list (independent_pdevs xs)) = pdevs_val e' (pdevs_of_list xs)" using assms proof (induct xs arbitrary: e rule: independent_pdevs.induct) case 1 thus ?case by force next case (2 x xs) let ?coll = "(filter (coll 0 x) (x#xs))" let ?ncoll = "(filter (Not o coll 0 x) (x#xs))" let ?e0 = "if sum_list ?coll = 0 then e else e ∘ (+) (Suc 0)" have "pdevs_val e (pdevs_of_list (independent_pdevs (x#xs))) = e 0 *⇩_{R}(sum_list ?coll) + pdevs_val ?e0 (pdevs_of_list (independent_pdevs ?ncoll))" (is "_ = ?vc + ?vnc") by (simp add: Let_def) also have e_split: "(λ_. e 0) ∈ UNIV → I" "?e0 ∈ UNIV → I" using 2(2) by auto from 2(1)[OF refl prod.collapse refl e_split(2)] obtain e' where e': "e' ∈ UNIV → I" and "?vnc = pdevs_val e' (pdevs_of_list ?ncoll)" by (auto simp add: o_def) note this(2) also have "?vc = pdevs_val (λ_. e 0) (pdevs_of_list ?coll)" by (simp add: pdevs_val_const_pdevs_of_list) also from pdevs_val_pdevs_of_list_append[OF e_split(1) e'] obtain e'' where e'': "e'' ∈ UNIV → I" and "pdevs_val (λ_. e 0) (pdevs_of_list ?coll) + pdevs_val e' (pdevs_of_list ?ncoll) = pdevs_val e'' (pdevs_of_list (?coll @ ?ncoll))" by metis note this(2) also from pdevs_val_perm[OF partition_permI e'', of "coll 0 x" "x#xs"] obtain e''' where e''': "e''' ∈ UNIV → I" and "… = pdevs_val e''' (pdevs_of_list (x # xs))" by metis note this(2) finally show ?case using e''' by auto qed lemma list_all_filter: "list_all p (filter p xs)" by (induct xs) auto lemma pdevs_val_independent_pdevs: assumes "list_all (λx. lex x 0) xs" assumes "list_all (λx. x ≠ 0) xs" assumes "e ∈ UNIV → {-1 .. 1}" shows "∃e'. e' ∈ UNIV → {-1 .. 1} ∧ pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (independent_pdevs xs))" using assms(1,2,3) proof (induct xs arbitrary: e rule: independent_pdevs.induct) case 1 thus ?case by force next case (2 x xs) let ?coll = "(filter (coll 0 x) (x#xs))" let ?ncoll = "(filter (Not o coll 0 x) xs)" from 2 have "x ≠ 0" by simp from pdevs_val_partition[OF 2(4), of "x#xs" "coll 0 x"] obtain f g where part: "pdevs_val e (pdevs_of_list (x # xs)) = pdevs_val f (pdevs_of_list ?coll) + pdevs_val g (pdevs_of_list (filter (Not o coll 0 x) (x#xs)))" and f: "f ∈ UNIV → {-1 .. 1}" and g: "g ∈ UNIV → {-1 .. 1}" by blast note part also have "list_all (λx. lex x 0) (filter (coll 0 x) (x#xs))" using 2(2) by (auto simp: inner_prod_def list_all_iff) from pdevs_val_coll[OF list_all_filter this ‹x ≠ 0› f] obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *⇩_{R}sum_list (filter (coll 0 x) (x#xs))" and f': "f' ∈ {-1 .. 1}" by blast note this(1) also have "filter (Not o coll 0 x) (x#xs) = ?ncoll" by simp also from 2(2) have "list_all (λx. lex x 0) ?ncoll" "list_all (λx. x ≠ 0) ?ncoll" by (auto simp: list_all_iff) from 2(1)[OF refl partition_filter_conv[symmetric] refl this g] obtain g' where "pdevs_val g (pdevs_of_list ?ncoll) = pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))" and g': "g' ∈ UNIV → {-1 .. 1}" by metis note this(1) also define h where "h = (if sum_list ?coll ≠ 0 then rec_nat f' (λi _. g' i) else g')" have "f' *⇩_{R}sum_list ?coll + pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll)) = pdevs_val h (pdevs_of_list (independent_pdevs (x#xs)))" by (simp add: h_def o_def Let_def) finally have "pdevs_val e (pdevs_of_list (x # xs)) = pdevs_val h (pdevs_of_list (independent_pdevs (x # xs)))" . moreover have "h ∈ UNIV → {-1 .. 1}" proof fix i show "h i ∈ {-1 .. 1}" using f' g' by (cases i) (auto simp: h_def) qed ultimately show ?case by blast qed lemma pdevs_val_independent_pdevs_strict: assumes "list_all (λx. lex x 0) xs" assumes "list_all (λx. x ≠ 0) xs" assumes "e ∈ UNIV → {-1 <..< 1}" shows "∃e'. e' ∈ UNIV → {-1 <..< 1} ∧ pdevs_val e (pdevs_of_list xs) = pdevs_val e' (pdevs_of_list (independent_pdevs xs))" using assms(1,2,3) proof (induct xs arbitrary: e rule: independent_pdevs.induct) case 1 thus ?case by force next case (2 x xs) let ?coll = "(filter (coll 0 x) (x#xs))" let ?ncoll = "(filter (Not o coll 0 x) xs)" from 2 have "x ≠ 0" by simp from pdevs_val_partition[OF 2(4), of "x#xs" "coll 0 x"] obtain f g where part: "pdevs_val e (pdevs_of_list (x # xs)) = pdevs_val f (pdevs_of_list ?coll) + pdevs_val g (pdevs_of_list (filter (Not o coll 0 x) (x#xs)))" and f: "f ∈ UNIV → {-1 <..< 1}" and g: "g ∈ UNIV → {-1 <..< 1}" by blast note part also have "list_all (λx. lex x 0) (filter (coll 0 x) (x#xs))" using 2(2) by (auto simp: inner_prod_def list_all_iff) from pdevs_val_coll_strict[OF list_all_filter this ‹x ≠ 0› f] obtain f' where "pdevs_val f (pdevs_of_list ?coll) = f' *⇩_{R}sum_list (filter (coll 0 x) (x#xs))" and f': "f' ∈ {-1 <..< 1}" by blast note this(1) also have "filter (Not o coll 0 x) (x#xs) = ?ncoll" by simp also from 2(2) have "list_all (λx. lex x 0) ?ncoll" "list_all (λx. x ≠ 0) ?ncoll" by (auto simp: list_all_iff) from 2(1)[OF refl partition_filter_conv[symmetric] refl this g] obtain g' where "pdevs_val g (pdevs_of_list ?ncoll) = pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll))" and g': "g' ∈ UNIV → {-1 <..< 1}" by metis note this(1) also define h where "h = (if sum_list ?coll ≠ 0 then rec_nat f' (λi _. g' i) else g')" have "f' *⇩_{R}sum_list ?coll + pdevs_val g' (pdevs_of_list (independent_pdevs ?ncoll)) = pdevs_val h (pdevs_of_list (independent_pdevs (x#xs)))" by (simp add: h_def o_def Let_def) finally have "pdevs_val e (pdevs_of_list (x # xs)) = pdevs_val h (pdevs_of_list (independent_pdevs (x # xs)))" . moreover have "h ∈ UNIV → {-1 <..< 1}" proof fix i show "h i ∈ {-1 <..< 1}" using f' g' by (cases i) (auto simp: h_def) qed ultimately show ?case by blast qed lemma sum_list_independent_pdevs: "sum_list (independent_pdevs xs) = sum_list xs" proof (induct xs rule: independent_pdevs.induct) case (2 y ys) from 2[OF refl prod.collapse refl] show ?case using sum_list_partition[of "coll 0 y" ys, symmetric] by (auto simp: Let_def) qed simp lemma independent_pdevs_eq_Nil_iff: "list_all (λx. lex x 0) xs ⟹ list_all (λx. x ≠ 0) xs ⟹ independent_pdevs xs = [] ⟷ xs = []" proof (induct xs) case Nil thus ?case by simp next case (Cons x xs) from Cons(2) have "list_all (λx. lex x 0) (x # filter (coll 0 x) xs)" by (auto simp: list_all_iff) from sum_list_nlex_eq_zero_iff[OF this] Cons(3) show ?case by (auto simp: list_all_iff) qed subsection ‹Independent Oriented Generators› definition "inl p = independent_pdevs (map snd (list_of_pdevs (nlex_pdevs p)))" lemma distinct_inl[simp]: "distinct (inl (snd X))" by (auto simp: inl_def) lemma in_set_inl_nonzero: "x ∈ set (inl xs) ⟹ x ≠ 0" by (auto simp: inl_def in_set_independent_pdevs_nonzero) lemma inl_ncoll: "y ∈ set (inl (snd X)) ⟹ z ∈ set (inl (snd X)) ⟹ y ≠ z ⟹ ¬coll 0 y z" unfolding inl_def by (rule independent_pdevs_pairwise_non_coll, assumption+) (auto simp: inl_def list_of_pdevs_nonzero) lemma in_set_inl_lex: "x ∈ set (inl xs) ⟹ lex x 0" by (auto simp: inl_def list_of_pdevs_def dest!: in_set_independent_pdevs_invariant_nlex split: if_split_asm) interpretation ccw0: linorder_list "ccw 0" "set (inl (snd X))" proof unfold_locales fix a b c show "a ≠ b ⟹ ccw 0 a b ∨ ccw 0 b a" by (metis UNIV_I ccw_self(1) nondegenerate) assume a: "a ∈ set (inl (snd X))" show "ccw 0 a a" by simp assume b: "b ∈ set (inl (snd X))" show "ccw 0 a b ⟹ ccw 0 b a ⟹ a = b" by (metis ccw_self(1) in_set_inl_nonzero mem_Collect_eq not_ccw_eq a b) assume c: "c ∈ set (inl (snd X))" assume distinct: "a ≠ b" "b ≠ c" "a ≠ c" assume ab: "ccw 0 a b" and bc: "ccw 0 b c" show "ccw 0 a c" using a b c ab bc proof (cases "a = (0, 1)" "b = (0, 1)" "c = (0, 1)" rule: case_split[case_product case_split[case_product case_split]]) assume nu: "a ≠ (0, 1)" "b ≠ (0, 1)" "c ≠ (0, 1)" have "distinct5 a b c (0, 1) 0" "in5 UNIV a b c (0, 1) 0" using a b c distinct nu by (simp_all add: in_set_inl_nonzero) moreover have "ccw 0 (0, 1) a" "ccw 0 (0, 1) b" "ccw 0 (0, 1) c" by (auto intro!: nlex_ccw_left in_set_inl_lex a b c) ultimately show ?thesis using ab bc by (rule ccw.transitive[where S=UNIV and s="(0, 1)"]) next assume "a ≠ (0, 1)" "b = (0, 1)" "c ≠ (0, 1)" thus ?thesis using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left a b ab by blast next assume "a ≠ (0, 1)" "b ≠ (0, 1)" "c = (0, 1)" thus ?thesis using ccw_switch23 in_set_inl_lex inl_ncoll nlex_ccw_left b c bc by blast qed (auto simp add: nlex_ccw_left in_set_inl_lex) qed lemma sorted_inl: "ccw.sortedP 0 (ccw.selsort 0 (inl (snd X)))" by (rule ccw0.sortedP_selsort) auto lemma sorted_scaled_inl: "ccw.sortedP 0 (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X))))" using sorted_inl by (rule ccw_sorted_scaleR) simp lemma distinct_selsort_inl: "distinct (ccw.selsort 0 (inl (snd X)))" by simp lemma distinct_map_scaleRI: fixes xs::"'a::real_vector list" shows "distinct xs ⟹ c ≠ 0 ⟹ distinct (map ((*⇩_{R}) c) xs)" by (induct xs) auto lemma distinct_scaled_inl: "distinct (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X))))" using distinct_selsort_inl by (rule distinct_map_scaleRI) simp lemma ccw'_sortedP_scaled_inl: "ccw'.sortedP 0 (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X))))" using ccw_sorted_implies_ccw'_sortedP by (rule ccw'_sorted_scaleR) (auto simp: sorted_inl inl_ncoll) lemma pdevs_val_pdevs_of_list_inl2E: assumes "e ∈ UNIV → {-1 .. 1}" obtains e' where "pdevs_val e X = pdevs_val e' (pdevs_of_list (inl X))" "e' ∈ UNIV → {-1 .. 1}" proof - let ?l = "map snd (list_of_pdevs (nlex_pdevs X))" have l: "list_all (λx. Counterclockwise_2D_Arbitrary.lex x 0) ?l" "list_all (λx. x ≠ 0) (map snd (list_of_pdevs (nlex_pdevs X)))" by (auto simp: list_all_iff list_of_pdevs_def) from pdevs_val_nlex_pdevs[OF assms(1)] obtain e' where "e' ∈ UNIV → {-1 .. 1}" "pdevs_val e X = pdevs_val e' (nlex_pdevs X)" by auto note this(2) also from pdevs_val_of_list_of_pdevs2[OF ‹e' ∈ _›] obtain e'' where "e'' ∈ UNIV → {-1 .. 1}" "… = pdevs_val e'' (pdevs_of_list ?l)" by metis note this(2) also from pdevs_val_independent_pdevs[OF l ‹e'' ∈ _›] obtain e''' where "e''' ∈ UNIV → {-1 .. 1}" and "… = pdevs_val e''' (pdevs_of_list (independent_pdevs ?l))" by metis note this(2) also have "… = pdevs_val e''' (pdevs_of_list (inl X))" by (simp add: inl_def) finally have "pdevs_val e X = pdevs_val e''' (pdevs_of_list (inl X))" . thus thesis using ‹e''' ∈ _› .. qed lemma pdevs_val_pdevs_of_list_inlE: assumes "e ∈ UNIV → I" "uminus ` I = I" "0 ∈ I" obtains e' where "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e' X" "e' ∈ UNIV → I" proof - let ?l = "map snd (list_of_pdevs (nlex_pdevs X))" have "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e (pdevs_of_list (independent_pdevs ?l))" by (simp add: inl_def) also from pdevs_val_independent_pdevs2[OF ‹e ∈ _›] obtain e' where "pdevs_val e (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e' (pdevs_of_list ?l)" and "e' ∈ UNIV → I" by auto note this(1) also from pdevs_val_of_list_of_pdevs[OF ‹e' ∈ _› ‹0 ∈ I›, of "nlex_pdevs X"] obtain e'' where "pdevs_val e' (pdevs_of_list ?l) = pdevs_val e'' (nlex_pdevs X)" and "e'' ∈ UNIV → I" by metis note this(1) also from pdevs_val_nlex_pdevs2[OF ‹e'' ∈ _› ‹_ = I›] obtain e''' where "pdevs_val e'' (nlex_pdevs X) = pdevs_val e''' X" "e''' ∈ UNIV → I" by metis note this(1) finally have "pdevs_val e (pdevs_of_list (inl X)) = pdevs_val e''' X" . thus ?thesis using ‹e''' ∈ UNIV → I› .. qed lemma sum_list_nlex_eq_sum_list_inl: "sum_list (map snd (list_of_pdevs (nlex_pdevs X))) = sum_list (inl X)" by (auto simp: inl_def sum_list_list_of_pdevs sum_list_independent_pdevs) lemma Affine_inl: "Affine (fst X, pdevs_of_list (inl (snd X))) = Affine X" by (auto simp: Affine_def valuate_def aform_val_def elim: pdevs_val_pdevs_of_list_inlE[of _ _ "snd X"] pdevs_val_pdevs_of_list_inl2E[of _ "snd X"]) subsection ‹Half Segments› definition half_segments_of_aform::"point aform ⇒ (point*point) list" where "half_segments_of_aform X = (let x0 = lowest_vertex (fst X, nlex_pdevs (snd X)) in polychain_of x0 (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X)))))" lemma subsequent_half_segments: fixes X assumes "Suc i < length (half_segments_of_aform X)" shows "snd (half_segments_of_aform X ! i) = fst (half_segments_of_aform X ! Suc i)" using assms by (cases i) (auto simp: half_segments_of_aform_def Let_def polychain_of_subsequent_eq) lemma polychain_half_segments_of_aform: "polychain (half_segments_of_aform X)" by (auto simp: subsequent_half_segments intro!: polychainI) lemma fst_half_segments: "half_segments_of_aform X ≠ [] ⟹ fst (half_segments_of_aform X ! 0) = lowest_vertex (fst X, nlex_pdevs (snd X))" by (auto simp: half_segments_of_aform_def Let_def o_def split_beta') lemma nlex_half_segments_of_aform: "(a, b) ∈ set (half_segments_of_aform X) ⟹ lex b a" by (auto simp: half_segments_of_aform_def prod_eq_iff lex_def dest!: in_set_polychain_ofD in_set_inl_lex) lemma ccw_half_segments_of_aform_all: assumes cd: "(c, d) ∈ set (half_segments_of_aform X)" shows "list_all (λ(xi, xj). ccw xi xj c ∧ ccw xi xj d) (half_segments_of_aform X)" proof - have "list_all (λ(xi, xj). ccw xi xj (fst (c, d)) ∧ ccw xi xj (snd (c, d))) (polychain_of (lowest_vertex (fst X, nlex_pdevs (snd X))) ((map ((*⇩_{R}) 2) (linorder_list0.selsort (ccw 0) (inl (snd X))))))" using ccw'_sortedP_scaled_inl cd[unfolded half_segments_of_aform_def Let_def] by (rule polychain_of_ccw_conjunction) thus ?thesis unfolding half_segments_of_aform_def[unfolded Let_def, symmetric] fst_conv snd_conv . qed lemma ccw_half_segments_of_aform: assumes ij: "(xi, xj) ∈ set (half_segments_of_aform X)" assumes c: "(c, d) ∈ set (half_segments_of_aform X)" shows "ccw xi xj c" "ccw xi xj d" using ccw_half_segments_of_aform_all[OF c] ij by (auto simp add: list_all_iff) lemma half_segments_of_aform1: assumes ch: "x ∈ convex hull set (map fst (half_segments_of_aform X))" assumes ab: "(a, b) ∈ set (half_segments_of_aform X)" shows "ccw a b x" using finite_set _ ch proof (rule ccw.convex_hull) fix c assume "c ∈ set (map fst (half_segments_of_aform X))" then obtain d where "(c, d) ∈ set (half_segments_of_aform X)" by auto with ab show "ccw a b c" by (rule ccw_half_segments_of_aform(1)) qed (insert ab, simp add: nlex_half_segments_of_aform) lemma half_segments_of_aform2: assumes ch: "x ∈ convex hull set (map snd (half_segments_of_aform X))" assumes ab: "(a, b) ∈ set (half_segments_of_aform X)" shows "ccw a b x" using finite_set _ ch proof (rule ccw.convex_hull) fix d assume "d ∈ set (map snd (half_segments_of_aform X))" then obtain c where "(c, d) ∈ set (half_segments_of_aform X)" by auto with ab show "ccw a b d" by (rule ccw_half_segments_of_aform(2)) qed (insert ab, simp add: nlex_half_segments_of_aform) lemma in_set_half_segments_of_aform_aform_valE: assumes "(x2, y2) ∈ set (half_segments_of_aform X)" obtains e where "y2 = aform_val e X" "e ∈ UNIV → {-1 .. 1}" proof - from assms obtain d where "y2 = lowest_vertex (fst X, nlex_pdevs (snd X)) + sum_list (take (Suc d) (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X)))))" by (auto simp: half_segments_of_aform_def elim!: in_set_polychain_of_imp_sum_list) also have "lowest_vertex (fst X, nlex_pdevs (snd X)) = fst X - sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X))))" by (simp add: lowest_vertex_def) also have "sum_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))) = pdevs_val (λ_. 1) (nlex_pdevs (snd X))" by (auto simp: pdevs_val_sum_list) also have "sum_list (take (Suc d) (map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X))))) = pdevs_val (λi. if i ≤ d then 2 else 0) (pdevs_of_list (ccw.selsort 0 (inl (snd X))))" (is "_ = pdevs_val ?e _") by (subst sum_list_take_pdevs_val_eq) (auto simp: pdevs_val_sum if_distrib pdevs_apply_pdevs_of_list degree_pdevs_of_list_scaleR intro!: sum.cong ) also obtain e'' where "… = pdevs_val e'' (pdevs_of_list (inl (snd X)))" "e'' ∈ UNIV → {0..2}" by (auto intro: pdevs_val_selsort_ccw2[of "inl (snd X)" ?e "{0 .. 2}"]) note this(1) also note inl_def also let ?l = "map snd (list_of_pdevs (nlex_pdevs (snd X)))" from pdevs_val_independent_pdevs2[OF ‹e'' ∈ _›] obtain e''' where "pdevs_val e'' (pdevs_of_list (independent_pdevs ?l)) = pdevs_val e''' (pdevs_of_list ?l)" and "e''' ∈ UNIV → {0..2}" by auto note this(1) also have "0 ∈ {0 .. 2::real}" by simp from pdevs_val_of_list_of_pdevs[OF ‹e''' ∈ _› this, of "nlex_pdevs (snd X)"] obtain e'''' where "pdevs_val e''' (pdevs_of_list ?l) = pdevs_val e'''' (nlex_pdevs (snd X))" and "e'''' ∈ UNIV → {0 .. 2}" by metis note this(1) finally have "y2 = fst X + (pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (λ_. 1) (nlex_pdevs (snd X)))" by simp also have "pdevs_val e'''' (nlex_pdevs (snd X)) - pdevs_val (λ_. 1) (nlex_pdevs (snd X)) = pdevs_val (λi. e'''' i - 1) (nlex_pdevs (snd X))" by (simp add: pdevs_val_minus) also have "(λi. e'''' i - 1) ∈ UNIV → {-1 .. 1}" using ‹e'''' ∈ _› by auto from pdevs_val_nlex_pdevs2[OF this] obtain f where "f ∈ UNIV → {-1 .. 1}" and "pdevs_val (λi. e'''' i - 1) (nlex_pdevs (snd X)) = pdevs_val f (snd X)" by auto note this(2) finally have "y2 = aform_val f X" by (simp add: aform_val_def) thus ?thesis using ‹f ∈ _› .. qed lemma fst_hd_half_segments_of_aform: assumes "half_segments_of_aform X ≠ []" shows "fst (hd (half_segments_of_aform X)) = lowest_vertex (fst X, (nlex_pdevs (snd X)))" using assms by (auto simp: half_segments_of_aform_def Let_def fst_hd_polychain_of) lemma "linorder_list0.sortedP (ccw' (lowest_vertex (fst X, nlex_pdevs (snd X)))) (map snd (half_segments_of_aform X))" (is "linorder_list0.sortedP (ccw' ?x0) ?ms") unfolding half_segments_of_aform_def Let_def by (rule ccw'_sortedP_polychain_of_snd) (rule ccw'_sortedP_scaled_inl) lemma rev_zip: "length xs = length ys ⟹ rev (zip xs ys) = zip (rev xs) (rev ys)" by (induct xs ys rule: list_induct2) auto lemma zip_upt_self_aux: "zip [0..<length xs] xs = map (λi. (i, xs ! i)) [0..<length xs]" by (auto intro!: nth_equalityI) lemma half_segments_of_aform_strict: assumes "e ∈ UNIV → {-1 <..< 1}" assumes "seg ∈ set (half_segments_of_aform X)" assumes "length (half_segments_of_aform X) ≠ 1" shows "ccw' (fst seg) (snd seg) (aform_val e X)" using assms unfolding half_segments_of_aform_def Let_def proof - have len: "length (map ((*⇩_{R}) 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))) ≠ 1" using assms by (auto simp: half_segments_of_aform_def) have "aform_val e X = fst X + pdevs_val e (snd X)" by (simp add: aform_val_def) also obtain e' where "e' ∈ UNIV → {-1 <..< 1}" "pdevs_val e (snd X) = pdevs_val e' (nlex_pdevs (snd X))" using pdevs_val_nlex_pdevs[OF ‹e ∈ _›] by auto note this(2) also obtain e'' where "e'' ∈ UNIV → {-1 <..< 1}" "… = pdevs_val e'' (pdevs_of_list (map snd (list_of_pdevs (nlex_pdevs (snd X)))))" by (metis pdevs_val_of_list_of_pdevs2[OF ‹e' ∈ _›]) note this(2) also obtain e''' where "e''' ∈ UNIV → {-1 <..< 1}" "… = pdevs_val e''' (pdevs_of_list (inl (snd X)))" unfolding inl_def using pdevs_val_independent_pdevs_strict[OF list_all_list_of_pdevsI, OF lex_nlex_pdevs list_of_pdevs_all_nonzero ‹e'' ∈ _›] by metis note this(2) also from pdevs_val_selsort_ccw[OF distinct_inl ‹e''' ∈ _›] obtain f where "f ∈ UNIV → {-1 <..< 1}" "… = pdevs_val f (pdevs_of_list (linorder_list0.selsort (ccw 0) (inl (snd X))))" (is "_ = pdevs_val _ (pdevs_of_list ?sl)") by metis note this(2) also have "… = pdevs_val (λi. f i + 1) (pdevs_of_list ?sl) + lowest_vertex (fst X, nlex_pdevs (snd X)) - fst X" proof - have "sum_list (dense_list_of_pdevs (nlex_pdevs (snd X))) = sum_list (dense_list_of_pdevs (pdevs_of_list (ccw.selsort 0 (inl (snd X)))))" by (subst dense_list_of_pdevs_pdevs_of_list) (auto simp: in_set_independent_pdevs_nonzero dense_list_of_pdevs_pdevs_of_list inl_def sum_list_distinct_selsort sum_list_independent_pdevs sum_list_list_of_pdevs) thus ?thesis by (auto simp add: pdevs_val_add lowest_vertex_def algebra_simps pdevs_val_sum_list sum_list_list_of_pdevs in_set_inl_nonzero dense_list_of_pdevs_pdevs_of_list) qed also have "pdevs_val (λi. f i + 1) (pdevs_of_list ?sl) = pdevs_val (λi. 1/2 * (f i + 1)) (pdevs_of_list (map ((*⇩_{R}) 2) ?sl))" (is "_ = pdevs_val ?f' (pdevs_of_list ?ssl)") by (subst pdevs_val_cmul) (simp add: pdevs_of_list_map_scaleR) also have "distinct ?ssl" "?f' ∈ UNIV → {0<..<1}" using ‹f ∈ _› by (auto simp: distinct_map_scaleRI Pi_iff algebra_simps real_0_less_add_iff) from pdevs_of_list_sum[OF this] obtain g where "g ∈ UNIV → {0<..<1}" "pdevs_val ?f' (pdevs_of_list ?ssl) = (∑P∈set ?ssl. g P *⇩_{R}P)" by blast note this(2) finally have "aform_val e X = lowest_vertex (fst X, nlex_pdevs (snd X)) + (∑P∈set ?ssl. g P *⇩_{R}P)" by simp also have "ccw' (fst seg) (snd seg) …" using ‹g ∈ _› _ len ‹seg ∈ _›[unfolded half_segments_of_aform_def Let_def] by (rule in_polychain_of_ccw) (simp add: ccw'_sortedP_scaled_inl) finally show ?thesis . qed lemma half_segments_of_aform_strict_all: assumes "e ∈ UNIV → {-1 <..< 1}" assumes "length (half_segments_of_aform X) ≠ 1" shows "list_all (λseg. ccw' (fst seg) (snd seg) (aform_val e X)) (half_segments_of_aform X)" using assms by (auto intro!: half_segments_of_aform_strict simp: list_all_iff) lemma list_allD: "list_all P xs ⟹ x ∈ set xs ⟹ P x" by (auto simp: list_all_iff) lemma minus_one_less_multI: fixes e x::real shows "- 1 ≤ e ⟹ 0 < x ⟹ x < 1 ⟹ - 1 < e * x" by (metis abs_add_one_gt_zero abs_real_def le_less_trans less_not_sym mult_less_0_iff mult_less_cancel_left1 real_0_less_add_iff) lemma less_one_multI: fixes e x::real shows "e ≤ 1 ⟹ 0 < x ⟹ x < 1 ⟹ e * x < 1" by (metis (erased, opaque_lifting) less_eq_real_def monoid_mult_class.mult.left_neutral mult_strict_mono zero_less_one) lemma ccw_half_segments_of_aform_strictI: assumes "e ∈ UNIV → {-1 <..< 1}" assumes "(s1, s2) ∈ set (half_segments_of_aform X)" assumes "length (half_segments_of_aform X) ≠ 1" assumes "x = (aform_val e X)" shows "ccw' s1 s2 x" using half_segments_of_aform_strict[OF assms(1-3)] assms(4) by simp lemma ccw'_sortedP_subsequent: assumes "Suc i < length xs" "ccw'.sortedP 0 (map dirvec xs)" "fst (xs ! Suc i) = snd (xs ! i)" shows "ccw' (fst (xs ! i)) (snd (xs ! i)) (snd (xs ! Suc i))" using assms proof (induct xs arbitrary: i) case Nil thus ?case by simp next case (Cons x xs) thus ?case by (auto simp: nth_Cons dirvec_minus split: nat.split elim!: ccw'.sortedP_Cons) (metis (no_types, lifting) ccw'.renormalize length_greater_0_conv nth_mem prod.case_eq_if) qed lemma ccw'_sortedP_uminus: "ccw'.sortedP 0 xs ⟹ ccw'.sortedP 0 (map uminus xs)" by (induct xs) (auto intro!: ccw'.sortedP.Cons elim!: ccw'.sortedP_Cons simp del: uminus_Pair) lemma subsequent_half_segments_ccw: fixes X assumes "Suc i < length (half_segments_of_aform X)" shows "ccw' (fst (half_segments_of_aform X ! i)) (snd (half_segments_of_aform X ! i)) (snd (half_segments_of_aform X ! Suc i))" using assms by (intro ccw'_sortedP_subsequent ) (auto simp: subsequent_half_segments half_segments_of_aform_def sorted_inl polychain_of_subsequent_eq intro!: ccw_sorted_implies_ccw'_sortedP[OF inl_ncoll] ccw'_sorted_scaleR) lemma convex_polychain_half_segments_of_aform: "convex_polychain (half_segments_of_aform X)" proof cases assume "length (half_segments_of_aform X) = 1" thus ?thesis by (auto simp: length_Suc_conv convex_polychain_def polychain_def) next assume len: "length (half_segments_of_aform X) ≠ 1" show ?thesis by (rule convex_polychainI) (simp_all add: polychain_half_segments_of_aform subsequent_half_segments_ccw ccw'_def[symmetric]) qed lemma hd_distinct_neq_last: "distinct xs ⟹ length xs > 1 ⟹ hd xs ≠ last xs" by (metis One_nat_def add_Suc_right distinct.simps(2) last.simps last_in_set less_irrefl list.exhaust list.sel(1) list.size(3) list.size(4) add.right_neutral nat_neq_iff not_less0) lemma ccw_hd_last_half_segments_dirvec: assumes "length (half_segments_of_aform X) > 1" shows "ccw' 0 (dirvec (hd (half_segments_of_aform X))) (dirvec (last (half_segments_of_aform X)))" proof - let ?i = "ccw.selsort 0 (inl (snd X))" let ?s = "map ((*⇩_{R}) 2) (ccw.selsort 0 (inl (snd X)))" from assms have l: "1 < length (inl (snd X))" "inl (snd X) ≠ []" using assms by (auto simp add: half_segments_of_aform_def) hence "hd ?i ∈ set ?i" "last ?i ∈ set ?i" by (auto intro!: hd_in_set last_in_set simp del: ccw.set_selsort) hence "¬coll 0 (hd ?i) (last ?i)" using l by (intro inl_ncoll[of _ X]) (auto simp: hd_distinct_neq_last) hence "¬coll 0 (hd ?s) (last ?s)" using l by (auto simp: hd_map last_map) hence "ccw' 0 (hd (map ((*⇩_{R}) 2) (linorder_list0.selsort (ccw 0) (inl (snd X))))) (last (map ((*⇩_{R}) 2) (linorder_list0.selsort (ccw 0) (inl (snd X)))))" using assms by (auto simp add: half_segments_of_aform_def intro!: sorted_inl ccw_sorted_scaleR ccw.hd_last_sorted ccw_ncoll_imp_ccw) with assms show ?thesis by (auto simp add: half_segments_of_aform_def Let_def dirvec_hd_polychain_of dirvec_last_polychain_of length_greater_0_conv[symmetric] simp del: polychain_of.simps length_greater_0_conv split: if_split_asm) qed lemma map_fst_half_segments_aux_eq: "[] ≠ half_segments_of_aform X ⟹ map fst (half_segments_of_aform X) = fst (hd (half_segments_of_aform X))#butlast (map snd (half_segments_of_aform X))" by (rule nth_equalityI) (auto simp: nth_Cons hd_conv_nth nth_butlast subsequent_half_segments split: nat.split) lemma le_less_Suc_eq: "x - Suc 0 ≤ (i::nat) ⟹ i < x ⟹ x - Suc 0 = i" by simp lemma map_snd_half_segments_aux_eq: "half_segments_of_aform X ≠ [] ⟹ map snd (half_segments_of_aform X) = tl (map fst (half_segments_of_aform X)) @ [snd (last (half_segments_of_aform X))]" by (rule nth_equalityI) (auto simp: nth_Cons hd_conv_nth nth_append nth_tl subsequent_half_segments not_less last_conv_nth algebra_simps dest!: le_less_Suc_eq split: nat.split) lemma ccw'_sortedP_snd_half_segments_of_aform: "ccw'.sortedP (lowest_vertex (fst X, nlex_pdevs (snd X))) (map snd (half_segments_of_aform X))" by (auto simp: half_segments_of_aform_def Let_def intro!: ccw'.sortedP.Cons ccw'_sortedP_polychain_of_snd ccw'_sortedP_scaled_inl) lemma lex_half_segments_lowest_vertex: assumes "(c, d) ∈ set (half_segments_of_aform X)" shows "lex d (lowest_vertex (fst X, nlex_pdevs (snd X)))" unfolding half_segments_of_aform_def Let_def by (rule lex_polychain_of_center[OF assms[unfolded half_segments_of_aform_def Let_def], unfolded snd_conv]) (auto simp: list_all_iff lex_def dest!: in_set_inl_lex) lemma lex_half_segments_lowest_vertex': assumes "d ∈ set (map snd (half_segments_of_aform X))" shows "lex d (lowest_vertex (fst X, nlex_pdevs (snd X)))" using assms by (auto intro: lex_half_segments_lowest_vertex) lemma lex_half_segments_last: assumes "(c, d) ∈ set (half_segments_of_aform X)" shows "lex (snd (last (half_segments_of_aform X))) d" using assms unfolding half_segments_of_aform_def Let_def by (rule lex_polychain_of_last) (auto simp: list_all_iff lex_def dest!: in_set_inl_lex) lemma lex_half_segments_last': assumes "d ∈ set (map snd (half_segments_of_aform X))" shows "lex (snd (last (half_segments_of_aform X))) d" using assms by (auto intro: lex_half_segments_last) lemma ccw'_half_segments_lowest_last: assumes set_butlast: "(c, d) ∈ set (butlast (half_segments_of_aform X))" assumes ne: "inl (snd X) ≠ []" shows "ccw' (lowest_vertex (fst X, nlex_pdevs (snd X))) d (snd (last (half_segments_of_aform X)))" using set_butlast unfolding half_segments_of_aform_def Let_def by (rule ccw'_polychain_of_sorted_center_last) (auto simp: ne ccw'_sortedP_scaled_inl) lemma distinct_fst_half_segments: "distinct (map fst (half_segments_of_aform X))" by (auto simp: half_segments_of_aform_def list_all_iff lex_scale1_zero simp del: scaleR_Pair intro!: distinct_fst_polychain_of dest: in_set_inl_nonzero in_set_inl_lex) lemma distinct_snd_half_segments: "distinct (map snd (half_segments_of_aform X)