# 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)

"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

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)

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
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 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
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

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)"
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
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"
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
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
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))