Theory Mixed_Integer_Solutions

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 "<v" 50) where
  "v <v w = (dim_vec v = dim_vec w  ( i < dim_vec w. v $ i < w $ i))"

lemma less_vecD: assumes "v <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 <v w"
  using assms unfolding less_vec_def by auto

lemma less_vec_lesseq_vec: "v <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 A1 :: "'a mat"
  assumes db: "is_det_bound db"
    and A1: "A1  carrier_mat nr1 n"
    and A2: "A2  carrier_mat nr2 n"
    and b1: "b1  carrier_vec nr1"
    and b2: "b2  carrier_vec nr2"
    and A1Bnd: "A1  m  Bounded_mat (of_int Bnd)"
    and b1Bnd: "b1  v  Bounded_vec (of_int Bnd)"
    and A2Bnd: "A2  m  Bounded_mat (of_int Bnd)"
    and b2Bnd: "b2  v  Bounded_vec (of_int Bnd)"
    and x: "x  carrier_vec n"
    and xI: "x  indexed_Ints_vec I"
    and sol_nonstrict: "A1 *v x  b1"
    and sol_strict: "A2 *v x <v b2"
  shows " x.
  x  carrier_vec n 
  x  indexed_Ints_vec I 
  A1 *v x  b1 
  A2 *v x <v b2 
  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 = A1 @r A2"
  define b where "b = b1 @v b2"
  define nr where "nr = nr1 + nr2"
  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  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  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  v  Bounded_vec B"
    and YBnd: "Y  Bounded_vec B" unfolding B_def by blast
  let ?P = "{x  carrier_vec n. A1 *v x  b1  A2 *v x  b2}"
  let ?L = "?P  {x. A2 *v x <v b2}  indexed_Ints_vec I"
  have "polyhedron A b = {x  carrier_vec n. A *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 ac is large *)
        let ?z = "λ d. lincomb a C - d 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 "fC. 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 v c" unfolding a'_def using id
          by (simp add: generic(1))
        hence 1: "y + lincomb a' C  {x  carrier_vec n. A1 *v x  b1  A2 *v x  b2}"
          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 v c  indexed_Ints_vec I" unfolding indexed_Ints_vec_def using pInt by simp
        have prod: "A2 *v (?x b)  carrier_vec nr2" for b using A2 C c y by auto
        have 2: "y + lincomb a' C  {x. A2 *v x <v b2}" unfolding lin_id
        proof (intro less_vecI[OF prod b2] CollectI)
          fix i
          assume i: "i < nr2"
          from sol have "A2 *v (?x 0) <v b2" using y C c by auto
          from less_vecD[OF this b2 i]
          have lt: "row A2 i  ?x 0 < b2 $ i" using A2 i by auto
          from generic(2)[of "a c"] i A2
          have le: "row A2 i  ?x (a c)  b2 $ i"
            unfolding less_eq_vec_def by auto
          from A2 i have A2icarr: "row A2 i  carrier_vec n" by auto
          have "row A2 i  ?x p < b2 $ i"
          proof -
            define lhs where "lhs = row A2 i  y + row A2 i  lincomb a C - b2 $ i"
            define mult where "mult = row A2 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 "(A2 *v ?x p) $ i < b2 $ i" using i A2 by auto
        qed
        have "y + lincomb a' C = y + lincomb a C - p 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: "cC. 0  a' c" unfolding a'_def p_def using p_lt_ac a by auto
        have 5: "cinsert 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  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 A1 :: "'a mat"
  assumes db: "is_det_bound db" 
    and A1: "A1  carrier_mat nr1 n"
    and A2: "A2  carrier_mat nr2 n"
    and b1: "b1  carrier_vec nr1"
    and b2: "b2  carrier_vec nr2"
    and A1Bnd: "A1  m  Bounded_mat (of_int Bnd)"
    and b1Bnd: "b1  v  Bounded_vec (of_int Bnd)"
    and A2Bnd: "A2  m  Bounded_mat (of_int Bnd)"
    and b2Bnd: "b2  v  Bounded_vec (of_int Bnd)"
    and x: "x  carrier_vec n"
    and xI: "x  indexed_Ints_vec I"
    and sol_nonstrict: "A1 *v x  b1"
    and sol_strict: "A2 *v x <v b2"
    and non_degenerate: "nr1  0  nr2  0  Bnd  0" 
  shows " x.
  x  carrier_vec n 
  x  indexed_Ints_vec I 
  A1 *v x  b1 
  A2 *v x <v b2 
  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  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 = 0m 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: "A1 = 0m nr1 n" and nr1: "nr1  0  Bnd  0" 
      by auto
    from main[OF A2 A2Bnd] have A2: "A2 = 0m nr2 n" and nr2: "nr2  0  Bnd  0" 
      by auto
    let ?x = "0v n" 
    show ?thesis
    proof (intro exI[of _ ?x] conjI)
      show "A1 *v ?x  b1" using sol_nonstrict x unfolding A1 by auto
      show "A2 *v ?x <v b2" 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)  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)  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: "A1  carrier_mat nr1 n"
    and A2: "A2  carrier_mat nr2 n"
    and b1: "b1  carrier_vec nr1"
    and b2: "b2  carrier_vec nr2"
    and A1Bnd: "A1  Bounded_mat Bnd"
    and b1Bnd: "b1  Bounded_vec Bnd"
    and A2Bnd: "A2  Bounded_mat Bnd"
    and b2Bnd: "b2  Bounded_vec Bnd"
    and x: "x  carrier_vec n"
    and xI: "x  indexed_Ints_vec I"
    and sol_nonstrict: "map_mat of_int A1 *v x  map_vec of_int b1"
    and sol_strict: "map_mat of_int A2 *v x <v map_vec of_int b2"
    and non_degenerate: "nr1  0  nr2  0  Bnd  0" 
  shows " x :: 'a vec.
  x  carrier_vec n 
  x  indexed_Ints_vec I 
  map_mat of_int A1 *v x  map_vec of_int b1 
  map_mat of_int A2 *v x <v map_vec of_int b2 
  x  Bounded_vec (of_int (of_nat (n+1) * db n Bnd))"
proof -
  let ?oi = "of_int :: int  'a" 
  let ?A1 = "map_mat ?oi A1" 
  let ?A2 = "map_mat ?oi A2" 
  let ?b1 = "map_vec ?oi b1" 
  let ?b2 = "map_vec ?oi b2" 
  let ?Bnd = "?oi Bnd" 
  from A1 have A1': "?A1  carrier_mat nr1 n" by auto
  from A2 have A2': "?A2  carrier_mat nr2 n" by auto
  from b1 have b1': "?b1  carrier_vec nr1" by auto
  from b2 have b2': "?b2  carrier_vec nr2" 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_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) <v of_int_hom.vec_hom w  v <v w"
  unfolding less_vec_def by auto

lemma Ints_vec_to_int_vec: assumes "v  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 A1 :: "int mat"
  assumes db: "is_det_bound db" 
    and A1: "A1  carrier_mat nr1 n"
    and A2: "A2  carrier_mat nr2 n"
    and b1: "b1  carrier_vec nr1"
    and b2: "b2  carrier_vec nr2"
    and A1Bnd: "A1  Bounded_mat Bnd"
    and b1Bnd: "b1  Bounded_vec Bnd"
    and A2Bnd: "A2  Bounded_mat Bnd"
    and b2Bnd: "b2  Bounded_vec Bnd"
    and x: "x  carrier_vec n"
    and sol_nonstrict: "A1 *v x  b1"
    and sol_strict: "A2 *v x <v b2"
    and non_degenerate: "nr1  0  nr2  0  Bnd  0" 
  shows " x.
    x  carrier_vec n 
    A1 *v x  b1 
    A2 *v x <v b2 
    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  v" and
    le: "?oiM A1 *v x  ?oiv b1" and
    less: "?oiM A2 *v x <v ?oiv b2" 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: "A1 *v xI  b1" .
  from less[unfolded xI, folded of_int_hom.mult_mat_vec_hom[OF A2 x], unfolded of_int_hom_less]
  have less: "A2 *v xI <v b2" .
  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 *v x  b"
    and non_degenerate: "nr  0  Bnd  0" 
  shows " y.
  y  carrier_vec n 
  A *v y  b 
  y  Bounded_vec (of_nat (n+1) * db n Bnd)"
proof -
  let ?A2 = "0m 0 n :: int mat"
  let ?b2 = "0v 0 :: int vec"
  from non_degenerate have degen: "nr  0  (0 :: nat)  0  Bnd  0" by auto
  have "y. y  carrier_vec n  A *v y  b  ?A2 *v y <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_hadamard = 
  small_integer_solution_nonstrict[OF det_bound_hadamard, unfolded det_bound_hadamard_def]


end