Theory Decomposition_Theorem

section ‹The Decomposition Theorem›

text ‹This theory contains a proof of the fact, that every polyhedron can be decomposed
  into a convex hull of a finite set of points + a finitely generated cone, including bounds
  on the numbers that are required in the decomposition.
  We further prove the inverse direction of this theorem (without bounds) and
  as a corollary, we derive that a polyhedron is bounded iff it is the convex hull
  of finitely many points, i.e., a polytope.›

theory Decomposition_Theorem
  imports
    Farkas_Minkowsky_Weyl
    Convex_Hull
begin

context gram_schmidt
begin

definition "polytope P = (∃ V. V ⊆ carrier_vec n ∧ finite V ∧ P = convex_hull V)"

definition "polyhedron A b = {x ∈ carrier_vec n. A *⇩v x ≤ b}"

lemma polyhedra_are_convex:
  assumes A: "A ∈ carrier_mat nr n"
    and b: "b ∈ carrier_vec nr"
    and P: "P = polyhedron A b"
  shows "convex P"
proof (intro convexI)
  show Pcarr: "P ⊆ carrier_vec n" using assms unfolding polyhedron_def by auto
  fix a :: 'a and x y
  assume xy: "x ∈ P" "y ∈ P" and a: "0 ≤ a" "a ≤ 1"
  from xy[unfolded P polyhedron_def]
  have x: "x ∈ carrier_vec n" and y: "y ∈ carrier_vec n" and le: "A *⇩v x ≤ b" "A *⇩v y ≤ b" by auto
  show "a ⋅⇩v x + (1 - a) ⋅⇩v y ∈ P" unfolding P polyhedron_def
  proof (intro CollectI conjI)
    from x have ax: "a ⋅⇩v x ∈ carrier_vec n" by auto
    from y have ay: "(1 - a) ⋅⇩v y ∈ carrier_vec n" by auto
    show "a ⋅⇩v x + (1 - a) ⋅⇩v y ∈ carrier_vec n" using ax ay by auto
    show "A *⇩v (a ⋅⇩v x + (1 - a) ⋅⇩v y) ≤ b"
    proof (intro lesseq_vecI[OF _ b])
      show "A *⇩v (a ⋅⇩v x + (1 - a) ⋅⇩v y) ∈ carrier_vec nr" using A x y by auto
      fix i
      assume i: "i < nr"
      from lesseq_vecD[OF b le(1) i] lesseq_vecD[OF b le(2) i]
      have le: "(A *⇩v x) $ i ≤ b $ i" "(A *⇩v y) $ i ≤ b $ i" by auto
      have "(A *⇩v (a ⋅⇩v x + (1 - a) ⋅⇩v y)) $ i = a * (A *⇩v x) $ i + (1 - a) * (A *⇩v y) $ i"
        using A x y i by (auto simp: scalar_prod_add_distrib[of _ n])
      also have "… ≤ a * b $ i + (1 - a) * b $ i"
        by (rule add_mono; rule mult_left_mono, insert le a, auto)
      also have "… = b $ i" by (auto simp: field_simps)
      finally show "(A *⇩v (a ⋅⇩v x + (1 - a) ⋅⇩v y)) $ i ≤ b $ i" .
    qed
  qed
qed

end



locale gram_schmidt_m = n: gram_schmidt n f_ty + m: gram_schmidt m f_ty
  for n m :: nat and f_ty
begin

lemma vec_first_lincomb_list:
  assumes Xs: "set Xs ⊆ carrier_vec n"
    and nm: "m ≤ n"
  shows "vec_first (n.lincomb_list c Xs) m =
       m.lincomb_list c (map (λ v. vec_first v m) Xs)"
  using Xs
proof (induction Xs arbitrary: c)
  case Nil
  show ?case by (simp add: nm)
next
  case (Cons x Xs)
  from Cons.prems have x: "x ∈ carrier_vec n" and Xs: "set Xs ⊆ carrier_vec n" by auto

  have "vec_first (n.lincomb_list c (x # Xs)) m =
          vec_first (c 0 ⋅⇩v x + n.lincomb_list (c ∘ Suc) Xs) m" by auto
  also have "… = vec_first (c 0 ⋅⇩v x) m + vec_first (n.lincomb_list (c ∘ Suc) Xs) m"
    using vec_first_add[of m "c 0 ⋅⇩v x"] x n.lincomb_list_carrier[OF Xs, of "c ∘ Suc"] nm
    by simp
  also have "vec_first (c 0 ⋅⇩v x) m = c 0 ⋅⇩v vec_first x m"
    using vec_first_smult[OF nm, of x "c 0"] Cons.prems by auto
  also have "vec_first (n.lincomb_list (c ∘ Suc) Xs) m =
               m.lincomb_list (c ∘ Suc) (map (λ v. vec_first v m) Xs)"
    using Cons by simp
  also have "c 0 ⋅⇩v vec_first x m + … =
               m.lincomb_list c (map (λ v. vec_first v m) (x # Xs))"
    by simp
  finally show ?case by auto
qed

lemma convex_hull_next_dim:
  assumes "n = m + 1"
    and X: "X ⊆ carrier_vec n"
    and "finite X"
    and Xm1: "∀ y ∈ X. y $ m = 1"
    and y_dim: "y ∈ carrier_vec n"
    and y: "y $ m = 1"
  shows "(vec_first y m ∈ m.convex_hull {vec_first y m | y. y ∈ X}) = (y ∈ n.cone X)"
proof -
  from ‹finite X› obtain Xs where Xs: "X = set Xs" using finite_list by auto
  let ?Y = "{vec_first y m | y. y ∈ X}"
  let ?Ys = "map (λ y. vec_first y m) Xs"
  have Ys: "?Y = set ?Ys" using Xs by auto

  define x where "x = vec_first y m"
  {
    have "y = vec_first y m @⇩v vec_last y 1"
      using ‹n = m + 1› vec_first_last_append y_dim by auto
    also have "vec_last y 1 = vec_of_scal (vec_last y 1 $ 0)"
      using vec_of_scal_dim_1[of "vec_last y 1"] by simp
    also have "vec_last y 1 $ 0 = y $ m"
      using y_dim ‹n = m + 1› vec_last_index[of y m 1 0] by auto
    finally have "y = x @⇩v vec_of_scal 1" unfolding x_def using y by simp
  } note xy = this
  {
    assume "y ∈ n.cone X"
    then obtain c where x: "n.nonneg_lincomb c X y"
      using n.cone_iff_finite_cone[OF X] ‹finite X›
      unfolding n.finite_cone_def by auto

    have "1 = y $ m" by (simp add: y)
    also have "y = n.lincomb c X"
      using x unfolding n.nonneg_lincomb_def by simp
    also have "… $ m = (∑x∈X. c x * x $ m)"
      using n.lincomb_index[OF _ X] ‹n = m + 1› by simp
    also have "… = sum c X"
      by (rule n.R.finsum_restrict, auto, rule restrict_ext, simp add: Xm1)
    finally have "y ∈ n.convex_hull X"
      unfolding n.convex_hull_def n.convex_lincomb_def
      using ‹finite X› x by auto
  }
  moreover have "n.convex_hull X ⊆ n.cone X"
    unfolding n.convex_hull_def n.convex_lincomb_def n.finite_cone_def n.cone_def
    using ‹finite X› by auto
  moreover have "n.convex_hull X = n.convex_hull_list Xs"
    by (rule n.finite_convex_hull_iff_convex_hull_list[OF X Xs])
  moreover {
    assume "y ∈ n.convex_hull_list Xs"
    then obtain c where c: "n.lincomb_list c Xs = y"
      and c0: "∀ i < length Xs. c i ≥ 0" and c1: "sum c {0..<length Xs} = 1"
      unfolding n.convex_hull_list_def n.convex_lincomb_list_def
        n.nonneg_lincomb_list_def by fast
    have "m.lincomb_list c ?Ys = vec_first y m"
      using c vec_first_lincomb_list[of Xs c] X Xs ‹n = m + 1› by simp
    hence "x ∈ m.convex_hull_list ?Ys"
      unfolding m.convex_hull_list_def m.convex_lincomb_list_def
        m.nonneg_lincomb_list_def
      using x_def c0 c1 x_def by auto
  } moreover {
    assume "x ∈ m.convex_hull_list ?Ys"
    then obtain c where x: "m.lincomb_list c ?Ys = x"
      and c0: "∀ i < length Xs. c i ≥ 0"
      and c1: "sum c {0..<length Xs} = 1"
      unfolding m.convex_hull_list_def m.convex_lincomb_list_def
        m.nonneg_lincomb_list_def by auto

    have "n.lincomb_list c Xs $ m = (∑j = 0..<length Xs. c j * Xs ! j $ m)"
      using n.lincomb_list_index[of m Xs c] ‹n = m + 1› Xs X by fastforce
    also have "… = sum c {0..<length Xs}"
      apply(rule n.R.finsum_restrict, auto, rule restrict_ext)
      by (simp add: Xm1 Xs)
    also have "… = 1" by (rule c1)
    finally have "vec_last (n.lincomb_list c Xs) 1 $ 0 = 1"
      using vec_of_scal_dim_1 vec_last_index[of "n.lincomb_list c Xs" m 1 0]
        n.lincomb_list_carrier Xs X ‹n = m + 1› by simp
    hence "vec_last (n.lincomb_list c Xs) 1 = vec_of_scal 1"
      using vec_of_scal_dim_1 by auto

    moreover have "vec_first (n.lincomb_list c Xs) m = x"
      using vec_first_lincomb_list ‹n = m + 1› Xs X x by auto

    moreover have "n.lincomb_list c Xs =
                   vec_first (n.lincomb_list c Xs) m @⇩v vec_last (n.lincomb_list c Xs) 1"
      using vec_first_last_append Xs X n.lincomb_list_carrier ‹n = m + 1› by auto

    ultimately have "n.lincomb_list c Xs = y" using xy by simp

    hence "y ∈ n.convex_hull_list Xs"
      unfolding n.convex_hull_list_def n.convex_lincomb_list_def
        n.nonneg_lincomb_list_def using c0 c1 by blast
  }
  moreover have "m.convex_hull ?Y = m.convex_hull_list ?Ys"
    using m.finite_convex_hull_iff_convex_hull_list[OF _ Ys] by fastforce
  ultimately show ?thesis unfolding x_def by blast
qed

lemma cone_next_dim:
  assumes "n = m + 1"
    and X: "X ⊆ carrier_vec n"
    and "finite X"
    and Xm0: "∀ y ∈ X. y $ m = 0"
    and y_dim: "y ∈ carrier_vec n"
    and y: "y $ m = 0"
  shows "(vec_first y m ∈ m.cone {vec_first y m | y. y ∈ X}) = (y ∈ n.cone X)"
proof -
  from ‹finite X› obtain Xs where Xs: "X = set Xs" using finite_list by auto
  let ?Y = "{vec_first y m | y. y ∈ X}"
  let ?Ys = "map (λ y. vec_first y m) Xs"
  have Ys: "?Y = set ?Ys" using Xs by auto

  define x where "x = vec_first y m"
  {
    have "y = vec_first y m @⇩v vec_last y 1"
      using ‹n = m + 1› vec_first_last_append y_dim by auto
    also have "vec_last y 1 = vec_of_scal (vec_last y 1 $ 0)"
      using vec_of_scal_dim_1[of "vec_last y 1"] by simp
    also have "vec_last y 1 $ 0 = y $ m"
      using y_dim ‹n = m + 1› vec_last_index[of y m 1 0] by auto
    finally have "y = x @⇩v vec_of_scal 0" unfolding x_def using y by simp
  } note xy = this

  have "n.cone X = n.cone_list Xs"
    using n.cone_iff_finite_cone[OF X ‹finite X›] n.finite_cone_iff_cone_list[OF X Xs]
    by simp
  moreover {
    assume "y ∈ n.cone_list Xs"
    then obtain c where y: "n.lincomb_list c Xs = y" and c: "∀ i < length Xs. c i ≥ 0"
      unfolding n.cone_list_def n.nonneg_lincomb_list_def by blast
    from y have "m.lincomb_list c ?Ys = x"
      unfolding x_def
      using vec_first_lincomb_list Xs X ‹n = m + 1› by auto
    hence "x ∈ m.cone_list ?Ys" using c
      unfolding m.cone_list_def m.nonneg_lincomb_list_def by auto
  } moreover {
    assume "x ∈ m.cone_list ?Ys"
    then obtain c where x: "m.lincomb_list c ?Ys = x" and c: "∀ i < length Xs. c i ≥ 0"
      unfolding m.cone_list_def m.nonneg_lincomb_list_def by auto

    have "vec_last (n.lincomb_list c Xs) 1 $ 0 = n.lincomb_list c Xs $ m"
      using ‹n = m + 1› n.lincomb_list_carrier X Xs vec_last_index[of _ m 1 0]
      by auto
    also have "… = 0"
      using n.lincomb_list_index[of m Xs c] Xs X ‹n = m + 1› Xm0 by simp
    also have "… = vec_last y 1 $ 0"
      using y y_dim ‹n = m + 1› vec_last_index[of y m 1 0] by auto
    finally have "vec_last (n.lincomb_list c Xs) 1 = vec_last y 1" by fastforce

    moreover have "vec_first (n.lincomb_list c Xs) m = x"
      using vec_first_lincomb_list[of Xs c] x X Xs ‹n = m + 1›
      unfolding x_def by simp

    ultimately have "n.lincomb_list c Xs = y" unfolding x_def
      using vec_first_last_append[of _ m 1] ‹n = m + 1› y_dim
        n.lincomb_list_carrier[of Xs c] Xs X
      by metis
    hence "y ∈ n.cone_list Xs"
      unfolding n.cone_list_def n.nonneg_lincomb_list_def using c by blast
  }
  moreover have "m.cone_list ?Ys = m.cone ?Y"
    using m.finite_cone_iff_cone_list[OF _ Ys] m.cone_iff_finite_cone[of ?Y]
      ‹finite X› by force
  ultimately show ?thesis unfolding x_def by blast
qed

end

context gram_schmidt
begin

lemma decomposition_theorem_polyhedra_1:
  assumes A: "A ∈ carrier_mat nr n"
    and b: "b ∈ carrier_vec nr"
    and P: "P = polyhedron A b"
  shows "∃ Q X. X ⊆ carrier_vec n ∧ finite X ∧
    Q ⊆ carrier_vec n ∧ finite Q ∧
    P = convex_hull Q + cone X ∧
    (is_det_bound db ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (of_int Bnd) ⟶ b ∈ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ⟶
      X ⊆ ℤ⇩v ∩ Bounded_vec (of_int (db n (max 1 Bnd)))
    ∧ Q ⊆ Bounded_vec (of_int (db n (max 1 Bnd))))"
proof -
  let ?oi = "of_int :: int ⇒ 'a" 

  interpret next_dim: gram_schmidt "n + 1" "TYPE ('a)".
  interpret gram_schmidt_m "n + 1" n "TYPE('a)".

  from P[unfolded polyhedron_def] have "P ⊆ carrier_vec n" by auto

  have mcb: "mat_of_col (-b) ∈ carrier_mat nr 1" using b by auto
  define M where "M = (A @⇩c mat_of_col (-b)) @⇩r (0⇩m 1 n @⇩c -1⇩m 1)"
  have M_top: "A @⇩c mat_of_col (- b) ∈ carrier_mat nr (n + 1)"
    by (rule carrier_append_cols[OF A mcb])
  have M_bottom: "(0⇩m 1 n @⇩c -1⇩m 1) ∈ carrier_mat 1 (n + 1)"
    by (rule carrier_append_cols, auto)
  have M_dim: "M ∈ carrier_mat (nr + 1) (n + 1)"
    unfolding M_def
    by (rule carrier_append_rows[OF M_top M_bottom])

  {
    fix x :: "'a vec" fix t assume x: "x ∈ carrier_vec n"
    have "x @⇩v vec_of_scal t ∈ next_dim.polyhedral_cone M =
          (A *⇩v x - t ⋅⇩v b ≤ 0⇩v nr ∧ t ≥ 0)"
    proof -
      let ?y = "x @⇩v vec_of_scal t"
      have y: "?y ∈ carrier_vec (n + 1)" using x by(simp del: One_nat_def)
      have "?y ∈ next_dim.polyhedral_cone M =
            (M *⇩v ?y ≤ 0⇩v (nr + 1))"
        unfolding next_dim.polyhedral_cone_def using y M_dim by auto
      also have "0⇩v (nr + 1) = 0⇩v nr @⇩v 0⇩v 1" by auto
      also have "M *⇩v ?y ≤ 0⇩v nr @⇩v 0⇩v 1 =
                   ((A @⇩c mat_of_col (-b)) *⇩v ?y ≤ 0⇩v nr ∧
                   (0⇩m 1 n @⇩c -1⇩m 1) *⇩v ?y ≤ 0⇩v 1)"
        unfolding M_def
        by (intro append_rows_le[OF M_top M_bottom _ y], auto)
      also have "(A @⇩c mat_of_col(-b)) *⇩v ?y =
                 A *⇩v x + mat_of_col(-b) *⇩v vec_of_scal t"
        by (rule mat_mult_append_cols[OF A _ x],
            auto simp add: b simp del: One_nat_def)
      also have "mat_of_col(-b) *⇩v vec_of_scal t = t ⋅⇩v (-b)"
        by(rule mult_mat_of_row_vec_of_scal)
      also have "A *⇩v x + t ⋅⇩v (-b) = A *⇩v x - t ⋅⇩v b" by auto
      also have "(0⇩m 1 n @⇩c - 1⇩m 1) *⇩v (x @⇩v vec_of_scal t) =
                 0⇩m 1 n *⇩v x + - 1⇩m 1 *⇩v vec_of_scal t"
        by(rule mat_mult_append_cols, auto simp add: x simp del: One_nat_def)
      also have "… = - vec_of_scal t" using x by (auto simp del: One_nat_def)
      also have "(… ≤ 0⇩v 1) = (t ≥ 0)" unfolding less_eq_vec_def by auto
      finally show "(?y ∈ next_dim.polyhedral_cone M) =
                    (A *⇩v x - t ⋅⇩v b ≤ 0⇩v nr ∧ t ≥ 0)" by auto
    qed
  } note M_cone_car = this
  from next_dim.farkas_minkowsky_weyl_theorem_2[OF M_dim, of db "max 1 Bnd"]
  obtain X where X: "next_dim.polyhedral_cone M = next_dim.cone X" and
    fin_X: "finite X" and X_carrier: "X ⊆ carrier_vec (n+1)"
    and Bnd: "is_det_bound db ⟹ M ∈ ℤ⇩m ∩ Bounded_mat (?oi (max 1 Bnd)) ⟹
          X ⊆ ℤ⇩v ∩ Bounded_vec (?oi (db n (max 1 Bnd)))"
    by auto
  let ?f = "λ x. if x $ n = 0 then 1 else 1 / (x $ n)"
  define Y where "Y = {?f x ⋅⇩v x | x. x ∈ X}"
  have "finite Y" unfolding Y_def using fin_X by auto
  have Y_carrier: "Y ⊆ carrier_vec (n+1)" unfolding Y_def using X_carrier by auto
  have "?f ` X ⊆ {y. y > 0}"
  proof
    fix y
    assume "y ∈ ?f ` X"
    then obtain x where x: "x ∈ X" and y: "y = ?f x" by auto
    show "y ∈ {y. y > 0}"
    proof cases
      assume "x $ n = 0"
      thus "y ∈ {y. y > 0}" using y by auto
    next
      assume P: "x $ n ≠ 0"
      have "x = vec_first x n @⇩v vec_last x 1"
        using x X_carrier vec_first_last_append by auto
      also have "vec_last x 1 = vec_of_scal (vec_last x 1 $ 0)" by auto
      also have "vec_last x 1 $ 0 = x $ n"
        using x X_carrier unfolding vec_last_def by auto
      finally have "x = vec_first x n @⇩v vec_of_scal (x $ n)" by auto
      moreover have "x ∈ next_dim.polyhedral_cone M"
        using x X X_carrier next_dim.set_in_cone by auto
      ultimately have "x $ n ≥ 0" using M_cone_car vec_first_carrier by metis
      hence "x $ n > 0" using P by auto
      thus "y ∈ {y. y > 0}" using y by auto
    qed
  qed
  hence Y: "next_dim.cone Y = next_dim.polyhedral_cone M" unfolding Y_def
    using next_dim.cone_smult_basis[OF X_carrier] X by auto
  define Y0 where "Y0 = {v ∈ Y. v $ n = 0}"
  define Y1 where "Y1 = Y - Y0"
  have Y0_carrier: "Y0 ⊆ carrier_vec (n + 1)" and Y1_carrier: "Y1 ⊆ carrier_vec (n + 1)"
    unfolding Y0_def Y1_def using Y_carrier by auto
  have "finite Y0" and "finite Y1"
    unfolding Y0_def Y1_def using ‹finite Y› by auto

  have Y1: "⋀ y. y ∈ Y1 ⟹ y $ n = 1"
  proof -
    fix y assume y: "y ∈ Y1"
    hence "y ∈ Y" unfolding Y1_def by auto
    then obtain x where "x ∈ X" and x: "y = ?f x ⋅⇩v x" unfolding Y_def by auto
    then have "x $ n ≠ 0" using x y Y1_def Y0_def by auto
    then have "y = 1 / (x $ n) ⋅⇩v x" using x by auto
    then have "y $ n = 1 / (x $ n) * x $ n" using X_carrier ‹x ∈ X› by auto
    thus "y $ n = 1" using ‹x $ n ≠ 0› by auto
  qed

  let ?Z0 = "{vec_first y n | y. y ∈ Y0}"
  let ?Z1 = "{vec_first y n | y. y ∈ Y1}"
  show ?thesis
  proof (intro exI conjI impI)
    show "?Z0 ⊆ carrier_vec n" by auto
    show "?Z1 ⊆ carrier_vec n" by auto
    show "finite ?Z0" using ‹finite Y0› by auto
    show "finite ?Z1" using ‹finite Y1› by auto
    show "P = convex_hull ?Z1 + cone ?Z0"
    proof -
      {
        fix x
        assume "x ∈ P"
        hence xn: "x ∈ carrier_vec n" and "A *⇩v x ≤ b"
          using P unfolding polyhedron_def by auto
        hence "A *⇩v x - 1 ⋅⇩v b ≤ 0⇩v nr"
          using vec_le_iff_diff_le_0 A b carrier_vecD mult_mat_vec_carrier one_smult_vec
          by metis
        hence "x @⇩v vec_of_scal 1 ∈ next_dim.polyhedral_cone M"
          using M_cone_car[OF xn] by auto
        hence "x @⇩v vec_of_scal 1 ∈ next_dim.cone Y" using Y by auto
        hence "x @⇩v vec_of_scal 1 ∈ next_dim.finite_cone Y"
          using next_dim.cone_iff_finite_cone[OF Y_carrier ‹finite Y›] by auto
        then obtain c where c: "next_dim.nonneg_lincomb c Y (x @⇩v vec_of_scal 1)"
          unfolding next_dim.finite_cone_def using ‹finite Y› by auto
        let ?y = "next_dim.lincomb c Y1"
        let ?z = "next_dim.lincomb c Y0"
        have y_dim: "?y ∈ carrier_vec (n + 1)" and z_dim: "?z ∈ carrier_vec (n + 1)"
          unfolding next_dim.nonneg_lincomb_def
          using Y0_carrier Y1_carrier next_dim.lincomb_closed by simp_all
        hence yz_dim: "?y + ?z ∈ carrier_vec (n + 1)" by auto
        have "x @⇩v vec_of_scal 1 = next_dim.lincomb c Y"
          using c unfolding next_dim.nonneg_lincomb_def by auto
        also have "Y = Y1 ∪ Y0" unfolding Y1_def using Y0_def by blast
        also have "next_dim.lincomb c (Y1 ∪ Y0) = ?y + ?z"
          using next_dim.lincomb_union2[of Y1 Y0]
            ‹finite Y0› ‹finite Y› Y0_carrier Y_carrier
          unfolding Y1_def by fastforce
        also have "?y + ?z = vec_first (?y + ?z) n @⇩v vec_last (?y + ?z) 1"
          using vec_first_last_append[of "?y + ?z" n 1] add_carrier_vec yz_dim
          by simp
        also have "vec_last (?y + ?z) 1 = vec_of_scal ((?y + ?z) $ n)"
          using vec_of_scal_dim_1 vec_last_index[OF yz_dim, of 0] by auto
        finally have "x @⇩v vec_of_scal 1 =
                     vec_first (?y + ?z) n @⇩v vec_of_scal ((?y + ?z) $ n)" by auto
        hence "x = vec_first (?y + ?z) n" and
          yz_last: "vec_of_scal 1 = vec_of_scal ((?y + ?z) $ n)"
          using append_vec_eq yz_dim xn by auto
        hence xyz: "x = vec_first ?y n + vec_first ?z n"
          using vec_first_add[of n ?y ?z] y_dim z_dim by simp

        have "1 = ((?y + ?z) $ n)" using yz_last index_vec_of_scal
          by (metis (no_types, lifting))
        hence "1 = ?y $ n + ?z $ n" using y_dim z_dim by auto
        moreover have zn0: "?z $ n = 0"
          using next_dim.lincomb_index[OF _ Y0_carrier] Y0_def by auto
        ultimately have yn1: "1 = ?y $ n" by auto
        have "next_dim.nonneg_lincomb c Y1 ?y"
          using c Y1_def
          unfolding next_dim.nonneg_lincomb_def by auto
        hence "?y ∈ next_dim.cone Y1"
          using next_dim.cone_iff_finite_cone[OF Y1_carrier] ‹finite Y1›
          unfolding next_dim.finite_cone_def by auto
        hence y: "vec_first ?y n ∈ convex_hull ?Z1"
          using convex_hull_next_dim[OF _ Y1_carrier ‹finite Y1› _ y_dim] Y1 yn1
          by simp

        have "next_dim.nonneg_lincomb c Y0 ?z" using c Y0_def
          unfolding next_dim.nonneg_lincomb_def by blast
        hence "?z ∈ next_dim.cone Y0"
          using ‹finite Y0› next_dim.cone_iff_finite_cone[OF Y0_carrier ‹finite Y0›]
          unfolding next_dim.finite_cone_def
          by fastforce
        hence z: "vec_first ?z n ∈ cone ?Z0"
          using cone_next_dim[OF _ Y0_carrier ‹finite Y0› _ _ zn0] Y0_def
            next_dim.lincomb_closed[OF Y0_carrier] by blast

        from xyz y z have "x ∈ convex_hull ?Z1 + cone ?Z0" by blast
      } moreover {
        fix x
        assume "x ∈ convex_hull ?Z1 + cone ?Z0"
        then obtain y z where "x = y + z" and y: "y ∈ convex_hull ?Z1"
          and z: "z ∈ cone ?Z0" by (auto elim: set_plus_elim)

        have yn: "y ∈ carrier_vec n"
          using y convex_hull_carrier[OF ‹?Z1 ⊆ carrier_vec n›] by blast
        hence "y @⇩v vec_of_scal 1 ∈ carrier_vec (n + 1)"
          using vec_of_scal_dim(2) by fast
        moreover have "vec_first (y @⇩v vec_of_scal 1) n ∈ convex_hull ?Z1"
          using vec_first_append[OF yn] y by auto
        moreover have "(y @⇩v vec_of_scal 1) $ n = 1" using yn by simp
        ultimately have "y @⇩v vec_of_scal 1 ∈ next_dim.cone Y1"
          using convex_hull_next_dim[OF _ Y1_carrier ‹finite Y1›] Y1 by blast
        hence y_cone: "y @⇩v vec_of_scal 1 ∈ next_dim.cone Y"
          using next_dim.cone_mono[of Y1 Y] Y1_def by blast

        have zn: "z ∈ carrier_vec n" using z cone_carrier[of ?Z0] by fastforce
        hence "z @⇩v vec_of_scal 0 ∈ carrier_vec (n + 1)"
          using vec_of_scal_dim(2) by fast
        moreover have "vec_first (z @⇩v vec_of_scal 0) n ∈ cone ?Z0"
          using vec_first_append[OF zn] z by auto
        moreover have "(z @⇩v vec_of_scal 0) $ n = 0" using zn by simp
        ultimately have "z @⇩v vec_of_scal 0 ∈ next_dim.cone Y0"
          using cone_next_dim[OF _ Y0_carrier ‹finite Y0›] Y0_def by blast
        hence z_cone: "z @⇩v vec_of_scal 0 ∈ next_dim.cone Y"
          using Y0_def next_dim.cone_mono[of Y0 Y] by blast

        have xn: "x ∈ carrier_vec n" using ‹x = y + z› yn zn by blast
        have "x @⇩v vec_of_scal 1 = (y @⇩v vec_of_scal 1) + (z @⇩v vec_of_scal 0)"
          using ‹x = y + z› append_vec_add[OF yn zn]
          unfolding vec_of_scal_def by auto
        hence "x @⇩v vec_of_scal 1 ∈ next_dim.cone Y"
          using next_dim.cone_elem_sum[OF Y_carrier y_cone z_cone] by simp
        hence "A *⇩v x - b ≤ 0⇩v nr" using M_cone_car[OF xn] Y by simp
        hence "A *⇩v x ≤ b" using vec_le_iff_diff_le_0[of "A *⇩v x" b]
            dim_mult_mat_vec[of A x] A by simp
        hence "x ∈ P" using P xn unfolding polyhedron_def by blast
      }
      ultimately show "P = convex_hull ?Z1 + cone ?Z0" by blast
    qed

    let ?Bnd = "db n (max 1 Bnd)"
    assume "A ∈ ℤ⇩m ∩ Bounded_mat (?oi Bnd)"
      "b ∈ ℤ⇩v ∩ Bounded_vec (?oi Bnd)"
      and db: "is_det_bound db" 
    hence *: "A ∈ ℤ⇩m" "A ∈ Bounded_mat (?oi Bnd)" "b ∈ ℤ⇩v" "b ∈ Bounded_vec (?oi Bnd)" by auto
    have "elements_mat M ⊆ elements_mat A ∪ vec_set (-b) ∪ {0,-1}"
      unfolding M_def
      unfolding elements_mat_append_rows[OF M_top M_bottom]
      unfolding elements_mat_append_cols[OF A mcb]
      by (subst elements_mat_append_cols, auto)
    also have "… ⊆ ℤ ∩ ({x. abs x ≤ ?oi Bnd} ∪ {0,-1})"
      using *[unfolded Bounded_mat_elements_mat Ints_mat_elements_mat
          Bounded_vec_vec_set Ints_vec_vec_set] by auto
    also have "… ⊆ ℤ ∩ ({x. abs x ≤ ?oi (max 1 Bnd)})" by (auto simp: of_int_max)
    finally have "M ∈ ℤ⇩m" "M ∈ Bounded_mat (?oi (max 1 Bnd))"
      unfolding Bounded_mat_elements_mat Ints_mat_elements_mat by auto
    hence "M ∈ ℤ⇩m ∩ Bounded_mat (?oi (max 1 Bnd))" by blast
    from Bnd[OF db this]
    have XBnd: "X ⊆ ℤ⇩v ∩ Bounded_vec (?oi ?Bnd)" .
    {
      fix y
      assume y: "y ∈ Y"
      then obtain x where y: "y = ?f x ⋅⇩v x" and xX: "x ∈ X" unfolding Y_def by auto
      with ‹X ⊆ carrier_vec (n+1)› have x: "x ∈ carrier_vec (n+1)" by auto
      from XBnd xX have xI: "x ∈ ℤ⇩v" and xB: "x ∈ Bounded_vec (?oi ?Bnd)" by auto
      {
        assume "y $ n = 0"
        hence "y = x" unfolding y using x by auto
        hence "y ∈ ℤ⇩v ∩ Bounded_vec (?oi ?Bnd)" using xI xB by auto
      } note y0 = this
      {
        assume "y $ n ≠ 0"
        hence x0: "x $ n ≠ 0" using x unfolding y by auto
        from x xI have "x $ n ∈ ℤ" unfolding Ints_vec_def by auto
        with x0 have "abs (x $ n) ≥ 1" by (meson Ints_nonzero_abs_ge1)
        hence abs: "abs (1 / (x $ n)) ≤ 1" by simp
        {
          fix a
          have "abs ((1 / (x $ n)) * a) = abs (1 / (x $ n)) * abs a"
            by simp
          also have "… ≤ 1 * abs a"
            by (rule mult_right_mono[OF abs], auto)
          finally have "abs ((1 / (x $ n)) * a) ≤ abs a" by auto
        } note abs = this
        from x0 have y: "y = (1 / (x $ n)) ⋅⇩v x" unfolding y by auto
        have vy: "vec_set y = (λ a. (1 / (x $ n)) * a) ` vec_set x"
          unfolding y by (auto simp: vec_set_def)
        have "y ∈ Bounded_vec (?oi ?Bnd)" using xB abs
          unfolding Bounded_vec_vec_set vy
          by (smt imageE max.absorb2 max.bounded_iff)
      } note yn0 = this
      note y0 yn0
    } note BndY = this
    from ‹Y ⊆ carrier_vec (n+1)›
    have setvY: "y ∈ Y ⟹ set⇩v (vec_first y n) ⊆ set⇩v y" for y
      unfolding vec_first_def vec_set_def by auto
    from BndY(1) setvY
    show "?Z0 ⊆ ℤ⇩v ∩ Bounded_vec (?oi (db n (max 1 Bnd)))"
      by (force simp: Bounded_vec_vec_set Ints_vec_vec_set Y0_def)
    from BndY(2) setvY
    show "?Z1 ⊆ Bounded_vec (?oi (db n (max 1 Bnd)))"
      by (force simp: Bounded_vec_vec_set Ints_vec_vec_set Y0_def Y1_def)
  qed
qed

lemma decomposition_theorem_polyhedra_2:
  assumes Q: "Q ⊆ carrier_vec n" and fin_Q: "finite Q"
    and X: "X ⊆ carrier_vec n" and fin_X: "finite X"
    and P: "P = convex_hull Q + cone X"
  shows "∃A b nr. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b"
proof -
  interpret next_dim: gram_schmidt "n + 1" "TYPE ('a)".
  interpret gram_schmidt_m "n + 1" n "TYPE('a)".

  from fin_Q obtain Qs where Qs: "Q = set Qs" using finite_list by auto
  from fin_X obtain Xs where Xs: "X = set Xs" using finite_list by auto
  define Y where "Y = {x @⇩v vec_of_scal 1 | x. x ∈ Q}"
  define Z where "Z = {x @⇩v vec_of_scal 0 | x. x ∈ X}"
  have fin_Y: "finite Y" unfolding Y_def using fin_Q by simp
  have fin_Z: "finite Z" unfolding Z_def using fin_X by simp
  have Y_dim: "Y ⊆ carrier_vec (n + 1)"
    unfolding Y_def using Q append_carrier_vec[OF _ vec_of_scal_dim(2)[of 1]]
    by blast
  have Z_dim: "Z ⊆ carrier_vec (n + 1)"
    unfolding Z_def using X append_carrier_vec[OF _ vec_of_scal_dim(2)[of 0]]
    by blast
  have Y_car: "Q = {vec_first x n | x. x ∈ Y}"
  proof (intro equalityI subsetI)
    fix x assume x: "x ∈ Q"
    hence "x @⇩v vec_of_scal 1 ∈ Y" unfolding Y_def by blast
    thus "x ∈ {vec_first x n | x. x ∈ Y}"
      using Q vec_first_append[of x n "vec_of_scal 1"] x by force
  next
    fix x assume "x ∈ {vec_first x n | x. x ∈ Y}"
    then obtain y where "y ∈ Q" and "x = vec_first (y @⇩v vec_of_scal 1) n"
      unfolding Y_def by blast
    thus "x ∈ Q" using Q vec_first_append[of y] by auto
  qed
  have Z_car: "X = {vec_first x n | x. x ∈ Z}"
  proof (intro equalityI subsetI)
    fix x assume x: "x ∈ X"
    hence "x @⇩v vec_of_scal 0 ∈ Z" unfolding Z_def by blast
    thus "x ∈ {vec_first x n | x. x ∈ Z}"
      using X vec_first_append[of x n "vec_of_scal 0"] x by force
  next
    fix x assume "x ∈ {vec_first x n | x. x ∈ Z}"
    then obtain y where "y ∈ X" and "x = vec_first (y @⇩v vec_of_scal 0) n"
      unfolding Z_def by blast
    thus "x ∈ X" using X vec_first_append[of y] by auto
  qed
  have Y_last: "∀ x ∈ Y. x $ n = 1" unfolding Y_def using Q by auto
  have Z_last: "∀ x ∈ Z. x $ n = 0" unfolding Z_def using X by auto

  have "finite (Y ∪ Z)" using fin_Y fin_Z by blast
  moreover have "Y ∪ Z ⊆ carrier_vec (n + 1)" using Y_dim Z_dim by blast
  ultimately obtain B nr
    where B: "next_dim.cone (Y ∪ Z) = next_dim.polyhedral_cone B"
      and B_carrier: "B ∈ carrier_mat nr (n + 1)"
    using next_dim.farkas_minkowsky_weyl_theorem[of "next_dim.cone (Y ∪ Z)"]
    by blast
  define A where "A = mat_col_first B n"
  define b where "b = col B n"
  have B_blocks: "B = A @⇩c mat_of_col b"
    unfolding A_def b_def
    using mat_col_first_last_append[of B n 1] B_carrier
      mat_of_col_dim_col_1[of "mat_col_last B 1"] by auto
  have A_carrier: "A ∈ carrier_mat nr n" unfolding A_def using B_carrier by force
  have b_carrier: "b ∈ carrier_vec nr" unfolding b_def using B_carrier by force

  {
    fix x assume "x ∈ P"
    then obtain y z where x: "x = y + z" and y: "y ∈ convex_hull Q" and z: "z ∈ cone X"
      using P by (auto elim: set_plus_elim)

    have yn: "y ∈ carrier_vec n" using y convex_hull_carrier[OF Q] by blast
    moreover have zn: "z ∈ carrier_vec n" using z cone_carrier[OF X] by blast
    ultimately have xn: "x ∈ carrier_vec n" using x by blast

    have yn1: "y @⇩v vec_of_scal 1 ∈ carrier_vec (n + 1)"
      using append_carrier_vec[OF yn] vec_of_scal_dim by fast
    have y_last: "(y @⇩v vec_of_scal 1) $ n = 1" using yn by force
    have "vec_first (y @⇩v vec_of_scal 1) n = y"
      using vec_first_append[OF yn] by simp
    hence "y @⇩v vec_of_scal 1 ∈ next_dim.cone Y"
      using convex_hull_next_dim[OF _ Y_dim fin_Y Y_last yn1 y_last] Y_car y by argo
    hence y_cone: "y @⇩v vec_of_scal 1 ∈ next_dim.cone (Y ∪ Z)"
      using next_dim.cone_mono[of Y "Y ∪ Z"] by blast

    have zn1: "z @⇩v vec_of_scal 0 ∈ carrier_vec (n + 1)"
      using append_carrier_vec[OF zn] vec_of_scal_dim by fast
    have z_last: "(z @⇩v vec_of_scal 0) $ n = 0" using zn by force
    have "vec_first (z @⇩v vec_of_scal 0) n = z"
      using vec_first_append[OF zn] by simp
    hence "z @⇩v vec_of_scal 0 ∈ next_dim.cone Z"
      using cone_next_dim[OF _ Z_dim fin_Z Z_last zn1 z_last] Z_car z by argo
    hence z_cone: "z @⇩v vec_of_scal 0 ∈ next_dim.cone (Y ∪ Z)"
      using next_dim.cone_mono[of Z "Y ∪ Z"] by blast

    from ‹x = y + z›
    have "x @⇩v vec_of_scal 1 = (y @⇩v vec_of_scal 1) + (z @⇩v vec_of_scal 0)"
      using append_vec_add[OF yn zn] vec_of_scal_dim_1
      unfolding vec_of_scal_def by auto
    hence "x @⇩v vec_of_scal 1 ∈ next_dim.cone (Y ∪ Z) ∧ x ∈ carrier_vec n"
      using next_dim.cone_elem_sum[OF _ y_cone z_cone] Y_dim Z_dim xn by auto
  } moreover {
    fix x assume "x @⇩v vec_of_scal 1 ∈ next_dim.cone (Y ∪ Z)"
    then obtain c where x: "next_dim.lincomb c (Y ∪ Z) = x @⇩v vec_of_scal 1"
      and c: "c ` (Y ∪ Z) ⊆ {t. t ≥ 0}"
      using next_dim.cone_iff_finite_cone Y_dim Z_dim fin_Y fin_Z
      unfolding next_dim.finite_cone_def next_dim.nonneg_lincomb_def by auto

    let ?y = "next_dim.lincomb c Y"
    let ?z = "next_dim.lincomb c Z"
    have xyz: "x @⇩v vec_of_scal 1 = ?y + ?z"
      using x next_dim.lincomb_union[OF Y_dim Z_dim _ fin_Y fin_Z] Y_last Z_last
      by fastforce

    have y_dim: "?y ∈ carrier_vec (n + 1)" using next_dim.lincomb_closed[OF Y_dim]
      by blast
    have z_dim: "?z ∈ carrier_vec (n + 1)" using next_dim.lincomb_closed[OF Z_dim]
      by blast
    have "x @⇩v vec_of_scal 1 ∈ carrier_vec (n + 1)"
      using xyz add_carrier_vec[OF y_dim z_dim] by argo
    hence x_dim: "x ∈ carrier_vec n"
      using carrier_dim_vec[of x n] carrier_dim_vec[of _ "n + 1"]
      by force

    have z_last: "?z $ n = 0" using Z_last next_dim.lincomb_index[OF _ Z_dim, of n]
      by force
    have "?y $ n + ?z $ n = (x @⇩v vec_of_scal 1) $ n"
      using xyz index_add_vec(1) z_dim by simp
    also have "… = 1" using x_dim by auto
    finally have y_last: "?y $ n = 1" using z_last by algebra

    have "?y ∈ next_dim.cone Y"
      using next_dim.cone_iff_finite_cone[OF Y_dim] fin_Y c
      unfolding next_dim.finite_cone_def next_dim.nonneg_lincomb_def by auto
    hence y_cone: "vec_first ?y n ∈ convex_hull Q"
      using convex_hull_next_dim[OF _ Y_dim fin_Y Y_last y_dim y_last] Y_car
      by blast

    have "?z ∈ next_dim.cone Z"
      using next_dim.cone_iff_finite_cone[OF Z_dim] fin_Z c
      unfolding next_dim.finite_cone_def next_dim.nonneg_lincomb_def by auto
    hence z_cone: "vec_first ?z n ∈ cone X"
      using cone_next_dim[OF _ Z_dim fin_Z Z_last z_dim z_last] Z_car
      by blast

    have "x = vec_first (x @⇩v vec_of_scal 1) n" using vec_first_append[OF x_dim] by simp
    also have "… = vec_first ?y n + vec_first ?z n"
      using xyz vec_first_add[of n ?y ?z] y_dim z_dim carrier_dim_vec by auto
    finally have "x ∈ P"
      using y_cone z_cone P by blast
  } moreover {
    fix x :: "'a vec"
    assume xn: "x ∈ carrier_vec n"
    hence "(x @⇩v vec_of_scal 1 ∈ next_dim.polyhedral_cone B) =
          (B *⇩v (x @⇩v vec_of_scal 1) ≤ 0⇩v nr)"
      unfolding next_dim.polyhedral_cone_def using B_carrier
      using append_carrier_vec[OF _ vec_of_scal_dim(2)[of 1]] by auto
    also have "… = ((A @⇩c mat_of_col b) *⇩v (x @⇩v vec_of_scal 1) ≤ 0⇩v nr)"
      using B_blocks by blast
    also have "(A @⇩c mat_of_col b) *⇩v (x @⇩v vec_of_scal 1) =
               A *⇩v x + mat_of_col b *⇩v vec_of_scal 1"
      by (rule mat_mult_append_cols, insert A_carrier b_carrier xn, auto simp del: One_nat_def)
    also have "mat_of_col b *⇩v vec_of_scal 1 = b"
      using mult_mat_of_row_vec_of_scal[of b 1] by simp
    also have "A *⇩v x + b = A *⇩v x - -b" by auto
    finally have "(x @⇩v vec_of_scal 1 ∈ next_dim.polyhedral_cone B) = (A *⇩v x ≤ -b)"
      using vec_le_iff_diff_le_0[of "A *⇩v x" "-b"] A_carrier by simp
  }
  ultimately have "P = polyhedron A (-b)"
    unfolding polyhedron_def using B by blast
  moreover have "-b ∈ carrier_vec nr" using b_carrier by simp
  ultimately show ?thesis using A_carrier by blast
qed

lemma decomposition_theorem_polyhedra:
  "(∃ A b nr. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b) ⟷
   (∃ Q X. Q ∪ X ⊆ carrier_vec n ∧ finite (Q ∪ X) ∧ P = convex_hull Q + cone X)" (is "?l = ?r")
proof
  assume ?l
  then obtain A b nr where A: "A ∈ carrier_mat nr n"
    and b: "b ∈ carrier_vec nr" and P: "P = polyhedron A b" by auto
  from decomposition_theorem_polyhedra_1[OF this] obtain Q X
    where *: "X ⊆ carrier_vec n" "finite X" "Q ⊆ carrier_vec n" "finite Q" "P = convex_hull Q + cone X"
    by meson
  show ?r
    by (rule exI[of _ Q], rule exI[of _ X], insert *, auto simp: polytope_def)
next
  assume ?r
  then obtain Q X where QX_carrier: "Q ∪ X ⊆ carrier_vec n"
    and QX_fin: "finite (Q ∪ X)"
    and P: "P = convex_hull Q + cone X" by blast
  from QX_carrier have Q: "Q ⊆ carrier_vec n" and X: "X ⊆ carrier_vec n" by simp_all
  from QX_fin have fin_Q: "finite Q" and fin_X: "finite X" by simp_all
  show ?l using decomposition_theorem_polyhedra_2[OF Q fin_Q X fin_X P] by blast
qed

lemma polytope_equiv_bounded_polyhedron:
  "polytope P ⟷
  (∃A b nr bnd. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b ∧ P ⊆ Bounded_vec bnd)"
proof
  assume polyP: "polytope P"
  from this obtain Q where Qcarr: "Q ⊆ carrier_vec n" and finQ: "finite Q"
    and PconvhQ: "P = convex_hull Q" unfolding polytope_def by auto
  let ?X = "{}"
  have "convex_hull Q + {0⇩v n} = convex_hull Q" using Qcarr add_0_right_vecset[of "convex_hull Q"]
    by (simp add: convex_hull_carrier)
  hence "P = convex_hull Q + cone ?X" using PconvhQ by simp
  hence "Q ∪ ?X ⊆ carrier_vec n ∧ finite (Q ∪ ?X) ∧ P = convex_hull Q + cone ?X"
    using Qcarr finQ PconvhQ by simp
  hence "∃ A b nr. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b"
    using decomposition_theorem_polyhedra by blast
  hence Ppolyh: "∃A b nr. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b" by blast
  from finite_Bounded_vec_Max[OF Qcarr finQ] obtain bnd where "Q ⊆ Bounded_vec bnd" by auto
  hence Pbnd: "P ⊆ Bounded_vec bnd" using convex_hull_bound PconvhQ Qcarr by auto
  from Ppolyh Pbnd show "∃A b nr bnd. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr
    ∧ P = polyhedron A b ∧ P ⊆ Bounded_vec bnd" by auto
next
  assume "∃A b nr bnd. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b
    ∧ P ⊆ Bounded_vec bnd"
  from this obtain A b nr bnd where Adim: "A ∈ carrier_mat nr n" and bdim: "b ∈ carrier_vec nr"
    and Ppolyh: "P = polyhedron A b" and Pbnd: "P ⊆ Bounded_vec bnd" by auto
  have "∃ A b nr. A ∈ carrier_mat nr n ∧ b ∈ carrier_vec nr ∧ P = polyhedron A b"
    using Adim bdim Ppolyh by blast
  hence "∃ Q X. Q ∪ X ⊆ carrier_vec n ∧ finite (Q ∪ X) ∧ P = convex_hull Q + cone X"
    using decomposition_theorem_polyhedra by simp
  from this obtain Q X where QXcarr: "Q ∪ X ⊆ carrier_vec n"
    and finQX: "finite (Q ∪ X)" and Psum: "P = convex_hull Q + cone X" by auto
  from QXcarr have Qcarr: "convex_hull Q ⊆ carrier_vec n" by (simp add: convex_hull_carrier)
  from QXcarr have Xcarr: "cone X ⊆ carrier_vec n" by (simp add: gram_schmidt.cone_carrier)
  from Pbnd have Pcarr: "P ⊆ carrier_vec n" using Ppolyh unfolding polyhedron_def by simp
  have "P = convex_hull Q"
  proof(cases "Q = {}")
    case True
    then show "P = convex_hull Q" unfolding Psum by (auto simp: set_plus_def)
  next
    case False
    hence convnotempty: "convex_hull Q ≠ {}" using QXcarr by simp
    have Pbndex: "∃bnd. P ⊆ Bounded_vec bnd" using Pbnd
      using QXcarr by auto
    from False have "(∃ bndc. cone X ⊆ Bounded_vec bndc)"
      using bounded_vecset_sum[OF Qcarr Xcarr Psum Pbndex] False convnotempty by blast
    hence "cone X = {0⇩v n}" using bounded_cone_is_zero QXcarr by auto
    thus ?thesis unfolding Psum using Qcarr by (auto simp: add_0_right_vecset)
  qed
  thus "polytope P" using finQX QXcarr unfolding polytope_def by auto
qed
end

end