Theory Missing_VectorSpace

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

section ‹Missing Vector Spaces›

text ‹This theory provides some lemmas which we required when working with vector spaces.›

theory Missing_VectorSpace
imports
  VectorSpace.VectorSpace
  Missing_Ring
  "HOL-Library.Multiset"
begin


(**** The following lemmas that could be moved to HOL/Finite_Set.thy  ****)

(*This a generalization of comp_fun_commute. It is a similar definition, but restricted to a set. 
  When "A = UNIV::'a set", we have "comp_fun_commute_on f A = comp_fun_commute f"*)
locale comp_fun_commute_on = 
  fixes f :: "'a ⇒ 'a ⇒ 'a" and A::"'a set"
  assumes comp_fun_commute_restrict: "∀y∈A. ∀x∈A. ∀z∈A. f y (f x z) = f x (f y z)"
  and f: "f : A → A → A" 
begin

lemma comp_fun_commute_on_UNIV:
  assumes "A = (UNIV :: 'a set)"
  shows "comp_fun_commute f"
  unfolding comp_fun_commute_def 
  using assms comp_fun_commute_restrict f by auto

lemma fun_left_comm: 
  assumes "y ∈ A" and "x ∈ A" and "z ∈ A" shows "f y (f x z) = f x (f y z)"
  using comp_fun_commute_restrict assms by auto

lemma commute_left_comp: 
  assumes "y ∈ A" and "x∈A" and "z∈A" and "g ∈ A → A" 
  shows "f y (f x (g z)) = f x (f y (g z))"
  using assms by (auto simp add: Pi_def o_assoc comp_fun_commute_restrict)

lemma fold_graph_finite:
  assumes "fold_graph f z B y"
  shows "finite B"
  using assms by induct simp_all

lemma fold_graph_closed:
  assumes "fold_graph f z B y" and "B ⊆ A" and "z ∈ A"
  shows "y ∈ A"
  using assms 
proof (induct set: fold_graph)
  case emptyI
  then show ?case by auto
next
  case (insertI x B y)
  then show ?case using insertI f by auto
qed

lemma fold_graph_insertE_aux:
  "fold_graph f z B y ⟹ a ∈ B ⟹ z∈A
  ⟹ B ⊆ A
  ⟹  ∃y'. y = f a y' ∧ fold_graph f z (B - {a}) y' ∧ y' ∈ A"
proof (induct set: fold_graph)
  case emptyI
  then show ?case by auto
next
  case (insertI x B y)
  show ?case
  proof (cases "x = a")
    case True 
    show ?thesis
    proof (rule exI[of _ y])
      have B: "(insert x B - {a}) = B" using True insertI by auto 
      have "f x y = f a y" by (simp add: True) 
      moreover have "fold_graph f z (insert x B - {a}) y" by (simp add: B insertI)
      moreover have "y ∈ A" using insertI fold_graph_closed[of z B] by auto
      ultimately show " f x y = f a y ∧ fold_graph f z (insert x B - {a}) y ∧ y ∈ A" by simp
    qed
  next
    case False
    then obtain y' where y: "y = f a y'" and y': "fold_graph f z (B - {a}) y'" and y'_in_A: "y' ∈ A"
      using insertI f by auto
    have "f x y = f a (f x y')"
      unfolding y 
    proof (rule fun_left_comm)
      show "x ∈ A" using insertI by auto
      show "a ∈ A" using insertI by auto
      show "y' ∈ A" using y'_in_A by auto
    qed  
    moreover have "fold_graph f z (insert x B - {a}) (f x y')"
      using y' and ‹x ≠ a› and ‹x ∉ B›
      by (simp add: insert_Diff_if fold_graph.insertI)    
    moreover have "(f x y') ∈ A" using insertI f y'_in_A by auto
    ultimately show ?thesis using y'_in_A
      by auto
  qed
qed
    
lemma fold_graph_insertE:
  assumes "fold_graph f z (insert x B) v" and "x ∉ B" and "insert x B ⊆ A" and "z∈A"
  obtains y where "v = f x y" and "fold_graph f z B y"
  using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])

lemma fold_graph_determ: "fold_graph f z B x ⟹ fold_graph f z B y ⟹  B ⊆ A ⟹ z∈A ⟹ y = x"
proof (induct arbitrary: y set: fold_graph)
  case emptyI
  then show ?case
    by (meson empty_fold_graphE)
next
  case (insertI x B y v)
  from ‹fold_graph f z (insert x B) v› and ‹x ∉ B› and ‹insert x B ⊆ A› and  ‹z ∈ A›
  obtain y' where "v = f x y'" and "fold_graph f z B y'"
    by (rule fold_graph_insertE)
  from ‹fold_graph f z B y'› and ‹insert x B ⊆ A› have "y' = y" using insertI by auto    
  with ‹v = f x y'› show "v = f x y"
    by simp
qed

lemma fold_equality: "fold_graph f z B y ⟹ B ⊆ A ⟹ z ∈ A ⟹ Finite_Set.fold f z B = y"
  by (cases "finite B") 
  (auto simp add: Finite_Set.fold_def intro: fold_graph_determ dest: fold_graph_finite)
    
lemma fold_graph_fold:
  assumes f: "finite B" and BA: "B⊆A" and z: "z ∈ A"
  shows "fold_graph f z B (Finite_Set.fold f z B)"
proof -
   have "∃x. fold_graph f z B x"
    by (rule finite_imp_fold_graph[OF f])
  moreover note fold_graph_determ
  ultimately have "∃!x. fold_graph f z B x" using f BA z by auto    
  then have "fold_graph f z B (The (fold_graph f z B))"
    by (rule theI')
  with assms show ?thesis
    by (simp add: Finite_Set.fold_def)
qed
  
(*This lemma is a generalization of thm comp_fun_commute.fold_insert*)
lemma fold_insert [simp]:
  assumes "finite B" and "x ∉ B" and BA: "insert x B ⊆ A" and z: "z ∈ A"
  shows "Finite_Set.fold f z (insert x B) = f x (Finite_Set.fold f z B)"
  proof (rule fold_equality[OF _ BA z])
  from ‹finite B› have "fold_graph f z B (Finite_Set.fold f z B)"
   using BA fold_graph_fold z by auto
  hence "fold_graph f z (insert x B) (f x (Finite_Set.fold f z B))"
    using BA  fold_graph.insertI assms by auto
  then show "fold_graph f z (insert x B) (f x (Finite_Set.fold f z B))"
    by simp
qed
end

(*This lemma is a generalization of thm Finite_Set.fold_cong *)
lemma fold_cong:
  assumes f: "comp_fun_commute_on f A" and g: "comp_fun_commute_on g A"
    and "finite S"
    and cong: "⋀x. x ∈ S ⟹ f x = g x"
    and "s = t" and "S = T" 
    and SA: "S ⊆ A" and s: "s∈A"
  shows "Finite_Set.fold f s S = Finite_Set.fold g t T"
proof -
  have "Finite_Set.fold f s S = Finite_Set.fold g s S"
    using ‹finite S› cong SA s
  proof (induct S)
    case empty
    then show ?case by simp
  next
    case (insert x F)
    interpret f: comp_fun_commute_on f A by (fact f)
    interpret g: comp_fun_commute_on g A by (fact g)
    show ?case  using insert by auto
  qed
  with assms show ?thesis by simp
qed
                    
context comp_fun_commute_on
begin  

lemma comp_fun_Pi: "(λx. f x ^^ g x) ∈ A → A → A"
proof -    
  have "(f x ^^ g x) y ∈ A" if y: "y ∈ A" and x: "x ∈ A" for x y
    using x y
   proof (induct "g x" arbitrary: g)
     case 0
     then show ?case by auto
   next
     case (Suc n g)
     define h where "h z = g z - 1" for z
     have hyp: "(f x ^^ h x) y ∈ A" 
       using h_def Suc.prems Suc.hyps diff_Suc_1 by metis
     have "g x = Suc (h x)" unfolding h_def
       using Suc.hyps(2) by auto     
     then show ?case using f x hyp unfolding Pi_def by auto
   qed 
  thus ?thesis by (auto simp add: Pi_def)
qed

(*This lemma is a generalization of thm comp_fun_commute.comp_fun_commute_funpow *)
lemma comp_fun_commute_funpow: "comp_fun_commute_on (λx. f x ^^ g x) A"
proof -
  have f: " (f y ^^ g y) ((f x ^^ g x) z) = (f x ^^ g x) ((f y ^^ g y) z)"
    if x: "x∈A" and y: "y ∈ A" and z: "z ∈ A" for x y z
  proof (cases "x = y")
    case False
    show ?thesis
    proof (induct "g x" arbitrary: g)
      case (Suc n g)
      have hyp1: "(f y ^^ g y) (f x k) = f x ((f y ^^ g y) k)" if k: "k ∈ A" for k
      proof (induct "g y" arbitrary: g)
        case 0
        then show ?case by simp
      next
        case (Suc n g)       
        define h where "h z = g z - 1" for z
        with Suc have "n = h y"
          by simp
        with Suc have hyp: "(f y ^^ h y) (f x k) = f x ((f y ^^ h y) k)"
          by auto
        from Suc h_def have g: "g y = Suc (h y)"
          by simp
        have "((f y ^^ h y) k) ∈ A" using y k comp_fun_Pi[of h] unfolding Pi_def by auto
        then show ?case
          by (simp add: comp_assoc g hyp) (auto simp add: o_assoc comp_fun_commute_restrict x y k)
      qed
      define h where "h a = (if a = x then g x - 1 else g a)" for a
      with Suc have "n = h x"
        by simp
      with Suc have "(f y ^^ h y) ((f x ^^ h x) z) = (f x ^^ h x) ((f y ^^ h y) z)"
        by auto
      with False have Suc2: "(f x ^^ h x) ((f y ^^ g y) z) = (f y ^^ g y) ((f x ^^ h x) z)"
        using h_def by auto      
      from Suc h_def have g: "g x = Suc (h x)"
        by simp
      have "(f x ^^ h x) z ∈A" using comp_fun_Pi[of h] x z unfolding Pi_def by auto
      hence *: "(f y ^^ g y) (f x ((f x ^^ h x) z)) = f x ((f y ^^ g y) ((f x ^^ h x) z))" 
        using hyp1 by auto
      thus ?case using g Suc2 by auto
    qed simp
  qed simp
  thus ?thesis by (auto simp add: comp_fun_commute_on_def comp_fun_Pi o_def)
qed

(*This lemma is a generalization of thm comp_fun_commute.fold_mset_add_mset*)
lemma fold_mset_add_mset: 
  assumes MA: "set_mset M ⊆ A" and s: "s ∈ A" and x: "x ∈ A"
  shows "fold_mset f s (add_mset x M) = f x (fold_mset f s M)"
proof -
  interpret mset: comp_fun_commute_on "λy. f y ^^ count M y" A
    by (fact comp_fun_commute_funpow)
  interpret mset_union: comp_fun_commute_on "λy. f y ^^ count (add_mset x M) y" A
    by (fact comp_fun_commute_funpow)
  show ?thesis
  proof (cases "x ∈ set_mset M")
    case False
    then have *: "count (add_mset x M) x = 1"
      by (simp add: not_in_iff)
     have "Finite_Set.fold (λy. f y ^^ count (add_mset x M) y) s (set_mset M) =
      Finite_Set.fold (λy. f y ^^ count M y) s (set_mset M)"
       by (rule fold_cong[of _ A], auto simp add: assms False comp_fun_commute_funpow)
    with False * s MA x show ?thesis
      by (simp add: fold_mset_def del: count_add_mset)
  next
    case True
    let ?f = "(λxa. f xa ^^ count (add_mset x M) xa)"
    let ?f2 = "(λx. f x ^^ count M x)"
    define N where "N = set_mset M - {x}"
    have F: "Finite_Set.fold ?f s (insert x N) = ?f x (Finite_Set.fold ?f s N)" 
      by (rule mset_union.fold_insert, auto simp add: assms N_def)
    have F2: "Finite_Set.fold ?f2 s (insert x N) = ?f2 x (Finite_Set.fold ?f2 s N)"
      by (rule mset.fold_insert, auto simp add: assms N_def)
    from N_def True have *: "set_mset M = insert x N" "x ∉ N" "finite N" by auto
    then have "Finite_Set.fold (λy. f y ^^ count (add_mset x M) y) s N =
      Finite_Set.fold (λy. f y ^^ count M y) s N" 
      using MA N_def s 
      by (auto intro!: fold_cong comp_fun_commute_funpow)
    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset, unfold F F2, auto)      
  qed
qed
end

(**** End of the lemmas that could be moved to HOL/Finite_Set.thy  ****)


lemma Diff_not_in: "a ∉ A - {a}" by auto

context abelian_group begin

lemma finsum_restrict:
  assumes fA: "f : A → carrier G"
      and restr: "restrict f A = restrict g A"
  shows "finsum G f A = finsum G g A"
proof (rule finsum_cong';rule?)
  fix a assume a: "a : A"
  have "f a = restrict f A a" using a by simp
  also have "... = restrict g A a" using restr by simp
  also have "... = g a" using a by simp
  finally show "f a = g a".
  thus "g a : carrier G" using fA a by force
qed

lemma minus_nonzero: "x : carrier G ⟹ x ≠ 𝟬 ⟹ ⊖ x ≠ 𝟬"
  using r_neg by force

end

lemma (in ordered_comm_monoid_add) positive_sum:
  assumes X : "finite X"
      and "f : X → { y :: 'a. y ≥ 0 }"
  shows "sum f X ≥ 0 ∧ (sum f X = 0 ⟶ f ` X ⊆ {0})"
  using assms
proof (induct set:finite)
  case (insert x X)
    hence x0: "f x ≥ 0" and sum0: "sum f X ≥ 0" by auto
    hence "sum f (insert x X) ≥ 0" using insert by auto
    moreover
    { assume "sum f (insert x X) = 0"
      hence "f x = 0" "sum f X = 0"
        using sum0 x0 insert add_nonneg_eq_0_iff by auto
    }
    ultimately show ?case using insert by blast
qed auto


lemma insert_union: "insert x X = X ∪ {x}" by auto


context vectorspace begin

lemmas lincomb_insert2 = lincomb_insert[unfolded insert_union[symmetric]]

lemma lincomb_restrict:
  assumes U: "U ⊆ carrier V"
      and a: "a : U → carrier K"
      and restr: "restrict a U = restrict b U"
  shows "lincomb a U = lincomb b U"
proof -
  let ?f = "λa u. a u ⊙⇘V⇙ u"
  have fa: "?f a : U → carrier V" using a U by auto
  have "restrict (?f a) U = restrict (?f b) U"
  proof
    fix u
    have "u : U ⟹ a u = b u" using restr unfolding restrict_def by metis
    thus "restrict (?f a) U u = restrict (?f b) U u" by auto
  qed
  thus ?thesis
    unfolding lincomb_def using finsum_restrict[OF fa] by auto
qed

lemma lindep_span:
  assumes U: "U ⊆ carrier V" and finU: "finite U"
  shows "lin_dep U = (∃u ∈ U. u ∈ span (U - {u}))" (is "?l = ?r")
proof
  assume l: "?l" show "?r"
  proof -
    from l[unfolded lin_dep_def]
    obtain A a u
    where finA: "finite A"
      and AU: "A ⊆ U"
      and aA: "a : A → carrier K"
      and aA0: "lincomb a A = zero V"
      and uA: "u:A"
      and au0: "a u ≠ zero K" by auto
    define a' where "a' = (λv. (if v : A then a v else zero K))"
    have a'U: "a' : U → carrier K" unfolding a'_def using aA by auto
    have uU: "u : U" using uA AU by auto
    have a'u0: "a' u ≠ zero K" unfolding a'_def using au0 uA by auto
    define B where "B = U - A"
    have B: "B ⊆ carrier V" unfolding B_def using U by auto
    have UAB: "U = A ∪ B" unfolding B_def using AU by auto
    have finB: "finite B" using finU B_def by auto
    have AB: "A ∩ B = {}" unfolding B_def by auto
    let ?f = "λv. a v ⊙⇘V⇙ v"
    have fA: "?f : A → carrier V" unfolding a'_def using aA AU U by auto
    let ?f' = "λv. a' v ⊙⇘V⇙ v"
    have "restrict ?f A = restrict ?f' A" unfolding a'_def by auto
    hence finsum: "finsum V ?f' A = finsum V ?f A"
      using finsum_restrict[OF fA] by simp
    have f'A: "?f' : A → carrier V"
    proof
      fix x assume xA: "x ∈ A"
      show "?f' x : carrier V" unfolding a'_def using aA xA AU U by auto
    qed
    have f'B: "?f' : B → carrier V"
    proof
      fix x assume xB: "x : B"
      have "x ∉ A" using a'U xB unfolding B_def by auto
      thus "?f' x : carrier V"using xB B unfolding a'_def by auto
    qed
    have sumB0: "finsum V ?f' B = zero V"
    proof -
      { fix B'
        have "finite B' ⟹ B' ⊆ B ⟹ finsum V ?f' B' = zero V"
        proof(induct set:finite)
          case (insert b B')
            have finB': "finite B'" and bB': "b ∉ B'" using insert by auto
            have f'B': "?f' : B' → carrier V" using f'B insert by auto
            have bA: "b ∉ A" using insert unfolding B_def by auto
            have b: "b : carrier V" using insert B by auto
            have foo: "a' b ⊙⇘V⇙ b ∈ carrier V" unfolding a'_def using bA b by auto
            have IH: "finsum V ?f' B' = zero V" using insert by auto
            show ?case
              unfolding finsum_insert[OF finB' bB' f'B' foo]
              using IH a'_def bA b by auto
         qed auto
      }
      thus ?thesis using finB by auto
    qed
    have a'A0: "lincomb a' U = zero V"
      unfolding UAB
      unfolding lincomb_def
      unfolding finsum_Un_disjoint[OF finA finB AB f'A f'B]
      unfolding finsum
      unfolding aA0[unfolded lincomb_def]
      unfolding sumB0 by simp
    have uU: "u:U" using uA AU by auto
    moreover have "u : span (U - {u})"
      using lincomb_isolate(2)[OF finU U a'U uU a'u0 a'A0].
    ultimately show ?r by auto
  qed
  next assume r: "?r" show "?l"
  proof -
    from r obtain u where uU: "u : U" and uspan: "u : span (U-{u})" by auto
    hence u: "u : carrier V" using U by auto
    have finUu: "finite (U-{u})" using finU by auto
    have Uu: "U-{u} ⊆ carrier V" using U by auto
    obtain a
      where ulin: "u = lincomb a (U-{u})"
        and a: "a : U-{u} → carrier K"
      using uspan unfolding finite_span[OF finUu Uu] by auto
    show "?l" unfolding lin_dep_def
    proof(intro exI conjI)
      let ?a = "λv. if v = u then ⊖⇘K⇙ one K else a v"
      show "?a : U → carrier K" using a by auto
      hence a': "?a : U-{u}∪{u} → carrier K" by auto
      have "U = U-{u}∪{u}" using uU by auto
      also have "lincomb ?a ... = ?a u ⊙⇘V⇙ u ⊕⇘V⇙ lincomb ?a (U-{u})"
        unfolding lincomb_insert[OF finUu Uu a' Diff_not_in u] by auto
      also have "restrict a (U-{u}) = restrict ?a (U-{u})" by auto
        hence "lincomb ?a (U-{u}) = lincomb a (U-{u})"
          using lincomb_restrict[OF Uu a] by auto
      also have "?a u ⊙⇘V⇙ u = ⊖⇘V⇙ u" using smult_minus_1[OF u] by simp
      also have "lincomb a (U-{u}) = u" using ulin..
      also have "⊖⇘V⇙ u ⊕⇘V⇙ u = zero V" using l_neg[OF u].
      finally show "lincomb ?a U = zero V" by auto
    qed (insert uU finU, auto)
  qed
qed

lemma not_lindepD:
  assumes "~ lin_dep S"
      and "finite A" "A ⊆ S" "f : A → carrier K" "lincomb f A = zero V"
    shows "f : A → {zero K}"
  using assms unfolding lin_dep_def by blast


lemma span_mem:
  assumes E: "E ⊆ carrier V" and uE: "u : E" shows "u : span E"
  unfolding span_def
proof (rule,intro exI conjI)
  show "u = lincomb (λ_. one K) {u}" unfolding lincomb_def using uE E by auto
  show "{u} ⊆ E" using uE by auto
qed auto

lemma lincomb_distrib:
  assumes U: "U ⊆ carrier V"
      and a: "a : U → carrier K"
      and c: "c : carrier K"
  shows "c ⊙⇘V⇙ lincomb a U = lincomb (λu. c ⊗⇘K⇙ a u) U"
    (is "_ = lincomb ?b U")
  using U a
proof (induct U rule: infinite_finite_induct)
  case empty show ?case unfolding lincomb_def using c by simp next
  case (insert u U)
    then have U: "U ⊆ carrier V"
          and u: "u : carrier V"
          and a: "a : insert u U → carrier K"
          and finU: "finite U" by auto
    hence aU: "a : U → carrier K" by auto
    have b: "?b : insert u U → carrier K" using a c by auto
    show ?case
      unfolding lincomb_insert2[OF finU U a ‹u∉U› u]
      unfolding lincomb_insert2[OF finU U b ‹u∉U› u]
      using insert U aU c u smult_r_distr smult_assoc1 by auto next
  case (infinite U)
    thus ?case unfolding lincomb_def using assms by simp
qed

lemma span_swap:
  assumes finE[simp]: "finite E"
      and E[simp]: "E ⊆ carrier V"
      and u[simp]: "u : carrier V"
      and usE: "u ∉ span E"
      and v[simp]: "v : carrier V"
      and usEv: "u : span (insert v E)"
  shows "span (insert u E) ⊆ span (insert v E)" (is "?L ⊆ ?R")
proof -
  have Eu[simp]: "insert u E ⊆ carrier V" by auto
  have Ev[simp]: "insert v E ⊆ carrier V" by auto
  have finEu: "finite (insert u E)" and finEv: "finite (insert v E)"
    using finE by auto
  have uE: "u ∉ E" using usE span_mem by force
  have vE: "v ∉ E"
  proof
    assume "v : E"
    hence EvE: "insert v E = E" using insert_absorb by auto
    hence "u : span E" using usEv by auto
    thus "False" using usE by auto
  qed
  obtain ua
    where ua[simp]: "ua : (insert v E) → carrier K"
      and uua: "u = lincomb ua (insert v E)"
    using usEv finite_span[OF finEv Ev]  by auto
  hence uaE[simp]: "ua : E → carrier K" and [simp]: "ua v : carrier K"
    by auto

  show "?L ⊆ ?R"
  proof
    fix x assume "x : ?L"
    then obtain xa
    where xa: "xa : insert u E → carrier K"
      and xxa: "x = lincomb xa (insert u E)"
      unfolding finite_span[OF finEu Eu] by auto
    hence xaE[simp]: "xa : E → carrier K" and xau[simp]: "xa u : carrier K" by auto
    show "x : span (insert v E)"
      unfolding finite_span[OF finEv Ev]
    proof (rule,intro exI conjI)
      define a where "a = (λe. xa u ⊗⇘K⇙ ua e)"
      define a' where "a' = (λe. a e ⊕⇘K⇙ xa e)"
      define a'' where "a'' = (λe. if e = v then xa u ⊗⇘K⇙ ua v else a' e)"
      have aE: "a : E → carrier K" unfolding a_def using xau uaE u by blast
      hence a'E: "a' : E → carrier K" unfolding a'_def using xaE by blast
      thus a'': "a'' : insert v E → carrier K" unfolding a''_def by auto
      have restr: "restrict a' E = restrict a'' E"
        unfolding a''_def using vE by auto
      have "x = xa u ⊙⇘V⇙ u ⊕⇘V⇙ lincomb xa E"
        using xxa lincomb_insert2 finE E xa uE u by auto
      also have
        "xa u ⊙⇘V⇙ u = xa u ⊙⇘V⇙ lincomb ua (insert v E)"
        using uua by auto
      also have "lincomb ua (insert v E) = ua v ⊙⇘V⇙ v ⊕⇘V⇙ lincomb ua E"
        using lincomb_insert2 finE E ua vE v by auto
      also have "xa u ⊙⇘V⇙ ... = xa u ⊙⇘V⇙ (ua v ⊙⇘V⇙ v) ⊕⇘V⇙ xa u ⊙⇘V⇙ lincomb ua E"
        using smult_r_distr by auto
      also have "xa u ⊙⇘V⇙ lincomb ua E = lincomb a E"
        unfolding a_def using lincomb_distrib[OF E] by auto
      finally have "x = xa u ⊙⇘V⇙ (ua v ⊙⇘V⇙ v) ⊕⇘V⇙ (lincomb a E ⊕⇘V⇙ lincomb xa E)"
        using a_assoc xau v aE xaE by auto
      also have "lincomb a E ⊕⇘V⇙ lincomb xa E = lincomb a' E"
        unfolding a'_def using lincomb_sum[OF finE E aE xaE]..
      also have "... = lincomb a'' E"
        using lincomb_restrict[OF E a'E ] restr by auto
      finally have "x = ((xa u ⊗⇘K⇙ ua v) ⊙⇘V⇙ v) ⊕⇘V⇙ lincomb a'' E"
        using smult_assoc1 by auto
      also have "xa u ⊗⇘K⇙ ua v = a'' v" unfolding a''_def by simp
      also have "(a'' v ⊙⇘V⇙ v) ⊕⇘V⇙ lincomb a'' E = lincomb a'' (insert v E)"
        using lincomb_insert2[OF finE E a'' vE] by auto
      finally show "x = lincomb a'' (insert v E)".
    qed
  qed
qed

lemma basis_swap:
  assumes finE[simp]: "finite E"
      and u[simp]: "u : carrier V"
      and uE[simp]: "u ∉ E"
      and b: "basis (insert u E)"
      and v[simp]: "v : carrier V"
      and uEv: "u : span (insert v E)"
  shows "basis (insert v E)"
  unfolding basis_def
proof (intro conjI)
  have Eu[simp]: "insert u E ⊆ carrier V"
   and spanEu: "carrier V = span (insert u E)"
   and indEu: "~ lin_dep (insert u E)"
    using b[unfolded basis_def] by auto
  hence E[simp]: "E ⊆ carrier V" by auto
  thus Ev[simp]: "insert v E ⊆ carrier V" using v by auto
  have finEu: "finite (insert u E)"
   and finEv: "finite (insert v E)" using finE by auto
  have usE: "u ∉ span E"
  proof
    assume "u : span E"
    hence "u : span (insert u E - {u})" using uE by auto
    moreover have "u : insert u E" by auto
    ultimately have "lin_dep (insert u E)"
      unfolding lindep_span[OF Eu finEu] by auto
    thus "False" using b unfolding basis_def by auto
  qed

  obtain ua
    where ua[simp]: "ua : insert v E → carrier K"
      and uua: "u = lincomb ua (insert v E)"
    using uEv finite_span[OF finEv Ev]  by auto
  hence uaE[simp]: "ua : E → carrier K"
    and uav[simp]: "ua v : carrier K"
    by auto

  have vE: "v ∉ E"
  proof
    assume "v : E"
    hence EvE: "insert v E = E" using insert_absorb by auto
    hence "u : span E" using uEv by auto
    thus "False" using usE by auto
  qed
  have vsE: "v ∉ span E"
  proof
    assume "v : span E"
    then obtain va
      where va[simp]: "va : E → carrier K"
        and vva: "v = lincomb va E"
      using finite_span[OF finE E] by auto
    define va' where "va' = (λe. ua v ⊗⇘K⇙ va e)"
    define va'' where "va'' = (λe. va' e ⊕⇘K⇙ ua e)"
    have va'[simp]: "va' : E → carrier K"
      unfolding va'_def using uav va by blast
    hence va''[simp]: "va'' : E → carrier K"
      unfolding va''_def using ua by blast
    from uua
    have "u = ua v ⊙⇘V⇙ v ⊕⇘V⇙ lincomb ua E"
      using lincomb_insert2 vE by auto
    also have "ua v ⊙⇘V⇙ v = ua v ⊙⇘V⇙ (lincomb va E)"
      using vva by auto
    also have "... = lincomb va' E"
      unfolding va'_def using lincomb_distrib by auto
    finally have "u = lincomb va'' E"
      unfolding va''_def
      using lincomb_sum[OF finE E] by auto
    hence "u : span E" using finite_span[OF finE E] va'' by blast
    hence "lin_dep (insert u E)" using lindep_span by simp
    then show False using indEu by auto
  qed

  have indE: "~ lin_dep E" using indEu subset_li_is_li by auto

  show "~ lin_dep (insert v E)" using lin_dep_iff_in_span[OF E indE v vE] vsE by auto

  show "span (insert v E) = carrier V" (is "?L = ?R")
  proof (rule)
    show "?L ⊆ ?R"
    proof
      have finEv: "finite (insert v E)" using finE by auto
      fix x assume "x : ?L"
      then obtain a
        where a: "a : insert v E → carrier K"
          and x: "x = lincomb a (insert v E)"
        unfolding finite_span[OF finEv Ev] by auto
      from a have av: "a v : carrier K" by auto
      from a have a2: "a : E → carrier K" by auto
      show "x : ?R"
        unfolding x
        unfolding lincomb_insert2[OF finE E a vE v]
        using lincomb_closed[OF E a2] av v
        by auto
    qed
    show "?R ⊆ ?L"
      using span_swap[OF finE E u usE v uEv] spanEu by auto
  qed
qed

lemma span_empty: "span {} = {zero V}"
  unfolding finite_span[OF finite.emptyI empty_subsetI]
  unfolding lincomb_def by simp

lemma span_self: assumes [simp]: "v : carrier V" shows "v : span {v}"
proof -
  have "v = lincomb (λx. one K) {v}" unfolding lincomb_def by auto
  thus ?thesis using finite_span by auto
qed

lemma span_zero: "zero V : span U" unfolding span_def lincomb_def by force

definition emb where "emb f D x = (if x : D then f x else zero K)"

lemma emb_carrier[simp]: "f : D → R ⟹ emb f D : D → R"
  apply rule unfolding emb_def by auto

lemma emb_restrict: "restrict (emb f D) D = restrict f D"
  apply rule unfolding restrict_def emb_def by auto

lemma emb_zero: "emb f D : X - D → { zero K }"
  apply rule unfolding emb_def by auto

lemma lincomb_clean:
  assumes A: "A ⊆ carrier V"
    and Z: "Z ⊆ carrier V"
    and finA: "finite A"
    and finZ: "finite Z"
    and aA: "a : A → carrier K"
    and aZ: "a : Z → { zero K }"
  shows "lincomb a (A ∪ Z) = lincomb a A"
  using finZ Z aZ
proof(induct set:finite)
  case empty thus ?case by simp next
  case (insert z Z) show ?case
    proof (cases "z : A")
      case True hence "A ∪ insert z Z = A ∪ Z" by auto
        thus ?thesis using insert by simp next
      case False
        have finAZ: "finite (A ∪ Z)" using finA insert by simp
        have AZ: "A ∪ Z ⊆ carrier V" using A insert by simp
        have a: "a : insert z (A ∪ Z) → carrier K" using insert aA by force
        have "a z = zero K" using insert by auto
        also have "... ⊙⇘V⇙ z = zero V" using insert by auto
        also have "... ⊕⇘V⇙ lincomb a (A ∪ Z) = lincomb a (A ∪ Z)"
          using insert AZ aA by auto
        also have "... = lincomb a A" using insert by simp
        finally have "a z ⊙⇘V⇙ z ⊕⇘V⇙ lincomb a (A ∪ Z) = lincomb a A".
        thus ?thesis
          using lincomb_insert2[OF finAZ AZ a] False insert by auto
    qed
qed

lemma span_add1:
  assumes U: "U ⊆ carrier V" and v: "v : span U" and w: "w : span U"
  shows "v ⊕⇘V⇙ w : span U"
proof -
  from v obtain a A
    where finA: "finite A"
      and va: "lincomb a A = v"
      and AU: "A ⊆ U"
      and a: "a : A → carrier K"
    unfolding span_def by auto
  hence A: "A ⊆ carrier V" using U by auto
  from w obtain b B
    where finB: "finite B"
      and wb: "lincomb b B = w"
      and BU: "B ⊆ U"
      and b: "b : B → carrier K"
    unfolding span_def by auto
  hence B: "B ⊆ carrier V" using U by auto

  have B_A: "B - A ⊆ carrier V" and A_B: "A - B ⊆ carrier V" using A B by auto

  have a': "emb a A : A ∪ B → carrier K"
    apply (rule Pi_I) unfolding emb_def using a by auto
  hence a'A: "emb a A : A → carrier K" by auto
  have a'Z: "emb a A : B - A → { zero K }"
    apply (rule Pi_I) unfolding emb_def using a by auto

  have b': "emb b B : A ∪ B → carrier K"
    apply (rule Pi_I) unfolding emb_def using b by auto
  hence b'B: "emb b B : B → carrier K" by auto
  have b'Z: "emb b B : A - B → { zero K }"
    apply (rule Pi_I) unfolding emb_def using b by auto

  show ?thesis
    unfolding span_def
    proof (rule,intro exI conjI)
      let ?v = "lincomb (emb a A) (A ∪ B)"
      let ?w = "lincomb (emb b B) (A ∪ B)"
      let ?ab = "λu. (emb a A) u ⊕⇘K⇙ (emb b B) u"
      show finAB: "finite (A ∪ B)" using finA finB by auto
      show "A ∪ B ⊆ U" using AU BU by auto
      show "?ab : A ∪ B → carrier K" using a' b' by auto
      have "v = ?v"
        using va lincomb_restrict[OF A a emb_restrict[symmetric]]
        using lincomb_clean[OF A B_A] a'A a'Z finA finB by simp
      moreover have "w = ?w"
        apply (subst Un_commute)
        using wb lincomb_restrict[OF B b emb_restrict[symmetric]]
        using lincomb_clean[OF B A_B] finA finB b'B b'Z by simp
      ultimately show "v ⊕⇘V⇙ w = lincomb ?ab (A ∪ B)"
        using lincomb_sum[OF finAB] A B a' b' by simp
    qed
qed

lemma span_neg:
  assumes U: "U ⊆ carrier V" and vU: "v : span U"
  shows "⊖⇘V⇙ v : span U"
proof -
  have v: "v : carrier V" using vU U unfolding span_def by auto
  from vU[unfolded span_def]
  obtain a A
    where finA: "finite A"
      and AU: "A ⊆ U"
      and a: "a ∈ A → carrier K"
      and va: "v = lincomb a A" by auto
  hence A: "A ⊆ carrier V" using U by simp
  let ?a = "λu. ⊖⇘K⇙ one K ⊗⇘K⇙ a u"

  have "⊖⇘V⇙ v = ⊖⇘K⇙ one K ⊙⇘V⇙ v" using smult_minus_1_back[OF v].
  also have "... = ⊖⇘K⇙ one K ⊙⇘V⇙ lincomb a A" using va by simp
  finally have main: "⊖⇘V⇙ v = lincomb ?a A"
    unfolding lincomb_distrib[OF A a R.a_inv_closed[OF R.one_closed]] by auto
  show ?thesis
    unfolding span_def
    apply rule
    using main a finA AU by force
qed

lemma span_closed[simp]: "U ⊆ carrier V ⟹ v : span U ⟹ v : carrier V"
  unfolding span_def by auto

lemma span_add:
  assumes U: "U ⊆ carrier V" and vU: "v : span U" and w[simp]: "w : carrier V"
  shows "w : span U ⟷ v ⊕⇘V⇙ w : span U" (is "?L ⟷ ?R")
proof
  show "?L ⟹ ?R" using span_add1[OF U vU] by auto
  assume R: "?R" show "?L"
  proof -
    have v[simp]: "v : carrier V" using vU U by simp
    have "w = zero V ⊕⇘V⇙ w" using M.l_zero by auto
    also have "... = ⊖⇘V⇙ v ⊕⇘V⇙ v ⊕⇘V⇙ w" using M.l_neg by auto
    also have "... = ⊖⇘V⇙ v ⊕⇘V⇙ (v ⊕⇘V⇙ w)"
      using M.l_zero M.a_assoc M.a_closed by auto
    also have "... : span U" using span_neg[OF U vU] span_add1[OF U] R by auto
    finally show ?thesis.
  qed
qed


lemma lincomb_union:
  assumes U: "U ⊆ carrier V"
      and U'[simp]: "U' ⊆ carrier V"
      and disj: "U ∩ U' = {}"
      and finU: "finite U"
      and finU': "finite U'"
      and a: "a : U ∪ U' → carrier K"
    shows "lincomb a (U ∪ U') = lincomb a U ⊕⇘V⇙ lincomb a U'"
  using finU U disj a
proof (induct set:finite)
  case empty thus ?case by (subst(2) lincomb_def, simp) next
  case (insert u U) thus ?case
    unfolding Un_insert_left
    using lincomb_insert2 finU' insert a_assoc by auto
qed

lemma span_union1:
  assumes U: "U ⊆ carrier V" and U': "U' ⊆ carrier V" and UU': "span U = span U'"
      and W: "W ⊆ carrier V" and W': "W' ⊆ carrier V" and WW': "span W = span W'"
  shows "span (U ∪ W) ⊆ span (U' ∪ W')" (is "?L ⊆ ?R")
proof
  fix x assume "x : ?L"
  then obtain a A
    where finA: "finite A"
      and AUW: "A ⊆ U ∪ W"
      and x: "x = lincomb a A"
      and a: "a : A → carrier K"
    unfolding span_def by auto
  let ?AU = "A ∩ U" and ?AW = "A ∩ W - U"
  have AU: "?AU ⊆ carrier V" using U by auto
  have AW: "?AW ⊆ carrier V" using W by auto
  have disj: "?AU ∩ ?AW = {}" by auto
  have U'W': "U' ∪ W' ⊆ carrier V" using U' W' by auto

  have "?AU ∪ ?AW = A" using AUW by auto
  hence "x = lincomb a (?AU ∪ ?AW)" using x by auto
  hence "x = lincomb a ?AU ⊕⇘V⇙ lincomb a ?AW"
    using lincomb_union[OF AU AW disj] finA a by auto
  moreover
    have "lincomb a ?AU : span U" and "lincomb a ?AW : span W"
      unfolding span_def using AU a finA by auto
    hence "lincomb a ?AU : span U'" and "lincomb a ?AW : span W'"
      using UU' WW' by auto
    hence "lincomb a ?AU : ?R" and "lincomb a ?AW : ?R"
      using span_is_monotone[OF Un_upper1, of U']
      using span_is_monotone[OF Un_upper2, of W'] by auto
  ultimately
    show "x : ?R" using span_add1[OF U'W'] by auto
qed

lemma span_Un:
  assumes U: "U ⊆ carrier V" and U': "U' ⊆ carrier V" and UU': "span U = span U'"
      and W: "W ⊆ carrier V" and W': "W' ⊆ carrier V" and WW': "span W = span W'"
  shows "span (U ∪ W) = span (U' ∪ W')" (is "?L = ?R")
  using span_union1[OF assms]
  using span_union1[OF U' U UU'[symmetric] W' W WW'[symmetric]]
  by auto

lemma lincomb_zero:
  assumes U: "U ⊆ carrier V" and a: "a : U → {zero K}"
  shows "lincomb a U = zero V"
  using U a
proof (induct U rule: infinite_finite_induct)
  case empty show ?case unfolding lincomb_def by auto next
  case (insert u U)
    hence "a ∈ insert u U → carrier K" using zero_closed by force
    thus ?case using insert by (subst lincomb_insert2; auto)
qed (auto simp: lincomb_def)

end

context module
begin

lemma lincomb_empty[simp]: "lincomb a {} = 𝟬⇘M⇙"
  unfolding lincomb_def by auto

end

context linear_map
begin

interpretation Ker: vectorspace K "(V.vs kerT)"
  using kerT_is_subspace
  using V.subspace_is_vs by blast

interpretation im: vectorspace K "(W.vs imT)"
  using imT_is_subspace
  using W.subspace_is_vs by blast

lemma inj_imp_Ker0:
assumes "inj_on T (carrier V)"
shows "carrier (V.vs kerT) = {𝟬⇘V⇙}"
  unfolding mod_hom.ker_def
  using assms inj_on_contraD by fastforce

lemma Ke0_imp_inj:
assumes c: "carrier (V.vs kerT) = {𝟬⇘V⇙}"
shows "inj_on T (carrier V)"
proof (auto simp add: inj_on_def)
  fix x y
  assume x: "x ∈ carrier V" and y: "y ∈ carrier V"
  and Tx_Ty: "T x = T y" 
  hence "T x ⊖⇘W⇙ T y = 𝟬⇘W⇙" using W.module.M.minus_other_side by auto
  hence "T (x ⊖⇘V⇙ y) = 𝟬⇘W⇙" by (simp add: x y)
  hence "x ⊖⇘V⇙ y ∈ carrier (V.vs kerT)" by (simp add: mod_hom.ker_def x y) 
  hence "x ⊖⇘V⇙ y = 𝟬⇘V⇙" using c by fast
  thus "x = y" by (simp add: x y)
qed

corollary Ke0_iff_inj: "inj_on T (carrier V) = (carrier (V.vs kerT) = {𝟬⇘V⇙})"
using inj_imp_Ker0 Ke0_imp_inj by auto

lemma inj_imp_dim_ker0:
assumes "inj_on T (carrier V)"
shows "vectorspace.dim K (V.vs kerT) = 0"
proof (unfold Ker.dim_def, rule Least_eq_0, rule exI[of _ "{}"])
    have Ker_rw: "carrier (V.vs kerT) = {𝟬⇘V⇙}" 
      unfolding mod_hom.ker_def
      using assms inj_on_contraD by fastforce
    have "finite {}" by simp 
    moreover have "card {} = 0" by simp
    moreover have "{} ⊆ carrier (V.vs kerT)" by simp
    moreover have "Ker.gen_set {}" unfolding Ker_rw by (simp add: Ker.span_empty)
    ultimately show "finite {} ∧ card {} = 0 ∧ {} ⊆ carrier (V.vs kerT) ∧ Ker.gen_set {}" by simp
qed


lemma surj_imp_imT_carrier:
assumes surj: "T` (carrier V) = carrier W"
shows "(imT) = carrier W"
by (simp add: surj im_def) 

lemma dim_eq:
assumes fin_dim_V: "V.fin_dim"
and i: "inj_on T (carrier V)" and surj: "T` (carrier V) = carrier W"
shows "V.dim = W.dim"
proof -
  have dim0: "vectorspace.dim K (V.vs kerT) = 0" 
    by (rule inj_imp_dim_ker0[OF i])
  have imT_W: "(imT) = carrier W"
    by (rule surj_imp_imT_carrier[OF surj])
  have rnt: "vectorspace.dim K (W.vs imT) + vectorspace.dim K (V.vs kerT) = V.dim"
    by (rule rank_nullity[OF fin_dim_V])
  hence "V.dim = vectorspace.dim K (W.vs imT)" using dim0 by auto
  also have "...  = W.dim" using imT_W by auto
  finally show ?thesis using fin_dim_V by auto
qed       


lemma lincomb_linear_image:
assumes inj_T: "inj_on T (carrier V)"
assumes A_in_V: "A ⊆ carrier V" and a: "a ∈ (T`A) → carrier K"
assumes f: "finite A"
shows "W.module.lincomb a (T`A) = T (V.module.lincomb (a ∘ T) A)"
using f using A_in_V a
proof (induct A)
  case empty thus ?case by auto
next
  case (insert x A)
  have T_insert_rw: "T ` insert x A = insert (T x) (T` A)" by simp
  have "W.module.lincomb a (T ` insert x A) = W.module.lincomb a (insert (T x) (T` A))" 
    unfolding T_insert_rw ..
  also have "... =  a (T x) ⊙⇘W⇙ (T x) ⊕⇘W⇙ W.module.lincomb a (T` A)"
  proof (rule W.lincomb_insert2)
    show "finite (T ` A)" by (simp add: insert.hyps(1))
    show "T ` A ⊆ carrier W" using insert.prems(1) by auto
    show "a ∈ insert (T x) (T ` A) → carrier K" 
      using insert.prems(2) by blast
    show "T x ∉ T ` A" 
      by (meson inj_T inj_on_image_mem_iff insert.hyps(2) insert.prems(1) insert_subset)
    show "T x ∈ carrier W" using insert.prems(1) by blast
  qed
  also have "... = a (T x) ⊙⇘W⇙ (T x) ⊕⇘W⇙ (T (V.module.lincomb (a ∘ T) A))"
    using insert.hyps(3) insert.prems(1) insert.prems(2) by fastforce 
  also have "... = T (a (T x) ⊙⇘V⇙ x) ⊕⇘W⇙ (T (V.module.lincomb (a ∘ T) A))"
    using insert.prems(1) insert.prems(2) by auto
  also have "... = T ((a (T x) ⊙⇘V⇙ x) ⊕⇘V⇙ (V.module.lincomb (a ∘ T) A))"
  proof (rule T_add[symmetric])
    show "a (T x) ⊙⇘V⇙ x ∈ carrier V" using insert.prems(1) insert.prems(2) by auto
    show "V.module.lincomb (a ∘ T) A ∈ carrier V"
    proof (rule V.module.lincomb_closed)
      show "A ⊆ carrier V" using insert.prems(1) by blast
      show "a ∘ T ∈ A → carrier K" using coeff_in_ring insert.prems(2) by auto
    qed
  qed
  also have "... = T (V.module.lincomb (a ∘ T) (insert x A))"
  proof (rule arg_cong[of _ _ T])
    have "a ∘ T ∈ insert x A → carrier K"
      using comp_def insert.prems(2) by auto
    then show "a (T x) ⊙⇘V⇙ x ⊕⇘V⇙ V.module.lincomb (a ∘ T) A 
      = V.module.lincomb (a ∘ T) (insert x A)"
      using V.lincomb_insert2 insert.hyps(1) insert.hyps(2) insert.prems(1) by force
  qed
  finally show ?case .
qed
   


lemma surj_fin_dim:  
  assumes fd: "V.fin_dim" and surj: "T` (carrier V) = carrier W"
  shows image_fin_dim: "W.fin_dim"
    using rank_nullity_main(2)[OF fd surj] .

lemma linear_inj_image_is_basis:
assumes inj_T: "inj_on T (carrier V)" and surj: "T` (carrier V) = carrier W"
and basis_B: "V.basis B"
and fin_dim_V: "V.fin_dim"
shows "W.basis (T`B)"
proof (rule W.dim_li_is_basis)
  have lm: "linear_map K V W T" by intro_locales
  have inj_TB: "inj_on T B"
    by (meson basis_B inj_T subset_inj_on V.basis_def)
  show "W.fin_dim" by (rule surj_fin_dim[OF fin_dim_V surj])  
  show "finite (T ` B)"
  proof (rule finite_imageI, rule V.fin[OF fin_dim_V])
    show "V.module.lin_indpt B" using basis_B unfolding V.basis_def by auto
    show "B ⊆ carrier V" using basis_B unfolding V.basis_def by auto
  qed
  show "T ` B ⊆ carrier W" using basis_B unfolding V.basis_def by auto
  show "W.dim ≤ card (T ` B)"
  proof -
    have d: "V.dim = W.dim" by (rule dim_eq[OF fin_dim_V inj_T surj])
    have "card (T` B) = card B" by (simp add: card_image inj_TB)
    also have "... = V.dim" using basis_B fin_dim_V V.basis_def V.dim_basis V.fin by auto
    finally show ?thesis using d by simp
  qed
  show "W.module.lin_indpt (T ` B)"
  proof (rule W.module.finite_lin_indpt2)
     show fin_TB: "finite (T ` B)" by fact
     show TB_W: "T ` B ⊆ carrier W" by fact
     fix a assume a: "a ∈ T ` B → carrier K" and lc_a: "W.module.lincomb a (T ` B) = 𝟬⇘W⇙"
     show "∀v∈T ` B. a v = 𝟬⇘K⇙" 
     proof (rule ballI)
      fix v assume v: "v ∈ T ` B"
      have "W.module.lincomb a (T ` B) = T (V.module.lincomb (a ∘ T) B)"
      proof (rule lincomb_linear_image[OF inj_T])
        show "B ⊆ carrier V" using V.vectorspace_axioms basis_B vectorspace.basis_def by blast
        show "a ∈ T ` B → carrier K" by (simp add: a)
        show "finite B" using fin_TB finite_image_iff inj_TB by blast
      qed
      hence T_lincomb: "T (V.module.lincomb (a ∘ T) B) = 𝟬⇘W⇙" using lc_a by simp
      have lincomb_0: "V.module.lincomb (a ∘ T) B = 𝟬⇘V⇙"
      proof -
        have "a ∘ T ∈ B → carrier K"
          using a by auto
        then show ?thesis
          by (metis V.module.M.zero_closed V.module.lincomb_closed 
            T_lincomb basis_B f0_is_0 inj_T inj_onD  V.basis_def)
      qed 
      have "(a ∘ T) ∈ B → {𝟬⇘K⇙}" 
      proof (rule V.not_lindepD[OF _ _ _ _ lincomb_0])
        show "V.module.lin_indpt B" using V.basis_def basis_B by blast
        show "finite B" using fin_TB finite_image_iff inj_TB by auto
        show "B ⊆ B" by auto
        show "a ∘ T ∈ B → carrier K" using a by auto
      qed
      thus "a v = 𝟬⇘K⇙" using v by auto
    qed
  qed
qed

end

lemma (in vectorspace) dim1I:
assumes "gen_set {v}"
assumes "v ≠ 𝟬⇘V⇙" "v ∈ carrier V"
shows "dim = 1"
proof -
  have "basis {v}" by (metis assms(1) assms(2) assms(3) basis_def empty_iff empty_subsetI
   finite.emptyI finite_lin_indpt2 insert_iff insert_subset insert_union lin_dep_iff_in_span
   span_empty)
  then show ?thesis using dim_basis by force
qed

lemma (in vectorspace) dim0I:
assumes "gen_set {𝟬⇘V⇙}"
shows "dim = 0"
proof -
  have "basis {}" unfolding basis_def using already_in_span assms finite_lin_indpt2 span_zero by auto
  then show ?thesis using dim_basis by force
qed

lemma (in vectorspace) dim_le1I:
assumes "gen_set {v}"
assumes "v ∈ carrier V"
shows "dim ≤ 1"
by (metis One_nat_def assms(1) assms(2) bot.extremum card.empty card.insert empty_iff finite.intros(1)
finite.intros(2) insert_subset vectorspace.gen_ge_dim vectorspace_axioms)

definition find_indices where "find_indices x xs ≡ [i ← [0..<length xs]. xs!i = x]"

lemma find_indices_Nil [simp]:
  "find_indices x [] = []"
  by (simp add: find_indices_def)

lemma find_indices_Cons:
  "find_indices x (y#ys) = (if x = y then Cons 0 else id) (map Suc (find_indices x ys))"
apply (unfold find_indices_def length_Cons, subst upt_conv_Cons, simp)
apply (fold map_Suc_upt, auto simp: filter_map o_def) done

lemma find_indices_snoc [simp]:
  "find_indices x (ys@[y]) = find_indices x ys @ (if x = y then [length ys] else [])"
  by (unfold find_indices_def, auto intro!: filter_cong simp: nth_append)

lemma mem_set_find_indices [simp]: "i ∈ set (find_indices x xs) ⟷ i < length xs ∧ xs!i = x"
  by (auto simp: find_indices_def)

lemma distinct_find_indices: "distinct (find_indices x xs)"
  unfolding find_indices_def by simp 

context abelian_monoid begin

definition sumlist
  where "sumlist xs ≡ foldr (⊕) xs 𝟬"
  (* fold is not good as it reverses the list, although the most general locale for monoids with
     ⊕ is already Abelian in Isabelle 2016-1. foldl is OK but it will not simplify Cons. *)

lemma [simp]:
  shows sumlist_Cons: "sumlist (x#xs) = x ⊕ sumlist xs"
    and sumlist_Nil: "sumlist [] = 𝟬"
  by (simp_all add: sumlist_def)

lemma sumlist_carrier [simp]:
  assumes "set xs ⊆ carrier G" shows "sumlist xs ∈ carrier G"
  using assms by (induct xs, auto)

lemma sumlist_neutral:
  assumes "set xs ⊆ {𝟬}" shows "sumlist xs = 𝟬"
proof (insert assms, induct xs)
  case (Cons x xs)
  then have "x = 𝟬" and "set xs ⊆ {𝟬}" by auto
  with Cons.hyps show ?case by auto
qed simp

lemma sumlist_append:
  assumes "set xs ⊆ carrier G" and "set ys ⊆ carrier G"
  shows "sumlist (xs @ ys) = sumlist xs ⊕ sumlist ys"
proof (insert assms, induct xs arbitrary: ys)
  case (Cons x xs)
  have "sumlist (xs @ ys) = sumlist xs ⊕ sumlist ys"
    using Cons.prems by (auto intro: Cons.hyps)
  with Cons.prems show ?case by (auto intro!: a_assoc[symmetric])
qed auto

lemma sumlist_snoc:
  assumes "set xs ⊆ carrier G" and "x ∈ carrier G"
  shows "sumlist (xs @ [x]) = sumlist xs ⊕ x"
  by (subst sumlist_append, insert assms, auto)

lemma sumlist_as_finsum:
  assumes "set xs ⊆ carrier G" and "distinct xs" shows "sumlist xs = (⨁x∈set xs. x)"
  using assms by (induct xs, auto intro:finsum_insert[symmetric])

lemma sumlist_map_as_finsum:
  assumes "f : set xs → carrier G" and "distinct xs"
  shows "sumlist (map f xs) = (⨁x ∈ set xs. f x)"
  using assms by (induct xs, auto)

definition summset where "summset M ≡ fold_mset (⊕) 𝟬 M"

lemma summset_empty [simp]: "summset {#} = 𝟬" by (simp add: summset_def)

lemma fold_mset_add_carrier: "a ∈ carrier G ⟹ set_mset M ⊆ carrier G ⟹ fold_mset (⊕) a M ∈ carrier G" 
proof (induct M arbitrary: a)
  case (add x M)
  thus ?case by 
    (subst comp_fun_commute_on.fold_mset_add_mset[of _ "carrier G"], unfold_locales, auto simp: a_lcomm)
qed simp

lemma summset_carrier[intro]: "set_mset M ⊆ carrier G ⟹ summset M ∈ carrier G" 
  unfolding summset_def by (rule fold_mset_add_carrier, auto)  

lemma summset_add_mset[simp]:
  assumes a: "a ∈ carrier G" and MG: "set_mset M ⊆ carrier G"
  shows "summset (add_mset a M) = a ⊕ summset M"
  using assms 
  by (auto simp add: summset_def)
   (rule comp_fun_commute_on.fold_mset_add_mset, unfold_locales, auto simp add: a_lcomm)    
 
lemma sumlist_as_summset:
  assumes "set xs ⊆ carrier G" shows "sumlist xs = summset (mset xs)"
  by (insert assms, induct xs, auto)

lemma sumlist_rev:
  assumes "set xs ⊆ carrier G"
  shows "sumlist (rev xs) = sumlist xs"
  using assms by (simp add: sumlist_as_summset)

lemma sumlist_as_fold:
  assumes "set xs ⊆ carrier G"
  shows "sumlist xs = fold (⊕) xs 𝟬"
  by (fold sumlist_rev[OF assms], simp add: sumlist_def foldr_conv_fold)

end

context Module.module begin

definition lincomb_list
where "lincomb_list c vs = sumlist (map (λi. c i ⊙⇘M⇙ vs ! i) [0..<length vs])"

lemma lincomb_list_carrier:
  assumes "set vs ⊆ carrier M" and "c : {0..<length vs} → carrier R"
  shows "lincomb_list c vs ∈ carrier M"
  by (insert assms, unfold lincomb_list_def, intro sumlist_carrier, auto intro!: smult_closed)

lemma lincomb_list_Nil [simp]: "lincomb_list c [] = 𝟬⇘M⇙"
  by (simp add: lincomb_list_def)

lemma lincomb_list_Cons [simp]:
  "lincomb_list c (v#vs) = c 0 ⊙⇘M⇙ v ⊕⇘M⇙ lincomb_list (c o Suc) vs"
  by (unfold lincomb_list_def length_Cons, subst upt_conv_Cons, simp, fold map_Suc_upt, simp add: o_def)

lemma lincomb_list_eq_0:
  assumes "⋀i. i < length vs ⟹ c i ⊙⇘M⇙ vs ! i = 𝟬⇘M⇙"
  shows "lincomb_list c vs = 𝟬⇘M⇙"
proof (insert assms, induct vs arbitrary:c)
  case (Cons v vs)
  from Cons.prems[of 0] have [simp]: "c 0 ⊙⇘M⇙ v = 𝟬⇘M⇙" by auto
  from Cons.prems[of "Suc _"] Cons.hyps have "lincomb_list (c ∘ Suc) vs = 𝟬⇘M⇙" by auto
  then show ?case by (simp add: o_def)
qed simp

definition mk_coeff where "mk_coeff vs c v ≡ R.sumlist (map c (find_indices v vs))"

lemma mk_coeff_carrier:
  assumes "c : {0..<length vs} → carrier R" shows "mk_coeff vs c w ∈ carrier R"
  by (insert assms, auto simp: mk_coeff_def find_indices_def intro!:R.sumlist_carrier elim!:funcset_mem)

lemma mk_coeff_Cons:
  assumes "c : {0..<length (v#vs)} → carrier R"
  shows "mk_coeff (v#vs) c = (λw. (if w = v then c 0 else 𝟬) ⊕ mk_coeff vs (c o Suc) w)"
proof-
  from assms have "c o Suc : {0..<length vs} → carrier R" by auto
  from mk_coeff_carrier[OF this] assms
  show ?thesis by (auto simp add: mk_coeff_def find_indices_Cons)
qed

lemma mk_coeff_0[simp]:
  assumes "v ∉ set vs"
  shows "mk_coeff vs c v = 𝟬"
proof -
  have "(find_indices v vs) = []" using assms unfolding find_indices_def
    by (simp add: in_set_conv_nth)
  thus ?thesis  unfolding mk_coeff_def by auto
qed  

lemma lincomb_list_as_lincomb:
  assumes vs_M: "set vs ⊆ carrier M" and c: "c : {0..<length vs} → carrier R"
  shows "lincomb_list c vs = lincomb (mk_coeff vs c) (set vs)"
proof (insert assms, induct vs arbitrary: c)
  case (Cons v vs)
  have mk_coeff_Suc_closed: "mk_coeff vs (c ∘ Suc) a ∈ carrier R" for a
    apply (rule mk_coeff_carrier)
    using Cons.prems unfolding Pi_def by auto
  have x_in: "x ∈ carrier M" if x: "x∈ set vs" for x using Cons.prems x by auto
  show ?case apply (unfold mk_coeff_Cons[OF Cons.prems(2)] lincomb_list_Cons)
    apply (subst Cons) using Cons apply (force, force)
  proof (cases "v ∈ set vs", auto simp:insert_absorb)
    case False
    let ?f = "(λva. ((if va = v then c 0 else 𝟬) ⊕ mk_coeff vs (c ∘ Suc) va) ⊙⇘M⇙ va)"
    have mk_0: "mk_coeff vs (c ∘ Suc) v = 𝟬" using False by auto
    have [simp]: "(c 0 ⊕ 𝟬) = c 0"
      using Cons.prems(2) by force
    have finsum_rw: "(⨁⇘M⇙va∈insert v (set vs). ?f va) = (?f v) ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs). ?f va)"
    proof (rule finsum_insert, auto simp add: False, rule smult_closed, rule R.a_closed)
      fix x
      show "mk_coeff vs (c ∘ Suc) x ∈ carrier R" 
        using mk_coeff_Suc_closed by auto
      show "c 0 ⊙⇘M⇙ v ∈ carrier M"
      proof (rule smult_closed)
        show "c 0 ∈ carrier R"
          using Cons.prems(2) by fastforce
        show "v ∈ carrier M"
          using Cons.prems(1) by auto
      qed
      show "𝟬 ∈ carrier R"
        by simp
      assume x: "x ∈ set vs" show "x ∈ carrier M"
        using Cons.prems(1) x by auto
    qed
    have finsum_rw2: 
      "(⨁⇘M⇙va∈(set vs). ?f va) = (⨁⇘M⇙va∈set vs. (mk_coeff vs (c ∘ Suc) va) ⊙⇘M⇙ va)"
    proof (rule finsum_cong2, auto simp add: False)
      fix i assume i: "i ∈ set vs"
      have "c ∘ Suc ∈ {0..<length vs} → carrier R" using Cons.prems by auto
      then have [simp]: "mk_coeff vs (c ∘ Suc) i ∈ carrier R" 
        using mk_coeff_Suc_closed by auto
      have "𝟬 ⊕ mk_coeff vs (c ∘ Suc) i = mk_coeff vs (c ∘ Suc) i" by (rule R.l_zero, simp)
      then show "(𝟬 ⊕ mk_coeff vs (c ∘ Suc) i) ⊙⇘M⇙ i = mk_coeff vs (c ∘ Suc) i ⊙⇘M⇙ i" 
        by auto
      show "(𝟬 ⊕ mk_coeff vs (c ∘ Suc) i) ⊙⇘M⇙ i ∈ carrier M"
        using Cons.prems(1) i by auto
    qed
    show "c 0 ⊙⇘M⇙ v ⊕⇘M⇙ lincomb (mk_coeff vs (c ∘ Suc)) (set vs) =
    lincomb (λa. (if a = v then c 0 else 𝟬) ⊕ mk_coeff vs (c ∘ Suc) a) (insert v (set vs))" 
      unfolding lincomb_def
      unfolding finsum_rw mk_0 
      unfolding finsum_rw2 by auto
  next
    case True
    let ?f = "λva. ((if va = v then c 0 else 𝟬) ⊕ mk_coeff vs (c ∘ Suc) va) ⊙⇘M⇙ va"
    have rw: "(c 0 ⊕ mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v 
      = (c 0 ⊙⇘M⇙ v) ⊕⇘M⇙ (mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v"      
      using Cons.prems(1) Cons.prems(2) atLeast0_lessThan_Suc_eq_insert_0 
      using mk_coeff_Suc_closed smult_l_distr by auto
    have rw2: "((mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v) 
      ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs - {v}). ?f va) = (⨁⇘M⇙v∈set vs. mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v)"
    proof -
      have "(⨁⇘M⇙va∈(set vs - {v}). ?f va) = (⨁⇘M⇙v∈set vs - {v}. mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v)"
        by (rule finsum_cong2, unfold Pi_def, auto simp add: mk_coeff_Suc_closed x_in)
      moreover have "(⨁⇘M⇙v∈set vs. mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v) = ((mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v) 
        ⊕⇘M⇙ (⨁⇘M⇙v∈set vs - {v}. mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v)"
        by (rule M.add.finprod_split, auto simp add: mk_coeff_Suc_closed True x_in)
      ultimately show ?thesis by auto
    qed
    have "lincomb (λa. (if a = v then c 0 else 𝟬) ⊕ mk_coeff vs (c ∘ Suc) a) (set vs) 
      = (⨁⇘M⇙va∈set vs. ?f va)" unfolding lincomb_def ..
    also have "... = ?f v ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs - {v}). ?f va)"
    proof (rule M.add.finprod_split)
      have c0_mkcoeff_in: "c 0 ⊕ mk_coeff vs (c ∘ Suc) v ∈ carrier R" 
      proof (rule R.a_closed)
        show "c 0 ∈ carrier R " using Cons.prems by auto
        show "mk_coeff vs (c ∘ Suc) v ∈ carrier R"
          using mk_coeff_Suc_closed by auto
    qed
    moreover have "(𝟬 ⊕ mk_coeff vs (c ∘ Suc) va) ⊙⇘M⇙ va ∈ carrier M"
      if va: "va ∈ carrier M" for va 
      by (rule smult_closed[OF _ va], rule R.a_closed, auto simp add: mk_coeff_Suc_closed)
    ultimately show "?f ` set vs ⊆ carrier M" using Cons.prems(1) by auto        
      show "finite (set vs)" by simp
      show "v ∈ set vs" using True by simp
    qed
    also have "... = (c 0 ⊕ mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v 
      ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs - {v}). ?f va)" by auto
    also have "... = ((c 0 ⊙⇘M⇙ v) ⊕⇘M⇙ (mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v) 
      ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs - {v}). ?f va)" unfolding rw by simp
    also have "... = (c 0 ⊙⇘M⇙ v) ⊕⇘M⇙ (((mk_coeff vs (c ∘ Suc) v) ⊙⇘M⇙ v) 
      ⊕⇘M⇙ (⨁⇘M⇙va∈(set vs - {v}). ?f va))"
    proof (rule M.a_assoc)
      show "c 0 ⊙⇘M⇙ v ∈ carrier M" 
        using Cons.prems(1) Cons.prems(2) by auto
      show "mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v ∈ carrier M"
        using Cons.prems(1) mk_coeff_Suc_closed by auto
      show "(⨁⇘M⇙va∈set vs - {v}. ((if va = v then c 0 else 𝟬) 
        ⊕ mk_coeff vs (c ∘ Suc) va) ⊙⇘M⇙ va) ∈ carrier M"
        by (rule M.add.finprod_closed) (auto simp add: mk_coeff_Suc_closed x_in)
    qed
    also have "... = c 0 ⊙⇘M⇙ v ⊕⇘M⇙ (⨁⇘M⇙v∈set vs. mk_coeff vs (c ∘ Suc) v ⊙⇘M⇙ v)"
      unfolding rw2 ..
    also have "... = c 0 ⊙⇘M⇙ v ⊕⇘M⇙ lincomb (mk_coeff vs (c ∘ Suc)) (set vs)" 
      unfolding lincomb_def ..
    finally show "c 0 ⊙⇘M⇙ v ⊕⇘M⇙ lincomb (mk_coeff vs (c ∘ Suc)) (set vs) 
      = lincomb (λa. (if a = v then c 0 else 𝟬) ⊕ mk_coeff vs (c ∘ Suc) a) (set vs)" ..         
  qed
qed simp

definition "span_list vs ≡ {lincomb_list c vs | c. c : {0..<length vs} → carrier R}"

lemma in_span_listI:
  assumes "c : {0..<length vs} → carrier R" and "v = lincomb_list c vs"
  shows "v ∈ span_list vs"
  using assms by (auto simp: span_list_def)

lemma in_span_listE:
  assumes "v ∈ span_list vs"
      and "⋀c. c : {0..<length vs} → carrier R ⟹ v = lincomb_list c vs ⟹ thesis"
  shows thesis
  using assms by (auto simp: span_list_def)

lemmas lincomb_insert2 = lincomb_insert[unfolded insert_union[symmetric]]

lemma lincomb_zero:
  assumes U: "U ⊆ carrier M" and a: "a : U → {zero R}"
  shows "lincomb a U = zero M"
  using U a
proof (induct U rule: infinite_finite_induct)
  case empty show ?case unfolding lincomb_def by auto next
  case (insert u U)
    hence "a ∈ insert u U → carrier R" using zero_closed by force
    thus ?case using insert by (subst lincomb_insert2; auto)
qed (auto simp: lincomb_def)

end

hide_const (open) Multiset.mult
end