Theory Lattice_int
theory Lattice_int
imports
"Jordan_Normal_Form.Matrix"
"Jordan_Normal_Form.VS_Connect"
"BenOr_Kozen_Reif.More_Matrix"
begin
section ‹Basics on Lattices›
text ‹Connect the type ‹vec› to records of rings, commutative rings, fields and modules in order to
use properties of modules such as ‹lin_indpt› (linear independence).›
lemma dim_carrier: "dim_vec z = dim_col A ⟹ A *⇩v z ∈ carrier_vec (dim_row A)"
by (metis carrier_vec_dim_vec dim_mult_mat_vec)
text ‹Concrete type conversion ‹int vec› to ‹real vec››
definition real_of_int_vec :: "int vec ⇒ real vec" where
"real_of_int_vec v = map_vec real_of_int v"
definition real_to_int_vec :: "real vec ⇒ int vec" where
"real_to_int_vec v = map_vec floor v"
lemma dim_vec_real_of_int_vec[simp]: "dim_vec (real_of_int_vec v) = dim_vec v"
unfolding real_of_int_vec_def by auto
lemma real_of_int_vec_nth[simp, intro]:
"i<dim_vec v ⟹ (real_of_int_vec v) $ i = real_of_int (v$i)"
by (simp add: real_of_int_vec_def)
lemma real_of_int_vec_vec:
"real_of_int_vec (vec n f) = vec n (real_of_int ∘ f)"
by (auto simp add: real_of_int_vec_def)
text ‹Concrete type conversion ‹int mat› to ‹real mat››
definition real_of_int_mat :: "int mat ⇒ real mat" where
"real_of_int_mat A = map_mat real_of_int A"
definition real_to_int_mat :: "real mat ⇒ int mat" where
"real_to_int_mat A = map_mat floor A"
lemma dim_col_real_of_int_mat[simp]: "dim_col (real_of_int_mat A) = dim_col A"
unfolding real_of_int_mat_def by auto
lemma dim_row_real_of_int_mat[simp]: "dim_row (real_of_int_mat A) = dim_row A"
unfolding real_of_int_mat_def by auto
lemma real_of_int_mat_nth[simp, intro]:
"i<dim_row A ⟹ j<dim_col A ⟹ (real_of_int_mat A) $$ (i,j) = real_of_int (A $$ (i,j))"
by (simp add: real_of_int_mat_def)
lemma real_of_int_mat_mat:
"real_of_int_mat (mat n m f) = mat n m (real_of_int ∘ f)"
by (auto simp add: real_of_int_mat_def)
lemma real_of_int_mat_cols:
"cols (real_of_int_mat A) = map real_of_int_vec (cols A)"
by (simp add: list_eq_iff_nth_eq real_of_int_mat_def real_of_int_vec_def)
lemma distinct_cols_real_of_int_mat:
"distinct (cols A) = distinct (cols (real_of_int_mat A))"
by (smt (verit, best) cols_length distinct_conv_nth index_map_mat(3) nth_map
of_int_hom.vec_hom_inj real_of_int_mat_cols real_of_int_mat_def real_of_int_vec_def)
text ‹Algebraic lattices are discrete additive subgroups of $\mathbb{R}^n$.
Lattices can be represented by a basis, multiple bases can represent the same lattice.›
type_synonym int_lattice = "int vec set"
text ‹Linear independence›
consts is_indep :: "'a ⇒ bool"
overloading
is_indep_real ≡ "is_indep :: real mat ⇒ bool"
is_indep_int ≡ "is_indep :: int mat ⇒ bool"
begin
definition is_indep_real :: "real mat ⇒ bool" where
"is_indep A = (∀z::real vec. (A *⇩v z = 0⇩v (dim_row A) ∧
dim_vec z = dim_col A) ⟶ z = 0⇩v (dim_vec z))"
definition is_indep_int :: "int mat ⇒ bool" where
"is_indep A = (∀z::real vec. ((real_of_int_mat A) *⇩v z = 0⇩v (dim_row A) ∧
dim_vec z = dim_col A) ⟶ z = 0⇩v (dim_vec z))"
end
text ‹Definition of lattices›
definition is_lattice :: "int_lattice ⇒ bool" where
"is_lattice L ≡ (∃B::(int mat).
L = {B *⇩v z | z::int vec. dim_vec z = dim_col B}
∧ is_indep B)"
text ‹The lattice generated by the column vectors of a matrix.
This matrix does not need to be linearly independent.
Make certain that the output is indeed a lattice and not the entire space.›
definition gen_lattice :: "int mat ⇒ int vec set" where
"gen_lattice A = {A *⇩v z | z::int vec. dim_vec z = dim_col A}"
text ‹Theorems for lattices. The aim is to have a change of basis theorem for lattice bases.
The theorems are mostly taken from the respective theorems for the type ‹('a,'k::finite) vec›
and adapted to the type ‹'a vec›.›
lemma finsum_vec_carrier:
assumes "f ` A ⊆ carrier_vec nr" "finite A"
shows "finsum_vec TYPE('a::ring) nr f A ∈ carrier_vec nr"
using assms unfolding finsum_vec_def
by (metis (no_types, lifting) Pi_I' comm_monoid.finprod_closed comm_monoid_vec
image_subset_iff monoid_vec_simps(2))
lemma dim_vec_finsum_vec:
assumes "f ` A ⊆ carrier_vec nr" "finite A"
shows "dim_vec (finsum_vec TYPE('a::ring) nr f A) = nr"
using assms finsum_vec_carrier by (metis carrier_vecD)
text ‹Matrix-Vector-Multiplication as an element in the column span.›
lemma mat_mult_as_col_span:
assumes "(A :: 'a :: comm_ring mat) ∈ carrier_mat nr nc"
and "(z :: 'a vec) ∈ carrier_vec nc"
shows "A *⇩v z = finsum_vec TYPE('a) nr (λi. z$i ⋅⇩v col A i) {0..<nc}"
(is "?left = ?right")
proof -
have *: "finsum_vec TYPE('a) nr (λi. z$i ⋅⇩v col A i) {0..<nc} $ j = (A *⇩v z) $ j"
if "j<nr" for j
proof -
have "finsum_vec TYPE('a) nr (λi. z$i ⋅⇩v col A i) {0..<nc} $ j =
sum (λi. (z$i ⋅⇩v col A i) $ j) {0..<nc}"
by (subst index_finsum_vec, use assms that in ‹auto›)
also have "… = sum (λi. z$i * (col A i $ j)) {0..<nc}"
using assms(1) that by force
also have "… = sum (λi. z$i * A $$ (j,i)) {0..<nc}" using assms that by auto
also have "… = sum (λi. A $$ (j,i) * z$i) {0..<nc}"
by (meson mult.commute)
also have "… = sum (λi. row A j $ i * z $ i) {0..<nc}"
using assms that by (auto simp add: index_row(1)[symmetric] simp del: index_row(1))
also have "… = (A *⇩v z) $ j"
unfolding mult_mat_vec_def scalar_prod_def using assms that by auto
finally show ?thesis by blast
qed
then show ?thesis
proof (subst eq_vecI[of ?left ?right], goal_cases)
case (1 i)
have dim_nr: "dim_vec (A *⇩v z) = nr"
using assms(1) dim_mult_mat_vec by blast
show ?case using assms 1 unfolding dim_nr by auto
next
case 2
then show ?case using assms by (subst dim_vec_finsum_vec, auto)
qed auto
qed
text ‹A matrix is identical to the matrix generated by its indices.›
lemma mat_index:
"B = mat (dim_row B) (dim_col B) (λ(i,j). B $$ (i,j))"
by auto
text ‹Lemmas about the colums of a matrix.›
lemma col_unit_vec:
assumes "i<dim_col (B:: 'a :: {monoid_mult, semiring_0, zero_neq_one} mat)"
shows "B *⇩v (unit_vec (dim_col B) i) = col B i" (is "?left = ?right")
proof -
have "B $$ (ia, i) = (∑ib = 0..<dim_col B. B $$ (ia, ib) * (if ib = i then 1 else 0))"
if "ia < dim_row B" for ia
proof -
have "(∑ib = 0..<dim_col B. B $$ (ia, ib) * (if ib = i then 1 else 0)) =
(∑ib = 0..<dim_col B. (if ib = i then B $$ (ia, ib) else 0))"
by (smt (verit, best) mult.right_neutral mult_zero_right sum.cong)
also have "… = B $$ (ia, i) +
(∑ib∈ {0..<dim_col B}-{i}. (if ib = i then B $$ (ia, ib) else 0))"
by (simp add: assms)
also have "… = B $$ (ia, i)" by simp
finally show ?thesis by auto
qed
then show ?thesis using assms by (subst eq_vecI[of ?left ?right])
(auto simp add: unit_vec_def scalar_prod_def)
qed
lemma is_indep_not_null:
assumes "is_indep (B:: real mat)" "i<dim_col B"
shows "col B i ≠ 0⇩v (dim_row B)"
proof (rule ccontr)
assume "¬ (col B i ≠ 0⇩v (dim_row B))"
then have "col B i = 0⇩v (dim_row B)" by auto
then have "B *⇩v (unit_vec (dim_col B) i) = 0⇩v (dim_row B)"
using col_unit_vec assms(2) by metis
moreover have "dim_vec (unit_vec (dim_col B) i) = dim_col B" by auto
moreover have "(unit_vec (dim_col B) i) ≠ 0⇩v (dim_col B)"
by (simp add: assms(2))
ultimately have "¬ (is_indep B)" unfolding is_indep_real_def by auto
then show False using assms by auto
qed
lemma col_in_gen_lattice:
assumes "i<dim_col B"
shows "col B i ∈ gen_lattice B"
unfolding gen_lattice_def proof (safe)
have "col B i = B *⇩v (unit_vec (dim_col B) i)" using col_unit_vec[OF assms] by auto
moreover have "dim_vec (unit_vec (dim_col B) i) = dim_col B" by auto
ultimately show "∃z. col B i = B *⇩v z ∧ dim_vec z = dim_col B" by auto
qed
section ‹Change of Basis in a Lattice›
text ‹Definition of the column span.›
definition span :: "('a :: semiring_0) mat ⇒ 'a vec set" where
"span B = {B *⇩v z | z:: 'a vec. dim_vec z = dim_col B}"
text ‹Definition of the column dimension of a matrix›
definition dim :: "int mat ⇒ nat" where
"dim B = (if ∃b. is_indep (real_of_int_mat b) ∧ span (real_of_int_mat b) = span (real_of_int_mat B)
then dim_col (SOME b. is_indep (real_of_int_mat b) ∧
span (real_of_int_mat b) = span (real_of_int_mat B)) else 0)"
text ‹Abbreviation of the set of columns›
definition set_cols[simp]: "set_cols A = set (cols A)"
text ‹For the change of basis, we need to be able to delete and insert a column
vector in the column span.›
definition insert_col:
"insert_col A c = mat_of_cols (dim_row A) (c # cols A)"
definition delete_col:
"delete_col A c = mat_of_cols (dim_row A) (filter (λ x. ¬ (x = c)) (cols A))"
lemma set_cols_col:
"set_cols A = col A ` {0..<dim_col A}"
by (simp add: cols_def)
lemma set_cols_subset_col:
assumes "set_cols A ⊆ set_cols B"
"i<dim_col A"
obtains j where "col A i = col B j"
proof -
have "col A i ∈ set_cols B" using assms
by (metis cols_length cols_nth nth_mem set_cols subsetD)
then have "∃j. col A i = col B j ∧ j<dim_col B"
using set_cols_col by fastforce
then show ?thesis using that by blast
qed
text ‹Monotonicity of the span.›
lemma span_mono:
assumes "set_cols (A ::'a::comm_ring mat) ⊆ set_cols B" "dim_row A = dim_row B"
"distinct (cols A)"
shows "span A ⊆ span B"
using assms proof (induction "card (set_cols B - set_cols A)" arbitrary: A B rule: less_induct)
case less
then show ?case unfolding span_def
proof (safe, goal_cases)
case (1 _ z)
define nr where "nr = dim_row B"
define nc where "nc = dim_col B"
have 2: "B ∈ carrier_mat nr nc" unfolding nr_def nc_def by auto
have 3: "set (cols A) ⊆ set (cols B)" using less.prems(1) by auto
have 4: "z ∈ carrier_vec (length (cols A))" using 1(5)
by (metis carrier_vec_dim_vec cols_length)
have 5: "mat_of_cols nr (cols A) = A"
by (metis less.prems(2) mat_of_cols_cols nr_def)
obtain zb where "A *⇩v z = B *⇩v zb" "dim_vec zb = dim_col B"
using helper3[of B nr nc "cols A" z, OF 2 less.prems(3) 3 4] unfolding nc_def 5 by auto
then show ?case by auto
qed
qed
text ‹Monotonicity of linear independence›
lemma is_indep_mono:
assumes "set_cols B ⊆ set_cols A" "is_indep A" "distinct (cols B)" "dim_row A = dim_row B"
shows "is_indep (B::real mat)"
unfolding is_indep_real_def
proof (safe, goal_cases)
case (1 z)
define nr where "nr = dim_row A"
define nc where "nc = dim_col A"
have r: "nr = dim_row B" unfolding nr_def using assms(4) by auto
have A': "A ∈ carrier_mat nr nc" unfolding nr_def nc_def by auto
define ss where "ss = cols (B)"
have d: "distinct (cols B)" using assms(3)
by (simp add: distinct_cols_real_of_int_mat)
have sub: "set (cols B) ⊆ set (cols A)"
using assms(1) real_of_int_mat_cols by auto
from distinct_list_subset_nths[of "cols B" "cols A", OF d sub]
obtain ids where ids: "distinct ids" "set ids ⊆ {..<length (cols A)}"
and ss: "ss = map ((!) (cols A)) ids"
using assms(1) set_cols ss_def by blast
let ?ls = " map ((!) (cols A)) (filter (λi. i ∉ set ids) [0..<length (cols A)])"
from subindex_permutation2[OF ids] obtain f where
f: "f permutes {..<length (cols A)}"
"cols A = permute_list f (?ls @ ss)" using ss by blast
have f': "f permutes {..<nc}" using f(1) unfolding nc_def by simp
have *: "⋀x. x ∈ set ?ls ⟹ dim_vec x = nr" using nr_def by auto
let ?cs1 = "(list_of_vec (0⇩v (length ?ls) @⇩v z))"
have z: "z ∈ carrier_vec (length ss)" unfolding ss_def using 1
using carrier_dim_vec by auto
have "0⇩v nr = B *⇩v z" using 1 unfolding r by auto
also have "… = mat_of_cols nr ss *⇩v z" unfolding ss_def r by simp
also have "… = mat_of_cols nr (?ls @ ss) *⇩v vec_of_list (?cs1)"
using helper2[OF z] * by (metis vec_list)
also have "... = mat_of_cols nr (permute_list f (?ls @ ss)) *⇩v vec_of_list (permute_list f ?cs1)"
by (auto intro!: mat_of_cols_mult_mat_vec_permute_list[symmetric])
(metis cols_length f(1) f(2) length_append length_map length_permute_list,
use ss_def z in ‹force›)
also have "... = A *⇩v vec_of_list (permute_list f ?cs1)" using f(2)
by (simp add: nr_def)
finally have "A *⇩v vec_of_list (permute_list f ?cs1) = 0⇩v nr"
by presburger
then have zero: "vec_of_list (permute_list f ?cs1) = 0⇩v nc"
by (smt (verit, best) assms(2) carrier_vecD cols_length dim_vec_of_list f(2)
index_append_vec(2) index_map_mat(2) index_map_mat(3) index_zero_vec(2) is_indep_real_def
length_append length_list_of_vec length_permute_list nc_def nr_def real_of_int_mat_def z)
then have *: "permute_list f ?cs1 ! i = 0" if "i<nc" for i
by (metis index_zero_vec(1) that vec_of_list_index)
then have "?cs1 ! (f i) = 0" if "i<nc" for i
by (metis cols_length dim_vec_of_list f(1) index_zero_vec(2) length_permute_list nc_def
permute_list_nth that zero)
then have "(λi. ?cs1 ! (f i)) ` {..<nc} ⊆ {0}" by blast
then have "(λi. ?cs1 ! i) ` (f `{..<nc}) ⊆ {0}" by blast
then have "(λi. ?cs1 ! i) ` {..<nc} ⊆ {0}" using permutes_imp_bij[OF f']
by (metis cols_length f' length_map nc_def permutes_image)
then have *: "?cs1 ! i = 0" if "i<nc" for i using that by blast
then have "z $ i = 0" if "i<dim_vec z" for i using *[of "length ?ls + i"]
by (metis (no_types, lifting) add_diff_cancel_left' add_less_cancel_left dim_vec_of_list
index_append_vec(2) index_zero_vec(2) length_list_of_vec length_permute_list
list_of_vec_append not_add_less1 nth_append nth_list_of_vec that zero)
then show "z = 0⇩v (dim_vec z)"
by (metis eq_vecI index_zero_vec(1) index_zero_vec(2))
qed
text ‹Linear independent vectors are distinct.›
lemma is_indep_distinct:
assumes "is_indep (A::real mat)"
shows "distinct (cols A)"
proof (rule ccontr)
define nc where "nc = dim_col A"
define nr where "nr = dim_row A"
assume "¬ distinct (cols A)"
then obtain i j where ij: "i ≠ j" "i<nc" "j<nc" "col A i = col A j"
unfolding nc_def by (metis cols_length cols_nth distinct_conv_nth)
have "A *⇩v (unit_vec nc i - unit_vec nc j) = 0⇩v nr"
by (smt (verit, ccfv_threshold) ij carrier_mat_triv col_dim col_map_mat col_unit_vec
index_map_mat(2) index_map_mat(3) minus_cancel_vec mult_minus_distrib_mat_vec nc_def
nr_def real_of_int_mat_def unit_vec_carrier)
moreover have "dim_vec (unit_vec nc i - unit_vec nc j) = nc" by simp
moreover have "(unit_vec nc i - unit_vec nc j) ≠ 0⇩v nc" using ij
by (smt (z3) assms calculation(1) calculation(2) index_minus_vec(1) index_unit_vec(1)
index_unit_vec(3) index_zero_vec(1) is_indep_real_def nc_def nr_def)
ultimately have "¬ is_indep A" unfolding is_indep_real_def using nc_def nr_def
by (smt (verit, ccfv_threshold) carrier_matI col_dim col_unit_vec minus_cancel_vec
mult_minus_distrib_mat_vec unit_vec_carrier)
then show False using assms by auto
qed
text ‹Column vectors are in the column span.›
lemma span_base:
assumes "(a :: 'a :: {monoid_mult,semiring_0,zero_neq_one} vec) ∈ set_cols S"
shows "a ∈ span S"
proof -
obtain i where "i<dim_col S" "a = col S i" using assms
by (metis atLeastLessThan_iff imageE set_cols_col)
then have "a = S *⇩v (unit_vec (dim_col S) i)"
using col_unit_vec[OF ‹i<dim_col S›, symmetric] by auto
then show ?thesis unfolding span_def by auto
qed
text ‹Representing vectors in the column span of a linear independent matrix.
The representation function returns the coefficients needed to generate the
vector as an element in the column span.›
text ‹Respresentation function and its lemmas were adapted from ``HOL/Modules.thy''›
definition representation :: "real mat ⇒ real vec ⇒ real vec ⇒ real"
where "representation B v =
(if is_indep B ∧ v ∈ (span B) then
SOME f. (∀v. f v ≠ 0 ⟶ v ∈ set_cols B) ∧
B *⇩v (vec (dim_col B) (λi. f (col B i))) = v
else (λb. 0))"
text ‹If the column vectors form a basis of the column span, the representation function is unique.›
lemma unique_representation:
assumes basis: "is_indep (basis::real mat)"
and in_basis: "⋀v. f v ≠ 0 ⟹ v ∈ set_cols basis" "⋀v. g v ≠ 0 ⟹ v ∈ set_cols basis"
and eq: "basis *⇩v (vec (dim_col basis) (λi. f (col basis i))) =
basis *⇩v (vec (dim_col basis) (λi. g (col basis i)))"
shows "f = g"
proof (rule ext, rule ccontr)
fix v assume ne: "f v ≠ g v"
then have in_col: "v ∈ set_cols basis" using in_basis by metis
have "¬ is_indep basis"
unfolding is_indep_real_def
proof (subst not_all, subst not_imp)
let ?x = "vec (dim_col basis) (λi. (f (col basis i)- g (col basis i)))"
have "∃v∈set_cols basis. f v - g v ≠ 0"
using ne in_col right_minus_eq by blast
then have ex: "∃i<dim_col basis. f (col basis i) - g (col basis i) ≠ 0"
by (metis atLeastLessThan_iff imageE set_cols_col)
have "basis *⇩v (?x) =
basis *⇩v (vec (dim_col basis) (λi. f (col basis i))) -
basis *⇩v (vec (dim_col basis) (λi. g (col basis i)))"
proof -
have *: "?x = vec (dim_col basis) (λi. f (col basis i)) -
vec (dim_col basis) (λi. g (col basis i))" unfolding minus_vec_def by auto
show ?thesis unfolding *
by (meson carrier_mat_triv mult_minus_distrib_mat_vec vec_carrier)
qed
then have "basis *⇩v (?x) = 0⇩v (dim_row basis)" using eq by auto
moreover have "dim_vec ?x = dim_col basis"
using dim_vec by blast
moreover have "?x ≠ 0⇩v (dim_col basis)" using ex
by (metis (no_types, lifting) index_vec index_zero_vec(1))
ultimately show "∃x. (basis *⇩v x = 0⇩v (dim_row basis) ∧
dim_vec x = dim_col basis) ∧ x ≠ 0⇩v (dim_vec x)"
using real_of_int_vec_def by auto
qed
with basis show False by auto
qed
text ‹More properties on the representation function.›
lemma
shows representation_ne_zero: "⋀b. representation basis v b ≠ 0 ⟹ b ∈ set_cols basis"
and sum_nonzero_representation_eq:
"is_indep basis ⟹ v ∈ span basis ⟹
basis *⇩v (vec (dim_col basis) (λi. representation basis v (col basis i))) = v"
proof -
{ assume basis: "is_indep basis" and v: "v ∈ span basis"
define p where "p f ⟷
(∀v. f v ≠ 0 ⟶ v ∈ set_cols basis) ∧
basis *⇩v (vec (dim_col basis) (λi. f (col basis i))) = v" for f
obtain z where z: "basis *⇩v z = v" "dim_vec z = dim_col basis"
using ‹v ∈ span basis› unfolding span_def by auto
define r where "r = (λv. if (∃i<dim_col basis. v = col basis i)
then z$(SOME i. i<dim_col basis ∧ v = col basis i) else 0)"
then have "r (col basis i) = z$i" if "i<dim_col basis" for i
proof -
have "z $ (SOME j. j<dim_col basis ∧ col basis ia = col basis j) = z $ i"
if "i < dim_col basis"
"distinct (cols basis)"
"ia < dim_col basis"
"col basis i = col basis ia"
for ia
proof -
have "i = ia" using that
by (metis cols_length cols_nth distinct_conv_nth)
obtain j where j: "j = (SOME j. j<dim_col basis ∧ col basis i = col basis j)" by blast
then have "j<dim_col basis" "col basis i = col basis j"
by (smt (verit, best) ‹i = ia› someI_ex that(3))
(metis (mono_tags, lifting) j that(1) verit_sko_ex')
then have "i = j" using that
by (metis cols_length cols_nth distinct_conv_nth)
then show ?thesis unfolding j(1)
using that(4) by auto
qed
then show ?thesis
unfolding r_def using that is_indep_distinct[OF basis] by auto
qed
then have "z = (vec (dim_col basis) (λi. r (col basis i)))"
using z(2) by auto
then have *:
"basis *⇩v (vec (dim_col basis) (λi. r (col basis i))) = v"
using z by auto
define f where "f b = (if b ∈ set_cols basis then r b else 0)" for b
have "p f"
using * unfolding p_def f_def
by (smt (verit, best) cols_length cols_nth dim_vec eq_vecI index_vec nth_mem set_cols)
have *: "representation basis v = Eps p"
by (simp add: p_def[abs_def] representation_def basis v)
from someI[of p f, OF ‹p f›] have "p (representation basis v)"
unfolding * . }
note * = this
show "representation basis v b ≠ 0 ⟹ b ∈ set_cols basis" for b
using * by (cases "is_indep basis ∧ v ∈ span basis") (auto simp: representation_def)
show "is_indep basis ⟹ v ∈ span basis ⟹
basis *⇩v (vec (dim_col basis) (λi. representation basis v (col basis i))) = v"
using * by auto
qed
lemma representation_eqI:
assumes basis: "is_indep basis" and b: "v ∈ span basis"
and ne_zero: "⋀b. f b ≠ 0 ⟹ b ∈ set_cols basis"
and eq: "basis *⇩v (vec (dim_col basis) (λi. f (col basis i))) = v"
shows "representation basis v = f"
by (rule unique_representation[OF basis])
(auto simp: representation_ne_zero
sum_nonzero_representation_eq[OF basis b] ne_zero eq simp del: set_cols)
text ‹Representation function when extending the column space.›
lemma representation_extend:
assumes basis: "is_indep basis" and v: "v ∈ span basis'"
and basis': "set_cols basis' ⊆ set_cols basis" and d: "dim_row basis = dim_row basis'"
and dc: "distinct (cols basis')"
shows "representation basis v = representation basis' v"
proof (rule representation_eqI[OF basis])
show v': "v ∈ span basis" using span_mono[OF basis' d[symmetric] dc] v by auto
have *: "is_indep basis'" using is_indep_mono[OF basis' basis dc d] by (auto)
show "representation basis' v b ≠ 0 ⟹ b ∈ set_cols basis" for b
using representation_ne_zero basis' by auto
have dim_row: "dim_row basis' = dim_row basis"
by (metis "*" Lattice_int.sum_nonzero_representation_eq basis dim_mult_mat_vec v v')
show "basis *⇩v vec (dim_col basis) (λi. representation basis' v (col basis i)) = v "
proof -
have not_in': "representation basis' v b = 0" if "b ∉ set_cols basis'" for b
using Lattice_int.representation_ne_zero that by blast
let ?vec = "vec (dim_row basis) (λi. ∑ia = 0..<dim_vec
(vec (dim_col basis) (λi. Lattice_int.representation basis' v (col basis i))).
row basis i $ ia * vec (dim_col basis)
(λi. Lattice_int.representation basis' v (col basis i)) $ ia)"
have dim_v: "dim_vec v = dim_row basis"
using Lattice_int.span_def dim_row v by force
have "v= ?vec"
proof (subst eq_vecI[of v ?vec], goal_cases)
case (1 i)
obtain ids where ids: "distinct ids" "set ids ⊆ {..<length (cols basis)}"
and ss: "cols basis' = map ((!) (cols basis)) ids"
using distinct_list_subset_nths[OF dc, of "cols basis"] basis' set_cols by blast
define ls where "ls = map ((!) (cols basis))
(filter (λi. i ∉ set ids) [0..<length (cols basis)])"
from subindex_permutation2[OF ids] obtain p where
p: "p permutes {..<length (cols basis)}"
"cols basis = permute_list p (ls @ (cols basis'))" unfolding ls_def using ss by metis
then have p_i: "col basis i = (ls @ (cols basis')) ! (p i)" if "i<length (cols basis)" for i
by (metis cols_length cols_nth length_permute_list permute_list_nth that)
have len_ls: "length ls ≤ length (cols basis)"
by (metis length_append length_permute_list linorder_not_less not_add_less1 p(2))
have in_ls: "col basis j = ls ! (p j)" if "j ∈ p -` {0..<length ls}" for j
using p_i
by (metis atLeastLessThan_upt len_ls lessThan_atLeast0 lessThan_iff lessThan_subset_iff
nth_append p(1) permutes_in_image subset_code(1) that vimageE)
have not_in_ls: "col basis j = (cols basis') ! (p j - length ls)"
if "j ∈ p -` {length ls..<length (cols basis)}" for j
proof -
have "(ls @ (cols basis')) ! (p j) = (cols basis') ! (p j - length ls)" using that
by (meson atLeastLessThan_iff leD nth_append vimage_eq)
then show ?thesis using p_i[of j] that
by (metis (mono_tags, lifting) atLeastLessThan_iff lessThan_iff p(1) permutes_def vimageE)
qed
have distinct: "distinct (cols basis)" using is_indep_distinct[OF basis] .
have ls_in_basis: "set ls ⊆ set_cols basis" unfolding set_cols ls_def
by (auto, metis cols_length cols_nth nth_mem)
have ls_not_in_basis': "(set ls) ∩ (set_cols basis') = {}"
proof (subst disjoint_iff, intro allI, intro impI)
fix x assume "x ∈ set ls"
then obtain j where j: "col basis j = x" using ls_in_basis
by (metis imageE set_cols_col subsetD)
then have "j ∉ set ids"using ‹x∈set ls› unfolding ls_def
by (smt (verit, del_insts) atLeastLessThan_iff atLeast_upt cols_length cols_nth distinct
distinct_conv_nth ids(2) imageE list.set_map mem_Collect_eq set_filter set_upt subsetD)
then show "x ∉ set_cols basis'" unfolding set_cols ss j[symmetric]
by (smt (verit, ccfv_threshold) ‹x ∈ set ls› atLeast_upt distinct distinct_conv_nth ids(2)
in_set_conv_nth j length_map lessThan_iff ls_def mem_Collect_eq nth_map nth_mem
set_filter subsetD)
qed
have rep: "representation basis' v = (SOME f. (∀v. f v ≠ 0 ⟶ v ∈ set_cols basis') ∧
basis' *⇩v vec (dim_col basis') (λi. f (col basis' i)) = v) "
unfolding representation_def using ‹is_indep basis'› ‹v∈span basis'› by auto
then obtain f where some_f: "f = (SOME f. (∀v. f v ≠ 0 ⟶ v ∈ set_cols basis') ∧
basis' *⇩v vec (dim_col basis') (λi. f (col basis' i)) = v)" by blast
then have f: "∀v. f v ≠ 0 ⟶ v ∈ set_cols basis'"
"basis' *⇩v vec (dim_col basis') (λi. f (col basis' i)) = v"
apply (metis not_in' rep)
by (metis "*" Lattice_int.sum_nonzero_representation_eq rep some_f v)
then have rep_f: "representation basis' v = f" using rep some_f by auto
have not_in_f: "f b = 0" if "b ∉ set_cols basis' " for b using not_in'
using f(1) that by blast
have f_ls_0: "f (ls ! j) = 0" if "j<length ls" for j
apply (subst not_in_f) using ls_not_in_basis' nth_mem that by auto
have "?vec $ i = vec (dim_vec v) (λi. ∑ia = 0..<dim_col basis.
row basis i $ ia * vec (dim_col basis) (λj. f (col basis j)) $ ia) $ i"
using dim_v[symmetric] rep_f by auto
also have "… = (∑ia = 0..<dim_col basis.
row basis i $ ia * vec (dim_col basis) (λj. f (col basis j)) $ ia)"
using ‹i<dim_vec v› by auto
also have "… = (∑ia = 0..<length (cols basis). basis $$ (i, ia) * (f (col basis ia)))"
using "1" dim_v by force
also have "… = (∑ia ∈ p -` {0..<length (cols basis)}.
(col basis ia $ i) * (f (col basis ia)))"
using "1" dim_v p(1) by (simp add: atLeast0LessThan permutes_vimage)
also have "… = (∑ia ∈ p -` {0..<length ls} ∪ p -` {length ls..<length (cols basis)}.
(col basis ia $ i) * (f (col basis ia)))"
by (metis (no_types, lifting) bot_nat_0.extremum ivl_disj_un_two(3) len_ls vimage_Un)
also have "… = (∑ia ∈ p -` {0..< length ls}. (col basis ia $ i) * (f (col basis ia))) +
(∑ia ∈ p -` {length ls..<length (cols basis)}. (col basis ia $ i) * (f (col basis ia)))"
proof (subst sum.union_disjoint, goal_cases)
case 1 then show ?case
by (metis (no_types, lifting) atLeast_upt len_ls lessThan_subset_iff p(1)
permutes_vimage set_upt subset_eq_atLeast0_lessThan_finite vimage_mono)
next
case 2 then show ?case
by (metis (no_types, lifting) atLeast0LessThan diff_is_0_eq' diff_le_self
finite_nat_iff_bounded ivl_subset length_map length_upt map_nth p(1) permutes_vimage
vimage_mono)
qed auto
also have "… = (∑ia ∈ {0..<length (cols basis')}.
(col basis' (ia) $ i) * (f (col basis' (ia))))"
proof -
have "(∑ia ∈ p -` {0..< length ls}. (col basis ia $ i) * (f (col basis ia))) =
(∑ia ∈ p -` {0..< length ls}. (ls ! (p ia) $ i) * (f (ls ! (p ia))))"
using in_ls by force
moreover have "… = (∑ia ∈ {0..< length ls}. (ls ! ia $ i) * (f (ls ! ia)))"
proof -
have inj: "inj_on p (p -` {0..<length ls})"
by (metis inj_onI p(1) permutes_def)
have "p ` p -` {0..<length ls} = {0..<length ls}"
by (metis p(1) permutes_def surj_def surj_image_vimage_eq)
then show ?thesis using sum.reindex[OF inj,of "(λj. ls ! j $ i * f (ls ! j))", symmetric]
unfolding comp_def by auto
qed
moreover have "… = 0" by (simp add: f_ls_0)
ultimately have "(∑ia ∈ p -` {0..< length ls}. (col basis ia $ i) * (f (col basis ia)))
= 0" by auto
moreover have "(∑ia ∈ p -` {length ls..<length (cols basis)}. (col basis ia $ i) *
(f (col basis ia))) =
(∑ia ∈ p -` {length ls..<length (cols basis)}. (col basis' (p ia -length ls) $ i) *
(f (col basis' (p ia -length ls))))"
proof -
have "(col basis ia $ i) * (f (col basis ia)) = (col basis' (p ia -length ls) $ i) *
(f (col basis' (p ia -length ls)))" if "ia ∈ p -` {length ls..<length (cols basis)}"
for ia using not_in_ls[OF that]
by (metis add_diff_cancel_left' atLeastLessThan_iff cols_length cols_nth diff_less_mono
length_append length_permute_list p(2) that vimageD)
then show ?thesis by simp
qed
moreover have "… = (∑ia ∈ {length ls..<length (cols basis)}. (col basis' (ia -length ls) $ i) *
(f (col basis' (ia -length ls))))"
proof -
have inj: "inj_on p (p -` {length ls..<length (cols basis)})"
by (metis inj_onI p(1) permutes_def)
have "p ` p -` {length ls..<length (cols basis)} = {length ls..<length (cols basis)}"
by (metis p(1) permutes_def surj_def surj_image_vimage_eq)
then show ?thesis using sum.reindex[OF inj,of "(λj. col basis' (j - length ls) $ i *
f (col basis' (j - length ls)))", symmetric]
unfolding comp_def by auto
qed
moreover have "… = (∑ia ∈ {length ls..<length ls + length (cols basis')}.
(col basis' (ia -length ls) $ i) * (f (col basis' (ia -length ls))))"
by (simp add: p(2))
moreover have "… = (∑ia ∈ {0..<length (cols basis')}.
(col basis' (ia) $ i) * (f (col basis' (ia))))"
proof -
have inj: "inj_on (λj. j-length ls) {length ls..<length ls + length (cols basis')}"
using inj_on_diff_nat by fastforce
have "x ∈ (λx. x - length ls) ` {length ls..<length ls + dim_col basis'}"
if "x < dim_col basis'" for x using that
by (metis add_diff_cancel_left' atLeastLessThan_iff image_eqI linorder_not_less
nat_add_left_cancel_less not_add_less1)
then have "(λj. j - length ls) ` {length ls..<length ls + length (cols basis')} =
{0..<length (cols basis')}"
by auto
then show ?thesis using sum.reindex[OF inj,
of "(λia. col basis' ia $ i * f (col basis' ia))", symmetric]
unfolding comp_def by auto
qed
ultimately show ?thesis by auto
qed
also have "… = (∑ia ∈ {0..<length (cols basis')}.
(basis' $$ (i, ia)) * (f (col basis' (ia))))"
using "1" dim_row dim_v by auto
also have "… = (∑ia ∈ {0..<length (cols basis')}.
(row basis' i $ ia) * (f (col basis' (ia))))"
using "1" dim_row dim_v by force
also have "… = (∑ia ∈ {0..<length (cols basis')}.
(row basis' i $ ia) * vec (dim_col basis') (λj. f (col basis' j)) $ ia)" by force
also have "… = (row basis' i) ∙ vec (dim_col basis') (λj. f (col basis' j))"
by (simp add: scalar_prod_def)
also have "… = vec (dim_vec v) (λi. (row basis' i) ∙
vec (dim_col basis') (λj. f (col basis' j))) $ i" by (simp add: "1")
also have "… = (basis' *⇩v vec (dim_col basis') (λj. f (col basis' j))) $ i"
unfolding mult_mat_vec_def using d dim_v by presburger
also have "… = v $ i" using f(2) by blast
finally have "?vec $ i = v $ i" by blast
then show ?case by auto
next
case (2)
then show ?case using dim_v by auto
qed (auto)
then show ?thesis unfolding mult_mat_vec_def scalar_prod_def by auto
qed
qed
text ‹The representation of the $i$-th column vector is the $i$-th unit vector.›
lemma representation_basis:
assumes basis: "is_indep basis" and b: "b ∈ set_cols basis"
shows "representation basis b = (λv. if v = b then 1 else 0)"
proof (rule unique_representation[OF basis])
show "representation basis b v ≠ 0 ⟹ v ∈ set_cols basis" for v
using representation_ne_zero .
show "(if v = b then 1 else 0) ≠ 0 ⟹ v ∈ set_cols basis" for v
using b by (cases "v = b") (auto simp: b)
have *: "{v. (if v = b then 1 else 0::int) ≠ 0} = {b}"
by auto
obtain j where j: "col basis j = b" "j<dim_col basis"
by (metis atLeastLessThan_iff b imageE set_cols_col)
have dis: "distinct (cols basis)" using basis is_indep_distinct by simp
have unit: "vec (dim_col basis) (λi. if col basis i = b then 1 else 0) =
unit_vec (dim_col basis) j" (is "?l = ?r")
proof (subst eq_vecI[of ?l ?r], goal_cases)
case (1 i)
then show ?case using dis j
by (smt (verit, best) cols_length cols_nth dim_vec distinct_conv_nth index_unit_vec(1)
index_vec)
qed auto
show "basis *⇩v vec (dim_col basis) (λi. Lattice_int.representation basis b (col basis i)) =
basis *⇩v vec (dim_col basis) (λi. if col basis i = b then 1 else 0)"
using * sum_nonzero_representation_eq[OF basis span_base[OF b]] unfolding unit
by (subst col_unit_vec, simp add: j, unfold j(1), simp)
qed
text ‹The spanning and independent set of vectors is a basis.›
lemma spanning_subset_independent:
assumes BA: "set_cols B ⊆ set_cols A" and iA: "is_indep (A::real mat)"
and AsB:"set_cols A ⊆ span B"
and d: "distinct (cols B)" and dr: "dim_row A = dim_row B"
shows "set_cols A = set_cols B"
proof (intro antisym[OF _ BA] subsetI)
have iB: "is_indep B" using is_indep_mono[OF BA iA d dr] .
fix v assume "v ∈ set_cols A"
with AsB have "v ∈ span B" by auto
let ?RB = "representation B v" and ?RA = "representation A v"
have "?RB v = 1"
unfolding representation_extend[OF iA ‹v ∈ span B› BA dr d, symmetric]
representation_basis[OF iA ‹v ∈ set_cols A›] by simp
then show "v ∈ set_cols B"
using representation_ne_zero[of B v v] by auto
qed
lemma nth_lin_combo:
assumes "i < dim_row A" "dim_col A = dim_vec b"
shows "(A *⇩v b) $ i = (∑j=0..<dim_col A. A $$ (i,j) * b $ j)"
using assms unfolding mult_mat_vec_def scalar_prod_def by auto
text ‹Insert and delete with the span.›
lemma dim_col_insert_col:
"dim_col (insert_col S a) = dim_col S + 1"
by (simp add: insert_col)
lemma dim_col_delete_col:
assumes "a ∈ set_cols S" "distinct (cols S)" "dim_vec a = dim_row S"
shows "dim_col (delete_col S a) = dim_col S - 1"
proof -
have *: "{x. x ≠ a} ∩ set (cols S) = set (cols S) - {a}" by fastforce
have "length (filter (λx. x ≠ a) (cols S)) = length (cols S) - 1"
unfolding distinct_length_filter[OF ‹distinct (cols S)›] *
by (metis assms(1) assms(2) card_Diff_singleton distinct_card set_cols)
then have "length (cols (delete_col S a)) = length (cols S) - 1"
unfolding delete_col by auto
then show ?thesis by (metis cols_length)
qed
lemma dim_row_delete_col:
"dim_row (delete_col T b) = dim_row T"
by (simp add: delete_col)
lemma span_insert1:
assumes "dim_vec (a :: 'a ::comm_ring vec) = dim_row S"
shows "span (insert_col S a) = {x. ∃k y. x = y + k ⋅⇩v a ∧ y ∈ span S ∧ dim_vec x = dim_row S}"
unfolding span_def proof (safe, goal_cases)
case (1 x z)
obtain za zs where z: "z = vCons za zs"
by (metis "1" add_Suc_right dim_vec insert_col list.size(4) mat_of_cols_carrier(3)
nat.simps(3) vec_cases)
have "dim_vec z = dim_col S + 1" using 1 by (simp add: insert_col)
then have *: "dim_vec zs = dim_col S" using z by auto
have "mat_of_cols (dim_row S) (a # cols S) *⇩v vCons za zs = S *⇩v zs + za ⋅⇩v a"
proof (subst mat_of_cols_cons_mat_vec, goal_cases one two three)
case one
then show ?case using * by (metis carrier_vec_dim_vec cols_length)
next
case three
then show ?case
by (simp add: assms comm_add_vec mult_mat_vec_def smult_vec_def)
qed (use assms in ‹auto›)
moreover have "S *⇩v zs ∈ span S" unfolding span_def using * by auto
moreover have "dim_vec (mat_of_cols (dim_row S) (a # cols S) *⇩v vCons za zs) =
dim_row S" by auto
ultimately show ?case unfolding z insert_col using "*" by blast
next
case (2 x k y z)
have "S *⇩v z + k ⋅⇩v a = mat_of_cols (dim_row S) (cols S) *⇩v z + k ⋅⇩v a" by simp
moreover have "mat_of_cols (dim_row S) (cols S) *⇩v z + k ⋅⇩v a =
mat_of_cols (dim_row S) (a # cols S) *⇩v (vCons k z)"
proof (subst mat_of_cols_cons_mat_vec, goal_cases one two three)
case one
then show ?case using 2
by (metis carrier_vec_dim_vec cols_length)
next
case three
then show ?case
by (simp add: assms comm_add_vec mult_mat_vec_def smult_vec_def)
qed (use assms in ‹auto›)
moreover have "dim_vec (vCons k z) = dim_col (insert_col S a)"
using 2 by (simp add: insert_col)
ultimately show ?case unfolding insert_col by auto
qed
lemma span_insert2:
assumes "dim_vec a = dim_row S"
shows "span (insert_col S (a :: 'a ::comm_ring vec)) =
{x. ∃k. (x - k ⋅⇩v a) ∈ span S ∧ dim_vec x = dim_row S}"
proof -
have "span (insert_col S a) = {x. ∃k y. x = y + k ⋅⇩v a ∧ y ∈ span S ∧ dim_vec x = dim_row S}"
using span_insert1[OF assms] by auto
moreover have "{x. ∃k y. x = y + k ⋅⇩v a ∧ y ∈ span S ∧ dim_vec x = dim_row S} =
{x. ∃k. x - k ⋅⇩v a ∈ Lattice_int.span S ∧ dim_vec x = dim_row S}"
proof (safe, goal_cases)
case (1 x k y)
then have i: "y + ((k ⋅⇩v a) - (k ⋅⇩v a)) ∈ Lattice_int.span S"
by (smt (verit, ccfv_SIG) Lattice_int.span_def assms dim_carrier mem_Collect_eq
minus_cancel_vec right_zero_vec smult_vec_def vec_carrier)
have rew: "y + ((k ⋅⇩v a) - (k ⋅⇩v a)) = (y + (k ⋅⇩v a)) - (k ⋅⇩v a) "
using assoc_add_vec[of y _ "k ⋅⇩v a" "- k ⋅⇩v a" ] by auto
show ?case using i unfolding rew using assms by auto
next
case (2 x k)
have "x = x + (k ⋅⇩v a - k ⋅⇩v a)" using "2"(2) assms by auto
then have "x = (x - k ⋅⇩v a) + k ⋅⇩v a"
using assoc_add_vec[of x _ "- k ⋅⇩v a" "k ⋅⇩v a" ]
using "2"(2) assms by auto
moreover have "(x - k ⋅⇩v a) ∈ Lattice_int.span S" using "2"(1) by blast
ultimately show ?case using 2 by auto
qed
ultimately show ?thesis by auto
qed
lemma insert_delete_span:
assumes "(a :: 'a ::comm_ring vec) ∈ set_cols A" "distinct (cols A)" "dim_vec a = dim_row A"
shows "span (insert_col (delete_col A a) a) = span (A)"
unfolding span_def
proof (safe, goal_cases)
case (1 x z)
define nr where "nr = dim_row A"
define nc where "nc = dim_col A"
obtain c where c: "mat_of_cols nr (a # cols (delete_col A a)) *⇩v z = A *⇩v c"
"dim_vec c = nc"
proof (subst helper3[where A = A and nr = nr and nc = nc and ss = "a # cols (delete_col A a)"
and v = z], goal_cases)
case 2
then show ?case using assms(2) unfolding delete_col
by (metis (mono_tags, lifting) cols_dim cols_mat_of_cols distinct.simps(2) distinct_filter
dual_order.trans filter_is_subset mem_Collect_eq set_filter)
next
case 3
then show ?case using assms(1)
by (metis (mono_tags, lifting) cols_dim cols_mat_of_cols delete_col filter_is_subset in_mono
set_ConsD set_cols subsetI)
next
case 4
then show ?case using 1
by (metis carrier_vecI insert_col mat_of_cols_carrier(3))
qed (auto simp add: nc_def nr_def)
then show ?case unfolding nr_def nc_def
by (metis delete_col insert_col mat_of_cols_carrier(2) mat_of_cols_cols nc_def nr_def)
next
case (2 x z)
define nr where "nr = dim_row A"
define nc where "nc = dim_col A"
have gr0: "dim_col A > 0" using assms(1)
by (metis atLeastLessThan_iff bot_nat_0.not_eq_extremum cols_def imageE less_nat_zero_code
list.set_map set_cols set_upt)
obtain c where c: "mat_of_cols nr (cols A) *⇩v z = insert_col (delete_col A a) a *⇩v c"
"dim_vec c = nc"
proof (subst helper3[where A = "insert_col (delete_col A a) a" and nr = nr and nc = nc
and ss = "cols A" and v = z], goal_cases)
case 1
have "dim_row (insert_col (delete_col A a) a) = dim_row A"
by (simp add: delete_col insert_col)
moreover have "dim_col (insert_col (delete_col A a) a) = dim_col A"
unfolding dim_col_insert_col dim_col_delete_col[OF assms] using gr0 by simp
ultimately show ?case unfolding nr_def nc_def by auto
next
case 3
show ?case using assms(1) unfolding insert_col delete_col
proof (subst cols_mat_of_cols, goal_cases)
case 1
have "a ∈ set (cols A) ⟹ a ∈ carrier_vec (dim_row A)"
using assms(3) carrier_vecI by blast
moreover have "x ∈ set (cols (delete_col A a)) ⟹ x ∈ carrier_vec (dim_row A)" for x
by (metis cols_dim delete_col mat_of_cols_carrier(2) subsetD)
ultimately show ?case
by (metis "1" cols_dim insert_subset list.set(2) mat_of_cols_carrier(2) nr_def set_cols)
next
case 2
then show ?case
by (smt (verit, best) cols_dim cols_mat_of_cols filter_set insert_iff list.set(2)
member_filter subsetI subset_trans)
qed
next
case 4
then show ?case using 2 by (metis carrier_vec_dim_vec cols_length)
qed (auto simp add: nc_def nr_def assms)
then show ?case unfolding nr_def nc_def
by (metis Suc_eq_plus1 Suc_pred' assms(1) assms(2) assms(3) dim_col_delete_col
dim_col_insert_col gr0 mat_of_cols_cols)
qed
text ‹Deleting a generating element.›
lemma span_breakdown:
assumes bS: "(b :: 'a :: comm_ring vec) ∈ set_cols S"
and aS: "a ∈ span S"
and b: "dim_vec b = dim_row S"
and d: "distinct (cols S)"
shows "∃k. a - k ⋅⇩v b ∈ span (delete_col S b)"
proof -
have r: "dim_vec b = dim_row (delete_col S b)"
by (simp add: b delete_col)
have s: "span (insert_col (delete_col S b) b) = span S"
by (subst insert_delete_span[OF bS d b], auto)
have "span S = {x. ∃k. x - k ⋅⇩v b ∈ Lattice_int.span (delete_col S b) ∧
dim_vec x = dim_row (delete_col S b)}"
using span_insert2 [of b "delete_col S b"] r unfolding s by auto
then show ?thesis using assms by auto
qed
lemma uminus_scalar_mult:
"(-k) ⋅⇩v a = - (k ⋅⇩v (a:: 'a ::comm_ring_1 vec))"
unfolding smult_vec_def
by (subst eq_vecI[of "vec (dim_vec a) (λi. - k * a $ i)" "- vec (dim_vec a) (λi. k * a $ i)"])
auto
lemma span_scale: "(x :: 'a ::field vec) ∈ span S ⟹ c ⋅⇩v x ∈ span S"
unfolding span_def
proof safe
fix z assume *: "dim_vec z = dim_col S" "x = S *⇩v z"
show "∃za. c ⋅⇩v (S *⇩v z) = S *⇩v za ∧ dim_vec za = dim_col S"
proof (intro exI[of _ "c ⋅⇩v z"], safe, goal_cases)
case 1
show ?case by (metis "*"(1) carrier_mat_triv carrier_vec_dim_vec mult_mat_vec)
next
case 2
show ?case by (simp add: "*"(1))
qed
qed
lemma span_diff:
assumes "(x :: 'a::ring vec) ∈ span S" "y ∈ span S"
"x ∈ carrier_vec (dim_row S)" "y ∈ carrier_vec (dim_row S)"
shows "x - y ∈ span S"
using assms unfolding span_def
proof (safe, goal_cases)
case (1 zx zy)
then have "zx ∈ carrier_vec (dim_col S)" "zy ∈ carrier_vec (dim_col S)"
by (metis carrier_vec_dim_vec)+
then have "S *⇩v zx - S *⇩v zy = S *⇩v (zx - zy)"
by (subst mult_minus_distrib_mat_vec[where A = S and v = zx and w = zy, symmetric], auto)
moreover have "dim_vec (zx-zy) = dim_col S" using 1 by auto
ultimately show ?case by auto
qed
text ‹Adding a generating element.›
lemma in_span_insert:
assumes a: "(a :: 'a ::field vec) ∈ span (insert_col S b)"
and na: "a ∉ span S"
and br: "dim_vec b = dim_row S"
and bnotS: "b ∉ set_cols S"
and d: "distinct (cols S)"
shows "b ∈ span (insert_col S a)"
using assms
proof -
define nr where "nr = dim_row S"
have carrier_a: "a ∈ carrier_vec nr"
using a br carrier_dim_vec nr_def span_insert2 by fastforce
have carrier_b: "b ∈ carrier_vec nr"
by (simp add: br carrier_vecI nr_def)
have bi: "b ∈ set_cols (insert_col S b)"
by (simp add: br carrier_dim_vec insert_col)
have br': "dim_vec b = dim_row (insert_col S b)" using br
by (simp add: insert_col)
have di: "distinct (cols (insert_col S b))" using d bnotS
by (metis br carrier_vec_dim_vec cols_dim cols_mat_of_cols distinct.simps(2) insert_col
insert_subset list.simps(15) set_cols)
from span_breakdown[of b "insert_col S b" a, OF bi a br' di]
obtain k where k: "a - k ⋅⇩v b ∈ span (delete_col S b)"
by (smt (verit, best) assms(1) bnotS br delete_col filter_True mat_of_cols_cols
mem_Collect_eq set_cols span_insert2)
have "k ≠ 0"
proof
assume "k = 0"
have s: "set_cols (delete_col S b) ⊆ set_cols S"
by (metis (no_types, lifting) cols_dim cols_mat_of_cols delete_col dual_order.trans
filter_is_subset set_cols)
have r: "dim_row (delete_col S b) = dim_row S" by (simp add: delete_col)
have dc: "distinct (cols (delete_col S b))"
by (metis cols_dim cols_mat_of_cols d delete_col distinct_filter dual_order.trans
filter_is_subset)
have "a = a - k ⋅⇩v b" using ‹k = 0›
using a br carrier_dim_vec span_insert2 by fastforce
then have "a ∈ Lattice_int.span (delete_col S b)" using k by auto
then have "a ∈ span S" using span_mono[of "delete_col S b" S, OF s r dc] by auto
with na show False by blast
qed
then have eq: "b = (1/k) ⋅⇩v a - (1/k) ⋅⇩v (a - k ⋅⇩v b)"
proof -
have carrier_kb: "- k ⋅⇩v b ∈ carrier_vec nr" using carrier_b by simp
have "1 / k ⋅⇩v (- k ⋅⇩v b) = -b" by (subst smult_smult_assoc, use ‹k≠0› in ‹auto›)
then have "(1/k) ⋅⇩v (a + (- k ⋅⇩v b)) = ((1/k) ⋅⇩v a - b)"
by (subst smult_add_distrib_vec[where a = "1/k" and v = a and w = "-k⋅⇩v b",
OF carrier_a carrier_kb], auto)
then have *: "(1/k) ⋅⇩v (a - k ⋅⇩v b) = ((1/k) ⋅⇩v a - b)" unfolding uminus_scalar_mult
by (metis carrier_a carrier_b minus_add_uminus_vec smult_carrier_vec)
have **: "(1/k) ⋅⇩v a - (1/k) ⋅⇩v (a - k ⋅⇩v b) = (1/k) ⋅⇩v a - (1/k) ⋅⇩v a + b" unfolding *
using carrier_a carrier_b by auto
then show ?thesis unfolding ** using carrier_a carrier_b by auto
qed
from k have k2: "(1/k) ⋅⇩v (a - k ⋅⇩v b) ∈ span (delete_col S b)"
by (rule span_scale)
have sub: "span (delete_col S b) ⊆ span (insert_col S a)"
proof (subst span_mono, goal_cases)
case 1
then show ?case
by (smt (verit, best) carrier_a cols_dim cols_mat_of_cols delete_col dual_order.refl
dual_order.trans filter_is_subset insert_col insert_subset list.set(2) nr_def set_cols)
next
case 2
then show ?case by (simp add: delete_col insert_col)
next
case 3
then show ?case by (metis cols_dim cols_mat_of_cols d delete_col distinct_filter
dual_order.trans filter_is_subset set_cols)
qed auto
then have "(1/k) ⋅⇩v (a - k ⋅⇩v b) ∈ span (insert_col S a)" using k2 sub by blast
moreover have "1 / k ⋅⇩v a ∈ span (insert_col S a)"
by (metis Lattice_int.span_base Lattice_int.span_scale carrier_a cols_dim cols_mat_of_cols
insertCI insert_col insert_subsetI list.set(2) nr_def set_cols)
ultimately show ?thesis by (subst eq)
(metis Lattice_int.span_diff br carrier_a carrier_vecD carrier_vec_dim_vec
index_minus_vec(2) index_smult_vec(2) insert_col mat_of_cols_carrier(2) nr_def)
qed
lemma delete_not_in_set_cols:
assumes "b ∉ set_cols T"
shows "delete_col T b = T"
unfolding delete_col using assms
by (metis (mono_tags, lifting) filter_True mat_of_cols_cols set_cols)
lemma delete_col_span:
assumes "(a :: 'a ::comm_ring vec) ∈ span (delete_col T b)" "distinct (cols T)"
shows "a ∈ span T"
using assms using span_mono[of "delete_col T b" T]
by (metis (no_types, lifting) cols_dim cols_mat_of_cols delete_col distinct_filter
dual_order.trans filter_is_subset in_mono mat_of_cols_carrier(2) set_cols)
text ‹Changing a generating element.›
lemma in_span_delete_field:
assumes aT:"(a :: 'a :: field vec) ∈ span T" and aTb: "a ∉ span (delete_col T b)"
and dr: "dim_vec b = dim_row T" and d:"distinct (cols T)"
shows "b ∈ span (insert_col (delete_col T b) a)"
proof (subst in_span_insert[of a "delete_col T b" b], goal_cases)
case 1
then show ?case proof (cases "b∈set_cols T")
case True
show ?thesis using aT insert_delete_span[OF True d dr] by (simp)
next
case False
then show ?thesis by (metis assms(1) assms(2) delete_not_in_set_cols)
qed
case 4
then show ?case
by (smt (verit) cols_dim cols_mat_of_cols delete_col dual_order.trans filter_is_subset
filter_set member_filter set_cols)
next
case 5
then show ?case
by (metis cols_dim cols_mat_of_cols d delete_col distinct_filter dual_order.trans
filter_is_subset)
qed (use assms in ‹auto simp add: dim_row_delete_col›)
text ‹Simplifications on multiplication.›
lemma mat_of_cols_mult_vCons:
assumes "dim_vec (x :: 'a ::comm_ring vec) = dim_row S" "dim_vec zs = dim_col S"
shows "mat_of_cols (dim_row S) (x # cols S) *⇩v vCons z0 zs = z0 ⋅⇩v x + S *⇩v zs"
using assms carrier_vec_dim_vec[of zs]
unfolding assms(2) by (subst mat_of_cols_cons_mat_vec, auto)
lemma mult_mat_vec_ring:
assumes m: "(A::'a::comm_ring mat) ∈ carrier_mat nr nc" and v: "v ∈ carrier_vec nc"
shows "A *⇩v (k ⋅⇩v v) = k ⋅⇩v (A *⇩v v)" (is "?l = ?r")
proof
have nr: "dim_vec ?l = nr" using m v by auto
also have "... = dim_vec ?r" using m v by auto
finally show "dim_vec ?l = dim_vec ?r".
show "⋀i. i < dim_vec ?r ⟹ ?l $ i = ?r $ i"
proof -
fix i assume "i < dim_vec ?r"
hence i: "i < dim_row A" using nr m by auto
hence i2: "i < dim_vec (A *⇩v v)" using m by auto
show "?l $ i = ?r $ i"
apply (subst (1) mult_mat_vec_def)
apply (subst (2) smult_vec_def)
unfolding index_vec[OF i] index_vec[OF i2]
unfolding mult_mat_vec_def smult_vec_def
unfolding scalar_prod_def index_vec[OF i]
by (simp add: mult.left_commute sum_distrib_left)
qed
qed
text ‹Adding a span element to the generating set does not change the span.›
lemma span_redundant:
assumes "(x :: 'a ::comm_ring vec) ∈ span S"
shows "span (insert_col S x) = span S"
proof
have "∃za. insert_col S x *⇩v z = S *⇩v za ∧ dim_vec za = dim_col S"
if "dim_vec z = dim_col (insert_col S x)" for z
proof -
have dim_z: "dim_vec z = dim_col S + 1" using that by (simp add: insert_col)
obtain za where za_def: "z = vCons (z$0) za"
by (metis ‹dim_vec z = dim_col (insert_col S x)› add_Suc_right dim_vec insert_col list.size(4)
mat_of_cols_carrier(3) nat.simps(3) vec_cases vec_index_vCons_0)
obtain zx where zx_def: "x = S *⇩v zx" "dim_col S = dim_vec zx"
using assms unfolding span_def by auto
have "dim_vec x = dim_row S" using zx_def(1) by auto
moreover have "dim_vec za = dim_col S"
by (metis Suc_eq_plus1_left add.commute add_diff_cancel_left' dim_vec_vCons dim_z za_def)
ultimately have "insert_col S x *⇩v z = z$0 ⋅⇩v x + S *⇩v za"
unfolding insert_col by (subst za_def, subst mat_of_cols_mult_vCons, auto)
also have "… = z$0 ⋅⇩v (S *⇩v zx) + S *⇩v za" unfolding zx_def by auto
also have "… = S *⇩v (z $ 0 ⋅⇩v zx) + S *⇩v za"
by (subst mult_mat_vec_ring[symmetric]) (auto simp add: zx_def(2))
also have "… = S *⇩v (z$0 ⋅⇩v zx + za)"
by (metis ‹dim_vec za = dim_col S› carrier_matI carrier_vec_dim_vec index_smult_vec(2)
mult_add_distrib_mat_vec zx_def(2))
finally have "insert_col S x *⇩v z = S *⇩v (z$0 ⋅⇩v zx + za)" by blast
moreover have "dim_vec (z$0 ⋅⇩v zx + za) = dim_col S"
by (metis Suc_eq_plus1_left add.commute add_diff_cancel_left' dim_vec_vCons dim_z
index_add_vec(2) za_def)
ultimately show ?thesis by blast
qed
then show "span (insert_col S x) ⊆ span S" unfolding span_def by auto
next
have "∃za. S *⇩v z = insert_col S x *⇩v za ∧
dim_vec za = dim_col (insert_col S x)" if "dim_vec z = dim_col S" for z
proof -
define za where za_def: "za = vCons 0 z"
have "dim_vec za = dim_col S + 1" using that za_def by force
then have "dim_vec za = dim_col (insert_col S x)"
by (simp add: insert_col)
moreover have "S *⇩v z = insert_col S x *⇩v za"
proof -
have "dim_vec x = dim_row S"
using Lattice_int.span_def assms by force
moreover have "dim_vec z = dim_col S"
using that by blast
moreover have "S *⇩v z = 0 ⋅⇩v x + S *⇩v z"
using calculation(1) by auto
ultimately show ?thesis unfolding insert_col za_def
by (subst mat_of_cols_mult_vCons)
qed
ultimately show ?thesis by blast
qed
then show "span S ⊆ span (insert_col S x)" unfolding span_def by auto
qed
text ‹Transitivity of inserting elements.›
lemma span_trans:
assumes "(x :: 'a ::comm_ring vec) ∈ span S" "y ∈ span (insert_col S x)"
shows "y ∈ span S"
using Lattice_int.span_redundant assms by blast
text ‹More on inserting, deleting and the set of columns.›
lemma delet_col_not_in_set_cols:
assumes "dim_vec b = dim_row T"
shows "b ∉ set_cols (delete_col T b)"
unfolding delete_col
by (metis (mono_tags, lifting) cols_dim cols_mat_of_cols dual_order.trans filter_is_subset
filter_set member_filter set_cols)
lemma dim_col_distinct:
assumes "distinct (cols S)"
shows "card (set_cols S) = dim_col S"
by (simp add: assms distinct_card)
lemma set_cols_mono:
assumes "set_cols S ⊆ set_cols T" "distinct (cols S)" "distinct (cols T)"
shows "dim_col S ≤ dim_col T"
using assms
by (metis List.finite_set card_mono dim_col_distinct set_cols)
lemma set_cols_insert_col:
assumes "dim_vec b = dim_row U"
shows "set_cols (insert_col U b) = set_cols U ∪ {b}"
by (metis (no_types, opaque_lifting) Un_commute Un_insert_right assms carrier_vec_dim_vec
cols_dim cols_mat_of_cols insert_col insert_subset list.set(2) set_cols sup_bot.left_neutral)
lemma set_cols_real_of_int_mat:
"set_cols (real_of_int_mat S) = real_of_int_vec ` (set_cols S)"
unfolding set_cols using real_of_int_mat_cols by auto
lemma real_of_int_mat_span:
"real_of_int_vec ` (span S) ⊆ span (real_of_int_mat S)"
by (smt (verit, ccfv_SIG) Lattice_int.span_def carrier_mat_triv carrier_vec_dim_vec
image_subset_iff index_map_mat(3) index_map_vec(2) mem_Collect_eq of_int_hom.mult_mat_vec_hom
real_of_int_mat_def real_of_int_vec_def)
lemma real_of_int_vec_ex:
assumes "x ∈ real_of_int_vec ` A"
shows "∃y. x = real_of_int_vec y"
using assms by blast
lemma real_of_int_vec_obtain:
assumes "x ∈ real_of_int_vec ` A"
obtains y where "x = real_of_int_vec y"
using assms by blast
lemma real_of_int_vec_inj:
"inj real_of_int_vec"
unfolding real_of_int_vec_def
by (simp add: injI of_int_hom.vec_hom_inj)
lemma real_of_int_mat_mat_of_cols:
assumes "∀i<length cs. cs ! i ∈ carrier_vec nr"
shows "real_of_int_mat (mat_of_cols nr cs) = mat_of_cols nr (map real_of_int_vec cs)"
proof-
have "real_of_int (cs ! j $ i) = map real_of_int_vec cs ! j $ i" if "j<length cs" "i<nr"
for i j unfolding nth_map[OF that(1)] proof (subst real_of_int_vec_nth)
have "dim_vec (cs ! j) = nr" using assms that(1)
using carrier_vecD by blast
then show "i < dim_vec (cs ! j)" using that(2) by auto
qed (auto)
then show ?thesis unfolding mat_of_cols_def by (subst real_of_int_mat_mat,
unfold o_def case_prod_beta, subst cong_mat, auto)
qed
lemma real_of_int_mat_delete_col:
"delete_col (real_of_int_mat T) (real_of_int_vec b) = real_of_int_mat (delete_col T b)"
unfolding delete_col
proof (subst real_of_int_mat_mat_of_cols, goal_cases)
case 1 show ?case by (meson cols_dim filter_is_subset nth_mem subset_iff)
next
case 2
have "(real_of_int_vec x ≠ real_of_int_vec b) = (x ≠ b)" for x
by (simp add: inj_eq real_of_int_vec_inj)
then have *:"filter (λx. x ≠ real_of_int_vec b) (cols (real_of_int_mat T)) =
map real_of_int_vec (filter (λx. x ≠ b) (cols T))"
unfolding real_of_int_mat_cols filter_map comp_def by auto
show ?case using cong1[OF *] by auto
qed
text ‹Lemma to exchange a subset of columns from one basis to another.
Pay attention that this only works over the reals, not over the integers
since we need to do divisions.
The ‹exchange_lemma› was adapted from ``HOL/Vector\_Spaces.thy''.
Note that the connection ``Jordan\_Normal\_Form/VS\_Connect'' between the type
‹('a,'k::finite) vec› and ‹'a vec› does not include the theorem ‹exchange_lemma›.
due to some problems in lifting/transfer.›
lemma exchange_lemma:
assumes i: "is_indep (S::real mat)"
and sp: "set_cols S ⊆ span T"
and d: "distinct (cols T)"
and dr: "dim_row S = dim_row T"
shows "∃t'. dim_col t' = dim_col T ∧ set_cols S ⊆ set_cols t' ∧
set_cols t' ⊆ set_cols S ∪ set_cols T ∧
distinct (cols t')"
using i sp d dr
proof (induct "card (set_cols T - set_cols S)" arbitrary: S T rule: less_induct)
case less
define nr where "nr = dim_row S"
have "nr = dim_row T" using less.prems(4) nr_def by blast
have "nr = dim_row S" by (simp add: nr_def)
have "nr = dim_row T" by (simp add: ‹nr = dim_row T›)
have sp': "set_cols (S) ⊆ span (T)" using less.prems(2)
unfolding set_cols_real_of_int_mat using real_of_int_mat_span by (auto)
have d': "distinct (cols (T))"
using distinct_cols_real_of_int_mat less.prems(3) by blast
have dr': "dim_row (S) = dim_row (T)" by (simp add: less.prems(4))
have ft: "finite (set_cols T)" by auto
note S = ‹is_indep S›
let ?P = "λt'. dim_col t' = dim_col T ∧ set_cols S ⊆ set_cols t' ∧
set_cols t' ⊆ set_cols S ∪ set_cols T ∧ distinct (cols t')"
show ?case
proof (cases "set_cols S ⊆ set_cols T ∨ set_cols T ⊆ set_cols S")
case True
then show ?thesis
proof
assume "set_cols S ⊆ set_cols T"
then have "set_cols S ⊆ set_cols T"
using set_cols_real_of_int_mat by auto
then show ?thesis using d' by blast
next
assume s: "set_cols T ⊆ set_cols S"
then show ?thesis
using spanning_subset_independent[OF s S _ less.prems(3) less.prems(4)]
using less.prems by (metis d' inf_sup_ord(3))
qed
next
case False
then have st: "¬ set_cols S ⊆ set_cols T" "¬ set_cols T ⊆ set_cols S"
by auto
from st(2) obtain b where b: "b ∈ set_cols T" "b ∉ set_cols S"
by blast
have "nr = dim_vec b"
by (metis ‹nr = dim_row T› b(1) carrier_vecD cols_dim set_cols subset_eq)
from b have "set_cols T - {b} - (set_cols S) ⊂ set_cols T - set_cols S"
by blast
then have cardlt: "card (set_cols T - {b} - set_cols S) < card (set_cols T - set_cols S)"
using ft by (auto intro: psubset_card_mono)
from b ft have ct0: "card (set_cols T) ≠ 0"
by auto
let ?T_b = "delete_col T b"
have "nr = dim_row ?T_b" by (simp add: ‹nr = dim_row T› dim_row_delete_col)
from ft have ftb: "finite (set_cols ?T_b)"
by auto
have dim_col_T_gr_0: "dim_col T > 0" using b(1)
by (metis atLeastLessThan_iff bot_nat_0.not_eq_extremum cols_def imageE list.set_map
set_cols set_upt zero_order(3))
have dim_col_T_b: "dim_col ?T_b = dim_col T - 1"
proof -
have "length (cols T) > 0" using dim_col_T_gr_0 unfolding cols_length by auto
have "length (filter (λx. x = b) (cols T)) = 1"
proof -
have "length (filter (λx. x = b) (cols T)) =
card {i. i < dim_col T ∧ col T i = b}"
unfolding length_filter_conv_card using cols_nth by (metis cols_length)
then show ?thesis using d' ‹b ∈ set_cols T›
by (smt (verit, del_insts) Collect_cong List.finite_set One_nat_def card.empty
card.insert distinct_card distinct_filter equals0D list.set(1) set_cols set_filter
singleton_conv)
qed
then have "length (filter (λx. x ≠ b) (cols T)) = length (cols T) - 1"
using sum_length_filter_compl by (metis add_diff_cancel_left')
then show ?thesis unfolding delete_col by auto
qed
have "dim_vec b = dim_row T"
using b(1) carrier_dim_vec cols_dim set_cols by blast
have set_cols_T_b: "set_cols ?T_b = set_cols T - {b}"
proof -
have "set_cols ?T_b ⊆ set_cols T"
by (smt (verit) cols_dim cols_mat_of_cols delete_col filter_is_subset order_trans set_cols)
moreover have "b ∉ set_cols ?T_b" using ‹dim_vec b = dim_row T›
by (subst delet_col_not_in_set_cols, auto)
ultimately show ?thesis
by (smt (verit, del_insts) Diff_subset cols_dim cols_mat_of_cols delete_col dual_order.trans
set_cols set_minus_filter_out)
qed
show ?thesis
proof (cases "set_cols S ⊆ span ?T_b")
case True
from cardlt have cardlt': "card (set_cols ?T_b - set_cols S) <
card (set_cols T - set_cols S)"
using set_cols_T_b by presburger
have d_delete: "distinct (cols (delete_col T b))" using d
by (metis b(1) card_Diff_singleton card_distinct cols_length d' dim_col_T_b dim_col_distinct
set_cols set_cols_T_b)
have dim_row_STb: "dim_row S = dim_row (delete_col T b)"
by (simp add: dim_row_delete_col less.prems(4))
obtain U where U: "dim_col U = dim_col ?T_b" "set_cols S ⊆ set_cols U"
"set_cols U ⊆ set_cols S ∪ set_cols ?T_b" "distinct (cols U)"
using less(1)[OF cardlt' S True d_delete dim_row_STb] by auto
have "nr = dim_row U" using U(2) unfolding ‹nr = dim_row S›
by (smt (verit, best) carrier_vecD cols_dim image_subset_iff set_cols
set_cols_real_of_int_mat st(1) subsetD subsetI)
let ?w = "insert_col U b"
have dim_col_w: "dim_col ?w = dim_col U + 1" unfolding insert_col by simp
have "dim_vec b = dim_row U" unfolding ‹nr = dim_vec b›[symmetric]
using ‹nr = dim_row U› .
then have set_cols_w: "set_cols ?w = set_cols U ∪ {b}"
by (subst set_cols_insert_col, auto)
have th0: "set_cols S ⊆ set_cols ?w"
using U(2) set_cols_w by auto
have th1: "set_cols ?w ⊆ set_cols S ∪ set_cols T"
using U b set_cols_w set_cols_T_b by auto
have bu: "b ∉ set_cols U"
using b U
by (metis DiffD2 Un_iff insertCI set_cols_T_b sup.orderE)
from U(1) have "dim_col U = dim_col T - 1"
using dim_col_T_b by presburger
then have th2: "dim_col (?w) = dim_col T" unfolding dim_col_w
using dim_col_T_gr_0 by linarith
have th3: "distinct (cols ?w)"
proof -
have "b ∉ set_cols U" using bu by blast
then show ?thesis
by (metis List.finite_set Suc_pred' U(4) ‹dim_col U = dim_col T - 1› card_distinct
card_insert_disjoint cols_length dim_col_T_gr_0 dim_col_distinct insert_union set_cols
set_cols_w th2)
qed
from th0 th1 th2 th3 have th: "?P ?w" by blast
from th show ?thesis by blast
next
case False
then obtain a where a: "a ∈ set_cols S" "a ∉ span ?T_b" by blast
have ab: "a ≠ b" using a b by blast
have at: "a ∉ set_cols T" using a ab span_base[of a "?T_b"]
by (metis DiffI empty_iff insert_iff set_cols_T_b)
let ?insert_a = "insert_col ?T_b a"
have set_cols_insert: "set_cols ?insert_a = {a} ∪ set_cols ?T_b"
by (smt (verit, ccfv_SIG) Lattice_int.span_def Un_commute a(1) delete_col dim_mult_mat_vec
less.prems(2) mat_of_cols_carrier(2) mem_Collect_eq set_cols_insert_col subsetD)
have dim_col_insert_a: "dim_col (?insert_a) = dim_col T"
by (metis One_nat_def Suc_eq_plus1_left Suc_pred' add.commute cols_length dim_col_T_b
dim_col_T_gr_0 insert_col list.size(4) mat_of_cols_carrier(3))
have mlt: "card (set_cols ?insert_a - set_cols S) < card (set_cols T - set_cols S)"
using cardlt a b by (metis insert_Diff1 insert_is_Un set_cols_T_b set_cols_insert)
have sp': "set_cols S ⊆ span (?insert_a)"
proof
fix x
assume xs: "x ∈ set_cols S"
let ?insert_b = "mat_of_cols (dim_row T) (b # cols ?insert_a)"
have T: "set_cols T ⊆ set_cols ?insert_b"
using b
by (smt (verit, ccfv_SIG) cols_dim cols_mat_of_cols delete_col dual_order.refl
insert_Diff insert_col insert_is_Un insert_subset list.set(2) mat_of_cols_carrier(2)
set_cols set_cols_T_b set_cols_insert)
have bs: "b ∈ span (?insert_a)"
using in_span_delete_field
by (metis ‹dim_vec b = dim_row T› a(1) a(2) d' in_mono sp')
from xs sp have "x ∈ span T" using less.prems(2) by blast
with span_mono[OF T] have x: "x ∈ span (?insert_b)"
using less.prems(3) by auto
from span_trans show "x ∈ span (?insert_a)"
by (metis bs delete_col insert_col mat_of_cols_carrier(2) x)
qed
from less(1)[OF mlt S sp'] obtain U where U:
"dim_col U = dim_col (insert_col (?T_b) a)"
"set_cols S ⊆ set_cols U" "set_cols U ⊆ set_cols S ∪ set_cols (insert_col (?T_b) a)"
"distinct (cols U)"
by (metis Lattice_int.span_base ‹dim_vec b = dim_row T› a(2) b(1) card_distinct
card_insert_disjoint cols_length delet_col_not_in_set_cols delete_col dim_col_distinct
dim_col_insert_a ftb insert_Diff insert_col insert_is_Un less.prems(3) less.prems(4)
mat_of_cols_carrier(2) set_cols set_cols_T_b set_cols_insert)
from U a b ft at ct0 have "?P U"
using dim_col_insert_a set_cols_T_b set_cols_insert by auto
then show ?thesis by blast
qed
qed
qed
text ‹A linearly independent set has smaller or equal cardinality than the span it lies in.›
lemma independent_span_bound:
assumes i: "is_indep (S :: int mat)" and d: "distinct (cols T)"
and sp: "set_cols S ⊆ span T"
and dr: "dim_row S = dim_row T"
shows "dim_col S ≤ dim_col T"
proof -
have i': "is_indep (real_of_int_mat S)" using i unfolding is_indep_real_def is_indep_int_def
by auto
have sp': "set_cols (real_of_int_mat S) ⊆ Lattice_int.span (real_of_int_mat T)"
using sp by (metis image_mono real_of_int_mat_span set_cols_real_of_int_mat subset_trans)
have d': "distinct (cols (real_of_int_mat T))" using d
by (simp add: distinct_cols_real_of_int_mat)
have dr': "dim_row (real_of_int_mat S) = dim_row (real_of_int_mat T)" using dr
by (simp add: distinct_cols_real_of_int_mat)
obtain t' where t: "dim_col t' = dim_col (real_of_int_mat T)"
"set_cols (real_of_int_mat S) ⊆ set_cols t'"
"set_cols t' ⊆ set_cols (real_of_int_mat S) ∪ set_cols (real_of_int_mat T)"
"distinct (cols t')"
using exchange_lemma[OF i' sp' d' dr'] by blast
have dS: "distinct (cols (real_of_int_mat S))" using is_indep_distinct[OF i']
using distinct_cols_real_of_int_mat by blast
have "dim_col S = dim_col (real_of_int_mat S)" by simp
moreover have "dim_col (real_of_int_mat S) ≤ dim_col t'"
using set_cols_mono[OF t(2) dS t(4)] by auto
moreover have "dim_col t' = dim_col T" unfolding t(1) by simp
ultimately show ?thesis by auto
qed
text ‹When two bases $B$ and $B'$ generate the same lattice, both have the same
length because the change of basis theorem allows us to convert one basis in the other.›
lemma gen_lattice_in_span:
assumes "gen_lattice B = gen_lattice B'"
shows "set_cols B ⊆ Lattice_int.span B'"
unfolding gen_lattice_def
by (smt (verit, ccfv_SIG) Lattice_int.span_base Lattice_int.span_def assms gen_lattice_def subsetI)
lemma basis_exchange:
assumes gen_eq: "gen_lattice B = gen_lattice B'"
and "is_indep B" and "is_indep B'"
shows "dim_col B = dim_col B'"
proof -
have i:"is_indep (real_of_int_mat B)" "is_indep (real_of_int_mat B')"
using assms unfolding is_indep_real_def is_indep_int_def by auto
have dr: "dim_row B = dim_row B'"
by (smt (z3) dim_mult_mat_vec gen_eq gen_lattice_def index_zero_vec(2) mem_Collect_eq)
have "dim_col B ≤ dim_col B'"
using assms(2) is_indep_distinct[OF i(2)] gen_lattice_in_span[OF assms(1)] dr
Lattice_int.independent_span_bound distinct_cols_real_of_int_mat by presburger
moreover have "dim_col B' ≤ dim_col B"
using assms(3) is_indep_distinct[OF i(1)] gen_lattice_in_span[OF assms(1)[symmetric]] dr
Lattice_int.independent_span_bound distinct_cols_real_of_int_mat by presburger
ultimately show ?thesis by linarith
qed
text ‹Basis matrix of a lattice›
definition basis_of :: "int vec set ⇒ int mat" where
"basis_of L = (SOME B. L = gen_lattice B ∧ is_indep B)"
definition dim_lattice :: "int_lattice ⇒ nat" where
"dim_lattice L = (THE x. x = dim_col (basis_of L))"
lemma dim_lattice_gen_lattice:
assumes "is_indep B"
shows "dim_lattice (gen_lattice B) = dim_col B"
unfolding dim_lattice_def using assms basis_exchange[of "basis_of (gen_lattice B)" B]
by (auto simp add: basis_of_def)
(metis (mono_tags, lifting) tfl_some)
text ‹A lattice generated by a linearly independent matrix is indeed a lattice.›
lemma is_lattice_gen_lattice:
assumes "is_indep A"
shows "is_lattice (gen_lattice A)"
unfolding is_lattice_def gen_lattice_def using assms by auto
end