diff --git a/thys/Linear_Inequalities/Mixed_Integer_Solutions.thy b/thys/Linear_Inequalities/Mixed_Integer_Solutions.thy --- a/thys/Linear_Inequalities/Mixed_Integer_Solutions.thy +++ b/thys/Linear_Inequalities/Mixed_Integer_Solutions.thy @@ -1,474 +1,474 @@ section \Mixed Integer Solutions\ text \We prove that if an integral system of linear inequalities $Ax \leq b \wedge A'x < b'$ has a (mixed)integer solution, then there is also a small (mixed)integer solution, where the numbers are bounded by $(n+1) * db\, m\, n$ where $n$ is the number of variables, $m$ is a bound on the absolute values of numbers occurring in $A,A',b,b'$, and $db\,m\,n$ is a bound on determinants for matrices of size $n$ with values of at most $m$.\ theory Mixed_Integer_Solutions imports Decomposition_Theorem begin definition less_vec :: "'a vec \ ('a :: ord) vec \ bool" (infix "<\<^sub>v" 50) where "v <\<^sub>v w = (dim_vec v = dim_vec w \ (\ i < dim_vec w. v $ i < w $ i))" lemma less_vecD: assumes "v <\<^sub>v w" and "w \ carrier_vec n" shows "i < n \ v $ i < w $ i" using assms unfolding less_vec_def by auto lemma less_vecI: assumes "v \ carrier_vec n" "w \ carrier_vec n" "\ i. i < n \ v $ i < w $ i" shows "v <\<^sub>v w" using assms unfolding less_vec_def by auto lemma less_vec_lesseq_vec: "v <\<^sub>v (w :: 'a :: preorder vec) \ v \ w" unfolding less_vec_def less_eq_vec_def by (auto simp: less_le_not_le) lemma floor_less: "x \ \ \ of_int \x\ < x" using le_less by fastforce lemma floor_of_int_eq[simp]: "x \ \ \ of_int \x\ = x" by (metis Ints_cases of_int_floor_cancel) locale gram_schmidt_floor = gram_schmidt n f_ty for n :: nat and f_ty :: "'a :: {floor_ceiling, trivial_conjugatable_linordered_field} itself" begin lemma small_mixed_integer_solution_main: fixes A\<^sub>1 :: "'a mat" assumes db: "is_det_bound db" and A1: "A\<^sub>1 \ carrier_mat nr\<^sub>1 n" and A2: "A\<^sub>2 \ carrier_mat nr\<^sub>2 n" and b1: "b\<^sub>1 \ carrier_vec nr\<^sub>1" and b2: "b\<^sub>2 \ carrier_vec nr\<^sub>2" and A1Bnd: "A\<^sub>1 \ \\<^sub>m \ Bounded_mat (of_int Bnd)" and b1Bnd: "b\<^sub>1 \ \\<^sub>v \ Bounded_vec (of_int Bnd)" and A2Bnd: "A\<^sub>2 \ \\<^sub>m \ Bounded_mat (of_int Bnd)" and b2Bnd: "b\<^sub>2 \ \\<^sub>v \ Bounded_vec (of_int Bnd)" and x: "x \ carrier_vec n" and xI: "x \ indexed_Ints_vec I" and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \ b\<^sub>1" and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2" shows "\ x. x \ carrier_vec n \ x \ indexed_Ints_vec I \ A\<^sub>1 *\<^sub>v x \ b\<^sub>1 \ A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \ x \ Bounded_vec (of_int (of_nat (n + 1) * db n (max 1 Bnd)))" proof - let ?oi = "of_int :: int \ 'a" let ?Bnd = "?oi Bnd" define B where "B = ?oi (db n (max 1 Bnd))" define A where "A = A\<^sub>1 @\<^sub>r A\<^sub>2" define b where "b = b\<^sub>1 @\<^sub>v b\<^sub>2" define nr where "nr = nr\<^sub>1 + nr\<^sub>2" have B0: "B \ 0" unfolding B_def of_int_0_le_iff by (rule is_det_bound_ge_zero[OF db], auto) note defs = A_def b_def nr_def from A1 A2 have A: "A \ carrier_mat nr n" unfolding defs by auto from b1 b2 have b: "b \ carrier_vec nr" unfolding defs by auto from A1Bnd A2Bnd A1 A2 have ABnd: "A \ \\<^sub>m \ Bounded_mat ?Bnd" unfolding defs by (auto simp: Ints_mat_elements_mat Bounded_mat_elements_mat elements_mat_append_rows) from b1Bnd b2Bnd b1 b2 have bBnd: "b \ \\<^sub>v \ Bounded_vec ?Bnd" unfolding defs by (auto simp: Ints_vec_vec_set Bounded_vec_vec_set) from decomposition_theorem_polyhedra_1[OF A b refl, of db Bnd] ABnd bBnd db obtain Y Z where Z: "Z \ carrier_vec n" and finX: "finite Z" and Y: "Y \ carrier_vec n" and finY: "finite Y" and poly: "polyhedron A b = convex_hull Y + cone Z" and ZBnd: "Z \ \\<^sub>v \ Bounded_vec B" and YBnd: "Y \ Bounded_vec B" unfolding B_def by blast let ?P = "{x \ carrier_vec n. A\<^sub>1 *\<^sub>v x \ b\<^sub>1 \ A\<^sub>2 *\<^sub>v x \ b\<^sub>2}" let ?L = "?P \ {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \ indexed_Ints_vec I" have "polyhedron A b = {x \ carrier_vec n. A *\<^sub>v x \ b}" unfolding polyhedron_def by auto also have "\ = ?P" unfolding defs by (intro Collect_cong conj_cong refl append_rows_le[OF A1 A2 b1]) finally have poly: "?P = convex_hull Y + cone Z" unfolding poly .. have "x \ ?P" using x sol_nonstrict less_vec_lesseq_vec[OF sol_strict] by blast note sol = this[unfolded poly] from set_plus_elim[OF sol] obtain y z where xyz: "x = y + z" and yY: "y \ convex_hull Y" and zZ: "z \ cone Z" by auto from convex_hull_carrier[OF Y] yY have y: "y \ carrier_vec n" by auto from Caratheodory_theorem[OF Z] zZ obtain C where zC: "z \ finite_cone C" and CZ: "C \ Z" and lin: "lin_indpt C" by auto from subset_trans[OF CZ Z] lin have card: "card C \ n" using dim_is_n li_le_dim(2) by auto from finite_subset[OF CZ finX] have finC: "finite C" . from zC[unfolded finite_cone_def nonneg_lincomb_def] finC obtain a where za: "z = lincomb a C" and nonneg: "\ u. u \ C \ a u \ 0" by auto from CZ Z have C: "C \ carrier_vec n" by auto have z: "z \ carrier_vec n" using C unfolding za by auto have yB: "y \ Bounded_vec B" using yY convex_hull_bound[OF YBnd Y] by auto { fix D assume DC: "D \ C" from finite_subset[OF this finC] have "finite D" . hence "\ a. y + lincomb a C \ ?L \ (\ c \ C. a c \ 0) \ (\ c \ D. a c \ 1)" using DC proof (induct D) case empty show ?case by (intro exI[of _ a], fold za xyz, insert sol_strict x xI nonneg \x \ ?P\, auto) next case (insert c D) then obtain a where sol: "y + lincomb a C \ ?L" and a: "(\ c \ C. a c \ 0)" and D: "(\ c \ D. a c \ 1)" by auto from insert(4) C have c: "c \ carrier_vec n" and cC: "c \ C" by auto show ?case proof (cases "a c > 1") case False thus ?thesis by (intro exI[of _ a], insert sol a D, auto) next case True (* this is the core reasoning step where a\<^sub>c is large *) let ?z = "\ d. lincomb a C - d \\<^sub>v c" let ?x = "\ d. y + ?z d" { fix d have lin: "lincomb a (C - {c}) \ carrier_vec n" using C by auto have id: "?z d = lincomb (\ e. if e = c then (a c - d) else a e) C" unfolding lincomb_del2[OF finC C TrueI cC] by (subst (2) lincomb_cong[OF refl, of _ _ a], insert C c lin, auto simp: diff_smult_distrib_vec) { assume le: "d \ a c" have "?z d \ finite_cone C" proof - have "\f\C. 0 \ (\e. if e = c then a c - d else a e) f" using le a finC by simp then show ?thesis unfolding id using le a finC by (simp add: C lincomb_in_finite_cone) qed hence "?z d \ cone Z" using CZ using finC local.cone_def by blast hence "?x d \ ?P" unfolding poly by (intro set_plus_intro[OF yY], auto) } note sol = this { fix w :: "'a vec" assume w: "w \ carrier_vec n" have "w \ (?x d) = w \ y + w \ lincomb a C - d * (w \ c)" by (subst scalar_prod_add_distrib[OF w y], (insert C c, force), subst scalar_prod_minus_distrib[OF w], insert w c C, auto) } note scalar = this note id sol scalar } note generic = this let ?fl = "(of_int (floor (a c)) :: 'a)" define p where "p = (if ?fl = a c then a c - 1 else ?fl)" have p_lt_ac: "p < a c" unfolding p_def using floor_less floor_of_int_eq by auto have p1_ge_ac: "p + 1 \ a c" unfolding p_def using floor_correct le_less by auto have p1: "p \ 1" using True unfolding p_def by auto define a' where "a' = (\e. if e = c then a c - p else a e)" have lin_id: "lincomb a' C = lincomb a C - p \\<^sub>v c" unfolding a'_def using id by (simp add: generic(1)) hence 1: "y + lincomb a' C \ {x \ carrier_vec n. A\<^sub>1 *\<^sub>v x \ b\<^sub>1 \ A\<^sub>2 *\<^sub>v x \ b\<^sub>2}" using p_lt_ac generic(2)[of p] by auto have pInt: "p \ \" unfolding p_def using sol by auto have "C \ indexed_Ints_vec I" using CZ ZBnd using indexed_Ints_vec_subset by force hence "c \ indexed_Ints_vec I" using cC by auto hence pvindInts: "p \\<^sub>v c \ indexed_Ints_vec I" unfolding indexed_Ints_vec_def using pInt by simp have prod: "A\<^sub>2 *\<^sub>v (?x b) \ carrier_vec nr\<^sub>2" for b using A2 C c y by auto have 2: "y + lincomb a' C \ {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2}" unfolding lin_id proof (intro less_vecI[OF prod b2] CollectI) fix i assume i: "i < nr\<^sub>2" from sol have "A\<^sub>2 *\<^sub>v (?x 0) <\<^sub>v b\<^sub>2" using y C c by auto from less_vecD[OF this b2 i] have lt: "row A\<^sub>2 i \ ?x 0 < b\<^sub>2 $ i" using A2 i by auto from generic(2)[of "a c"] i A2 have le: "row A\<^sub>2 i \ ?x (a c) \ b\<^sub>2 $ i" unfolding less_eq_vec_def by auto from A2 i have A2icarr: "row A\<^sub>2 i \ carrier_vec n" by auto have "row A\<^sub>2 i \ ?x p < b\<^sub>2 $ i" proof - define lhs where "lhs = row A\<^sub>2 i \ y + row A\<^sub>2 i \ lincomb a C - b\<^sub>2 $ i" define mult where "mult = row A\<^sub>2 i \ c" have le2: "lhs \ a c * mult" using le unfolding generic(3)[OF A2icarr] lhs_def mult_def by auto have lt2: "lhs < 0 * mult" using lt unfolding generic(3)[OF A2icarr] lhs_def by auto from le2 lt2 have "lhs < p * mult" using p_lt_ac p1 True by (smt dual_order.strict_trans linorder_neqE_linordered_idom mult_less_cancel_right not_less zero_less_one_class.zero_less_one) then show ?thesis unfolding generic(3)[OF A2icarr] lhs_def mult_def by auto qed thus "(A\<^sub>2 *\<^sub>v ?x p) $ i < b\<^sub>2 $ i" using i A2 by auto qed have "y + lincomb a' C = y + lincomb a C - p \\<^sub>v c" by (subst lin_id, insert y C c, auto simp: add_diff_eq_vec) also have "\ \ indexed_Ints_vec I" using sol by(intro diff_indexed_Ints_vec[OF _ _ _ pvindInts, of _ n ], insert c C, auto) finally have 3: "y + lincomb a' C \ indexed_Ints_vec I" by auto have 4: "\c\C. 0 \ a' c" unfolding a'_def p_def using p_lt_ac a by auto have 5: "\c\insert c D. a' c \ 1" unfolding a'_def using p1_ge_ac D p_def by auto show ?thesis by (intro exI[of _ a'], intro conjI IntI 1 2 3 4 5) qed qed } from this[of C] obtain a where sol: "y + lincomb a C \ ?L" and bnds: "(\ c \ C. a c \ 0)" "(\ c \ C. a c \ 1)" by auto show ?thesis proof (intro exI[of _ "y + lincomb a C"] conjI) from ZBnd CZ have BndC: "C \ Bounded_vec B" and IntC: "C \ \\<^sub>v" by auto have "lincomb a C \ Bounded_vec (of_nat n * B)" using lincomb_card_bound[OF BndC C B0 _ card] bnds by auto from sum_in_Bounded_vecI[OF yB this y] C have "y + lincomb a C \ Bounded_vec (B + of_nat n * B)" by auto also have "B + of_nat n * B = of_nat (n+1) * B" by (auto simp: field_simps) finally show "y + lincomb a C \ Bounded_vec (of_int (of_nat (n + 1) * db n (max 1 Bnd)))" unfolding B_def by auto qed (insert sol, auto) qed text \We get rid of the max-1 operation, by showing that a smaller value of Bnd can only occur in very special cases where the theorem is trivially satisfied.\ lemma small_mixed_integer_solution: fixes A\<^sub>1 :: "'a mat" assumes db: "is_det_bound db" and A1: "A\<^sub>1 \ carrier_mat nr\<^sub>1 n" and A2: "A\<^sub>2 \ carrier_mat nr\<^sub>2 n" and b1: "b\<^sub>1 \ carrier_vec nr\<^sub>1" and b2: "b\<^sub>2 \ carrier_vec nr\<^sub>2" and A1Bnd: "A\<^sub>1 \ \\<^sub>m \ Bounded_mat (of_int Bnd)" and b1Bnd: "b\<^sub>1 \ \\<^sub>v \ Bounded_vec (of_int Bnd)" and A2Bnd: "A\<^sub>2 \ \\<^sub>m \ Bounded_mat (of_int Bnd)" and b2Bnd: "b\<^sub>2 \ \\<^sub>v \ Bounded_vec (of_int Bnd)" and x: "x \ carrier_vec n" and xI: "x \ indexed_Ints_vec I" and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \ b\<^sub>1" and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2" and non_degenerate: "nr\<^sub>1 \ 0 \ nr\<^sub>2 \ 0 \ Bnd \ 0" shows "\ x. x \ carrier_vec n \ x \ indexed_Ints_vec I \ A\<^sub>1 *\<^sub>v x \ b\<^sub>1 \ A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \ x \ Bounded_vec (of_int (int (n+1) * db n Bnd))" proof (cases "Bnd \ 1") case True hence "max 1 Bnd = Bnd" by auto with small_mixed_integer_solution_main[OF assms(1-13)] True show ?thesis by auto next case trivial: False let ?oi = "of_int :: int \ 'a" show ?thesis proof (cases "n = 0") case True with x have "x \ Bounded_vec b" for b unfolding Bounded_vec_def by auto with xI x sol_nonstrict sol_strict show ?thesis by blast next case n: False { fix A nr assume A: "A \ carrier_mat nr n" and Bnd: "A \ \\<^sub>m \ Bounded_mat (?oi Bnd)" { fix i j assume "i < nr" "j < n" with Bnd A have *: "A $$ (i,j) \ \" "abs (A $$ (i,j)) \ ?oi Bnd" unfolding Bounded_mat_def Ints_mat_def by auto from Ints_nonzero_abs_less1[OF *(1)] *(2) trivial have "A $$ (i,j) = 0" by (meson add_le_less_mono int_one_le_iff_zero_less less_add_same_cancel2 of_int_0_less_iff zero_less_abs_iff) with *(2) have "Bnd \ 0" "A $$ (i,j) = 0" by auto } note main = this have A0: "A = 0\<^sub>m nr n" by (intro eq_matI, insert main A, auto) have "nr \ 0 \ Bnd \ 0" using main[of 0 0] n by auto note A0 this } note main = this from main[OF A1 A1Bnd] have A1: "A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n" and nr1: "nr\<^sub>1 \ 0 \ Bnd \ 0" by auto from main[OF A2 A2Bnd] have A2: "A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n" and nr2: "nr\<^sub>2 \ 0 \ Bnd \ 0" by auto let ?x = "0\<^sub>v n" show ?thesis proof (intro exI[of _ ?x] conjI) show "A\<^sub>1 *\<^sub>v ?x \ b\<^sub>1" using sol_nonstrict x unfolding A1 by auto show "A\<^sub>2 *\<^sub>v ?x <\<^sub>v b\<^sub>2" using sol_strict x unfolding A2 by auto show "?x \ carrier_vec n" by auto show "?x \ indexed_Ints_vec I" unfolding indexed_Ints_vec_def by auto from nr1 nr2 non_degenerate have Bnd: "Bnd \ 0" by auto from is_det_bound_ge_zero[OF db Bnd] have "db n Bnd \ 0" . hence "?oi (of_nat (n + 1) * db n Bnd) \ 0" by simp thus "?x \ Bounded_vec (?oi (of_nat (n + 1) * db n Bnd))" by (auto simp: Bounded_vec_def) qed qed qed lemmas small_mixed_integer_solution_hadamard = small_mixed_integer_solution[OF det_bound_hadamard, unfolded det_bound_hadamard_def of_int_mult of_int_of_nat_eq] lemma Bounded_vec_of_int: assumes "v \ Bounded_vec bnd" shows "(map_vec of_int v :: 'a vec) \ \\<^sub>v \ Bounded_vec (of_int bnd)" using assms apply (simp add: Ints_vec_vec_set Bounded_vec_vec_set Ints_def) apply (intro conjI, force) apply (clarsimp) subgoal for x apply (elim ballE[of _ _ x], auto) by (metis of_int_abs of_int_le_iff) done lemma Bounded_mat_of_int: assumes "A \ Bounded_mat bnd" shows "(map_mat of_int A :: 'a mat) \ \\<^sub>m \ Bounded_mat (of_int bnd)" using assms apply (simp add: Ints_mat_elements_mat Bounded_mat_elements_mat Ints_def) apply (intro conjI, force) apply (clarsimp) subgoal for x apply (elim ballE[of _ _ x], auto) by (metis of_int_abs of_int_le_iff) done lemma small_mixed_integer_solution_int_mat: fixes x :: "'a vec" assumes db: "is_det_bound db" and A1: "A\<^sub>1 \ carrier_mat nr\<^sub>1 n" and A2: "A\<^sub>2 \ carrier_mat nr\<^sub>2 n" and b1: "b\<^sub>1 \ carrier_vec nr\<^sub>1" and b2: "b\<^sub>2 \ carrier_vec nr\<^sub>2" and A1Bnd: "A\<^sub>1 \ Bounded_mat Bnd" and b1Bnd: "b\<^sub>1 \ Bounded_vec Bnd" and A2Bnd: "A\<^sub>2 \ Bounded_mat Bnd" and b2Bnd: "b\<^sub>2 \ Bounded_vec Bnd" and x: "x \ carrier_vec n" and xI: "x \ indexed_Ints_vec I" and sol_nonstrict: "map_mat of_int A\<^sub>1 *\<^sub>v x \ map_vec of_int b\<^sub>1" and sol_strict: "map_mat of_int A\<^sub>2 *\<^sub>v x <\<^sub>v map_vec of_int b\<^sub>2" and non_degenerate: "nr\<^sub>1 \ 0 \ nr\<^sub>2 \ 0 \ Bnd \ 0" shows "\ x :: 'a vec. x \ carrier_vec n \ x \ indexed_Ints_vec I \ map_mat of_int A\<^sub>1 *\<^sub>v x \ map_vec of_int b\<^sub>1 \ map_mat of_int A\<^sub>2 *\<^sub>v x <\<^sub>v map_vec of_int b\<^sub>2 \ x \ Bounded_vec (of_int (of_nat (n+1) * db n Bnd))" proof - let ?oi = "of_int :: int \ 'a" let ?A1 = "map_mat ?oi A\<^sub>1" let ?A2 = "map_mat ?oi A\<^sub>2" let ?b1 = "map_vec ?oi b\<^sub>1" let ?b2 = "map_vec ?oi b\<^sub>2" let ?Bnd = "?oi Bnd" from A1 have A1': "?A1 \ carrier_mat nr\<^sub>1 n" by auto from A2 have A2': "?A2 \ carrier_mat nr\<^sub>2 n" by auto from b1 have b1': "?b1 \ carrier_vec nr\<^sub>1" by auto from b2 have b2': "?b2 \ carrier_vec nr\<^sub>2" by auto from small_mixed_integer_solution[OF db A1' A2' b1' b2' Bounded_mat_of_int[OF A1Bnd] Bounded_vec_of_int[OF b1Bnd] Bounded_mat_of_int[OF A2Bnd] Bounded_vec_of_int[OF b2Bnd] x xI sol_nonstrict sol_strict non_degenerate] show ?thesis . qed -lemmas small_mixed_integer_solution_int_mat_gram = +lemmas small_mixed_integer_solution_int_mat_hadamard = small_mixed_integer_solution_int_mat[OF det_bound_hadamard, unfolded det_bound_hadamard_def of_int_mult of_int_of_nat_eq] end lemma of_int_hom_le: "(of_int_hom.vec_hom v :: 'a :: linordered_field vec) \ of_int_hom.vec_hom w \ v \ w" unfolding less_eq_vec_def by auto lemma of_int_hom_less: "(of_int_hom.vec_hom v :: 'a :: linordered_field vec) <\<^sub>v of_int_hom.vec_hom w \ v <\<^sub>v w" unfolding less_vec_def by auto lemma Ints_vec_to_int_vec: assumes "v \ \\<^sub>v" shows "\ w. v = map_vec of_int w" proof - have "\ i. \ x. i < dim_vec v \ v $ i = of_int x" using assms unfolding Ints_vec_def Ints_def by auto from choice[OF this] obtain x where "\ i. i < dim_vec v \ v $ i = of_int (x i)" by auto thus ?thesis by (intro exI[of _ "vec (dim_vec v) x"], auto) qed lemma small_integer_solution: fixes A\<^sub>1 :: "int mat" assumes db: "is_det_bound db" and A1: "A\<^sub>1 \ carrier_mat nr\<^sub>1 n" and A2: "A\<^sub>2 \ carrier_mat nr\<^sub>2 n" and b1: "b\<^sub>1 \ carrier_vec nr\<^sub>1" and b2: "b\<^sub>2 \ carrier_vec nr\<^sub>2" and A1Bnd: "A\<^sub>1 \ Bounded_mat Bnd" and b1Bnd: "b\<^sub>1 \ Bounded_vec Bnd" and A2Bnd: "A\<^sub>2 \ Bounded_mat Bnd" and b2Bnd: "b\<^sub>2 \ Bounded_vec Bnd" and x: "x \ carrier_vec n" and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \ b\<^sub>1" and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2" and non_degenerate: "nr\<^sub>1 \ 0 \ nr\<^sub>2 \ 0 \ Bnd \ 0" shows "\ x. x \ carrier_vec n \ A\<^sub>1 *\<^sub>v x \ b\<^sub>1 \ A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \ x \ Bounded_vec (of_nat (n+1) * db n Bnd)" proof - let ?oi = rat_of_int let ?x = "map_vec ?oi x" let ?oiM = "map_mat ?oi" let ?oiv = "map_vec ?oi" from x have xx: "?x \ carrier_vec n" by auto have Int: "?x \ indexed_Ints_vec UNIV" unfolding indexed_Ints_vec_def Ints_def by auto interpret gram_schmidt_floor n "TYPE(rat)" . from small_mixed_integer_solution_int_mat[OF db A1 A2 b1 b2 A1Bnd b1Bnd A2Bnd b2Bnd xx Int _ _ non_degenerate, folded of_int_hom.mult_mat_vec_hom[OF A1 x] of_int_hom.mult_mat_vec_hom[OF A2 x], unfolded of_int_hom_less of_int_hom_le, OF sol_nonstrict sol_strict, folded indexed_Ints_vec_UNIV] obtain x where x: "x \ carrier_vec n" and xI: "x \ \\<^sub>v" and le: "?oiM A\<^sub>1 *\<^sub>v x \ ?oiv b\<^sub>1" and less: "?oiM A\<^sub>2 *\<^sub>v x <\<^sub>v ?oiv b\<^sub>2" and Bnd: "x \ Bounded_vec (?oi (int (n + 1) * db n Bnd))" by blast from Ints_vec_to_int_vec[OF xI] obtain xI where xI: "x = ?oiv xI" by auto from x[unfolded xI] have x: "xI \ carrier_vec n" by auto from le[unfolded xI, folded of_int_hom.mult_mat_vec_hom[OF A1 x], unfolded of_int_hom_le] have le: "A\<^sub>1 *\<^sub>v xI \ b\<^sub>1" . from less[unfolded xI, folded of_int_hom.mult_mat_vec_hom[OF A2 x], unfolded of_int_hom_less] have less: "A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2" . show ?thesis proof (intro exI[of _ xI] conjI x le less) show "xI \ Bounded_vec (int (n + 1) * db n Bnd)" unfolding Bounded_vec_def proof clarsimp fix i assume i: "i < dim_vec xI" with Bnd[unfolded Bounded_vec_def] have "\x $ i\ \ ?oi (int (n + 1) * db n Bnd)" by (auto simp: xI) also have "\x $ i\ = ?oi (\xI $ i\)" unfolding xI using i by simp finally show "\xI $ i\ \ (1 + int n) * db n Bnd" unfolding of_int_le_iff by auto qed qed qed corollary small_integer_solution_nonstrict: fixes A :: "int mat" assumes db: "is_det_bound db" and A: "A \ carrier_mat nr n" and b: "b \ carrier_vec nr" and ABnd: "A \ Bounded_mat Bnd" and bBnd: "b \ Bounded_vec Bnd" and x: "x \ carrier_vec n" and sol: "A *\<^sub>v x \ b" and non_degenerate: "nr \ 0 \ Bnd \ 0" shows "\ y. y \ carrier_vec n \ A *\<^sub>v y \ b \ y \ Bounded_vec (of_nat (n+1) * db n Bnd)" proof - let ?A2 = "0\<^sub>m 0 n :: int mat" let ?b2 = "0\<^sub>v 0 :: int vec" from non_degenerate have degen: "nr \ 0 \ (0 :: nat) \ 0 \ Bnd \ 0" by auto have "\y. y \ carrier_vec n \ A *\<^sub>v y \ b \ ?A2 *\<^sub>v y <\<^sub>v ?b2 \ y \ Bounded_vec (of_nat (n+1) * db n Bnd)" apply (rule small_integer_solution[OF db A _ b _ ABnd bBnd _ _ x sol _ degen]) by (auto simp: Bounded_mat_def Bounded_vec_def less_vec_def) thus ?thesis by blast qed -lemmas small_integer_solution_nonstrict_gram = +lemmas small_integer_solution_nonstrict_hadamard = small_integer_solution_nonstrict[OF det_bound_hadamard, unfolded det_bound_hadamard_def] end