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