Theory LP_Preliminaries

theory LP_Preliminaries
imports More_Jordan_Normal_Forms Matrix_LinPoly
theory LP_Preliminaries
 imports 
    More_Jordan_Normal_Forms
    Matrix_LinPoly
    Jordan_Normal_Form.Matrix_Impl
    Farkas.Simplex_for_Reals
    "HOL-Library.Mapping"
begin

(*
        Component wise greater equal constraints for vector b starting at index 
            ‹ [xindex, xindex+1,…,xindex+n] ≥ [b0, b1,…,bn] › 
*)

fun vars_from_index_geq_vec where
  "vars_from_index_geq_vec index b = [GEQ (lp_monom 1 (i+index)) (b$i). i ← [0..<dim_vec b]]"


lemma constraints_set_vars_geq_vec_def:
  "set (vars_from_index_geq_vec start b) = 
   {GEQ (lp_monom 1 (i+start)) (b$i) |i. i ∈ {0..<dim_vec b}}"
  using set_comprehension_list_comprehension[of 
      "(λi. GEQ (lp_monom 1 (i+start)) (b$i))" "dim_vec b"] by auto

lemma vars_from_index_geq_sat:
  assumes "⟨x⟩ ⊨cs set (vars_from_index_geq_vec start b)"
  assumes "i < dim_vec b"
  shows "⟨x⟩ (i+start) ≥ b$i"
proof -
  have e_e:"GEQ (lp_monom 1 (i+start)) (b$i) ∈ set (vars_from_index_geq_vec start b)"
    using constraints_set_vars_geq_vec_def[of start b] using assms(2) by auto
  then have "⟨x⟩ ⊨c GEQ (lp_monom 1 (i+start)) (b$i)"
    using assms(1) by blast
  then have "(lp_monom 1 (i+start)) ⦃⟨x⟩⦄ ≥ (b$i)"
    using satisfies_constraint.simps(4)[of "⟨x⟩" "lp_monom 1 (i + start)" "b$i"]
    by simp
  then show ?thesis 
    by simp
qed


(* Matrix A less equal vector b (A ≤ b):
           a1 b1 c1 d1 ∙ X ≤ b_1,
           a2 b2 c2 d2 ∙ X ≤ b_2,
           ...
*)

fun mat_x_leq_vec where
    "mat_x_leq_vec A b = [LEQ (matrix_to_lpolies A!i) (b$i) . i <- [0..<dim_vec b]]"

lemma mat_x_leq_vec_sol:
  assumes "⟨x⟩ ⊨cs set (mat_x_leq_vec A b)"
  assumes "i < dim_vec b"
  shows "((matrix_to_lpolies A)!i) ⦃⟨x⟩⦄ ≤ b$i"
proof -
  have e_e: "LEQ ((matrix_to_lpolies A)!i) (b$i) ∈ set (mat_x_leq_vec A b)"
    by (simp add: assms(2))
  then have "⟨x⟩ ⊨c LEQ ((matrix_to_lpolies A)!i) (b$i)"
    using assms(1) by blast
  then show ?thesis 
    using satisfies_constraint.simps by auto
qed


(* Matrix A less equal vector b (A = b):
           a1 b1 c1 d1 ∙ X = b_1,
           a2 b2 c2 d2 ∙ X = b_2,
           ... 
*)
fun x_mat_eq_vec where
    "x_mat_eq_vec b A = [EQ (matrix_to_lpolies A!i) (b$i) . i <- [0..<dim_vec b]]"

lemma x_mat_eq_vec_sol:
  assumes "x ⊨cs set (x_mat_eq_vec b A)"
  assumes "i < dim_vec b"
  shows "((matrix_to_lpolies A)!i) ⦃ x ⦄ = b$i"
proof -
  have e_e: "EQ ((matrix_to_lpolies A)!i) (b$i) ∈ set (x_mat_eq_vec b A)"
    by (simp add: assms(2))
  then have "x ⊨c EQ ((matrix_to_lpolies A)!i) (b$i)"
    using assms(1) by blast
  then show ?thesis 
    using satisfies_constraint.simps by auto
qed


section ‹ Get different matrices into same space, without interference ›

(* Given matrix A and B create: 
               A 0
               0 B  
*)
fun two_block_non_interfering where
  "two_block_non_interfering A B = (let z1 = 0m (dim_row A) (dim_col B);
                                        z2 = 0m (dim_row B) (dim_col A) in
                                    four_block_mat A z1 z2 B)"

lemma split_two_block_non_interfering:
  assumes "split_block (two_block_non_interfering A B) (dim_row A) (dim_col A) = (Q1, Q2, Q3, Q4)"
  shows "Q1 = A" "Q4 = B"
  using split_four_block_dual_fst_lst[of A _ _ B Q1 Q2 Q3 Q4] 
    assms by auto

lemma two_block_non_interfering_dims: 
  "dim_row (two_block_non_interfering A B) = dim_row A + dim_row B"
  "dim_col (two_block_non_interfering A B) = dim_col A + dim_col B"
  by (simp)+

lemma two_block_non_interfering_zeros_are_0:
  assumes "i < dim_row A"
    and "j ≥ dim_col A"
    and "j < dim_col (two_block_non_interfering A B)"
  shows "(two_block_non_interfering A B)$$(i,j) = 0" "(two_block_non_interfering A B)$$(i,j) = 0"
  using four_block_mat_def assms two_block_non_interfering_dims[of A B] by auto 

lemma two_block_non_interfering_row_comp1:
  assumes "i <dim_row A"
  shows "row (two_block_non_interfering A B) i = row A i @v (0v (dim_col B))"
  using assms by auto

lemma two_block_non_interfering_row_comp2:
  assumes "i <dim_row (two_block_non_interfering A B)"
    and "i ≥ dim_row A"
  shows "row (two_block_non_interfering A B) i = (0v (dim_col A)) @v row B (i - dim_row A)"
  using assms by (auto)

lemma first_vec_two_block_non_inter_is_first_vec:
  assumes "dim_col A + dim_col B = dim_vec v"
  assumes "dim_row A = n"
  shows "vec_first (two_block_non_interfering A B *v v) n = A *v (vec_first v (dim_col A))"
proof
  fix i
  assume a: "i < dim_vec (A *v vec_first v (dim_col A))"
  let ?tb = "two_block_non_interfering A B"
  have i_n: "i < n" using a assms(2) by auto
  have "vec_first (?tb *v v) n $ i = vec_first (vec (dim_row ?tb) (λ i. row ?tb i ∙ v)) n $ i"
    unfolding mult_mat_vec_def by simp
  also have "... = (vec n  (λ i. row ?tb i ∙ v)) $ i"
    unfolding vec_first_def using trans_less_add1
    by (metis a assms(2) dim_mult_mat_vec index_vec  two_block_non_interfering_dims(1))
  also have "... = row ?tb i ∙ v" by (simp add: i_n)
  also have "... = (row A i @v 0v (dim_col B)) ∙ v"
    using assms(2) i_n two_block_non_interfering_row_comp1 by fastforce
  also have "... = row A i ∙ vec_first v (dim_vec (row A i)) + 
                   0v (dim_col B) ∙ vec_last v (dim_vec (0v (dim_col B)))"
    using append_split_vec_distrib_scalar_prod[of "row A i" "0v (dim_col B)" v] assms(1) by auto
  then have "vec_first (two_block_non_interfering A B *v v) n $ i = 
             row A i ∙ vec_first v (dim_vec (row A i))"
    using calculation by auto
  then show "vec_first (two_block_non_interfering A B *v v) n $ i = 
             (A *v vec_first v (dim_col A)) $ i"
    by (simp add: assms(2) i_n)
next
  have "dim_vec (A *v v) = dim_row A" using dim_vec_def dim_mult_mat_vec[of A v] by auto
  then have "dim_vec (vec_first (two_block_non_interfering A B *v v) n) = n" by auto
  then show "dim_vec (vec_first (two_block_non_interfering A B *v v) n) = 
             dim_vec (A *v vec_first v (dim_col A))"
    by (simp add: assms(2))
qed

lemma last_vec_two_block_non_inter_is_last_vec:
  assumes "dim_col A + dim_col B = dim_vec v"
  assumes "dim_row B = n"
  shows "vec_last ((two_block_non_interfering A B) *v v) n = B *v (vec_last v (dim_col B))"
proof
  fix i
  assume a: "i < dim_vec (B *v vec_last v (dim_col B))"
  let ?tb = "two_block_non_interfering A B"
  let ?vl = "(vec (dim_row ?tb) (λ i. row ?tb i ∙ v))"
  have i_n: "i < n" using  assms(2) using a by auto
  have in3: "(dim_row ?tb) - n + i ≥ dim_row A"
    by (simp add: assms(2))
  have in3': "(dim_row ?tb) - n + i < dim_row ?tb"
    by (simp add: assms(2) i_n two_block_non_interfering_dims(1)) 
  have "dim_row A + n = dim_row (two_block_non_interfering A B)"
    by (simp add: assms(2) two_block_non_interfering_dims(1))
  then have dim_a: "dim_row A = dim_row (two_block_non_interfering A B) - n"
    by (metis (no_types) diff_add_inverse2)
  have "vec_last (?tb *v v) n $ i = vec_last (vec (dim_row ?tb) (λ i. row ?tb i ∙ v)) n $ i"
    unfolding mult_mat_vec_def by auto
  also have "... = ?vl $ (dim_vec ?vl - n + i)"
    unfolding vec_last_def using i_n index_vec by blast
  also have "... = row ?tb ((dim_row ?tb) - n + i) ∙ v"
    unfolding index_vec by (simp add: assms(2) i_n two_block_non_interfering_dims(1))
  also have "... = row B i ∙ vec_last v (dim_vec (row B i))"
  proof -
    have "dim_vec (0v (dim_col A) @v row B i) = dim_vec v"
      by (simp add: ‹dim_col A + dim_col B = dim_vec v›)
    then show ?thesis using dim_a assms(1) in3' two_block_non_interfering_row_comp2
        append_split_vec_distrib_scalar_prod[of "0v (dim_col A)" "row B i" v]
      by (metis add.commute add.right_neutral diff_add_inverse
          in3 index_zero_vec(2) scalar_prod_left_zero  vec_first_carrier)
  qed
  also have "... = row B i ∙ vec_last v (dim_col B)" by simp
  thus "vec_last (two_block_non_interfering A B *v v) n $ i = (B *v vec_last v (dim_col B)) $ i"
    using assms(2) calculation i_n by auto
qed (simp add: assms(2))

lemma two_block_non_interfering_mult_decomposition:
  assumes "dim_col A + dim_col B = dim_vec v"      
  shows "two_block_non_interfering A B *v v =
         A *v vec_first v (dim_col A) @v B *v vec_last v (dim_col B)"
proof -
  let ?tb = "two_block_non_interfering A B"
  from first_vec_two_block_non_inter_is_first_vec[of A B v "dim_row A", OF assms]
  have "vec_first (?tb *v v) (dim_row A) = A *v vec_first v (dim_col A)"
    by blast
  moreover from last_vec_two_block_non_inter_is_last_vec[of A B v "dim_row B", OF assms]
  have "vec_last (?tb *v v) (dim_row B) = B *v vec_last v (dim_col B)"
    by blast
  ultimately show ?thesis using vec_first_last_append[of "?tb *v v" "(dim_row A)" "(dim_row B)"]
      dim_mult_mat_vec[of "?tb" v] two_block_non_interfering_dims(1)[of A B] 
    by (metis carrier_vec_dim_vec)
qed


(* A ≤ b   
   A = c *)
fun mat_leqb_eqc where
    "mat_leqb_eqc A b c = (let lst = matrix_to_lpolies (two_block_non_interfering A AT) in
                         [LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
                         [EQ  (lst!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)]])"

lemma mat_leqb_eqc_for_LEQ:
  assumes "i < dim_vec b"
  assumes "i < dim_row A"
  shows "(mat_leqb_eqc A b c)!i = LEQ ((matrix_to_lpolies A)!i) (b$i)"
proof -
  define lst where lst: "lst = (mat_leqb_eqc A b c)"
  define l where l: "l = matrix_to_lpolies (two_block_non_interfering A AT)"
  have ileqA: "i < dim_row A" using assms by auto
  have "l!i = vec_to_lpoly ((row A i)@v 0v (dim_row A))"
    unfolding l using two_block_non_interfering_row_comp1[of i A "AT", OF ileqA]
    by (metis ileqA lpoly_of_v_equals_v_append0 matrix_to_lp_vec_to_lpoly_row 
        trans_less_add1 two_block_non_interfering_dims(1))
  then have leq: "l!i = (matrix_to_lpolies A)!i"
    using lpoly_of_v_equals_v_append0[of "row A i" "(dim_row A)"] l
    by (simp add: ileqA)
  have *: "lst = [LEQ (l!i) (b$i) . i <- [0..<dim_vec b]] @
                         [EQ  (l!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)] ]"
    unfolding l lst by (metis mat_leqb_eqc.simps)
  have "([LEQ (l!i) (b$i). i <- [0..<dim_vec b]] @ 
         [EQ (l!i) ((b@vc)$i). i <- [dim_vec b ..< dim_vec (b@vc)]]) ! i = 
         [LEQ (l!i) (b$i). i <- [0..<dim_vec b]]!i"
    using assms(2) lst by (simp add: assms(1) nth_append)
  also have "... = LEQ (l!i) (b$i)"
    using l lst
    by (simp add: assms(1))
  finally show ?thesis
    using "*" leq lst  using mat_leqb_eqc.simps[of A b c] by auto

qed

lemma mat_leqb_eqc_for_EQ:
  assumes "dim_vec b ≤ i" and "i < dim_vec (b@vc)"
  assumes "dim_row A = dim_vec b" and "dim_col A ≥ dim_vec c"
  shows "(mat_leqb_eqc A b c)!i = 
    EQ (vec_to_lpoly (0v (dim_col A) @v row AT (i-dim_vec b))) (c$(i-dim_vec b))"
proof -
  define lst where lst: "lst = (mat_leqb_eqc A b c)"
  define l where l: "l = matrix_to_lpolies (two_block_non_interfering A AT)"
  have i_s: "i < dim_row (two_block_non_interfering A AT)"
    using assms by (simp add: assms(2) assms(3) two_block_non_interfering_dims(1))
  have l':"l!i = vec_to_lpoly ((0v (dim_col A)) @v (row AT (i - dim_vec b)))"
    using l two_block_non_interfering_row_comp2[of i A "AT", OF i_s]
      assms(1) assms(3) i_s matrix_to_lp_vec_to_lpoly_row by presburger
  have "([LEQ (l!i) (b$i) . i <- [0..<dim_vec b]] @
                         [EQ  (l!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)]])!i =
        [EQ  (l!i) ((b@vc)$i) . i <- [dim_vec b..< dim_vec (b@vc)]] ! (i - dim_vec b)"
    by (simp add: assms(1) leD nth_append)
  also have "... = EQ (l!i) ((b@vc)$i)" 
    using assms(1) assms(2) by auto
  also have "... = EQ (l!i) (c$(i-dim_vec b))"
    using assms(1) assms(2) by auto
  then show ?thesis
    using mat_leqb_eqc.simps by (metis (full_types) calculation l l')
qed

lemma mat_leqb_eqc_satisfies1:
  assumes "x ⊨cs set (mat_leqb_eqc A b c)"
  assumes "i < dim_vec b"
    and "i < dim_row A"
  shows "(matrix_to_lpolies A!i) ⦃x⦄ ≤ b$i"
proof -
  have e_e: "LEQ (matrix_to_lpolies A ! i) (b$i) ∈ set (mat_leqb_eqc A b c)"
    using mat_leqb_eqc_for_LEQ[of i b A c, OF assms(2) assms(3)] 
      nth_mem[of i "matrix_to_lpolies A"] mat_leqb_eqc.simps 
    by (metis (no_types, lifting) assms(2) diff_zero in_set_conv_nth length_append length_map 
        length_upt trans_less_add1)
  then have "x ⊨c LEQ ((matrix_to_lpolies A)!i) (b$i)"
    using assms by blast
  then show ?thesis 
    using satisfies_constraint.simps by auto
qed

lemma mat_leqb_eqc_satisfies2:
  assumes "x ⊨cs set (mat_leqb_eqc A b c)"
  assumes "dim_vec b ≤ i" and "i < dim_vec (b@vc)"
    and "dim_row A = dim_vec b" and "dim_vec c ≤ dim_col A"
  shows "(matrix_to_lpolies (two_block_non_interfering A AT) ! i) ⦃x⦄ = (b @v c) $ i"
proof -
  have e_e: "EQ (vec_to_lpoly (0v (dim_col A) @v row AT (i - dim_vec b))) (c $ (i - dim_vec b))
              ∈ set (mat_leqb_eqc A b c)"
    using assms(2) mat_leqb_eqc.simps[of A b c] 
      nth_mem[of i "(mat_leqb_eqc A b c)"]
    using  mat_leqb_eqc_for_EQ[of b i c A, OF assms(2) assms(3) assms(4) assms(5)]
    by (metis (mono_tags, lifting) add_diff_cancel_left' assms(3) diff_zero index_append_vec(2) 
        length_append length_map length_upt)
  hence sateq: "x ⊨c EQ (vec_to_lpoly (0v (dim_col A) @v 
                row AT (i - dim_vec b))) (c $ (i - dim_vec b))"
    using assms(1) by blast
  have *: "i < dim_row (two_block_non_interfering A AT)"
    by (metis assms(3) assms(4) assms(5) dual_order.order_iff_strict dual_order.strict_trans 
        index_append_vec(2) index_transpose_mat(2) nat_add_left_cancel_less 
        two_block_non_interfering_dims(1))
  have **: "dim_row A ≤ i"
    by (simp add: assms(2) assms(4))
  then have "x ⊨c EQ ((matrix_to_lpolies (two_block_non_interfering A AT))!i) ((b@vc)$i)"
    using two_block_non_interfering_row_comp2[of i A "AT", OF * **]
    by (metis "*" sateq assms(3) assms(4) index_append_vec(1) index_append_vec(2) leD
        matrix_to_lp_vec_to_lpoly_row)
  then show ?thesis
    using satisfies_constraint.simps(5) by simp
qed

lemma mat_leqb_eqc_simplex_satisfies2:
  assumes "simplex (mat_leqb_eqc A b c) = Sat x"
  assumes "dim_vec b ≤ i" and "i < dim_vec (b@vc)"
    and "dim_row A = dim_vec b" and "dim_vec c ≤ dim_col A"
  shows "(matrix_to_lpolies (two_block_non_interfering A AT) ! i) ⦃⟨x⟩⦄ = (b @v c) $ i"
  using mat_leqb_eqc_satisfies2 assms(1) assms(2) assms(3) assms(4) assms(5) simplex(3) by blast

fun index_geq_n where
  "index_geq_n i n = GEQ (lp_monom 1 i) n"

lemma index_geq_n_simplex: 
  assumes "⟨x⟩  ⊨c (index_geq_n i n)"
  shows "⟨x⟩ i ≥ n"
  using assms by simp


(* In the variables x_i to x_i+(length v) we synthesise a vector that is pointwise
       greater than v *)
fun from_index_geq0_vector where
  "from_index_geq0_vector i v = [GEQ (lp_monom 1 (i+j)) (v$j) . j <-[0..<dim_vec v]]"

lemma from_index_geq_vector_simplex: 
  assumes "x ⊨cs set (from_index_geq0_vector i v)"
  "j < dim_vec v"
  shows "x (i + j) ≥ v$j"
proof -
  have "GEQ (lp_monom 1 (i+j)) (v$j)∈ set (from_index_geq0_vector i v)"
    by (simp add: assms(2))
  moreover have "x ⊨c GEQ (lp_monom 1 (i+j)) (v$j)"
    using calculation(1) assms  by force
  ultimately show ?thesis by simp
qed

lemma from_index_geq0_vector_simplex2: 
  assumes "⟨x⟩ ⊨cs set (from_index_geq0_vector i v)"
  assumes "i ≤ j" and "j < (dim_vec v) + i"
  shows "⟨x⟩ j ≥ v$(j - i)"
  by (metis assms(1) assms(2) assms(3) from_index_geq_vector_simplex 
      le_add_diff_inverse less_diff_conv2)


(* [c1, ... cm, 01, ... 0n] * X ≥ [01, ... 0m, b1,...,bn] * X *)
fun x_times_c_geq_y_times_b where
  "x_times_c_geq_y_times_b c b = GEQPP (vec_to_lpoly (c @v 0v (dim_vec b)))
                                       (vec_to_lpoly (0v (dim_vec c) @v b))"

lemma x_times_c_geq_y_times_b_correct:
  assumes "simplex [x_times_c_geq_y_times_b c b] = Sat x"
  shows "((vec_to_lpoly (c @v 0v (dim_vec b))) ⦃ ⟨x⟩ ⦄) ≥
         ((vec_to_lpoly (0v (dim_vec c) @v b)) ⦃ ⟨x⟩ ⦄)"
 using assms simplex(3) by fastforce


(* Splitting an assignment into two vectors *)

(* The first [0...(i-1)] elements and [i...j] elements *)
definition split_i_j_x where
  "split_i_j_x i j x = (vec i ⟨x⟩, vec (j - i) (λy. ⟨x⟩ (y+i)))"

abbreviation split_n_m_x where 
  "split_n_m_x n m x ≡ split_i_j_x n (n+m) x"


lemma split_vec_dims:
  assumes "split_i_j_x i j x = (a ,b)"
  shows "dim_vec a = i" "dim_vec b = (j - i)"
  using assms(1) unfolding split_i_j_x_def by auto+

lemma split_n_m_x_abbrev_dims: 
  assumes "split_n_m_x n m x = (a, b)"
  shows "dim_vec a = n" "dim_vec b = m"
  using split_vec_dims 
  using assms apply blast
  using assms split_vec_dims(2) by fastforce

lemma split_access_fst_1:
  assumes "k < i"
  assumes "split_i_j_x i j x = (a, b)"
  shows "a $ k = ⟨x⟩ k"
  by (metis Pair_inject assms(1) assms(2) index_vec split_i_j_x_def)

lemma split_access_snd_1:
  assumes "i ≤ k" and "k < j"
  assumes "split_i_j_x i j x = (a, b)"
  shows "b $ (k - i) = ⟨x⟩ k"
proof -
  have "vec (j - i) (λn. ⟨x⟩ (n + i)) = b"
    by (metis (no_types) assms(3) prod.sel(2) split_i_j_x_def)
  then show ?thesis
    using assms(1) assms(2) by fastforce
qed

lemma split_access_fst_2:
  assumes "(x, y) = split_i_j_x i j Z"
  assumes "k < dim_vec x"
  shows "x$k = ⟨Z⟩ k"
  by (metis assms(1) assms(2) split_access_fst_1 split_vec_dims(1))

lemma split_access_snd_2:
  assumes "(x, y) = split_i_j_x i j Z"
  assumes "k < dim_vec y"
  shows "y$k = ⟨Z⟩ (k+dim_vec x)"
  using assms split_i_j_x_def[of i j Z] by auto

lemma from_index_geq0_vector_split_snd:
  assumes "⟨X⟩ ⊨cs set (from_index_geq0_vector d v)"
  assumes "(x, y) = split_n_m_x d m X"
  shows "⋀i. i < dim_vec v ⟹ i < m ⟹ y$i ≥ v$i"
  using assms unfolding split_i_j_x_def 
  using from_index_geq_vector_simplex[of d v "⟨X⟩" _] index_vec by (simp add: add.commute)

lemma split_coeff_vec_index_sum:
  assumes "(x,y) = split_i_j_x (dim_vec (lpoly_to_vec v)) l X"
  shows "(∑i = 0..<dim_vec x. Abstract_Linear_Poly.coeff v i * ⟨X⟩ i) = 
         (∑i = 0..<dim_vec x. lpoly_to_vec v $ i * x $ i)"
proof -
  from valuate_with_dim_poly[of v "⟨X⟩", symmetric] 
  have "(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * ⟨X⟩ i) = 
        (∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * x $ i)"
    by (metis (no_types, lifting) assms split_access_fst_1 split_vec_dims(1) sum.ivl_cong)
  then show ?thesis
    by (metis (no_types, lifting) assms dim_poly_dim_vec_equiv 
        lin_poly_to_vec_coeff_access split_vec_dims(1) sum.ivl_cong)
qed

lemma scalar_prod_valuation_after_split_equiv1:
  assumes "(x,y) = split_i_j_x (dim_vec (lpoly_to_vec v)) l X"
  shows "(lpoly_to_vec v) ∙ x = (v ⦃⟨X⟩⦄)"
proof -
  from valuate_with_dim_poly[of v "⟨X⟩", symmetric] 
  have 1: "(v ⦃⟨X⟩⦄) = (∑i = 0..<dim_poly v. Abstract_Linear_Poly.coeff v i * ⟨X⟩ i)" by simp
  have "(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * ⟨X⟩ i) = 
    (∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * x $ i)"
    by (metis (no_types, lifting) assms split_access_fst_1 split_vec_dims(1) sum.ivl_cong)
  also have "... =  (lpoly_to_vec v) ∙ x"
    unfolding scalar_prod_def by blast
  finally show ?thesis
    by (metis (no_types, lifting) "1" dim_poly_dim_vec_equiv lin_poly_to_vec_coeff_access 
        split_vec_dims(1) sum.ivl_cong assms)
qed


definition mat_times_vec_leq ("[_*v_]≤_" [1000,1000,100])
  where
    "[A *v x]≤b ⟷ (∀i < dim_vec b. (A *v x)$i ≤ b$i) ∧
                    (dim_row A = dim_vec b) ∧
                    (dim_col A = dim_vec x)"

definition vec_times_mat_eq ("[_v*_]=_" [1000,1000,100])
  where
    "[y v* A]=c ⟷ (∀i < dim_vec c. (AT *v y)$i = c$i) ∧
                    (dim_col AT = dim_vec y) ∧
                    (dim_row AT = dim_vec c)"

definition vec_times_mat_leq ("[_v*_]≤_" [1000,1000,100])
  where
    "[y v* A]≤c ⟷ (∀i < dim_vec c. (AT *v y)$i ≤ c$i) ∧
                    (dim_col AT = dim_vec y) ∧
                    (dim_row AT = dim_vec c)"

lemma mat_times_vec_leqI[intro]:
  assumes "dim_row A = dim_vec b"
  assumes "dim_col A = dim_vec x"
  assumes "⋀i. i < dim_vec b ⟹ (A *v x)$i ≤ b$i"
  shows "[A *v x]≤b"
  unfolding mat_times_vec_leq_def using assms by auto

lemma mat_times_vec_leqD[dest]:
  assumes "[A *v x]≤b"
  shows "dim_row A = dim_vec b" "dim_col A = dim_vec x" "⋀i. i < dim_vec b ⟹ (A *v x)$i ≤ b$i"
  using assms mat_times_vec_leq_def by blast+

lemma vec_times_mat_eqD[dest]:
  assumes "[y v* A]=c"
  shows "(∀i < dim_vec c. (AT *v y)$i = c$i)" "(dim_col AT = dim_vec y)" "(dim_row AT = dim_vec c)"
  using assms vec_times_mat_eq_def by blast+

lemma vec_times_mat_leqD[dest]:
  assumes "[y v* A]≤c"
  shows "(∀i < dim_vec c. (AT *v y)$i ≤ c$i)" "(dim_col AT = dim_vec y)" "(dim_row AT = dim_vec c)"
  using assms vec_times_mat_leq_def by blast+

lemma mat_times_vec_eqI[intro]:  
  assumes "dim_col AT = dim_vec x"
  assumes "dim_row AT = dim_vec c"
  assumes "⋀i. i < dim_vec c ⟹ (AT *v x)$i = c$i"
  shows "[x v* A]=c"
  unfolding vec_times_mat_eq_def using assms by blast

lemma mat_leqb_eqc_split_correct1:
  assumes "dim_vec b = dim_row A"
  assumes "⟨X⟩ ⊨cs set (mat_leqb_eqc A b c)"
  assumes "(x,y) = split_i_j_x (dim_col A) l X"  
  shows "[A *v x]≤b"
proof (standard, goal_cases)
  case 1
  then show ?case using assms(1)[symmetric] .
  case 2
  then show ?case using assms(3) unfolding split_i_j_x_def 
    using split_vec_dims[of  0 "dim_col A" X x y] by auto
  case (3 i)
  with mat_leqb_eqc_satisfies1[of A b c "⟨X⟩" i] 
  have m: "(matrix_to_lpolies A ! i) ⦃ ⟨X⟩ ⦄ ≤ b $ i"
    using assms(1) assms(2) by linarith
  have leq: "dim_poly (vec_to_lpoly (row A i)) ≤ dim_col A"
    using vec_to_poly_dim_less[of "row A i"] by simp
  have i: "i < dim_row A"
    using "3" assms(1) by linarith
  from two_block_non_interfering_row_comp1[of i A "AT"]
  have "row (two_block_non_interfering A AT) i = row A i @v 0v (dim_col AT)"
    using "3" assms(1) by linarith
  have "(vec_to_lpoly (row A i @v 0v (dim_col AT))) ⦃⟨X⟩⦄ = ((vec_to_lpoly (row A i)) ⦃⟨X⟩⦄)"
    using lpoly_of_v_equals_v_append0 by auto
  also have "... = (∑a = 0..<dim_poly (vec_to_lpoly (row A i)). 
                      Abstract_Linear_Poly.coeff (vec_to_lpoly (row A i)) a * ⟨X⟩ a)" 
    using valuate_with_dim_poly[of "vec_to_lpoly (row A i)" "⟨X⟩"] by blast
  also have "... = (∑a = 0..<dim_col A. Abstract_Linear_Poly.coeff (vec_to_lpoly (row A i)) a * ⟨X⟩ a)"
    using split_coeff_vec_index_sum[of x y]
      sum_dim_vec_equals_sum_dim_poly[of "row A i" "⟨X⟩"] by auto
  also have "... = row A i ∙ x" 
    unfolding scalar_prod_def using ‹dim_col A = dim_vec x› i assms(3)
    using matrix_to_lpolies_coeff_access[of i A] matrix_to_lp_vec_to_lpoly_row[of i A] 
      split_access_fst_1[of _ "(dim_col A)" l X x y] by fastforce
  finally show ?case
    using m i lpoly_of_v_equals_v_append0 by auto
qed

lemma mat_leqb_eqc_split_simplex_correct1:
  assumes "dim_vec b = dim_row A"
  assumes "simplex (mat_leqb_eqc A b c) = Sat X"
  assumes "(x,y) = split_i_j_x (dim_col A) l X"  
  shows "[A *v x]≤b"
  using mat_leqb_eqc_split_correct1[of b A c X x y] assms(1) assms(2) assms(3) simplex(3) by blast

lemma sat_mono:
  assumes "set A ⊆ set B"
  shows "⟨X⟩ ⊨cs set B ⟹ ⟨X⟩ ⊨cs set A"
  using assms(1) assms by blast

lemma mat_leqb_eqc_split_subset_correct1:
  assumes "dim_vec b = dim_row A"
  assumes "set (mat_leqb_eqc A b c) ⊆ set S"
  assumes "simplex S = Sat X"
  assumes "(x,y) = split_i_j_x (dim_col A) l X"  
  shows "[A *v x]≤b"
  using sat_mono assms(1) assms(2) assms(3) assms(4) 
    mat_leqb_eqc_split_correct1 simplex(3) by blast

lemma mat_leqb_eqc_split_correct2:
  assumes "dim_vec c = dim_row AT"
  assumes "dim_vec b = dim_col AT"
  assumes "⟨X⟩ ⊨cs set (mat_leqb_eqc A b c)"
  assumes "(x, y) = split_n_m_x (dim_row AT) (dim_col AT) X"  
  shows "[y v* A]=c"
proof (standard, goal_cases)
case 1
  then show ?case 
    using assms split_n_m_x_abbrev_dims(2)[OF assms(4)[symmetric]] by linarith
  case 2
  then show ?case using assms(1)[symmetric] .
  case (3 i)
  define lst where lst: "lst = matrix_to_lpolies (two_block_non_interfering A AT)"
  define db where db: "db = dim_vec b"
  define dc where dc: "dc = dim_vec c"
  have cA: "dim_vec c ≤ dim_col A"
    by (simp add: assms(1))
  have dbi_dim: "db+i < dim_vec (b @v c)"
    by (simp add: "3" db)
  have *: "dim_vec b ≤ db+i"
    by (simp add: db)
  have "([LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
        [EQ  (lst!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)]]) ! (db + i) =
         EQ (lst!(db+i)) ((b@vc)$(db+i))" using mat_leqb_eqc_for_EQ[of b "db+i" c A]
    nth_append[of "[LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]]" 
      "[EQ  (lst!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)]]"]
    by (simp add: "3" db)
  have rowA: "dim_vec b = dim_row A"
    using assms index_transpose_mat(3)[of A] by linarith
  have "⟨X⟩ ⊨c EQ (lst!(db+i)) (c$i)"
  proof -
    have "db + i - dim_vec b = i"
      using db diff_add_inverse by blast
    then have "(lst ! (db + i)) ⦃ ⟨X⟩ ⦄ = c $ i"
      by (metis dbi_dim rowA * cA assms(3) index_append_vec(1)
          index_append_vec(2) leD lst mat_leqb_eqc_satisfies2)
    then show ?thesis
      using satisfies_constraint.simps(5)[of "⟨X⟩" "(lst ! (db + i))" "(c $ i)"] by simp
  qed
  then have sat: "(lst!(db+i)) ⦃⟨X⟩⦄ = c$i"
    by simp
  define V where V: "V = vec (db+dc) (λi. ⟨X⟩ i)"
  have vdim: "dim_vec V = dim_vec (b@vc)" using V db dc by simp
  have *: "db + i < dim_row (two_block_non_interfering A AT)"
    by (metis dbi_dim assms(1) index_append_vec(2) rowA two_block_non_interfering_dims(1))
  have **: "dim_row A ≤ db + i"
    by (simp add: assms(2) db)
  from two_block_non_interfering_row_comp2[of "db+i" A "AT", OF * **]
  have eql: "row (two_block_non_interfering A AT) (db + i) = 0v (dim_col A) @v row AT i"
    by (simp add: assms(2) db)
  with matrix_to_lp_vec_to_lpoly_row[of i "AT"]
  have eqv: "lst!(db+i) = vec_to_lpoly (0v (dim_col A) @v row AT i)"
    using "*" lst matrix_to_lp_vec_to_lpoly_row by presburger
  then  have "∀j<dim_col A. Abstract_Linear_Poly.coeff (lst!(db+i)) j = 0"
    by (metis index_append_vec(1) index_append_vec(2) index_zero_vec(1) index_zero_vec(2) 
        vec_to_lin_poly_coeff_access trans_less_add1)
  moreover have "∀j≥db+dc. Abstract_Linear_Poly.coeff (lst!(db+i)) j = 0"
    by (metis (mono_tags, lifting) eqv index_transpose_mat(3) index_zero_vec(2) leD
        add.commute assms(1) assms(2) coeff_nonzero_dim_vec_non_zero(2) index_append_vec(2) 
        index_row(2) index_transpose_mat(2) db dc)
  moreover have "vars (lst!(db+i)) ⊆ {dim_col A..<db+dc}"
    by (meson atLeastLessThan_iff calculation(1) calculation(2) coeff_zero not_le subsetI)
  ultimately have "(lst!(db+i))⦃⟨X⟩⦄ = (∑j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j * ⟨X⟩ j)"
    using eval_poly_with_sum_superset[of "{dim_col A..<db+dc}" "lst!(db+i)" "⟨X⟩"] by blast
  also have "... = (∑j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j * V$j)" 
    using V by auto
  also have "... = (∑j∈{dim_col A..<db+dc}. (0v (dim_col A) @v row AT i)$j * V$j)"
  proof - 
    have "∀j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j = (0v (dim_col A) @v row AT i)$j"
      by (metis ‹V ≡ vec (db + dc) ⟨X⟩› vdim assms(1) assms(2) index_transpose_mat(2)
          atLeastLessThan_iff dim_vec eql eqv index_append_vec(2) index_row(2) 
          vec_to_lin_poly_coeff_access semiring_normalization_rules(24) 
          two_block_non_interfering_dims(2))
    then show ?thesis
      by (metis (mono_tags, lifting) sum.cong)
  qed
  also have "... = (∑j∈{0..<dim_col A}. (0v (dim_col A) @v row AT i)$j * V$j) + 
                   (∑j∈{dim_col A..<db+dc}. (0v (dim_col A) @v row AT i)$j * V$j)"
    by (metis (no_types, lifting) add_cancel_left_left atLeastLessThan_iff mult_eq_0_iff
        class_semiring.add.finprod_all1 index_append_vec(1) index_zero_vec(1)
        index_zero_vec(2) trans_less_add1)
  also have "... = (∑j∈{0..<db+dc}. (0v (dim_col A) @v row AT i)$j * V$j)"
    by (metis (no_types, lifting) add.commute assms(1) dc index_transpose_mat(2) 
        le_add1 le_add_same_cancel1 sum.atLeastLessThan_concat)
  also have "... = (0v (dim_col A) @v row AT i) ∙ V"
    unfolding scalar_prod_def by (simp add: V)
  also have "... = 0v (dim_col A) ∙ vec_first V (dim_vec (0v (dim_col A))) + 
                   row AT i ∙ vec_last V (dim_vec (row AT i))"
    using append_split_vec_distrib_scalar_prod[of "0v (dim_col A)" "row AT i" V]
    by (metis (no_types, lifting) ‹dim_vec V = dim_vec (b @v c)› add.commute assms(1) 
        assms(2) index_append_vec(2) index_row(2) index_transpose_mat(2) 
        index_transpose_mat(3) index_zero_vec(2))
  also have  "0v (dim_col A) ∙ vec_first V (dim_vec (0v (dim_col A))) + 
                   row AT i ∙ vec_last V (dim_vec (row AT i)) = (row AT i) ∙ y"
  proof - 
    have "vec_last V (dim_vec (row AT i)) = y"
    proof (standard, goal_cases)
      case (1 i)
      then show ?case 
      proof -
        have f1: "dim_col AT = db"
          by (simp add: assms(2) db)
        then have "∀v va. vec db (λn. ⟨X⟩ (n + dc)) = v ∨ (x, y) ≠ (va, v)"
          by (metis Pair_inject add_diff_cancel_left' assms(1) assms(4) dc split_i_j_x_def)
        then show ?case
          unfolding V vec_last_def
          using split_access_fst_1[of "(dim_row AT)"  i "(dim_col AT)" X x y]
          by (metis "1" add.commute add_diff_cancel_left' add_less_cancel_left 
              dim_vec f1 index_row(2) index_vec)
      qed
    next
      case 2
      then show ?case
        using ‹dim_col AT = dim_vec y› by auto
    qed
    then show ?thesis
      by (simp add: assms(1))
  qed
  then show ?case unfolding mult_mat_vec_def by (metis "3" assms(1) calculation index_vec sat)
qed

lemma mat_leqb_eqc_split_simplex_correct2:
  assumes "dim_vec c = dim_row AT"
  assumes "dim_vec b = dim_col AT"
  assumes "simplex (mat_leqb_eqc A b c) = Sat X"
  assumes "(x, y) = split_n_m_x (dim_row AT) (dim_col AT) X"  
  shows "[y v* A]=c"
  using assms(1) assms(2) assms(3) assms(4) mat_leqb_eqc_split_correct2 simplex(3) by blast

lemma mat_leqb_eqc_correct:
  assumes "dim_vec c = dim_row AT"
    and "dim_vec b = dim_col AT"
  assumes "simplex (mat_leqb_eqc A b c) = Sat X"
  assumes "(x, y) = split_n_m_x (dim_row AT) (dim_col AT) X"
  shows "[y v* A]=c" "[A *v x]≤b"
  using mat_leqb_eqc_split_simplex_correct1[of b A c X x y]
  using assms(1) assms(2) assms(3) assms(4) mat_leqb_eqc_split_simplex_correct2 apply blast
  using mat_leqb_eqc_split_correct2[of b A c X x y]
  by (metis (no_types) Matrix.transpose_transpose assms(2) assms(3) assms(4) index_transpose_mat(3)
      mat_leqb_eqc_split_simplex_correct1[of b A c X x y])

lemma eval_lpoly_eq_dot_prod_split1:
  assumes "(x, y) = split_n_m_x (dim_vec c) (dim_vec b) X"
  shows"(vec_to_lpoly c) ⦃⟨X⟩⦄ =  c ∙ x"
proof -
  have *: "(vec_to_lpoly c) ⦃⟨X⟩⦄ =
           (∑i∈vars (vec_to_lpoly c). Abstract_Linear_Poly.coeff (vec_to_lpoly c) i * ⟨X⟩ i)"
    using linear_poly_sum sum.cong eval_poly_with_sum by auto
  also have "... = (∑i∈{0..<dim_vec c}. Abstract_Linear_Poly.coeff (vec_to_lpoly c) i * ⟨X⟩ i)"
    using vars_subset_dim_vec_to_lpoly_dim[of c] linear_poly_sum[of "vec_to_lpoly c" "⟨X⟩"] 
      eval_poly_with_sum_superset[of "{0..<dim_vec c}" "vec_to_lpoly c" "⟨X⟩"] by auto
  also have "... = (∑i∈{0..<dim_vec c}. c$i * x$i)"
    using split_access_fst_1[of _ "dim_vec c" "(dim_vec c) + (dim_vec b)" X x y]
      split_access_snd_1[of "dim_vec c" _ "((dim_vec c) + (dim_vec b))" X x y]
      vec_to_lin_poly_coeff_access[of _ c] using assms by auto
  also have "... = c ∙ x"
    unfolding scalar_prod_def
    using split_vec_dims(1)[of "dim_vec c" "(dim_vec c) + (dim_vec b)" X x y] assms by auto
  finally show ?thesis .
qed

lemma eval_lpoly_eq_dot_prod_split2:
  assumes "(x, y) = split_n_m_x (dim_vec b) (dim_vec c) X"
  shows"(vec_to_lpoly (0v (dim_vec b) @v c)) ⦃⟨X⟩⦄ =  c ∙ y"
proof -
  let ?p = "(vec_to_lpoly ((0v (dim_vec b) @v c)))"
  let ?v0 = "(0v (dim_vec b) @v c)"
  have *: "∀i<dim_vec b. Abstract_Linear_Poly.coeff ?p i = 0"
    using coeff_nonzero_dim_vec_non_zero(1) by fastforce
  have **: "dim_vec ?v0 = dim_vec b + dim_vec c"
    by simp
  have "?p ⦃⟨X⟩⦄ = (∑i∈vars ?p. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
    using eval_poly_with_sum by blast
  also have "... = (∑i∈{0..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)" 
    using eval_poly_with_sum_superset[of "{0..<dim_vec ?v0}" ?p "⟨X⟩"] calculation
      vars_subset_dim_vec_to_lpoly_dim[of ?v0] by force
  also have "... = (∑i∈{0..<dim_vec b}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i) + 
                   (∑i∈{(dim_vec b)..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
    by (simp add: sum.atLeastLessThan_concat)
  also have "... = (∑i∈{(dim_vec b)..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
    using * by simp
  also have "... = (∑i∈{(dim_vec b)..<dim_vec ?v0}. ?v0$i * ⟨X⟩ i)"
    using vec_to_lin_poly_coeff_access by auto
  also have "... = (∑i∈{0..<dim_vec c}. ?v0$(i+dim_vec b) * ⟨X⟩ (i+dim_vec b))"
    using index_zero_vec(2)[of "dim_vec b"] index_append_vec(2)[of "0v (dim_vec b)" c] ** *
       sum.shift_bounds_nat_ivl[of "(λi. ?v0$i * ⟨X⟩ i)" 0 "dim_vec b" "dim_vec c"]
    by (simp add: add.commute)
  also have "... = (∑i∈{0..<dim_vec c}. c$i * ⟨X⟩ (i+dim_vec b))"
    by auto
  also have "... = (∑i∈{0..<dim_vec c}. c$i * y$i)"
    using split_access_snd_2[of x y "(dim_vec b)" "(dim_vec c)" X] assms
    by (metis (mono_tags, lifting) atLeastLessThan_iff split_access_snd_2 
        split_n_m_x_abbrev_dims(2) split_vec_dims(1) sum.cong)
  also have "... = c ∙ y"
    by (metis assms scalar_prod_def split_n_m_x_abbrev_dims(2))
  finally show ?thesis .
qed

lemma x_times_c_geq_y_times_b_split_dotP:
  assumes "⟨X⟩ ⊨c x_times_c_geq_y_times_b c b"
  assumes "(x, y) = split_n_m_x (dim_vec c) (dim_vec b) X"
  shows "c ∙ x ≥ b ∙ y"
  using assms lpoly_of_v_equals_v_append0 eval_lpoly_eq_dot_prod_split2[of x y c b X]
   eval_lpoly_eq_dot_prod_split1[of x y c b X]  by auto

lemma mult_right_leq:
  fixes A :: "('a::{comm_semiring_1,ordered_semiring}) mat"
  assumes "dim_vec y = dim_vec b"
    and "∀i < dim_vec y. y$i ≥ 0"
    and "[A *v x]≤ b"
  shows "(A *v x) ∙ y ≤ b ∙ y"
proof -
  have "(∑n<dim_vec b. (A *v x) $ n * y $ n) ≤ (∑n<dim_vec b. b $ n * y $ n)"
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) lessThan_iff 
        mat_times_vec_leq_def mult_right_mono sum_mono)
  then show ?thesis
    by (metis (no_types) assms(1) atLeast0LessThan scalar_prod_def)
qed

lemma mult_right_eq:
  assumes "dim_vec x = dim_vec c"
    and "[y v* A]=c"
  shows "(AT *v y) ∙ x = c ∙ x"
  unfolding scalar_prod_def 
  using atLeastLessThan_iff[of _ 0 "dim_vec x"] vec_times_mat_eq_def[of y A c] 
    sum.cong[of _ _ "λi. (AT *v y) $ i * x $ i" "λi. c $ i * x $ i"]
  by (metis (mono_tags, lifting) assms(1) assms(2))

lemma soundness_mat_x_leq:
  assumes "dim_row A = dim_vec b"
  assumes "simplex (mat_x_leq_vec A b) = Sat X"
  shows "∃x. [A *v x]≤b"
proof
  define x where x: "x = fst (split_n_m_x (dim_col A) (dim_row A) X)"
  have *: "dim_vec x = dim_col A" by (simp add: split_i_j_x_def x)
  have "∀i<dim_vec b. (A *v x) $ i ≤ b $ i"
  proof (standard, standard)
    fix i
    assume "i < dim_vec b"
    have "row A i ∙ x ≤ b$i"
      using mat_x_leq_vec_sol[of A b X i]
      by (metis ‹i < dim_vec b› assms(1) assms(2) eval_lpoly_eq_dot_prod_split1 
          fst_conv index_row(2) matrix_to_lp_vec_to_lpoly_row simplex(3) split_i_j_x_def x)
    then show "(A *v x) $ i ≤ b $ i"
      by (simp add: ‹i < dim_vec b› assms(1))
  qed
  then show "[A *v x]≤b"
    using mat_times_vec_leqI[of A b x, OF assms(1) *[symmetric]] by auto
qed

lemma completeness_mat_x_leq:
  assumes "∃x. [A *v x]≤b"
  shows "∃X. simplex (mat_x_leq_vec A b) = Sat X"
proof (rule ccontr)
  assume 1: "∄X. simplex (mat_x_leq_vec A b) = Inr X"
  have *: "∄v. v ⊨cs set (mat_x_leq_vec A b)"
    using simplex(1)[of "mat_x_leq_vec A b"] using "1" sum.exhaust_sel by blast
  then have "dim_vec b = dim_row A" using assms mat_times_vec_leqD(1)[of A _ b] by auto
  then obtain x where x: "[A *v x]≤b" 
    using assms by blast
  have x_A: "dim_vec x = dim_col A"
    using x by auto
  define v where v: "v = (λi. (if i < dim_vec x then x$i else 0))"
  have v_d: "∀i < dim_vec x. x$i = v i"
    by (simp add: v)
  have "v ⊨cs set (mat_x_leq_vec A b)"
  proof 
    fix c
    assume "c ∈ set (mat_x_leq_vec A b)"
    then obtain i where i: "c = LEQ (matrix_to_lpolies A!i) (b$i)" "i < dim_vec b"
      by auto
    let ?p = "matrix_to_lpolies A!i"
    have 2: "?p⦃ v ⦄ = (row A i) ∙ x"
      using matrix_to_lpolies_lambda_valuate_scalarP[of i A x] v
      by (metis ‹dim_vec b = dim_row A› i(2) x_A)
    also have "... ≤ b$i"
      by (metis i(2) index_mult_mat_vec mat_times_vec_leq_def x)
    finally show "v ⊨c c"
      using i(1) satisfies_constraint.simps(3)[of v "(matrix_to_lpolies A ! i)" "b $ i"] 
        2 ‹row A i ∙ x ≤ b $ i› by simp
  qed
  then show False using * by auto
qed

lemma soundness_mat_x_eq_vec:
  assumes "dim_row AT = dim_vec c"
  assumes "simplex (x_mat_eq_vec c AT) = Sat X"
  shows  "∃x. [x v* A]=c"
proof 
  define x where x: "x = fst (split_n_m_x (dim_col AT) (dim_row AT) X)"
  have "dim_vec x = dim_col AT"
    unfolding split_i_j_x_def using split_vec_dims(1)[of "(dim_col AT)" _ X x] fst_conv[of x]
    by (simp add: split_i_j_x_def x)
  have "∀i < dim_vec c. (AT *v x)$i = c$i"
  proof (standard, standard)
    fix i
    assume a: "i < dim_vec c"
    have *: "⟨X⟩ ⊨cs set (x_mat_eq_vec c AT)"
      using assms(2) simplex(3) by blast
    then have "row AT i ∙ x = c$i"
      using x_mat_eq_vec_sol[of c "AT" "⟨X⟩" i, OF * a] eval_lpoly_eq_dot_prod_split1 fstI       
      by (metis a assms(1) index_row(2) matrix_to_lpolies_vec_of_row split_i_j_x_def x)
    then show "(AT *v x) $ i = c $ i"
      unfolding mult_mat_vec_def using a assms(1) by auto
  qed
  then show "[x v* A]=c"
    using mat_times_vec_eqI[of A x c, OF ‹dim_vec x = dim_col AT[symmetric] assms(1)] by auto
qed

lemma completeness_mat_x_eq_vec:
  assumes "∃x. [x v* A]=c"
  shows "∃X. simplex (x_mat_eq_vec c AT) = Sat X"
proof (rule ccontr)
  assume 1: "∄X. simplex (x_mat_eq_vec c AT) = Inr X"
  then have *: "∄v. v ⊨cs set (x_mat_eq_vec c AT)"
    using simplex(1)[of "x_mat_eq_vec c AT"] using sum.exhaust_sel 1 by blast
  then have "dim_vec c = dim_col A" using assms
    by (metis index_transpose_mat(2) vec_times_mat_eqD(3))
  obtain x where " [x v* A]=c" using assms by auto
  then have "dim_vec x = dim_col AT" using assms
    by (metis ‹[x v* A]=c› vec_times_mat_eq_def)
  define v where v: "v = (λi. (if i < dim_vec x then x$i else 0))"
  have v_d: "∀i < dim_vec x. x$i = v i"
    by (simp add: v)
  have "v ⊨cs set (x_mat_eq_vec c AT)"
  proof 
    fix a
    assume "a ∈ set (x_mat_eq_vec c AT)"
    then obtain i where i: "a = EQ (matrix_to_lpolies AT!i) (c$i)" "i < dim_vec c"
      by (metis (no_types, lifting) add_cancel_right_left diff_zero in_set_conv_nth length_map length_upt nth_map_upt x_mat_eq_vec.simps)
    let ?p = "matrix_to_lpolies AT!i"
    have 2: "?p⦃ v ⦄ = (row AT i) ∙ x"
      using matrix_to_lpolies_lambda_valuate_scalarP[of i "AT" x] v
      by (metis ‹dim_vec c = dim_col A› ‹dim_vec x = dim_col AT i(2) index_transpose_mat(2))
    also have "... = c$i"
      by (metis ‹[x v* A]=c› ‹dim_vec c = dim_col A› i(2) index_mult_mat_vec index_transpose_mat(2) vec_times_mat_eqD(1))
    finally show "v ⊨c a"
      using i(1) satisfies_constraint.simps(5)[of v "(matrix_to_lpolies AT ! i)" "(c $ i)"] by simp
  qed
  then show False
    using "*" by blast
qed

lemma soundness_mat_leqb_eqc1:
  assumes "dim_row A = dim_vec b"
  assumes "simplex (mat_leqb_eqc A b c) = Sat X"
  shows "∃x. [A *v x]≤b"
proof
  define x where x: "x = fst (split_n_m_x (dim_col A) (dim_row A) X)"
  have *: "dim_vec x = dim_col A" by (simp add: split_i_j_x_def x)
  have "∀i<dim_vec b. (A *v x) $ i ≤ b $ i"
  proof (standard, standard)
    fix i
    assume "i < dim_vec b"
    have "row A i ∙ x ≤ b$i"
      using mat_x_leq_vec_sol[of A b X i]
      by (metis ‹i < dim_vec b› assms(1) assms(2) fst_conv split_i_j_x_def x
          index_mult_mat_vec mat_leqb_eqc_split_simplex_correct1 mat_times_vec_leqD(3))
    then show "(A *v x) $ i ≤ b $ i"
      by (simp add: ‹i < dim_vec b› assms(1))
  qed
  then show "[A *v x]≤b"
    using mat_times_vec_leqI[of A b x, OF assms(1) *[symmetric]] by auto
qed

lemma soundness_mat_leqb_eqc2:
  assumes "dim_row AT = dim_vec c"
  assumes "dim_col AT = dim_vec b"
  assumes "simplex (mat_leqb_eqc A b c) = Sat X"
  shows "∃y. [y v* A]=c"
proof (standard, intro mat_times_vec_eqI)
  define y where x: "y = snd (split_n_m_x (dim_col A) (dim_row A) X)"
  have *: "dim_vec y = dim_row A" by (simp add: split_i_j_x_def x)
  show "dim_col AT = dim_vec y" by (simp add: "*")
  show "dim_row AT = dim_vec c" using assms(1) by blast
  show "⋀i. i < dim_vec c ⟹ (AT *v y) $ i = c $ i"
  proof -
    fix i
    assume a: "i < dim_vec c"
    have "[y v* A]=c"
      using mat_leqb_eqc_split_correct2[of c A b _ _ y, OF assms(1)[symmetric] assms(2)[symmetric]]
      by (metis Matrix.transpose_transpose assms(3) index_transpose_mat(2) 
          simplex(3) snd_conv split_i_j_x_def x)
    then show "(AT *v y) $ i = c $ i"
      by (metis a vec_times_mat_eq_def)
  qed
qed

lemma completeness_mat_leqb_eqc:  
  assumes "∃x. [A *v x]≤b" 
    and "∃y. [y v* A]=c"
  shows "∃X. simplex (mat_leqb_eqc A b c) = Sat X"
proof (rule ccontr)
  assume 1: "∄X. simplex (mat_leqb_eqc A b c) = Sat X"
  have *: "∄v. v ⊨cs set (mat_leqb_eqc A b c)"
    using simplex(1)[of "mat_leqb_eqc A b c"] using "1" sum.exhaust_sel by blast
  then have "dim_vec b = dim_row A" 
    using assms mat_times_vec_leqD(1)[of A _ b] by presburger
  then obtain x y where x: "[A *v x]≤b" "[y v* A]=c"
    using assms by blast
  have x_A: "dim_vec x = dim_col A"
    using x by auto
  have yr: "dim_vec y = dim_row A"
    using vec_times_mat_eq_def x(2) by force
  define v where v: "v = (λi. (if i < dim_vec (x@vy) then (x@vy)$i else 0))"
  have v_d: "∀i < dim_vec (x@vy). (x@vy)$i = v i"
    by (simp add: v)
  have i_in: "∀i ∈ {0..< dim_vec y}. y$i = v (i+dim_vec x)"
    by (simp add: v)
  have "v ⊨cs set (mat_leqb_eqc A b c)"
  proof
    fix e
    assume asm: "e ∈ set (mat_leqb_eqc A b c)"
    define lst where lst: "lst = matrix_to_lpolies (two_block_non_interfering A AT)"
    let ?L = "[LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
              [EQ  (lst!i) ((b@vc)$i) . i <- [dim_vec b ..< dim_vec (b@vc)]]"
    have L: "mat_leqb_eqc A b c = ?L"
      by (metis (full_types) lst mat_leqb_eqc.simps)
    then obtain i where i: "e = ?L!i" "i ∈{0..<length ?L}"
      using asm by (metis atLeastLessThan_iff in_set_conv_nth not_le not_less0)
    have ldimbc: "length ?L = dim_vec (b@vc)"
      using i(2) by auto
    consider (leqb) "i ∈ {0..<dim_vec b}" | (eqc) "i ∈ {dim_vec b..<length ?L}"
      using i(2) leI by auto
    then show "v ⊨c e"
    proof (cases)
      case leqb
      have il: "i < dim_vec b"
        using atLeastLessThan_iff leqb by blast
      have iA: "i < dim_row A"
        using ‹dim_vec b = dim_row A› ‹i < dim_vec b› by linarith
      then have *: "e = LEQ (lst!i) (b$i)"
        by (simp add: i(1) nth_append il)
      then have "... = LEQ ((matrix_to_lpolies A)!i) (b$i)"
        using mat_leqb_eqc_for_LEQ[of i b A c, OF il ‹i < dim_row A›] L i(1) by simp
      then have eqmp: "lst!i = ((matrix_to_lpolies A)!i)"
        by blast
      have sset: "vars (lst!i) ⊆ {0..<dim_vec x}" using matrix_to_lpolies_vec_of_row
        by (metis ‹i < dim_row A› eqmp index_row(2)  
            vars_subset_dim_vec_to_lpoly_dim x_A)
      have **: "((lst!i) ⦃ v ⦄) = ((vec_to_lpoly (row A i)) ⦃ v ⦄)"
        by (simp add: ‹i < dim_row A› eqmp)
      also have "... = (∑j∈vars(lst!i). Abstract_Linear_Poly.coeff (lst!i) j * v j)"
        using ** eval_poly_with_sum by auto
      also have "... = (∑j∈{0..<dim_vec x}. Abstract_Linear_Poly.coeff (lst!i) j * v j)"
        using sset eval_poly_with_sum_superset[of "{0..<dim_vec x}" "lst!i" v, 
            OF finite_atLeastLessThan sset] "**" using calculation by linarith
      also have "... = (∑j∈{0..<dim_vec x}. Abstract_Linear_Poly.coeff (lst!i) j * x$j)"
        using v by (auto split: if_split)
      also have "... = (∑j∈{0..<dim_vec x}. (row A i)$j * x$j)"
        using matrix_to_lpolies_vec_of_row[of i A, OF iA] 
          vec_to_lin_poly_coeff_access[of _ "row A i"] index_row(2)[of A i] 
          atLeastLessThan_iff by (metis (no_types, lifting) eqmp sum.cong x_A)
      also have  "... = row A i ∙ x" unfolding scalar_prod_def by (simp)
      also have "... ≤ b$i"
        by (metis ‹i < dim_vec b› index_mult_mat_vec mat_times_vec_leq_def x(1))
      finally show ?thesis 
        by (simp add: "*")
    next
      case eqc
      have igeq: "i ≥ dim_vec b"
        using atLeastLessThan_iff eqc by blast
      have *: "i < length ?L"
        using atLeastLessThan_iff eqc by blast
      have "e =?L!i"
        using L i(1) by presburger
      have "?L!i ∈ set [EQ  (lst!i) ((b@vc)$i). i <- [dim_vec b..< dim_vec (b@vc)]]"
        using in_second_append_list length_map
        by (metis (no_types, lifting) igeq *  length_upt minus_nat.diff_0)
      then have "?L!i = [EQ  (lst!i) ((b@vc)$i). i <- [dim_vec b..< dim_vec (b@vc)]]!(i-dim_vec b)"
        by (metis (no_types, lifting) ‹dim_vec b ≤ i› diff_zero leD 
            length_map length_upt nth_append)
      then have "?L!i = EQ (lst!i) ((b@vc)$i)"
        using add_diff_inverse_nat diff_less_mono
        by (metis (no_types, lifting) ‹dim_vec b ≤ i› * ldimbc  leD nth_map_upt)
      then have e: "e = EQ (lst!i) ((b@vc)$i)"
        using i(1) by blast
      with mat_leqb_eqc_for_EQ[of b i c A, OF igeq] 
      have lsta: "(lst!i) = (vec_to_lpoly (0v (dim_col A) @v row AT (i - dim_vec b)))"
        by (metis (no_types, lifting) ‹dim_vec b = dim_row A› * ldimbc assms(2) igeq 
            index_append_vec(2) lst matrix_to_lpolies_vec_of_row vec_times_mat_eq_def
            two_block_non_interfering_dims(1) two_block_non_interfering_row_comp2 )
      let ?p = "(vec_to_lpoly (0v (dim_col A) @v row AT (i - dim_vec b)))"
      have "dim_poly ?p ≤ dim_col A + dim_row A" 
        using dim_poly_of_append_vec[of "0v (dim_col A)" "row AT (i - dim_vec b)"]
          index_zero_vec(2)[of "dim_col A"]
        by (metis ‹dim_vec (0v (dim_col A)) = dim_col A› index_row(2) index_transpose_mat(3))
      have "∀i < dim_col A. Abstract_Linear_Poly.coeff ?p i = 0"
        using vec_coeff_append1[of _ "0v (dim_col A)" "row AT (i - dim_vec b)"]
        by (metis atLeastLessThan_iff index_zero_vec(1) index_zero_vec(2) zero_le)
      then have "dim_vec (0v (dim_col A) @v row AT (i - dim_vec b)) = dim_col A + dim_row A"
        by (metis index_append_vec(2) index_row(2) index_transpose_mat(3) index_zero_vec(2))
      then have allcr: "∀j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) = (row AT (i - dim_vec b))$j" 
        by (metis add_diff_cancel_right' atLeastLessThan_iff diff_add_inverse index_zero_vec(2) 
            le_add_same_cancel2 less_diff_conv vec_coeff_append2)
      have vs: "vars ?p ⊆ {dim_col A..<dim_col A + dim_row A}"
        using vars_vec_append_subset by (metis index_row(2) index_transpose_mat(3))
      have "?p ⦃ v ⦄ = (∑j∈vars ?p. Abstract_Linear_Poly.coeff ?p j * v j)"
        using eval_poly_with_sum by blast
      also have "... = (∑j∈{dim_col A..<dim_col A + dim_row A}. Abstract_Linear_Poly.coeff ?p j * v j)"     
        by (metis (mono_tags, lifting) DiffD2 vs coeff_zero finite_atLeastLessThan
            mult_not_zero sum.mono_neutral_left)
      also have "... = (∑j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) * v (j+dim_col A))"
        using sum.shift_bounds_nat_ivl[of "λj. Abstract_Linear_Poly.coeff ?p j * v j" 0 "dim_col A" "dim_row A"]
        by (metis (no_types, lifting) add.commute add_cancel_left_left)
      also have "... = (∑j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) * y$j)"
        using v i_in yr by (metis (no_types, lifting) sum.cong x_A) 
      also have "... = (∑j∈{0..<dim_row A}. (row AT (i - dim_vec b))$j * y$j)"
        using allcr by (metis (no_types, lifting) sum.cong)
      also have "... = (row AT (i - dim_vec b)) ∙ y"
        by (metis ‹dim_vec y = dim_row A› scalar_prod_def)
      also have "... = (b@vc)$i"
        using vec_times_mat_eqD[OF x(2)] * igeq by auto
      finally show ?thesis
        using e lsta satisfies_constraint.simps(5)[of _ "(lst ! i)" "((b @v c) $ i)"] by simp
    qed
  qed
  then show False using * by blast
qed

lemma sound_and_compltete_mat_leqb_eqc [iff]:  
  assumes "dim_row AT = dim_vec c"
  assumes "dim_col AT = dim_vec b"
  shows "(∃x. [A *v x]≤b) ∧ (∃y. [y v* A]=c) ⟷ (∃X. simplex (mat_leqb_eqc A b c) = Sat X)"
  by (metis assms(1) assms(2) completeness_mat_leqb_eqc index_transpose_mat(3) 
      soundness_mat_leqb_eqc1 soundness_mat_leqb_eqc2)



section ‹ Translate Inequalities to Matrix Form ›

(* We (obviously) cannot use strict inequalities hence we use the option type *)

fun nonstrict_constr where 
  "nonstrict_constr (LEQ p r) = True" |
  "nonstrict_constr (GEQ p r) = True" |
  "nonstrict_constr (EQ p r) = True" |
  "nonstrict_constr (LEQPP p q) = True" |
  "nonstrict_constr (GEQPP p q) = True" |
  "nonstrict_constr (EQPP p q) = True" |
  "nonstrict_constr _ = False"

abbreviation "nonstrict_constrs cs ≡ (∀a ∈ set cs. nonstrict_constr a)"

fun transf_constraint where
  "transf_constraint (LEQ p r) = [LEQ p r]" |
  "transf_constraint (GEQ p r) = [LEQ (-p) (-r)]" |
  "transf_constraint (EQ p r) = [LEQ p r, LEQ (-p) (-r)]" |
  "transf_constraint (LEQPP p q) = [LEQ (p - q) 0]" |
  "transf_constraint (GEQPP p q) = [LEQ (-(p - q)) 0]" |
  "transf_constraint (EQPP p q) = [LEQ (p - q) 0, LEQ (-(p - q)) 0]" |
  "transf_constraint _ = []"


fun transf_constraints where
"transf_constraints [] = []" |
"transf_constraints (x#xs) = transf_constraint x @ (transf_constraints xs)"


lemma trans_constraint_creats_LEQ_only:
  assumes "transf_constraint x ≠ []"
  shows "(∀x ∈ set (transf_constraint x). ∃a b. x = LEQ a b)"
  using assms by (cases x, auto+)

lemma trans_constraints_creats_LEQ_only:
  assumes "transf_constraints xs ≠ []"
  assumes "x ∈ set (transf_constraints xs)"
  shows "∃p r. LEQ p r = x"
  using assms apply(induction xs) 
  using trans_constraint_creats_LEQ_only apply(auto) 
    apply fastforce
   apply (metis in_set_simps(3) trans_constraint_creats_LEQ_only) 
  by fastforce

lemma non_strict_constr_no_LT: 
  assumes "nonstrict_constrs cs"
  shows "∀x ∈ set cs. ¬(∃a b. LT a b = x)"
  using assms nonstrict_constr.simps(7) by blast

lemma non_strict_constr_no_GT: 
  assumes "nonstrict_constrs cs"
  shows "∀x ∈ set cs. ¬(∃a b. GT a b = x)"
  using assms nonstrict_constr.simps(8) by blast

lemma non_strict_constr_no_LTPP: 
  assumes "nonstrict_constrs cs"
  shows "∀x ∈ set cs. ¬(∃a b. LTPP a b = x)"
  using assms nonstrict_constr.simps(9) by blast

lemma non_strict_constr_no_GTPP: 
  assumes "nonstrict_constrs cs"
  shows "∀x ∈ set cs. ¬(∃a b. GTPP a b = x)"
  using assms nonstrict_constr.simps(10) by blast

lemma non_strict_consts_cond:
  assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. LT a b = x)"
  assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. GT a b = x)"
  assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. LTPP a b = x)"
  assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. GTPP a b = x)"
  shows "nonstrict_constrs cs"
  by (metis assms(1) assms(2) assms(3) assms(4) nonstrict_constr.elims(3))

lemma sat_constr_sat_transf_constrs:
  assumes "v ⊨c cs" 
  shows "v ⊨cs set (transf_constraint cs)"
  using assms by (cases cs) (simp add: valuate_uminus valuate_minus)+

lemma sat_constrs_sat_transf_constrs:
  assumes "v ⊨cs set cs" 
  shows "v ⊨cs set (transf_constraints cs)"
  using assms by(induction cs, simp) (metis UnE list.set_intros(1) 
      list.set_intros(2) sat_constr_sat_transf_constrs set_append transf_constraints.simps(2))

lemma sat_transf_constrs_sat_constr: 
  assumes "nonstrict_constr cs"
  assumes "v ⊨cs set (transf_constraint cs)"
  shows "v ⊨c cs"
  using assms by (cases cs) (simp add: valuate_uminus valuate_minus)+

lemma sat_transf_constrs_sat_constrs:
  assumes "nonstrict_constrs cs"
  assumes "v ⊨cs set (transf_constraints cs)"
  shows "v ⊨cs set cs"
  using assms by (induction cs, auto) (simp add: sat_transf_constrs_sat_constr)

end