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 = 0v (dim_row A)  
    dim_vec z = dim_col A)  z = 0v (dim_vec z))"
definition is_indep_int :: "int mat  bool" where
  "is_indep A = (z::real vec. ((real_of_int_mat A) *v z = 0v (dim_row A)  
    dim_vec z = dim_col A)  z = 0v (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  0v (dim_row B)"
proof (rule ccontr)
  assume "¬ (col B i  0v (dim_row B))"
  then have "col B i = 0v (dim_row B)" by auto
  then have "B *v (unit_vec (dim_col B) i) = 0v (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)  0v (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 (0v (length ?ls) @v z))"
  have z: "z  carrier_vec (length ss)" unfolding ss_def using 1 
  using carrier_dim_vec by auto
  have "0v 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) = 0v nr" 
  by presburger
  then have zero: "vec_of_list (permute_list f ?cs1) = 0v 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 = 0v (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) = 0v 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)  0v 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  "vset_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) = 0v (dim_row basis)" using eq by auto
    moreover have "dim_vec ?x = dim_col basis" 
    using dim_vec by blast
    moreover have "?x  0v (dim_col basis)" using ex
    by (metis (no_types, lifting) index_vec index_zero_vec(1)) 
    ultimately show "x. (basis *v x = 0v (dim_row basis) 
         dim_vec x = dim_col basis)  x  0v (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 xset 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' vspan 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 k0 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 = "-kv 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 "bset_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