# Theory Cone

```section ‹Cones›

text ‹We define the notions like cone, polyhedral cone, etc. and prove some basic facts about them.›

theory Cone
imports
Basis_Extension
Missing_VS_Connect
Integral_Bounded_Vectors
begin

context gram_schmidt
begin

definition "nonneg_lincomb c Vs b = (lincomb c Vs = b ∧ c ` Vs ⊆ {x. x ≥ 0})"
definition "nonneg_lincomb_list c Vs b = (lincomb_list c Vs = b ∧ (∀ i < length Vs. c i ≥ 0))"

definition finite_cone :: "'a vec set ⇒ 'a vec set" where
"finite_cone Vs = ({ b. ∃ c. nonneg_lincomb c (if finite Vs then Vs else {}) b})"

definition cone :: "'a vec set ⇒ 'a vec set" where
"cone Vs = ({ x. ∃ Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws})"

definition cone_list :: "'a vec list ⇒ 'a vec set" where
"cone_list Vs = {b. ∃c. nonneg_lincomb_list c Vs b}"

lemma finite_cone_iff_cone_list: assumes Vs: "Vs ⊆ carrier_vec n"
and id: "Vs = set Vsl"
shows "finite_cone Vs = cone_list Vsl"
proof -
have fin: "finite Vs" unfolding id by auto
from Vs id have Vsl: "set Vsl ⊆ carrier_vec n" by auto
{
fix c b
assume b: "lincomb c Vs = b" and c: "c ` Vs ⊆ {x. x ≥ 0}"
from lincomb_as_lincomb_list[OF Vsl, of c]
have b: "lincomb_list (λi. if ∃j<i. Vsl ! i = Vsl ! j then 0 else c (Vsl ! i)) Vsl = b"
unfolding b[symmetric] id by simp
have "∃ c. nonneg_lincomb_list c Vsl b"
unfolding nonneg_lincomb_list_def
apply (intro exI conjI, rule b)
by (insert c, auto simp: set_conv_nth id)
}
moreover
{
fix c b
assume b: "lincomb_list c Vsl = b" and c: "(∀ i < length Vsl. c i ≥ 0)"
have "nonneg_lincomb (mk_coeff Vsl c) Vs b"
unfolding b[symmetric] nonneg_lincomb_def
apply (subst lincomb_list_as_lincomb[OF Vsl])
by (insert c, auto simp: id mk_coeff_def intro!: sum_list_nonneg)
hence "∃ c. nonneg_lincomb c Vs b" by blast
}
ultimately show ?thesis unfolding finite_cone_def cone_list_def
nonneg_lincomb_def nonneg_lincomb_list_def using fin by auto
qed

lemma cone_alt_def: assumes Vs: "Vs ⊆ carrier_vec n"
shows "cone Vs = ({ x. ∃ Ws. set Ws ⊆ Vs ∧ x ∈ cone_list Ws})"
unfolding cone_def
proof (intro Collect_cong iffI)
fix x
assume "∃Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws"
then obtain Ws where *: "finite Ws" "Ws ⊆ Vs" "x ∈ finite_cone Ws" by auto
from finite_list[OF *(1)] obtain Wsl where id: "Ws = set Wsl" by auto
from finite_cone_iff_cone_list[OF _ this] *(2-3) Vs
have "x ∈ cone_list Wsl" by auto
with *(2) id show "∃Wsl. set Wsl ⊆ Vs ∧ x ∈ cone_list Wsl" by blast
next
fix x
assume "∃Wsl. set Wsl ⊆ Vs ∧ x ∈ cone_list Wsl"
then obtain Wsl where "set Wsl ⊆ Vs" "x ∈ cone_list Wsl" by auto
thus "∃Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws" using Vs
by (intro exI[of _ "set Wsl"], subst finite_cone_iff_cone_list, auto)
qed

lemma cone_mono: "Vs ⊆ Ws ⟹ cone Vs ⊆ cone Ws"
unfolding cone_def by blast

lemma finite_cone_mono: assumes fin: "finite Ws"
and Ws: "Ws ⊆ carrier_vec n"
and sub: "Vs ⊆ Ws"
shows "finite_cone Vs ⊆ finite_cone Ws"
proof
fix b
assume "b ∈ finite_cone Vs"
then obtain c where b: "b = lincomb c Vs" and c: "c ` Vs ⊆ {x. x ≥ 0}"
unfolding finite_cone_def nonneg_lincomb_def using finite_subset[OF sub fin] by auto
define d where "d = (λ v. if v ∈ Vs then c v else 0)"
from c have d: "d ` Ws ⊆ {x. x ≥ 0}" unfolding d_def by auto
have "lincomb d Ws = lincomb d (Ws - Vs) + lincomb d Vs"
by (rule lincomb_vec_diff_add[OF Ws sub fin], auto)
also have "lincomb d Vs = lincomb c Vs"
by (rule lincomb_cong, insert Ws sub, auto simp: d_def)
also have "lincomb d (Ws - Vs) = 0⇩v n"
by (rule lincomb_zero, insert Ws sub, auto simp: d_def)
also have "0⇩v n + lincomb c Vs = lincomb c Vs" using Ws sub by auto
also have "… = b" unfolding b by simp
finally
have "b = lincomb d Ws" by auto
then show "b ∈ finite_cone Ws" using d fin
unfolding finite_cone_def nonneg_lincomb_def by auto
qed

lemma finite_cone_carrier: "A ⊆ carrier_vec n ⟹ finite_cone A ⊆ carrier_vec n"
unfolding finite_cone_def nonneg_lincomb_def by auto

lemma cone_carrier: "A ⊆ carrier_vec n ⟹ cone A ⊆ carrier_vec n"
using finite_cone_carrier unfolding cone_def by blast

lemma cone_iff_finite_cone: assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
shows "cone A = finite_cone A"
proof
show "finite_cone A ⊆ cone A" unfolding cone_def using fin by auto
show "cone A ⊆ finite_cone A" unfolding cone_def using fin finite_cone_mono[OF fin A] by auto
qed

lemma set_in_finite_cone:
assumes Vs: "Vs ⊆ carrier_vec n"
and fin: "finite Vs"
shows "Vs ⊆ finite_cone Vs"
proof
fix x
assume x: "x ∈ Vs"
show "x ∈ finite_cone Vs" unfolding finite_cone_def
proof
let ?c = "λ y. if x = y then 1 else 0 :: 'a"
have Vsx: "Vs - {x} ⊆ carrier_vec n" using Vs by auto
have "lincomb ?c Vs = x + lincomb ?c (Vs - {x})"
using lincomb_del2 x Vs fin by auto
also have "lincomb ?c (Vs - {x}) = 0⇩v n" using lincomb_zero Vsx by auto
also have "x + 0⇩v n = x " using M.r_zero Vs x by auto
finally have "lincomb ?c Vs = x" by auto
moreover have "?c ` Vs ⊆ {z. z ≥ 0}" by auto
ultimately show "∃c. nonneg_lincomb c (if finite Vs then Vs else {}) x"
unfolding nonneg_lincomb_def
using fin by auto
qed
qed

lemma set_in_cone:
assumes Vs: "Vs ⊆ carrier_vec n"
shows "Vs ⊆ cone Vs"
proof
fix x
assume x: "x ∈ Vs"
show "x ∈ cone Vs" unfolding cone_def
proof (intro CollectI exI)
have "x ∈ carrier_vec n" using Vs x by auto
then have "x ∈ finite_cone {x}" using set_in_finite_cone by auto
then show "finite {x} ∧ {x} ⊆ Vs ∧ x ∈ finite_cone {x}" using x by auto
qed
qed

lemma zero_in_finite_cone:
assumes Vs: "Vs ⊆ carrier_vec n"
shows "0⇩v n ∈ finite_cone Vs"
proof -
let ?Vs = "(if finite Vs then Vs else {})"
have "lincomb (λ x. 0 :: 'a) ?Vs = 0⇩v n" using lincomb_zero Vs by auto
moreover have "(λ x. 0 :: 'a) ` ?Vs ⊆ {y. y ≥ 0}" by auto
ultimately show ?thesis unfolding finite_cone_def nonneg_lincomb_def by blast
qed

lemma lincomb_in_finite_cone:
assumes "x = lincomb l W"
and "finite W"
and "∀i ∈ W . l i ≥ 0"
and "W ⊆ carrier_vec n"
shows "x ∈ finite_cone W"
using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto

lemma lincomb_in_cone:
assumes "x = lincomb l W"
and "finite W"
and "∀i ∈ W . l i ≥ 0"
and "W ⊆ carrier_vec n"
shows "x ∈ cone W"
using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto

lemma zero_in_cone: "0⇩v n ∈ cone Vs"
proof -
have "finite {}" by auto
moreover have "{} ⊆ cone Vs" by auto
moreover have "0⇩v n ∈ finite_cone {}" using zero_in_finite_cone by auto
ultimately show ?thesis unfolding cone_def by blast
qed

lemma cone_smult:
assumes a: "a ≥ 0"
and Vs: "Vs ⊆ carrier_vec n"
and x: "x ∈ cone Vs"
shows "a ⋅⇩v x ∈ cone Vs"
proof -
from x Vs obtain Ws c where Ws: "Ws ⊆ Vs" and fin: "finite Ws" and
"nonneg_lincomb c Ws x"
unfolding cone_def finite_cone_def by auto
then have "nonneg_lincomb (λ w. a * c w) Ws (a ⋅⇩v x)"
unfolding nonneg_lincomb_def using a lincomb_distrib Vs by auto
then show ?thesis using Ws fin unfolding cone_def finite_cone_def by auto
qed

lemma finite_cone_empty[simp]: "finite_cone {} = {0⇩v n}"
by (auto simp: finite_cone_def nonneg_lincomb_def)

lemma cone_empty[simp]: "cone {} = {0⇩v n}"
unfolding cone_def by simp

lemma cone_elem_sum:
assumes Vs: "Vs ⊆ carrier_vec n"
and x: "x ∈ cone Vs"
and y: "y ∈ cone Vs"
shows "x + y ∈ cone Vs"
proof -
obtain Xs where Xs: "Xs ⊆ Vs" and fin_Xs: "finite Xs"
and Xs_cone: "x ∈ finite_cone Xs"
using Vs x unfolding cone_def by auto
obtain Ys where Ys: "Ys ⊆ Vs" and fin_Ys: "finite Ys"
and Ys_cone: "y ∈ finite_cone Ys"
using Vs y unfolding cone_def
by auto
have "x ∈ finite_cone (Xs ∪ Ys)" and "y ∈ finite_cone (Xs ∪ Ys)"
using finite_cone_mono fin_Xs fin_Ys Xs Ys Vs Xs_cone Ys_cone
by (blast, blast)
then obtain cx cy where "nonneg_lincomb cx (Xs ∪ Ys) x"
and "nonneg_lincomb cy (Xs ∪ Ys) y"
unfolding finite_cone_def using fin_Xs fin_Ys by auto
hence "nonneg_lincomb (λ v. cx v + cy v) (Xs ∪ Ys) (x + y)"
unfolding nonneg_lincomb_def
using lincomb_sum[of "Xs ∪ Ys" cx cy] fin_Xs fin_Ys Xs Ys Vs
by fastforce
hence "x + y ∈ finite_cone (Xs ∪ Ys)"
unfolding finite_cone_def using fin_Xs fin_Ys by auto
thus ?thesis unfolding cone_def using fin_Xs fin_Ys Xs Ys by auto
qed

lemma cone_cone:
assumes Vs: "Vs ⊆ carrier_vec n"
shows "cone (cone Vs) = cone Vs"
proof
show "cone Vs ⊆ cone (cone Vs)"
by (rule set_in_cone[OF cone_carrier[OF Vs]])
next
show "cone (cone Vs) ⊆ cone Vs"
proof
fix x
assume x: "x ∈ cone (cone Vs)"
then obtain Ws c where Ws: "set Ws ⊆ cone Vs"
and c: "nonneg_lincomb_list c Ws x"
using cone_alt_def Vs cone_carrier unfolding cone_list_def by auto

have "set Ws ⊆ cone Vs ⟹ nonneg_lincomb_list c Ws x ⟹ x ∈ cone Vs"
proof (induction Ws arbitrary: x c)
case Nil
hence "x = 0⇩v n" unfolding nonneg_lincomb_list_def by auto
thus "x ∈ cone Vs" using zero_in_cone by auto
next
case (Cons a Ws)
have "a ∈ cone Vs" using Cons.prems(1) by auto
moreover have "c 0 ≥ 0"
using Cons.prems(2) unfolding nonneg_lincomb_list_def by fastforce
ultimately have "c 0 ⋅⇩v a ∈ cone Vs" using cone_smult Vs by auto
moreover have "lincomb_list (c ∘ Suc) Ws ∈ cone Vs"
using Cons unfolding nonneg_lincomb_list_def by fastforce
moreover have "x = c 0 ⋅⇩v a + lincomb_list (c ∘ Suc) Ws"
using Cons.prems(2) unfolding nonneg_lincomb_list_def
by auto
ultimately show "x ∈ cone Vs" using cone_elem_sum Vs by auto
qed

thus "x ∈ cone Vs" using Ws c by auto
qed
qed

lemma cone_smult_basis:
assumes Vs: "Vs ⊆ carrier_vec n"
and l: "l ` Vs ⊆ {x. x > 0}"
shows "cone {l v ⋅⇩v v | v . v ∈ Vs} = cone Vs"
proof
have "{l v ⋅⇩v v |v. v ∈ Vs} ⊆ cone Vs"
proof
fix x
assume "x ∈ {l v ⋅⇩v v | v. v ∈ Vs}"
then obtain v where "v ∈ Vs" and "x = l v ⋅⇩v v" by auto
thus "x ∈ cone Vs" using
set_in_cone[OF Vs] cone_smult[OF _ Vs, of "l v" v] l by fastforce
qed
thus "cone {l v ⋅⇩v v | v. v ∈ Vs} ⊆ cone Vs"
using cone_mono cone_cone[OF Vs] by blast
next
have lVs: "{l v ⋅⇩v v | v. v ∈ Vs} ⊆ carrier_vec n" using Vs by auto
have "Vs ⊆ cone {l v ⋅⇩v v | v. v ∈ Vs}"
proof
fix v assume v: "v ∈ Vs"
hence "l v ⋅⇩v v ∈ cone {l v ⋅⇩v v | v. v ∈ Vs}" using set_in_cone[OF lVs] by auto
moreover have "1 / l v > 0" using l v by auto
ultimately have "(1 / l v) ⋅⇩v (l v ⋅⇩v v) ∈ cone {l v ⋅⇩v v | v. v ∈ Vs}"
using cone_smult[OF _ lVs] by auto
also have "(1 / l v) ⋅⇩v (l v ⋅⇩v v) = v" using l v
finally show "v ∈ cone {l v ⋅⇩v v | v. v ∈ Vs}" by auto
qed
thus "cone Vs ⊆ cone {l v ⋅⇩v v | v. v ∈ Vs}"
using cone_mono cone_cone[OF lVs] by blast
qed

assumes C: "C ⊆ carrier_vec n"
shows "cone C + cone C = cone C"
proof
note CC = cone_carrier[OF C]
have "cone C = cone C + {0⇩v n}" by (subst add_0_right_vecset[OF CC], simp)
also have "… ⊆ cone C + cone C"
by (rule set_plus_mono2, insert zero_in_cone, auto)
finally show "cone C ⊆ cone C + cone C" by auto
from cone_elem_sum[OF C]
show "cone C + cone C ⊆ cone C"
by (auto elim!: set_plus_elim)
qed

lemma orthogonal_cone:
assumes X: "X ⊆ carrier_vec n"
and W: "W ⊆ carrier_vec n"
and finX: "finite X"
and spanLW: "span (set Ls ∪ W) = carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ set Ls ⟹ w ∙ x = 0"
and WWs: "W = set Ws"
and spanL: "span (set Ls) = span X"
and LX: "set Ls ⊆ X"
and lin_Ls_Bs: "lin_indpt_list (Ls @ Bs)"
and len_Ls_Bs: "length (Ls @ Bs) = n"
shows "cone (X ∪ set Bs) ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X"
"⋀ x. ∀w∈W. w ∙ x = 0 ⟹ Z ⊆ X ⟹ B ⊆ set Bs ⟹ x = lincomb c (Z ∪ B)
⟹ x = lincomb c (Z - B)"
proof -
from WWs have finW: "finite W" by auto
define Y where "Y = X ∪ set Bs"
from lin_Ls_Bs[unfolded lin_indpt_list_def] have
Ls: "set Ls ⊆ carrier_vec n" and
Bs: "set Bs ⊆ carrier_vec n" and
distLsBs: "distinct (Ls @ Bs)" and
lin: "lin_indpt (set (Ls @ Bs))"  by auto
have LW: "set Ls ∩ W = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain x where xX: "x ∈ set Ls" and xW: "x ∈ W" by auto
from ortho[OF xW xX] have "x ∙ x = 0" by auto
hence "sq_norm x = 0" by (auto simp: sq_norm_vec_as_cscalar_prod)
with vs_zero_lin_dep[OF _ lin] xX Ls Bs show False by auto
qed
have Y: "Y ⊆ carrier_vec n" using X Bs unfolding Y_def by auto
have CLB: "carrier_vec n = span (set (Ls @ Bs))"
using lin_Ls_Bs len_Ls_Bs lin_indpt_list_length_eq_n by blast
also have "… ⊆ span Y"
by (rule span_is_monotone, insert LX, auto simp: Y_def)
finally have span: "span Y = carrier_vec n" using Y by auto
have finY: "finite Y" using finX finW unfolding Y_def by auto
{
fix x Z B d
assume xX: "∀w∈W. w ∙ x = 0" and ZX: "Z ⊆ X" and B: "B ⊆ set Bs" and
xd: "x = lincomb d (Z ∪ B)"
from ZX B X Bs have ZB: "Z ∪ B ⊆ carrier_vec n" by auto
with xd have x: "x ∈ carrier_vec n" by auto
from xX W have w0: "w ∈ W ⟹ w ∙ x = 0" for w by auto
from finite_in_span[OF _ _ x[folded spanLW]] Ls X W finW finX
obtain c where xc: "x = lincomb c (set Ls ∪ W)" by auto
have "x = lincomb c (set Ls ∪ W)" unfolding xc by auto
also have "… = lincomb c (set Ls) + lincomb c W"
by (rule lincomb_union, insert X LX W LW finW, auto)
finally have xsum: "x = lincomb c (set Ls) + lincomb c W" .
{
fix w
assume wW: "w ∈ W"
with W have w: "w ∈ carrier_vec n" by auto
from w0[OF wW, unfolded xsum]
have "0 = w ∙ (lincomb c (set Ls) + lincomb c W)" by simp
also have "… = w ∙ lincomb c (set Ls) + w ∙ lincomb c W"
by (rule scalar_prod_add_distrib[OF w], insert Ls W, auto)
also have "w ∙ lincomb c (set Ls) = 0" using ortho[OF wW]
by (subst lincomb_scalar_prod_right[OF Ls w], auto)
finally have "w ∙ lincomb c W = 0" by simp
}
hence "lincomb c W ∙ lincomb c W = 0" using W
by (subst lincomb_scalar_prod_left, auto)
hence "sq_norm (lincomb c W) = 0"
by (auto simp: sq_norm_vec_as_cscalar_prod)
hence 0: "lincomb c W = 0⇩v n" using lincomb_closed[OF W, of c] by simp
have xc: "x = lincomb c (set Ls)" unfolding xsum 0 using Ls by auto
hence xL: "x ∈ span (set Ls)" by auto
let ?X = "Z - B"
have "lincomb d ?X ∈ span X" using finite_subset[OF _ finX, of ?X] X ZX by auto
from finite_in_span[OF finite_set Ls this[folded spanL]]
obtain e where ed: "lincomb e (set Ls) = lincomb d ?X" by auto
from B finite_subset[OF B] have finB: "finite B" by auto
from B Bs have BC: "B ⊆ carrier_vec n" by auto
define f where "f =
(λ x. if x ∈ set Bs then if x ∈ B then d x else 0 else if x ∈ set Ls then e x else undefined)"
have "x = lincomb d (?X ∪ B)" unfolding xd by auto
also have "… = lincomb d ?X + lincomb d B"
by (rule lincomb_union[OF _ _ _ finite_subset[OF _ finX]], insert ZX X finB B Bs, auto)
finally have xd: "x = lincomb d ?X + lincomb d B" .
also have "… = lincomb e (set Ls) + lincomb d B" unfolding ed by auto
also have "lincomb e (set Ls) = lincomb f (set Ls)"
by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: f_def)
also have "lincomb d B = lincomb f B"
by (rule lincomb_cong[OF _ BC], insert B, auto simp: f_def)
also have "lincomb f B = lincomb f (B ∪ (set Bs - B))"
by (subst lincomb_clean, insert finB Bs B, auto simp: f_def)
also have "B ∪ (set Bs - B) = set Bs" using B by auto
finally have "x = lincomb f (set Ls) + lincomb f (set Bs)" by auto
also have "lincomb f (set Ls) + lincomb f (set Bs) = lincomb f (set (Ls @ Bs))"
by (subst lincomb_union[symmetric], insert Ls distLsBs Bs, auto)
finally have "x = lincomb f (set (Ls @ Bs))" .
hence f: "f ∈ set (Ls @ Bs) →⇩E UNIV ∧ lincomb f (set (Ls @ Bs)) = x"
by (auto simp: f_def split: if_splits)
from finite_in_span[OF finite_set Ls xL] obtain g where
xg: "x = lincomb g (set Ls)" by auto
define h where "h = (λ x. if x ∈ set Bs then 0 else if x ∈ set Ls then g x else undefined)"
have "x = lincomb h (set Ls)" unfolding xg
by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: h_def)
also have "… = lincomb h (set Ls) + 0⇩v n" using Ls by auto
also have "0⇩v n = lincomb h (set Bs)"
by (rule lincomb_zero[symmetric, OF Bs], auto simp: h_def)
also have "lincomb h (set Ls) + lincomb h (set Bs) = lincomb h (set (Ls @ Bs))"
by (subst lincomb_union[symmetric], insert Ls Bs distLsBs, auto)
finally have "x = lincomb h (set (Ls @ Bs))" .
hence h: "h ∈ set (Ls @ Bs) →⇩E UNIV ∧ lincomb h (set (Ls @ Bs)) = x"
by (auto simp: h_def split: if_splits)
have basis: "basis (set (Ls @ Bs))" using lin_Ls_Bs[unfolded lin_indpt_list_def] len_Ls_Bs
using CLB basis_def by blast
from Ls Bs have "set (Ls @ Bs) ⊆ carrier_vec n" by auto
from basis[unfolded basis_criterion[OF finite_set this], rule_format, OF x] f h
have fh: "f = h" by auto
hence "⋀ x. x ∈ set Bs ⟹ f x = 0" unfolding h_def by auto
hence "⋀ x. x ∈ B ⟹ d x = 0" unfolding f_def using B by force
thus "x = lincomb d ?X" unfolding xd
by (subst (2) lincomb_zero, insert BC ZB X, auto intro!: M.r_zero)
} note main = this
have "cone Y ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X" (is "?I = _")
proof
{
fix x
assume xX: "x ∈ cone X"
with cone_carrier[OF X] have x: "x ∈ carrier_vec n" by auto
have "X ⊆ Y" unfolding Y_def by auto
from cone_mono[OF this] xX have xY: "x ∈ cone Y" by auto
from cone_iff_finite_cone[OF X finX] xX have "x ∈ finite_cone X" by auto
from this[unfolded finite_cone_def nonneg_lincomb_def] finX obtain c
where "x = lincomb c X" by auto
with finX X have "x ∈ span X" by auto
with spanL have "x ∈ span (set Ls)" by auto
from finite_in_span[OF _ Ls this] obtain c where
xc: "x = lincomb c (set Ls)" by auto
{
fix w
assume wW: "w ∈ W"
hence w: "w ∈ carrier_vec n" using W by auto
have "w ∙ x = 0" unfolding xc using ortho[OF wW]
by (subst lincomb_scalar_prod_right[OF Ls w], auto)
}
with xY x have "x ∈ ?I" by blast
}
thus "cone X ⊆ ?I" by blast
{
fix x
let ?X = "X - set Bs"
assume "x ∈ ?I"
with cone_carrier[OF Y] cone_iff_finite_cone[OF Y finY]
have xY: "x ∈ finite_cone Y" and x: "x ∈ carrier_vec n"
and w0: "⋀ w. w ∈ W ⟹ w ∙ x = 0" by auto
from xY[unfolded finite_cone_def nonneg_lincomb_def] finY obtain d
where xd: "x = lincomb d Y" and nonneg: "d ` Y ⊆ Collect ((≤) 0)" by auto
from main[OF _ _ _ xd[unfolded Y_def]] w0
have "x = lincomb d ?X" by auto
hence "nonneg_lincomb d ?X x" unfolding nonneg_lincomb_def
using nonneg[unfolded Y_def] by auto
hence "x ∈ finite_cone ?X" using finX
unfolding finite_cone_def by auto
hence "x ∈ cone X" using finite_subset[OF _ finX, of ?X] unfolding cone_def by blast
}
then show "?I ⊆ cone X" by auto
qed
thus "cone (X ∪ set Bs) ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X" unfolding Y_def .
qed

definition "polyhedral_cone (A :: 'a mat) = { x . x ∈ carrier_vec n ∧ A *⇩v x ≤ 0⇩v (dim_row A)}"

lemma polyhedral_cone_carrier: assumes "A ∈ carrier_mat nr n"
shows "polyhedral_cone A ⊆ carrier_vec n"
using assms unfolding polyhedral_cone_def by auto

lemma cone_in_polyhedral_cone:
assumes CA: "C ⊆ polyhedral_cone A"
and A: "A ∈ carrier_mat nr n"
shows "cone C ⊆ polyhedral_cone A"
proof
interpret nr: gram_schmidt nr "TYPE ('a)".
from polyhedral_cone_carrier[OF A] assms(1)
have C: "C ⊆ carrier_vec n" by auto
fix x
assume x: "x ∈ cone C"
then have xn: "x ∈ carrier_vec n"
using cone_carrier[OF C] by auto
from x[unfolded cone_alt_def[OF C] cone_list_def nonneg_lincomb_list_def]
obtain ll Ds where l0: "lincomb_list ll Ds = x" and l1: "∀i<length Ds. 0 ≤ ll i"
and DsC: "set Ds ⊆ C"
by auto
from DsC C have Ds: "set Ds ⊆ carrier_vec n" by auto

have "A *⇩v x = A *⇩v (lincomb_list ll Ds)" using l0 by auto
also have "… = nr.lincomb_list ll (map (λ d. A *⇩v d) Ds)"
proof -
have one: " ∀w∈set Ds. dim_vec w = n" using DsC C by auto
have two: "∀w∈set (map ((*⇩v) A) Ds). dim_vec w = nr" using A DsC C by auto
show "A *⇩v lincomb_list ll Ds = nr.lincomb_list ll (map ((*⇩v) A) Ds)"
unfolding lincomb_list_as_mat_mult[OF one] nr.lincomb_list_as_mat_mult[OF two] length_map
proof (subst assoc_mult_mat_vec[symmetric, OF A], force+, rule arg_cong[of _ _ "λ x. x *⇩v _"])
show "A * mat_of_cols n Ds = mat_of_cols nr (map ((*⇩v) A) Ds)"
unfolding mat_of_cols_def
by (intro eq_matI, insert A Ds[unfolded set_conv_nth],
(force intro!: arg_cong[of _ _ "λ x. row A _ ∙ x"])+)
qed
qed
also have "… ≤ 0⇩v nr"
proof (intro lesseq_vecI[of _ nr])
have *: "set (map ((*⇩v) A) Ds) ⊆ carrier_vec nr" using A Ds by auto
show Carr: "nr.lincomb_list ll (map ((*⇩v) A) Ds) ∈ carrier_vec nr"
by (intro nr.lincomb_list_carrier[OF *])
fix i
assume i: "i < nr"
from CA[unfolded polyhedral_cone_def] A
have l2: "x ∈ C ⟹ A *⇩v x ≤ 0⇩v nr" for x by auto
show "nr.lincomb_list ll (map ((*⇩v) A) Ds) \$ i ≤ 0⇩v nr \$ i"
unfolding subst nr.lincomb_list_index[OF i *] length_map index_zero_vec(1)[OF i]
proof (intro sum_nonpos mult_nonneg_nonpos)
fix j
assume "j ∈ {0..<length Ds}"
hence j: "j < length Ds" by auto
from j show "0 ≤ ll j" using l1 by auto
from j have "Ds ! j ∈ C" using DsC by auto
from l2[OF this] have l2: "A *⇩v Ds ! j ≤ 0⇩v nr" by auto
from lesseq_vecD[OF _ this i] i have "(A *⇩v Ds ! j) \$ i ≤ 0" by auto
thus "map ((*⇩v) A) Ds ! j \$ i ≤ 0" using j i by auto
qed
qed auto
finally show "x ∈ polyhedral_cone A"
unfolding polyhedral_cone_def using A xn by auto
qed

lemma bounded_cone_is_zero:
assumes Ccarr: "C ⊆ carrier_vec n" and bnd: "cone C ⊆ Bounded_vec bnd"
shows "cone C = {0⇩v n}"
proof(rule ccontr)
assume "¬ ?thesis"
then obtain v where vC: "v ∈ cone C" and vnz: "v ≠ 0⇩v n"
using zero_in_cone assms by auto
have vcarr: "v ∈ carrier_vec n" using vC Ccarr cone_carrier by blast
from vnz vcarr obtain i where i_le_n: "i < dim_vec v" and vinz: "v \$ i ≠ 0" by force
define M where "M = (1 / (v \$ i) * (bnd + 1))"
have abs_ge_bnd: "abs (M * (v \$ i)) > bnd" unfolding M_def by (simp add: vinz)
have aMvC: "(abs M) ⋅⇩v v ∈ cone C" using cone_smult[OF _ Ccarr vC] abs_ge_bnd by simp
have "¬(abs (abs M * (v \$ i)) ≤ bnd)" using abs_ge_bnd by simp
hence "(abs M) ⋅⇩v v ∉ Bounded_vec bnd" unfolding Bounded_vec_def using i_le_n aMvC by auto
thus False using aMvC bnd by auto
qed

lemma cone_of_cols: fixes A :: "'a mat" and b :: "'a vec"
assumes A: "A ∈ carrier_mat n nr" and b: "b ∈ carrier_vec n"
shows "b ∈ cone (set (cols A)) ⟷ (∃ x. x ≥ 0⇩v nr ∧ A *⇩v x = b)"
proof -
let ?C = "set (cols A)"
from A have C: "?C ⊆ carrier_vec n" and C': " ∀w∈set (cols A). dim_vec w = n"
unfolding cols_def by auto
have id: "finite ?C = True" "length (cols A) = nr" using A by auto
have Aid: "mat_of_cols n (cols A) = A" using A unfolding mat_of_cols_def
by (intro eq_matI, auto)
show ?thesis
unfolding cone_iff_finite_cone[OF C finite_set] finite_cone_iff_cone_list[OF C refl]
unfolding cone_list_def nonneg_lincomb_list_def mem_Collect_eq id
unfolding lincomb_list_as_mat_mult[OF C'] id Aid
proof -
{
fix x
assume "x≥0⇩v nr" "A *⇩v x = b"
hence "∃c. A *⇩v vec nr c = b ∧ (∀i<nr. 0 ≤ c i)" using A b
by (intro exI[of _ "λ i. x \$ i"], auto simp: less_eq_vec_def intro!: arg_cong[of _ _ "(*⇩v) A"])
}
moreover
{
fix c
assume "A *⇩v vec nr c = b" "(∀i<nr. 0 ≤ c i)"
hence "∃ x. x≥0⇩v nr ∧ A *⇩v x = b"
by (intro exI[of _ "vec nr c"], auto simp: less_eq_vec_def)
}
ultimately show "(∃c. A *⇩v vec nr c = b ∧ (∀i<nr. 0 ≤ c i)) = (∃x≥0⇩v nr. A *⇩v x = b)" by blast
qed
qed

end
end```