section ‹Integer Hull› text ‹We define the integer hull of a polyhedron, i.e., the convex hull of all integer solutions. Moreover, we prove the result of Meyer that the integer hull of a polyhedron defined by an integer matrix is again a polyhedron, and give bounds for a corresponding decomposition theorem.› theory Integer_Hull imports Decomposition_Theorem Mixed_Integer_Solutions (* for gram-schmidt-floor *) begin context gram_schmidt begin definition "integer_hull P = convex_hull (P ∩ ℤ⇩_{v})" lemma integer_hull_mono: "P ⊆ Q ⟹ integer_hull P ⊆ integer_hull Q" unfolding integer_hull_def by (intro convex_hull_mono, auto) end lemma abs_neg_floor: "¦of_int b¦ ≤ Bnd ⟹ - (floor Bnd) ≤ b" using abs_le_D2 floor_mono by fastforce lemma abs_pos_floor: "¦of_int b¦ ≤ Bnd ⟹ b ≤ floor Bnd" using abs_le_D1 le_floor_iff by auto context gram_schmidt_floor begin lemma integer_hull_integer_cone: assumes C: "C ⊆ carrier_vec n" and CI: "C ⊆ ℤ⇩_{v}" shows "integer_hull (cone C) = cone C" proof have "cone C ∩ ℤ⇩_{v}⊆ cone C" by blast thus "integer_hull (cone C) ⊆ cone C" using cone_cone[OF C] convex_cone[OF C] convex_hull_mono unfolding integer_hull_def convex_def by metis { fix x assume "x ∈ cone C" then obtain D where finD: "finite D" and DC: "D ⊆ C" and x: "x ∈ finite_cone D" unfolding cone_def by auto from DC C CI have D: "D ⊆ carrier_vec n" and DI: "D ⊆ ℤ⇩_{v}" by auto from D x finD have "x ∈ finite_cone (D ∪ {0⇩_{v}n})" using finite_cone_mono[of "D ∪ {0⇩_{v}n}" D] by auto then obtain l where x: "lincomb l (D ∪ {0⇩_{v}n}) = x" and l: "l ` (D ∪ {0⇩_{v}n}) ⊆ {t. t ≥ 0}" using finD unfolding finite_cone_def nonneg_lincomb_def by auto define L where "L = sum l (D ∪ {0⇩_{v}n})" define L_sup :: 'a where "L_sup = of_int (floor L + 1)" have "L_sup ≥ L" using floor_correct[of L] unfolding L_sup_def by linarith have "L ≥ 0" unfolding L_def using sum_nonneg[of _ l] l by blast hence "L_sup ≥ 1" unfolding L_sup_def by simp hence "L_sup > 0" by fastforce let ?f = "λ y. if y = 0⇩_{v}n then L_sup - L else 0" have "lincomb ?f {0⇩_{v}n} = 0⇩_{v}n" using already_in_span[of "{}" "0⇩_{v}n"] lincomb_in_span local.span_empty by auto moreover have "lincomb ?f (D - {0⇩_{v}n}) = 0⇩_{v}n" by(rule lincomb_zero, insert D, auto) ultimately have "lincomb ?f (D ∪ {0⇩_{v}n}) = 0⇩_{v}n" using lincomb_vec_diff_add[of "D ∪ {0⇩_{v}n}" "{0⇩_{v}n}"] D finD by simp hence lcomb_f: "lincomb (λ y. l y + ?f y) (D ∪ {0⇩_{v}n}) = x" using lincomb_sum[of "D ∪ {0⇩_{v}n}" l ?f] finD D x by simp have "sum ?f (D ∪ {0⇩_{v}n}) = L_sup - L" by (simp add: sum.subset_diff[of "{0⇩_{v}n}" "D ∪ {0⇩_{v}n}" ?f] finD) hence "sum (λ y. l y + ?f y) (D ∪ {0⇩_{v}n}) = L_sup" using l L_def by auto moreover have "(λ y. l y + ?f y) ` (D ∪ {0⇩_{v}n}) ⊆ {t. t ≥ 0}" using ‹L ≤ L_sup› l by force ultimately obtain l' where x: "lincomb l' (D ∪ {0⇩_{v}n}) = x" and l': "l' ` (D ∪ {0⇩_{v}n}) ⊆ {t. t ≥ 0}" and sum_l': "sum l' (D ∪ {0⇩_{v}n}) = L_sup" using lcomb_f by blast let ?D' = "{L_sup ⋅⇩_{v}v | v. v ∈ D ∪ {0⇩_{v}n}}" have Did: "?D' = (λ v. L_sup ⋅⇩_{v}v) ` (D ∪ {0⇩_{v}n})" by force define l'' where "l'' = (λ y. l' ((1 / L_sup) ⋅⇩_{v}y) / L_sup)" obtain lD where dist: "distinct lD" and lD: "D ∪ {0⇩_{v}n} = set lD" using finite_distinct_list[of "D ∪ {0⇩_{v}n}"] finD by auto let ?lD' = "map ((⋅⇩_{v}) L_sup) lD" have dist': "distinct ?lD'" using distinct_smult_nonneg[OF _ dist] ‹L_sup > 0› by fastforce have x': "lincomb l'' ?D' = x" unfolding x[symmetric] l''_def unfolding lincomb_def Did proof (subst finsum_reindex) from ‹L_sup > 0› smult_vec_nonneg_eq[of L_sup] show "inj_on ((⋅⇩_{v}) L_sup) (D ∪ {0⇩_{v}n})" by (auto simp: inj_on_def) show "(λv. l' (1 / L_sup ⋅⇩_{v}v) / L_sup ⋅⇩_{v}v) ∈ (⋅⇩_{v}) L_sup ` (D ∪ {0⇩_{v}n}) → carrier_vec n" using D by auto from ‹L_sup > 0› have "L_sup ≠ 0" by auto then show "(⨁⇘V⇙x∈D ∪ {0⇩_{v}n}. l' (1 / L_sup ⋅⇩_{v}(L_sup ⋅⇩_{v}x)) / L_sup ⋅⇩_{v}(L_sup ⋅⇩_{v}x)) = (⨁⇘V⇙v∈D ∪ {0⇩_{v}n}. l' v ⋅⇩_{v}v)" by (intro finsum_cong, insert D, auto simp: smult_smult_assoc) qed have "D ∪ {0⇩_{v}n} ⊆ cone C" using set_in_cone[OF C] DC zero_in_cone by blast hence D': "?D' ⊆ cone C" using cone_smult[of L_sup, OF _ C] ‹L_sup > 0› by auto have "D ∪ {0⇩_{v}n} ⊆ ℤ⇩_{v}" unfolding zero_vec_def using DI Ints_vec_def by auto moreover have "L_sup ∈ ℤ" unfolding L_sup_def by auto ultimately have D'I: "?D' ⊆ ℤ⇩_{v}" unfolding Ints_vec_def by force have "1 = sum l' (D ∪ {0⇩_{v}n}) * (1 / L_sup)" using sum_l' ‹L_sup > 0› by auto also have "sum l' (D ∪ {0⇩_{v}n}) = sum_list (map l' lD)" using sum.distinct_set_conv_list[OF dist] lD by auto also have "map l' lD = map (l' ∘ ((⋅⇩_{v}) (1 / L_sup))) ?lD'" using smult_smult_assoc[of "1 / L_sup" L_sup] ‹L_sup > 0› by (simp add: comp_assoc) also have "l' ∘ ((⋅⇩_{v}) (1 / L_sup)) = (λ x. l' ((1 / L_sup) ⋅⇩_{v}x))" by (rule comp_def) also have "sum_list (map … ?lD') * (1 / L_sup) = sum_list (map (λy. l' (1 / L_sup ⋅⇩_{v}y) * (1 / L_sup)) ?lD')" using sum_list_mult_const[of _ "1 / L_sup" ?lD'] by presburger also have "… = sum_list (map l'' ?lD')" unfolding l''_def using ‹L_sup > 0› by simp also have "… = sum l'' (set ?lD')" using sum.distinct_set_conv_list[OF dist'] by metis also have "set ?lD' = ?D'" using lD by auto finally have sum_l': "sum l'' ?D' = 1" by auto moreover have "l'' ` ?D' ⊆ {t. t ≥ 0}" proof fix y assume "y ∈ l'' ` ?D'" then obtain x where y: "y = l'' x" and "x ∈ ?D'" by blast then obtain v where "v ∈ D ∪ {0⇩_{v}n}" and x: "x = L_sup ⋅⇩_{v}v" by blast hence "0 ≤ l' v / L_sup" using l' ‹L_sup > 0› by fastforce also have "… = l'' x" unfolding x l''_def using smult_smult_assoc[of "1 / L_sup" "L_sup" v] ‹L_sup > 0› by simp finally show "y ∈ {t. t ≥ 0}" using y by blast qed moreover have "finite ?D'" using finD by simp ultimately have "x ∈ integer_hull (cone C)" unfolding integer_hull_def convex_hull_def using x' D' D'I convex_lincomb_def[of l'' ?D' x] nonneg_lincomb_def[of l'' ?D' x] by fast } thus "cone C ⊆ integer_hull (cone C)" by blast qed theorem decomposition_theorem_integer_hull_of_polyhedron: assumes db: "is_det_bound db" and A: "A ∈ carrier_mat nr n" and b: "b ∈ carrier_vec nr" and AI: "A ∈ ℤ⇩_{m}" and bI: "b ∈ ℤ⇩_{v}" and P: "P = polyhedron A b" and Bnd: "of_int Bnd ≥ Max (abs ` (elements_mat A ∪ vec_set b))" shows "∃ H C. H ∪ C ⊆ carrier_vec n ∩ ℤ⇩_{v}∧ H ⊆ Bounded_vec (of_nat (n + 1) * of_int (db n (max 1 Bnd))) ∧ C ⊆ Bounded_vec (of_int (db n (max 1 Bnd))) ∧ finite (H ∪ C) ∧ integer_hull P = convex_hull H + cone C" proof - define MBnd where "MBnd = Max (abs ` (elements_mat A ∪ set⇩_{v}b))" define DBnd :: 'a where "DBnd = of_int (db n (max 1 Bnd))" define nBnd where "nBnd = of_nat (n+1) * DBnd" have DBnd0: "DBnd ≥ 0" unfolding DBnd_def of_int_0_le_iff by (rule is_det_bound_ge_zero[OF db], auto) have Pn: "P ⊆ carrier_vec n" unfolding P polyhedron_def by auto have "A ∈ Bounded_mat MBnd ∧ b ∈ Bounded_vec MBnd" unfolding MBnd_def Bounded_mat_elements_mat Bounded_vec_vec_set by (intro ballI conjI Max_ge finite_imageI imageI finite_UnI, auto) hence "A ∈ Bounded_mat (of_int Bnd) ∧ b ∈ Bounded_vec (of_int Bnd)" using Bounded_mat_mono[OF Bnd] Bounded_vec_mono[OF Bnd] unfolding MBnd_def by auto from decomposition_theorem_polyhedra_1[OF A b P, of db Bnd] db AI bI this obtain QQ Q C where C: "C ⊆ carrier_vec n" and finC: "finite C" and QQ: "QQ ⊆ carrier_vec n" and finQ: "finite QQ" and BndQQ: "QQ ⊆ Bounded_vec DBnd" and P: "P = Q + cone C" and Q_def: "Q = convex_hull QQ" and CI: "C ⊆ ℤ⇩_{v}" and BndC: "C ⊆ Bounded_vec DBnd" by (auto simp: DBnd_def) define Bnd' where "Bnd' = of_nat n * DBnd" note coneC = cone_iff_finite_cone[OF C finC] have Q: "Q ⊆ carrier_vec n" unfolding Q_def using convex_hull_carrier[OF QQ] . define B where "B = {x. ∃ a D. nonneg_lincomb a D x ∧ D ⊆ C ∧ lin_indpt D ∧ (∀ d ∈ D. a d ≤ 1)}" { fix b assume "b ∈ B" then obtain a D where b: "b = lincomb a D" and DC: "D ⊆ C" and linD: "lin_indpt D" and bnd_a: "∀ d ∈ D. 0 ≤ a d ∧ a d ≤ 1" by (force simp: B_def nonneg_lincomb_def) from DC C have D: "D ⊆ carrier_vec n" by auto from DC finC have finD: "finite D" by (metis finite_subset) from D linD finD have cardD: "card D ≤ n" using dim_is_n li_le_dim(2) by auto from BndC DC have BndD: "D ⊆ Bounded_vec DBnd" by auto from lincomb_card_bound[OF this D DBnd0 _ cardD, of a, folded b] bnd_a have "b ∈ Bounded_vec Bnd'" unfolding Bnd'_def by force } hence BndB: "B ⊆ Bounded_vec Bnd'" .. from BndQQ have BndQ: "Q ⊆ Bounded_vec DBnd" unfolding Q_def using QQ by (metis convex_hull_bound) have B: "B ⊆ carrier_vec n" unfolding B_def nonneg_lincomb_def using C by auto from Q B have QB: "Q + B ⊆ carrier_vec n" by (auto elim!: set_plus_elim) from sum_in_Bounded_vecI[of _ DBnd _ Bnd' n] BndQ BndB B Q have "Q + B ⊆ Bounded_vec (DBnd + Bnd')" by (auto elim!: set_plus_elim) also have "DBnd + Bnd' = nBnd" unfolding nBnd_def Bnd'_def by (simp add: algebra_simps) finally have QB_Bnd: "Q + B ⊆ Bounded_vec nBnd" by blast have finQBZ: "finite ((Q + B) ∩ ℤ⇩_{v})" proof (rule finite_subset[OF subsetI]) define ZBnd where "ZBnd = floor nBnd" let ?vecs = "set (map vec_of_list (concat_lists (map (λ i. map (of_int :: _ ⇒ 'a) [-ZBnd..ZBnd]) [0..<n])))" have id: "?vecs = vec_of_list ` {as. length as = n ∧ (∀i<n. ∃ b. as ! i = of_int b ∧ b ∈ {- ZBnd..ZBnd})}" unfolding set_map by (rule image_cong, auto) show "finite ?vecs" by (rule finite_set) fix x assume "x ∈ (Q + B) ∩ ℤ⇩_{v}" hence xQB: "x ∈ Q + B" and xI: "x ∈ ℤ⇩_{v}" by auto from xQB QB_Bnd QB have xBnd: "x ∈ Bounded_vec nBnd" and x: "x ∈ carrier_vec n" by auto have xid: "x = vec_of_list (list_of_vec x)" by auto show "x ∈ ?vecs" unfolding id proof (subst xid, intro imageI CollectI conjI allI impI) show "length (list_of_vec x) = n" using x by auto fix i assume i: "i < n" have id: "list_of_vec x ! i = x $ i" using i x by auto from xBnd[unfolded Bounded_vec_def] i x have xiBnd: "abs (x $ i) ≤ nBnd" by auto from xI[unfolded Ints_vec_def] i x have "x $ i ∈ ℤ" by auto then obtain b where b: "x $ i = of_int b" unfolding Ints_def by blast show "∃b. list_of_vec x ! i = of_int b ∧ b ∈ {- ZBnd..ZBnd}" unfolding id ZBnd_def using xiBnd unfolding b by (intro exI[of _ b], auto intro!: abs_neg_floor abs_pos_floor) qed qed have QBZ: "(Q + B) ∩ ℤ⇩_{v}⊆ carrier_vec n" using QB by auto from decomposition_theorem_polyhedra_2[OF QBZ finQBZ, folded integer_hull_def, OF C finC refl] obtain A' b' nr' where A': "A' ∈ carrier_mat nr' n" and b': "b' ∈ carrier_vec nr'" and IH: "integer_hull (Q + B) + cone C = polyhedron A' b'" by auto { fix p assume "p ∈ P ∩ ℤ⇩_{v}" hence pI: "p ∈ ℤ⇩_{v}" and p: "p ∈ Q + cone C" unfolding P by auto from set_plus_elim[OF p] obtain q c where pqc: "p = q + c" and qQ: "q ∈ Q" and cC: "c ∈ cone C" by auto from qQ Q have q: "q ∈ carrier_vec n" by auto from Caratheodory_theorem[OF C] cC obtain D where cD: "c ∈ finite_cone D" and DC: "D ⊆ C" and linD: "lin_indpt D" by auto from DC C have D: "D ⊆ carrier_vec n" by auto from DC finC have finD: "finite D" by (metis finite_subset) from cD finD obtain a where "nonneg_lincomb a D c" unfolding finite_cone_def by auto hence caD: "c = lincomb a D" and a0: "⋀ d. d ∈ D ⟹ a d ≥ 0" unfolding nonneg_lincomb_def by auto define a1 where "a1 = (λ c. a c - of_int (floor (a c)))" define a2 where "a2 = (λ c. of_int (floor (a c)) :: 'a)" define d where "d = lincomb a2 D" define b where "b = lincomb a1 D" have b: "b ∈ carrier_vec n" and d: "d ∈ carrier_vec n" unfolding d_def b_def using D by auto have bB: "b ∈ B" unfolding B_def b_def nonneg_lincomb_def proof (intro CollectI exI[of _ a1] exI[of _ D] conjI ballI refl subsetI linD) show "x ∈ a1 ` D ⟹ 0 ≤ x" for x using a0 unfolding a1_def by auto show "a1 c ≤ 1" for c unfolding a1_def by linarith qed (insert DC, auto) have cbd: "c = b + d" unfolding b_def d_def caD lincomb_sum[OF finD D, symmetric] by (rule lincomb_cong[OF refl D], auto simp: a1_def a2_def) have "nonneg_lincomb a2 D d" unfolding d_def nonneg_lincomb_def by (intro allI conjI refl subsetI, insert a0, auto simp: a2_def) hence dC: "d ∈ cone C" unfolding cone_def finite_cone_def using finC finD DC by auto have p: "p = (q + b) + d" unfolding pqc cbd using q b d by auto have dI: "d ∈ ℤ⇩_{v}" using CI DC C unfolding d_def indexed_Ints_vec_UNIV by (intro lincomb_indexed_Ints_vec, auto simp: a2_def) from diff_indexed_Ints_vec[of _ _ _ UNIV, folded indexed_Ints_vec_UNIV, OF _ d pI dI, unfolded p] have "q + b + d - d ∈ ℤ⇩_{v}" using q b d by auto also have "q + b + d - d = q + b" using q b d by auto finally have qbI: "q + b ∈ ℤ⇩_{v}" by auto have "p ∈ integer_hull (Q + B) + cone C" unfolding p integer_hull_def by (intro set_plus_intro dC set_mp[OF set_in_convex_hull] IntI qQ bB qbI, insert Q B, auto elim!: set_plus_elim) } hence "P ∩ ℤ⇩_{v}⊆ integer_hull (Q + B) + cone C" by auto hence one_dir: "integer_hull P ⊆ integer_hull (Q + B) + cone C" unfolding IH unfolding integer_hull_def using convex_convex_hull[OF polyhedra_are_convex[OF A' b' refl]] convex_hull_mono by blast have "integer_hull (Q + B) + cone C ⊆ integer_hull P + cone C" unfolding P proof (intro set_plus_mono2 subset_refl integer_hull_mono) show "B ⊆ cone C" unfolding B_def cone_def finite_cone_def using finite_subset[OF _ finC] by auto qed also have "… = integer_hull P + integer_hull (cone C)" using integer_hull_integer_cone[OF C CI] by simp also have "… = convex_hull (P ∩ ℤ⇩_{v}) + convex_hull (cone C ∩ ℤ⇩_{v})" unfolding integer_hull_def by simp also have "… = convex_hull ((P ∩ ℤ⇩_{v}) + (cone C ∩ ℤ⇩_{v}))" by (rule convex_hull_sum[symmetric], insert Pn cone_carrier[OF C], auto) also have "… ⊆ convex_hull ((P + cone C) ∩ ℤ⇩_{v})" proof (rule convex_hull_mono) show "P ∩ ℤ⇩_{v}+ cone C ∩ ℤ⇩_{v}⊆ (P + cone C) ∩ ℤ⇩_{v}" using add_indexed_Ints_vec[of _ n _ UNIV, folded indexed_Ints_vec_UNIV] cone_carrier[OF C] Pn by (auto elim!: set_plus_elim) qed also have "… = integer_hull (P + cone C)" unfolding integer_hull_def .. also have "P + cone C = P" proof - have CC: "cone C ⊆ carrier_vec n" using C by (rule cone_carrier) have "P + cone C = Q + (cone C + cone C)" unfolding P by (rule assoc_add_vecset[symmetric, OF Q CC CC]) also have "cone C + cone C = cone C" by (rule cone_add_cone[OF C]) finally show ?thesis unfolding P . qed finally have "integer_hull (Q + B) + cone C ⊆ integer_hull P" . with one_dir have id: "integer_hull P = integer_hull (Q + B) + cone C" by auto show ?thesis unfolding id unfolding integer_hull_def DBnd_def[symmetric] nBnd_def[symmetric] proof (rule exI[of _ "(Q + B) ∩ ℤ⇩_{v}"], intro exI[of _ C] conjI refl BndC) from QB_Bnd show "(Q + B) ∩ ℤ⇩_{v}⊆ Bounded_vec nBnd" by auto show "(Q + B) ∩ ℤ⇩_{v}∪ C ⊆ carrier_vec n ∩ ℤ⇩_{v}" using QB C CI by auto show "finite ((Q + B) ∩ ℤ⇩_{v}∪ C)" using finQBZ finC by auto qed qed corollary integer_hull_of_polyhedron: assumes A: "A ∈ carrier_mat nr n" and b: "b ∈ carrier_vec nr" and AI: "A ∈ ℤ⇩_{m}" and bI: "b ∈ ℤ⇩_{v}" and P: "P = polyhedron A b" shows "∃ A' b' nr'. A' ∈ carrier_mat nr' n ∧ b' ∈ carrier_vec nr' ∧ integer_hull P = polyhedron A' b'" proof - obtain Bnd where Bnd: "Max (abs ` (elements_mat A ∪ set⇩_{v}b)) ≤ of_int Bnd" by (meson ex_le_of_int) from decomposition_theorem_integer_hull_of_polyhedron[OF det_bound_fact A b AI bI P Bnd] obtain H C where HC: "H ∪ C ⊆ carrier_vec n ∩ ℤ⇩_{v}" "finite (H ∪ C)" and decomp: "integer_hull P = convex_hull H + cone C" by auto show ?thesis by (rule decomposition_theorem_polyhedra_2[OF _ _ _ _ decomp], insert HC, auto) qed corollary small_integer_solution_nonstrict_via_decomp: fixes A :: "'a mat" assumes db: "is_det_bound db" and A: "A ∈ carrier_mat nr n" and b: "b ∈ carrier_vec nr" and AI: "A ∈ ℤ⇩_{m}" and bI: "b ∈ ℤ⇩_{v}" and Bnd: "of_int Bnd ≥ Max (abs ` (elements_mat A ∪ vec_set b))" and x: "x ∈ carrier_vec n" and xI: "x ∈ ℤ⇩_{v}" and sol: "A *⇩_{v}x ≤ b" shows "∃ y. y ∈ carrier_vec n ∧ y ∈ ℤ⇩_{v}∧ A *⇩_{v}y ≤ b ∧ y ∈ Bounded_vec (of_nat (n+1) * of_int (db n (max 1 Bnd)))" proof - from x sol have "x ∈ polyhedron A b" unfolding polyhedron_def by auto with xI x have xsol: "x ∈ integer_hull (polyhedron A b)" unfolding integer_hull_def by (meson IntI convex_hull_mono in_mono inf_sup_ord(1) inf_sup_ord(2) set_in_convex_hull) from decomposition_theorem_integer_hull_of_polyhedron[OF db A b AI bI refl Bnd] obtain H C where HC: "H ∪ C ⊆ carrier_vec n ∩ ℤ⇩_{v}" "H ⊆ Bounded_vec (of_nat (n + 1) * of_int (db n (max 1 Bnd)))" "finite (H ∪ C)" and id: "integer_hull (polyhedron A b) = convex_hull H + cone C" by auto from xsol[unfolded id] have "H ≠ {}" unfolding set_plus_def by auto then obtain h where hH: "h ∈ H" by auto with set_in_convex_hull have "h ∈ convex_hull H" using HC by auto moreover have "0⇩_{v}n ∈ cone C" by (intro zero_in_cone) ultimately have "h + 0⇩_{v}n ∈ integer_hull (polyhedron A b)" unfolding id by auto also have "h + 0⇩_{v}n = h" using hH HC by auto also have "integer_hull (polyhedron A b) ⊆ convex_hull (polyhedron A b)" unfolding integer_hull_def by (rule convex_hull_mono, auto) also have "convex_hull (polyhedron A b) = polyhedron A b" using A b using convex_convex_hull polyhedra_are_convex by blast finally have h: "h ∈ carrier_vec n" "A *⇩_{v}h ≤ b" unfolding polyhedron_def by auto show ?thesis by (intro exI[of _ h] conjI h, insert HC hH, auto) qed lemmas small_integer_solution_nonstrict_via_decomp_hadamard = small_integer_solution_nonstrict_via_decomp[OF det_bound_hadamard, unfolded det_bound_hadamard_def] end end