diff --git a/thys/Jordan_Normal_Form/Missing_VectorSpace.thy b/thys/Jordan_Normal_Form/Missing_VectorSpace.thy --- a/thys/Jordan_Normal_Form/Missing_VectorSpace.thy +++ b/thys/Jordan_Normal_Form/Missing_VectorSpace.thy @@ -1,1400 +1,1400 @@ (* 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 \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> v" have fA: "?f : A \ carrier V" unfolding a'_def using aA AU U by auto let ?f' = "\v. a' v \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> 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 \\<^bsub>K\<^esub> 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 \\<^bsub>V\<^esub> u \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> u = \\<^bsub>V\<^esub> u" using smult_minus_1[OF u] by simp also have "lincomb a (U-{u}) = u" using ulin.. also have "\\<^bsub>V\<^esub> u \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> lincomb a U = lincomb (\u. c \\<^bsub>K\<^esub> 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 \\<^bsub>K\<^esub> ua e)" define a' where "a' = (\e. a e \\<^bsub>K\<^esub> xa e)" define a'' where "a'' = (\e. if e = v then xa u \\<^bsub>K\<^esub> 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 \\<^bsub>V\<^esub> u \\<^bsub>V\<^esub> lincomb xa E" using xxa lincomb_insert2 finE E xa uE u by auto also have "xa u \\<^bsub>V\<^esub> u = xa u \\<^bsub>V\<^esub> lincomb ua (insert v E)" using uua by auto also have "lincomb ua (insert v E) = ua v \\<^bsub>V\<^esub> v \\<^bsub>V\<^esub> lincomb ua E" using lincomb_insert2 finE E ua vE v by auto also have "xa u \\<^bsub>V\<^esub> ... = xa u \\<^bsub>V\<^esub> (ua v \\<^bsub>V\<^esub> v) \\<^bsub>V\<^esub> xa u \\<^bsub>V\<^esub> lincomb ua E" using smult_r_distr by auto also have "xa u \\<^bsub>V\<^esub> lincomb ua E = lincomb a E" unfolding a_def using lincomb_distrib[OF E] by auto finally have "x = xa u \\<^bsub>V\<^esub> (ua v \\<^bsub>V\<^esub> v) \\<^bsub>V\<^esub> (lincomb a E \\<^bsub>V\<^esub> lincomb xa E)" using a_assoc xau v aE xaE by auto also have "lincomb a E \\<^bsub>V\<^esub> 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 \\<^bsub>K\<^esub> ua v) \\<^bsub>V\<^esub> v) \\<^bsub>V\<^esub> lincomb a'' E" using smult_assoc1 by auto also have "xa u \\<^bsub>K\<^esub> ua v = a'' v" unfolding a''_def by simp also have "(a'' v \\<^bsub>V\<^esub> v) \\<^bsub>V\<^esub> 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 \\<^bsub>K\<^esub> va e)" define va'' where "va'' = (\e. va' e \\<^bsub>K\<^esub> 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 \\<^bsub>V\<^esub> v \\<^bsub>V\<^esub> lincomb ua E" using lincomb_insert2 vE by auto also have "ua v \\<^bsub>V\<^esub> v = ua v \\<^bsub>V\<^esub> (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 "... \\<^bsub>V\<^esub> z = zero V" using insert by auto also have "... \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> z \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> 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 \\<^bsub>K\<^esub> (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 \\<^bsub>V\<^esub> 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 "\\<^bsub>V\<^esub> 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. \\<^bsub>K\<^esub> one K \\<^bsub>K\<^esub> a u" have "\\<^bsub>V\<^esub> v = \\<^bsub>K\<^esub> one K \\<^bsub>V\<^esub> v" using smult_minus_1_back[OF v]. also have "... = \\<^bsub>K\<^esub> one K \\<^bsub>V\<^esub> lincomb a A" using va by simp finally have main: "\\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> w" using M.l_zero by auto also have "... = \\<^bsub>V\<^esub> v \\<^bsub>V\<^esub> v \\<^bsub>V\<^esub> w" using M.l_neg by auto also have "... = \\<^bsub>V\<^esub> v \\<^bsub>V\<^esub> (v \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> 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 \\<^bsub>V\<^esub> 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 {} = \\<^bsub>M\<^esub>" 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) = {\\<^bsub>V\<^esub>}" unfolding mod_hom.ker_def using assms inj_on_contraD by fastforce lemma Ke0_imp_inj: assumes c: "carrier (V.vs kerT) = {\\<^bsub>V\<^esub>}" 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 \\<^bsub>W\<^esub> T y = \\<^bsub>W\<^esub>" using W.module.M.minus_other_side by auto hence "T (x \\<^bsub>V\<^esub> y) = \\<^bsub>W\<^esub>" by (simp add: x y) hence "x \\<^bsub>V\<^esub> y \ carrier (V.vs kerT)" by (simp add: mod_hom.ker_def x y) hence "x \\<^bsub>V\<^esub> y = \\<^bsub>V\<^esub>" 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) = {\\<^bsub>V\<^esub>})" 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) = {\\<^bsub>V\<^esub>}" 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) \\<^bsub>W\<^esub> (T x) \\<^bsub>W\<^esub> 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_alt insert.hyps(2) insert.prems(1) insert_subset) + 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) \\<^bsub>W\<^esub> (T x) \\<^bsub>W\<^esub> (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) \\<^bsub>V\<^esub> x) \\<^bsub>W\<^esub> (T (V.module.lincomb (a \ T) A))" using insert.prems(1) insert.prems(2) by auto also have "... = T ((a (T x) \\<^bsub>V\<^esub> x) \\<^bsub>V\<^esub> (V.module.lincomb (a \ T) A))" proof (rule T_add[symmetric]) show "a (T x) \\<^bsub>V\<^esub> 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) \\<^bsub>V\<^esub> x \\<^bsub>V\<^esub> 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) = \\<^bsub>W\<^esub>" show "\v\T ` B. a v = \\<^bsub>K\<^esub>" 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) = \\<^bsub>W\<^esub>" using lc_a by simp have lincomb_0: "V.module.lincomb (a \ T) B = \\<^bsub>V\<^esub>" 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 \ {\\<^bsub>K\<^esub>}" 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 = \\<^bsub>K\<^esub>" using v by auto qed qed qed end lemma (in vectorspace) dim1I: assumes "gen_set {v}" assumes "v \ \\<^bsub>V\<^esub>" "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 {\\<^bsub>V\<^esub>}" 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.. 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 \\<^bsub>M\<^esub> vs ! i) [0.. carrier M" and "c : {0.. 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 [] = \\<^bsub>M\<^esub>" by (simp add: lincomb_list_def) lemma lincomb_list_Cons [simp]: "lincomb_list c (v#vs) = c 0 \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> 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 \\<^bsub>M\<^esub> vs ! i = \\<^bsub>M\<^esub>" shows "lincomb_list c vs = \\<^bsub>M\<^esub>" proof (insert assms, induct vs arbitrary:c) case (Cons v vs) from Cons.prems[of 0] have [simp]: "c 0 \\<^bsub>M\<^esub> v = \\<^bsub>M\<^esub>" by auto from Cons.prems[of "Suc _"] Cons.hyps have "lincomb_list (c \ Suc) vs = \\<^bsub>M\<^esub>" 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.. 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.. 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.. 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.. 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) \\<^bsub>M\<^esub> 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: "(\\<^bsub>M\<^esub>va\insert v (set vs). ?f va) = (?f v) \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>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 \\<^bsub>M\<^esub> 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: "(\\<^bsub>M\<^esub>va\(set vs). ?f va) = (\\<^bsub>M\<^esub>va\set vs. (mk_coeff vs (c \ Suc) va) \\<^bsub>M\<^esub> va)" proof (rule finsum_cong2, auto simp add: False) fix i assume i: "i \ set vs" have "c \ Suc \ {0.. 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) \\<^bsub>M\<^esub> i = mk_coeff vs (c \ Suc) i \\<^bsub>M\<^esub> i" by auto show "(\ \ mk_coeff vs (c \ Suc) i) \\<^bsub>M\<^esub> i \ carrier M" using Cons.prems(1) i by auto qed show "c 0 \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> 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) \\<^bsub>M\<^esub> va" have rw: "(c 0 \ mk_coeff vs (c \ Suc) v) \\<^bsub>M\<^esub> v = (c 0 \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (mk_coeff vs (c \ Suc) v) \\<^bsub>M\<^esub> 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) \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>va\(set vs - {v}). ?f va) = (\\<^bsub>M\<^esub>v\set vs. mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> v)" proof - have "(\\<^bsub>M\<^esub>va\(set vs - {v}). ?f va) = (\\<^bsub>M\<^esub>v\set vs - {v}. mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> v)" by (rule finsum_cong2, unfold Pi_def, auto simp add: mk_coeff_Suc_closed x_in) moreover have "(\\<^bsub>M\<^esub>v\set vs. mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> v) = ((mk_coeff vs (c \ Suc) v) \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>v\set vs - {v}. mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> 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) = (\\<^bsub>M\<^esub>va\set vs. ?f va)" unfolding lincomb_def .. also have "... = ?f v \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>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) \\<^bsub>M\<^esub> 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) \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>va\(set vs - {v}). ?f va)" by auto also have "... = ((c 0 \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (mk_coeff vs (c \ Suc) v) \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>va\(set vs - {v}). ?f va)" unfolding rw by simp also have "... = (c 0 \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (((mk_coeff vs (c \ Suc) v) \\<^bsub>M\<^esub> v) \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>va\(set vs - {v}). ?f va))" proof (rule M.a_assoc) show "c 0 \\<^bsub>M\<^esub> v \ carrier M" using Cons.prems(1) Cons.prems(2) by auto show "mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> v \ carrier M" using Cons.prems(1) mk_coeff_Suc_closed by auto show "(\\<^bsub>M\<^esub>va\set vs - {v}. ((if va = v then c 0 else \) \ mk_coeff vs (c \ Suc) va) \\<^bsub>M\<^esub> va) \ carrier M" by (rule M.add.finprod_closed) (auto simp add: mk_coeff_Suc_closed x_in) qed also have "... = c 0 \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> (\\<^bsub>M\<^esub>v\set vs. mk_coeff vs (c \ Suc) v \\<^bsub>M\<^esub> v)" unfolding rw2 .. also have "... = c 0 \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> lincomb (mk_coeff vs (c \ Suc)) (set vs)" unfolding lincomb_def .. finally show "c 0 \\<^bsub>M\<^esub> v \\<^bsub>M\<^esub> 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.. carrier R}" lemma in_span_listI: assumes "c : {0.. 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.. 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 diff --git a/thys/Linear_Inequalities/Fundamental_Theorem_Linear_Inequalities.thy b/thys/Linear_Inequalities/Fundamental_Theorem_Linear_Inequalities.thy --- a/thys/Linear_Inequalities/Fundamental_Theorem_Linear_Inequalities.thy +++ b/thys/Linear_Inequalities/Fundamental_Theorem_Linear_Inequalities.thy @@ -1,777 +1,777 @@ section \The Fundamental Theorem of Linear Inequalities\ text \The theorem states that for a given set of vectors A and vector b, either b is in the cone of a linear independent subset of A, or there is a hyperplane that contains span(A,b)-1 linearly independent vectors of A that separates A from b. We prove this theorem and derive some consequences, e.g., Caratheodory's theorem that b is the cone of A iff b is in the cone of a linear independent subset of A.\ theory Fundamental_Theorem_Linear_Inequalities imports Cone Normal_Vector Dim_Span begin context gram_schmidt begin text \The mentions equivances A-D are: \<^item> A: b is in the cone of vectors A, \<^item> B: b is in the cone of a subset of linear independent of vectors A, \<^item> C: there is no separating hyperplane of b and the vectors A, which contains dim many linear independent vectors of A \<^item> D: there is no separating hyperplane of b and the vectors A\ lemma fundamental_theorem_of_linear_inequalities_A_imp_D: assumes A: "A \ carrier_vec n" and fin: "finite A" and b: "b \ cone A" shows "\ c. c \ carrier_vec n \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" proof assume "\ c. c \ carrier_vec n \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" then obtain c where c: "c \ carrier_vec n" and ai: "\ ai. ai \ A \ c \ ai \ 0" and cb: "c \ b < 0" by auto from b[unfolded cone_def nonneg_lincomb_def finite_cone_def] obtain l AA where bc: "b = lincomb l AA" and l: "l ` AA \ {x. x \ 0}" and AA: "AA \ A" by auto from cone_carrier[OF A] b have b: "b \ carrier_vec n" by auto have "0 \ (\ai\AA. l ai * (c \ ai))" by (intro sum_nonneg mult_nonneg_nonneg, insert l ai AA, auto) also have "\ = (\ai\AA. l ai * (ai \ c))" by (rule sum.cong, insert c A AA comm_scalar_prod, force+) also have "\ = (\ai\AA. ((l ai \\<^sub>v ai) \ c))" by (rule sum.cong, insert smult_scalar_prod_distrib c A AA, auto) also have "\ = b \ c" unfolding bc lincomb_def by (subst finsum_scalar_prod_sum[symmetric], insert c A AA, auto) also have "\ = c \ b" using comm_scalar_prod b c by auto also have "\ < 0" by fact finally show False by simp qed text \The difficult direction is that C implies B. To this end we follow the proof that at least one of B and the negation of C is satisfied.\ context fixes a :: "nat \ 'a vec" and b :: "'a vec" and m :: nat assumes a: "a ` {0 ..< m} \ carrier_vec n" and inj_a: "inj_on a {0 ..< m}" and b: "b \ carrier_vec n" and full_span: "span (a ` {0 ..< m}) = carrier_vec n" begin private definition "goal = ((\ I. I \ {0 ..< m} \ card (a ` I) = n \ lin_indpt (a ` I) \ b \ finite_cone (a ` I)) \ (\ c I. I \ {0 ..< m} \ c \ {normal_vector (a ` I), - normal_vector (a ` I)} \ Suc (card (a ` I)) = n \ lin_indpt (a ` I) \ (\ i < m. c \ a i \ 0) \ c \ b < 0))" private lemma card_a_I[simp]: "I \ {0 ..< m} \ card (a ` I) = card I" by (smt inj_a card_image inj_on_image_eq_iff subset_image_inj subset_refl subset_trans) private lemma in_a_I[simp]: "I \ {0 ..< m} \ i < m \ (a i \ a ` I) = (i \ I)" using inj_a - by (meson atLeastLessThan_iff image_eqI inj_on_image_mem_iff_alt zero_le) + by (meson atLeastLessThan_iff image_eqI inj_on_image_mem_iff zero_le) private definition "valid_I = { I. card I = n \ lin_indpt (a ` I) \ I \ {0 ..< m}}" private definition cond where "cond I I' l c h k \ b = lincomb l (a ` I) \ h \ I \ l (a h) < 0 \ (\ h'. h' \ I \ h' < h \ l (a h') \ 0) \ c \ carrier_vec n \ span (a ` (I - {h})) = { x. x \ carrier_vec n \ c \ x = 0} \ c \ b < 0 \ k < m \ c \ a k < 0 \ (\ k'. k' < k \ c \ a k' \ 0) \ I' = insert k (I - {h})" private definition "step_rel = Restr { (I'', I). \ l c h k. cond I I'' l c h k } valid_I" private lemma finite_step_rel: "finite step_rel" proof (rule finite_subset) show "step_rel \ (Pow {0 ..< m} \ Pow {0 ..< m})" unfolding step_rel_def valid_I_def by auto qed auto private lemma acyclic_imp_goal: "acyclic step_rel \ goal" proof (rule ccontr) assume ngoal: "\ goal" (* then the algorithm will not terminate *) { fix I assume I: "I \ valid_I" hence Im: "I \ {0.. carrier_vec n" using a Im by auto have cardD: "card ?D = n" using cardI Im by simp have spanD: "span ?D = carrier_vec n" by (intro span_carrier_lin_indpt_card_n lin cardD carrD) obtain lamb where b_is_lincomb: "b = lincomb lamb (a ` I)" using finite_in_span[OF fin carrD, of b] using spanD b carrD fin_dim lin by auto define h where "h = (LEAST h. h \ I \ lamb (a h) < 0)" have "\ I'. (I', I) \ step_rel" proof (cases "\i\ I . lamb (a i) \ 0") case cond1_T: True have goal unfolding goal_def by (intro disjI1 exI[of _ I] conjI lin cardI lincomb_in_finite_cone[OF b_is_lincomb finD _ carrD], insert cardI Im cond1_T, auto) with ngoal show ?thesis by auto next case cond1_F: False hence "\ h. h \ I \ lamb (a h) < 0" by fastforce from LeastI_ex[OF this, folded h_def] have h: "h \ I" "lamb (a h) < 0" by auto from not_less_Least[of _ "\ h. h \ I \ lamb (a h) < 0", folded h_def] have h_least: "\ k. k \ I \ k < h \ lamb (a k) \ 0" by fastforce obtain I' where I'_def: "I' = I - {h}" by auto obtain c where c_def: "c = pos_norm_vec (a ` I') (a h)" by auto let ?D' = "a ` I'" have I'm: "I' \ {0.. carrier_vec n" using a Im I'_def by auto have finD': "finite (?D')" using Im I'_def subset_eq_atLeast0_lessThan_finite by auto have D'subs: "?D' \ ?D" using I'_def by auto have linD': "lin_indpt (?D')" using lin I'_def Im D'subs subset_li_is_li by auto have D'strictsubs: "?D = ?D' \ {a h}" using h I'_def by auto have h_nin_I: "h \ I'" using h I'_def by auto have ah_nin_D': "a h \ ?D'" using h inj_a Im h_nin_I by (subst in_a_I, auto simp: I'_def) have cardD': "Suc (card (?D')) = n " using cardD ah_nin_D' D'strictsubs finD' by simp have ah_carr: "a h \ carrier_vec n" using h a Im by auto note pnv = pos_norm_vec[OF carrD' finD' linD' cardD' c_def] have ah_nin_span: "a h \ span ?D'" using D'strictsubs lin_dep_iff_in_span[OF carrD' linD' ah_carr ah_nin_D'] lin by auto have cah_ge_zero:"c \ a h > 0" and "c \ carrier_vec n" and cnorm: "span ?D' = {x \ carrier_vec n. x \ c = 0}" using ah_carr ah_nin_span pnv by auto have ccarr: "c \ carrier_vec n" by fact have "b \ c = lincomb lamb (a ` I) \ c" using b_is_lincomb by auto also have "\ = (\w\ ?D. lamb w * (w \ c))" using lincomb_scalar_prod_left[OF carrD, of c lamb] pos_norm_vec ccarr by blast also have "\ = lamb (a h) * (a h \ c) + (\w\ ?D'. lamb w * (w \ c))" using sum.insert[OF finD' ah_nin_D', of lamb] D'strictsubs ah_nin_D' finD' by auto also have "(\w\ ?D'. lamb w * (w \ c)) = 0" apply (rule sum.neutral) using span_mem[OF carrD', unfolded cnorm] by simp also have "lamb (a h) * (a h \ c) + 0 < 0" using cah_ge_zero h(2) comm_scalar_prod[OF ah_carr ccarr] by (auto intro: mult_neg_pos) finally have cb_le_zero: "c \ b < 0" using comm_scalar_prod[OF b ccarr] by auto show ?thesis proof (cases "\i < m . c \ a i \ 0") case cond2_T: True have goal unfolding goal_def by (intro disjI2 exI[of _ c] exI[of _ I'] conjI cb_le_zero linD' cond2_T cardD' I'm pnv(4)) with ngoal show ?thesis by auto next case cond2_F: False define k where "k = (LEAST k. k < m \ c \ a k < 0)" let ?I'' = "insert k I'" show ?thesis unfolding step_rel_def proof (intro exI[of _ ?I''], standard, unfold mem_Collect_eq split, intro exI) from LeastI_ex[OF ] have "\k. k < m \ c \ a k < 0" using cond2_F by fastforce from LeastI_ex[OF this, folded k_def] have k: "k < m" "c \ a k < 0" by auto show "cond I ?I'' lamb c h k" unfolding cond_def I'_def[symmetric] cnorm proof(intro conjI cb_le_zero b_is_lincomb h ccarr h_least refl k) show "{x \ carrier_vec n. x \ c = 0} = {x \ carrier_vec n. c \ x = 0}" using comm_scalar_prod[OF ccarr] by auto from not_less_Least[of _ "\ k. k < m \ c \ a k < 0", folded k_def] have "\k' < k . k' > m \ c \ a k' \ 0" using k(1) less_trans not_less by blast then show "\k' < k . c \ a k' \ 0" using k(1) by auto qed have "?I'' \ valid_I" unfolding valid_I_def proof(standard, intro conjI) from k a have ak_carr: "a k \ carrier_vec n" by auto have ak_nin_span: "a k \ span ?D'" using k(2) cnorm comm_scalar_prod[OF ak_carr ccarr] by auto hence ak_nin_D': "a k \ ?D'" using span_mem[OF carrD'] by auto from lin_dep_iff_in_span[OF carrD' linD' ak_carr ak_nin_D'] show "lin_indpt (a ` ?I'')" using ak_nin_span by auto show "?I'' \ {0..insert k I' \ {0.. card_a_I card_insert_disjoint image_insert) qed then show "(?I'', I) \ valid_I \ valid_I" using I by auto qed qed qed } note step = this { (* create some valid initial set I *) from exists_lin_indpt_subset[OF a, unfolded full_span] obtain A where lin: "lin_indpt A" and span: "span A = carrier_vec n" and Am: "A \ a ` {0 .. carrier_vec n" by auto from lin span A have card: "card A = n" using basis_def dim_basis dim_is_n fin_dim_li_fin by auto from A Am obtain I where A: "A = a ` I" and I: "I \ {0 ..< m}" by (metis subset_imageE) have "I \ valid_I" using I card lin unfolding valid_I_def A by auto hence "\ I. I \ valid_I" .. } note init = this have step_valid: "(I',I) \ step_rel \ I' \ valid_I" for I I' unfolding step_rel_def by auto have "\ (wf step_rel)" proof from init obtain I where I: "I \ valid_I" by auto assume "wf step_rel" from this[unfolded wf_eq_minimal, rule_format, OF I] step step_valid show False by blast qed with wf_iff_acyclic_if_finite[OF finite_step_rel] have "\ acyclic step_rel" by auto thus "acyclic step_rel \ False" by auto qed private lemma acyclic_step_rel: "acyclic step_rel" proof (rule ccontr) assume "\ ?thesis" hence "\ acyclic (step_rel\)" by auto (* obtain cycle *) then obtain I where "(I, I) \ (step_rel^-1)^+" unfolding acyclic_def by blast from this[unfolded trancl_power] obtain len where "(I, I) \ (step_rel^-1) ^^ len" and len0: "len > 0" by blast (* obtain all intermediate I's *) from this[unfolded relpow_fun_conv] obtain Is where stepsIs: "\ i. i < len \ (Is (Suc i), Is i) \ step_rel" and IsI: "Is 0 = I" "Is len = I" by auto { fix i assume "i \ len" hence "i - 1 < len" using len0 by auto from stepsIs[unfolded step_rel_def, OF this] have "Is i \ valid_I" by (cases i, auto) } note Is_valid = this from stepsIs[unfolded step_rel_def] have "\ i. \ l c h k. i < len \ cond (Is i) (Is (Suc i)) l c h k" by auto (* obtain all intermediate c's h's, l's, k's *) from choice[OF this] obtain ls where "\ i. \ c h k. i < len \ cond (Is i) (Is (Suc i)) (ls i) c h k" by auto from choice[OF this] obtain cs where "\ i. \ h k. i < len \ cond (Is i) (Is (Suc i)) (ls i) (cs i) h k" by auto from choice[OF this] obtain hs where "\ i. \ k. i < len \ cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) k" by auto from choice[OF this] obtain ks where cond: "\ i. i < len \ cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) (ks i)" by auto (* finally derive contradiction *) let ?R = "{hs i | i. i < len}" define r where "r = Max ?R" from cond[OF len0] have "hs 0 \ I" using IsI unfolding cond_def by auto hence R0: "hs 0 \ ?R" using len0 by auto have finR: "finite ?R" by auto from Max_in[OF finR] R0 have rR: "r \ ?R" unfolding r_def[symmetric] by auto then obtain p where rp: "r = hs p" and p: "p < len" by auto from Max_ge[OF finR, folded r_def] have rLarge: "i < len \ hs i \ r" for i by auto have exq: "\q. ks q = r \ q < len" proof (rule ccontr) assume neg: "\?thesis" show False proof(cases "r \ I") case True have 1: "j\{Suc p..len} \ r \ Is j" for j proof(induction j rule: less_induct) case (less j) from less(2) have j_bounds: "j = Suc p \ j > Suc p" by auto from less(2) have j_len: "j \ len" by auto have pj_cond: "j = Suc p \ cond (Is p) (Is j) (ls p) (cs p) (hs p) (ks p)" using cond p by blast have r_neq_ksp: "r \ ks p" using p neg by auto have "j = Suc p \ Is j = insert (ks p) (Is p - {r})" using rp cond pj_cond cond_def[of "Is p" "Is j" _ _ r] by blast hence c1: "j = Suc p \ r \ Is j" using r_neq_ksp by simp have IH: "\t. t < j \ t \ {Suc p..len} \ r \ Is t" by fact have r_neq_kspj: "j > Suc p \ j \ len \ r \ ks (j-1)" using j_len neg IH by auto have jsucj_cond: "j > Suc p \ j \ len \ Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})" using cond_def[of "Is (j-1)" "Is j"] cond by (metis (no_types, lifting) Suc_less_eq2 diff_Suc_1 le_simps(3)) hence "j > Suc p \ j \ len \ r \ insert (ks (j-1)) (Is (j-1))" using IH r_neq_kspj by auto hence "j > Suc p \ j \ len \ r \ Is j" using jsucj_cond by simp then show ?case using j_bounds j_len c1 by blast qed then show ?thesis using neg IsI(2) True p by auto next case False have 2: "j\{0..p} \ r \ Is j" for j proof(induction j rule: less_induct) case(less j) from less(2) have j_bound: "j \ p" by auto have r_nin_Is0: "r \ Is 0" using IsI(1) False by simp have IH: "\t. t < j \ t \ {0..p} \ r \ Is t" using less.IH by blast have j_neq_ksjpred: "j > 0 \ r \ ks (j -1)" using neg j_bound p by auto have Is_jpredj: "j > 0 \ Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})" using cond_def[of "Is (j-1)" "Is j" _ _ "hs (j-1)" "ks (j-1)"] cond by (metis (full_types) One_nat_def Suc_pred diff_le_self j_bound le_less_trans p) have "j > 0 \ r \ insert (ks (j-1)) (Is (j-1))" using j_neq_ksjpred IH j_bound by fastforce hence "j > 0 \ r \ Is j" using Is_jpredj by blast then show ?case using j_bound r_nin_Is0 by blast qed have 3: "r \ Is p" using rp cond cond_def p by blast then show ?thesis using 2 3 by auto qed qed then obtain q where q1: "ks q = r" and q_len: "q < len" by blast { fix t i1 i2 assume "i1 < len" "i2 < len" "t < m" assume "t\ Is i1" "t\ Is i2" have "\j < len. t = hs j" proof (rule ccontr) assume "\ ?thesis" hence hst: "\ j. j < len \ hs j \ t" by auto have main: "t \ Is (i + k) \ i + k \ len \ t \ Is k" for i k proof (induct i) case (Suc i) hence i: "i + k < len" by auto from cond[OF this, unfolded cond_def] have "Is (Suc i + k) = insert (ks (i + k)) (Is (i + k) - {hs (i + k)})" by auto from Suc(2)[unfolded this] hst[OF i] have "t \ Is (i + k)" by auto from Suc(1)[OF this] i show ?case by auto qed auto from main[of i2 0] \i2 < len\ \t \ Is i2\ have "t \ Is 0" by auto with IsI have "t \ Is len" by auto with main[of "len - i1" i1] \i1 < len\ have "t \ Is i1" by auto with \t \ Is i1\ show False by blast qed } note innotin = this { fix i assume i: "i \ {Suc r.. Is p" have "i \ Is q" proof (rule ccontr) have i_range: "i < m" using i by simp assume "\ ?thesis" then have ex: "\j < len. i = hs j" using innotin[OF p q_len i_range i_in_Isp] by simp then obtain j where j_hs: "i = hs j" by blast have "i>r" using i by simp then show False using j_hs p rLarge ex by force qed } hence "(i \ Is p) \ (i \ Is q)" by blast } note bla = this have blin: "b = lincomb (ls p) (a ` (Is p))" using cond_def p cond by blast have carrDp: "(a ` (Is p)) \ carrier_vec n " using Is_valid valid_I_def a p by (smt image_subset_iff less_imp_le_nat mem_Collect_eq subsetD) have carrcq: "cs q \ carrier_vec n" using cond cond_def q_len by simp have ineq1: "(cs q) \ b < 0" using cond_def q_len cond by blast let ?Isp_lt_r = "{x \ Is p . x < r}" let ?Isp_gt_r = "{x \ Is p . x > r}" have Is_disj: "?Isp_lt_r \ ?Isp_gt_r = {}" using Is_valid by auto have "?Isp_lt_r \ Is p" by simp hence Isp_lt_0m: "?Isp_lt_r \ {0.. Is p" by simp hence Isp_gt_0m: "?Isp_gt_r \ {0.. {0.. {0.. {0.. {0.. B = {}" have "r \ Is p" using rp p cond unfolding cond_def by simp hence r_lt_m: "r < m" using p Is_valid[of p] unfolding valid_I_def by auto hence 1: "A \ {0.. {0.. a ` B = {}" using inj_on_image_Int[OF inj_a 1 2] ABinters by auto } note inja = this have "(Is p \ {0.. (Is p \ {r}) = {}" by auto hence "a ` (Is p \ {0.. Is p \ {r}) = a ` (Is p \ {0.. a ` (Is p \ {r})" using inj_a by auto moreover have "Is p \ {0.. Is p \ {r} \ {0.. {0.. {Suc r.. {0.. {0.. {0.. Is p \ {r}) \ (Is p \ {Suc r.. {0.. a ` (Is p \ {r})) \ a ` (Is p \ {Suc r.. {0.. Is p \ {r}" "Is p \ {Suc r.. {0.. Is p \ {r} \ Is p \ {Suc r ..< m}" using rp p Is_valid[of p] unfolding valid_I_def by auto have gtr: "(\w \ (a ` (Is p \ {Suc r ..< m})). ((ls p) w) * (cs q \ w)) = 0" proof (rule sum.neutral, clarify) fix w assume w1: "w \ Is p" and w2: "w\{Suc r.. Is q" using bla[OF w2] w1 by blast moreover have "hs q \ r" using rR rLarge using q_len by blast ultimately have "w \ hs q" using w2 by simp hence "w \ Is q -{hs q}" using w1 w_in_q by auto moreover have "Is q - {hs q} \ {0.. span ( a ` (Is q - {hs q}))" using a by (intro span_mem, auto) moreover have "cs q \ carrier_vec n \ span (a ` (Is q - {hs q})) = { x. x \ carrier_vec n \ cs q \ x = 0}" using cond[of q] q_len unfolding cond_def by auto ultimately have "(cs q) \ (a w) = 0" using a w2 by simp then show "ls p (a w) * (cs q \ a w) = 0" by simp qed note pp = cond[OF p, unfolded cond_def rp[symmetric]] note qq = cond[OF q_len, unfolded cond_def q1] have "(cs q) \ b = (cs q) \ lincomb (ls p) (a ` (Is p))" using blin by auto also have "\ = (\w \ (a ` (Is p)). ((ls p) w) * (cs q \ w))" by (subst lincomb_scalar_prod_right[OF carrDp carrcq], simp) also have "\ = (\w \ (a ` (Is p \ {0.. a ` (Is p \ {r}) \ a ` (Is p \ {Suc r.. w))" by (subst (1) split, rule sum.cong, auto) also have "\ = (\w \ (a ` (Is p \ {0.. w)) + (\w \ (a ` (Is p \ {r})). ((ls p) w) * (cs q \ w)) + (\w \ (a ` (Is p \ {Suc r ..< m})). ((ls p) w) * (cs q \ w))" apply (subst sum.union_disjoint[OF _ _ one]) apply (force+)[2] apply (subst sum.union_disjoint) apply (force+)[2] apply (rule inja) by auto also have "\ = (\w \ (a ` (Is p \ {0.. w)) + (\w \ (a ` (Is p \ {r})). ((ls p) w) * (cs q \ w))" using sum.neutral gtr by simp also have "\ > 0 + 0" proof (intro add_le_less_mono sum_nonneg mult_nonneg_nonneg) { fix x assume x: "x \ a ` (Is p \ {0.. ls p x" using pp x by auto show "0 \ cs q \ x" using qq x by auto } have "r \ Is p" using pp by blast hence "a ` (Is p \ {r}) = {a r}" by auto hence id: "(\w\a ` (Is p \ {r}). ls p w * (cs q \ w)) = ls p (a r) * (cs q \ a r)" by simp show "0 < (\w\a ` (Is p \ {r}). ls p w * (cs q \ w))" unfolding id proof (rule mult_neg_neg) show "ls p (a r) < 0" using pp by auto show "cs q \ a r < 0" using qq by auto qed qed finally have "cs q \ b > 0" by simp moreover have "cs q \ b < 0" using qq by blast ultimately show False by auto qed lemma fundamental_theorem_neg_C_or_B_in_context: assumes W: "W = a ` {0 ..< m}" shows "(\ U. U \ W \ card U = n \ lin_indpt U \ b \ finite_cone U) \ (\c U. U \ W \ c \ {normal_vector U, - normal_vector U} \ Suc (card U) = n \ lin_indpt U \ (\w \ W. 0 \ c \ w) \ c \ b < 0)" using acyclic_imp_goal[unfolded goal_def, OF acyclic_step_rel] proof assume "\I. I\{0.. card (a ` I) = n \ lin_indpt (a ` I) \ b \ finite_cone (a ` I)" thus ?thesis unfolding W by (intro disjI1, blast) next assume "\c I. I \ {0.. c \ {normal_vector (a ` I), - normal_vector (a ` I)} \ Suc (card (a ` I)) = n \ lin_indpt (a ` I) \ (\i c \ a i) \ c \ b < 0" then obtain c I where "I \ {0.. c \ {normal_vector (a ` I), - normal_vector (a ` I)} \ Suc (card (a ` I)) = n \ lin_indpt (a ` I) \ (\i c \ a i) \ c \ b < 0" by auto thus ?thesis unfolding W by (intro disjI2 exI[of _ c] exI[of _ "a ` I"], auto) qed end lemma fundamental_theorem_of_linear_inequalities_C_imp_B_full_dim: assumes A: "A \ carrier_vec n" and fin: "finite A" and span: "span A = carrier_vec n" (* this condition was a wlog in the proof *) and b: "b \ carrier_vec n" and C: "\ c B. B \ A \ c \ {normal_vector B, - normal_vector B} \ Suc (card B) = n \ lin_indpt B \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" shows "\ B \ A. lin_indpt B \ card B = n \ b \ finite_cone B" proof - from finite_distinct_list[OF fin] obtain as where Aas: "A = set as" and dist: "distinct as" by auto define m where "m = length as" define a where "a = (\ i. as ! i)" have inj: "inj_on a {0..< (m :: nat)}" and id: "A = a ` {0.. {b. b \ carrier_vec n \ (\ B c. B \ A \ c \ {normal_vector B, - normal_vector B} \ Suc (card B) = n \ lin_indpt B \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0)}" defines "HyperA \ {b. b \ carrier_vec n \ (\ c. c \ carrier_vec n \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0)}" defines "lin_indpt_cone \ \ { finite_cone B | B. B \ A \ card B = n \ lin_indpt B}" assumes A: "A \ carrier_vec n" and fin: "finite A" and span: "span A = carrier_vec n" shows "cone A = lin_indpt_cone" "cone A = HyperN" "cone A = HyperA" proof - have "lin_indpt_cone \ cone A" unfolding lin_indpt_cone_def cone_def using fin finite_cone_mono A by auto moreover have "cone A \ HyperA" proof fix c assume cA: "c \ cone A" from fundamental_theorem_of_linear_inequalities_A_imp_D[OF A fin this] cone_carrier[OF A] cA show "c \ HyperA" unfolding HyperA_def by auto qed moreover have "HyperA \ HyperN" proof fix c assume "c \ HyperA" hence False: "\ v. v \ carrier_vec n \ (\a\<^sub>i\A. 0 \ v \ a\<^sub>i) \ v \ c < 0 \ False" and c: "c \ carrier_vec n" unfolding HyperA_def by auto show "c \ HyperN" unfolding HyperN_def proof (standard, intro conjI c notI, clarify, goal_cases) case (1 W nv) with A fin have fin: "finite W" and W: "W \ carrier_vec n" by (auto intro: finite_subset) show ?case using False[of nv] 1 normal_vector[OF fin _ _ W] by auto qed qed moreover have "HyperN \ lin_indpt_cone" proof fix b assume "b \ HyperN" from this[unfolded HyperN_def] fundamental_theorem_of_linear_inequalities_C_imp_B_full_dim[OF A fin span, of b] show "b \ lin_indpt_cone" unfolding lin_indpt_cone_def by auto qed ultimately show "cone A = lin_indpt_cone" "cone A = HyperN" "cone A = HyperA" by auto qed lemma fundamental_theorem_of_linear_inequalities_C_imp_B: assumes A: "A \ carrier_vec n" and fin: "finite A" and b: "b \ carrier_vec n" and C: "\ c A'. c \ carrier_vec n \ A' \ A \ Suc (card A') = dim_span (insert b A) \ (\ a \ A'. c \ a = 0) \ lin_indpt A' \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" shows "\ B \ A. lin_indpt B \ card B = dim_span A \ b \ finite_cone B" proof - from exists_lin_indpt_sublist[OF A] obtain A' where lin: "lin_indpt_list A'" and span: "span (set A') = span A" and A'A: "set A' \ A" by auto hence linA': "lin_indpt (set A')" unfolding lin_indpt_list_def by auto from A'A A have A': "set A' \ carrier_vec n" by auto have dim_spanA: "dim_span A = card (set A')" by (rule sym, rule same_span_imp_card_eq_dim_span[OF A' A span linA']) show ?thesis proof (cases "b \ span A") case False with span have "b \ span (set A')" by auto with lin have linAb: "lin_indpt_list (A' @ [b])" unfolding lin_indpt_list_def using lin_dep_iff_in_span[OF A' _ b] span_mem[OF A', of b] b by auto interpret gso: gram_schmidt_fs_lin_indpt n "A' @ [b]" by (standard, insert linAb[unfolded lin_indpt_list_def], auto) let ?m = "length A'" define c where "c = - gso.gso ?m" have c: "c \ carrier_vec n" using gso.gso_carrier[of ?m] unfolding c_def by auto from gso.gso_times_self_is_norm[of ?m] have "b \ gso.gso ?m = sq_norm (gso.gso ?m)" unfolding c_def using b c by auto also have "\ > 0" using gso.sq_norm_pos[of ?m] by auto finally have cb: "c \ b < 0" using b c comm_scalar_prod[OF b c] unfolding c_def by auto { fix a assume "a \ A" hence "a \ span (set A')" unfolding span using span_mem[OF A] by auto from finite_in_span[OF _ A' this] obtain l where "a = lincomb l (set A')" by auto hence "c \ a = c \ lincomb l (set A')" by simp also have "\ = 0" by (subst lincomb_scalar_prod_right[OF A' c], rule sum.neutral, insert A', unfold set_conv_nth, insert gso.gso_scalar_zero[of ?m] c, auto simp: c_def nth_append ) finally have "c \ a = 0" . } note cA = this have "\ c A'. c \ carrier_vec n \ A' \ A \ Suc (card A') = dim_span (insert b A) \ (\ a \ A'. c \ a = 0) \ lin_indpt A' \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" proof (intro exI[of _ c] exI[of _ "set A'"] conjI A'A linA' cb c) show "\a\set A'. c \ a = 0" "\a\<^sub>i\A. 0 \ c \ a\<^sub>i" using cA A'A by auto have "dim_span (insert b A) = Suc (dim_span A)" by (rule dim_span_insert[OF A b False]) also have "\ = Suc (card (set A'))" unfolding dim_spanA .. finally show "Suc (card (set A')) = dim_span (insert b A)" .. qed with C have False by blast thus ?thesis .. next case bspan: True define N where "N = normal_vectors A'" from normal_vectors[OF lin, folded N_def] have N: "set N \ carrier_vec n" and orthA'N: "\ w nv. w \ set A' \ nv \ set N \ nv \ w = 0" and linAN: "lin_indpt_list (A' @ N)" and lenAN: "length (A' @ N) = n" and disj: "set A' \ set N = {}" by auto from linAN lenAN have full_span': "span (set (A' @ N)) = carrier_vec n" using lin_indpt_list_length_eq_n by blast hence full_span'': "span (set A' \ set N) = carrier_vec n" by auto from A N A' have AN: "A \ set N \ carrier_vec n" and A'N: "set (A' @ N) \ carrier_vec n" by auto hence "span (A \ set N) \ carrier_vec n" by (simp add: span_is_subset2) with A'A span_is_monotone[of "set (A' @ N)" "A \ set N", unfolded full_span'] have full_span: "span (A \ set N) = carrier_vec n" unfolding set_append by fast from fin have finAN: "finite (A \ set N)" by auto note fundamental = fundamental_theorem_of_linear_inequalities_full_dim[OF AN finAN full_span] show ?thesis proof (cases "b \ cone (A \ set N)") case True from this[unfolded fundamental(1)] obtain C where CAN: "C \ A \ set N" and cardC: "card C = n" and linC: "lin_indpt C" and bC: "b \ finite_cone C" by auto have finC: "finite C" using finite_subset[OF CAN] fin by auto from CAN A N have C: "C \ carrier_vec n" by auto from bC[unfolded finite_cone_def nonneg_lincomb_def] finC obtain c where bC: "b = lincomb c C" and nonneg: "\ b. b \ C \ c b \ 0" by auto let ?C = "C - set N" show ?thesis proof (intro exI[of _ ?C] conjI) from subset_li_is_li[OF linC] show "lin_indpt ?C" by auto show CA: "?C \ A" using CAN by auto have bc: "b = lincomb c (?C \ (C \ set N))" unfolding bC by (rule arg_cong[of _ _ "lincomb _"], auto) have "b = lincomb c (?C - C \ set N)" proof (rule orthogonal_cone(2)[OF A N fin full_span'' orthA'N refl span A'A linAN lenAN _ CA _ bc]) show "\w\set N. w \ b = 0" using ortho_span'[OF A' N _ bspan[folded span]] orthA'N by auto qed auto also have "?C - C \ set N = ?C" by auto finally have "b = lincomb c ?C" . with nonneg have "nonneg_lincomb c ?C b" unfolding nonneg_lincomb_def by auto thus "b \ finite_cone ?C" unfolding finite_cone_def using finite_subset[OF CA fin] by auto have Cid: "C \ set N \ ?C = C" by auto have "length A' + length N = n" by fact also have "\ = card (C \ set N \ ?C) " using Cid cardC by auto also have "\ = card (C \ set N) + card ?C" by (subst card_Un_disjoint, insert finC, auto) also have "\ \ length N + card ?C" by (rule add_right_mono, rule order.trans, rule card_mono[OF finite_set[of N]], auto intro: card_length) also have "length A' = card (set A')" using lin[unfolded lin_indpt_list_def] distinct_card[of A'] by auto finally have le: "dim_span A \ card ?C" using dim_spanA by auto have CA: "?C \ span A" using CA C in_own_span[OF A] by auto have linC: "lin_indpt ?C" using subset_li_is_li[OF linC] by auto show "card ?C = dim_span A" using card_le_dim_span[OF _ CA linC] le C by force qed next case False from False[unfolded fundamental(2)] b obtain C c where CAN: "C \ A \ set N" and cardC: "Suc (card C) = n" and linC: "lin_indpt C" and contains: "(\a\<^sub>i\A \ set N. 0 \ c \ a\<^sub>i)" and cb: "c \ b < 0" and nv: "c \ {normal_vector C, - normal_vector C}" by auto from CAN A N have C: "C \ carrier_vec n" by auto from cardC have cardCn: "card C < n" by auto from finite_subset[OF CAN] fin have finC: "finite C" by auto let ?C = "C - set N" note nv' = normal_vector(1-4)[OF finC cardC linC C] from nv' nv have c: "c \ carrier_vec n" by auto have "\ c A'. c \ carrier_vec n \ A' \ A \ Suc (card A') = dim_span (insert b A) \ (\ a \ A'. c \ a = 0) \ lin_indpt A' \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0" proof (intro exI[of _ c] exI[of _ ?C] conjI cb c) show CA: "?C \ A" using CAN by auto show "\a\<^sub>i\A. 0 \ c \ a\<^sub>i" using contains by auto show lin': "lin_indpt ?C" using subset_li_is_li[OF linC] by auto show sC0: "\a\ ?C. c \ a = 0" using nv' nv C by auto have Cid: "C \ set N \ ?C = C" by auto have "dim_span (set A') = card (set A')" by (rule sym, rule same_span_imp_card_eq_dim_span[OF A' A' refl linA']) also have "\ = length A'" using lin[unfolded lin_indpt_list_def] distinct_card[of A'] by auto finally have dimA': "dim_span (set A') = length A'" . from bspan have "span (insert b A) = span A" using b A using already_in_span by auto from dim_span_cong[OF this[folded span]] dimA' have dimbA: "dim_span (insert b A) = length A'" by simp also have "\ = Suc (card ?C)" proof (rule ccontr) assume neq: "length A' \ Suc (card ?C)" have "length A' + length N = n" by fact also have "\ = Suc (card (C \ set N \ ?C))" using Cid cardC by auto also have "\ = Suc (card (C \ set N) + card ?C)" by (subst card_Un_disjoint, insert finC, auto) finally have id: "length A' + length N = Suc (card (C \ set N) + card ?C)" . have le1: "card (C \ set N) \ length N" by (metis Int_lower2 List.finite_set card_length card_mono inf.absorb_iff2 le_inf_iff) from CA C A have CsA: "?C \ span (set A')" unfolding span by (meson in_own_span order.trans) from card_le_dim_span[OF _ this lin'] C have le2: "card ?C \ length A'" unfolding dimA' by auto from id le1 le2 neq have id2: "card ?C = length A'" by linarith+ from card_eq_dim_span_imp_same_span[OF A' CsA lin' id2[folded dimA']] have "span ?C = span A" unfolding span by auto with bspan have "b \ span ?C" by auto from orthocompl_span[OF _ _ c this] C sC0 have "c \ b = 0" by auto with cb show False by simp qed finally show "Suc (card ?C) = dim_span (insert b A)" by simp qed with assms(4) have False by blast thus ?thesis .. qed qed qed lemma fundamental_theorem_of_linear_inequalities: fixes A :: "'a vec set" defines "HyperN \ {b. b \ carrier_vec n \ (\ c B. c \ carrier_vec n \ B \ A \ Suc (card B) = dim_span (insert b A) \ lin_indpt B \ (\ a \ B. c \ a = 0) \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0)}" defines "HyperA \ {b. b \ carrier_vec n \ (\ c. c \ carrier_vec n \ (\ a\<^sub>i \ A. c \ a\<^sub>i \ 0) \ c \ b < 0)}" defines "lin_indpt_cone \ \ { finite_cone B | B. B \ A \ card B = dim_span A \ lin_indpt B}" assumes A: "A \ carrier_vec n" and fin: "finite A" shows "cone A = lin_indpt_cone" "cone A = HyperN" "cone A = HyperA" proof - have "lin_indpt_cone \ cone A" unfolding lin_indpt_cone_def cone_def using fin finite_cone_mono A by auto moreover have "cone A \ HyperA" using fundamental_theorem_of_linear_inequalities_A_imp_D[OF A fin] cone_carrier[OF A] unfolding HyperA_def by blast moreover have "HyperA \ HyperN" unfolding HyperA_def HyperN_def by blast moreover have "HyperN \ lin_indpt_cone" proof fix b assume "b \ HyperN" from this[unfolded HyperN_def] fundamental_theorem_of_linear_inequalities_C_imp_B[OF A fin, of b] show "b \ lin_indpt_cone" unfolding lin_indpt_cone_def by blast qed ultimately show "cone A = lin_indpt_cone" "cone A = HyperN" "cone A = HyperA" by auto qed corollary Caratheodory_theorem: assumes A: "A \ carrier_vec n" shows "cone A = \ {finite_cone B |B. B \ A \ lin_indpt B}" proof show "\ {finite_cone B |B. B \ A \ lin_indpt B} \ cone A" unfolding cone_def using fin[OF fin_dim _ subset_trans[OF _ A]] by auto { fix a assume "a \ cone A" from this[unfolded cone_def] obtain B where finB: "finite B" and BA: "B \ A" and a: "a \ finite_cone B" by auto from BA A have B: "B \ carrier_vec n" by auto hence "a \ cone B" using finB a by (simp add: cone_iff_finite_cone) with fundamental_theorem_of_linear_inequalities(1)[OF B finB] obtain C where CB: "C \ B" and a: "a \ finite_cone C" and "lin_indpt C" by auto with BA have "a \ \ {finite_cone B |B. B \ A \ lin_indpt B}" by auto } thus "\ {finite_cone B |B. B \ A \ lin_indpt B} \ cone A" by blast qed end end \ No newline at end of file