# 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 ⟹ 0⇩m nr nc *⇩v x = 0⇩v 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 = (A⇧T @⇩r B⇧T)⇧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 (A⇧T) = 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 (0⇩v n) m = 0⇩v 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]: "set⇩v 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))⇧T⇧T"
by auto
also have "((A @⇩c B) * mat_of_col (v1 @⇩v v2))⇧T =
(mat_of_row (v1 @⇩v v2))⇧T⇧T * (A⇧T @⇩r B⇧T)⇧T⇧T"
unfolding append_cols_def mat_of_col_def
proof (rule transpose_mult, force, unfold transpose_carrier_mat, rule mat_of_row_carrier)
have "A⇧T ∈ carrier_mat nc1 nr" using A by auto
moreover have "B⇧T ∈ carrier_mat nc2 nr" using B by auto
ultimately have "A⇧T @⇩r B⇧T ∈ carrier_mat (nc1 + nc2) nr" by auto
hence "dim_row (A⇧T @⇩r B⇧T) = nc1 + nc2" by auto
thus "v1 @⇩v v2 ∈ carrier_vec (dim_row (A⇧T @⇩r B⇧T))" using v1 v2 by auto
qed
also have "… = (mat_of_row (v1 @⇩v v2)) * (A⇧T @⇩r B⇧T)" by auto
also have "… = mat_of_row v1 * A⇧T + mat_of_row v2 * B⇧T"
using mat_of_row_mult_append_rows[OF v1 v2] A B by auto
also have "…⇧T = (mat_of_row v1 * A⇧T)⇧T + (mat_of_row v2 * B⇧T)⇧T"
using transpose_add A B by auto
also have "(mat_of_row v1 * A⇧T)⇧T = A⇧T⇧T * ((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 * B⇧T)⇧T = B⇧T⇧T * ((mat_of_row v2)⇧T)"
using transpose_mult B v2 transpose_carrier_mat mat_of_row_carrier(1)
by metis
also have "A⇧T⇧T * ((mat_of_row v1)⇧T) + B⇧T⇧T * ((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 ≤ 0⇩v (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 A⇧T n)⇧T"

definition "mat_col_last A n ≡ (mat_row_last A⇧T 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 "A⇧T"] 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 ≤ 0⇩v n) = (v ≤ 0⇩v 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 ≤ 0⇩v n" shows "l ⋅⇩v v ≤ 0⇩v 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 "∃x1∈carrier_vec n. ∃x2∈carrier_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),
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 = (∑w∈W. 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 = (∑w∈W. 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 = 0⇩v 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 "… = {0⇩v 0}" by auto
finally have "X ⊆ {0⇩v 0}" .
from finite_subset[OF this] show "finite X" by auto
qed
from X have "span X ⊆ carrier_vec n" by auto
with span have span: "span X = carrier_vec n" by auto
from dim_is_n card have card: "card X ≤ dim" by auto
from dim_gen_is_basis[OF fin X span card] show "basis X" .
qed

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

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

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

lemma lincomb_list_index:
assumes i: "i < n"
shows "set Xs ⊆ carrier_vec n ⟹
lincomb_list c Xs $i = sum (λ j. c j * (Xs ! j)$ i) {0..<length Xs}"
proof (induction Xs rule: rev_induct)
case (snoc x Xs)
hence x: "x ∈ carrier_vec n" and Xs: "set Xs ⊆ carrier_vec n" by auto
hence "lincomb_list c (Xs @ [x]) = lincomb_list c Xs + c (length Xs) ⋅⇩v x" by auto
also have "… $i = lincomb_list c Xs$ i + (c (length Xs) ⋅⇩v x) $i" using i index_add_vec(1) x by simp also have "(c (length Xs) ⋅⇩v x)$ i = c (length Xs) * x $i" using i x by simp also have "x$ i= (Xs @ [x]) ! (length Xs) $i" by simp also have "lincomb_list c Xs$ i = (∑j = 0..<length Xs. c j * Xs ! j $i)" by (rule snoc.IH[OF Xs]) also have "… = (∑j = 0..<length Xs. c j * (Xs @ [x]) ! j$ i)"
by (rule R.finsum_restrict, force, rule restrict_ext, auto simp: append_Cons_nth_left)
finally show ?case
using sum.atLeast0_lessThan_Suc[of "λ j. c j * (Xs @ [x]) ! j $i" "length Xs"] by fastforce qed (simp add: i) end end # Theory Basis_Extension section ‹Basis Extension› text ‹We prove that every linear indepent set/list of vectors can be extended into a basis. Similarly, from every set of vectors one can extract a linear independent set of vectors that spans the same space.› theory Basis_Extension imports LLL_Basis_Reduction.Gram_Schmidt_2 begin context cof_vec_space begin lemma lin_indpt_list_length_le_n: assumes "lin_indpt_list xs" shows "length xs ≤ n" proof - from assms[unfolded lin_indpt_list_def] have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto from dist have "card (set xs) = length xs" by (rule distinct_card) moreover have "card (set xs) ≤ n" using lin xs dim_is_n li_le_dim(2) by auto ultimately show ?thesis by auto qed lemma lin_indpt_list_length_eq_n: assumes "lin_indpt_list xs" and "length xs = n" shows "span (set xs) = carrier_vec n" "basis (set xs)" proof - from assms[unfolded lin_indpt_list_def] have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto from dist have "card (set xs) = length xs" by (rule distinct_card) with assms have "card (set xs) = n" by auto with lin xs show "span (set xs) = carrier_vec n" "basis (set xs)" using dim_is_n by (metis basis_def dim_basis dim_li_is_basis fin_dim finite_basis_exists gen_ge_dim li_le_dim(1))+ qed lemma expand_to_basis: assumes lin: "lin_indpt_list xs" shows "∃ ys. set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n" proof - define y where "y = n - length xs" from lin have "length xs ≤ n" by (rule lin_indpt_list_length_le_n) hence "length xs + y = n" unfolding y_def by auto thus "∃ ys. set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n" using lin proof (induct y arbitrary: xs) case (0 xs) thus ?case by (intro exI[of _ Nil], auto) next case (Suc y xs) hence "length xs < n" by auto from Suc(3)[unfolded lin_indpt_list_def] have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto from distinct_card[OF dist] Suc(2) have card: "card (set xs) < n" by auto have "span (set xs) ≠ carrier_vec n" using card dim_is_n xs basis_def dim_basis lin by auto with span_closed[OF xs] have "span (set xs) ⊂ carrier_vec n" by auto also have "carrier_vec n = span (set (unit_vecs n))" unfolding span_unit_vecs_is_carrier .. finally have sub: "span (set xs) ⊂ span (set (unit_vecs n))" . have "∃ u. u ∈ set (unit_vecs n) ∧ u ∉ span (set xs)" using span_subsetI[OF xs, of "set (unit_vecs n)"] sub by force then obtain u where uu: "u ∈ set (unit_vecs n)" and usxs: "u ∉ span (set xs)" by auto then have u: "u ∈ carrier_vec n" unfolding unit_vecs_def by auto let ?xs = "xs @ [u]" from span_mem[OF xs, of u] usxs have uxs: "u ∉ set xs" by auto with dist have dist: "distinct ?xs" by auto have lin: "lin_indpt (set ?xs)" using lin_dep_iff_in_span[OF xs lin u uxs] usxs by auto from lin dist u xs have lin: "lin_indpt_list ?xs" unfolding lin_indpt_list_def by auto from Suc(2) have "length ?xs + y = n" by auto from Suc(1)[OF this lin] obtain ys where "set ys ⊆ set (unit_vecs n)" "lin_indpt_list (?xs @ ys)" "length (?xs @ ys) = n" by auto thus ?case using uu by (intro exI[of _ "u # ys"], auto) qed qed definition "basis_extension xs = (SOME ys. set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n)" lemma basis_extension: assumes "lin_indpt_list xs" shows "set (basis_extension xs) ⊆ set (unit_vecs n)" "lin_indpt_list (xs @ basis_extension xs)" "length (xs @ basis_extension xs) = n" using someI_ex[OF expand_to_basis[OF assms], folded basis_extension_def] by auto lemma exists_lin_indpt_sublist: assumes X: "X ⊆ carrier_vec n" shows "∃ Ls. lin_indpt_list Ls ∧ span (set Ls) = span X ∧ set Ls ⊆ X" proof - let ?T = ?thesis have "(∃ Ls. lin_indpt_list Ls ∧ span (set Ls) ⊆ span X ∧ set Ls ⊆ X ∧ length Ls = k) ∨ ?T" for k proof (induct k) case 0 have "lin_indpt {}" by (simp add: lindep_span) thus ?case using span_is_monotone by (auto simp: lin_indpt_list_def) next case (Suc k) show ?case proof (cases ?T) case False with Suc obtain Ls where lin: "lin_indpt_list Ls" and span: "span (set Ls) ⊆ span X" and Ls: "set Ls ⊆ X" and len: "length Ls = k" by auto from Ls X have LsC: "set Ls ⊆ carrier_vec n" by auto show ?thesis proof (cases "X ⊆ span (set Ls)") case True hence "span X ⊆ span (set Ls)" using LsC X by (metis span_subsetI) with span have "span (set Ls) = span X" by auto hence ?T by (intro exI[of _ Ls] conjI True lin Ls) thus ?thesis by auto next case False with span obtain x where xX: "x ∈ X" and xSLs: "x ∉ span (set Ls)" by auto from Ls X have LsC: "set Ls ⊆ carrier_vec n" by auto from span_mem[OF this, of x] xSLs have xLs: "x ∉ set Ls" by auto let ?Ls = "x # Ls" show ?thesis proof (intro disjI1 exI[of _ ?Ls] conjI) show "length ?Ls = Suc k" using len by auto show "lin_indpt_list ?Ls" using lin xSLs xLs unfolding lin_indpt_list_def using lin_dep_iff_in_span[OF LsC _ _ xLs] xX X by auto show "set ?Ls ⊆ X" using xX Ls by auto from span_is_monotone[OF this] show "span (set ?Ls) ⊆ span X" . qed qed qed auto qed from this[of "n + 1"] lin_indpt_list_length_le_n show ?thesis by fastforce qed lemma exists_lin_indpt_subset: assumes "X ⊆ carrier_vec n" shows "∃ Ls. lin_indpt Ls ∧ span (Ls) = span X ∧ Ls ⊆ X" proof - from exists_lin_indpt_sublist[OF assms] obtain Ls where "lin_indpt_list Ls ∧ span (set Ls) = span X ∧ set Ls ⊆ X" by auto thus ?thesis by (intro exI[of _ "set Ls"], auto simp: lin_indpt_list_def) qed end end # Theory Sum_Vec_Set section ‹Sum of Vector Sets› text ‹We use Isabelle's Set-Algebra theory to be able to write V + W for sets of vectors V and W, and prove some obvious properties about them.› theory Sum_Vec_Set imports Missing_Matrix "HOL-Library.Set_Algebras" begin lemma add_0_right_vecset: assumes "(A :: 'a :: monoid_add vec set) ⊆ carrier_vec n" shows "A + {0⇩v 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 "{0⇩v 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 i∥⇧2 = (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 = (∑x∈C. 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 (∑x∈X. c x * x$ i)"
by (subst lincomb_index[OF i X], auto)
also have "… ≤ (∑x∈X. abs (c x * x $i))" by auto also have "… = (∑x∈X. abs (c x) * abs (x$ i))" by (auto simp: abs_mult)
also have "… ≤ (∑x∈X. 1 * abs (x $i))" by (rule sum_mono[OF mult_right_mono], insert c, auto) also have "… = (∑x∈X. abs (x$ i))" by simp
also have "… ≤ (∑x∈X. 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) = 0⇩v n"
by (rule lincomb_zero, insert Ws sub, auto simp: d_def)
also have "0⇩v 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}) = 0⇩v n" using lincomb_zero Vsx by auto
also have "x + 0⇩v 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 "0⇩v n ∈ finite_cone Vs"
proof -
let ?Vs = "(if finite Vs then Vs else {})"
have "lincomb (λ x. 0 :: 'a) ?Vs = 0⇩v 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: "0⇩v n ∈ cone Vs"
proof -
have "finite {}" by auto
moreover have "{} ⊆ cone Vs" by auto
moreover have "0⇩v 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 {} = {0⇩v n}"
by (auto simp: finite_cone_def nonneg_lincomb_def)

lemma cone_empty[simp]: "cone {} = {0⇩v 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 = 0⇩v 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 + {0⇩v 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. ∀w∈W. w ∙ x = 0} = cone X"
"⋀ x. ∀w∈W. 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: "∀w∈W. 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 = 0⇩v 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) + 0⇩v n" using Ls by auto
also have "0⇩v 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. ∀w∈W. 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. ∀w∈W. w ∙ x = 0} = cone X" unfolding Y_def .
qed

definition "polyhedral_cone (A :: 'a mat) = { x . x ∈ carrier_vec n ∧ A *⇩v x ≤ 0⇩v (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: " ∀w∈set Ds. dim_vec w = n" using DsC C by auto
have two: "∀w∈set (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 "… ≤ 0⇩v 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 ≤ 0⇩v nr" for x by auto
show "nr.lincomb_list ll (map ((*⇩v) A) Ds) $i ≤ 0⇩v 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 ≤ 0⇩v 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 = {0⇩v n}"
proof(rule ccontr)
assume "¬ ?thesis"
then obtain v where vC: "v ∈ cone C" and vnz: "v ≠ 0⇩v 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 ≥ 0⇩v nr ∧ A *⇩v x = b)"
proof -
let ?C = "set (cols A)"
from A have C: "?C ⊆ carrier_vec n" and C': " ∀w∈set (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 "x≥0⇩v 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. x≥0⇩v 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)) = (∃x≥0⇩v 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 (∑x∈Y. c x * x $i)" unfolding x by (subst lincomb_index[OF i Y], auto) also have "… ≤ (∑x∈Y. abs (c x * x$ i))" by auto
also have "… = (∑x∈Y. abs (c x) * abs (x $i))" by (simp add: abs_mult) also have "… ≤ (∑x∈Y. abs (c x) * Bnd)" by (intro sum_mono mult_left_mono, insert YBnd[unfolded Bounded_vec_def] i Y, force+) also have "… = (∑x∈Y. abs (c x)) * Bnd" by (simp add: sum_distrib_right) also have "(∑x∈Y. abs (c x)) = (∑x∈Y. 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 0⇩v 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 0⇩v 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 = 0⇩v n" using i x by auto
moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩v 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 = 0⇩v 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 0⇩v 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 = 0⇩v n"
using snoc.IH[OF Vs] i by auto
moreover have "(if i = length Vs then 1 else 0) ⋅⇩v x = 0⇩v n" using i x by auto
moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩v n) = 0⇩v 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 = 0⇩v n"
using Vs assms by (simp add: subset_code(1))
hence "lincomb_list (c ∘ Suc) Vs = 0⇩v 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 ⟹(∑x∈set 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) = 0⇩v 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 = 0⇩v 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 "(∑w∈W. 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 = 0⇩v 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 ≠ 0⇩v 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) = 0⇩v 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: "0⇩v 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 "v∙v=0" using ortho by auto moreover have "v ∈ carrier_vec n" using assms v by auto ultimately have "v=0⇩v 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 = 0⇩v n" using ortho_sum_in_span[OF W X ortho] by simp hence z2: "lincomb c X = 0⇩v 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 ≠ 0⇩v 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 ≠ 0⇩v n" proof assume nv: "nv = 0⇩v 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 ≠ 0⇩v 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 "… = (∑w∈D. 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 = 0⇩v 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) = 0⇩v 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 "0⇩v 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}) =
0⇩v 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 ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
proof
assume "∃ c. c ∈ carrier_vec n ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 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 ≤ (∑ai∈AA. l ai * (c ∙ ai))"
by (intro sum_nonneg mult_nonneg_nonneg, insert l ai AA, auto)
also have "… = (∑ai∈AA. l ai * (ai ∙ c))"
by (rule sum.cong, insert c A AA comm_scalar_prod, force+)
also have "… = (∑ai∈AA. ((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))`