(* 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