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
      by(auto simp add: smult_smult_assoc)
    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

lemma cone_add_cone:
  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