Theory Jordan_Normal_Form.VS_Connect

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
(* with contributions from Alexander Bentkamp, Universität des Saarlandes *)

section ‹Matrices as Vector Spaces›

text ‹This theory connects the Matrix theory with the VectorSpace theory of
  Holden Lee. As a consequence notions like span, basis, linear dependence, etc. 
  are available for vectors and matrices of the Matrix-theory.›

theory VS_Connect
imports 
  Matrix
  Missing_VectorSpace
  Determinant
begin

hide_const (open) Multiset.mult
hide_const (open) Polynomial.smult
hide_const (open) Modules.module
hide_const (open) subspace
hide_fact (open) subspace_def

named_theorems class_ring_simps

abbreviation class_ring :: "'a :: {times,plus,one,zero} ring" where
  "class_ring ≡ ⦇ carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+) ⦈"

interpretation class_semiring: semiring "class_ring :: 'a :: semiring_1 ring"
  rewrites [class_ring_simps]: "carrier class_ring = UNIV"
    and [class_ring_simps]: "mult class_ring = (*)"
    and [class_ring_simps]: "add class_ring = (+)"
    and [class_ring_simps]: "one class_ring = 1"
    and [class_ring_simps]: "zero class_ring = 0"
    and [class_ring_simps]: "pow (class_ring :: 'a ring) = (^)"
    and [class_ring_simps]: "finsum (class_ring :: 'a ring) = sum"
proof -
  let ?r = "class_ring :: 'a ring"
  show "semiring ?r"
    by (unfold_locales, auto simp: field_simps)
  then interpret semiring ?r .
  {
    fix x y
    have "x [^]⇘?r⇙ y = x ^ y"
      by (induct y, auto simp: power_commutes)
  }
  thus "([^]⇘?r⇙) = (^)" by (intro ext)
  {
    fix f and A :: "'b set"
    have "finsum ?r f A = sum f A"
      by (induct A rule: infinite_finite_induct, auto)
  }
  thus "finsum ?r = sum" by (intro ext)
qed auto 

interpretation class_ring: ring "class_ring :: 'a :: ring_1 ring"
  rewrites "carrier class_ring = UNIV"
    and "mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and [class_ring_simps]: "a_inv (class_ring :: 'a ring) = uminus"
    and [class_ring_simps]: "a_minus (class_ring :: 'a ring) = minus"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum"
proof -
  let ?r = "class_ring :: 'a ring"
  interpret semiring ?r ..
  show "finsum ?r = sum" "pow ?r = (^)" by (simp_all add: class_ring_simps)
  {
    fix x :: 'a
    have "∃y. x + y = 0" by (rule exI[of _ "-x"], auto)
  } note [simp] = this
  show "ring ?r"
    by (unfold_locales, auto simp: field_simps Units_def)
  then interpret ring ?r .
  {
    fix x :: 'a
    have "⊖⇘?r⇙ x = - x" unfolding a_inv_def m_inv_def
      by (rule the1_equality, rule ex1I[of _ "- x"], auto simp: minus_unique)
  } note ainv = this
  thus inv: "a_inv ?r = uminus" by (intro ext)
  {
    fix x y :: 'a
    have "x ⊖⇘?r⇙ y = x - y"
      apply (subst a_minus_def)
      using inv by auto
  }
  thus "(λx y. x ⊖⇘?r⇙ y) = minus" by (intro ext)
qed (auto simp: class_ring_simps)

interpretation class_cring: cring "class_ring :: 'a :: comm_ring_1 ring"
  rewrites "carrier class_ring = UNIV"
    and "mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and "a_inv (class_ring :: 'a ring) = uminus"
    and "a_minus (class_ring :: 'a ring) = minus"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum"
    and [class_ring_simps]: "finprod class_ring = prod"
proof -
  let ?r = "class_ring :: 'a ring"
  interpret ring ?r ..
  show "cring ?r"
    by (unfold_locales, auto)
  then interpret cring ?r .
  show "a_inv (class_ring :: 'a ring) = uminus"
    and "a_minus (class_ring :: 'a ring) = minus"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum" by (simp_all add: class_ring_simps)
  {
    fix f and A :: "'b set"
    have "finprod ?r f A = prod f A"
      by (induct A rule: infinite_finite_induct, auto)
  }
  thus "finprod ?r = prod" by (intro ext)
qed (auto simp: class_ring_simps)

definition div0 :: "'a :: {one,plus,times,zero}" where
  "div0 ≡ m_inv (class_ring :: 'a ring) 0"

lemma class_field: "field (class_ring :: 'a :: field ring)" (is "field ?r")
proof -
  interpret cring ?r ..
  {
    fix x :: 'a
    have "x ≠ 0 ⟹ ∃xa. xa * x = 1 ∧ x * xa = 1"
      by (intro exI[of _ "inverse x"], auto)
  } note [simp] = this
  show "field ?r" 
    by (unfold_locales, auto simp: Units_def)
qed

interpretation class_field: field "class_ring :: 'a :: field ring"
  rewrites "carrier class_ring = UNIV"
    and "mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and "a_inv class_ring = uminus"
    and "a_minus class_ring = minus"
    and "pow class_ring = (^)"
    and "finsum class_ring = sum"
    and "finprod class_ring = prod"
    and [class_ring_simps]: "m_inv (class_ring :: 'a ring) x = 
      (if x = 0 then div0 else inverse x)" 
    (* problem that m_inv ?r 0 = inverse 0 is not guaranteed  *)
proof -
  let ?r = "class_ring :: 'a ring"
  show "field ?r" using class_field.
  then interpret field ?r.
  show "a_inv ?r = uminus"
    and "a_minus ?r = minus"
    and "pow ?r = (^)"
    and "finsum ?r = sum"
    and "finprod ?r = prod" by (fact class_ring_simps)+
  show "inv⇘?r⇙ x = (if x = 0 then div0 else inverse x)"
  proof (cases "x = 0")
    case True
    thus ?thesis unfolding div0_def by simp
  next
    case False
    thus ?thesis unfolding m_inv_def
      by (intro the1_equality ex1I[of _ "inverse x"], auto simp: inverse_unique)
  qed
qed (auto simp: class_ring_simps)

lemmas matrix_vs_simps = module_mat_simps class_ring_simps

definition class_field :: "'a :: field ring"
  where [class_ring_simps]: "class_field ≡ class_ring"




locale matrix_ring = 
  fixes n :: nat
    and field_type :: "'a :: field itself"
begin
abbreviation R where "R ≡ ring_mat TYPE('a) n n"
sublocale ring R
  rewrites "carrier R = carrier_mat n n"
    and "add R = (+)"
    and "mult R = (*)"
    and "one R = 1⇩m n"
    and "zero R = 0⇩m n n"
  using ring_mat by (auto simp: ring_mat_simps)

end

lemma matrix_vs: "vectorspace (class_ring :: 'a :: field ring) (module_mat TYPE('a) nr nc)"
proof -
  interpret abelian_group "module_mat TYPE('a) nr nc"
    by (rule abelian_group_mat)
  show ?thesis unfolding class_field_def
    by (unfold_locales, unfold matrix_vs_simps, 
      auto simp: add_smult_distrib_left_mat add_smult_distrib_right_mat)
qed


locale vec_module =
  fixes f_ty::"'a::comm_ring_1 itself"
  and n::"nat"
begin

abbreviation V where "V ≡ module_vec TYPE('a) n"

sublocale Module.module "class_ring :: 'a ring" V
  rewrites "carrier V = carrier_vec n"
    and "add V = (+)"
    and "zero V = 0⇩v n"
    and "module.smult V = (⋅⇩v)"
    and "carrier class_ring = UNIV"
    and "monoid.mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and "a_inv (class_ring :: 'a ring) = uminus"
    and "a_minus (class_ring :: 'a ring) = (-)"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum"
    and "finprod (class_ring :: 'a ring) = prod"
    and "⋀X. X ⊆ UNIV = True" (* These rewrite rules will clean lemmas *)
    and "⋀x. x ∈ UNIV = True"
    and "⋀a A. a ∈ A → UNIV ≡ True"
    and "⋀P. P ∧ True ≡ P"
    and "⋀P. (True ⟹ P) ≡ Trueprop P"
  apply unfold_locales
  apply (auto simp: module_vec_simps class_ring_simps Units_def add_smult_distrib_vec 
      smult_add_distrib_vec intro!:bexI[of _ "- _"])
  done

lemma finsum_index:
  assumes i: "i < n"
    and f: "f ∈ A → carrier_vec n"
    and A: "A ⊆ carrier_vec n"
  shows "finsum V f A $ i = sum (λx. f x $ i) A"
  using A f
proof (induct A rule: infinite_finite_induct)
  case empty
    then show ?case using i by simp next
  case (insert x X)
    then have Xf: "finite X"
      and xX: "x ∉ X"
      and x: "x ∈ carrier_vec n"
      and X: "X ⊆ carrier_vec n"
      and fx: "f x ∈ carrier_vec n"
      and f: "f ∈ X → carrier_vec n" by auto
    have i2: "i < dim_vec (finsum V f X)"
      using i finsum_closed[OF f] by auto
    have ix: "i < dim_vec x" using x i by auto
    show ?case
      unfolding finsum_insert[OF Xf xX f fx]
      unfolding sum.insert[OF Xf xX]
      unfolding index_add_vec(1)[OF i2]
      using insert lincomb_def
      by auto
  qed (insert i, auto)


lemma mat_of_rows_mult_as_finsum:
  assumes "v ∈ carrier_vec (length lst)" "⋀ i. i < length lst ⟹ lst ! i ∈ carrier_vec n"
  defines "f l ≡ sum (λ i. if l = lst ! i then v $ i else 0) {0..<length lst}"
  shows mat_of_cols_mult_as_finsum:"mat_of_cols n lst *⇩v v = lincomb f (set lst)"
proof -
  from assms have "∀ i < length lst. lst ! i ∈ carrier_vec n" by blast
  note an = all_nth_imp_all_set[OF this] hence slc:"set lst ⊆ carrier_vec n" by auto
  hence dn [simp]:"⋀ x. x ∈ set lst ⟹ dim_vec x = n" by auto
  have dl [simp]:"dim_vec (lincomb f (set lst)) = n" using an
    by (simp add: slc)
  show ?thesis proof
    show "dim_vec (mat_of_cols n lst *⇩v v) = dim_vec (lincomb f (set lst))" using assms(1,2) by auto
    fix i assume i:"i < dim_vec (lincomb f (set lst))" hence i':"i < n" by auto
    with an have fcarr:"(λv. f v ⋅⇩v v) ∈ set lst → carrier_vec n" by auto
    from i' have "(mat_of_cols n lst *⇩v v) $ i = row (mat_of_cols n lst) i ∙ v" by auto
    also have "… = (∑ia = 0..<dim_vec v. lst ! ia $ i * v $ ia)"
      unfolding mat_of_cols_def row_def scalar_prod_def
      apply(rule sum.cong[OF refl]) using i an assms(1) by auto
    also have "… = (∑ia = 0..<length lst. lst ! ia $ i * v $ ia)" using assms(1) by auto
    also have "… = (∑x∈set lst. f x * x $ i)"
      unfolding f_def sum_distrib_right apply (subst sum.swap)
      apply(rule sum.cong[OF refl])
      unfolding if_distrib if_distribR mult_zero_left sum.delta[OF finite_set] by auto
    also have "… = (∑x∈set lst. (f x ⋅⇩v x) $ i)"
      apply(rule sum.cong[OF refl],subst index_smult_vec) using i slc by auto
    also have "… = (⨁⇘V⇙v∈set lst. f v ⋅⇩v v) $ i" 
      unfolding finsum_index[OF i' fcarr slc] by auto
    finally show "(mat_of_cols n lst *⇩v v) $ i = lincomb f (set lst) $ i"
      by (auto simp:lincomb_def)
  qed
qed

lemma lincomb_as_lincomb_list:
  fixes ws f
  assumes s: "set ws ⊆ carrier_vec n"
  shows "lincomb f (set ws) = lincomb_list (λi. if ∃j<i. ws!i = ws!j then 0 else f (ws ! i)) ws"
  using assms
proof (induct ws rule: rev_induct)
  case (snoc a ws)
  let ?f = "λi. if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)"
  let ?g = "λi. (if ∃j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) ⋅⇩v (ws @ [a]) ! i"
  let ?g2= "(λi. (if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)) ⋅⇩v ws ! i)"
  have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using snoc.prems(1) by auto
  then have ws: "set ws ⊆ carrier_vec n" by auto
  have hyp: "lincomb f (set ws) = lincomb_list ?f ws"
    by (intro snoc.hyps ws)  
  show ?case
  proof (cases "a∈set ws")
    case True    
    have g_length: "?g (length ws) = 0⇩v n" using True
      by (auto, metis in_set_conv_nth nth_append)
    have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
       by auto
    also have "... = (map ?g [0..<length ws]) @ [0⇩v n]" using g_length by simp
    finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0⇩v n]" .
    have "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
      by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
    also have "... =  M.sumlist (map ?g [0..<length ws]) + 0⇩v n "
      by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
    also have "... = M.sumlist (map ?g [0..<length ws] @ [0⇩v n])" 
      by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append)
    finally have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) 
      = M.sumlist (map ?g [0..<length ws] @ [0⇩v n])" .
    have "lincomb f (set (ws @ [a])) = lincomb f (set ws)" using True unfolding lincomb_def
      by (simp add: insert_absorb)
    thus ?thesis 
      unfolding hyp lincomb_list_def map_rw summlist_rw
      by auto
  next
    case False    
    have g_length: "?g (length ws) = f a ⋅⇩v a" using False by (auto simp add: nth_append)
    have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
       by auto
    also have "... = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" using g_length by simp
    finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" .
    have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
      by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
    have "lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))" by auto
    also have "... = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
    also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp    
    also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
    proof (rule finsum_insert)
      show "finite (set ws)" by auto
      show "a ∉ set ws" using False by auto
      show "(λv. f v ⋅⇩v v) ∈ set ws → carrier_vec n"
        using snoc.prems(1) by auto
      show "f a ⋅⇩v a ∈ carrier_vec n" using snoc.prems by auto
    qed
    also have "... = (f a ⋅⇩v a) + lincomb f (set ws)" unfolding lincomb_def ..
    also have "... = (f a ⋅⇩v a) + lincomb_list ?f ws" using hyp by auto
    also have "... =  lincomb_list ?f ws  + (f a ⋅⇩v a)"
      using M.add.m_comm lincomb_list_carrier snoc.prems by auto
    also have "... = lincomb_list (λi. if ∃j<i. (ws @ [a]) ! i 
      = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) (ws @ [a])" 
    proof (unfold lincomb_list_def map_rw summlist_rw, rule M.sumlist_snoc[symmetric])
      show "set (map ?g [0..<length ws]) ⊆ carrier_vec n" using snoc.prems
        by (auto simp add: nth_append)
      show "f a ⋅⇩v a ∈ carrier_vec n"
        using snoc.prems by auto
    qed
    finally show ?thesis .
  qed
qed auto
end

locale matrix_vs = 
  fixes nr :: nat
    and nc :: nat
    and field_type :: "'a :: field itself"
begin

abbreviation V where "V ≡ module_mat TYPE('a) nr nc"
sublocale  
  vectorspace class_ring V
  rewrites "carrier V = carrier_mat nr nc"
    and "add V = (+)"
    and "mult V = (*)"
    and "one V = 1⇩m nr"
    and "zero V = 0⇩m nr nc"
    and "smult V = (⋅⇩m)"
    and "carrier class_ring = UNIV"
    and "mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and "a_inv (class_ring :: 'a ring) = uminus"
    and "a_minus (class_ring :: 'a ring) = minus"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum"
    and "finprod (class_ring :: 'a ring) = prod"
    and "m_inv (class_ring :: 'a ring) x = 
      (if x = 0 then div0 else inverse x)"
  by (rule matrix_vs, auto simp: matrix_vs_simps class_field_def)
end

lemma vec_module: "module (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
proof -
  interpret abelian_group "module_vec TYPE('a) n"
    apply (unfold_locales)
    unfolding module_vec_def Units_def
    using add_inv_exists_vec by auto
  show ?thesis
    unfolding class_field_def
    apply (unfold_locales)
    unfolding class_ring_simps
    unfolding module_vec_simps
    using add_smult_distrib_vec
    by (auto simp: smult_add_distrib_vec)
qed

lemma vec_vs: "vectorspace (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
  unfolding vectorspace_def
  using vec_module class_field 
  by (auto simp: class_field_def)

locale vec_space =
  fixes f_ty::"'a::field itself"
  and n::"nat"
begin

  sublocale vec_module f_ty n.

  sublocale vectorspace class_ring V 
  rewrites cV[simp]: "carrier V = carrier_vec n"
    and [simp]: "add V = (+)"
    and [simp]: "zero V = 0⇩v n"
    and [simp]: "smult V = (⋅⇩v)"
    and "carrier class_ring = UNIV"
    and "mult class_ring = (*)"
    and "add class_ring = (+)"
    and "one class_ring = 1"
    and "zero class_ring = 0"
    and "a_inv (class_ring :: 'a ring) = uminus"
    and "a_minus (class_ring :: 'a ring) = minus"
    and "pow (class_ring :: 'a ring) = (^)"
    and "finsum (class_ring :: 'a ring) = sum"
    and "finprod (class_ring :: 'a ring) = prod"
    and "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)"
  using vec_vs
  unfolding class_field_def
  by (auto simp: module_vec_simps class_ring_simps)

lemma finsum_vec[simp]: "finsum_vec TYPE('a) n = finsum V"
  by (force simp: finsum_vec_def monoid_vec_def finsum_def finprod_def)

lemma finsum_scalar_prod_sum:
  assumes f: "f : U → carrier_vec n"
      and w: "w: carrier_vec n"
  shows "finsum V f U ∙ w = sum (λu. f u ∙ w) U"
  using w f
proof (induct U rule: infinite_finite_induct)
  case (insert u U)
    hence f: "f : U → carrier_vec n" "f u : carrier_vec n"  by auto
    show ?case
      unfolding finsum_insert[OF insert(1) insert(2) f]
      apply (subst add_scalar_prod_distrib) using insert by auto
qed auto

lemma vec_neg[simp]: assumes "x : carrier_vec n" shows "⊖⇘V⇙ x = - x"
  unfolding a_inv_def m_inv_def apply simp 
  apply (rule the_equality, intro conjI)
  using assms apply auto
  using M.minus_unique uminus_carrier_vec uminus_r_inv_vec by blast

lemma finsum_dim:
  "finite A ⟹ f ∈ A → carrier_vec n ⟹ dim_vec (finsum V f A) = n"
proof(induct set:finite)
  case (insert a A)
    hence dfa: "dim_vec (f a) = n" by auto
    have f: "f ∈ A → carrier_vec n" using insert by auto
    hence fa: "f a ∈ carrier_vec n" using insert by auto
    show ?case
      unfolding finsum_insert[OF insert(1) insert(2) f fa]
      using insert by auto
qed simp

lemma lincomb_dim:
  assumes fin: "finite X"
    and X: "X ⊆ carrier_vec n"
  shows "dim_vec (lincomb a X) = n"
proof -
  let ?f = "λv. a v ⋅⇩v v"
  have f: "?f ∈ X → carrier_vec n" apply rule using X by auto
  show ?thesis
    unfolding lincomb_def
    using finsum_dim[OF fin f].
qed


lemma lincomb_index:
  assumes i: "i < n"
    and X: "X ⊆ carrier_vec n"
  shows "lincomb a X $ i = sum (λx. a x * x $ i) X"
proof -
  let ?f = "λx. a x ⋅⇩v x"
  have f: "?f : X → carrier_vec n" using X by auto
  have point: "⋀v. v ∈ X ⟹ (a v ⋅⇩v v) $ i = a v * v $ i" using i X by auto
  show ?thesis
    unfolding lincomb_def
    unfolding finsum_index[OF i f X]
    using point X by simp
qed

lemma append_insert: "set (xs @ [x]) = insert x (set xs)" by simp

lemma lincomb_units:
  assumes i: "i < n" 
  shows "lincomb a (set (unit_vecs n)) $ i = a (unit_vec n i)"
  unfolding lincomb_index[OF i unit_vecs_carrier]
  unfolding unit_vecs_first
proof -
  let ?f = "λm i. ∑x∈set (unit_vecs_first n m). a x * x $ i"
  have zero:"⋀m j. m ≤ j ⟹ j < n ⟹ ?f m j = 0"
  proof -
    fix m
    show "⋀j. m ≤ j ⟹ j < n ⟹ ?f m j = 0"
    proof (induction m)
      case (Suc m)
        hence mj:"m≤j" and mj':"m≠j" and jn:"j<n" and mn:"m<n" by auto
        hence mem: "unit_vec n m ∉ set (unit_vecs_first n m)"
          apply(subst unit_vecs_first_distinct) by auto
        show ?case
          unfolding unit_vecs_first.simps
          unfolding append_insert
          unfolding sum.insert[OF finite_set mem]
          unfolding index_unit_vec(1)[OF mn jn]
          unfolding Suc(1)[OF mj jn] using mj' by simp
    qed simp
  qed
  { fix m
    have "i < m ⟹ m ≤ n ⟹ ?f m i = a (unit_vec n i)"
    proof (induction m arbitrary: i)
      case (Suc m)
        hence iSm: "i < Suc m" and i:"i<n" and mn: "m<n" by auto
        hence mem: "unit_vec n m ∉ set (unit_vecs_first n m)"
          apply(subst unit_vecs_first_distinct) by auto
        show ?case
          unfolding unit_vecs_first.simps
          unfolding append_insert
          unfolding sum.insert[OF finite_set mem]
          unfolding index_unit_vec(1)[OF mn i]
          using zero Suc by (cases "i = m",auto)
    qed auto
  }
  thus "?f n i = a (unit_vec n i)" using assms by auto
qed

lemma lincomb_coordinates:
  assumes v: "v : carrier_vec n"
  defines "a ≡ (λu. v $ (THE i. u = unit_vec n i))"
  shows "lincomb a (set (unit_vecs n)) = v"
proof -
  have a: "a ∈ set (unit_vecs n) → UNIV" by auto
  have fvu: "⋀i. i < n ⟹ v $ i = a (unit_vec n i)"
    unfolding a_def using unit_vec_eq by auto
  show ?thesis
    apply rule
    unfolding lincomb_dim[OF finite_set unit_vecs_carrier]
    using v lincomb_units fvu
    by auto
qed

lemma span_unit_vecs_is_carrier: "span (set (unit_vecs n)) = carrier_vec n" (is "?L = ?R")
proof (rule;rule)
  fix v assume vsU: "v ∈ ?L" show "v ∈ ?R"
  proof -
    obtain a
      where v: "v = lincomb a (set (unit_vecs n))"
      using vsU
      unfolding finite_span[OF finite_set unit_vecs_carrier] by auto
    thus ?thesis using lincomb_closed[OF unit_vecs_carrier] by auto
  qed
  next fix v::"'a vec" assume v: "v ∈ ?R" show "v ∈ ?L"
    unfolding span_def
    using lincomb_coordinates[OF v,symmetric] by auto
qed

lemma fin_dim[simp]: "fin_dim"
  unfolding fin_dim_def
  apply (intro eqTrueI exI conjI) using span_unit_vecs_is_carrier unit_vecs_carrier by auto

lemma unit_vecs_basis: "basis (set (unit_vecs n))" unfolding basis_def span_unit_vecs_is_carrier
proof (intro conjI)
  show "¬ lin_dep (set (unit_vecs n))" 
  proof
    assume "lin_dep (set (unit_vecs n))"
    from this[unfolded lin_dep_def] obtain A a v where
      fin: "finite A" and A: "A ⊆ set (unit_vecs n)"  
      and lc: "lincomb a A = 0⇩v n" and v: "v ∈ A" and av: "a v ≠ 0"      
      by auto
    from v A obtain i where i: "i < n" and vu: "v = unit_vec n i" unfolding unit_vecs_def by auto
    define b where "b = (λ x. if x ∈ A then a x else 0)"
    have id: "A ∪ (set (unit_vecs n) - A) = set (unit_vecs n)" using A by auto
    from lincomb_index[OF i unit_vecs_carrier]
    have "lincomb b (set (unit_vecs n)) $ i = (∑x∈ (A ∪ (set (unit_vecs n) - A)). b x * x $ i)" 
      unfolding id .
    also have "… = (∑x∈ A. b x * x $ i) + (∑x∈ set (unit_vecs n) - A. b x * x $ i)"
      by (rule sum.union_disjoint, insert fin, auto)
    also have "(∑x∈ A. b x * x $ i) = (∑x∈ A. a x * x $ i)"
      by (rule sum.cong, auto simp: b_def)
    also have "… = lincomb a A $ i" 
      by (subst lincomb_index[OF i], insert A unit_vecs_carrier, auto)
    also have "… = 0" unfolding lc using i by simp
    also have "(∑x∈ set (unit_vecs n) - A. b x * x $ i) = 0"
      by (rule sum.neutral, auto simp: b_def)
    finally have "lincomb b (set (unit_vecs n)) $ i = 0" by simp
    from lincomb_units[OF i, of b, unfolded this]
    have "b v = 0" unfolding vu by simp
    with v av show False unfolding b_def by simp
  qed
qed (insert unit_vecs_carrier, auto)

lemma unit_vecs_length[simp]: "length (unit_vecs n) = n"
  unfolding unit_vecs_def by auto

lemma unit_vecs_distinct: "distinct (unit_vecs n)"
  unfolding distinct_conv_nth unit_vecs_length
proof (intro allI impI)
  fix i j
  assume *: "i < n" "j < n" "i ≠ j"
  show "unit_vecs n ! i ≠ unit_vecs n ! j"
  proof
    assume "unit_vecs n ! i = unit_vecs n ! j"
    from arg_cong[OF this, of "λ v. v $ i"] 
    show False using * unfolding unit_vecs_def by auto
  qed
qed

lemma dim_is_n: "dim = n"
  unfolding dim_basis[OF finite_set unit_vecs_basis]
  unfolding distinct_card[OF unit_vecs_distinct]
  by simp

end

locale mat_space =
  vec_space f_ty nc for f_ty::"'a::field itself" and nc::"nat" +
  fixes nr :: "nat"
begin
  abbreviation M where "M ≡ ring_mat TYPE('a) nc nr"
end

context vec_space
begin
lemma fin_dim_span:
assumes "finite A" "A ⊆ carrier V"
shows "vectorspace.fin_dim class_ring (vs (span A))"
proof -
  have "vectorspace class_ring (span_vs A)"
   using assms span_is_subspace subspace_def subspace_is_vs by simp
  have "A ⊆ span A" using assms in_own_span by simp
  have "submodule class_ring (span A) V" using assms span_is_submodule by simp
  have "LinearCombinations.module.span class_ring (vs (span A)) A = carrier (vs (span A))"
    using  span_li_not_depend(1)[OF ‹A ⊆ span A› ‹submodule class_ring (span A) V›] by auto
  then show ?thesis unfolding vectorspace.fin_dim_def[OF ‹vectorspace class_ring (span_vs A)›]
    using List.finite_set ‹A ⊆ span A› ‹vectorspace class_ring (vs (span A))›
    vec_vs vectorspace.carrier_vs_is_self[OF ‹vectorspace class_ring (span_vs A)›] using assms(1) by auto
qed

lemma fin_dim_span_cols:
assumes "A ∈ carrier_mat n nc"
shows "vectorspace.fin_dim class_ring (vs (span (set (cols A))))"
  using fin_dim_span cols_dim List.finite_set assms carrier_matD(1) module_vec_simps(3) by force
end

context vec_module
begin

lemma lincomb_list_as_mat_mult:
  assumes "∀w ∈ set ws. dim_vec w = n"
  shows "lincomb_list c ws = mat_of_cols n ws *⇩v vec (length ws) c" (is "?l ws c = ?r ws c")
proof (insert assms, induct ws arbitrary: c)
  case Nil
  then show ?case by (auto simp: mult_mat_vec_def scalar_prod_def)
next
  case (Cons w ws)
  { fix i assume i: "i < n"
    have "?l (w#ws) c = c 0 ⋅⇩v w + mat_of_cols n ws *⇩v vec (length ws) (c ∘ Suc)"
      by (simp add: Cons o_def)
    also have "… $ i = ?r (w#ws) c $ i"
      using Cons i index_smult_vec
      by (simp add: mat_of_cols_Cons_index_0 mat_of_cols_Cons_index_Suc o_def vec_Suc mult_mat_vec_def row_def length_Cons)
    finally have "?l (w#ws) c $ i = …".
  }
  with Cons show ?case by (intro eq_vecI, auto)
qed

lemma lincomb_vec_diff_add:
    assumes A: "A ⊆ carrier_vec n"
    and BA: "B ⊆ A" and fin_A: "finite A" 
    and f: "f ∈ A → UNIV" shows "lincomb f A = lincomb f (A-B) + lincomb f B"
proof -
  have "A - B ∪ B = A" using BA by auto
  hence "lincomb f A = lincomb f (A - B ∪ B)"  by simp
  also have "... = lincomb f (A-B) + lincomb f B"
    by (rule lincomb_union, insert assms, auto intro: finite_subset)
  finally show ?thesis .
qed

lemma dim_sumlist:
  assumes "∀x∈set xs. dim_vec x = n"
  shows "dim_vec (M.sumlist xs) = n" using assms by (induct xs, auto)

lemma sumlist_nth:
  assumes "∀x∈set xs. dim_vec x = n" and "i<n"
  shows "(M.sumlist xs) $ i= sum (λj. (xs ! j) $ i) {0..<length xs}"
  using assms
proof (induct xs rule: rev_induct)
  case (snoc a xs) 
  have [simp]: "x ∈ carrier_vec n" if x: "x∈set xs" for x 
    using snoc.prems x unfolding carrier_vec_def by auto
  have [simp]: "a ∈ carrier_vec n" 
    using snoc.prems unfolding carrier_vec_def by auto
  have hyp: "M.sumlist xs $ i = (∑j = 0..<length xs. xs ! j $ i)" 
    by (rule snoc.hyps, auto simp add: snoc.prems)  
  have "M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]" 
    by (rule M.sumlist_append, auto simp add: snoc.prems)
  also have "... = M.sumlist xs + a" by auto
  also have "... $ i = (M.sumlist xs $ i) + (a $ i)" 
    by (rule index_add_vec(1), auto simp add: snoc.prems)
  also have "... =  (∑j = 0..<length xs. xs ! j $ i) + (a $ i)" unfolding hyp by simp
  also have "... = (∑j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)"
    by (auto, rule sum.cong, auto simp add: nth_append)     
  finally show ?case .
qed auto

lemma lincomb_as_lincomb_list_distinct:
  assumes s: "set ws ⊆ carrier_vec n" and d: "distinct ws"
  shows "lincomb f (set ws) = lincomb_list (λi. f (ws ! i)) ws"
proof (insert assms, induct ws)
  case Nil
  then show ?case by auto
next
  case (Cons a ws)
  have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using Cons.prems(1) by auto
  then have ws: "set ws ⊆ carrier_vec n" by auto
  have hyp: "lincomb f (set (ws)) = lincomb_list (λi. f (ws ! i)) ws"
  proof (intro Cons.hyps ws)
    show "distinct ws" using Cons.prems(2) by auto
  qed  
  have "(map (λi. f (ws ! i) ⋅⇩v ws ! i) [0..<length ws]) = (map (λv. f v ⋅⇩v v) ws)"
    by (intro nth_equalityI, auto)
  with ws have sumlist_rw: "sumlist (map (λi. f (ws ! i) ⋅⇩v ws ! i) [0..<length ws])
    = sumlist (map (λv. f v ⋅⇩v v) ws)"
    by (subst (1 2) sumlist_as_summset, auto)
  have "lincomb f (set (a # ws)) = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
  also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp
  also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
    by (rule finsum_insert, insert Cons.prems, auto)
  also have "... = f a ⋅⇩v a + lincomb_list (λi. f (ws ! i)) ws" using hyp lincomb_def by auto
  also have "... = f a ⋅⇩v a + sumlist (map (λv. f v ⋅⇩v v) ws)" 
    unfolding lincomb_list_def sumlist_rw by auto
  also have "... = sumlist (map (λv. f v ⋅⇩v v) (a # ws))"
  proof -
    let ?a = "(map (λv. f v ⋅⇩v v) [a])"
    have a: "a ∈ carrier_vec n" using Cons.prems(1) by auto
    have "f a ⋅⇩v a = sumlist (map (λv. f v ⋅⇩v v) [a])" using Cons.prems(1) by auto
    hence "f a ⋅⇩v a + sumlist (map (λv. f v ⋅⇩v v) ws) 
      = sumlist ?a + sumlist (map (λv. f v ⋅⇩v v) ws)" by simp
    also have "... = sumlist (?a @ (map (λv. f v ⋅⇩v v) ws))"
      by (rule sumlist_append[symmetric], auto simp add: a)
    finally show ?thesis by auto
  qed
  also have "... = sumlist (map (λi. f ((a # ws) ! i) ⋅⇩v (a # ws) ! i) [0..<length (a # ws)])"
  proof -
    have u: "(map (λi. f ((a # ws) ! i) ⋅⇩v (a # ws) ! i) [0..<length (a # ws)]) 
        = (map (λv. f v ⋅⇩v v) (a # ws))"
      by (smt (verit, del_insts) length_map map_equality_iff map_nth nth_map)
    show ?thesis unfolding u ..
  qed
  also have "... = lincomb_list (λi. f ((a # ws) ! i)) (a # ws)"
    unfolding lincomb_list_def ..
  finally show ?case .
qed

end

locale idom_vec = vec_module f_ty for f_ty :: "'a :: idom itself"
begin

lemma lin_dep_cols_imp_det_0':
  fixes ws
  defines "A ≡ mat_of_cols n ws"
  assumes dimv_ws: "∀w∈set ws. dim_vec w = n"
  assumes A: "A ∈ carrier_mat n n" and ld_cols: "lin_dep (set (cols A))"
  shows  "det A = 0"
proof (cases "distinct ws")
  case False
  obtain i j where ij: "i≠j" and c: "col A i = col A j" and i: "i<n" and j: "j<n" 
    using False A unfolding A_def
    by (metis dimv_ws distinct_conv_nth carrier_matD(2) 
        col_mat_of_cols mat_of_cols_carrier(3) nth_mem carrier_vecI)
  show ?thesis by (rule det_identical_columns[OF A ij i j c])  
next
  case True
  have d1[simp]: "⋀x. x ∈ set ws ⟹ x ∈ carrier_vec n" using dimv_ws by auto 
  obtain A' f' v where f'_in: "f' ∈ A' → UNIV" 
    and lc_f': "lincomb f' A' = 0⇩v n" and f'_v: "f' v ≠ 0"
    and v_A': "v ∈ A'" and A'_in_rows: "A' ⊆ set (cols A)" 
    using ld_cols unfolding lin_dep_def by auto
  define f where "f ≡ λx. if x ∉ A' then 0 else f' x"
  have f_in: "f ∈ (set (cols A)) → UNIV" using f'_in by auto
  have A'_in_carrier: "A' ⊆ carrier_vec n"
    by (metis (no_types) A'_in_rows A_def cols_dim carrier_matD(1) mat_of_cols_carrier(1) subset_trans)
  have lc_f: "lincomb f (set (cols A)) = 0⇩v n"   
  proof -
    have l1: "lincomb f (set (cols A) - A') = 0⇩v n"
      by (rule lincomb_zero, auto simp add: f_def, insert A cols_dim, blast)
    have l2: "lincomb f A' = 0⇩v n " using lc_f' unfolding f_def using A'_in_carrier by auto
    have "lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'"
    proof (rule lincomb_vec_diff_add)
      show "set (cols A) ⊆ carrier_vec n"
        using A cols_dim by blast
      show "A' ⊆ set (cols A)"
        using A'_in_rows by blast
    qed auto
    also have "... =  0⇩v n" using l1 l2 by auto
    finally show ?thesis .
  qed
  have v_in: "v ∈ (set (cols A))" using v_A' A'_in_rows by auto 
  have fv: "f v ≠ 0" using f'_v v_A' unfolding f_def by auto
  let ?c = "(λi. f (ws ! i))"
  have "lincomb f (set ws) = lincomb_list ?c ws"
    by (rule lincomb_as_lincomb_list_distinct[OF _ True], auto)
  have "∃v.  v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ A *⇩v v = 0⇩v n"
  proof (rule exI[of _ " vec (length ws) ?c"], rule conjI)
    show "vec (length ws) ?c ∈ carrier_vec n" using A A_def by auto
    have vec_not0: "vec (length ws) ?c ≠ 0⇩v n"
    proof -
      obtain i where ws_i: "(ws ! i) = v" and i: "i<length ws" using v_in unfolding A_def        
        by (metis d1 cols_mat_of_cols in_set_conv_nth subset_eq)
      have "vec (length ws) ?c $ i = ?c i" by (rule index_vec[OF i])
      also have "... = f v" using ws_i by simp
      also have "... ≠ 0" using fv by simp
      finally show ?thesis
        using A A_def i by fastforce
    qed
    have "A *⇩v vec (length ws) ?c = mat_of_cols n ws *⇩v vec (length ws) ?c" unfolding A_def ..
    also have "... = lincomb_list ?c ws" by (rule lincomb_list_as_mat_mult[symmetric, OF dimv_ws])
    also have "... = lincomb f (set ws)" 
      by (rule lincomb_as_lincomb_list_distinct[symmetric, OF _ True], auto)
    also have "... =  0⇩v n" 
      using lc_f unfolding A_def using A by (simp add: subset_code(1))
    finally show "vec (length ws) (λi. f (ws ! i)) ≠ 0⇩v n ∧ A *⇩v vec (length ws) (λi. f (ws ! i)) = 0⇩v n"
      using vec_not0 by fast
  qed 
  thus ?thesis unfolding det_0_iff_vec_prod_zero[OF A] .
qed

lemma lin_dep_cols_imp_det_0:
  assumes A: "A ∈ carrier_mat n n" and ld: "lin_dep (set (cols A))"
  shows "det A = 0" 
proof -
  have col_rw: "(cols (mat_of_cols n (cols A))) = cols A"
    using A by auto
  have m: "mat_of_cols n (cols A) = A" using A by auto
  show ?thesis
  by (rule A lin_dep_cols_imp_det_0'[of "cols A", unfolded col_rw, unfolded m, OF _ A ld])
     (metis A cols_dim carrier_matD(1) subsetCE carrier_vecD)
qed

corollary lin_dep_rows_imp_det_0:
  assumes A: "A ∈ carrier_mat n n" and ld: "lin_dep (set (rows A))"
  shows "det A = 0" 
  by (subst det_transpose[OF A, symmetric], rule lin_dep_cols_imp_det_0, auto simp add: ld A)

lemma det_not_0_imp_lin_indpt_rows:
  assumes A: "A ∈ carrier_mat n n" and det: "det A ≠ 0"  
  shows "lin_indpt (set (rows A))"
    using lin_dep_rows_imp_det_0[OF A] det by auto

lemma upper_triangular_imp_lin_indpt_rows:
  assumes A: "A ∈ carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 ∉ set (diag_mat A)"
  shows "lin_indpt (set (rows A))"
  using det_not_0_imp_lin_indpt_rows upper_triangular_imp_det_eq_0_iff assms
  by auto

(* Connection from set-based to list-based *)

lemma span_list_as_span:
  assumes "set vs ⊆ carrier_vec n"
  shows "span_list vs = span (set vs)"
  using assms
proof (auto simp: span_list_def span_def)
  fix f show "∃a A. lincomb_list f vs = lincomb a A ∧ finite A ∧ A ⊆ set vs" 
    using assms lincomb_list_as_lincomb by auto
next
  fix f::"'a vec ⇒'a" and A assume fA: "finite A" and A: "A ⊆ set vs" 
  have [simp]: "x ∈ carrier_vec n" if x: "x ∈ A" for x using A x assms by auto
  have [simp]:  "v ∈ carrier_vec n" if v: "v ∈ set vs" for v using assms v by auto
  have set_vs_Un: "((set vs) - A) ∪ A = set vs" using A by auto
  let ?f = "(λx. if x∈(set vs) - A then 0 else f x)"
  have f0: "(⨁⇘V⇙v∈(set vs) - A. ?f v ⋅⇩v v) = 0⇩v n" by (rule M.finsum_all0, auto)  
  have "lincomb f A = lincomb ?f A"
    by (auto simp add: lincomb_def intro!: finsum_cong2)
  also have "... = (⨁⇘V⇙v∈(set vs) - A. ?f v ⋅⇩v v) + (⨁⇘V⇙v∈A. ?f v ⋅⇩v v)" 
    unfolding f0 lincomb_def by auto
  also have "... = lincomb ?f (((set vs) - A) ∪ A)" 
    unfolding lincomb_def 
    by (rule M.finsum_Un_disjoint[symmetric], auto simp add: fA)
  also have "... = lincomb ?f (set vs)" using set_vs_Un by auto
  finally have "lincomb f A = lincomb ?f (set vs)" .    
  with lincomb_as_lincomb_list[OF assms] 
  show "∃c. lincomb f A = lincomb_list c vs" by auto    
qed

lemma in_spanI[intro]:
  assumes "v = lincomb a A" "finite A" "A ⊆ W"
  shows "v ∈ span W"
unfolding span_def using assms by auto
lemma in_spanE:
  assumes "v ∈ span W"
  shows "∃ a A. v = lincomb a A ∧ finite A ∧ A ⊆ W"
using assms unfolding span_def by auto

declare in_own_span[intro]

lemma smult_in_span:
  assumes "W ⊆ carrier_vec n" and insp: "x ∈ span W"
  shows "c ⋅⇩v x ∈ span W"
proof -
  from in_spanE[OF insp] obtain a A where a: "x = lincomb a A" "finite A" "A ⊆ W" by blast
  have "c ⋅⇩v x = lincomb (λ x. c * a x) A" using a(1) unfolding lincomb_def a
    apply(subst finsum_smult) using assms a by (auto simp:smult_smult_assoc)
  thus "c ⋅⇩v x ∈ span W" using a(2,3) by auto
qed

lemma span_subsetI: assumes ws: "ws ⊆ carrier_vec n" 
  "us ⊆ span ws" 
shows "span us ⊆ span ws" 
  by (simp add: assms(1) span_is_submodule span_is_subset subsetI ws)

end

context vec_space begin
sublocale idom_vec.

lemma sumlist_in_span: assumes W: "W ⊆ carrier_vec n"  
  shows "(⋀x. x ∈ set xs ⟹ x ∈ span W) ⟹ sumlist xs ∈ span W" 
proof (induct xs)
  case Nil
  thus ?case using W by force
next
  case (Cons x xs)
  from span_is_subset2[OF W] Cons(2) have xs: "x ∈ carrier_vec n" "set xs ⊆ carrier_vec n" by auto
  from span_add1[OF W Cons(2)[of x] Cons(1)[OF Cons(2)]]
  have "x + sumlist xs ∈ span W" by auto
  also have "x + sumlist xs = sumlist ([x] @ xs)" 
    by (subst sumlist_append, insert xs, auto)
  finally show ?case by simp
qed

lemma span_span[simp]:
  assumes "W ⊆ carrier_vec n"
  shows "span (span W) = span W"
proof(standard,standard,goal_cases)
  case (1 x) with in_spanE obtain a A where a: "x = lincomb a A" "finite A" "A ⊆ span W" by blast
  from a(3) assms have AC:"A ⊆ carrier_vec n" by auto
  show ?case unfolding a(1)[unfolded lincomb_def]
  proof(insert a(3),atomize (full),rule finite_induct[OF a(2)],goal_cases)
    case 1
    then show ?case using span_zero by auto
  next
    case (2 x F)
    { assume F:"insert x F ⊆ span W"
      hence "a x ⋅⇩v x ∈ span W" by (intro smult_in_span[OF assms],auto)
      hence "a x ⋅⇩v x + (⨁⇘V⇙v∈F. a v ⋅⇩v v) ∈ span W"
        using span_add1 F 2 assms by auto
      hence "(⨁⇘V⇙v∈insert x F. a v ⋅⇩v v) ∈ span W"
        apply(subst M.finsum_insert[OF 2(1,2)]) using F assms by auto
    }
    then show ?case by auto
  qed
next
  case 2
  show ?case using assms by(intro in_own_span, auto)
qed


lemma upper_triangular_imp_basis:
  assumes A: "A ∈ carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 ∉ set (diag_mat A)"
  shows "basis (set (rows A))"
  using upper_triangular_imp_distinct[OF assms]
  using upper_triangular_imp_lin_indpt_rows[OF assms] A
  by (auto intro: dim_li_is_basis simp: distinct_card dim_is_n set_rows_carrier)

lemma fin_dim_span_rows:
assumes A: "A ∈ carrier_mat nr n"
shows "vectorspace.fin_dim class_ring (vs (span (set (rows A))))"
proof (rule fin_dim_span) 
  show "set (rows A) ⊆ carrier V" using A rows_carrier[of A] unfolding carrier_mat_def by auto
  show "finite (set (rows A))" by auto
qed

definition "row_space B = span (set (rows B))"
definition "col_space B = span (set (cols B))"

lemma row_space_eq_col_space_transpose:
  shows "row_space A = col_space A⇧T"
  unfolding col_space_def row_space_def cols_transpose ..

lemma col_space_eq_row_space_transpose:
  shows "col_space A = row_space A⇧T"
  unfolding col_space_def row_space_def Matrix.rows_transpose ..


lemma col_space_eq:
  assumes A: "A ∈ carrier_mat n nc"
  shows "col_space A = {y∈carrier_vec (dim_row A). ∃x∈carrier_vec (dim_col A). A *⇩v x = y}"
proof -
  let ?ws = "cols A"
  have set_cols_in: "set (cols A) ⊆ carrier_vec n" using A unfolding cols_def by auto
  have "lincomb f S ∈ carrier_vec (dim_row A)" if "finite S" and S: "S ⊆ set (cols A)" for f S 
    using lincomb_closed A
    by (metis (full_types) S carrier_matD(1) cols_dim lincomb_closed subsetCE subsetI)
  moreover have "∃x∈carrier_vec (dim_col A). A *⇩v x = lincomb f S" 
    if fin_S: "finite S" and S: "S ⊆ set (cols A)" for f S
  proof -    
    let ?g = "(λv. if v ∈ S then f v else 0)"
    let ?g' = "(λi. if ∃j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"
    let ?Z = "set ?ws - S"
    have union: "set ?ws = S ∪ ?Z" using S by auto
    have inter: "S ∩ ?Z = {}" by auto    
    have "lincomb f S = lincomb ?g S" by (rule lincomb_cong, insert set_cols_in A S, auto)
    also have "... = lincomb ?g (S ∪ ?Z)" 
      by (rule lincomb_clean[symmetric],insert set_cols_in A S fin_S, auto)
    also have "... = lincomb ?g (set ?ws)" using union by auto
    also have "... = lincomb_list ?g' ?ws" 
      by (rule lincomb_as_lincomb_list[OF set_cols_in])
    also have "... = mat_of_cols n ?ws *⇩v vec (length ?ws) ?g'" 
      by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
    also have "... = A *⇩v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto
    finally show ?thesis by auto
  qed 
  moreover have "∃f S. A *⇩v x = lincomb f S ∧ finite S ∧ S ⊆ set (cols A)" 
    if Ax: "A *⇩v x ∈ carrier_vec (dim_row A)" and x: "x ∈ carrier_vec (dim_col A)" for x 
  proof -
    let ?c = "λi. x $ i"
    have x_vec: "vec (length ?ws) ?c = x" using x by auto
    have "A *⇩v x = mat_of_cols n ?ws *⇩v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto
    also have "... = lincomb_list ?c ?ws" 
      by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
    also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)" 
      by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)
    finally show ?thesis by auto
  qed
  ultimately show ?thesis unfolding col_space_def span_def by auto
qed

lemma vector_space_row_space: 
  assumes A: "A ∈ carrier_mat nr n"
  shows "vectorspace class_ring (vs (row_space A))"
proof -
  have fin: "finite (set (rows A))" by auto
  have s: "set (rows A) ⊆ carrier V" using A unfolding rows_def by auto
  have "span_vs (set (rows A)) = vs (span (set (rows A)))" by auto
  moreover have "vectorspace class_ring (span_vs (set (rows A)))" 
    using fin s span_is_subspace subspace_def subspace_is_vs by simp
  ultimately show ?thesis unfolding row_space_def by auto
qed

lemma row_space_eq:
  assumes A: "A ∈ carrier_mat nr n"
  shows "row_space A = {w∈carrier_vec (dim_col A). ∃y∈carrier_vec (dim_row A). A⇧T *⇩v y = w}" 
  using A col_space_eq unfolding row_space_eq_col_space_transpose by auto

lemma row_space_is_preserved:
  assumes inv_P: "invertible_mat P" and P: "P ∈ carrier_mat m m" and A: "A ∈ carrier_mat m n"
  shows "row_space (P*A) = row_space A"
proof -
  have At: "A⇧T ∈ carrier_mat n m" using A by auto
  have Pt: "P⇧T ∈ carrier_mat m m" using P by auto
  have PA: "P*A ∈ carrier_mat m n" using P A by auto
  have "w ∈ row_space A" if w: "w ∈ row_space (P*A)" for w
  proof -
    have w_carrier: "w ∈ carrier_vec (dim_col (P*A))"
      using w mult_carrier_mat[OF P A] row_space_eq by auto     
    from that and this obtain y where y: "y ∈ carrier_vec (dim_row (P * A))" 
      and w_By: "w = (P*A)⇧T *⇩v y" unfolding row_space_eq[OF PA] by blast
    have ym: "y ∈ carrier_vec m" using y Pt by auto
    have "w=((P*A)⇧T) *⇩v y" using w_By .
    also have "... = (A⇧T * P⇧T) *⇩v y" using transpose_mult[OF P A] by auto
    also have "... = A⇧T *⇩v (P⇧T *⇩v y)" by (rule assoc_mult_mat_vec[OF At Pt], insert Pt y, auto)
    finally show "w ∈ row_space A" unfolding row_space_eq[OF A] using At Pt ym by auto
  qed
    moreover have "w ∈ row_space (P*A)" if w: "w ∈ row_space A" for w
    proof -
      have w_carrier: "w ∈ carrier_vec (dim_col A)" using w A unfolding row_space_eq[OF A] by auto
      obtain P' where PP': "inverts_mat P P'" and P'P: "inverts_mat P' P" 
        using inv_P P unfolding invertible_mat_def by blast
      have P': "P' ∈ carrier_mat m m" using PP' P'P P unfolding inverts_mat_def 
        by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_one_mat(3))        
      from that obtain y where y: "y ∈ carrier_vec (dim_row A)" and 
        w_Ay: "w = A⇧T *⇩v y" unfolding row_space_eq[OF A] by blast
      have Py: "(P'⇧T *⇩v y) ∈ carrier_vec m" using P' y A by auto
      have "w = A⇧T *⇩v y" using w_Ay .
      also have "... = ((P' * P)*A)⇧T *⇩v y" 
        using P'P left_mult_one_mat A P' unfolding inverts_mat_def by auto
      also have "... = ((P' * (P*A))⇧T) *⇩v y" using assoc_mult_mat_vec P' P A by auto
      also have "... = ((P*A)⇧T * P'⇧T) *⇩v y" using transpose_mult P A P' mult_carrier_mat by metis        
      also have "... = (P*A)⇧T *⇩v (P'⇧T *⇩v y)" using A P' PA y by auto
      finally show "w ∈ row_space (P*A)"
        unfolding row_space_eq[OF PA] 
        using Py w_carrier A P by fastforce
    qed
  ultimately show ?thesis by auto
qed

end

context vec_module begin

lemma R_sumlist[simp]: "R.sumlist = sum_list" 
proof (intro ext) 
  fix xs
  show "R.sumlist xs = sum_list xs" by (induct xs, auto)
qed

lemma sumlist_dim: assumes "⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n"
  shows "dim_vec (sumlist xs) = n"
  using sumlist_carrier assms
  by fastforce
    
lemma sumlist_vec_index: assumes "⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n"
  and "i < n" 
shows "sumlist xs $ i = sum_list (map (λ x. x $ i) xs)" 
  unfolding M.sumlist_def using assms(1) proof(induct xs)
  case (Cons a xs)
  hence cond:"⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n" by auto
  from Cons(1)[OF cond] have IH:"foldr (+) xs (0⇩v n) $ i = (∑x←xs. x $ i)" by auto
  have "(a + foldr (+) xs (0⇩v n)) $ i = a $ i + (∑x←xs. x $ i)" 
    apply(subst index_add_vec) unfolding IH
    using sumlist_dim[OF cond,unfolded M.sumlist_def] assms by auto
  then show ?case by auto next
  case Nil thus ?case using assms by auto
qed
 
lemma scalar_prod_left_sum_distrib: 
  assumes vs: "⋀ v. v ∈ set vvs ⟹ v ∈ carrier_vec n" and w: "w ∈ carrier_vec n" 
  shows "sumlist vvs ∙ w = sum_list (map (λ v. v ∙ w) vvs)"
  using vs
proof (induct vvs)
  case (Cons v vs)
  from Cons have v: "v ∈ carrier_vec n" and vs: "sumlist vs ∈ carrier_vec n" 
    by (auto intro!: sumlist_carrier)
  have "sumlist (v # vs) ∙ w = sumlist ([v] @ vs) ∙ w " by auto
  also have "… = (v + sumlist vs) ∙ w" 
    by (subst sumlist_append, insert Cons v vs, auto)
  also have "… = v ∙ w + (sumlist vs ∙ w)" 
    by (rule add_scalar_prod_distrib[OF v vs w])
  finally show ?case using Cons by auto
qed (insert w, auto)   

lemma scalar_prod_right_sum_distrib: 
  assumes vs: "⋀ v. v ∈ set vvs ⟹ v ∈ carrier_vec n" and w: "w ∈ carrier_vec n" 
  shows "w ∙ sumlist vvs = sum_list (map (λ v. w ∙ v) vvs)"
  by (subst comm_scalar_prod[OF w sumlist_carrier], insert vs w, force,
  subst scalar_prod_left_sum_distrib[OF vs w], force,
  rule arg_cong[of _ _ sum_list], rule nth_equalityI, 
  auto simp: set_conv_nth intro!: comm_scalar_prod)

lemma lincomb_list_add_vec_2: assumes us: "set us ⊆ carrier_vec n" 
  and x: "x = lincomb_list lc (us [i := us ! i + c ⋅⇩v us ! j])"
  and i: "j < length us" "i < length us" "i ≠ j" 
shows "x = lincomb_list (lc (j := lc j + lc i * c)) us" (is "_ = ?x")
proof -
  let ?xx = "lc j + lc i * c" 
  let ?i = "us ! i" 
  let ?j = "us ! j" 
  let ?v = "?i + c ⋅⇩v ?j" 
  let ?ws = "us [i := us ! i + c ⋅⇩v us ! j]"
  from us have usk: "k < length us ⟹ us ! k ∈ carrier_vec n" for k by auto
  from usk i have ij: "?i ∈ carrier_vec n" "?j ∈ carrier_vec n" by auto
  hence v: "c ⋅⇩v ?j ∈ carrier_vec n" "?v ∈ carrier_vec n" by auto
  with us have ws: "set ?ws ⊆ carrier_vec n" unfolding set_conv_nth using i 
    by (auto, rename_tac k, case_tac "k = i", auto)
  from us have us': "∀w∈set us. dim_vec w = n" by auto 
  from ws have ws': "∀w∈set ?ws. dim_vec w = n" by auto 
  have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))" 
    by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x ∈ {0 ..< length us}", auto)
  define M2 where "M2 = M.summset
      {#lc ia ⋅⇩v ?ws ! ia. ia ∈# mset_set ({0..<length us} - {i, j})#}" 
  define M1 where "M1 = M.summset {#(if i = j then ?xx else lc i) ⋅⇩v us ! i. i ∈# mset_set ({0..<length us} - {i, j})#}" 
  have M1: "M1 ∈ carrier_vec n" unfolding M1_def using usk by fastforce
  have M2: "M1 = M2" unfolding M2_def M1_def
    by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto) 
  have x1: "x = lc j ⋅⇩v ?j + (lc i ⋅⇩v ?i + lc i ⋅⇩v (c ⋅⇩v ?j) + M1)" 
    unfolding x lincomb_list_def M2 M2_def
    apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, 
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
    by (subst M.summset_add_mset, auto)+
  have x2: "?x = ?xx ⋅⇩v ?j + (lc i ⋅⇩v ?i + M1)"
    unfolding x lincomb_list_def M1_def
    apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, 
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
    by (subst M.summset_add_mset, auto)+
  show ?thesis unfolding x1 x2 using M1 ij
    by (intro eq_vecI, auto simp: field_simps)
qed

lemma lincomb_list_add_vec_1: assumes us: "set us ⊆ carrier_vec n" 
  and x: "x = lincomb_list lc us"
  and i: "j < length us" "i < length us" "i ≠ j" 
shows "x = lincomb_list (lc (j := lc j - lc i * c)) (us [i := us ! i + c ⋅⇩v us ! j])" (is "_ = ?x")
proof -
  let ?i = "us ! i" 
  let ?j = "us ! j" 
  let ?v = "?i + c ⋅⇩v ?j" 
  let ?ws = "us [i := us ! i + c ⋅⇩v us ! j]"
  from us have usk: "k < length us ⟹ us ! k ∈ carrier_vec n" for k by auto
  from usk i have ij: "?i ∈ carrier_vec n" "?j ∈ carrier_vec n" by auto
  hence v: "c ⋅⇩v ?j ∈ carrier_vec n" "?v ∈ carrier_vec n" by auto
  with us have ws: "set ?ws ⊆ carrier_vec n" unfolding set_conv_nth using i 
    by (auto, rename_tac k, case_tac "k = i", auto)
  from us have us': "∀w∈set us. dim_vec w = n" by auto 
  from ws have ws': "∀w∈set ?ws. dim_vec w = n" by auto 
  have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))" 
    by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x ∈ {0 ..< length us}", auto)
  define M2 where "M2 = M.summset
      {#(if ia = j then lc j - lc i * c else lc ia) ⋅⇩v ?ws ! ia
      . ia ∈# mset_set ({0..<length us} - {i, j})#}" 
  define M1 where "M1 = M.summset {#lc i ⋅⇩v us ! i. i ∈# mset_set ({0..<length us} - {i, j})#}" 
  have M1: "M1 ∈ carrier_vec n" unfolding M1_def using usk by fastforce
  have M2: "M1 = M2" unfolding M2_def M1_def
    by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto) 
  have x1: "x = lc j ⋅⇩v ?j + (lc i ⋅⇩v ?i + M1)" 
    unfolding x lincomb_list_def M1_def
    apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, 
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
    by (subst M.summset_add_mset, auto)+
  have x2: "?x = (lc j - lc i * c) ⋅⇩v ?j + (lc i ⋅⇩v ?i + lc i ⋅⇩v (c ⋅⇩v ?j) + M1)"
    unfolding x lincomb_list_def M2 M2_def
    apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, 
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
    by (subst M.summset_add_mset, auto)+
  show ?thesis unfolding x1 x2 using M1 ij
    by (intro eq_vecI, auto simp: field_simps)
qed

end

context vec_space
begin
lemma add_vec_span: assumes us: "set us ⊆ carrier_vec n" 
  and i: "j < length us" "i < length us" "i ≠ j" 
shows "span (set us) = span (set (us [i := us ! i + c ⋅⇩v us ! j]))" (is "_ = span (set ?ws)")
proof -
  let ?i = "us ! i" 
  let ?j = "us ! j" 
  let ?v = "?i + c ⋅⇩v ?j" 
  from us i have ij: "?i ∈ carrier_vec n" "?j ∈ carrier_vec n" by auto
  hence v: "?v ∈ carrier_vec n" by auto
  with us have ws: "set ?ws ⊆ carrier_vec n" unfolding set_conv_nth using i 
    by (auto, rename_tac k, case_tac "k = i", auto)
  have "span (set us) = span_list us" unfolding span_list_as_span[OF us] ..
  also have "… = span_list ?ws"
  proof -
    {
      fix x
      assume "x ∈ span_list us" 
      then obtain lc where "x = lincomb_list lc us" by (metis in_span_listE)
      from lincomb_list_add_vec_1[OF us this i, of c]
      have "x ∈ span_list ?ws" unfolding span_list_def by auto
    }
    moreover
    {
      fix x
      assume "x ∈ span_list ?ws" 
      then obtain lc where "x = lincomb_list lc ?ws" by (metis in_span_listE)
      from lincomb_list_add_vec_2[OF us this i]
      have "x ∈ span_list us" unfolding span_list_def by auto
    }
    ultimately show ?thesis by blast
  qed
  also have "… = span (set ?ws)" unfolding span_list_as_span[OF ws] ..
  finally show ?thesis .
qed

lemma prod_in_span[intro!]:
  assumes "b ∈ carrier_vec n" "S ⊆ carrier_vec n" "a = 0 ∨ b ∈ span S"
  shows "a ⋅⇩v b ∈ span S"
proof(cases "a = 0")
  case True
  then show ?thesis by (auto simp:lmult_0[OF assms(1)] span_zero)
next
  case False with assms have "b ∈ span S" by auto
  from this[THEN in_spanE]
  obtain aa A where a[intro!]: "b = lincomb aa A" "finite A" "A ⊆ S" by auto
  hence [intro!]:"(λv. aa v ⋅⇩v v) ∈ A → carrier_vec n" using assms by auto 
  show ?thesis proof
    show "a ⋅⇩v b = lincomb (λ v. a * aa v) A" using a(1) unfolding lincomb_def smult_smult_assoc[symmetric]
      by(subst finsum_smult[symmetric]) force+
  qed auto
qed

lemma det_nonzero_congruence:
  assumes eq:"A * M = B * M" and det:"det (M::'a mat) ≠ 0"
  and M: "M ∈ carrier_mat n n" and carr:"A ∈ carrier_mat n n" "B ∈ carrier_mat n n"
  shows "A = B"
proof -
  have "1⇩m n ∈ carrier_mat n n" by auto
  from det_non_zero_imp_unit[OF M det] gauss_jordan_check_invertable[OF M this]
  have gj_fst:"(fst (gauss_jordan M (1⇩m n)) = 1⇩m n)" by metis
  define Mi where "Mi = snd (gauss_jordan M (1⇩m n))"
  with gj_fst have gj:"gauss_jordan M (1⇩m n) = (1⇩m n, Mi)"
    unfolding fst_def snd_def by (auto split:prod.split)
  from gauss_jordan_compute_inverse(1,3)[OF M gj]
  have Mi: "Mi ∈ carrier_mat n n" and is1:"M * Mi = 1⇩m n" by metis+
  from arg_cong[OF eq, of "λ M. M * Mi"]
  show "A = B" unfolding carr[THEN assoc_mult_mat[OF _ M Mi]] is1 carr[THEN right_mult_one_mat].
qed

end


(* TODO: Is a function like this already in the library
   find_index is used to rewrite the sumlists in the lattice_of definition to finsums *)

fun find_index :: "'b list ⇒ 'b ⇒ nat" where
  "find_index [] _ = 0" |
  "find_index (x#xs) y = (if x = y then 0 else find_index xs y + 1)"

lemma find_index_not_in_set: "x ∉ set xs ⟷ find_index xs x = length xs"
  by (induction xs) auto

lemma find_index_in_set: "x ∈ set xs ⟹ xs ! (find_index xs x) = x"
  by (induction xs) auto

lemma find_index_inj: "inj_on (find_index xs) (set xs)"
  by (induction xs) (auto simp add: inj_on_def)

lemma find_index_leq_length: "find_index xs x < length xs ⟷ x ∈ set xs"
  by (induction xs) (auto)


context vec_module
begin
definition lattice_of :: "'a vec list ⇒ 'a vec set" where
  "lattice_of fs = range (λ c. sumlist (map (λ i. of_int (c i) ⋅⇩v fs ! i) [0 ..< length fs]))"

lemma lattice_of_finsum:
  assumes "set fs ⊆ carrier_vec n"
  shows "lattice_of fs = range (λ c. finsum V (λ i. of_int (c i) ⋅⇩v fs ! i) {0 ..< length fs})"
proof -
  have "sumlist (map (λ i. of_int (c i) ⋅⇩v fs ! i) [0 ..< length fs])
        = finsum V (λ i. of_int (c i) ⋅⇩v fs ! i) {0 ..< length fs}" for c
    using  assms by (subst sumlist_map_as_finsum) (fastforce)+
  then show ?thesis
    unfolding lattice_of_def by auto
qed

lemma in_latticeE: assumes "f ∈ lattice_of fs" obtains c where
    "f = sumlist (map (λ i. of_int (c i) ⋅⇩v fs ! i) [0 ..< length fs])" 
  using assms unfolding lattice_of_def by auto
    
lemma in_latticeI: assumes "f = sumlist (map (λ i. of_int (c i) ⋅⇩v fs ! i) [0 ..< length fs])" 
  shows "f ∈ lattice_of fs" 
  using assms unfolding lattice_of_def by auto

lemma finsum_over_indexes_to_vectors:
  assumes "set vs ⊆ carrier_vec n" "l = length vs"
  shows "∃c. (⨁⇘V⇙x∈{0..<l}. of_int (g x) ⋅⇩v vs ! x) = (⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)"
  using assms proof (induction l arbitrary: vs)
  case (Suc l)
  then obtain vs' v where vs'_def: "vs = vs' @ [v]"
    by (metis Zero_not_Suc length_0_conv rev_exhaust)
  have c: "∃c. (⨁⇘V⇙i∈{0..<l}. of_int (g i) ⋅⇩v vs' ! i) = (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)"
    using Suc vs'_def by (auto)
  then obtain c 
    where c_def: "(⨁⇘V⇙x∈{0..<l}. of_int (g x) ⋅⇩v vs' ! x) = (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)"
    by blast
  have "(⨁⇘V⇙x∈{0..<Suc l}. of_int (g x) ⋅⇩v vs ! x) 
        = of_int (g l) ⋅⇩v vs ! l + (⨁⇘V⇙x∈{0..<l}. of_int (g x) ⋅⇩v vs ! x)"
     using Suc by (subst finsum_insert[symmetric]) (fastforce intro!: finsum_cong')+
  also have "vs = vs' @ [v]"
    using vs'_def by simp
  also have "(⨁⇘V⇙x∈{0..<l}. of_int (g x) ⋅⇩v (vs' @ [v]) ! x) = (⨁⇘V⇙x∈{0..<l}. of_int (g x) ⋅⇩v vs' ! x)"
    using Suc vs'_def by (intro finsum_cong') (auto simp add: in_mono nth_append)
  also note c_def
  also have "(vs' @ [v]) ! l = v"
    using Suc vs'_def by auto
  also have "∃d'. of_int (g l) ⋅⇩v v + (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v) = (⨁⇘V⇙v∈set vs. of_int (d' v) ⋅⇩v v)"
  proof (cases "v ∈ set vs'")
    case True
    then have I: "set vs' = insert v (set vs' - {v})"
      by blast
    define c' where "c' x = (if x = v then c x + g l else c x)" for x
    have "of_int (g l) ⋅⇩v v + (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)
          = of_int (g l) ⋅⇩v v + (of_int (c v) ⋅⇩v v + (⨁⇘V⇙v∈set vs' - {v}. of_int (c v) ⋅⇩v v))"
      using Suc vs'_def by (subst I, subst finsum_insert) fastforce+
    also have "… = of_int (g l) ⋅⇩v v + of_int (c v) ⋅⇩v v + (⨁⇘V⇙v∈set vs' - {v}. of_int (c v) ⋅⇩v v)"
      using Suc vs'_def by (subst a_assoc) (auto intro!: finsum_closed)
    also have "of_int (g l) ⋅⇩v v + of_int (c v) ⋅⇩v v = of_int (c' v)  ⋅⇩v v"
      unfolding c'_def by (auto simp add: add_smult_distrib_vec)
    also have "(⨁⇘V⇙v∈set vs' - {v}. of_int (c v) ⋅⇩v v) = (⨁⇘V⇙v∈set vs' - {v}. of_int (c' v) ⋅⇩v v)"
      using Suc vs'_def unfolding c'_def by (intro finsum_cong') (auto)
    also have "of_int (c' v) ⋅⇩v v + (⨁⇘V⇙v∈set vs' - {v}. of_int (c' v) ⋅⇩v v)
               = (⨁⇘V⇙v∈insert v (set vs'). of_int (c' v) ⋅⇩v v)"
      using Suc vs'_def by (subst finsum_insert[symmetric]) (auto)
    finally show ?thesis
      using vs'_def by force
  next
    case False
    define c' where "c' x = (if x = v then g l else c x)" for x
    have "of_int (g l) ⋅⇩v v + (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)
          = of_int (c' v) ⋅⇩v v + (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)"
      unfolding c'_def by simp
    also have "(⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v) = (⨁⇘V⇙v∈set vs'. of_int (c' v) ⋅⇩v v)"
      unfolding c'_def using Suc False vs'_def by (auto intro!: finsum_cong')
    also have "of_int (c' v) ⋅⇩v v + (⨁⇘V⇙v∈set vs'. of_int (c' v) ⋅⇩v v)
               = (⨁⇘V⇙v∈insert v (set vs'). of_int (c' v) ⋅⇩v v)"
      using False Suc vs'_def by (subst finsum_insert[symmetric]) (auto)
    also have "(⨁⇘V⇙v∈set vs'. of_int (c' v) ⋅⇩v v) = (⨁⇘V⇙v∈set vs'. of_int (c v) ⋅⇩v v)"
      unfolding c'_def using False Suc vs'_def by (auto intro!: finsum_cong')
    finally show ?thesis
      using vs'_def by auto
  qed
  finally show ?case
    unfolding vs'_def by blast
qed (auto)

lemma lattice_of_altdef:
  assumes "set vs ⊆ carrier_vec n"
  shows "lattice_of vs = range (λc. ⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)"
proof -
  have "v ∈ lattice_of vs" if "v ∈ range (λc. ⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)" for v
  proof -
    obtain c where v: "v = (⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)"
      using ‹v ∈ range (λc. ⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)› by (auto)
    define c' where "c' i = (if find_index vs (vs ! i) = i then c (vs ! i) else 0)" for i
    have "v = (⨁⇘V⇙v∈set vs. of_int (c' (find_index vs v)) ⋅⇩v vs ! (find_index vs v))"
      unfolding v
      using assms by (auto intro!: finsum_cong' simp add: c'_def find_index_in_set in_mono)
    also have "… = (⨁⇘V⇙i∈find_index vs ` (set vs). of_int (c' i) ⋅⇩v vs ! i)"
      using assms find_index_in_set find_index_inj by (subst finsum_reindex) fastforce+
    also have "… = (⨁⇘V⇙i∈set [0..<length vs]. of_int (c' i) ⋅⇩v vs ! i)"
    proof -
      have "i ∈ find_index vs ` set vs" if "i < length vs" "find_index vs (vs ! i) = i" for i
        using that by (metis imageI nth_mem)
      then show ?thesis
        unfolding c'_def using find_index_leq_length assms 
        by (intro add.finprod_mono_neutral_cong_left) (auto simp add: in_mono find_index_leq_length)
    qed
    also have "… = sumlist (map (λi. of_int (c' i) ⋅⇩v vs ! i) [0..<length vs])"
      using assms by (subst sumlist_map_as_finsum) (fastforce)+
    finally show ?thesis
      unfolding lattice_of_def by blast
  qed
  moreover have "v ∈ range (λc. ⨁⇘V⇙v∈set vs. of_int (c v) ⋅⇩v v)" if "v ∈ lattice_of vs" for v
  proof -
    obtain c where "v = sumlist (map (λi. of_int (c i) ⋅⇩v vs ! i) [0..<length vs])"
      using ‹v ∈ lattice_of vs› unfolding lattice_of_def by (auto)
    also have "… = (⨁⇘V⇙x∈{0..<length vs}. of_int (c x) ⋅⇩v vs ! x)"
      using that assms by (subst sumlist_map_as_finsum) fastforce+
    also obtain d where  "… = (⨁⇘V⇙v∈set vs. of_int (d v) ⋅⇩v v)"
      using finsum_over_indexes_to_vectors assms by blast
    finally show ?thesis
      by blast
  qed
  ultimately show ?thesis
    by fastforce
qed

lemma basis_in_latticeI:
  assumes fs: "set fs ⊆ carrier_vec n" and "f ∈ set fs" 
  shows "f ∈ lattice_of fs"
proof -
  define c :: "'a vec ⇒ int" where "c v = (if v = f then 1 else 0)" for v
  have "f = (⨁⇘V⇙v∈{f}. of_int (c v) ⋅⇩v v)"
    using assms by (auto simp add: c_def)
  also have "… = (⨁⇘V⇙v∈set fs. of_int (c v) ⋅⇩v v)"
    using assms by (intro add.finprod_mono_neutral_cong_left) (auto simp add: c_def)
  finally show ?thesis
    using assms lattice_of_altdef by blast
qed

lemma lattice_of_eq_set:
  assumes "set fs = set gs" "set fs ⊆ carrier_vec n"
  shows "lattice_of fs = lattice_of gs"
  using assms lattice_of_altdef by simp

lemma lattice_of_swap: assumes fs: "set fs ⊆ carrier_vec n" 
  and ij: "i < length fs" "j < length fs" "i ≠ j" 
  and gs: "gs = fs[ i := fs ! j, j := fs ! i]" 
shows "lattice_of gs = lattice_of fs"
  using assms mset_swap by (intro lattice_of_eq_set) auto

lemma lattice_of_add: assumes fs: "set fs ⊆ carrier_vec n" 
  and ij: "i < length fs" "j < length fs" "i ≠ j" 
  and gs: "gs = fs[ i := fs ! i + of_int l ⋅⇩v fs ! j]" 
shows "lattice_of gs = lattice_of fs"
proof -
  {
    fix i j l and fs :: "'a vec list" 
    assume *: "i < j" "j < length fs" and fs: "set fs ⊆ carrier_vec n"
    note * = ij(1) *
    let ?gs = "fs[ i := fs ! i + of_int l ⋅⇩v fs ! j]"
    let ?len = "[0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]" 
    have "[0 ..< length fs] = [0 ..< j] @ [j] @ [Suc j ..< length fs]" using *
      by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append 
          upt_conv_Cons zero_less_Suc)
    also have "[0 ..< j] = [0 ..< i] @ [i] @ [Suc i ..< j]" using *
      by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append 
          upt_conv_Cons zero_less_Suc)
    finally have len: "[0..<length fs] = ?len" by simp
    from fs have fs: "⋀ i. i < length fs ⟹ fs ! i ∈ carrier_vec n" unfolding set_conv_nth by auto
    from fs have fsd: "⋀ i. i < length fs ⟹ dim_vec (fs ! i) = n" by auto
    from fsd[of i] fsd[of j] * have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n" by auto
    {
      fix f
      assume "f ∈ lattice_of fs" 
      from in_latticeE[OF this, unfolded len] obtain c where
        f: "f = sumlist (map (λi. of_int (c i) ⋅⇩v fs ! i) ?len)" by auto
      define sc where "sc = (λ xs. sumlist (map (λi. of_int (c i) ⋅⇩v fs ! i) xs))"
      define d where "d = (λ k. if k = j then c j - c i * l else c k)"
      define sd where "sd = (λ xs. sumlist (map (λi. of_int (d i) ⋅⇩v ?gs ! i) xs))"
      have isc: "set is ⊆ {0 ..< length fs} ⟹ sc is ∈ carrier_vec n" for "is" 
        unfolding sc_def by (intro sumlist_carrier, auto simp: fs)
      have isd: "set is ⊆ {0 ..< length fs} ⟹ sd is ∈ carrier_vec n" for "is" 
        unfolding sd_def using * by (intro sumlist_carrier, auto, rename_tac k,
        case_tac "k = i", auto simp: fs)
      let ?a = "sc [0..<i]" let ?b = "sc [i]" let ?c = "sc [Suc i ..< j]" let ?d = "sc [j]" 
      let ?e = "sc [Suc j ..< length fs]" 
      let ?A = "sd [0..<i]" let ?B = "sd [i]" let ?C = "sd [Suc i ..< j]" let ?D = "sd [j]" 
      let ?E = "sd [Suc j ..< length fs]" 
      let ?CC = "carrier_vec n" 
      have ae: "?a ∈ ?CC" "?b ∈ ?CC" "?c ∈ ?CC" "?d ∈ ?CC" "?e ∈ ?CC"  
        using * by (auto intro: isc)
      have AE: "?A ∈ ?CC" "?B ∈ ?CC" "?C ∈ ?CC" "?D ∈ ?CC" "?E ∈ ?CC"  
        using * by (auto intro: isd)
      have sc_sd: "{i,j} ∩ set is ⊆ {} ⟹ sc is = sd is" for "is" 
        unfolding sc_def sd_def by (rule arg_cong[of _ _ sumlist], rule map_cong, auto simp: d_def,
        rename_tac k, case_tac "i = k", auto)
      have "f = ?a + (?b + (?c + (?d + ?e)))"         
        unfolding f map_append sc_def using fs *
        by ((subst sumlist_append, force, force)+, simp)
      also have "… = ?a + ((?b + ?d) + (?c + ?e))" using ae by auto          
      also have "… = ?A + ((?b + ?d) + (?C + ?E))" 
        using * by (auto simp: sc_sd)
      also have "?b + ?d = ?B + ?D" unfolding sd_def sc_def d_def sumlist_def
        by (rule eq_vecI, insert * fsd, auto simp: algebra_simps)
      finally have "f = ?A + (?B + (?C + (?D + ?E)))" using AE by auto
      also have "… = sumlist (map (λi. of_int (d i) ⋅⇩v ?gs ! i) ?len)" 
        unfolding f map_append sd_def using fs *
        by ((subst sumlist_append, force, force)+, simp)
      also have "… = sumlist (map (λi. of_int (d i) ⋅⇩v ?gs ! i) [0 ..< length ?gs])"
        unfolding len[symmetric] by simp
      finally have "f = sumlist (map (λi. of_int (d i) ⋅⇩v ?gs ! i) [0 ..< length ?gs])" .
      from in_latticeI[OF this] have "f ∈ lattice_of ?gs" .
    }
    hence "lattice_of fs ⊆ lattice_of ?gs" by blast
  } note main = this 
  {
    fix i j and fs :: "'a vec list" 
    assume *: "i < j" "j < length fs" and fs: "set fs ⊆ carrier_vec n"
    let ?gs = "fs[ i := fs ! i + of_int l ⋅⇩v fs ! j]"
    define gs where "gs = ?gs" 
    from main[OF * fs, of l, folded gs_def]
    have one: "lattice_of fs ⊆ lattice_of gs" .
    have *: "i < j" "j < length gs" "set gs ⊆ carrier_vec n" using * fs unfolding gs_def set_conv_nth
      by (auto, rename_tac k, case_tac "k = i", (force intro!: add_carrier_vec)+)
    from fs have fs: "⋀ i. i < length fs ⟹ fs ! i ∈ carrier_vec n" unfolding set_conv_nth by auto
    from fs have fsd: "⋀ i. i < length fs ⟹ dim_vec (fs ! i) = n" by auto
    from fsd[of i] fsd[of j] * have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n" by (auto simp: gs_def)
    from main[OF *, of "-l"]
    have "lattice_of gs ⊆ lattice_of (gs[i := gs ! i + of_int (- l) ⋅⇩v gs ! j])" .
    also have "gs[i := gs ! i + of_int (- l) ⋅⇩v gs ! j] = fs" unfolding gs_def
      by (rule nth_equalityI, auto, insert * fsd, rename_tac k, case_tac "k = i", auto)
    ultimately have "lattice_of fs = lattice_of ?gs" using one unfolding gs_def by auto
  } note main = this
  show ?thesis
  proof (cases "i < j")
    case True
    from main[OF this ij(2) fs] show ?thesis unfolding gs by simp
  next
    case False
    with ij have ji: "j < i" by auto
    define hs where "hs = fs[i := fs ! j, j := fs ! i]" 
    define ks where "ks = hs[j := hs ! j + of_int l ⋅⇩v hs ! i]" 
    from ij fs have ij': "i < length hs" "set hs ⊆ carrier_vec n" unfolding hs_def by auto
    hence ij'': "set ks ⊆ carrier_vec n" "i < length ks" "j < length ks" "i ≠ j" 
      using ji unfolding ks_def set_conv_nth by (auto, rename_tac k, case_tac "k = i", 
        force, case_tac "k = j", (force intro!: add_carrier_vec)+)
    from lattice_of_swap[OF fs ij refl] 
    have "lattice_of fs = lattice_of hs" unfolding hs_def by auto
    also have "… = lattice_of ks" 
      using main[OF ji ij'] unfolding ks_def .
    also have "… = lattice_of (ks[i := ks ! j, j := ks ! i])" 
      by (rule sym, rule lattice_of_swap[OF ij'' refl])
    also have "ks[i := ks ! j, j := ks ! i] = gs" unfolding gs ks_def hs_def
      by (rule nth_equalityI, insert ij, auto, 
       rename_tac k, case_tac "k = i", force, case_tac "k = j", auto)
    finally show ?thesis by simp
  qed
qed

lemma lattice_of_altdef_lincomb:
  assumes "set fs ⊆ carrier_vec n"
  shows "lattice_of fs = {y. ∃f. lincomb (of_int ∘ f) (set fs) = y}"
  unfolding lincomb_def lattice_of_altdef[OF assms] image_def by auto


definition "orthogonal_complement W = {x. x ∈ carrier_vec n ∧ (∀y ∈ W. x ∙ y = 0)}"

lemma orthogonal_complement_subset:
  assumes "A ⊆ B"
  shows "orthogonal_complement B ⊆ orthogonal_complement A"
unfolding orthogonal_complement_def using assms by auto

end

context vec_space
begin


lemma in_orthogonal_complement_span[simp]:
  assumes [intro]:"S ⊆ carrier_vec n"
  shows "orthogonal_complement (span S) = orthogonal_complement S"
proof
  show "orthogonal_complement (span S) ⊆ orthogonal_complement S"
    by(fact orthogonal_complement_subset[OF in_own_span[OF assms]])
  {fix x :: "'a vec"
    fix a fix A :: "'a vec set"
    assume x [intro]:"x ∈ carrier_vec n" and f: "finite A" and S:"A ⊆ S"
    assume i0:"∀y∈S. x ∙ y = 0"
    have "x ∙ lincomb a A = 0"
      unfolding comm_scalar_prod[OF x lincomb_closed[OF subset_trans[OF S assms]]]
    proof(insert S,atomize(full),rule finite_induct[OF f],goal_cases)
      case 1 thus ?case using assms x by force
    next
      case (2 f F)
      { assume i:"insert f F ⊆ S"
        hence F:"F ⊆ S" and f: "f ∈ S" by auto
        from F f assms
        have [intro]:"F ⊆ carrier_vec n"
          and fc[intro]:"f ∈ carrier_vec n"
          and [intro]:"x ∈ F ⟹ x ∈ carrier_vec n" for x by auto
        have laf:"lincomb a F ∙ x = 0" using F 2 by auto
        have [simp]:"(∑u∈F. (a u ⋅⇩v u) ∙ x) = 0"
          by(insert laf[unfolded lincomb_def],atomize(full),subst finsum_scalar_prod_sum) auto
        from f i0 have [simp]:"f ∙ x = 0" by (subst comm_scalar_prod) auto
        from lincomb_closed[OF subset_trans[OF i assms]]
        have "lincomb a (insert f F) ∙ x = 0" unfolding lincomb_def
          apply(subst finsum_scalar_prod_sum,force,force)
          using 2(1,2) smult_scalar_prod_distrib[OF fc x] by auto
      } thus ?case by auto
      qed
  }
  thus "orthogonal_complement S ⊆ orthogonal_complement (span S)"
    unfolding orthogonal_complement_def span_def by auto
qed

end


context 
begin

interpretation vec_module "TYPE(int)" .

lemma lattice_of_cols_as_mat_mult:
  assumes A: "A ∈ carrier_mat n nc" (*Integer matrix*)
  shows "lattice_of (cols A) = {y∈carrier_vec (dim_row A). ∃x∈carrier_vec (dim_col A). A *⇩v x = y}"
proof -
  let ?ws = "cols A"
  have set_cols_in: "set (cols A) ⊆ carrier_vec n" using A unfolding cols_def by auto
  have "lincomb (of_int ∘ f)(set  ?ws) ∈ carrier_vec (dim_row A)" for f 
    using lincomb_closed A
    by (metis (full_types) carrier_matD(1) cols_dim lincomb_closed)
  moreover have "∃x∈carrier_vec (dim_col A). A *⇩v x = lincomb (of_int ∘ f) (set (cols A))" for f
  proof -    
    let ?g = "(λv. of_int (f v))"
    let ?g' = "(λi. if ∃j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"           
    have "lincomb (of_int ∘ f) (set (cols A)) = lincomb ?g (set ?ws)" unfolding o_def by auto
    also have "... = lincomb_list ?g' ?ws" 
      by (rule lincomb_as_lincomb_list[OF set_cols_in])
    also have "... = mat_of_cols n ?ws *⇩v vec (length ?ws) ?g'" 
      by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
    also have "... = A *⇩v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto
    finally show ?thesis by auto
  qed 
  moreover have "∃f. A *⇩v x = lincomb (of_int ∘ f) (set (cols A))" 
    if Ax: "A *⇩v x ∈ carrier_vec (dim_row A)" and x: "x ∈ carrier_vec (dim_col A)" for x 
  proof -
    let ?c = "λi. x $ i"
    have x_vec: "vec (length ?ws) ?c = x" using x by auto
    have "A *⇩v x = mat_of_cols n ?ws *⇩v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto
    also have "... = lincomb_list ?c ?ws"
      by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
    also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)" 
      by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)    
    finally show ?thesis by auto
  qed
  ultimately show ?thesis unfolding lattice_of_altdef_lincomb[OF set_cols_in]
    by (metis (mono_tags, opaque_lifting))
qed


corollary lattice_of_as_mat_mult:
  assumes fs: "set fs ⊆ carrier_vec n"
  shows "lattice_of fs = {y∈carrier_vec n. ∃x∈carrier_vec (length fs). (mat_of_cols n fs) *⇩v x = y}"
proof -
  have cols_eq: "cols (mat_of_cols n fs) = fs" using cols_mat_of_cols[OF fs] by simp
  have m: "(mat_of_cols n fs) ∈ carrier_mat n (length fs)" using mat_of_cols_carrier(1) by auto
  show ?thesis using lattice_of_cols_as_mat_mult[OF m] unfolding cols_eq using m by auto
qed
end



end