Session Linear_Inequalities

Theory Missing_Matrix

section ‹Missing Lemmas on Vectors and Matrices›

text ‹We provide some results on vector spaces which should be merged into Jordan-Normal-Form/Matrix.›
theory Missing_Matrix
  imports Jordan_Normal_Form.Matrix
begin

lemma orthogonalD': assumes "orthogonal vs"
  and "v  set vs" and "w  set vs"
shows "(v  w = 0) = (v  w)"
proof -
  from assms(2) obtain i where v: "v = vs ! i" and i: "i < length vs" by (auto simp: set_conv_nth)
  from assms(3) obtain j where w: "w = vs ! j" and j: "j < length vs" by (auto simp: set_conv_nth)
  from orthogonalD[OF assms(1) i j, folded v w] orthogonalD[OF assms(1) i i, folded v v]
  show ?thesis using v w by auto
qed

lemma zero_mat_mult_vector[simp]: "x  carrier_vec nc  0m nr nc *v x = 0v nr"
  by (intro eq_vecI, auto)

lemma add_diff_cancel_right_vec:
  "a  carrier_vec n  (b :: 'a :: cancel_ab_semigroup_add vec)  carrier_vec n 
    (a + b) - b = a"
  by (intro eq_vecI, auto)

lemma elements_four_block_mat_id:
  assumes c: "A  carrier_mat nr1 nc1" "B  carrier_mat nr1 nc2"
    "C  carrier_mat nr2 nc1" "D  carrier_mat nr2 nc2"
  shows
    "elements_mat (four_block_mat A B C D) =
   elements_mat A  elements_mat B  elements_mat C  elements_mat D"
    (is "elements_mat ?four = ?X")
proof
  show "elements_mat ?four  ?X"
    by (rule elements_four_block_mat[OF c])
  have 4: "?four  carrier_mat (nr1 + nr2) (nc1 + nc2)" using c by auto
  {
    fix x
    assume "x  ?X"
    then consider (A) "x  elements_mat A"
      | (B) "x  elements_mat B"
      | (C) "x  elements_mat C"
      | (D) "x  elements_mat D" by auto
    hence "x  elements_mat ?four"
    proof (cases)
      case A
      from elements_matD[OF this] obtain i j
        where *: "i < nr1" "j < nc1" and x: "x = A $$ (i,j)"
        using c by auto
      from elements_matI[OF 4, of i j x] * c
      show ?thesis unfolding x by auto
    next
      case B
      from elements_matD[OF this] obtain i j
        where *: "i < nr1" "j < nc2" and x: "x = B $$ (i,j)"
        using c by auto
      from elements_matI[OF 4, of i "nc1 + j" x] * c
      show ?thesis unfolding x by auto
    next
      case C
      from elements_matD[OF this] obtain i j
        where *: "i < nr2" "j < nc1" and x: "x = C $$ (i,j)"
        using c by auto
      from elements_matI[OF 4, of "nr1 + i" j x] * c
      show ?thesis unfolding x by auto
    next
      case D
      from elements_matD[OF this] obtain i j
        where *: "i < nr2" "j < nc2" and x: "x = D $$ (i,j)"
        using c by auto
      from elements_matI[OF 4, of "nr1 + i" "nc1 + j" x] * c
      show ?thesis unfolding x by auto
    qed
  }
  thus "elements_mat ?four  ?X" by blast
qed


lemma elements_mat_append_rows: "A  carrier_mat nr n  B  carrier_mat nr2 n 
  elements_mat (A @r B) = elements_mat A  elements_mat B"
  unfolding append_rows_def
  by (subst elements_four_block_mat_id, auto)

lemma elements_mat_uminus[simp]: "elements_mat (-A) = uminus ` elements_mat A"
  unfolding elements_mat_def by auto

lemma vec_set_uminus[simp]: "vec_set (-A) = uminus ` vec_set A"
  unfolding vec_set_def by auto

definition append_cols :: "'a :: zero mat  'a mat  'a mat"  (infixr "@c" 65) where
  "A @c B = (AT @r BT)T"

lemma carrier_append_cols[simp, intro]:
  "A  carrier_mat nr nc1 
   B  carrier_mat nr nc2  (A @c B)  carrier_mat nr (nc1 + nc2)"
  unfolding append_cols_def by auto

lemma elements_mat_transpose_mat[simp]: "elements_mat (AT) = elements_mat A"
  unfolding elements_mat_def by auto

lemma elements_mat_append_cols: "A  carrier_mat n nc  B  carrier_mat n nc1
   elements_mat (A @c B) = elements_mat A  elements_mat B"
  unfolding append_cols_def elements_mat_transpose_mat
  by (subst elements_mat_append_rows, auto)

lemma vec_first_index:
  assumes v: "dim_vec v  n"
    and i: "i < n"
  shows "(vec_first v n) $ i = v $ i"
  unfolding vec_first_def using assms by simp

lemma vec_last_index:
  assumes v: "v  carrier_vec (n + m)"
    and i: "i < m"
  shows "(vec_last v m) $ i = v $ (n + i)"
  unfolding vec_last_def using assms by simp

lemma vec_first_add:
  assumes "dim_vec x  n"
    and "dim_vec y  n"
  shows"vec_first (x + y) n = vec_first x n + vec_first y n"
  unfolding vec_first_def using assms by auto

lemma vec_first_zero[simp]: "m  n  vec_first (0v n) m = 0v m"
  unfolding vec_first_def by auto

lemma vec_first_smult:
  " m  n; x  carrier_vec n   vec_first (c v x) m = c v vec_first x m"
  unfolding vec_first_def by auto

lemma elements_mat_mat_of_row[simp]: "elements_mat (mat_of_row v) = vec_set v"
  by (auto simp: mat_of_row_def elements_mat_def vec_set_def)

lemma vec_set_append_vec[simp]: "vec_set (v @v w) = vec_set v  vec_set w"
  by (metis list_of_vec_append set_append set_list_of_vec)

lemma vec_set_vNil[simp]: "setv vNil = {}" using set_list_of_vec by force

lemma diff_smult_distrib_vec: "((x :: 'a::ring) - y) v v = x v v - y v v"
  unfolding smult_vec_def minus_vec_def
  by (rule eq_vecI, auto simp: left_diff_distrib)

lemma add_diff_eq_vec: fixes y :: "'a :: group_add vec"
  shows "y  carrier_vec n  x  carrier_vec n  z  carrier_vec n  y + (x - z) = y + x - z"
  by (intro eq_vecI, auto simp: add_diff_eq)

definition "mat_of_col v = (mat_of_row v)T"

lemma elements_mat_mat_of_col[simp]: "elements_mat (mat_of_col v) = vec_set v"
  unfolding mat_of_col_def by auto

lemma mat_of_col_dim[simp]: "dim_row (mat_of_col v) = dim_vec v"
  "dim_col (mat_of_col v) = 1"
  "mat_of_col v  carrier_mat (dim_vec v) 1"
  unfolding mat_of_col_def by auto

lemma col_mat_of_col[simp]: "col (mat_of_col v) 0 = v"
  unfolding mat_of_col_def by auto


lemma mult_mat_of_col: "A  carrier_mat nr nc  v  carrier_vec nc 
                        A * mat_of_col v = mat_of_col (A *v v)"
  by (intro mat_col_eqI, auto)

lemma mat_mult_append_cols: fixes A :: "'a :: comm_semiring_0 mat"
  assumes A: "A  carrier_mat nr nc1"
    and B: "B  carrier_mat nr nc2"
    and v1: "v1  carrier_vec nc1"
    and v2: "v2  carrier_vec nc2"
  shows "(A @c B) *v (v1 @v v2) = A *v v1 + B *v v2"
proof -
  have "(A @c B) *v (v1 @v v2) = (A @c B) *v col (mat_of_col (v1 @v v2)) 0" by auto
  also have " = col ((A @c B) * mat_of_col (v1 @v v2)) 0" by auto
  also have "(A @c B) * mat_of_col (v1 @v v2) = ((A @c B) * mat_of_col (v1 @v v2))TT"
    by auto
  also have "((A @c B) * mat_of_col (v1 @v v2))T =
             (mat_of_row (v1 @v v2))TT * (AT @r BT)TT"
    unfolding append_cols_def mat_of_col_def
  proof (rule transpose_mult, force, unfold transpose_carrier_mat, rule mat_of_row_carrier)
    have "AT  carrier_mat nc1 nr" using A by auto
    moreover have "BT  carrier_mat nc2 nr" using B by auto
    ultimately have "AT @r BT  carrier_mat (nc1 + nc2) nr" by auto
    hence "dim_row (AT @r BT) = nc1 + nc2" by auto
    thus "v1 @v v2  carrier_vec (dim_row (AT @r BT))" using v1 v2 by auto
  qed
  also have " = (mat_of_row (v1 @v v2)) * (AT @r BT)" by auto
  also have " = mat_of_row v1 * AT + mat_of_row v2 * BT"
    using mat_of_row_mult_append_rows[OF v1 v2] A B by auto
  also have "T = (mat_of_row v1 * AT)T + (mat_of_row v2 * BT)T"
    using transpose_add A B by auto
  also have "(mat_of_row v1 * AT)T = ATT * ((mat_of_row v1)T)"
    using transpose_mult A v1 transpose_carrier_mat mat_of_row_carrier(1)
    by metis
  also have "(mat_of_row v2 * BT)T = BTT * ((mat_of_row v2)T)"
    using transpose_mult B v2 transpose_carrier_mat mat_of_row_carrier(1)
    by metis
  also have "ATT * ((mat_of_row v1)T) + BTT * ((mat_of_row v2)T) =
             A * mat_of_col v1 + B * mat_of_col v2"
    unfolding mat_of_col_def by auto
  also have "col  0 = col (A * mat_of_col v1) 0 + col (B * mat_of_col v2) 0"
    using assms by auto
  also have " = col (mat_of_col (A *v v1)) 0 + col (mat_of_col (B *v v2)) 0"
    using mult_mat_of_col assms by auto
  also have " = A *v v1 + B *v v2" by auto
  finally show ?thesis by auto
qed

lemma vec_first_append:
  assumes "v  carrier_vec n"
  shows "vec_first (v @v w) n = v"
proof -
  have "v @v w = vec_first (v @v w) n @v vec_last (v @v w) (dim_vec w)"
    using vec_first_last_append assms by simp
  thus ?thesis using append_vec_eq[OF assms] by simp
qed

lemma vec_le_iff_diff_le_0: fixes a :: "'a :: ordered_ab_group_add vec"
  shows "(a  b) = (a - b  0v (dim_vec a))"
  unfolding less_eq_vec_def by auto

definition "mat_row_first A n  mat n (dim_col A) (λ (i, j). A $$ (i, j))"

definition "mat_row_last A n  mat n (dim_col A) (λ (i, j). A $$ (dim_row A - n + i, j))"

lemma mat_row_first_carrier[simp]: "mat_row_first A n  carrier_mat n (dim_col A)"
  unfolding mat_row_first_def by simp

lemma mat_row_first_dim[simp]:
  "dim_row (mat_row_first A n) = n"
  "dim_col (mat_row_first A n) = dim_col A"
  unfolding mat_row_first_def by simp_all

lemma mat_row_last_carrier[simp]: "mat_row_last A n  carrier_mat n (dim_col A)"
  unfolding mat_row_last_def by simp

lemma mat_row_last_dim[simp]:
  "dim_row (mat_row_last A n) = n"
  "dim_col (mat_row_last A n) = dim_col A"
  unfolding mat_row_last_def by simp_all

lemma mat_row_first_nth[simp]: "i < n  row (mat_row_first A n) i = row A i"
  unfolding mat_row_first_def row_def by fastforce

lemma append_rows_nth:
  assumes "A  carrier_mat nr1 nc"
    and "B  carrier_mat nr2 nc"
  shows "i < nr1  row (A @r B) i = row A i"
    and " i  nr1; i < nr1 + nr2   row (A @r B) i = row B (i - nr1)"
  unfolding append_rows_def using row_four_block_mat assms by auto

lemma mat_of_row_last_nth[simp]:
  "i < n  row (mat_row_last A n) i = row A (dim_row A - n + i)"
  unfolding mat_row_last_def row_def by auto

lemma mat_row_first_last_append:
  assumes "dim_row A = m + n"
  shows "(mat_row_first A m) @r (mat_row_last A n) = A"
proof (rule eq_rowI)
  show "dim_row (mat_row_first A m @r mat_row_last A n) = dim_row A"
    unfolding append_rows_def using assms by fastforce
  show "dim_col (mat_row_first A m @r mat_row_last A n) = dim_col A"
    unfolding append_rows_def by fastforce
  fix i
  assume i: "i < dim_row A"
  show "row (mat_row_first A m @r mat_row_last A n) i = row A i"
  proof cases
    assume i: "i < m"
    thus ?thesis using append_rows_nth(1)[OF mat_row_first_carrier[of A m]
          mat_row_last_carrier[of A n] i] by simp
  next
    assume i': "¬ i < m"
    thus ?thesis using append_rows_nth(2)[OF mat_row_first_carrier[of A m]
          mat_row_last_carrier[of A n]] i assms by simp
  qed
qed

definition "mat_col_first A n  (mat_row_first AT n)T"

definition "mat_col_last A n  (mat_row_last AT n)T"

lemma mat_col_first_carrier[simp]: "mat_col_first A n  carrier_mat (dim_row A) n"
  unfolding mat_col_first_def by fastforce

lemma mat_col_first_dim[simp]:
  "dim_row (mat_col_first A n) = dim_row A"
  "dim_col (mat_col_first A n) = n"
  unfolding mat_col_first_def by simp_all

lemma mat_col_last_carrier[simp]: "mat_col_last A n  carrier_mat (dim_row A) n"
  unfolding mat_col_last_def by fastforce

lemma mat_col_last_dim[simp]:
  "dim_row (mat_col_last A n) = dim_row A"
  "dim_col (mat_col_last A n) = n"
  unfolding mat_col_last_def by simp_all

lemma mat_col_first_nth[simp]:
  " i < n; i < dim_col A   col (mat_col_first A n) i = col A i"
  unfolding mat_col_first_def by force

lemma append_cols_nth:
  assumes "A  carrier_mat nr nc1"
    and "B  carrier_mat nr nc2"
  shows "i < nc1  col (A @c B) i = col A i"
    and " i  nc1; i < nc1 + nc2   col (A @c B) i = col B (i - nc1)"
  unfolding append_cols_def append_rows_def using row_four_block_mat assms
  by auto

lemma mat_of_col_last_nth[simp]:
  " i < n; i < dim_col A   col (mat_col_last A n) i = col A (dim_col A - n + i)"
  unfolding mat_col_last_def by auto

lemma mat_col_first_last_append:
  assumes "dim_col A = m + n"
  shows "(mat_col_first A m) @c (mat_col_last A n) = A"
  unfolding append_cols_def mat_col_first_def mat_col_last_def
  using mat_row_first_last_append[of "AT"] assms by simp

lemma mat_of_row_dim_row_1: "(dim_row A = 1) = (A = mat_of_row (row A 0))"
proof
  show "dim_row A = 1  A = mat_of_row (row A 0)" by force
  show "A = mat_of_row (row A 0)  dim_row A = 1" using mat_of_row_dim(1) by metis
qed

lemma mat_of_col_dim_col_1: "(dim_col A = 1) = (A = mat_of_col (col A 0))"
proof
  show "dim_col A = 1  A = mat_of_col (col A 0)"
    unfolding mat_of_col_def by auto
  show "A = mat_of_col (col A 0)  dim_col A = 1" by (metis mat_of_col_dim(2))
qed

definition vec_of_scal :: "'a  'a vec" where "vec_of_scal x  vec 1 (λ i. x)"

lemma vec_of_scal_dim[simp]:
  "dim_vec (vec_of_scal x) = 1"
  "vec_of_scal x  carrier_vec 1"
  unfolding vec_of_scal_def by auto

lemma index_vec_of_scal[simp]: "(vec_of_scal x) $ 0 = x"
  unfolding vec_of_scal_def by auto

lemma row_mat_of_col[simp]: "i < dim_vec v  row (mat_of_col v) i = vec_of_scal (v $ i)"
  unfolding mat_of_col_def by auto

lemma vec_of_scal_dim_1: "(v  carrier_vec 1) = (v = vec_of_scal (v $ 0))"
  by(standard, auto simp del: One_nat_def, metis vec_of_scal_dim(2))

lemma mult_mat_of_row_vec_of_scal: fixes x :: "'a :: comm_ring_1"
  shows "mat_of_col v *v vec_of_scal x = x v v"
  by (auto simp add: scalar_prod_def)

lemma smult_pos_vec[simp]: fixes l :: "'a :: linordered_ring_strict"
  assumes l: "l > 0"
  shows "(l v v  0v n) = (v  0v n)"
proof (cases "dim_vec v = n")
  case True
  have "i < n  ((l v v) $ i  0)  v $ i  0" for i using True
      mult_le_cancel_left_pos[OF l, of _ 0] by simp
  thus ?thesis using True unfolding less_eq_vec_def by auto
qed (auto simp: less_eq_vec_def)

lemma finite_elements_mat[simp]: "finite (elements_mat A)"
  unfolding elements_mat_def by (rule finite_set)

lemma finite_vec_set[simp]: "finite (vec_set A)"
  unfolding vec_set_def by auto

lemma lesseq_vecI: assumes "v  carrier_vec n" "w  carrier_vec n"
  " i. i < n  v $ i  w $ i"
shows "v  w"
  using assms unfolding less_eq_vec_def by auto

lemma lesseq_vecD: assumes "w  carrier_vec n"
  and "v  w"
  and "i < n"
shows "v $ i  w $ i"
  using assms unfolding less_eq_vec_def by auto

lemma vec_add_mono: fixes a :: "'a :: ordered_ab_semigroup_add vec"
  assumes dim: "dim_vec b = dim_vec d"
    and ab: "a  b"
    and cd: "c  d"
  shows "a + c  b + d"
proof -
  have " i. i < dim_vec d  (a + c) $ i  (b + d) $ i"
  proof -
    fix i
    assume id: "i < dim_vec d"
    have ic: "i < dim_vec c" using id cd unfolding less_eq_vec_def by auto
    have ib: "i < dim_vec b" using id dim by auto
    have ia: "i < dim_vec a" using ib ab unfolding less_eq_vec_def by auto
    have "a $ i  b $ i" using ab ia ib unfolding less_eq_vec_def by auto
    moreover have "c $ i  d $ i" using cd ic id unfolding less_eq_vec_def by auto
    ultimately have abcdi: "a $ i + c $ i  b $ i + d $ i" using add_mono by auto
    have "(a + c) $ i = a $ i + c $ i" using index_add_vec(1) ic by auto
    also have "  b $ i + d $ i" using abcdi by auto
    also have "b $ i + d $ i = (b + d) $ i" using index_add_vec(1) id by auto
    finally show "(a + c) $ i  (b + d) $ i" by auto
  qed
  then show "a + c  b + d" unfolding less_eq_vec_def
    using dim index_add_vec(2) cd less_eq_vec_def by auto
qed

lemma smult_nneg_npos_vec: fixes l :: "'a :: ordered_semiring_0"
  assumes l: "l  0"
    and v: "v  0v n"
  shows "l v v  0v n"
proof -
  {
    fix i
    assume i: "i < n"
    then have vi: "v $ i  0" using v unfolding less_eq_vec_def by simp
    then have "(l v v) $ i = l * v $ i" using v i unfolding less_eq_vec_def by auto
    also have "l * v $ i  0" by (rule mult_nonneg_nonpos[OF l vi])
    finally have "(l v v) $ i  0" by auto
  }
  then show ?thesis using v unfolding less_eq_vec_def by auto
qed

lemma smult_vec_nonneg_eq: fixes c :: "'a :: field" 
  shows "c  0  (c v x = c v y) = (x = y)"
proof -
  have "c  0  c v x = c v y  x = y" 
    by (metis smult_smult_assoc[of "1 / c" "c"] nonzero_divide_eq_eq one_smult_vec)
  thus "c  0  ?thesis" by auto
qed

lemma distinct_smult_nonneg: fixes c :: "'a :: field"
  assumes c: "c  0"
  shows "distinct lC  distinct (map ((⋅v) c) lC)"
proof (induction lC)
  case (Cons v lC)
  from Cons.prems have "v  set lC" by fastforce
  hence "c v v  set (map ((⋅v) c) lC)" using smult_vec_nonneg_eq[OF c] by fastforce
  moreover have "map ((⋅v) c) (v # lC) = c v v # map ((⋅v) c) lC" by simp
  ultimately show ?case using Cons.IH Cons.prems by simp
qed auto

lemma exists_vec_append: "( x  carrier_vec (n + m). P x)  ( x1  carrier_vec n.  x2  carrier_vec m. P (x1 @v x2))" 
proof
  assume "x  carrier_vec (n + m). P x"
  from this obtain x where xcarr: "x  carrier_vec (n+m)" and Px: "P x" by auto
  have "x = vec n (λ i. x $ i) @v vec m (λ i. x $ (n + i))" 
    by (rule eq_vecI, insert xcarr, auto)
  hence "P x = P (vec n (λ i. x $ i) @v vec m (λ i. x $ (n + i)))" by simp
  also have 1: "" using xcarr Px calculation by blast
  finally show "x1carrier_vec n. x2carrier_vec m. P (x1 @v x2)" using 1 vec_carrier by blast
next
  assume "( x1  carrier_vec n.  x2  carrier_vec m. P (x1 @v x2))"
  from this obtain x1 x2 where x1: "x1  carrier_vec n" 
    and x2: "x2  carrier_vec m" and P12: "P (x1 @v x2)" by auto
  define x where "x = x1 @v x2"
  have xcarr: "x  carrier_vec (n+m)" using x1 x2 by (simp add: x_def)
  have "P x" using P12 xcarr using x_def by blast
  then show "( x  carrier_vec (n + m). P x)" using xcarr by auto
qed

end

Theory Missing_VS_Connect

section ‹Missing Lemmas on Vector Spaces›

text ‹We provide some results on vector spaces which should be merged into other AFP entries.›
theory Missing_VS_Connect
  imports
    Jordan_Normal_Form.VS_Connect
    Missing_Matrix
    Polynomial_Factorization.Missing_List
begin

context vec_space
begin
lemma span_diff: assumes A: "A  carrier_vec n"
  and a: "a  span A" and b: "b  span A"
shows "a - b  span A"
proof -
  from A a have an: "a  carrier_vec n" by auto
  from A b have bn: "b  carrier_vec n" by auto
  have "a + (-1 v b)  span A"
    by (rule span_add1[OF A a], insert b A, auto)
  also have "a + (-1 v b) = a - b" using an bn by auto
  finally show ?thesis by auto
qed

lemma finsum_scalar_prod_sum':
  assumes f: "f  U  carrier_vec n"
    and w: "w  carrier_vec n"
  shows "w  finsum V f U = sum (λu. w  f u) U"
  by (subst comm_scalar_prod[OF w], (insert f, auto)[1],
      subst finsum_scalar_prod_sum[OF f w],
      insert f, intro sum.cong[OF refl] comm_scalar_prod[OF _ w], auto)

lemma lincomb_scalar_prod_left: assumes "W  carrier_vec n" "v  carrier_vec n"
  shows "lincomb a W  v = (wW. a w * (w  v))"
  unfolding lincomb_def
  by (subst finsum_scalar_prod_sum, insert assms, auto intro!: sum.cong)

lemma lincomb_scalar_prod_right: assumes "W  carrier_vec n" "v  carrier_vec n"
  shows "v  lincomb a W = (wW. a w * (v  w))"
  unfolding lincomb_def
  by (subst finsum_scalar_prod_sum', insert assms, auto intro!: sum.cong)

lemma lin_indpt_empty[simp]: "lin_indpt {}"
  using lin_dep_def by auto

lemma span_carrier_lin_indpt_card_n:
  assumes "W  carrier_vec n" "card W = n" "lin_indpt W"
  shows "span W = carrier_vec n"
  using assms basis_def dim_is_n dim_li_is_basis fin_dim_li_fin by simp

lemma ortho_span: assumes W: "W  carrier_vec n"
  and X: "X  carrier_vec n"
  and ortho: " w x. w  W  x  X  w  x = 0"
  and w: "w  span W" and x: "x  X"
shows "w  x = 0"
proof -
  from w W obtain c V where "finite V" and VW: "V  W" and w: "w = lincomb c V"
    by (meson in_spanE)
  show ?thesis unfolding w
    by (subst lincomb_scalar_prod_left, insert W VW X x ortho, auto intro!: sum.neutral)
qed

lemma ortho_span': assumes W: "W  carrier_vec n"
  and X: "X  carrier_vec n"
  and ortho: " w x. w  W  x  X  x  w = 0"
  and w: "w  span W" and x: "x  X"
shows "x  w = 0"
proof -
  from w W obtain c V where "finite V" and VW: "V  W" and w: "w = lincomb c V"
    by (meson in_spanE)
  show ?thesis unfolding w
    by (subst lincomb_scalar_prod_right, insert W VW X x ortho, auto intro!: sum.neutral)
qed

lemma ortho_span_span: assumes W: "W  carrier_vec n"
  and X: "X  carrier_vec n"
  and ortho: " w x. w  W  x  X  w  x = 0"
  and w: "w  span W" and x: "x  span X"
shows "w  x = 0"
  by (rule ortho_span[OF W _ ortho_span'[OF X W _ _] w x], insert W X ortho, auto)

lemma lincomb_in_span[intro]:
  assumes X: "X carrier_vec n"
  shows "lincomb a X  span X"
proof(cases "finite X")
  case False hence "lincomb a X = 0v n" using X
    by (simp add: lincomb_def)
  thus ?thesis using X by force
qed (insert X, auto)

lemma generating_card_n_basis: assumes X: "X  carrier_vec n"
  and span: "carrier_vec n  span X"
  and card: "card X = n"
shows "basis X"
proof -
  have fin: "finite X"
  proof (cases "n = 0")
    case False
    with card show "finite X" by (meson card.infinite)
  next
    case True
    with X have "X  carrier_vec 0" by auto
    also have " = {0v 0}" by auto
    finally have "X  {0v 0}" .
    from finite_subset[OF this] show "finite X" by auto
  qed
  from X have "span X  carrier_vec n" by auto
  with span have span: "span X = carrier_vec n" by auto
  from dim_is_n card have card: "card X  dim" by auto
  from dim_gen_is_basis[OF fin X span card] show "basis X" .
qed

lemma lincomb_list_append:
  assumes Ws: "set Ws  carrier_vec n"
  shows "set Vs  carrier_vec n  lincomb_list f (Vs @ Ws) =
    lincomb_list f Vs + lincomb_list (λ i. f (i + length Vs)) Ws"
proof (induction Vs arbitrary: f)
  case Nil show ?case by(simp add: lincomb_list_carrier[OF Ws])
next
  case (Cons x Vs)
  have "lincomb_list f (x # (Vs @ Ws)) = f 0 v x + lincomb_list (f  Suc) (Vs @ Ws)"
    by (rule lincomb_list_Cons)
  also have "lincomb_list (f  Suc) (Vs @ Ws) =
             lincomb_list (f  Suc) Vs + lincomb_list (λ i. (f  Suc) (i + length Vs)) Ws"
    using Cons by auto
  also have "(λ i. (f  Suc) (i + length Vs)) = (λ i. f (i + length (x # Vs)))" by simp
  also have "f 0 v x + ((lincomb_list (f  Suc) Vs) + lincomb_list  Ws) =
             (f 0 v x + (lincomb_list (f  Suc) Vs)) + lincomb_list  Ws"
    using assoc_add_vec Cons.prems Ws lincomb_list_carrier by auto
  finally show ?case using lincomb_list_Cons by auto
qed

lemma lincomb_list_snoc[simp]:
  shows "set Vs  carrier_vec n  x  carrier_vec n 
          lincomb_list f (Vs @ [x]) = lincomb_list f Vs + f (length Vs) v x"
  using lincomb_list_append by auto

lemma lincomb_list_smult:
  "set Vs  carrier_vec n  lincomb_list (λ i. a * c i) Vs = a v lincomb_list c Vs"
proof (induction Vs rule: rev_induct)
  case (snoc x Vs)
  have x: "x  carrier_vec n" and Vs: "set Vs  carrier_vec n" using snoc.prems by auto
  have "lincomb_list (λ i. a * c i) (Vs @ [x]) =
        lincomb_list (λ i. a * c i) Vs + (a * c (length Vs)) v x"
    using x Vs by auto
  also have "lincomb_list (λ i. a * c i) Vs = a v lincomb_list c Vs"
    by(rule snoc.IH[OF Vs])
  also have "(a * c (length Vs)) v x = a v (c (length Vs) v x)"
    using smult_smult_assoc x by auto
  also have "a v lincomb_list c Vs +  = a v (lincomb_list c Vs + c (length Vs) v x)"
    using smult_add_distrib_vec[of _ n _ a] lincomb_list_carrier[OF Vs] x by simp
  also have "lincomb_list c Vs + c (length Vs) v x = lincomb_list c (Vs @ [x])"
    using Vs x by auto
  finally show ?case by auto
qed simp

lemma lincomb_list_index:
  assumes i: "i < n"
  shows "set Xs  carrier_vec n 
         lincomb_list c Xs $ i = sum (λ j. c j * (Xs ! j) $ i) {0..<length Xs}"
proof (induction Xs rule: rev_induct)
  case (snoc x Xs)
  hence x: "x  carrier_vec n" and Xs: "set Xs  carrier_vec n" by auto
  hence "lincomb_list c (Xs @ [x]) = lincomb_list c Xs + c (length Xs) v x" by auto
  also have " $ i = lincomb_list c Xs $ i + (c (length Xs) v x) $ i"
    using i index_add_vec(1) x by simp
  also have "(c (length Xs) v x) $ i = c (length Xs) * x $ i" using i x by simp
  also have "x $ i= (Xs @ [x]) ! (length Xs) $ i" by simp
  also have "lincomb_list c Xs $ i = (j = 0..<length Xs. c j * Xs ! j $ i)"
    by (rule snoc.IH[OF Xs])
  also have " =  (j = 0..<length Xs. c j * (Xs @ [x]) ! j $ i)"
    by (rule R.finsum_restrict, force, rule restrict_ext, auto simp: append_Cons_nth_left)
  finally show ?case
    using sum.atLeast0_lessThan_Suc[of "λ j. c j * (Xs @ [x]) ! j $ i" "length Xs"]
    by fastforce
qed (simp add: i)

end
end

Theory Basis_Extension

section ‹Basis Extension›

text ‹We prove that every linear indepent set/list of vectors can be extended into a basis.
  Similarly, from every set of vectors one can extract a linear independent set of vectors
  that spans the same space.›

theory Basis_Extension
  imports
    LLL_Basis_Reduction.Gram_Schmidt_2
begin


context cof_vec_space
begin

lemma lin_indpt_list_length_le_n: assumes "lin_indpt_list xs"
  shows "length xs  n"
proof -
  from assms[unfolded lin_indpt_list_def]
  have xs: "set xs  carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
  from dist have "card (set xs) = length xs" by (rule distinct_card)
  moreover have "card (set xs)  n"
    using lin xs dim_is_n li_le_dim(2) by auto
  ultimately show ?thesis by auto
qed

lemma lin_indpt_list_length_eq_n: assumes "lin_indpt_list xs"
  and "length xs = n"
shows "span (set xs) = carrier_vec n" "basis (set xs)"
proof -
  from assms[unfolded lin_indpt_list_def]
  have xs: "set xs  carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
  from dist have "card (set xs) = length xs" by (rule distinct_card)
  with assms have "card (set xs) = n" by auto
  with lin xs show "span (set xs) = carrier_vec n" "basis (set xs)"  using dim_is_n
    by (metis basis_def dim_basis dim_li_is_basis fin_dim finite_basis_exists gen_ge_dim li_le_dim(1))+
qed

lemma expand_to_basis: assumes lin: "lin_indpt_list xs"
  shows " ys. set ys  set (unit_vecs n)  lin_indpt_list (xs @ ys)  length (xs @ ys) = n"
proof -
  define y where "y = n - length xs"
  from lin have "length xs  n" by (rule lin_indpt_list_length_le_n)
  hence "length xs + y = n" unfolding y_def by auto
  thus " ys. set ys  set (unit_vecs n)  lin_indpt_list (xs @ ys)  length (xs @ ys) = n"
    using lin
  proof (induct y arbitrary: xs)
    case (0 xs)
    thus ?case by (intro exI[of _ Nil], auto)
  next
    case (Suc y xs)
    hence "length xs < n" by auto
    from Suc(3)[unfolded lin_indpt_list_def]
    have xs: "set xs  carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
    from distinct_card[OF dist] Suc(2) have card: "card (set xs) < n" by auto
    have "span (set xs)  carrier_vec n" using card dim_is_n xs basis_def dim_basis lin by auto
    with span_closed[OF xs] have "span (set xs)  carrier_vec n" by auto
    also have "carrier_vec n = span (set (unit_vecs n))"
      unfolding span_unit_vecs_is_carrier ..
    finally have sub: "span (set xs)  span (set (unit_vecs n))" .
    have " u. u  set (unit_vecs n)  u  span (set xs)"
      using span_subsetI[OF xs, of "set (unit_vecs n)"] sub by force
    then obtain u where uu: "u  set (unit_vecs n)" and usxs: "u  span (set xs)" by auto
    then have u: "u  carrier_vec n" unfolding unit_vecs_def by auto
    let ?xs = "xs @ [u]"
    from span_mem[OF xs, of u] usxs have uxs: "u  set xs" by auto
    with dist have dist: "distinct ?xs" by auto
    have lin: "lin_indpt (set ?xs)" using lin_dep_iff_in_span[OF xs lin u uxs] usxs by auto
    from lin dist u xs have lin: "lin_indpt_list ?xs" unfolding lin_indpt_list_def by auto
    from Suc(2) have "length ?xs + y = n" by auto
    from Suc(1)[OF this lin] obtain ys where
      "set ys  set (unit_vecs n)" "lin_indpt_list (?xs @ ys)" "length (?xs @ ys) = n" by auto
    thus ?case using uu
      by (intro exI[of _ "u # ys"], auto)
  qed
qed

definition "basis_extension xs = (SOME ys.
  set ys  set (unit_vecs n)  lin_indpt_list (xs @ ys)  length (xs @ ys) = n)"

lemma basis_extension: assumes "lin_indpt_list xs"
  shows "set (basis_extension xs)  set (unit_vecs n)"
    "lin_indpt_list (xs @ basis_extension xs)"
    "length (xs @ basis_extension xs) = n"
  using someI_ex[OF expand_to_basis[OF assms], folded basis_extension_def] by auto

lemma exists_lin_indpt_sublist: assumes X: "X  carrier_vec n"
  shows " Ls. lin_indpt_list Ls  span (set Ls) = span X  set Ls  X"
proof -
  let ?T = ?thesis
  have "( Ls. lin_indpt_list Ls  span (set Ls)  span X  set Ls  X  length Ls = k)  ?T" for k
  proof (induct k)
    case 0
    have "lin_indpt {}" by (simp add: lindep_span)
    thus ?case using span_is_monotone by (auto simp: lin_indpt_list_def)
  next
    case (Suc k)
    show ?case
    proof (cases ?T)
      case False
      with Suc obtain Ls where lin: "lin_indpt_list Ls"
        and span: "span (set Ls)  span X" and Ls: "set Ls  X"  and len: "length Ls = k" by auto
      from Ls X have LsC: "set Ls  carrier_vec n" by auto
      show ?thesis
      proof (cases "X  span (set Ls)")
        case True
        hence "span X  span (set Ls)" using LsC X by (metis span_subsetI)
        with span have "span (set Ls) = span X" by auto
        hence ?T by (intro exI[of _ Ls] conjI True lin Ls)
        thus ?thesis by auto
      next
        case False
        with span obtain x where xX: "x  X" and xSLs: "x  span (set Ls)" by auto
        from Ls X have LsC: "set Ls  carrier_vec n" by auto
        from span_mem[OF this, of x] xSLs have xLs: "x  set Ls" by auto
        let ?Ls = "x # Ls"
        show ?thesis
        proof (intro disjI1 exI[of _ ?Ls] conjI)
          show "length ?Ls = Suc k" using len by auto
          show "lin_indpt_list ?Ls" using lin xSLs xLs unfolding lin_indpt_list_def
            using lin_dep_iff_in_span[OF LsC _ _ xLs] xX X by auto
          show "set ?Ls  X" using xX Ls by auto
          from span_is_monotone[OF this]
          show "span (set ?Ls)  span X" .
        qed
      qed
    qed auto
  qed
  from this[of "n + 1"] lin_indpt_list_length_le_n show ?thesis by fastforce
qed

lemma exists_lin_indpt_subset: assumes "X  carrier_vec n"
  shows " Ls. lin_indpt Ls  span (Ls) = span X  Ls  X"
proof -
  from exists_lin_indpt_sublist[OF assms]
  obtain Ls where "lin_indpt_list Ls  span (set Ls) = span X  set Ls  X" by auto
  thus ?thesis by (intro exI[of _ "set Ls"], auto simp: lin_indpt_list_def)
qed
end

end

Theory Sum_Vec_Set

section ‹Sum of Vector Sets›

text ‹We use Isabelle's Set-Algebra theory to be able to write V + W for sets of vectors V and W,
 and prove some obvious properties about them.›
theory Sum_Vec_Set
  imports
    Missing_Matrix
    "HOL-Library.Set_Algebras"
begin


lemma add_0_right_vecset:
  assumes "(A :: 'a :: monoid_add vec set)  carrier_vec n"
  shows "A + {0v n} = A"
  unfolding set_plus_def using assms by force

lemma add_0_left_vecset:
  assumes "(A :: 'a :: monoid_add vec set)  carrier_vec n"
  shows "{0v n} + A = A"
  unfolding set_plus_def using assms by force

lemma assoc_add_vecset:
  assumes "(A :: 'a :: semigroup_add vec set)  carrier_vec n"
    and "B  carrier_vec n"
    and "C  carrier_vec n"
  shows "A + (B + C) = (A + B) + C"
proof -
  {
    fix x
    assume "x  A + (B + C)"
    then obtain a b c where "x = a + (b + c)" and *: "a  A" "b  B" "c  C"
      unfolding set_plus_def by auto
    with assms have "x = (a + b) + c" using assoc_add_vec[of a n b c] by force
    with * have "x  (A + B) + C" by auto
  }
  moreover
  {
    fix x
    assume "x  (A + B) + C"
    then obtain a b c where "x = (a + b) + c" and *: "a  A" "b  B" "c  C"
      unfolding set_plus_def by auto
    with assms have "x = a + (b + c)" using assoc_add_vec[of a n b c] by force
    with * have "x  A + (B + C)" by auto
  }
  ultimately show ?thesis by blast
qed

lemma sum_carrier_vec[intro]: "A  carrier_vec n  B  carrier_vec n  A + B  carrier_vec n"
  unfolding set_plus_def by force

lemma comm_add_vecset:
  assumes "(A :: 'a :: ab_semigroup_add vec set)  carrier_vec n"
    and "B  carrier_vec n"
  shows "A + B = B + A"
  unfolding set_plus_def using comm_add_vec assms by blast


end

Theory Integral_Bounded_Vectors

section ‹Integral and Bounded Matrices and Vectors›

text ‹We define notions of integral vectors and matrices and bounded vectors and matrices
  and prove some preservation lemmas. Moreover, we prove a bound on determinants.›
theory Integral_Bounded_Vectors
  imports
    Missing_VS_Connect
    Sum_Vec_Set
    LLL_Basis_Reduction.Gram_Schmidt_2 (* for some simp-rules *)
begin

(* TODO: move into theory Norms *)
lemma sq_norm_unit_vec[simp]: assumes i: "i < n"
  shows "unit_vec n i2 = (1 :: 'a :: {comm_ring_1,conjugatable_ring})"
proof -
  from i have id: "[0..<n] = [0..<i] @ [i] @ [Suc i ..< n]"
    by (metis append_Cons append_Nil diff_zero length_upt list_trisect)
  show ?thesis unfolding sq_norm_vec_def unit_vec_def
    by (auto simp: o_def id, subst (1 2) sum_list_0, auto)
qed

definition Ints_vec ("v") where
  "v = {x.  i < dim_vec x. x $ i  }"

definition indexed_Ints_vec  where
  "indexed_Ints_vec I = {x.  i < dim_vec x. i  I  x $ i  }"

lemma indexed_Ints_vec_UNIV: "v = indexed_Ints_vec UNIV"
  unfolding Ints_vec_def indexed_Ints_vec_def by auto

lemma indexed_Ints_vec_subset: "v  indexed_Ints_vec I"
  unfolding Ints_vec_def indexed_Ints_vec_def by auto

lemma Ints_vec_vec_set: "v  v = (vec_set v  )"
  unfolding Ints_vec_def vec_set_def by auto

definition Ints_mat ("m") where
  "m = {A.  i < dim_row A.  j < dim_col A. A $$ (i,j)  }"

lemma Ints_mat_elements_mat: "A  m = (elements_mat A  )"
  unfolding Ints_mat_def elements_mat_def by force

lemma minus_in_Ints_vec_iff[simp]: "(-x)  v  (x :: 'a :: ring_1 vec)  v"
  unfolding Ints_vec_vec_set by (auto simp: minus_in_Ints_iff)

lemma minus_in_Ints_mat_iff[simp]: "(-A)  m  (A :: 'a :: ring_1 mat)  m"
  unfolding Ints_mat_elements_mat by (auto simp: minus_in_Ints_iff)

lemma Ints_vec_rows_Ints_mat[simp]: "set (rows A)  v  A  m"
  unfolding rows_def Ints_vec_def Ints_mat_def by force

lemma unit_vec_integral[simp,intro]: "unit_vec n i  v"
  unfolding Ints_vec_def by (auto simp: unit_vec_def)

lemma diff_indexed_Ints_vec:
  "x  carrier_vec n  y  carrier_vec n  x  indexed_Ints_vec I  y  indexed_Ints_vec I
   x - y  indexed_Ints_vec I"
  unfolding indexed_Ints_vec_def by auto

lemma smult_indexed_Ints_vec: "x    v  indexed_Ints_vec I  x v v  indexed_Ints_vec I" 
  unfolding indexed_Ints_vec_def smult_vec_def by simp

lemma add_indexed_Ints_vec:
  "x  carrier_vec n  y  carrier_vec n  x  indexed_Ints_vec I  y  indexed_Ints_vec I
   x + y  indexed_Ints_vec I"
  unfolding indexed_Ints_vec_def by auto

lemma (in vec_space) lincomb_indexed_Ints_vec: assumes cI: " x. x  C  c x  "
  and C: "C  carrier_vec n"
  and CI: "C  indexed_Ints_vec I"
shows "lincomb c C  indexed_Ints_vec I"
proof -
  from C have id: "dim_vec (lincomb c C) = n" by auto
  show ?thesis unfolding indexed_Ints_vec_def mem_Collect_eq id
  proof (intro allI impI)
    fix i
    assume i: "i < n" and iI: "i  I"
    have "lincomb c C $ i = (xC. c x * x $ i)"
      by (rule lincomb_index[OF i C])
    also have "  "
      by (intro Ints_sum Ints_mult cI, insert i iI CI[unfolded indexed_Ints_vec_def] C, force+)
    finally show "lincomb c C $ i  " .
  qed
qed

definition "Bounded_vec (b :: 'a :: linordered_idom) = {x .  i < dim_vec x . abs (x $ i)  b}"

lemma Bounded_vec_vec_set: "v  Bounded_vec b  ( x  vec_set v. abs x  b)"
  unfolding Bounded_vec_def vec_set_def by auto

definition "Bounded_mat (b :: 'a :: linordered_idom) =
  {A . ( i < dim_row A .  j < dim_col A. abs (A $$ (i,j))  b)}"

lemma Bounded_mat_elements_mat: "A  Bounded_mat b  ( x  elements_mat A. abs x  b)"
  unfolding Bounded_mat_def elements_mat_def by auto

lemma Bounded_vec_rows_Bounded_mat[simp]: "set (rows A)  Bounded_vec B  A  Bounded_mat B"
  unfolding rows_def Bounded_vec_def Bounded_mat_def by force

lemma unit_vec_Bounded_vec[simp,intro]: "unit_vec n i  Bounded_vec (max 1 Bnd)"
  unfolding Bounded_vec_def unit_vec_def by auto

lemma Bounded_matD: assumes "A  Bounded_mat b"
  "A  carrier_mat nr nc"
shows "i < nr  j < nc  abs (A $$ (i,j))  b"
  using assms unfolding Bounded_mat_def by auto

lemma Bounded_vec_mono: "b  B  Bounded_vec b  Bounded_vec B"
  unfolding Bounded_vec_def by auto

lemma Bounded_mat_mono: "b  B  Bounded_mat b  Bounded_mat B"
  unfolding Bounded_mat_def by force

lemma finite_Bounded_vec_Max:
  assumes A: "A  carrier_vec n"
    and fin: "finite A"
  shows "A  Bounded_vec (Max { abs (a $ i) | a i. a  A  i < n})"
proof
  let ?B = "{ abs (a $ i) | a i. a  A  i < n}"
  have fin: "finite ?B"
    by (rule finite_subset[of _ "(λ (a,i). abs (a $ i)) ` (A × {0 ..< n})"], insert fin, auto)
  fix a
  assume a: "a  A"
  show "a  Bounded_vec (Max ?B)"
    unfolding Bounded_vec_def
    by (standard, intro allI impI Max_ge[OF fin], insert a A, force)
qed

definition det_bound :: "nat  'a :: linordered_idom  'a" where
  "det_bound n x = fact n * (x^n)"

lemma det_bound: assumes A: "A  carrier_mat n n"
  and x: "A  Bounded_mat x"
shows "abs (det A)  det_bound n x"
proof -
  have "abs (det A) = abs (p | p permutes {0..<n}. signof p * (i = 0..<n. A $$ (i, p i)))"
    unfolding det_def'[OF A] ..
  also have "  (p | p permutes {0..<n}. abs (signof p * (i = 0..<n. A $$ (i, p i))))"
    by (rule sum_abs)
  also have " = (p | p permutes {0..<n}. (i = 0..<n. abs (A $$ (i, p i))))"
    by (rule sum.cong[OF refl], auto simp: abs_mult abs_prod signof_def)
  also have "  (p | p permutes {0..<n}. (i = 0..<n. x))"
    by (intro sum_mono prod_mono conjI Bounded_matD[OF x A], auto)
  also have " = fact n * x^n" by (auto simp add: card_permutations)
  finally show "abs (det A)  det_bound n x" unfolding det_bound_def by auto
qed

lemma minus_in_Bounded_vec[simp]:
  "(-x)  Bounded_vec b  x  Bounded_vec b"
  unfolding Bounded_vec_def by auto

lemma sum_in_Bounded_vecI[intro]: assumes
  xB: "x  Bounded_vec B1" and
  yB: "y  Bounded_vec B2" and
  x: "x  carrier_vec n" and
  y: "y  carrier_vec n"
shows "x + y  Bounded_vec (B1 + B2)"
proof -
  from x y have id: "dim_vec (x + y) = n" by auto
  show ?thesis unfolding Bounded_vec_def mem_Collect_eq id
  proof (intro allI impI)
    fix i
    assume i: "i < n"
    with x y xB yB have *: "abs (x $ i)  B1" "abs (y $ i)  B2"
      unfolding Bounded_vec_def by auto
    thus "¦(x + y) $ i¦  B1 + B2" using i x y by simp
  qed
qed

lemma (in gram_schmidt) lincomb_card_bound: assumes XBnd: "X  Bounded_vec Bnd"
  and X: "X  carrier_vec n"
  and Bnd: "Bnd  0"
  and c: " x. x  X  abs (c x)  1"
  and card: "card X  k"
shows "lincomb c X  Bounded_vec (of_nat k * Bnd)"
proof -
  from X have dim: "dim_vec (lincomb c X) = n" by auto
  show ?thesis unfolding Bounded_vec_def mem_Collect_eq dim
  proof (intro allI impI)
    fix i
    assume i: "i < n"
    have "abs (lincomb c X $ i) = abs (xX. c x * x $ i)"
      by (subst lincomb_index[OF i X], auto)
    also have "  (xX. abs (c x * x $ i))" by auto
    also have " = (xX. abs (c x) * abs (x $ i))" by (auto simp: abs_mult)
    also have "  (xX. 1 * abs (x $ i))"
      by (rule sum_mono[OF mult_right_mono], insert c, auto)
    also have " = (xX. abs (x $ i))" by simp
    also have "  (xX. Bnd)"
      by (rule sum_mono, insert i XBnd[unfolded Bounded_vec_def] X, force)
    also have " = of_nat (card X) * Bnd" by simp
    also have "  of_nat k * Bnd"
      by (rule mult_right_mono[OF _ Bnd], insert card, auto)
    finally show "abs (lincomb c X $ i)  of_nat k * Bnd" by auto
  qed
qed

lemma bounded_vecset_sum:
  assumes Acarr: "A  carrier_vec n"
    and Bcarr: "B  carrier_vec n"
    and sum: "C = A + B"
    and Cbnd: " bndC. C  Bounded_vec bndC"
  shows "A  {}  ( bndB. B  Bounded_vec bndB)"
    and "B  {}  ( bndA. A  Bounded_vec bndA)"
proof -
  {
    fix A B :: "'a vec set"
    assume Acarr: "A  carrier_vec n"
    assume Bcarr: "B  carrier_vec n"
    assume sum: "C = A + B"
    assume Ane: "A  {}"
    have " bndB. B  Bounded_vec bndB"
    proof(cases "B = {}")
      case Bne: False
      from Cbnd obtain bndC where bndC: "C  Bounded_vec bndC" by auto
      from Ane obtain a where aA: "a  A" and acarr: "a  carrier_vec n" using Acarr by auto
      let ?M = "{abs (a $ i) | i. i < n}"
      have finM: "finite ?M" by simp
      define nb where "nb = abs bndC + Max ?M"
      {
        fix b
        assume bB: "b  B" and bcarr: "b  carrier_vec n"
        have ab: "a + b  Bounded_vec bndC" using aA bB bndC sum by auto
        {
          fix i
          assume i_lt_n: "i < n"
          hence ai_le_max: "abs(a $ i)  Max ?M" using acarr finM Max_ge by blast
          hence "abs(a $ i + b $ i)  abs bndC"
            using ab bcarr acarr index_add_vec(1) i_lt_n unfolding Bounded_vec_def by auto
          hence "abs(b $ i)  abs bndC + abs(a $ i)" by simp
          hence "abs(b $ i)  nb" using i_lt_n bcarr ai_le_max unfolding nb_def by simp
        }
        hence "b  Bounded_vec nb" unfolding Bounded_vec_def using bcarr carrier_vecD by blast
      }
      hence "B  Bounded_vec nb" unfolding Bounded_vec_def using Bcarr by auto
      thus ?thesis by auto
    qed auto
  } note theor = this
  show "A  {}  ( bndB. B  Bounded_vec bndB)" using theor[OF Acarr Bcarr sum] by simp
  have CBA: "C = B + A" unfolding sum by (rule comm_add_vecset[OF Acarr Bcarr])
  show "B  {}   bndA. A  Bounded_vec bndA" using theor[OF Bcarr Acarr CBA] by simp
qed

end

Theory Cone

section ‹Cones›

text ‹We define the notions like cone, polyhedral cone, etc. and prove some basic facts about them.›

theory Cone
  imports
    Basis_Extension
    Missing_VS_Connect
    Integral_Bounded_Vectors
begin

context gram_schmidt
begin

definition "nonneg_lincomb c Vs b = (lincomb c Vs = b  c ` Vs  {x. x  0})"
definition "nonneg_lincomb_list c Vs b = (lincomb_list c Vs = b  ( i < length Vs. c i  0))"

definition finite_cone :: "'a vec set  'a vec set" where
  "finite_cone Vs = ({ b.  c. nonneg_lincomb c (if finite Vs then Vs else {}) b})"

definition cone :: "'a vec set  'a vec set" where
  "cone Vs = ({ x.  Ws. finite Ws  Ws  Vs  x  finite_cone Ws})"

definition cone_list :: "'a vec list  'a vec set" where
  "cone_list Vs = {b. c. nonneg_lincomb_list c Vs b}"

lemma finite_cone_iff_cone_list: assumes Vs: "Vs  carrier_vec n"
  and id: "Vs = set Vsl"
shows "finite_cone Vs = cone_list Vsl"
proof -
  have fin: "finite Vs" unfolding id by auto
  from Vs id have Vsl: "set Vsl  carrier_vec n" by auto
  {
    fix c b
    assume b: "lincomb c Vs = b" and c: "c ` Vs  {x. x  0}"
    from lincomb_as_lincomb_list[OF Vsl, of c]
    have b: "lincomb_list (λi. if j<i. Vsl ! i = Vsl ! j then 0 else c (Vsl ! i)) Vsl = b"
      unfolding b[symmetric] id by simp
    have " c. nonneg_lincomb_list c Vsl b"
      unfolding nonneg_lincomb_list_def
      apply (intro exI conjI, rule b)
      by (insert c, auto simp: set_conv_nth id)
  }
  moreover
  {
    fix c b
    assume b: "lincomb_list c Vsl = b" and c: "( i < length Vsl. c i  0)"
    have "nonneg_lincomb (mk_coeff Vsl c) Vs b"
      unfolding b[symmetric] nonneg_lincomb_def
      apply (subst lincomb_list_as_lincomb[OF Vsl])
      by (insert c, auto simp: id mk_coeff_def intro!: sum_list_nonneg)
    hence " c. nonneg_lincomb c Vs b" by blast
  }
  ultimately show ?thesis unfolding finite_cone_def cone_list_def
      nonneg_lincomb_def nonneg_lincomb_list_def using fin by auto
qed

lemma cone_alt_def: assumes Vs: "Vs  carrier_vec n"
  shows "cone Vs = ({ x.  Ws. set Ws  Vs  x  cone_list Ws})"
  unfolding cone_def
proof (intro Collect_cong iffI)
  fix x
  assume "Ws. finite Ws  Ws  Vs  x  finite_cone Ws"
  then obtain Ws where *: "finite Ws" "Ws  Vs" "x  finite_cone Ws" by auto
  from finite_list[OF *(1)] obtain Wsl where id: "Ws = set Wsl" by auto
  from finite_cone_iff_cone_list[OF _ this] *(2-3) Vs
  have "x  cone_list Wsl" by auto
  with *(2) id show "Wsl. set Wsl  Vs  x  cone_list Wsl" by blast
next
  fix x
  assume "Wsl. set Wsl  Vs  x  cone_list Wsl"
  then obtain Wsl where "set Wsl  Vs" "x  cone_list Wsl" by auto
  thus "Ws. finite Ws  Ws  Vs  x  finite_cone Ws" using Vs
    by (intro exI[of _ "set Wsl"], subst finite_cone_iff_cone_list, auto)
qed

lemma cone_mono: "Vs  Ws  cone Vs  cone Ws"
  unfolding cone_def by blast

lemma finite_cone_mono: assumes fin: "finite Ws"
  and Ws: "Ws  carrier_vec n"
  and sub: "Vs  Ws"
shows "finite_cone Vs  finite_cone Ws"
proof
  fix b
  assume "b  finite_cone Vs"
  then obtain c where b: "b = lincomb c Vs" and c: "c ` Vs  {x. x  0}"
    unfolding finite_cone_def nonneg_lincomb_def using finite_subset[OF sub fin] by auto
  define d where "d = (λ v. if v  Vs then c v else 0)"
  from c have d: "d ` Ws  {x. x  0}" unfolding d_def by auto
  have "lincomb d Ws = lincomb d (Ws - Vs) + lincomb d Vs"
    by (rule lincomb_vec_diff_add[OF Ws sub fin], auto)
  also have "lincomb d Vs = lincomb c Vs"
    by (rule lincomb_cong, insert Ws sub, auto simp: d_def)
  also have "lincomb d (Ws - Vs) = 0v n"
    by (rule lincomb_zero, insert Ws sub, auto simp: d_def)
  also have "0v n + lincomb c Vs = lincomb c Vs" using Ws sub by auto
  also have " = b" unfolding b by simp
  finally
  have "b = lincomb d Ws" by auto
  then show "b  finite_cone Ws" using d fin
    unfolding finite_cone_def nonneg_lincomb_def by auto
qed

lemma finite_cone_carrier: "A  carrier_vec n  finite_cone A  carrier_vec n"
  unfolding finite_cone_def nonneg_lincomb_def by auto

lemma cone_carrier: "A  carrier_vec n  cone A  carrier_vec n"
  using finite_cone_carrier unfolding cone_def by blast

lemma cone_iff_finite_cone: assumes A: "A  carrier_vec n"
  and fin: "finite A"
shows "cone A = finite_cone A"
proof
  show "finite_cone A  cone A" unfolding cone_def using fin by auto
  show "cone A  finite_cone A" unfolding cone_def using fin finite_cone_mono[OF fin A] by auto
qed

lemma set_in_finite_cone:
  assumes Vs: "Vs  carrier_vec n"
    and fin: "finite Vs"
  shows "Vs  finite_cone Vs"
proof
  fix x
  assume x: "x  Vs"
  show "x  finite_cone Vs" unfolding finite_cone_def
  proof
    let ?c = "λ y. if x = y then 1 else 0 :: 'a"
    have Vsx: "Vs - {x}  carrier_vec n" using Vs by auto
    have "lincomb ?c Vs = x + lincomb ?c (Vs - {x})"
      using lincomb_del2 x Vs fin by auto
    also have "lincomb ?c (Vs - {x}) = 0v n" using lincomb_zero Vsx by auto
    also have "x + 0v n = x " using M.r_zero Vs x by auto
    finally have "lincomb ?c Vs = x" by auto
    moreover have "?c ` Vs  {z. z  0}" by auto
    ultimately show "c. nonneg_lincomb c (if finite Vs then Vs else {}) x"
      unfolding nonneg_lincomb_def
      using fin by auto
  qed
qed

lemma set_in_cone:
  assumes Vs: "Vs  carrier_vec n"
  shows "Vs  cone Vs"
proof
  fix x
  assume x: "x  Vs"
  show "x  cone Vs" unfolding cone_def
  proof (intro CollectI exI)
    have "x  carrier_vec n" using Vs x by auto
    then have "x  finite_cone {x}" using set_in_finite_cone by auto
    then show "finite {x}  {x}  Vs  x  finite_cone {x}" using x by auto
  qed
qed

lemma zero_in_finite_cone:
  assumes Vs: "Vs  carrier_vec n"
  shows "0v n  finite_cone Vs"
proof -
  let ?Vs = "(if finite Vs then Vs else {})"
  have "lincomb (λ x. 0 :: 'a) ?Vs = 0v n" using lincomb_zero Vs by auto
  moreover have "(λ x. 0 :: 'a) ` ?Vs  {y. y  0}" by auto
  ultimately show ?thesis unfolding finite_cone_def nonneg_lincomb_def by blast
qed

lemma lincomb_in_finite_cone:
  assumes "x = lincomb l W"
    and "finite W"
    and "i  W . l i  0"
    and "W  carrier_vec n"
  shows "x  finite_cone W"
  using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto

lemma lincomb_in_cone:
  assumes "x = lincomb l W"
    and "finite W"
    and "i  W . l i  0"
    and "W  carrier_vec n"
  shows "x  cone W"
  using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto

lemma zero_in_cone: "0v n  cone Vs"
proof -
  have "finite {}" by auto
  moreover have "{}  cone Vs" by auto
  moreover have "0v n  finite_cone {}" using zero_in_finite_cone by auto
  ultimately show ?thesis unfolding cone_def by blast
qed

lemma cone_smult:
  assumes a: "a  0"
    and Vs: "Vs  carrier_vec n"
    and x: "x  cone Vs"
  shows "a v x  cone Vs"
proof -
  from x Vs obtain Ws c where Ws: "Ws  Vs" and fin: "finite Ws" and
    "nonneg_lincomb c Ws x"
    unfolding cone_def finite_cone_def by auto
  then have "nonneg_lincomb (λ w. a * c w) Ws (a v x)"
    unfolding nonneg_lincomb_def using a lincomb_distrib Vs by auto
  then show ?thesis using Ws fin unfolding cone_def finite_cone_def by auto
qed

lemma finite_cone_empty[simp]: "finite_cone {} = {0v n}"
  by (auto simp: finite_cone_def nonneg_lincomb_def)

lemma cone_empty[simp]: "cone {} = {0v n}"
  unfolding cone_def by simp


lemma cone_elem_sum:
  assumes Vs: "Vs  carrier_vec n"
    and x: "x  cone Vs"
    and y: "y  cone Vs"
  shows "x + y  cone Vs"
proof -
  obtain Xs where Xs: "Xs  Vs" and fin_Xs: "finite Xs"
    and Xs_cone: "x  finite_cone Xs"
    using Vs x unfolding cone_def by auto
  obtain Ys where Ys: "Ys  Vs" and fin_Ys: "finite Ys"
    and Ys_cone: "y  finite_cone Ys"
    using Vs y unfolding cone_def
    by auto
  have "x  finite_cone (Xs  Ys)" and "y  finite_cone (Xs  Ys)"
    using finite_cone_mono fin_Xs fin_Ys Xs Ys Vs Xs_cone Ys_cone
    by (blast, blast)
  then obtain cx cy where "nonneg_lincomb cx (Xs  Ys) x"
    and "nonneg_lincomb cy (Xs  Ys) y"
    unfolding finite_cone_def using fin_Xs fin_Ys by auto
  hence "nonneg_lincomb (λ v. cx v + cy v) (Xs  Ys) (x + y)"
    unfolding nonneg_lincomb_def
    using lincomb_sum[of "Xs  Ys" cx cy] fin_Xs fin_Ys Xs Ys Vs
    by fastforce
  hence "x + y  finite_cone (Xs  Ys)"
    unfolding finite_cone_def using fin_Xs fin_Ys by auto
  thus ?thesis unfolding cone_def using fin_Xs fin_Ys Xs Ys by auto
qed

lemma cone_cone:
  assumes Vs: "Vs  carrier_vec n"
  shows "cone (cone Vs) = cone Vs"
proof
  show "cone Vs  cone (cone Vs)"
    by (rule set_in_cone[OF cone_carrier[OF Vs]])
next
  show "cone (cone Vs)  cone Vs"
  proof
    fix x
    assume x: "x  cone (cone Vs)"
    then obtain Ws c where Ws: "set Ws  cone Vs"
      and c: "nonneg_lincomb_list c Ws x"
      using cone_alt_def Vs cone_carrier unfolding cone_list_def by auto

    have "set Ws  cone Vs  nonneg_lincomb_list c Ws x  x  cone Vs"
    proof (induction Ws arbitrary: x c)
      case Nil
      hence "x = 0v n" unfolding nonneg_lincomb_list_def by auto
      thus "x  cone Vs" using zero_in_cone by auto
    next
      case (Cons a Ws)
      have "a  cone Vs" using Cons.prems(1) by auto
      moreover have "c 0  0"
        using Cons.prems(2) unfolding nonneg_lincomb_list_def by fastforce
      ultimately have "c 0 v a  cone Vs" using cone_smult Vs by auto
      moreover have "lincomb_list (c  Suc) Ws  cone Vs"
        using Cons unfolding nonneg_lincomb_list_def by fastforce
      moreover have "x = c 0 v a + lincomb_list (c  Suc) Ws"
        using Cons.prems(2) unfolding nonneg_lincomb_list_def
        by auto
      ultimately show "x  cone Vs" using cone_elem_sum Vs by auto
    qed

    thus "x  cone Vs" using Ws c by auto
  qed
qed

lemma cone_smult_basis:
  assumes Vs: "Vs  carrier_vec n"
    and l: "l ` Vs  {x. x > 0}"
  shows "cone {l v v v | v . v  Vs} = cone Vs"
proof
  have "{l v v v |v. v  Vs}  cone Vs"
  proof
    fix x
    assume "x  {l v v v | v. v  Vs}"
    then obtain v where "v  Vs" and "x = l v v v" by auto
    thus "x  cone Vs" using
        set_in_cone[OF Vs] cone_smult[OF _ Vs, of "l v" v] l by fastforce
  qed
  thus "cone {l v v v | v. v  Vs}  cone Vs"
    using cone_mono cone_cone[OF Vs] by blast
next
  have lVs: "{l v v v | v. v  Vs}  carrier_vec n" using Vs by auto
  have "Vs  cone {l v v v | v. v  Vs}"
  proof
    fix v assume v: "v  Vs"
    hence "l v v v  cone {l v v v | v. v  Vs}" using set_in_cone[OF lVs] by auto
    moreover have "1 / l v > 0" using l v by auto
    ultimately have "(1 / l v) v (l v v v)  cone {l v v v | v. v  Vs}"
      using cone_smult[OF _ lVs] by auto
    also have "(1 / l v) v (l v v v) = v" using l v
      by(auto simp add: smult_smult_assoc)
    finally show "v  cone {l v v v | v. v  Vs}" by auto
  qed
  thus "cone Vs  cone {l v v v | v. v  Vs}"
    using cone_mono cone_cone[OF lVs] by blast
qed

lemma cone_add_cone:
  assumes C: "C  carrier_vec n"
  shows "cone C + cone C = cone C"
proof
  note CC = cone_carrier[OF C]
  have "cone C = cone C + {0v n}" by (subst add_0_right_vecset[OF CC], simp)
  also have "  cone C + cone C"
    by (rule set_plus_mono2, insert zero_in_cone, auto)
  finally show "cone C  cone C + cone C" by auto
  from cone_elem_sum[OF C]
  show "cone C + cone C  cone C"
    by (auto elim!: set_plus_elim)
qed

lemma orthogonal_cone:
  assumes X: "X  carrier_vec n"
    and W: "W  carrier_vec n"
    and finX: "finite X"
    and spanLW: "span (set Ls  W) = carrier_vec n"
    and ortho: " w x. w  W  x  set Ls  w  x = 0"
    and WWs: "W = set Ws"
    and spanL: "span (set Ls) = span X"
    and LX: "set Ls  X"
    and lin_Ls_Bs: "lin_indpt_list (Ls @ Bs)"
    and len_Ls_Bs: "length (Ls @ Bs) = n"
  shows "cone (X  set Bs)  {x  carrier_vec n. wW. w  x = 0} = cone X"
    " x. wW. w  x = 0  Z  X  B  set Bs  x = lincomb c (Z  B)
     x = lincomb c (Z - B)"
proof -
  from WWs have finW: "finite W" by auto
  define Y where "Y = X  set Bs"
  from lin_Ls_Bs[unfolded lin_indpt_list_def] have
    Ls: "set Ls  carrier_vec n" and
    Bs: "set Bs  carrier_vec n" and
    distLsBs: "distinct (Ls @ Bs)" and
    lin: "lin_indpt (set (Ls @ Bs))"  by auto
  have LW: "set Ls  W = {}"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain x where xX: "x  set Ls" and xW: "x  W" by auto
    from ortho[OF xW xX] have "x  x = 0" by auto
    hence "sq_norm x = 0" by (auto simp: sq_norm_vec_as_cscalar_prod)
    with vs_zero_lin_dep[OF _ lin] xX Ls Bs show False by auto
  qed
  have Y: "Y  carrier_vec n" using X Bs unfolding Y_def by auto
  have CLB: "carrier_vec n = span (set (Ls @ Bs))"
    using lin_Ls_Bs len_Ls_Bs lin_indpt_list_length_eq_n by blast
  also have "  span Y"
    by (rule span_is_monotone, insert LX, auto simp: Y_def)
  finally have span: "span Y = carrier_vec n" using Y by auto
  have finY: "finite Y" using finX finW unfolding Y_def by auto
  {
    fix x Z B d
    assume xX: "wW. w  x = 0" and ZX: "Z  X" and B: "B  set Bs" and
      xd: "x = lincomb d (Z  B)"
    from ZX B X Bs have ZB: "Z  B  carrier_vec n" by auto
    with xd have x: "x  carrier_vec n" by auto
    from xX W have w0: "w  W  w  x = 0" for w by auto
    from finite_in_span[OF _ _ x[folded spanLW]] Ls X W finW finX
    obtain c where xc: "x = lincomb c (set Ls  W)" by auto
    have "x = lincomb c (set Ls  W)" unfolding xc by auto
    also have " = lincomb c (set Ls) + lincomb c W"
      by (rule lincomb_union, insert X LX W LW finW, auto)
    finally have xsum: "x = lincomb c (set Ls) + lincomb c W" .
    {
      fix w
      assume wW: "w  W"
      with W have w: "w  carrier_vec n" by auto
      from w0[OF wW, unfolded xsum]
      have "0 = w  (lincomb c (set Ls) + lincomb c W)" by simp
      also have " = w  lincomb c (set Ls) + w  lincomb c W"
        by (rule scalar_prod_add_distrib[OF w], insert Ls W, auto)
      also have "w  lincomb c (set Ls) = 0" using ortho[OF wW]
        by (subst lincomb_scalar_prod_right[OF Ls w], auto)
      finally have "w  lincomb c W = 0" by simp
    }
    hence "lincomb c W  lincomb c W = 0" using W
      by (subst lincomb_scalar_prod_left, auto)
    hence "sq_norm (lincomb c W) = 0"
      by (auto simp: sq_norm_vec_as_cscalar_prod)
    hence 0: "lincomb c W = 0v n" using lincomb_closed[OF W, of c] by simp
    have xc: "x = lincomb c (set Ls)" unfolding xsum 0 using Ls by auto
    hence xL: "x  span (set Ls)" by auto
    let ?X = "Z - B"
    have "lincomb d ?X  span X" using finite_subset[OF _ finX, of ?X] X ZX by auto
    from finite_in_span[OF finite_set Ls this[folded spanL]]
    obtain e where ed: "lincomb e (set Ls) = lincomb d ?X" by auto
    from B finite_subset[OF B] have finB: "finite B" by auto
    from B Bs have BC: "B  carrier_vec n" by auto
    define f where "f =
      (λ x. if x  set Bs then if x  B then d x else 0 else if x  set Ls then e x else undefined)"
    have "x = lincomb d (?X  B)" unfolding xd by auto
    also have " = lincomb d ?X + lincomb d B"
      by (rule lincomb_union[OF _ _ _ finite_subset[OF _ finX]], insert ZX X finB B Bs, auto)
    finally have xd: "x = lincomb d ?X + lincomb d B" .
    also have " = lincomb e (set Ls) + lincomb d B" unfolding ed by auto
    also have "lincomb e (set Ls) = lincomb f (set Ls)"
      by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: f_def)
    also have "lincomb d B = lincomb f B"
      by (rule lincomb_cong[OF _ BC], insert B, auto simp: f_def)
    also have "lincomb f B = lincomb f (B  (set Bs - B))"
      by (subst lincomb_clean, insert finB Bs B, auto simp: f_def)
    also have "B  (set Bs - B) = set Bs" using B by auto
    finally have "x = lincomb f (set Ls) + lincomb f (set Bs)" by auto
    also have "lincomb f (set Ls) + lincomb f (set Bs) = lincomb f (set (Ls @ Bs))"
      by (subst lincomb_union[symmetric], insert Ls distLsBs Bs, auto)
    finally have "x = lincomb f (set (Ls @ Bs))" .
    hence f: "f  set (Ls @ Bs) E UNIV  lincomb f (set (Ls @ Bs)) = x"
      by (auto simp: f_def split: if_splits)
    from finite_in_span[OF finite_set Ls xL] obtain g where
      xg: "x = lincomb g (set Ls)" by auto
    define h where "h = (λ x. if x  set Bs then 0 else if x  set Ls then g x else undefined)"
    have "x = lincomb h (set Ls)" unfolding xg
      by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: h_def)
    also have " = lincomb h (set Ls) + 0v n" using Ls by auto
    also have "0v n = lincomb h (set Bs)"
      by (rule lincomb_zero[symmetric, OF Bs], auto simp: h_def)
    also have "lincomb h (set Ls) + lincomb h (set Bs) = lincomb h (set (Ls @ Bs))"
      by (subst lincomb_union[symmetric], insert Ls Bs distLsBs, auto)
    finally have "x = lincomb h (set (Ls @ Bs))" .
    hence h: "h  set (Ls @ Bs) E UNIV  lincomb h (set (Ls @ Bs)) = x"
      by (auto simp: h_def split: if_splits)
    have basis: "basis (set (Ls @ Bs))" using lin_Ls_Bs[unfolded lin_indpt_list_def] len_Ls_Bs
      using CLB basis_def by blast
    from Ls Bs have "set (Ls @ Bs)  carrier_vec n" by auto
    from basis[unfolded basis_criterion[OF finite_set this], rule_format, OF x] f h
    have fh: "f = h" by auto
    hence " x. x  set Bs  f x = 0" unfolding h_def by auto
    hence " x. x  B  d x = 0" unfolding f_def using B by force
    thus "x = lincomb d ?X" unfolding xd
      by (subst (2) lincomb_zero, insert BC ZB X, auto intro!: M.r_zero)
  } note main = this
  have "cone Y  {x  carrier_vec n. wW. w  x = 0} = cone X" (is "?I = _")
  proof
    {
      fix x
      assume xX: "x  cone X"
      with cone_carrier[OF X] have x: "x  carrier_vec n" by auto
      have "X  Y" unfolding Y_def by auto
      from cone_mono[OF this] xX have xY: "x  cone Y" by auto
      from cone_iff_finite_cone[OF X finX] xX have "x  finite_cone X" by auto
      from this[unfolded finite_cone_def nonneg_lincomb_def] finX obtain c
        where "x = lincomb c X" by auto
      with finX X have "x  span X" by auto
      with spanL have "x  span (set Ls)" by auto
      from finite_in_span[OF _ Ls this] obtain c where
        xc: "x = lincomb c (set Ls)" by auto
      {
        fix w
        assume wW: "w  W"
        hence w: "w  carrier_vec n" using W by auto
        have "w  x = 0" unfolding xc using ortho[OF wW]
          by (subst lincomb_scalar_prod_right[OF Ls w], auto)
      }
      with xY x have "x  ?I" by blast
    }
    thus "cone X  ?I" by blast
    {
      fix x
      let ?X = "X - set Bs"
      assume "x  ?I"
      with cone_carrier[OF Y] cone_iff_finite_cone[OF Y finY]
      have xY: "x  finite_cone Y" and x: "x  carrier_vec n"
        and w0: " w. w  W  w  x = 0" by auto
      from xY[unfolded finite_cone_def nonneg_lincomb_def] finY obtain d
        where xd: "x = lincomb d Y" and nonneg: "d ` Y  Collect ((≤) 0)" by auto
      from main[OF _ _ _ xd[unfolded Y_def]] w0
      have "x = lincomb d ?X" by auto
      hence "nonneg_lincomb d ?X x" unfolding nonneg_lincomb_def
        using nonneg[unfolded Y_def] by auto
      hence "x  finite_cone ?X" using finX
        unfolding finite_cone_def by auto
      hence "x  cone X" using finite_subset[OF _ finX, of ?X] unfolding cone_def by blast
    }
    then show "?I  cone X" by auto
  qed
  thus "cone (X  set Bs)  {x  carrier_vec n. wW. w  x = 0} = cone X" unfolding Y_def .
qed

definition "polyhedral_cone (A :: 'a mat) = { x . x  carrier_vec n  A *v x  0v (dim_row A)}"

lemma polyhedral_cone_carrier: assumes "A  carrier_mat nr n"
  shows "polyhedral_cone A  carrier_vec n"
  using assms unfolding polyhedral_cone_def by auto

lemma cone_in_polyhedral_cone:
  assumes CA: "C  polyhedral_cone A"
    and A: "A  carrier_mat nr n"
  shows "cone C  polyhedral_cone A"
proof
  interpret nr: gram_schmidt nr "TYPE ('a)".
  from polyhedral_cone_carrier[OF A] assms(1)
  have C: "C  carrier_vec n" by auto
  fix x
  assume x: "x  cone C"
  then have xn: "x  carrier_vec n"
    using cone_carrier[OF C] by auto
  from x[unfolded cone_alt_def[OF C] cone_list_def nonneg_lincomb_list_def]
  obtain ll Ds where l0: "lincomb_list ll Ds = x" and l1: "i<length Ds. 0  ll i"
    and DsC: "set Ds  C"
    by auto
  from DsC C have Ds: "set Ds  carrier_vec n" by auto

  have "A *v x = A *v (lincomb_list ll Ds)" using l0 by auto
  also have " = nr.lincomb_list ll (map (λ d. A *v d) Ds)"
  proof -
    have one: " wset Ds. dim_vec w = n" using DsC C by auto
    have two: "wset (map ((*v) A) Ds). dim_vec w = nr" using A DsC C by auto
    show "A *v lincomb_list ll Ds = nr.lincomb_list ll (map ((*v) A) Ds)"
      unfolding lincomb_list_as_mat_mult[OF one] nr.lincomb_list_as_mat_mult[OF two] length_map
    proof (subst assoc_mult_mat_vec[symmetric, OF A], force+, rule arg_cong[of _ _ "λ x. x *v _"])
      show "A * mat_of_cols n Ds = mat_of_cols nr (map ((*v) A) Ds)"
        unfolding mat_of_cols_def
        by (intro eq_matI, insert A Ds[unfolded set_conv_nth],
            (force intro!: arg_cong[of _ _ "λ x. row A _  x"])+)
    qed
  qed
  also have "  0v nr"
  proof (intro lesseq_vecI[of _ nr])
    have *: "set (map ((*v) A) Ds)  carrier_vec nr" using A Ds by auto
    show Carr: "nr.lincomb_list ll (map ((*v) A) Ds)  carrier_vec nr"
      by (intro nr.lincomb_list_carrier[OF *])
    fix i
    assume i: "i < nr"
    from CA[unfolded polyhedral_cone_def] A
    have l2: "x  C  A *v x  0v nr" for x by auto
    show "nr.lincomb_list ll (map ((*v) A) Ds) $ i  0v nr $ i"
      unfolding subst nr.lincomb_list_index[OF i *] length_map index_zero_vec(1)[OF i]
    proof (intro sum_nonpos mult_nonneg_nonpos)
      fix j
      assume "j  {0..<length Ds}"
      hence j: "j < length Ds" by auto
      from j show "0  ll j" using l1 by auto
      from j have "Ds ! j  C" using DsC by auto
      from l2[OF this] have l2: "A *v Ds ! j  0v nr" by auto
      from lesseq_vecD[OF _ this i] i have "(A *v Ds ! j) $ i  0" by auto
      thus "map ((*v) A) Ds ! j $ i  0" using j i by auto
    qed
  qed auto
  finally show "x  polyhedral_cone A"
    unfolding polyhedral_cone_def using A xn by auto
qed

lemma bounded_cone_is_zero:
  assumes Ccarr: "C  carrier_vec n" and bnd: "cone C  Bounded_vec bnd"
  shows "cone C = {0v n}"
proof(rule ccontr)
  assume "¬ ?thesis"
  then obtain v where vC: "v  cone C" and vnz: "v  0v n"
    using zero_in_cone assms by auto
  have vcarr: "v  carrier_vec n" using vC Ccarr cone_carrier by blast
  from vnz vcarr obtain i where i_le_n: "i < dim_vec v" and vinz: "v $ i  0" by force
  define M where "M = (1 / (v $ i) * (bnd + 1))"
  have abs_ge_bnd: "abs (M * (v $ i)) > bnd" unfolding M_def by (simp add: vinz)
  have aMvC: "(abs M) v v  cone C" using cone_smult[OF _ Ccarr vC] abs_ge_bnd by simp
  have "¬(abs (abs M * (v $ i))  bnd)" using abs_ge_bnd by simp
  hence "(abs M) v v  Bounded_vec bnd" unfolding Bounded_vec_def using i_le_n aMvC by auto
  thus False using aMvC bnd by auto
qed

lemma cone_of_cols: fixes A :: "'a mat" and b :: "'a vec"
  assumes A: "A  carrier_mat n nr" and b: "b  carrier_vec n"
  shows "b  cone (set (cols A))  ( x. x  0v nr  A *v x = b)"
proof -
  let ?C = "set (cols A)"
  from A have C: "?C  carrier_vec n" and C': " wset (cols A). dim_vec w = n"
    unfolding cols_def by auto
  have id: "finite ?C = True" "length (cols A) = nr" using A by auto
  have Aid: "mat_of_cols n (cols A) = A" using A unfolding mat_of_cols_def
    by (intro eq_matI, auto)
  show ?thesis
    unfolding cone_iff_finite_cone[OF C finite_set] finite_cone_iff_cone_list[OF C refl]
    unfolding cone_list_def nonneg_lincomb_list_def mem_Collect_eq id
    unfolding lincomb_list_as_mat_mult[OF C'] id Aid
  proof -
    {
      fix x
      assume "x0v nr" "A *v x = b"
      hence "c. A *v vec nr c = b  (i<nr. 0  c i)" using A b
        by (intro exI[of _ "λ i. x $ i"], auto simp: less_eq_vec_def intro!: arg_cong[of _ _ "(*v) A"])
    }
    moreover
    {
      fix c
      assume "A *v vec nr c = b" "(i<nr. 0  c i)"
      hence " x. x0v nr  A *v x = b"
        by (intro exI[of _ "vec nr c"], auto simp: less_eq_vec_def)
    }
    ultimately show "(c. A *v vec nr c = b  (i<nr. 0  c i)) = (x0v nr. A *v x = b)" by blast
  qed
qed

end
end

Theory Convex_Hull

section ‹Convex Hulls›

text ‹We define the notion of convex hull of a set or list of vectors and derive basic
  properties thereof.›

theory Convex_Hull
  imports Cone
begin

context gram_schmidt
begin

definition "convex_lincomb c Vs b = (nonneg_lincomb c Vs b  sum c Vs = 1)"

definition "convex_lincomb_list c Vs b = (nonneg_lincomb_list c Vs b  sum c {0..<length Vs} = 1)"

definition "convex_hull Vs = {x.  Ws c. finite Ws  Ws  Vs  convex_lincomb c Ws x}"

lemma convex_hull_carrier[intro]: "Vs  carrier_vec n  convex_hull Vs  carrier_vec n"
  unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto

lemma convex_hull_mono: "Vs  Ws  convex_hull Vs  convex_hull Ws"
  unfolding convex_hull_def by auto

lemma convex_lincomb_empty[simp]: "¬ (convex_lincomb c {} x)"
  unfolding convex_lincomb_def by simp

lemma set_in_convex_hull:
  assumes "A  carrier_vec n"
  shows "A  convex_hull A"
proof
  fix a
  assume "a  A"
  hence acarr: "a  carrier_vec n" using assms by auto
  hence "convex_lincomb (λ x. 1) {a} a " unfolding convex_lincomb_def
    by (auto simp: nonneg_lincomb_def lincomb_def)
  then show "a  convex_hull A" using a  A unfolding convex_hull_def by auto
qed

lemma convex_hull_empty[simp]:
  "convex_hull {} = {}"
  "A  carrier_vec n  convex_hull A = {}  A = {}"
proof -
  show "convex_hull {} = {}" unfolding convex_hull_def by auto
  then show "A  carrier_vec n  convex_hull A = {}  A = {}"
    using set_in_convex_hull[of A] by auto
qed

lemma convex_hull_bound: assumes XBnd: "X  Bounded_vec Bnd"
  and X: "X  carrier_vec n"
shows "convex_hull X  Bounded_vec Bnd"
proof
  fix x
  assume "x  convex_hull X"
  from this[unfolded convex_hull_def]
  obtain Y c where fin: "finite Y" and YX: "Y  X" and cx: "convex_lincomb c Y x" by auto
  from cx[unfolded convex_lincomb_def nonneg_lincomb_def]
  have x: "x = lincomb c Y" and sum: "sum c Y = 1" and c0: " y. y  Y  c y  0" by auto
  from YX X XBnd have Y: "Y  carrier_vec n" and YBnd: "Y  Bounded_vec Bnd" by auto
  from x Y have dim: "dim_vec x = n" by auto
  show "x  Bounded_vec Bnd" unfolding Bounded_vec_def mem_Collect_eq dim
  proof (intro allI impI)
    fix i
    assume i: "i < n"
    have "abs (x $ i) = abs (xY. c x * x $ i)" unfolding x
      by (subst lincomb_index[OF i Y], auto)
    also have "  (xY. abs (c x * x $ i))" by auto
    also have " = (xY. abs (c x) * abs (x $ i))" by (simp add: abs_mult)
    also have "  (xY. abs (c x) * Bnd)"
      by (intro sum_mono mult_left_mono, insert YBnd[unfolded Bounded_vec_def] i Y, force+)
    also have " = (xY. abs (c x)) * Bnd"
      by (simp add: sum_distrib_right)
    also have "(xY. abs (c x)) = (xY. c x)"
      by (rule sum.cong, insert c0, auto)
    also have " = 1" by fact
    finally show "¦x $ i¦  Bnd" by auto
  qed
qed

definition "convex_hull_list Vs = {x.  c. convex_lincomb_list c Vs x}"

lemma lincomb_list_elem:
  "set Vs  carrier_vec n 
   lincomb_list (λ j. if i=j then 1 else 0) Vs = (if i < length Vs then Vs ! i else 0v n)"
proof (induction Vs rule: rev_induct)
  case (snoc x Vs)
  have x: "x  carrier_vec n" and Vs: "set Vs  carrier_vec n" using snoc.prems by auto
  let ?f = "λ j. if i = j then 1 else 0"
  have "lincomb_list ?f (Vs @ [x]) = lincomb_list ?f Vs + ?f (length Vs) v x"
    using x Vs by simp
  also have " = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n)" (is ?goal)
    using less_linear[of i "length Vs"]
  proof (elim disjE)
    assume i: "i < length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = Vs ! i"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) v x = 0v n" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = Vs ! i"
      using i append_Cons_nth_left by fastforce
    ultimately show ?goal using Vs i lincomb_list_carrier M.r_zero by metis
  next
    assume i: "i = length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0v n"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) v x = x" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = x"
      using i append_Cons_nth_left by simp
    ultimately show ?goal using x by simp
  next
    assume i: "i > length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0v n"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) v x = 0v n" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = 0v n"
      using i by simp
    ultimately show ?goal by simp
  qed
  finally show ?case by auto
qed simp

lemma set_in_convex_hull_list: fixes Vs :: "'a vec list"
  assumes "set Vs  carrier_vec n"
  shows "set Vs  convex_hull_list Vs"
proof
  fix x assume "x  set Vs"
  then obtain i where i: "i < length Vs"
    and x: "x = Vs ! i" using set_conv_nth[of Vs] by auto
  let ?f = "λ j. if i = j then 1 else 0 :: 'a"
  have "lincomb_list ?f Vs = x" using i x lincomb_list_elem[OF assms] by auto
  moreover have " j < length Vs. ?f j  0" by auto
  moreover have "sum ?f {0..<length Vs} = 1" using i by simp
  ultimately show "x  convex_hull_list Vs"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
qed

lemma convex_hull_list_combination:
  assumes Vs: "set Vs  carrier_vec n"
    and x: "x  convex_hull_list Vs"
    and y: "y  convex_hull_list Vs"
    and l0: "0  l" and l1: "l  1"
  shows "l v x + (1 - l) v y  convex_hull_list Vs"
proof -
  from x obtain cx where x: "lincomb_list cx Vs = x" and cx0: " i < length Vs. cx i  0"
    and cx1: "sum cx {0..<length Vs} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  from y obtain cy where y: "lincomb_list cy Vs = y" and cy0: " i < length Vs. cy i  0"
    and cy1: "sum cy {0..<length Vs} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  let ?c = "λ i. l * cx i + (1 - l) * cy i"
  have "set Vs  carrier_vec n 
        lincomb_list ?c Vs = l v lincomb_list cx Vs + (1 - l) v lincomb_list cy Vs"
  proof (induction Vs rule: rev_induct)
    case (snoc v Vs)
    have v: "v  carrier_vec n" and Vs: "set Vs  carrier_vec n"
      using snoc.prems by auto
    have "lincomb_list ?c (Vs @ [v]) = lincomb_list ?c Vs + ?c (length Vs) v v"
      using snoc.prems by auto
    also have "lincomb_list ?c Vs =
               l v lincomb_list cx Vs + (1 - l) v lincomb_list cy Vs"
      by (rule snoc.IH[OF Vs])
    also have "?c (length Vs) v v =
               l v (cx (length Vs) v v) + (1 - l) v (cy (length Vs) v v)"
      using add_smult_distrib_vec smult_smult_assoc by metis
    also have "l v lincomb_list cx Vs + (1 - l) v lincomb_list cy Vs +  =
                  l v (lincomb_list cx Vs + cx (length Vs) v v) +
                  (1 - l) v (lincomb_list cy Vs + cy (length Vs) v v)"
      using lincomb_list_carrier[OF Vs] v
      by (simp add: M.add.m_assoc M.add.m_lcomm smult_r_distr)
    finally show ?case using Vs v by simp
  qed simp
  hence "lincomb_list ?c Vs = l v x + (1 - l) v y" using Vs x y by simp
  moreover have " i < length Vs. ?c i  0" using cx0 cy0 l0 l1 by simp
  moreover have "sum ?c {0..<length Vs} = 1"
  proof(simp add: sum.distrib)
    have "(i = 0..<length Vs. (1 - l) * cy i) = (1 - l) * sum cy {0..<length Vs}"
      using sum_distrib_left by metis
    moreover have "(i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}"
      using sum_distrib_left by metis
    ultimately show "(i = 0..<length Vs. l * cx i) + (i = 0..<length Vs. (1 - l) * cy i) = 1"
      using cx1 cy1 by simp
  qed
  ultimately show ?thesis
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
qed

lemma convex_hull_list_mono:
  assumes "set Ws  carrier_vec n"
  shows "set Vs  set Ws  convex_hull_list Vs  convex_hull_list Ws"
proof (standard, induction Vs)
  case Nil
  from Nil(2) show ?case unfolding convex_hull_list_def convex_lincomb_list_def by auto
next
  case (Cons v Vs)
  have v: "v  set Ws" and Vs: "set Vs  set Ws" using Cons.prems(1) by auto
  hence v1: "v  convex_hull_list Ws" using set_in_convex_hull_list[OF assms] by auto
  from Cons.prems(2) obtain c
    where x: "lincomb_list c (v # Vs) = x" and c0: " i < length Vs + 1. c i  0"
      and c1: "sum c {0..<length Vs + 1} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  have x: "x = c 0 v v + lincomb_list (c  Suc) Vs" using Vs v assms x by auto

  show ?case proof (cases)
    assume P: "c 0 = 1"
    hence "sum (c  Suc) {0..<length Vs} = 0"
      using sum.atLeast0_lessThan_Suc_shift c1
      by (metis One_nat_def R.show_r_zero add.right_neutral add_Suc_right)
    moreover have " i. i  {0..<length Vs}  (c  Suc) i  0"
      using c0 by simp
    ultimately have " i  {0..<length Vs}. (c  Suc) i = 0"
      using sum_nonneg_eq_0_iff by blast
    hence " i. i < length Vs  (c  Suc) i v Vs ! i = 0v n"
      using Vs assms by (simp add: subset_code(1))
    hence "lincomb_list (c  Suc) Vs = 0v n"
      using lincomb_list_eq_0 by simp
    hence "x = v" using P x v assms by auto
    thus ?case using v1 by auto

  next

    assume P: "c 0  1"
    have c1: "c 0 + sum (c  Suc) {0..<length Vs} = 1"
      using sum.atLeast0_lessThan_Suc_shift[of c] c1 by simp
    have "sum (c  Suc) {0..<length Vs}  0" by (rule sum_nonneg, insert c0, simp)
    hence "c 0 < 1" using P c1 by auto
    let ?c' = "λ i. 1 / (1 - c 0) * (c  Suc) i"
    have "sum ?c' {0..<length Vs} = 1 / (1 - c 0) * sum (c  Suc) {0..<length Vs}"
      using c1 P sum_distrib_left by metis
    hence "sum ?c' {0..<length Vs} = 1" using P c1 by simp
    moreover have " i < length Vs. ?c' i  0" using c0 c 0 < 1 by simp
    ultimately have c': "lincomb_list ?c' Vs  convex_hull_list Ws"
      using Cons.IH[OF Vs]
        convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
      by blast
    have "lincomb_list ?c' Vs = 1 / (1 - c 0) v lincomb_list (c  Suc) Vs"
      by(rule lincomb_list_smult, insert Vs assms, auto)
    hence "(1 - c 0) v lincomb_list ?c' Vs = lincomb_list (c  Suc) Vs"
      using P by auto
    hence "x = c 0 v v + (1 - c 0) v lincomb_list ?c' Vs" using x by auto
    thus "x  convex_hull_list Ws"
      using convex_hull_list_combination[OF assms v1 c'] c0 c 0 < 1
      by simp
  qed
qed

lemma convex_hull_list_eq_set:
  "set Vs  carrier_vec n  set Vs = set Ws  convex_hull_list Vs = convex_hull_list Ws"
  using convex_hull_list_mono by blast

lemma find_indices_empty: "(find_indices x Vs = []) = (x  set Vs)"
proof (induction Vs rule: rev_induct)
  case (snoc v Vs)
  show ?case
  proof
    assume "find_indices x (Vs @ [v]) = []"
    hence "x  v  find_indices x Vs = []" by auto
    thus "x  set (Vs @ [v])" using snoc by simp
  next
    assume "x  set (Vs @ [v])"
    hence "x  v  find_indices x Vs = []" using snoc by auto
    thus "find_indices x (Vs @ [v]) = []" by simp
  qed
qed simp

lemma distinct_list_find_indices:
  shows " i < length Vs; Vs ! i = x; distinct Vs   find_indices x Vs = [i]"
proof (induction Vs rule: rev_induct)
  case (snoc v Vs)
  have dist: "distinct Vs" and xVs: "v  set Vs" using snoc.prems(3) by(simp_all)
  show ?case
  proof (cases)
    assume i: "i = length Vs"
    hence "x = v" using snoc.prems(2) by auto
    thus ?case using xVs find_indices_empty i
      by fastforce
  next
    assume "i  length Vs"
    hence i: "i < length Vs" using snoc.prems(1) by simp
    hence Vsi: "Vs ! i = x" using snoc.prems(2) append_Cons_nth_left by fastforce
    hence "x  v" using snoc.prems(3) i by auto
    thus ?case using snoc.IH[OF i Vsi dist] by simp
  qed
qed auto

lemma finite_convex_hull_iff_convex_hull_list: assumes Vs: "Vs  carrier_vec n"
  and id': "Vs = set Vsl'"
shows "convex_hull Vs = convex_hull_list Vsl'"
proof -
  have fin: "finite Vs" unfolding id' by auto
  from finite_distinct_list fin obtain Vsl
    where id: "Vs = set Vsl" and dist: "distinct Vsl" by auto
  from Vs id have Vsl: "set Vsl  carrier_vec n" by auto
  {
    fix c :: "nat  'a"
    have "distinct Vsl (xset Vsl. sum_list (map c (find_indices x Vsl))) =
                          sum c {0..<length Vsl}"
    proof (induction Vsl rule: rev_induct)
      case (snoc v Vsl)
      let ?coef = "λ x. sum_list (map c (find_indices x (Vsl @ [v])))"
      let ?coef' = "λ x. sum_list (map c (find_indices x Vsl))"
      have dist: "distinct Vsl" using snoc.prems by simp
      have "sum ?coef (set (Vsl @ [v])) = sum_list (map ?coef (Vsl @ [v]))"
        by (rule sum.distinct_set_conv_list[OF snoc.prems, of ?coef])
      also have " = sum_list (map ?coef Vsl) + ?coef v" by simp
      also have "sum_list (map ?coef Vsl) = sum ?coef (set Vsl)"
        using sum.distinct_set_conv_list[OF dist, of ?coef] by auto
      also have " = sum ?coef' (set Vsl)"
      proof (intro R.finsum_restrict[of ?coef] restrict_ext, standard)
        fix x
        assume "x  set Vsl"
        then obtain i where i: "i < length Vsl" and x: "x = Vsl ! i"
          using in_set_conv_nth[of x Vsl] by blast
        hence "(Vsl @ [v]) ! i = x" by (simp add: append_Cons_nth_left)
        hence "?coef x = c i"
          using distinct_list_find_indices[OF _ _ snoc.prems] i by fastforce
        also have  "c i = ?coef' x"
          using distinct_list_find_indices[OF i _ dist] x by simp
        finally show "?coef x = ?coef' x" by auto
      qed
      also have " = sum c {0..<length Vsl}" by (rule snoc.IH[OF dist])
      also have "?coef v = c (length Vsl)"
        using distinct_list_find_indices[OF _ _ snoc.prems, of "length Vsl" v]
          nth_append_length by simp
      finally show ?case using sum.atLeast0_lessThan_Suc by simp
    qed simp
  } note sum_sumlist = this
  {
    fix b
    assume "b  convex_hull_list Vsl"
    then obtain c where b: "lincomb_list c Vsl = b" and c: "( i < length Vsl. c i  0)"
      and c1: "sum c {0..<length Vsl} = 1"
      unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
      by auto
    have "convex_lincomb (mk_coeff Vsl c) Vs b"
      unfolding b[symmetric] convex_lincomb_def nonneg_lincomb_def
      apply (subst lincomb_list_as_lincomb[OF Vsl])
      by (insert c c1, auto simp: id mk_coeff_def dist sum_sumlist intro!: sum_list_nonneg)
    hence "b  convex_hull Vs"
      unfolding convex_hull_def convex_lincomb_def using fin by blast
  }
  moreover
  {
    fix b
    assume "b  convex_hull Vs"
    then obtain c Ws where Ws: "Ws  Vs" and b: "lincomb c Ws = b"
      and c: "c ` Ws  {x. x  0}" and c1: "sum c Ws = 1"
      unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto
    let ?d = "λ x. if x  Ws then c x else 0"
    have "lincomb ?d Vs = lincomb c Ws + lincomb (λ x. 0) (Vs - Ws)"
      using lincomb_union2[OF _ _ Diff_disjoint[of Ws Vs], of c "λ x. 0"]
        fin Vs Diff_partition[OF Ws] by metis
    also have "lincomb (λ x. 0) (Vs - Ws) = 0v n"
      using lincomb_zero[of "Vs - Ws" "λ x. 0"] Vs by auto
    finally have "lincomb ?d Vs = b" using b lincomb_closed Vs Ws by auto
    moreover have "?d ` Vs  {t. t  0}" using c by auto
    moreover have "sum ?d Vs = 1" using  c1 R.extend_sum[OF fin Ws] by auto
    ultimately have " c. convex_lincomb c Vs b"
      unfolding convex_lincomb_def nonneg_lincomb_def by blast
  }
  moreover
  {
    fix b
    assume " c. convex_lincomb c Vs b"
    then obtain c where b: "lincomb c Vs = b" and c: "c ` Vs  {x. x  0}"
      and c1: "sum c Vs = 1"
      unfolding convex_lincomb_def nonneg_lincomb_def by auto
    from lincomb_as_lincomb_list_distinct[OF Vsl dist, of c]
    have b: "lincomb_list (λi. c (Vsl ! i)) Vsl = b"
      unfolding b[symmetric] id by simp
    have "1 = sum c (set Vsl)" using c1 id by auto
    also have " = sum_list (map c Vsl)" by(rule sum.distinct_set_conv_list[OF dist])
    also have " = sum ((!) (map c Vsl)) {0..<length Vsl}"
      using sum_list_sum_nth length_map by metis
    also have " = sum (λ i. c (Vsl ! i)) {0..<length Vsl}" by simp
    finally have sum_1: "(i = 0..<length Vsl. c (Vsl ! i)) = 1" by simp

    have " c. convex_lincomb_list c Vsl b"
      unfolding convex_lincomb_list_def nonneg_lincomb_list_def
      by (intro exI[of _ "λi. c (Vsl ! i)"] conjI b sum_1)
        (insert c, force simp: set_conv_nth id)
    hence "b  convex_hull_list Vsl" unfolding convex_hull_list_def by auto
  }
  ultimately have "convex_hull Vs = convex_hull_list Vsl" by auto
  also have "convex_hull_list Vsl = convex_hull_list Vsl'"
    using convex_hull_list_eq_set[OF Vsl, of Vsl'] id id' by simp
  finally show ?thesis by simp
qed

definition "convex S = (convex_hull S = S)"

lemma convex_convex_hull: "convex S  convex_hull S = S"
  unfolding convex_def by auto

lemma convex_hull_convex_hull_listD: assumes A: "A  carrier_vec n"
  and x: "x  convex_hull A"
shows " as. set as  A  x  convex_hull_list as"
proof -
  from x[unfolded convex_hull_def]
  obtain X c where finX: "finite X" and XA: "X  A" and "convex_lincomb c X x" by auto
  hence x: "x  convex_hull X" unfolding convex_hull_def by auto
  from finite_list[OF finX] obtain xs where X: "X = set xs" by auto
  from finite_convex_hull_iff_convex_hull_list[OF _ this] x XA A have x: "x  convex_hull_list xs" by auto
  thus ?thesis using XA unfolding X by auto
qed

lemma convex_hull_convex_sum: assumes A: "A  carrier_vec n"
  and x: "x  convex_hull A"
  and y: "y  convex_hull A"
  and a: "0  a" "a  1"
shows "a v x + (1 - a) v y  convex_hull A"
proof -
  from convex_hull_convex_hull_listD[OF A x] obtain xs where xs: "set xs  A"
    and x: "x  convex_hull_list xs" by auto
  from convex_hull_convex_hull_listD[OF A y] obtain ys where ys: "set ys  A"
    and y: "y  convex_hull_list ys" by auto
  have fin: "finite (set (xs @ ys))" by auto
  have sub: "set (xs @ ys)  A" using xs ys by auto
  from convex_hull_list_mono[of "xs @ ys" xs] x sub A have x: "x  convex_hull_list (xs @ ys)" by auto
  from convex_hull_list_mono[of "xs @ ys" ys] y sub A have y: "y  convex_hull_list (xs @ ys)" by auto
  from convex_hull_list_combination[OF _ x y a]
  have "a v x + (1 - a) v y  convex_hull_list (xs @ ys)" using sub A by auto
  from finite_convex_hull_iff_convex_hull_list[of _ "xs @ ys"] this sub A
  have "a v x + (1 - a) v y  convex_hull (set (xs @ ys))" by auto
  with convex_hull_mono[OF sub]
  show "a v x + (1 - a) v y  convex_hull A" by auto
qed

lemma convexI: assumes S: "S  carrier_vec n"
  and step: " a x y. x  S  y  S  0  a  a  1  a v x + (1 - a) v y  S"
shows "convex S"
  unfolding convex_def
proof (standard, standard)
  fix z
  assume "z  convex_hull S"
  from this[unfolded convex_hull_def] obtain W c where "finite W" and WS: "W  S"
    and "convex_lincomb c W z" by auto
  then show "z  S"
  proof (induct W arbitrary: c z)
    case empty
    thus ?case unfolding convex_lincomb_def by auto
  next
    case (insert w W c z)
    have "convex_lincomb c (insert w W) z" by fact
    hence zl: "z = lincomb c (insert w W)" and nonneg: " w. w  W  0  c w"
      and cw: "c w  0"
      and sum: "sum c (insert w W) = 1"
      unfolding convex_lincomb_def nonneg_lincomb_def by auto
    have zl: "z = c w v w + lincomb c W" unfolding zl
      by (rule lincomb_insert2, insert insert S, auto)
    have sum: "c w + sum c W = 1" unfolding sum[symmetric]
      by (subst sum.insert, insert insert, auto)
    have W: "W  carrier_vec n" and w: "w  carrier_vec n" using S insert by auto
    show ?case
    proof (cases "sum c W = 0")
      case True
      with nonneg have c0: " w. w  W  c w = 0"
        using insert(1) sum_nonneg_eq_0_iff by auto
      with sum have cw: "c w = 1" by auto
      have lin0: "lincomb c W = 0v n"
        by (intro lincomb_zero W, insert c0, auto)
      have "z = w" unfolding zl cw lin0 using w by simp
      with insert(4) show ?thesis by simp
    next
      case False
      have "sum c W  0" using nonneg by (metis sum_nonneg)
      with False have pos: "sum c W > 0" by auto
      define b where "b = (λ w. inverse (sum c W) * c w)"
      have "convex_lincomb b W (lincomb b W)"
        unfolding convex_lincomb_def nonneg_lincomb_def b_def
      proof (intro conjI refl)
        show "(λw. inverse (sum c W) * c w) ` W  Collect ((≤) 0)" using nonneg pos by auto
        show "(wW. inverse (sum c W) * c w) = 1" unfolding sum_distrib_left[symmetric] using False by auto
      qed
      from insert(3)[OF _ this] insert
      have IH: "lincomb b W  S" by auto
      have lin: "lincomb c W = sum c W v lincomb b W"
        unfolding b_def
        by (subst lincomb_smult[symmetric, OF W], rule lincomb_cong[OF _ W], insert False, auto)
      from sum cw pos have sum: "sum c W = 1 - c w" and cw1: "c w  1" by auto
      show ?thesis unfolding zl lin unfolding sum
        by (rule step[OF _ IH cw cw1], insert insert, auto)
    qed
  qed
next
  show "S  convex_hull S" using S by (rule set_in_convex_hull)
qed

lemma convex_hulls_are_convex: assumes "A  carrier_vec n"
  shows "convex (convex_hull A)"
  by (intro convexI convex_hull_convex_sum convex_hull_carrier assms)

lemma convex_hull_sum: assumes A: "A  carrier_vec n" and B: "B  carrier_vec n"
  shows "convex_hull (A + B) = convex_hull A + convex_hull B"
proof
  note cA = convex_hull_carrier[OF A]
  note cB = convex_hull_carrier[OF B]
  have "convex (convex_hull A + convex_hull B)"
  proof (intro convexI sum_carrier_vec convex_hull_carrier A B)
    fix a :: 'a and x1 x2
    assume "x1  convex_hull A + convex_hull B" "x2  convex_hull A + convex_hull B"
    then obtain y1 y2 z1 z2 where
      x12: "x1 = y1 + z1" "x2 = y2 + z2" and
      y12: "y1  convex_hull A" "y2  convex_hull A" and
      z12: "z1  convex_hull B" "z2  convex_hull B"
      unfolding set_plus_def by auto
    from y12 z12 cA cB have carr:
      "y1  carrier_vec n" "y2  carrier_vec n"
      "z1  carrier_vec n" "z2  carrier_vec n"
      by auto
    assume a: "0  a" "a  1"
    have A: "a v y1 + (1 - a) v y2  convex_hull A" using y12 a A by (metis convex_hull_convex_sum)
    have B: "a v z1 + (1 - a) v z2  convex_hull B" using z12 a B by (metis convex_hull_convex_sum)
    have "a v x1 + (1 - a) v x2 = (a v y1 + a v z1) + ((1 - a) v y2 + (1 - a) v z2)" unfolding x12
      using carr by (auto simp: smult_add_distrib_vec)
    also have " = (a v y1 + (1 - a) v y2) + (a v z1 + (1 - a) v z2)" using carr
      by (intro eq_vecI, auto)
    finally show "a v x1 + (1 - a) v x2  convex_hull A + convex_hull B"
      using A B by auto
  qed
  from convex_convex_hull[OF this]
  have id: "convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B" .
  show "convex_hull (A + B)  convex_hull A + convex_hull B"
    by (subst id[symmetric], rule convex_hull_mono[OF set_plus_mono2]; intro set_in_convex_hull A B)
  show "convex_hull A + convex_hull B  convex_hull (A + B)"
  proof
    fix x
    assume "x  convex_hull A + convex_hull B"
    then obtain y z where x: "x = y + z" and y: "y  convex_hull A" and z: "z  convex_hull B"
      by (auto simp: set_plus_def)
    from convex_hull_convex_hull_listD[OF A y] obtain ys where ysA: "set ys  A" and
      y: "y  convex_hull_list ys" by auto
    from convex_hull_convex_hull_listD[OF B z] obtain zs where zsB: "set zs  B" and
      z: "z  convex_hull_list zs" by auto
    from y[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
    obtain c where yid: "y = lincomb_list c ys"
      and conv_c: "(i<length ys. 0  c i)  sum c {0..<length ys} = 1"
      by auto
    from z[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
    obtain d where zid: "z = lincomb_list d zs"
      and conv_d: "(i<length zs. 0  d i)  sum d {0..<length zs} = 1"
      by auto
    from ysA A have ys: "set ys  carrier_vec n" by auto
    from zsB B have zs: "set zs  carrier_vec n" by auto
    have [intro, simp]: "lincomb_list x ys  carrier_vec n" for x using lincomb_list_carrier[OF ys] .
    have [intro, simp]: "lincomb_list x zs  carrier_vec n" for x using lincomb_list_carrier[OF zs] .
    have dim[simp]: "dim_vec (lincomb_list d zs) = n" by auto
    from yid have y: "y  carrier_vec n" by auto
    from zid have z: "z  carrier_vec n" by auto
    {
      fix x
      assume "x  set (map ((+) y) zs)"
      then obtain z where "x = y + z" and "z  set zs" by auto
      then obtain j where j: "j < length zs" and x: "x = y + zs ! j" unfolding set_conv_nth by auto
      hence mem: "zs ! j  set zs" by auto
      hence zsj: "zs ! j  carrier_vec n" using zs by auto
      let ?list = "(map (λ y. y + zs ! j) ys)"
      let ?set = "set ?list"
      have set: "?set  carrier_vec n" using ys A zsj by auto
      have lin_map: "lincomb_list c ?list  carrier_vec n"
        by (intro lincomb_list_carrier[OF set])
      have "y + (zs ! j) = lincomb_list c ?list"
        unfolding yid using zsj lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ ys]
        by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_c)
      hence "convex_lincomb_list c ?list (y + (zs ! j))"
        unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_c by auto
      hence "y + (zs ! j)  convex_hull_list ?list" unfolding convex_hull_list_def by auto
      with finite_convex_hull_iff_convex_hull_list[OF set refl]
      have "(y + zs ! j)  convex_hull ?set" by auto
      also have "  convex_hull (A + B)"
        by (rule convex_hull_mono, insert mem ys ysA zsB, force simp: set_plus_def)
      finally have "x  convex_hull (A + B)" unfolding x .
    } note step1 = this
    {
      let ?list = "map ((+) y) zs"
      let ?set = "set ?list"
      have set: "?set  carrier_vec n" using zs B y by auto
      have lin_map: "lincomb_list d ?list  carrier_vec n"
        by (intro lincomb_list_carrier[OF set])
      have [simp]: "i < n  (j = 0..<length zs. d j * (y + zs ! j) $ i) =
        (j = 0..<length zs. d j * (y $ i + zs ! j $ i))" for i
        by (rule sum.cong, insert zs[unfolded set_conv_nth] y, auto)
      have "y + z = lincomb_list d ?list"
        unfolding zid using y zs lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ zs]
          set lincomb_list_carrier[OF zs, of d] zs[unfolded set_conv_nth]
        by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_d)
      hence "convex_lincomb_list d ?list x" unfolding x
        unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_d by auto
      hence "x  convex_hull_list ?list" unfolding convex_hull_list_def by auto
      with finite_convex_hull_iff_convex_hull_list[OF set refl]
      have "x  convex_hull ?set" by auto
      also have "  convex_hull (convex_hull (A + B))"
        by (rule convex_hull_mono, insert step1, auto)
      also have " = convex_hull (A + B)"
        by (rule convex_convex_hull[OF convex_hulls_are_convex], intro sum_carrier_vec A B)
      finally show "x  convex_hull (A + B)" .
    }
  qed
qed

lemma convex_hull_in_cone:
  "convex_hull C  cone C"
  unfolding convex_hull_def cone_def convex_lincomb_def finite_cone_def by auto

lemma convex_cone:
  assumes C: "C  carrier_vec n"
  shows "convex (cone C)"
  unfolding convex_def
  using convex_hull_in_cone set_in_convex_hull[OF cone_carrier[OF C]] cone_cone[OF C]
  by blast

end
end

Theory Normal_Vector

section ‹Normal Vectors›

text ‹We provide a function for the normal vector of a half-space (given as n-1 linearly
  independent vectors).
  We further provide a function that returns a list of normal vectors that span the
  orthogonal complement of some subspace of $R^n$.
  Bounds for all normal vectors are provided.›

theory Normal_Vector
  imports
    Integral_Bounded_Vectors
    Basis_Extension
begin

context gram_schmidt
begin
  (* TODO move *)
lemma ortho_sum_in_span:
  assumes W: "W  carrier_vec n"
    and X: "X  carrier_vec n"
    and ortho: " w x. w  W  x  X  x  w = 0"
    and inspan: "lincomb l1 X + lincomb l2 W  span X"
  shows "lincomb l2 W = 0v n"
proof (rule ccontr)
  let ?v = "lincomb l2 W"
  have vcarr: "?v  carrier_vec n" using W by auto
  have vspan: "?v  span W" using W by auto
  assume "¬?thesis"
  from this have vnz: "?v  0v n" by auto
  let ?x = "lincomb l1 X"
  have xcarr: "?x  carrier_vec n" using X by auto
  have xspan: "?x  span X" using X xcarr by auto
  have "0  sq_norm ?v" using vnz vcarr by simp
  also have "sq_norm ?v = 0 + ?v  ?v" by (simp add: sq_norm_vec_as_cscalar_prod)
  also have " = ?x  ?v + ?v  ?v"
    by (subst (2) ortho_span_span[OF X W ortho], insert X W, auto)
  also have " = (?x + ?v )  ?v" using xcarr vcarr
    using add_scalar_prod_distrib by force
  also have " = 0"
    by (rule ortho_span_span[OF X W ortho inspan vspan])
  finally show False by simp
qed

(* TODO move *)
lemma ortho_lin_indpt: assumes W: "W  carrier_vec n"
  and X: "X  carrier_vec n"
  and ortho: " w x. w  W  x  X  x  w = 0"
  and linW: "lin_indpt W"
  and linX: "lin_indpt X"
shows "lin_indpt (W  X)"
proof (rule ccontr)
  assume "¬?thesis"
  from this obtain c where zerocomb:"lincomb c (W  X) = 0v n"
    and notallz: "v  (W  X). c v  0"
    using assms fin_dim fin_dim_li_fin finite_lin_indpt2 infinite_Un le_sup_iff
    by metis
  have zero_nin_W: "0v n  W" using assms by (metis vs_zero_lin_dep)
  have WXinters: "W  X = {}"
  proof (rule ccontr)
    assume "¬?thesis"
    from this obtain v where v: "v W  X" by auto
    hence "vv=0" using ortho by auto
    moreover have "v  carrier_vec n" using assms v by auto
    ultimately have "v=0v n" using sq_norm_vec_as_cscalar_prod[of v] by auto
    then show False using zero_nin_W v by auto
  qed
  have finX: "finite X" using X linX by (simp add: fin_dim_li_fin)
  have finW: "finite W" using W linW by (simp add: fin_dim_li_fin)
  have split: "lincomb c (W  X) = lincomb c X + lincomb c W"
    using lincomb_union[OF W X WXinters finW finX]
    by (simp add: M.add.m_comm W X)
  hence "lincomb c X + lincomb c W   span X" using zerocomb
    using local.span_zero by auto
  hence z1: "lincomb c W = 0v n"
    using ortho_sum_in_span[OF W X ortho] by simp
  hence z2: "lincomb c X = 0v n" using split zerocomb X by simp
  have or: "(v  W. c v  0)  ( v X. c v  0)" using notallz by auto
  have ex1: "v  W. c v  0  False" using linW
    using finW lin_dep_def z1 by blast
  have ex2: " v X. c v  0  False" using linX
    using finX lin_dep_def z2 by blast
  show False using ex1 ex2 or by auto
qed

definition normal_vector :: "'a vec set  'a vec" where
  "normal_vector W = (let ws = (SOME ws. set ws = W  distinct ws);
     m = length ws;
     B = (λ j. mat m m (λ(i, j'). ws ! i $ (if j' < j then j' else Suc j')))
     in vec n (λ j. (-1)^(m+j) * det (B j)))"

lemma normal_vector: assumes fin: "finite W"
  and card: "Suc (card W) = n"
  and lin: "lin_indpt W"
  and W: "W  carrier_vec n"
shows "normal_vector W  carrier_vec n"
  "normal_vector W  0v n"
  "w  W  w  normal_vector W = 0"
  "w  W  normal_vector W  w = 0"
  "lin_indpt (insert (normal_vector W) W)"
  "normal_vector W  W"
  "W  v  Bounded_vec Bnd  normal_vector W  v  Bounded_vec (det_bound (n-1) Bnd)"
proof -
  define ws where "ws = (SOME ws. set ws = W  distinct ws)"
  from finite_distinct_list[OF fin]
  have " ws. set ws = W  distinct ws" by auto
  from someI_ex[OF this, folded ws_def] have id: "set ws = W" and dist: "distinct ws" by auto
  have len: "length ws = card W" using distinct_card[OF dist] id by auto
  let ?n = "length ws"
  define B where "B = (λ j. mat ?n ?n (λ(i, j'). ws ! i $ (if j' < j then j' else Suc j')))"
  define nv where "nv = vec n (λ j. (-1)^(?n+j) * det (B j))"
  have nv2: "normal_vector W = nv" unfolding normal_vector_def Let_def
      ws_def[symmetric] B_def nv_def ..
  define A where "A = (λ w. mat_of_rows n (ws @ [w]))"
  from len id card have len: "Suc ?n = n" by auto
  have A: "A w  carrier_mat n n" for w using id W len unfolding A_def by auto
  {
    fix w :: "'a vec"
    assume w: "w  carrier_vec n"
    from len have n1[simp]: "n - Suc 0 = ?n" by auto
    {
      fix j
      assume j: "j < n"
      have "mat_delete (A w) ?n j = B j"
        unfolding mat_delete_def A_def mat_of_rows_def B_def
        by (rule eq_matI, insert j len, auto simp: nth_append)
    } note B = this
    have "det (A w) = (j<n. (A w) $$ (length ws, j) * cofactor (A w) ?n j)"
      by (subst laplace_expansion_row[OF A, of ?n], insert len, auto)
    also have " = (j<n. w $ j * (-1)^(?n+j) * det (mat_delete (A w) ?n j))"
      by (rule sum.cong, auto simp: A_def mat_of_rows_def cofactor_def)
    also have " = (j<n. w $ j * (-1)^(?n+j) * det (B j))"
      by (rule sum.cong[OF refl], subst B, auto)
    also have " = (j<n. w $ j * nv $ j)"
      by (rule sum.cong[OF refl], auto simp: nv_def)
    also have " = w  nv" unfolding scalar_prod_def unfolding nv_def
      by (rule sum.cong, auto)
    finally have "det (A w) = w  nv" .
  } note det_scalar = this
  have nv: "nv  carrier_vec n" unfolding nv_def by auto
  {
    fix w
    assume wW: "w  W"
    with W have w: "w  carrier_vec n" by auto
    from wW id obtain i where i: "i < ?n" and ws: "ws ! i = w" unfolding set_conv_nth by auto
    from det_scalar[OF w] have "det (A w) = w  nv" .
    also have "det (A w) = 0"
      by (subst det_identical_rows[OF A, of i ?n], insert i ws len, auto simp: A_def mat_of_rows_def nth_append)
    finally have "w  nv = 0" ..
    note this this[unfolded comm_scalar_prod[OF w nv]]
  } note ortho = this
  have nv0: "nv  0v n"
  proof
    assume nv: "nv = 0v n"
    define bs where "bs = basis_extension ws"
    define w where "w = hd bs"
    have "lin_indpt_list ws" using dist lin W unfolding lin_indpt_list_def id by auto
    from basis_extension[OF this, folded bs_def] len
    have lin: "lin_indpt_list (ws @ bs)" and "length bs = 1" and bsc: "set bs  carrier_vec n"
      by (auto simp: unit_vecs_def)
    hence bs: "bs = [w]" unfolding w_def by (cases bs, auto)
    with bsc have w: "w  carrier_vec n" by auto
    note lin = lin[unfolded bs]
    from lin_indpt_list_length_eq_n[OF lin] len
    have basis: "basis (set (ws @ [w]))" by auto
    from w det_scalar nv have det0: "det (A w) = 0" by auto
    with basis_det_nonzero[OF basis] len show False
      unfolding A_def by auto
  qed
  let ?nv = "normal_vector W"
  from ortho nv nv0
  show nv: "?nv  carrier_vec n"
    and ortho: " w. w  W  w  ?nv = 0"
    " w. w  W  ?nv  w = 0"
    and n0: "?nv  0v n" unfolding nv2 by auto
  from n0 nv have "sq_norm ?nv  0" by auto
  hence nvnv: "?nv  ?nv  0" by (auto simp: sq_norm_vec_as_cscalar_prod)
  show nvW: "?nv  W" using nvnv ortho by blast
  have "?nv  span W" using W ortho nvnv nv
    using orthocompl_span by blast
  with lin_dep_iff_in_span[OF W lin nv nvW]
  show "lin_indpt (insert ?nv W)" by auto
  {
    assume "W  v  Bounded_vec Bnd"
    hence wsI: "set ws  v  Bounded_vec Bnd" unfolding id by auto
    have ws: "set ws  carrier_vec n" using W unfolding id by auto
    from wsI ws have wsI: "i < ?n  ws ! i  v  Bounded_vec Bnd  carrier_vec n" for i
      using len wsI unfolding set_conv_nth by auto
    have ints: "i < ?n  j < n  ws ! i $ j  " for i j
      using wsI[of i, unfolded Ints_vec_def] by force
    have bnd: "i < ?n  j < n  abs (ws ! i $ j)  Bnd" for i j
      using wsI[unfolded Bounded_vec_def, of i] by auto
    {
      fix i
      assume i: "i < n"
      have ints: "nv $ i  " unfolding nv_def using wsI len ws
        by (auto simp: i B_def set_conv_nth intro!: Ints_mult Ints_det ints)
      have "¦nv $ i¦  det_bound (n - 1) Bnd" unfolding nv_def using wsI len ws i
        by (auto simp: B_def Bounded_mat_def abs_mult intro!: det_bound bnd)
      note ints this
    }
    with nv nv2 show "?nv  v  Bounded_vec (det_bound (n - 1) Bnd)"
      unfolding Ints_vec_def Bounded_vec_def by auto
  }
qed

lemma normal_vector_span:
  assumes card: "Suc (card D) = n"
    and D: "D  carrier_vec n" and fin: "finite D" and lin: "lin_indpt D"
  shows "span D = { x. x  carrier_vec n  x  normal_vector D = 0}"
proof -
  note nv = normal_vector[OF fin card lin D]
  {
    fix x
    assume xspan: "x  span D"
    from finite_in_span[OF fin D xspan] obtain c where
      "x  normal_vector D = lincomb c D  normal_vector D" by auto
    also have " = (wD. c w * (w  normal_vector D))"
      by (rule lincomb_scalar_prod_left, insert D nv, auto)
    also have " = 0"
      apply (rule sum.neutral) using nv(1,2,3) D comm_scalar_prod[of "normal_vector D"] by fastforce
    finally have "x  carrier_vec n"  "x  normal_vector D = 0" using xspan D by auto
  }
  moreover
  {
    let ?n = "normal_vector D"
    fix x
    assume x: "x  carrier_vec n" and xscal: "x  normal_vector D = 0"
    let ?B = "(insert (normal_vector D) D)"
    have "card ?B = n" using card card_insert_disjoint[OF fin nv(6)] by auto
    moreover have B: "?B  carrier_vec n" using D nv by auto
    ultimately have "span ?B = carrier_vec n"
      by (intro span_carrier_lin_indpt_card_n, insert nv(5), auto)
    hence xspan: "x  span ?B" using x by auto
    obtain c where "x = lincomb c ?B" using finite_in_span[OF _ B xspan] fin by auto
    hence "0 = lincomb c ?B  normal_vector D" using xscal by auto
    also have " = (w ?B. c w * (w  normal_vector D))"
      by (subst lincomb_scalar_prod_left, insert B, auto)
    also have " = (w D. c w * (w  normal_vector D)) + c ?n * (?n  ?n)"
      by (subst sum.insert[OF fin nv(6)], auto)
    also have "(w D. c w * (w  normal_vector D)) = 0"
      apply(rule sum.neutral) using nv(1,3) comm_scalar_prod[OF nv(1)] D by fastforce
    also have "?n  ?n = sq_norm ?n" using sq_norm_vec_as_cscalar_prod[of ?n] by simp
    finally have "c ?n * sq_norm ?n = 0" by simp
    hence ncoord: "c ?n = 0" using nv(1-5) by auto
    have "x = lincomb c ?B" by fact
    also have " = lincomb c D"
      apply (subst lincomb_insert2[OF fin D _ nv(6,1)]) using ncoord nv(1) D by auto
    finally have "x  span D" using fin by auto
  }
  ultimately show ?thesis by auto
qed

definition normal_vectors :: "'a vec list  'a vec list" where
  "normal_vectors ws = (let us = basis_extension ws
    in map (λ i. normal_vector (set (ws @ us) - {us ! i})) [0..<length us])"

lemma normal_vectors:
  assumes lin: "lin_indpt_list ws"
  shows "set (normal_vectors ws)  carrier_vec n"
    "w  set ws  nv  set (normal_vectors ws)  nv  w = 0"
    "w  set ws  nv  set (normal_vectors ws)  w  nv = 0"
    "lin_indpt_list (ws @ normal_vectors ws)"
    "length ws + length (normal_vectors ws) = n"
    "set ws  set (normal_vectors ws) = {}"
    "set ws  v  Bounded_vec Bnd 
       set (normal_vectors ws)  v  Bounded_vec (det_bound (n-1) (max 1 Bnd))"
proof -
  define us where "us = basis_extension ws"
  from basis_extension[OF assms, folded us_def]
  have units: "set us  set (unit_vecs n)"
    and lin: "lin_indpt_list (ws @ us)"
    and len: "length (ws @ us) = n"
    by auto
  from lin_indpt_list_length_eq_n[OF lin len]
  have span: "span (set (ws @ us)) = carrier_vec n" by auto
  from lin[unfolded lin_indpt_list_def]
  have wsus: "set (ws @ us)  carrier_vec n"
    and dist: "distinct (ws @ us)"
    and lin': "lin_indpt (set (ws @ us))" by auto
  let ?nv = "normal_vectors ws"
  note nv_def = normal_vectors_def[of ws, unfolded Let_def, folded us_def]
  let ?m = "length ws"
  let ?n = "length us"
  have lnv[simp]: "length ?nv = length us" unfolding nv_def by auto
  {
    fix i
    let ?V = "set (ws @ us) - {us ! i}"
    assume i: "i < ?n"
    hence nvi: "?nv ! i = normal_vector ?V" unfolding nv_def by auto
    from i have "us ! i  set us" by auto
    with wsus have u: "us ! i  carrier_vec n" by auto
    have id: "?V  {us ! i} = set (ws @ us)" using i by auto
    have V: "?V  carrier_vec n" using wsus by auto
    have finV: "finite ?V" by auto
    have "Suc (card ?V) = card (insert (us ! i) ?V)"
      by (subst card_insert_disjoint[OF finV], auto)
    also have "insert (us ! i) ?V = set (ws @ us)" using i by auto
    finally have cardV: "Suc (card ?V) = n"
      using len distinct_card[OF dist] by auto
    from subset_li_is_li[OF lin'] have linV: "lin_indpt ?V" by auto
    from lin_dep_iff_in_span[OF _ linV u, unfolded id] wsus lin'
    have usV: "us ! i  span ?V" by auto
    note nv = normal_vector[OF finV cardV linV V, folded nvi]
    from normal_vector_span[OF cardV V _ linV, folded nvi] comm_scalar_prod[OF _ nv(1)]
    have span: "span ?V = {x  carrier_vec n. ?nv ! i  x = 0}"
      by auto
    from nv(1,2) have "sq_norm (?nv ! i)  0" by auto
    hence nvi: "?nv ! i  ?nv ! i  0"
      by (auto simp: sq_norm_vec_as_cscalar_prod)
    from span nvi have nvspan: "?nv ! i  span ?V" by auto
    from u usV[unfolded span] have "?nv ! i  us ! i  0" by blast
    note nv nvi this span usV nvspan
  } note nvi = this
  show nv: "set ?nv  carrier_vec n"
    unfolding set_conv_nth using nvi(1) by auto
  {
    fix w nv
    assume w: "w  set ws"
    with dist have wus: "w  set us" by auto
    assume n: "nv  set ?nv"
    with w wus show "nv  w = 0"
      unfolding set_conv_nth[of "normal_vectors _"] by (auto intro!: nvi(4)[of _ w])
    thus "w  nv = 0" using comm_scalar_prod[of w n nv] w nv n wsus by auto
  } note scalar_0 = this
  show "length ws + length ?nv = n" using len by simp
  {
    assume wsI: "set ws  v  Bounded_vec Bnd"
    {
      fix nv
      assume "nv  set ?nv"
      then obtain i where nv: "nv = ?nv ! i" and i: "i < ?n" unfolding set_conv_nth by auto
      from wsI have "set (ws @ us) - {us ! i}  v  Bounded_vec (max 1 Bnd)" using units
          Bounded_vec_mono[of Bnd "max 1 Bnd"]
        by (auto simp: unit_vecs_def)
      from nvi(7)[OF i this] nv
      have "nv  v  Bounded_vec (det_bound (n - 1) (max 1 Bnd))"
        by auto
    }
    thus "set ?nv  v  Bounded_vec (det_bound (n - 1) (max 1 Bnd))" by auto
  }
  have dist_nv: "distinct ?nv" unfolding distinct_conv_nth lnv
  proof (intro allI impI)
    fix i j
    assume i: "i < ?n" and j: "j < ?n" and ij: "i  j"
    with dist have usj: "us ! j  set (ws @ us) - {us ! i}"
      by (simp, auto simp: distinct_conv_nth set_conv_nth)
    from nvi(4)[OF i this] nvi(9)[OF j]
    show "?nv ! i  ?nv ! j" by auto
  qed
  show disj: "set ws  set ?nv = {}"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain w where w: "w  set ws" "w  set ?nv" by auto
    from scalar_0[OF this] this(1) have "sq_norm w = 0"
      by (auto simp: sq_norm_vec_as_cscalar_prod)
    with w wsus have "w = 0v n" by auto
    with vs_zero_lin_dep[OF wsus lin'] w(1) show False by auto
  qed
  have dist': "distinct (ws @ ?nv)" using dist disj dist_nv by auto
  show "lin_indpt_list (ws @ ?nv)" unfolding lin_indpt_list_def
  proof (intro conjI dist')
    show set: "set (ws @ ?nv)  carrier_vec n" using nv wsus by auto
    hence ws: "set ws  carrier_vec n" by auto
    have lin_nv: "lin_indpt (set ?nv)"
    proof
      assume "lin_dep (set ?nv)"
      from finite_lin_dep[OF finite_set this nv]
      obtain a v where comb: "lincomb a (set ?nv) = 0v n" and vnv: "v  set ?nv" and av0: "a v  0" by auto
      from vnv[unfolded set_conv_nth] obtain i where i: "i < ?n" and vi: "v = ?nv ! i" by auto
      define b where "b = (λ w. a w / a v)"
      define c where "c = (λ w. -1 * b w)"
      define x where "x = lincomb b (set ?nv - {v})"
      define w where "w = lincomb c (set ?nv - {v})"
      have w: "w  carrier_vec n" unfolding w_def using nv by auto
      have x: "x  carrier_vec n" unfolding x_def using nv by auto
      from arg_cong[OF comb, of "λ x. (1/ a v) v x"]
      have "0v n = 1 / a v v lincomb a (set ?nv)" by auto
      also have " = lincomb b (set ?nv)"
        by (subst lincomb_smult[symmetric, OF nv], auto simp: b_def)
      also have " = b v v v + lincomb b (set ?nv - {v})"
        by (subst lincomb_del2[OF _ nv _ vnv], auto)
      also have "b v v v = v" using av0 unfolding b_def by auto
      finally have "v + lincomb b (set ?nv - {v}) - lincomb b (set ?nv - {v}) =
         0v n - lincomb b (set ?nv - {v})" (is "?l = ?r") by simp
      also have "?l = v"
        by (rule add_diff_cancel_right_vec, insert vnv nv, auto)
      also have "?r = w" unfolding w_def c_def
        by (subst lincomb_smult, unfold x_def[symmetric], insert nv x, auto)
      finally have vw: "v = w" .
      have u: "us ! i  carrier_vec n" using i wsus by auto
      have nv': "set ?nv - {?nv ! i}  carrier_vec n" using nv by auto
      have "?nv ! i  us ! i = 0"
        unfolding vi[symmetric] vw unfolding w_def vi
        unfolding lincomb_scalar_prod_left[OF nv' u]
      proof (rule sum.neutral, intro ballI)
        fix x
        assume "x  set ?nv - {?nv ! i}"
        then obtain j where j: "j < ?n" and x: "x = ?nv ! j" and ij: "i  j" unfolding set_conv_nth by auto
        from dist[simplified] ij i j have "us ! i  us ! j" unfolding distinct_conv_nth by auto
        with i have "us ! i  set (ws @ us) - {us ! j}" by auto
        from nvi(3-4)[OF j this]
        show "c x * (x  us ! i) = 0" unfolding x by auto
      qed
      with nvi(9)[OF i] show False ..
    qed
    from subset_li_is_li[OF lin'] have "lin_indpt (set ws)" by auto
    from ortho_lin_indpt[OF nv ws scalar_0 lin_nv this]
    have "lin_indpt (set ?nv  set ws)" .
    also have "set ?nv  set ws = set (ws @ ?nv)" by auto
    finally show "lin_indpt (set (ws @ ?nv))" .
  qed
qed

definition pos_norm_vec :: "'a vec set  'a vec  'a vec" where
  "pos_norm_vec D x = (let c' = normal_vector D;
     c = (if c'  x > 0 then c' else -c') in c)"

lemma pos_norm_vec:
  assumes D: "D  carrier_vec n" and fin: "finite D" and lin: "lin_indpt D"
    and card: "Suc (card D) = n"
    and c_def: "c = pos_norm_vec D x"
  shows "c  carrier_vec n" "span D = { x. x  carrier_vec n  x  c = 0}"
    "x  span D  x  carrier_vec n  c  x > 0"
    "c  {normal_vector D, -normal_vector D}"
proof -
  have n: "normal_vector D  carrier_vec n" using normal_vector assms by auto
  show cnorm: "c  {normal_vector D, -normal_vector D}" unfolding c_def pos_norm_vec_def Let_def by auto
  then show c: "c  carrier_vec n" using assms normal_vector by auto
  have "span D = { x. x  carrier_vec n  x  normal_vector D = 0}"
    using normal_vector_span[OF card D fin lin] by auto
  also have " = { x. x  carrier_vec n  x  c = 0}" using cnorm c by auto
  finally show span_char: "span D = { x. x  carrier_vec n  x  c = 0}" by auto
  {
    assume x: "x  span D" "x  carrier_vec n"
    hence "c  x  0" using comm_scalar_prod[OF c] unfolding span_char by auto
    hence "normal_vector D  x  0" using cnorm n x by auto
    with x have b: "¬ (normal_vector D  x > 0)  (-normal_vector D)  x > 0"
      using assms n by auto
    then show "c  x > 0"  unfolding c_def pos_norm_vec_def Let_def
      by (auto split: if_splits)
  }
qed

end

end

Theory Dim_Span

section ‹Dimension of Spans›

text ‹We define the notion of dimension of a span of vectors and prove some natural results about them.
  The definition is made as a function, so that no interpretation of locales like subspace is required.›
theory Dim_Span
  imports Missing_VS_Connect
begin

context vec_space
begin
definition "dim_span W = Max (card ` {V. V  carrier_vec n  V  span W  lin_indpt V})"

lemma fixes V W :: "'a vec set"
  shows
    card_le_dim_span:
    "V  carrier_vec n  V  span W  lin_indpt V  card V  dim_span W" and
    card_eq_dim_span_imp_same_span:
    "W  carrier_vec n  V  span W  lin_indpt V  card V = dim_span W  span V = span W" and
    same_span_imp_card_eq_dim_span:
    "V  carrier_vec n  W  carrier_vec n  span V = span W  lin_indpt V  card V = dim_span W" and
    dim_span_cong:
    "span V = span W  dim_span V = dim_span W" and
    ex_basis_span:
    "V  carrier_vec n   W. W  carrier_vec n  lin_indpt W  span V = span W  dim_span V = card W"
proof -
  show cong: " V W. span V = span W  dim_span V = dim_span W" unfolding dim_span_def by auto
  {
    fix W :: "'a vec set"
    let ?M = "{V. V  carrier_vec n  V  span W  lin_indpt V}"
    have "card ` ?M  {0 .. n}"
    proof
      fix k
      assume "k  card ` ?M"
      then obtain V where V: "V  carrier_vec n  V  span W  lin_indpt V"
        and k: "k = card V"
        by auto
      from V have "card V  n" using dim_is_n li_le_dim by auto
      with k show "k  {0 .. n}" by auto
    qed
    from finite_subset[OF this]
    have fin: "finite (card ` ?M)" by auto
    have "{}  ?M" by (auto simp: span_empty span_zero)
    from imageI[OF this, of card]
    have "0  card ` ?M" by auto
    hence Mempty: "card ` ?M  {}" by auto
    from Max_ge[OF fin, folded dim_span_def]
    show " V :: 'a vec set. V  carrier_vec n  V  span W  lin_indpt V  card V  dim_span W"
      by auto
    note this fin Mempty
  } note part1 = this
  {
    fix V W :: "'a vec set"
    assume  W: "W  carrier_vec n"
      and VsW: "V  span W" and linV: "lin_indpt V" and card: "card V = dim_span W"
    from W VsW have V: "V  carrier_vec n" using span_mem[OF W] by auto
    from Max_in[OF part1(2,3), folded dim_span_def, of W]
    obtain WW where WW: "WW  carrier_vec n" "WW  span W" "lin_indpt WW"
      and id: "dim_span W = card WW" by auto
    show "span V = span W"
    proof (rule ccontr)
      from VsW V W have sub: "span V  span W" using span_subsetI by metis
      assume "span V  span W"
      with sub obtain w where wW: "w  span W" and wsV: "w  span V" by auto
      from wW W have w: "w  carrier_vec n" by auto
      from linV V have finV: "finite V" using fin_dim fin_dim_li_fin by blast
      from wsV span_mem[OF V, of w] have wV: "w  V" by auto
      let ?X = "insert w V"
      have "card ?X = Suc (card V)" using wV finV by simp
      hence gt: "card ?X > dim_span W" unfolding card by simp
      have linX: "lin_indpt ?X" using lin_dep_iff_in_span[OF V linV w wV] wsV by auto
      have XW: "?X  span W" using wW VsW by auto
      from part1(1)[OF _ XW linX] w V have "card ?X  dim_span W" by auto
      with gt show False by auto
    qed
  } note card_dim_span = this
  {
    fix V :: "'a vec set"
    assume V: "V  carrier_vec n"
    from Max_in[OF part1(2,3), folded dim_span_def, of V]
    obtain W where W: "W  carrier_vec n" "W  span V" "lin_indpt W"
      and idW: "card W = dim_span V" by auto
    show " W. W  carrier_vec n  lin_indpt W  span V = span W  dim_span V = card W"
    proof (intro exI[of _ W] conjI W idW[symmetric])
      from card_dim_span[OF V(1) W(2-3) idW] show "span V = span W"  by auto
    qed
  }
  {
    fix V W
    assume V: "V  carrier_vec n"
      and W: "W  carrier_vec n"
      and span: "span V = span W"
      and lin: "lin_indpt V"
    from Max_in[OF part1(2,3), folded dim_span_def, of W]
    obtain WW where WW: "WW  carrier_vec n" "WW  span W" "lin_indpt WW"
      and idWW: "card WW = dim_span W" by auto
    from card_dim_span[OF W WW(2-3) idWW] span
    have spanWW: "span WW = span V" by auto
    from span have "V  span W" using span_mem[OF V] by auto
    from part1(1)[OF V this lin] have VW: "card V  dim_span W" .
    have finWW: "finite WW" using WW by (simp add: fin_dim_li_fin)
    have finV: "finite V" using lin V by (simp add: fin_dim_li_fin)
    from replacement[OF finWW finV V WW(3) WW(2)[folded span], unfolded idWW]
    obtain C :: "'a vec set"
      where le: "int (card C)  int (card V) - int (dim_span W)" by auto
    from le have "int (dim_span W) + int (card C)  int (card V)" by linarith
    hence "dim_span W + card C  card V" by linarith
    with VW show "card V = dim_span W" by auto
  }
qed

lemma dim_span_le_n: assumes W: "W  carrier_vec n" shows "dim_span W  n"
proof -
  from ex_basis_span[OF W] obtain V where
    V: "V  carrier_vec n"
    and lin: "lin_indpt V"
    and dim: "dim_span W = card V"
    by auto
  show ?thesis unfolding dim using lin V
    using dim_is_n li_le_dim by auto
qed

lemma dim_span_insert: assumes W: "W  carrier_vec n"
  and v: "v  carrier_vec n" and vs: "v  span W"
shows "dim_span (insert v W) = Suc (dim_span W)"
proof -
  from ex_basis_span[OF W] obtain V where
    V: "V  carrier_vec n"
    and lin: "lin_indpt V"
    and span: "span W = span V"
    and dim: "dim_span W = card V"
    by auto
  from V vs[unfolded span] have vV: "v  V" using span_mem[OF V] by blast
  from lin_dep_iff_in_span[OF V lin v vV] vs span
  have lin': "lin_indpt (insert v V)" by auto
  have finV: "finite V" using lin V using fin_dim fin_dim_li_fin by blast
  have "card (insert v V) = Suc (card V)" using finV vV by auto
  hence cvV: "card (insert v V) = Suc (dim_span W)" using dim by auto
  have "span (insert v V) = span (insert v W)"
    using span V W v by (metis bot_least insert_subset insert_union span_union_is_sum)
  from same_span_imp_card_eq_dim_span[OF _ _ this lin'] cvV v V W
  show ?thesis by auto
qed
end
end

Theory Fundamental_Theorem_Linear_Inequalities

section ‹The Fundamental Theorem of Linear Inequalities›

text ‹The theorem states that for a given set of vectors A and vector b, either
  b is in the cone of a linear independent subset of A, or
  there is a hyperplane that contains span(A,b)-1 linearly independent vectors of A
  that separates A from b. We prove this theorem and derive some consequences, e.g.,
  Caratheodory's theorem that b is the cone of A iff b is in the cone of a linear
  independent subset of A.›

theory Fundamental_Theorem_Linear_Inequalities
  imports
    Cone
    Normal_Vector
    Dim_Span
begin

context gram_schmidt
begin

text ‹The mentions equivances A-D are:
  A: b is in the cone of vectors A,
  B: b is in the cone of a subset of linear independent of vectors A,
  C: there is no separating hyperplane of b and the vectors A,
      which contains dim many linear independent vectors of A
  D: there is no separating hyperplane of b and the vectors A›

lemma fundamental_theorem_of_linear_inequalities_A_imp_D:
  assumes A: "A  carrier_vec n"
    and fin: "finite A"
    and b: "b  cone A"
  shows " c. c  carrier_vec n  ( ai  A. c  ai  0)  c  b < 0"
proof
  assume " c. c  carrier_vec n  ( ai  A. c  ai  0)  c  b < 0"
  then obtain c where c: "c  carrier_vec n"
    and ai: " ai. ai  A  c  ai  0"
    and cb: "c  b < 0" by auto
  from b[unfolded cone_def nonneg_lincomb_def finite_cone_def]
  obtain l AA where bc: "b = lincomb l AA" and l: "l ` AA  {x. x  0}" and AA: "AA  A" by auto
  from cone_carrier[OF A] b have b: "b  carrier_vec n" by auto
  have "0  (aiAA. l ai * (c  ai))"
    by (intro sum_nonneg mult_nonneg_nonneg, insert l ai AA, auto)
  also have " = (aiAA. l ai * (ai  c))"
    by (rule sum.cong, insert c A AA comm_scalar_prod, force+)
  also have " = (aiAA. ((l ai v ai)  c))"
    by (rule sum.cong, insert smult_scalar_prod_distrib c A AA, auto)
  also have " = b  c" unfolding bc lincomb_def
    by (subst finsum_scalar_prod_sum[symmetric], insert c A AA, auto)
  also have " = c  b" using comm_scalar_prod b c by auto
  also have " < 0" by fact
  finally show False by simp
qed

text ‹The difficult direction is that C implies B. To this end we follow the
  proof that at least one of B and the negation of C is satisfied.›
context
  fixes a :: "nat  'a vec"
    and b :: "'a vec"
    and m :: nat
  assumes a: "a ` {0 ..< m}  carrier_vec n"
    and inj_a: "inj_on a {0 ..< m}"
    and b: "b  carrier_vec n"
    and full_span: "span (a ` {0 ..< m}) = carrier_vec n"
begin

private definition "goal = (( I. I  {0 ..< m}  card (a ` I) = n  lin_indpt (a ` I)  b  finite_cone (a ` I))
   ( c I. I  {0 ..< m}  c  {normal_vector (a ` I), - normal_vector (a ` I)}  Suc (card (a ` I)) = n
       lin_indpt (a ` I)  ( i < m. c  a i  0)  c  b < 0))"

private lemma card_a_I[simp]: "I  {0 ..< m}  card (a ` I) = card I"
  by (smt inj_a card_image inj_on_image_eq_iff subset_image_inj subset_refl subset_trans)

private lemma in_a_I[simp]: "I  {0 ..< m}  i < m  (a i  a ` I) = (i  I)"
  using inj_a
  by (meson atLeastLessThan_iff image_eqI inj_on_image_mem_iff zero_le)

private definition "valid_I = { I. card I = n  lin_indpt (a ` I)  I  {0 ..< m}}"

private definition cond where "cond I I' l c h k 
  b = lincomb l (a ` I) 
  h  I  l (a h) < 0  ( h'. h'  I  h' < h  l (a h')  0) 
  c  carrier_vec n  span (a ` (I - {h})) = { x. x  carrier_vec n  c  x = 0}  c  b < 0 
  k < m  c  a k < 0  ( k'. k' < k  c  a k'  0) 
  I' = insert k (I - {h})"

private definition "step_rel = Restr { (I'', I).  l c h k. cond I I'' l c h k } valid_I"

private lemma finite_step_rel: "finite step_rel"
proof (rule finite_subset)
  show "step_rel  (Pow {0 ..< m} × Pow {0 ..< m})" unfolding step_rel_def valid_I_def by auto
qed auto

private lemma acyclic_imp_goal: "acyclic step_rel  goal"
proof (rule ccontr)
  assume ngoal: "¬ goal" (* then the algorithm will not terminate *)
  {
    fix I
    assume I: "I  valid_I"
    hence Im: "I  {0..<m}" and
      lin: "lin_indpt (a ` I)" and
      cardI: "card I = n"
      by (auto simp: valid_I_def)
    let ?D = "(a ` I)"
    have finD: "finite ?D" using Im infinite_super by blast
    have carrD: "?D  carrier_vec n" using a Im by auto
    have cardD: "card ?D = n" using cardI Im by simp
    have spanD: "span ?D = carrier_vec n"
      by (intro span_carrier_lin_indpt_card_n lin cardD carrD)
    obtain lamb where b_is_lincomb: "b = lincomb lamb (a ` I)"
      using finite_in_span[OF fin carrD, of b] using spanD b carrD fin_dim lin by auto
    define h where "h = (LEAST h. h  I  lamb (a h) < 0)"
    have " I'. (I', I)  step_rel"
    proof (cases "i I . lamb (a i)  0")
      case cond1_T: True
      have goal unfolding goal_def
        by (intro disjI1 exI[of _ I] conjI lin cardI
            lincomb_in_finite_cone[OF b_is_lincomb finD _ carrD], insert cardI Im cond1_T, auto)
      with ngoal show ?thesis by auto
    next
      case cond1_F: False
      hence " h. h  I  lamb (a h) < 0" by fastforce
      from LeastI_ex[OF this, folded h_def] have h: "h  I" "lamb (a h) < 0" by auto
      from not_less_Least[of _ "λ h. h  I  lamb (a h) < 0", folded h_def]
      have h_least: " k. k  I  k < h  lamb (a k)  0" by fastforce
      obtain I' where I'_def: "I' = I - {h}" by auto
      obtain c where c_def: "c = pos_norm_vec (a ` I') (a h)" by auto
      let ?D' = "a ` I'"
      have I'm: "I'  {0..<m}" using Im I'_def by auto
      have carrD': " ?D'  carrier_vec n" using a Im I'_def by auto
      have finD': "finite (?D')" using Im I'_def subset_eq_atLeast0_lessThan_finite by auto
      have D'subs: "?D'  ?D" using I'_def by auto
      have linD': "lin_indpt (?D')" using lin I'_def Im D'subs subset_li_is_li by auto
      have D'strictsubs: "?D = ?D'  {a h}" using h I'_def by auto
      have h_nin_I: "h  I'" using h I'_def by auto
      have ah_nin_D': "a h  ?D'" using h inj_a Im h_nin_I by (subst in_a_I, auto simp: I'_def)
      have cardD': "Suc (card (?D')) = n " using cardD ah_nin_D' D'strictsubs finD' by simp
      have ah_carr: "a h  carrier_vec n" using h a Im by auto
      note pnv = pos_norm_vec[OF carrD' finD' linD' cardD' c_def]
      have ah_nin_span: "a h  span ?D'"
        using D'strictsubs lin_dep_iff_in_span[OF carrD' linD' ah_carr ah_nin_D'] lin by auto
      have cah_ge_zero:"c  a h > 0" and "c  carrier_vec n"
        and cnorm: "span ?D' = {x  carrier_vec n. x  c = 0}"
        using ah_carr ah_nin_span pnv by auto
      have ccarr: "c  carrier_vec n" by fact
      have "b  c = lincomb lamb (a ` I)  c" using b_is_lincomb by auto
      also have " = (w ?D. lamb w * (w  c))"
        using lincomb_scalar_prod_left[OF carrD, of c lamb] pos_norm_vec ccarr by blast
      also have " = lamb (a h) * (a h  c) + (w ?D'. lamb w * (w  c))"
        using sum.insert[OF finD' ah_nin_D', of lamb] D'strictsubs ah_nin_D' finD' by auto
      also have "(w ?D'. lamb w * (w  c)) = 0"
        apply (rule sum.neutral)
        using span_mem[OF carrD', unfolded cnorm] by simp
      also have "lamb (a h) * (a h  c) + 0 < 0"
        using cah_ge_zero h(2) comm_scalar_prod[OF ah_carr ccarr]
        by (auto intro: mult_neg_pos)
      finally have cb_le_zero: "c  b < 0" using comm_scalar_prod[OF b ccarr] by auto

      show ?thesis
      proof (cases "i < m . c  a i  0")
        case cond2_T: True
        have goal
          unfolding goal_def
          by (intro disjI2 exI[of _ c] exI[of _ I'] conjI cb_le_zero linD' cond2_T cardD' I'm pnv(4))
        with ngoal show ?thesis by auto
      next
        case cond2_F: False
        define k where "k = (LEAST k. k < m  c  a k < 0)"
        let ?I'' = "insert k I'"
        show ?thesis unfolding step_rel_def
        proof (intro exI[of _ ?I''], standard, unfold mem_Collect_eq split, intro exI)
          from LeastI_ex[OF ]
          have "k. k < m  c  a k < 0" using cond2_F by fastforce
          from LeastI_ex[OF this, folded k_def] have k: "k < m" "c  a k < 0" by auto
          show "cond I ?I'' lamb c h k" unfolding cond_def I'_def[symmetric] cnorm
          proof(intro conjI cb_le_zero b_is_lincomb h ccarr h_least refl k)
            show "{x  carrier_vec n. x  c = 0} = {x  carrier_vec n. c  x = 0}"
              using comm_scalar_prod[OF ccarr] by auto
            from not_less_Least[of _ "λ k. k < m  c  a k < 0", folded k_def]
            have "k' < k . k' > m  c  a k'  0" using k(1) less_trans not_less by blast
            then show "k' < k . c  a k'  0" using k(1) by auto
          qed

          have "?I''  valid_I" unfolding valid_I_def
          proof(standard, intro conjI)
            from k a have ak_carr: "a k  carrier_vec n" by auto
            have ak_nin_span: "a k  span ?D'" using k(2) cnorm comm_scalar_prod[OF ak_carr ccarr] by auto
            hence ak_nin_D': "a k  ?D'" using span_mem[OF carrD'] by auto
            from lin_dep_iff_in_span[OF carrD' linD' ak_carr ak_nin_D']
            show "lin_indpt (a ` ?I'')" using ak_nin_span by auto
            show "?I''  {0..<m}" using I'm k by auto
            show "card (insert k I') = n" using cardD' ak_nin_D' finD'
              by (metis ‹insert k I'  {0..<m} card_a_I card_insert_disjoint image_insert)
          qed
          then show "(?I'', I)  valid_I × valid_I"  using I by auto

        qed
      qed
    qed
  } note step = this
  { (* create some valid initial set I *)
    from exists_lin_indpt_subset[OF a, unfolded full_span]
    obtain A where lin: "lin_indpt A" and span: "span A = carrier_vec n" and Am: "A  a ` {0 ..<m}" by auto
    from Am a have A: "A  carrier_vec n" by auto
    from lin span A have card: "card A = n"
      using basis_def dim_basis dim_is_n fin_dim_li_fin by auto
    from A Am obtain I where  A: "A = a ` I" and I: "I  {0 ..< m}" by (metis subset_imageE)
    have "I  valid_I" using I card lin unfolding valid_I_def A by auto
    hence " I. I  valid_I" ..
  }
  note init = this
  have step_valid: "(I',I)  step_rel  I'  valid_I" for I I' unfolding step_rel_def by auto
  have "¬ (wf step_rel)"
  proof
    from init obtain I where I: "I  valid_I" by auto
    assume "wf step_rel"
    from this[unfolded wf_eq_minimal, rule_format, OF I] step step_valid show False by blast
  qed
  with wf_iff_acyclic_if_finite[OF finite_step_rel]
  have "¬ acyclic step_rel" by auto
  thus "acyclic step_rel  False" by auto
qed

private lemma acyclic_step_rel: "acyclic step_rel"
proof (rule ccontr)
  assume "¬ ?thesis"
  hence "¬ acyclic (step_rel¯)" by auto

(* obtain cycle *)
  then obtain I where "(I, I)  (step_rel^-1)^+" unfolding acyclic_def by blast
  from this[unfolded trancl_power]
  obtain len where "(I, I)  (step_rel^-1) ^^ len" and len0: "len > 0" by blast
      (* obtain all intermediate I's *)
  from this[unfolded relpow_fun_conv] obtain Is where
    stepsIs: " i. i < len  (Is (Suc i), Is i)  step_rel"
    and IsI: "Is 0 = I" "Is len = I" by auto
  {
    fix i
    assume "i  len" hence "i - 1 < len" using len0 by auto
    from stepsIs[unfolded step_rel_def, OF this]
    have "Is i  valid_I" by (cases i, auto)
  } note Is_valid = this
  from stepsIs[unfolded step_rel_def]
  have " i.  l c h k. i < len  cond (Is i) (Is (Suc i)) l c h k" by auto
      (* obtain all intermediate c's h's, l's, k's *)
  from choice[OF this] obtain ls where " i.  c h k. i < len  cond (Is i) (Is (Suc i)) (ls i) c h k" by auto
  from choice[OF this] obtain cs where " i.  h k. i < len  cond (Is i) (Is (Suc i)) (ls i) (cs i) h k" by auto
  from choice[OF this] obtain hs where " i.  k. i < len  cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) k" by auto
  from choice[OF this] obtain ks where
    cond: " i. i < len  cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) (ks i)" by auto
      (* finally derive contradiction *)
  let ?R = "{hs i | i. i < len}"
  define r where "r = Max ?R"
  from cond[OF len0] have "hs 0  I" using IsI unfolding cond_def by auto
  hence R0: "hs 0  ?R" using len0 by auto
  have finR: "finite ?R" by auto
  from Max_in[OF finR] R0
  have rR: "r  ?R" unfolding r_def[symmetric] by auto
  then obtain p where rp: "r = hs p" and p: "p < len" by auto
  from Max_ge[OF finR, folded r_def]
  have rLarge: "i < len  hs i  r" for i by auto
  have exq: "q. ks q = r  q < len"
  proof (rule ccontr)
    assume neg: "¬?thesis"
    show False
    proof(cases "r  I")
      case True
      have 1: "j{Suc p..len}  r  Is j" for j
      proof(induction j rule: less_induct)
        case (less j)
        from less(2) have j_bounds: "j = Suc p  j > Suc p" by auto
        from less(2) have j_len: "j  len" by auto
        have pj_cond: "j = Suc p  cond (Is p) (Is j) (ls p) (cs p) (hs p) (ks p)" using cond p by blast
        have r_neq_ksp: "r  ks p" using p neg by auto
        have "j = Suc p  Is j = insert (ks p) (Is p - {r})"
          using rp cond pj_cond cond_def[of "Is p" "Is j" _ _ r] by blast
        hence c1: "j = Suc p  r  Is j" using r_neq_ksp by simp
        have IH: "t. t < j  t  {Suc p..len}  r  Is t" by fact
        have r_neq_kspj: "j > Suc p  j  len  r  ks (j-1)" using j_len neg IH by auto
        have jsucj_cond: "j > Suc p  j  len  Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})"
          using cond_def[of "Is (j-1)" "Is j"] cond
          by (metis (no_types, lifting) Suc_less_eq2 diff_Suc_1 le_simps(3))
        hence "j > Suc p  j  len  r  insert (ks (j-1))