[STATEMENT]
lemma small_mixed_integer_solution_main: fixes A\<^sub>1 :: "'a mat"
  assumes db: "is_det_bound db"
    and A1: "A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n"
    and A2: "A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n"
    and b1: "b\<^sub>1 \<in> carrier_vec nr\<^sub>1"
    and b2: "b\<^sub>2 \<in> carrier_vec nr\<^sub>2"
    and A1Bnd: "A\<^sub>1 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)"
    and b1Bnd: "b\<^sub>1 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
    and A2Bnd: "A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)"
    and b2Bnd: "b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
    and x: "x \<in> carrier_vec n"
    and xI: "x \<in> indexed_Ints_vec I"
    and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1"
    and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2"
  shows "\<exists> x.
  x \<in> carrier_vec n \<and>
  x \<in> indexed_Ints_vec I \<and>
  A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and>
  A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and>
  x \<in> Bounded_vec (of_int (of_nat (n + 1) * db n (max 1 Bnd)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
let ?oi = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
let ?Bnd = "?oi Bnd"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
define B where "B = ?oi (db n (max 1 Bnd))"
[PROOF STATE]
proof (state)
this:
B = of_int (db n (max 1 Bnd))

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
define A where "A = A\<^sub>1 @\<^sub>r A\<^sub>2"
[PROOF STATE]
proof (state)
this:
A = A\<^sub>1 @\<^sub>r A\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
define b where "b = b\<^sub>1 @\<^sub>v b\<^sub>2"
[PROOF STATE]
proof (state)
this:
b = b\<^sub>1 @\<^sub>v b\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
define nr where "nr = nr\<^sub>1 + nr\<^sub>2"
[PROOF STATE]
proof (state)
this:
nr = nr\<^sub>1 + nr\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have B0: "B \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> B
[PROOF STEP]
unfolding B_def of_int_0_le_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> db n (max 1 Bnd)
[PROOF STEP]
by (rule is_det_bound_ge_zero[OF db], auto)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> B

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
note defs = A_def b_def nr_def
[PROOF STATE]
proof (state)
this:
A = A\<^sub>1 @\<^sub>r A\<^sub>2
b = b\<^sub>1 @\<^sub>v b\<^sub>2
nr = nr\<^sub>1 + nr\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from A1 A2
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
[PROOF STEP]
have A: "A \<in> carrier_mat nr n"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. A \<in> carrier_mat nr n
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. A\<^sub>1 @\<^sub>r A\<^sub>2 \<in> carrier_mat (nr\<^sub>1 + nr\<^sub>2) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat nr n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from b1 b2
[PROOF STATE]
proof (chain)
picking this:
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
have b: "b \<in> carrier_vec nr"
[PROOF STATE]
proof (prove)
using this:
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. b \<in> carrier_vec nr
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. b\<^sub>1 @\<^sub>v b\<^sub>2 \<in> carrier_vec (nr\<^sub>1 + nr\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> carrier_vec nr

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from A1Bnd A2Bnd A1 A2
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
[PROOF STEP]
have ABnd: "A \<in> \<int>\<^sub>m \<inter> Bounded_mat ?Bnd"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. A\<^sub>1 @\<^sub>r A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
[PROOF STEP]
by (auto simp: Ints_mat_elements_mat Bounded_mat_elements_mat elements_mat_append_rows)
[PROOF STATE]
proof (state)
this:
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from b1Bnd b2Bnd b1 b2
[PROOF STATE]
proof (chain)
picking this:
b\<^sub>1 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
have bBnd: "b \<in> \<int>\<^sub>v \<inter> Bounded_vec ?Bnd"
[PROOF STATE]
proof (prove)
using this:
b\<^sub>1 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
b\<^sub>1 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. b\<^sub>1 @\<^sub>v b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
[PROOF STEP]
by (auto simp: Ints_vec_vec_set Bounded_vec_vec_set)
[PROOF STATE]
proof (state)
this:
b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from decomposition_theorem_polyhedra_1[OF A b refl, of db Bnd] ABnd bBnd db
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q X. X \<subseteq> carrier_vec n \<and> finite X \<and> Q \<subseteq> carrier_vec n \<and> finite Q \<and> polyhedron A b = convex_hull Q + cone X \<and> (is_det_bound db \<longrightarrow> A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd) \<longrightarrow> b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<longrightarrow> X \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db n (max 1 Bnd))) \<and> Q \<subseteq> Bounded_vec (of_int (db n (max 1 Bnd))))
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
is_det_bound db
[PROOF STEP]
obtain Y Z where Z: "Z \<subseteq> carrier_vec n"
    and finX: "finite Z"
    and Y: "Y \<subseteq> carrier_vec n"
    and finY: "finite Y"
    and poly: "polyhedron A b = convex_hull Y + cone Z"
    and ZBnd: "Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B"
    and YBnd: "Y \<subseteq> Bounded_vec B"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q X. X \<subseteq> carrier_vec n \<and> finite X \<and> Q \<subseteq> carrier_vec n \<and> finite Q \<and> polyhedron A b = convex_hull Q + cone X \<and> (is_det_bound db \<longrightarrow> A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd) \<longrightarrow> b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<longrightarrow> X \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db n (max 1 Bnd))) \<and> Q \<subseteq> Bounded_vec (of_int (db n (max 1 Bnd))))
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
is_det_bound db

goal (1 subgoal):
 1. (\<And>Z Y. \<lbrakk>Z \<subseteq> carrier_vec n; finite Z; Y \<subseteq> carrier_vec n; finite Y; polyhedron A b = convex_hull Y + cone Z; Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B; Y \<subseteq> Bounded_vec B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
\<exists>Q X. X \<subseteq> carrier_vec n \<and> finite X \<and> Q \<subseteq> carrier_vec n \<and> finite Q \<and> polyhedron A b = convex_hull Q + cone X \<and> (is_det_bound db \<longrightarrow> A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd) \<longrightarrow> b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<longrightarrow> X \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db n (max 1 Bnd))) \<and> Q \<subseteq> Bounded_vec (of_int (db n (max 1 Bnd))))
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
b \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
is_det_bound db

goal (1 subgoal):
 1. (\<And>Z Y. \<lbrakk>Z \<subseteq> carrier_vec n; finite Z; Y \<subseteq> carrier_vec n; finite Y; polyhedron A b = convex_hull Y + cone Z; Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db n (max 1 Bnd))); Y \<subseteq> Bounded_vec (of_int (db n (max 1 Bnd)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Z \<subseteq> carrier_vec n
finite Z
Y \<subseteq> carrier_vec n
finite Y
polyhedron A b = convex_hull Y + cone Z
Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B
Y \<subseteq> Bounded_vec B

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
let ?P = "{x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
let ?L = "?P \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have "polyhedron A b = {x \<in> carrier_vec n. A *\<^sub>v x \<le> b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polyhedron A b = {x \<in> carrier_vec n. A *\<^sub>v x \<le> b}
[PROOF STEP]
unfolding polyhedron_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier_vec n. A *\<^sub>v x \<le> b} = {x \<in> carrier_vec n. A *\<^sub>v x \<le> b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
polyhedron A b = {x \<in> carrier_vec n. A *\<^sub>v x \<le> b}

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
polyhedron A b = {x \<in> carrier_vec n. A *\<^sub>v x \<le> b}

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have "\<dots> = ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier_vec n. A *\<^sub>v x \<le> b} = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier_vec n. (A\<^sub>1 @\<^sub>r A\<^sub>2) *\<^sub>v x \<le> b\<^sub>1 @\<^sub>v b\<^sub>2} = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
by (intro Collect_cong conj_cong refl append_rows_le[OF A1 A2 b1])
[PROOF STATE]
proof (state)
this:
{x \<in> carrier_vec n. A *\<^sub>v x \<le> b} = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
polyhedron A b = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
have poly: "?P = convex_hull Y + cone Z"
[PROOF STATE]
proof (prove)
using this:
polyhedron A b = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} = convex_hull Y + cone Z
[PROOF STEP]
unfolding poly
[PROOF STATE]
proof (prove)
using this:
convex_hull Y + cone Z = {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} = convex_hull Y + cone Z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
{x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} = convex_hull Y + cone Z

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have "x \<in> ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
using x sol_nonstrict less_vec_lesseq_vec[OF sol_strict]
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n
A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1
A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2

goal (1 subgoal):
 1. x \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
note sol = this[unfolded poly]
[PROOF STATE]
proof (state)
this:
x \<in> convex_hull Y + cone Z

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from set_plus_elim[OF sol]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a b. \<lbrakk>x = a + b; a \<in> convex_hull Y; b \<in> cone Z\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain y z where xyz: "x = y + z" and
    yY: "y \<in> convex_hull Y" and zZ: "z \<in> cone Z"
[PROOF STATE]
proof (prove)
using this:
(\<And>a b. \<lbrakk>x = a + b; a \<in> convex_hull Y; b \<in> cone Z\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>y z. \<lbrakk>x = y + z; y \<in> convex_hull Y; z \<in> cone Z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y + z
y \<in> convex_hull Y
z \<in> cone Z

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from convex_hull_carrier[OF Y] yY
[PROOF STATE]
proof (chain)
picking this:
convex_hull Y \<subseteq> carrier_vec n
y \<in> convex_hull Y
[PROOF STEP]
have y: "y \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
convex_hull Y \<subseteq> carrier_vec n
y \<in> convex_hull Y

goal (1 subgoal):
 1. y \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from Caratheodory_theorem[OF Z] zZ
[PROOF STATE]
proof (chain)
picking this:
cone Z = \<Union> {finite_cone B |B. B \<subseteq> Z \<and> lin_indpt B}
z \<in> cone Z
[PROOF STEP]
obtain C where zC: "z \<in> finite_cone C" and CZ: "C \<subseteq> Z" and lin: "lin_indpt C"
[PROOF STATE]
proof (prove)
using this:
cone Z = \<Union> {finite_cone B |B. B \<subseteq> Z \<and> lin_indpt B}
z \<in> cone Z

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>z \<in> finite_cone C; C \<subseteq> Z; lin_indpt C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> finite_cone C
C \<subseteq> Z
lin_indpt C

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from subset_trans[OF CZ Z] lin
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> carrier_vec n
lin_indpt C
[PROOF STEP]
have card: "card C \<le> n"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> carrier_vec n
lin_indpt C

goal (1 subgoal):
 1. card C \<le> n
[PROOF STEP]
using dim_is_n li_le_dim(2)
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> carrier_vec n
lin_indpt C
local.dim = n
\<lbrakk>fin_dim; ?A \<subseteq> carrier_vec n; lin_indpt ?A\<rbrakk> \<Longrightarrow> card ?A \<le> local.dim

goal (1 subgoal):
 1. card C \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C \<le> n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from finite_subset[OF CZ finX]
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
have finC: "finite C"
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. finite C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite C

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from zC[unfolded finite_cone_def nonneg_lincomb_def] finC
[PROOF STATE]
proof (chain)
picking this:
z \<in> {b. \<exists>c. lincomb c (if finite C then C else {}) = b \<and> c ` (if finite C then C else {}) \<subseteq> Collect ((\<le>) (0::'a))}
finite C
[PROOF STEP]
obtain a
    where za: "z = lincomb a C" and nonneg: "\<And> u. u \<in> C \<Longrightarrow> a u \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
z \<in> {b. \<exists>c. lincomb c (if finite C then C else {}) = b \<and> c ` (if finite C then C else {}) \<subseteq> Collect ((\<le>) (0::'a))}
finite C

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>z = lincomb a C; \<And>u. u \<in> C \<Longrightarrow> (0::'a) \<le> a u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = lincomb a C
?u4 \<in> C \<Longrightarrow> (0::'a) \<le> a ?u4

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from CZ Z
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> Z
Z \<subseteq> carrier_vec n
[PROOF STEP]
have C: "C \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> Z
Z \<subseteq> carrier_vec n

goal (1 subgoal):
 1. C \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have z: "z \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> carrier_vec n
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. z \<in> carrier_vec n
[PROOF STEP]
unfolding za
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb a C \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have yB: "y \<in> Bounded_vec B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> Bounded_vec B
[PROOF STEP]
using yY convex_hull_bound[OF YBnd Y]
[PROOF STATE]
proof (prove)
using this:
y \<in> convex_hull Y
convex_hull Y \<subseteq> Bounded_vec B

goal (1 subgoal):
 1. y \<in> Bounded_vec B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Bounded_vec B

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
y \<in> Bounded_vec B

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
fix D
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
assume DC: "D \<subseteq> C"
[PROOF STATE]
proof (state)
this:
D \<subseteq> C

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from finite_subset[OF this finC]
[PROOF STATE]
proof (chain)
picking this:
finite D
[PROOF STEP]
have "finite D"
[PROOF STATE]
proof (prove)
using this:
finite D

goal (1 subgoal):
 1. finite D
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite D

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
hence "\<exists> a. y + lincomb a C \<in> ?L \<and> (\<forall> c \<in> C. a c \<ge> 0) \<and> (\<forall> c \<in> D. a c \<le> 1)"
[PROOF STATE]
proof (prove)
using this:
finite D

goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))
[PROOF STEP]
using DC
[PROOF STATE]
proof (prove)
using this:
finite D
D \<subseteq> C

goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))
[PROOF STEP]
proof (induct D)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>{}. a c \<le> (1::'a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> C

goal (2 subgoals):
 1. {} \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>{}. a c \<le> (1::'a))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>{}. a c \<le> (1::'a))
[PROOF STEP]
by (intro exI[of _ a], fold za xyz, insert sol_strict x xI nonneg \<open>x \<in> ?P\<close>, auto)
[PROOF STATE]
proof (state)
this:
\<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>{}. a c \<le> (1::'a))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
case (insert c D)
[PROOF STATE]
proof (state)
this:
finite D
c \<notin> D
D \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))
insert c D \<subseteq> C

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite D
c \<notin> D
D \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))
insert c D \<subseteq> C
[PROOF STEP]
obtain a where sol: "y + lincomb a C \<in> ?L"
        and a: "(\<forall> c \<in> C. a c \<ge> 0)" and D: "(\<forall> c \<in> D. a c \<le> 1)"
[PROOF STATE]
proof (prove)
using this:
finite D
c \<notin> D
D \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))
insert c D \<subseteq> C

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I; \<forall>c\<in>C. (0::'a) \<le> a c; \<forall>c\<in>D. a c \<le> (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I
\<forall>c\<in>C. (0::'a) \<le> a c
\<forall>c\<in>D. a c \<le> (1::'a)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
from insert(4) C
[PROOF STATE]
proof (chain)
picking this:
insert c D \<subseteq> C
C \<subseteq> carrier_vec n
[PROOF STEP]
have c: "c \<in> carrier_vec n" and cC: "c \<in> C"
[PROOF STATE]
proof (prove)
using this:
insert c D \<subseteq> C
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. c \<in> carrier_vec n &&& c \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> carrier_vec n
c \<in> C

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>F. a c \<le> (1::'a)); insert x F \<subseteq> C\<rbrakk> \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert x F. a c \<le> (1::'a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
proof (cases "a c > 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
 2. \<not> (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (1::'a) < a c

goal (2 subgoals):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
 2. \<not> (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (1::'a) < a c

goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
by (intro exI[of _ a], insert sol a D, auto)
[PROOF STATE]
proof (state)
this:
\<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(1::'a) < a c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
(* this is the core reasoning step where a\<^sub>c is large *)
[PROOF STATE]
proof (state)
this:
(1::'a) < a c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
let ?z = "\<lambda> d. lincomb a C - d \<cdot>\<^sub>v c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
let ?x = "\<lambda> d. y + ?z d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have lin: "lincomb a (C - {c}) \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a (C - {c}) \<in> carrier_vec n
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb a (C - {c}) \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a (C - {c}) \<in> carrier_vec n

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have id: "?z d = lincomb (\<lambda> e. if e = c then (a c - d) else a e) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - d else a e) C
[PROOF STEP]
unfolding lincomb_del2[OF finC C TrueI cC]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a c \<cdot>\<^sub>v c + lincomb a (C - {c}) - d \<cdot>\<^sub>v c = (if c = c then a c - d else a c) \<cdot>\<^sub>v c + lincomb (\<lambda>e. if e = c then a c - d else a e) (C - {c})
[PROOF STEP]
by (subst (2) lincomb_cong[OF refl, of _ _ a], insert C c lin, auto simp: diff_smult_distrib_vec)
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - d else a e) C

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - d else a e) C

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
assume le: "d \<le> a c"
[PROOF STATE]
proof (state)
this:
d \<le> a c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have "?z d \<in> finite_cone C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
[PROOF STEP]
have "\<forall>f\<in>C. 0 \<le> (\<lambda>e. if e = c then a c - d else a e) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)
[PROOF STEP]
using le a finC
[PROOF STATE]
proof (prove)
using this:
d \<le> a c
\<forall>c\<in>C. (0::'a) \<le> a c
finite C

goal (1 subgoal):
 1. \<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)

goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)

goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)

goal (1 subgoal):
 1. lincomb (\<lambda>e. if e = c then a c - d else a e) C \<in> finite_cone C
[PROOF STEP]
using le a finC
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>C. (0::'a) \<le> (if f = c then a c - d else a f)
d \<le> a c
\<forall>c\<in>C. (0::'a) \<le> a c
finite C

goal (1 subgoal):
 1. lincomb (\<lambda>e. if e = c then a c - d else a e) C \<in> finite_cone C
[PROOF STEP]
by (simp add: C lincomb_in_finite_cone)
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
hence "?z d \<in> cone Z"
[PROOF STATE]
proof (prove)
using this:
lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C

goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z
[PROOF STEP]
using CZ
[PROOF STATE]
proof (prove)
using this:
lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
C \<subseteq> Z

goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z
[PROOF STEP]
using finC local.cone_def
[PROOF STATE]
proof (prove)
using this:
lincomb a C - d \<cdot>\<^sub>v c \<in> finite_cone C
C \<subseteq> Z
finite C
cone ?Vs = {x. \<exists>Ws. finite Ws \<and> Ws \<subseteq> ?Vs \<and> x \<in> finite_cone Ws}

goal (1 subgoal):
 1. lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
hence "?x d \<in> ?P"
[PROOF STATE]
proof (prove)
using this:
lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z

goal (1 subgoal):
 1. y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
unfolding poly
[PROOF STATE]
proof (prove)
using this:
lincomb a C - d \<cdot>\<^sub>v c \<in> cone Z

goal (1 subgoal):
 1. y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> convex_hull Y + cone Z
[PROOF STEP]
by (intro set_plus_intro[OF yY], auto)
[PROOF STATE]
proof (state)
this:
y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
d \<le> a c \<Longrightarrow> y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
note sol = this
[PROOF STATE]
proof (state)
this:
d \<le> a c \<Longrightarrow> y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
d \<le> a c \<Longrightarrow> y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
fix w :: "'a vec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
assume w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have "w \<bullet> (?x d) = w \<bullet> y + w \<bullet> lincomb a C - d * (w \<bullet> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> (y + (lincomb a C - d \<cdot>\<^sub>v c)) = w \<bullet> y + w \<bullet> lincomb a C - d * (w \<bullet> c)
[PROOF STEP]
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)
[PROOF STATE]
proof (state)
this:
w \<bullet> (y + (lincomb a C - d \<cdot>\<^sub>v c)) = w \<bullet> y + w \<bullet> lincomb a C - d * (w \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?w6 \<in> carrier_vec n \<Longrightarrow> ?w6 \<bullet> (y + (lincomb a C - d \<cdot>\<^sub>v c)) = ?w6 \<bullet> y + ?w6 \<bullet> lincomb a C - d * (?w6 \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
note scalar = this
[PROOF STATE]
proof (state)
this:
?w6 \<in> carrier_vec n \<Longrightarrow> ?w6 \<bullet> (y + (lincomb a C - d \<cdot>\<^sub>v c)) = ?w6 \<bullet> y + ?w6 \<bullet> lincomb a C - d * (?w6 \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
note id sol scalar
[PROOF STATE]
proof (state)
this:
lincomb a C - d \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - d else a e) C
d \<le> a c \<Longrightarrow> y + (lincomb a C - d \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
?w6 \<in> carrier_vec n \<Longrightarrow> ?w6 \<bullet> (y + (lincomb a C - d \<cdot>\<^sub>v c)) = ?w6 \<bullet> y + ?w6 \<bullet> lincomb a C - d * (?w6 \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
lincomb a C - ?d9 \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - ?d9 else a e) C
?d9 \<le> a c \<Longrightarrow> y + (lincomb a C - ?d9 \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
?w6 \<in> carrier_vec n \<Longrightarrow> ?w6 \<bullet> (y + (lincomb a C - ?d9 \<cdot>\<^sub>v c)) = ?w6 \<bullet> y + ?w6 \<bullet> lincomb a C - ?d9 * (?w6 \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
note generic = this
[PROOF STATE]
proof (state)
this:
lincomb a C - ?d9 \<cdot>\<^sub>v c = lincomb (\<lambda>e. if e = c then a c - ?d9 else a e) C
?d9 \<le> a c \<Longrightarrow> y + (lincomb a C - ?d9 \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
?w6 \<in> carrier_vec n \<Longrightarrow> ?w6 \<bullet> (y + (lincomb a C - ?d9 \<cdot>\<^sub>v c)) = ?w6 \<bullet> y + ?w6 \<bullet> lincomb a C - ?d9 * (?w6 \<bullet> c)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
let ?fl = "(of_int (floor (a c)) :: 'a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
define p where "p = (if ?fl  = a c then a c - 1 else ?fl)"
[PROOF STATE]
proof (state)
this:
p = (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have p_lt_ac: "p < a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p < a c
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) < a c
[PROOF STEP]
using floor_less floor_of_int_eq
[PROOF STATE]
proof (prove)
using this:
?x \<notin> \<int> \<Longrightarrow> of_int \<lfloor>?x\<rfloor> < ?x
?x \<in> \<int> \<Longrightarrow> of_int \<lfloor>?x\<rfloor> = ?x

goal (1 subgoal):
 1. (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) < a c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p < a c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have p1_ge_ac: "p + 1 \<ge> a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a c \<le> p + (1::'a)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a c \<le> (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) + (1::'a)
[PROOF STEP]
using floor_correct le_less
[PROOF STATE]
proof (prove)
using this:
of_int \<lfloor>?x\<rfloor> \<le> ?x \<and> ?x < of_int (\<lfloor>?x\<rfloor> + 1)
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. a c \<le> (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) + (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a c \<le> p + (1::'a)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have p1: "p \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> p
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(1::'a) < a c

goal (1 subgoal):
 1. (1::'a) \<le> p
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
(1::'a) < a c

goal (1 subgoal):
 1. (1::'a) \<le> (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> p

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
define a' where "a' = (\<lambda>e. if e = c then a c - p else a e)"
[PROOF STATE]
proof (state)
this:
a' = (\<lambda>e. if e = c then a c - p else a e)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have lin_id: "lincomb a' C = lincomb a C - p \<cdot>\<^sub>v c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a' C = lincomb a C - p \<cdot>\<^sub>v c
[PROOF STEP]
unfolding a'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>e. if e = c then a c - p else a e) C = lincomb a C - p \<cdot>\<^sub>v c
[PROOF STEP]
using id
[PROOF STATE]
proof (prove)
using this:
swapidseq 0 id

goal (1 subgoal):
 1. lincomb (\<lambda>e. if e = c then a c - p else a e) C = lincomb a C - p \<cdot>\<^sub>v c
[PROOF STEP]
by (simp add: generic(1))
[PROOF STATE]
proof (state)
this:
lincomb a' C = lincomb a C - p \<cdot>\<^sub>v c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
hence 1: "y + lincomb a' C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}"
[PROOF STATE]
proof (prove)
using this:
lincomb a' C = lincomb a C - p \<cdot>\<^sub>v c

goal (1 subgoal):
 1. y + lincomb a' C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
using p_lt_ac generic(2)[of p]
[PROOF STATE]
proof (prove)
using this:
lincomb a' C = lincomb a C - p \<cdot>\<^sub>v c
p < a c
p \<le> a c \<Longrightarrow> y + (lincomb a C - p \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. y + lincomb a' C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a' C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have pInt: "p \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<int>
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) \<in> \<int>
[PROOF STEP]
using sol
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I

goal (1 subgoal):
 1. (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) \<in> \<int>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> \<int>

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have "C \<subseteq> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> indexed_Ints_vec I
[PROOF STEP]
using CZ ZBnd
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> Z
Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B

goal (1 subgoal):
 1. C \<subseteq> indexed_Ints_vec I
[PROOF STEP]
using indexed_Ints_vec_subset
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> Z
Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B
\<int>\<^sub>v \<subseteq> indexed_Ints_vec ?I

goal (1 subgoal):
 1. C \<subseteq> indexed_Ints_vec I
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
C \<subseteq> indexed_Ints_vec I

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
hence "c \<in> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> indexed_Ints_vec I

goal (1 subgoal):
 1. c \<in> indexed_Ints_vec I
[PROOF STEP]
using cC
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> indexed_Ints_vec I
c \<in> C

goal (1 subgoal):
 1. c \<in> indexed_Ints_vec I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
hence pvindInts: "p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
using this:
c \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I
[PROOF STEP]
unfolding indexed_Ints_vec_def
[PROOF STATE]
proof (prove)
using this:
c \<in> {x. \<forall>i<dim_vec x. i \<in> I \<longrightarrow> x $ i \<in> \<int>}

goal (1 subgoal):
 1. p \<cdot>\<^sub>v c \<in> {x. \<forall>i<dim_vec x. i \<in> I \<longrightarrow> x $ i \<in> \<int>}
[PROOF STEP]
using pInt
[PROOF STATE]
proof (prove)
using this:
c \<in> {x. \<forall>i<dim_vec x. i \<in> I \<longrightarrow> x $ i \<in> \<int>}
p \<in> \<int>

goal (1 subgoal):
 1. p \<cdot>\<^sub>v c \<in> {x. \<forall>i<dim_vec x. i \<in> I \<longrightarrow> x $ i \<in> \<int>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have prod: "A\<^sub>2 *\<^sub>v (?x b) \<in> carrier_vec nr\<^sub>2" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v (y + (lincomb a C - b \<cdot>\<^sub>v c)) \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
using A2 C c y
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
C \<subseteq> carrier_vec n
c \<in> carrier_vec n
y \<in> carrier_vec n

goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v (y + (lincomb a C - b \<cdot>\<^sub>v c)) \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>2 *\<^sub>v (y + (lincomb a C - ?b4 \<cdot>\<^sub>v c)) \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have 2: "y + lincomb a' C \<in> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + lincomb a' C \<in> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2}
[PROOF STEP]
unfolding lin_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + (lincomb a C - p \<cdot>\<^sub>v c) \<in> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2}
[PROOF STEP]
proof (intro less_vecI[OF prod b2] CollectI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
assume i: "i < nr\<^sub>2"
[PROOF STATE]
proof (state)
this:
i < nr\<^sub>2

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
from sol
[PROOF STATE]
proof (chain)
picking this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I
[PROOF STEP]
have "A\<^sub>2 *\<^sub>v (?x 0) <\<^sub>v b\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I

goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) <\<^sub>v b\<^sub>2
[PROOF STEP]
using y C c
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I
y \<in> carrier_vec n
C \<subseteq> carrier_vec n
c \<in> carrier_vec n

goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) <\<^sub>v b\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) <\<^sub>v b\<^sub>2

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
from less_vecD[OF this b2 i]
[PROOF STATE]
proof (chain)
picking this:
(A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
have lt: "row A\<^sub>2 i \<bullet> ?x 0 < b\<^sub>2 $ i"
[PROOF STATE]
proof (prove)
using this:
(A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
using A2 i
[PROOF STATE]
proof (prove)
using this:
(A\<^sub>2 *\<^sub>v (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
i < nr\<^sub>2

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) < b\<^sub>2 $ i

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
from generic(2)[of "a c"] i A2
[PROOF STATE]
proof (chain)
picking this:
a c \<le> a c \<Longrightarrow> y + (lincomb a C - a c \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
i < nr\<^sub>2
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
[PROOF STEP]
have le: "row A\<^sub>2 i \<bullet> ?x (a c) \<le> b\<^sub>2 $ i"
[PROOF STATE]
proof (prove)
using this:
a c \<le> a c \<Longrightarrow> y + (lincomb a C - a c \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2}
i < nr\<^sub>2
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - a c \<cdot>\<^sub>v c)) \<le> b\<^sub>2 $ i
[PROOF STEP]
unfolding less_eq_vec_def
[PROOF STATE]
proof (prove)
using this:
a c \<le> a c \<Longrightarrow> y + (lincomb a C - a c \<cdot>\<^sub>v c) \<in> {x \<in> carrier_vec n. (dim_vec (A\<^sub>1 *\<^sub>v x) = dim_vec b\<^sub>1 \<and> (\<forall>i<dim_vec b\<^sub>1. (A\<^sub>1 *\<^sub>v x) $ i \<le> b\<^sub>1 $ i)) \<and> dim_vec (A\<^sub>2 *\<^sub>v x) = dim_vec b\<^sub>2 \<and> (\<forall>i<dim_vec b\<^sub>2. (A\<^sub>2 *\<^sub>v x) $ i \<le> b\<^sub>2 $ i)}
i < nr\<^sub>2
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - a c \<cdot>\<^sub>v c)) \<le> b\<^sub>2 $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - a c \<cdot>\<^sub>v c)) \<le> b\<^sub>2 $ i

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
from A2 i
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
i < nr\<^sub>2
[PROOF STEP]
have A2icarr: "row A\<^sub>2 i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
i < nr\<^sub>2

goal (1 subgoal):
 1. row A\<^sub>2 i \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A\<^sub>2 i \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
have "row A\<^sub>2 i \<bullet> ?x p < b\<^sub>2 $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
define lhs where "lhs = row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - b\<^sub>2 $ i"
[PROOF STATE]
proof (state)
this:
lhs = row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - b\<^sub>2 $ i

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
define mult where "mult = row A\<^sub>2 i \<bullet> c"
[PROOF STATE]
proof (state)
this:
mult = row A\<^sub>2 i \<bullet> c

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
have le2: "lhs \<le> a c * mult"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhs \<le> a c * mult
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - a c \<cdot>\<^sub>v c)) \<le> b\<^sub>2 $ i

goal (1 subgoal):
 1. lhs \<le> a c * mult
[PROOF STEP]
unfolding generic(3)[OF A2icarr] lhs_def mult_def
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - a c * (row A\<^sub>2 i \<bullet> c) \<le> b\<^sub>2 $ i

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - b\<^sub>2 $ i \<le> a c * (row A\<^sub>2 i \<bullet> c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lhs \<le> a c * mult

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
have lt2: "lhs < 0 * mult"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhs < (0::'a) * mult
[PROOF STEP]
using lt
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - (0::'a) \<cdot>\<^sub>v c)) < b\<^sub>2 $ i

goal (1 subgoal):
 1. lhs < (0::'a) * mult
[PROOF STEP]
unfolding generic(3)[OF A2icarr] lhs_def
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - (0::'a) * (row A\<^sub>2 i \<bullet> c) < b\<^sub>2 $ i

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - b\<^sub>2 $ i < (0::'a) * mult
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lhs < (0::'a) * mult

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
from le2 lt2
[PROOF STATE]
proof (chain)
picking this:
lhs \<le> a c * mult
lhs < (0::'a) * mult
[PROOF STEP]
have "lhs < p * mult"
[PROOF STATE]
proof (prove)
using this:
lhs \<le> a c * mult
lhs < (0::'a) * mult

goal (1 subgoal):
 1. lhs < p * mult
[PROOF STEP]
using p_lt_ac p1 True
[PROOF STATE]
proof (prove)
using this:
lhs \<le> a c * mult
lhs < (0::'a) * mult
p < a c
(1::'a) \<le> p
(1::'a) < a c

goal (1 subgoal):
 1. lhs < p * mult
[PROOF STEP]
by (smt dual_order.strict_trans linorder_neqE_linordered_idom
                  mult_less_cancel_right not_less zero_less_one_class.zero_less_one)
[PROOF STATE]
proof (state)
this:
lhs < p * mult

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lhs < p * mult
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lhs < p * mult

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
[PROOF STEP]
unfolding generic(3)[OF A2icarr] lhs_def mult_def
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - b\<^sub>2 $ i < p * (row A\<^sub>2 i \<bullet> c)

goal (1 subgoal):
 1. row A\<^sub>2 i \<bullet> y + row A\<^sub>2 i \<bullet> lincomb a C - p * (row A\<^sub>2 i \<bullet> c) < b\<^sub>2 $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i

goal (1 subgoal):
 1. \<And>i. i < nr\<^sub>2 \<Longrightarrow> (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
thus "(A\<^sub>2 *\<^sub>v ?x p) $ i < b\<^sub>2 $ i"
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i

goal (1 subgoal):
 1. (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
using i A2
[PROOF STATE]
proof (prove)
using this:
row A\<^sub>2 i \<bullet> (y + (lincomb a C - p \<cdot>\<^sub>v c)) < b\<^sub>2 $ i
i < nr\<^sub>2
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. (A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A\<^sub>2 *\<^sub>v (y + (lincomb a C - p \<cdot>\<^sub>v c))) $ i < b\<^sub>2 $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y + lincomb a' C \<in> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2}

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have "y + lincomb a' C = y + lincomb a C - p \<cdot>\<^sub>v c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + lincomb a' C = y + lincomb a C - p \<cdot>\<^sub>v c
[PROOF STEP]
by (subst lin_id, insert y C c, auto simp: add_diff_eq_vec)
[PROOF STATE]
proof (state)
this:
y + lincomb a' C = y + lincomb a C - p \<cdot>\<^sub>v c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y + lincomb a' C = y + lincomb a C - p \<cdot>\<^sub>v c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have "\<dots> \<in> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y + lincomb a C - p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I
[PROOF STEP]
using sol
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I

goal (1 subgoal):
 1. y + lincomb a C - p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I
[PROOF STEP]
by(intro diff_indexed_Ints_vec[OF _ _ _ pvindInts, of _ n ], insert c C, auto)
[PROOF STATE]
proof (state)
this:
y + lincomb a C - p \<cdot>\<^sub>v c \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y + lincomb a' C \<in> indexed_Ints_vec I
[PROOF STEP]
have 3: "y + lincomb a' C \<in> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
using this:
y + lincomb a' C \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. y + lincomb a' C \<in> indexed_Ints_vec I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a' C \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have 4: "\<forall>c\<in>C. 0 \<le> a' c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C. (0::'a) \<le> a' c
[PROOF STEP]
unfolding a'_def p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ca\<in>C. (0::'a) \<le> (if ca = c then a c - (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) else a ca)
[PROOF STEP]
using p_lt_ac a
[PROOF STATE]
proof (prove)
using this:
p < a c
\<forall>c\<in>C. (0::'a) \<le> a c

goal (1 subgoal):
 1. \<forall>ca\<in>C. (0::'a) \<le> (if ca = c then a c - (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>) else a ca)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C. (0::'a) \<le> a' c

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
have 5: "\<forall>c\<in>insert c D. a' c \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>insert c D. a' c \<le> (1::'a)
[PROOF STEP]
unfolding a'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ca\<in>insert c D. (if ca = c then a c - p else a ca) \<le> (1::'a)
[PROOF STEP]
using p1_ge_ac D p_def
[PROOF STATE]
proof (prove)
using this:
a c \<le> p + (1::'a)
\<forall>c\<in>D. a c \<le> (1::'a)
p = (if of_int \<lfloor>a c\<rfloor> = a c then a c - (1::'a) else of_int \<lfloor>a c\<rfloor>)

goal (1 subgoal):
 1. \<forall>ca\<in>insert c D. (if ca = c then a c - p else a ca) \<le> (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>insert c D. a' c \<le> (1::'a)

goal (1 subgoal):
 1. (1::'a) < a c \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))
[PROOF STEP]
by (intro exI[of _ a'], intro conjI IntI 1 2 3 4 5)
[PROOF STATE]
proof (state)
this:
\<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>insert c D. a c \<le> (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>D. a c \<le> (1::'a))

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?D6 \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>?D6. a c \<le> (1::'a))

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from this[of C]
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>C. a c \<le> (1::'a))
[PROOF STEP]
obtain a where
    sol: "y + lincomb a C \<in> ?L" and bnds: "(\<forall> c \<in> C. a c \<ge> 0)" "(\<forall> c \<in> C. a c \<le> 1)"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> C \<Longrightarrow> \<exists>a. y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I \<and> (\<forall>c\<in>C. (0::'a) \<le> a c) \<and> (\<forall>c\<in>C. a c \<le> (1::'a))

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I; \<forall>c\<in>C. (0::'a) \<le> a c; \<forall>c\<in>C. a c \<le> (1::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a C \<in> {x \<in> carrier_vec n. A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x \<le> b\<^sub>2} \<inter> {x. A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2} \<inter> indexed_Ints_vec I
\<forall>c\<in>C. (0::'a) \<le> a c
\<forall>c\<in>C. a c \<le> (1::'a)

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
proof (intro exI[of _ "y + lincomb a C"] conjI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from ZBnd CZ
[PROOF STATE]
proof (chain)
picking this:
Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B
C \<subseteq> Z
[PROOF STEP]
have BndC: "C \<subseteq> Bounded_vec B" and IntC: "C \<subseteq> \<int>\<^sub>v"
[PROOF STATE]
proof (prove)
using this:
Z \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec B
C \<subseteq> Z

goal (1 subgoal):
 1. C \<subseteq> Bounded_vec B &&& C \<subseteq> \<int>\<^sub>v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<subseteq> Bounded_vec B
C \<subseteq> \<int>\<^sub>v

goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have "lincomb a C \<in> Bounded_vec (of_nat n * B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a C \<in> Bounded_vec (of_nat n * B)
[PROOF STEP]
using lincomb_card_bound[OF BndC C B0 _ card] bnds
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> C \<Longrightarrow> \<bar>?c x\<bar> \<le> (1::'a)) \<Longrightarrow> lincomb ?c C \<in> Bounded_vec (of_nat n * B)
\<forall>c\<in>C. (0::'a) \<le> a c
\<forall>c\<in>C. a c \<le> (1::'a)

goal (1 subgoal):
 1. lincomb a C \<in> Bounded_vec (of_nat n * B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a C \<in> Bounded_vec (of_nat n * B)

goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
from sum_in_Bounded_vecI[OF yB this y] C
[PROOF STATE]
proof (chain)
picking this:
lincomb a C \<in> carrier_vec n \<Longrightarrow> y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)
C \<subseteq> carrier_vec n
[PROOF STEP]
have "y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)"
[PROOF STATE]
proof (prove)
using this:
lincomb a C \<in> carrier_vec n \<Longrightarrow> y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)
C \<subseteq> carrier_vec n

goal (1 subgoal):
 1. y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)

goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y + lincomb a C \<in> Bounded_vec (B + of_nat n * B)

goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
have "B + of_nat n * B = of_nat (n+1) * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B + of_nat n * B = of_nat (n + 1) * B
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
B + of_nat n * B = of_nat (n + 1) * B

goal (5 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
 5. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y + lincomb a C \<in> Bounded_vec (of_nat (n + 1) * B)
[PROOF STEP]
show "y + lincomb a C \<in> Bounded_vec (of_int (of_nat (n + 1) * db n (max 1 Bnd)))"
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> Bounded_vec (of_nat (n + 1) * B)

goal (1 subgoal):
 1. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
y + lincomb a C \<in> Bounded_vec (of_nat (n + 1) * of_int (db n (max 1 Bnd)))

goal (1 subgoal):
 1. y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + lincomb a C \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))

goal (4 subgoals):
 1. y + lincomb a C \<in> carrier_vec n
 2. y + lincomb a C \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v (y + lincomb a C) \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v (y + lincomb a C) <\<^sub>v b\<^sub>2
[PROOF STEP]
qed (insert sol, auto)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))

goal:
No subgoals!
[PROOF STEP]
qed