# 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) lemma add_diff_cancel_right_vec: "a ∈ carrier_vec n ⟹ (b :: 'a :: cancel_ab_semigroup_add vec) ∈ carrier_vec n ⟹ (a + b) - b = a" by (intro eq_vecI, auto) lemma elements_four_block_mat_id: assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2" "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2" shows "elements_mat (four_block_mat A B C D) = elements_mat A ∪ elements_mat B ∪ elements_mat C ∪ elements_mat D" (is "elements_mat ?four = ?X") proof show "elements_mat ?four ⊆ ?X" by (rule elements_four_block_mat[OF c]) have 4: "?four ∈ carrier_mat (nr1 + nr2) (nc1 + nc2)" using c by auto { fix x assume "x ∈ ?X" then consider (A) "x ∈ elements_mat A" | (B) "x ∈ elements_mat B" | (C) "x ∈ elements_mat C" | (D) "x ∈ elements_mat D" by auto hence "x ∈ elements_mat ?four" proof (cases) case A from elements_matD[OF this] obtain i j where *: "i < nr1" "j < nc1" and x: "x = A $$ (i,j)" using c by auto from elements_matI[OF 4, of i j x] * c show ?thesis unfolding x by auto next case B from elements_matD[OF this] obtain i j where *: "i < nr1" "j < nc2" and x: "x = B $$ (i,j)" using c by auto from elements_matI[OF 4, of i "nc1 + j" x] * c show ?thesis unfolding x by auto next case C from elements_matD[OF this] obtain i j where *: "i < nr2" "j < nc1" and x: "x = C $$ (i,j)" using c by auto from elements_matI[OF 4, of "nr1 + i" j x] * c show ?thesis unfolding x by auto next case D from elements_matD[OF this] obtain i j where *: "i < nr2" "j < nc2" and x: "x = D $$ (i,j)" using c by auto from elements_matI[OF 4, of "nr1 + i" "nc1 + j" x] * c show ?thesis unfolding x by auto qed } thus "elements_mat ?four ⊇ ?X" by blast qed lemma elements_mat_append_rows: "A ∈ carrier_mat nr n ⟹ B ∈ carrier_mat nr2 n ⟹ elements_mat (A @⇩_{r}B) = elements_mat A ∪ elements_mat B" unfolding append_rows_def by (subst elements_four_block_mat_id, auto) lemma elements_mat_uminus[simp]: "elements_mat (-A) = uminus ` elements_mat A" unfolding elements_mat_def by auto lemma vec_set_uminus[simp]: "vec_set (-A) = uminus ` vec_set A" unfolding vec_set_def by auto definition append_cols :: "'a :: zero mat ⇒ 'a mat ⇒ 'a mat" (infixr "@⇩_{c}" 65) where "A @⇩_{c}B = (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 lemma vec_first_add: assumes "dim_vec x ≥ n" and "dim_vec y ≥ n" shows"vec_first (x + y) n = vec_first x n + vec_first y n" unfolding vec_first_def using assms by auto lemma vec_first_zero[simp]: "m ≤ n ⟹ vec_first (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) lemma add_diff_eq_vec: fixes y :: "'a :: group_add vec" shows "y ∈ carrier_vec n ⟹ x ∈ carrier_vec n ⟹ z ∈ carrier_vec n ⟹ y + (x - z) = y + x - z" by (intro eq_vecI, auto simp: add_diff_eq) definition "mat_of_col v = (mat_of_row v)⇧^{T}" lemma elements_mat_mat_of_col[simp]: "elements_mat (mat_of_col v) = vec_set v" unfolding mat_of_col_def by auto lemma mat_of_col_dim[simp]: "dim_row (mat_of_col v) = dim_vec v" "dim_col (mat_of_col v) = 1" "mat_of_col v ∈ carrier_mat (dim_vec v) 1" unfolding mat_of_col_def by auto lemma col_mat_of_col[simp]: "col (mat_of_col v) 0 = v" unfolding mat_of_col_def by auto lemma mult_mat_of_col: "A ∈ carrier_mat nr nc ⟹ v ∈ carrier_vec nc ⟹ A * mat_of_col v = mat_of_col (A *⇩_{v}v)" by (intro mat_col_eqI, auto) lemma mat_mult_append_cols: fixes A :: "'a :: comm_semiring_0 mat" assumes A: "A ∈ carrier_mat nr nc1" and B: "B ∈ carrier_mat nr nc2" and v1: "v1 ∈ carrier_vec nc1" and v2: "v2 ∈ carrier_vec nc2" shows "(A @⇩_{c}B) *⇩_{v}(v1 @⇩_{v}v2) = A *⇩_{v}v1 + B *⇩_{v}v2" proof - have "(A @⇩_{c}B) *⇩_{v}(v1 @⇩_{v}v2) = (A @⇩_{c}B) *⇩_{v}col (mat_of_col (v1 @⇩_{v}v2)) 0" by auto also have "… = col ((A @⇩_{c}B) * mat_of_col (v1 @⇩_{v}v2)) 0" by auto also have "(A @⇩_{c}B) * mat_of_col (v1 @⇩_{v}v2) = ((A @⇩_{c}B) * mat_of_col (v1 @⇩_{v}v2))⇧^{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)[1], subst finsum_scalar_prod_sum[OF f w], insert f, intro sum.cong[OF refl] comm_scalar_prod[OF _ w], auto) lemma lincomb_scalar_prod_left: assumes "W ⊆ carrier_vec n" "v ∈ carrier_vec n" shows "lincomb a W ∙ v = (∑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 by (simp add: lincomb_def) thus ?thesis using X by force qed (insert X, auto) lemma generating_card_n_basis: assumes X: "X ⊆ carrier_vec n" and span: "carrier_vec n ⊆ span X" and card: "card X = n" shows "basis X" proof - have fin: "finite X" proof (cases "n = 0") case False with card show "finite X" by (meson card.infinite) next case True with X have "X ⊆ carrier_vec 0" by auto also have "… = {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 by(auto simp add: smult_smult_assoc) finally show "v ∈ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" by auto qed thus "cone Vs ⊆ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" using cone_mono cone_cone[OF lVs] by blast qed lemma cone_add_cone: assumes C: "C ⊆ carrier_vec n" shows "cone C + cone C = cone C" proof note CC = cone_carrier[OF C] have "cone C = cone C + {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)" using add_smult_distrib_vec smult_smult_assoc by metis also have "l ⋅⇩_{v}lincomb_list cx Vs + (1 - l) ⋅⇩_{v}lincomb_list cy Vs + … = l ⋅⇩_{v}(lincomb_list cx Vs + cx (length Vs) ⋅⇩_{v}v) + (1 - l) ⋅⇩_{v}(lincomb_list cy Vs + cy (length Vs) ⋅⇩_{v}v)" using lincomb_list_carrier[OF Vs] v by (simp add: M.add.m_assoc M.add.m_lcomm smult_r_distr) finally show ?case using Vs v by simp qed simp hence "lincomb_list ?c Vs = l ⋅⇩_{v}x + (1 - l) ⋅⇩_{v}y" using Vs x y by simp moreover have "∀ i < length Vs. ?c i ≥ 0" using cx0 cy0 l0 l1 by simp moreover have "sum ?c {0..<length Vs} = 1" proof(simp add: sum.distrib) have "(∑i = 0..<length Vs. (1 - l) * cy i) = (1 - l) * sum cy {0..<length Vs}" using sum_distrib_left by metis moreover have "(∑i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}" using sum_distrib_left by metis ultimately show "(∑i = 0..<length Vs. l * cx i) + (∑i = 0..<length Vs. (1 - l) * cy i) = 1" using cx1 cy1 by simp qed ultimately show ?thesis unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto qed lemma convex_hull_list_mono: assumes "set Ws ⊆ carrier_vec n" shows "set Vs ⊆ set Ws ⟹ convex_hull_list Vs ⊆ convex_hull_list Ws" proof (standard, induction Vs) case Nil from Nil(2) show ?case unfolding convex_hull_list_def convex_lincomb_list_def by auto next case (Cons v Vs) have v: "v ∈ set Ws" and Vs: "set Vs ⊆ set Ws" using Cons.prems(1) by auto hence v1: "v ∈ convex_hull_list Ws" using set_in_convex_hull_list[OF assms] by auto from Cons.prems(2) obtain c where x: "lincomb_list c (v # Vs) = x" and c0: "∀ i < length Vs + 1. c i ≥ 0" and c1: "sum c {0..<length Vs + 1} = 1" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto have x: "x = c 0 ⋅⇩_{v}v + lincomb_list (c ∘ Suc) Vs" using Vs v assms x by auto show ?case proof (cases) assume P: "c 0 = 1" hence "sum (c ∘ Suc) {0..<length Vs} = 0" using sum.atLeast0_lessThan_Suc_shift c1 by (metis One_nat_def R.show_r_zero add.right_neutral add_Suc_right) moreover have "⋀ i. i ∈ {0..<length Vs} ⟹ (c ∘ Suc) i ≥ 0" using c0 by simp ultimately have "∀ i ∈ {0..<length Vs}. (c ∘ Suc) i = 0" using sum_nonneg_eq_0_iff by blast hence "⋀ i. i < length Vs ⟹ (c ∘ Suc) i ⋅⇩_{v}Vs ! i = 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 (* finally derive contradiction *) let ?R = "{hs i | i. i < len}" define r where "r = Max ?R" from cond[OF len0] have "hs 0 ∈ I" using IsI unfolding cond_def by auto hence R0: "hs 0 ∈ ?R" using len0 by auto have finR: "finite ?R" by auto from Max_in[OF finR] R0 have rR: "r ∈ ?R" unfolding r_def[symmetric] by auto then obtain p where rp: "r = hs p" and p: "p < len" by auto from Max_ge[OF finR, folded r_def] have rLarge: "i < len ⟹ hs i ≤ r" for i by auto have exq: "∃q. ks q = r ∧ q < len" proof (rule ccontr) assume neg: "¬?thesis" show False proof(cases "r ∈ I") case True have 1: "j∈{Suc p..len} ⟹ r ∉ Is j" for j proof(induction j rule: less_induct) case (less j) from less(2) have j_bounds: "j = Suc p ∨ j > Suc p" by auto from less(2) have j_len: "j ≤ len" by auto have pj_cond: "j = Suc p ⟹ cond (Is p) (Is j) (ls p) (cs p) (hs p) (ks p)" using cond p by blast have r_neq_ksp: "r ≠ ks p" using p neg by auto have "j = Suc p ⟹ Is j = insert (ks p) (Is p - {r})" using rp cond pj_cond cond_def[of "Is p" "Is j" _ _ r] by blast hence c1: "j = Suc p ⟹ r ∉ Is j" using r_neq_ksp by simp have IH: "⋀t. t < j ⟹ t ∈ {Suc p..len} ⟹ r ∉ Is t" by fact have r_neq_kspj: "j > Suc p ∧ j ≤ len ⟹ r ≠ ks (j-1)" using j_len neg IH by auto have jsucj_cond: "j > Suc p ∧ j ≤ len ⟹ Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})" using cond_def[of "Is (j-1)" "Is j"] cond by (metis (no_types, lifting) Suc_less_eq2 diff_Suc_1 le_simps(3)) hence "j > Suc p ∧ j ≤ len ⟹ r ∉ insert (ks (j-1))