diff --git a/thys/Jordan_Normal_Form/VS_Connect.thy b/thys/Jordan_Normal_Form/VS_Connect.thy --- a/thys/Jordan_Normal_Form/VS_Connect.thy +++ b/thys/Jordan_Normal_Form/VS_Connect.thy @@ -1,1327 +1,1323 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) (* with contributions from Alexander Bentkamp, Universität des Saarlandes *) section \Matrices as Vector Spaces\ text \This theory connects the Matrix theory with the VectorSpace theory of Holden Lee. As a consequence notions like span, basis, linear dependence, etc. are available for vectors and matrices of the Matrix-theory.\ theory VS_Connect imports Matrix Missing_VectorSpace Determinant begin hide_const (open) Multiset.mult hide_const (open) Polynomial.smult hide_const (open) Modules.module hide_const (open) subspace hide_fact (open) subspace_def named_theorems class_ring_simps abbreviation class_ring :: "'a :: {times,plus,one,zero} ring" where "class_ring \ \ carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+) \" interpretation class_semiring: semiring "class_ring :: 'a :: semiring_1 ring" rewrites [class_ring_simps]: "carrier class_ring = UNIV" and [class_ring_simps]: "mult class_ring = (*)" and [class_ring_simps]: "add class_ring = (+)" and [class_ring_simps]: "one class_ring = 1" and [class_ring_simps]: "zero class_ring = 0" and [class_ring_simps]: "pow (class_ring :: 'a ring) = (^)" and [class_ring_simps]: "finsum (class_ring :: 'a ring) = sum" proof - let ?r = "class_ring :: 'a ring" show "semiring ?r" by (unfold_locales, auto simp: field_simps) then interpret semiring ?r . { fix x y have "x [^]\<^bsub>?r\<^esub> y = x ^ y" by (induct y, auto simp: power_commutes) } thus "([^]\<^bsub>?r\<^esub>) = (^)" by (intro ext) { fix f and A :: "'b set" have "finsum ?r f A = sum f A" by (induct A rule: infinite_finite_induct, auto) } thus "finsum ?r = sum" by (intro ext) qed auto interpretation class_ring: ring "class_ring :: 'a :: ring_1 ring" rewrites "carrier class_ring = UNIV" and "mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and [class_ring_simps]: "a_inv (class_ring :: 'a ring) = uminus" and [class_ring_simps]: "a_minus (class_ring :: 'a ring) = minus" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" proof - let ?r = "class_ring :: 'a ring" interpret semiring ?r .. show "finsum ?r = sum" "pow ?r = (^)" by (simp_all add: class_ring_simps) { fix x :: 'a have "\y. x + y = 0" by (rule exI[of _ "-x"], auto) } note [simp] = this show "ring ?r" by (unfold_locales, auto simp: field_simps Units_def) then interpret ring ?r . { fix x :: 'a have "\\<^bsub>?r\<^esub> x = - x" unfolding a_inv_def m_inv_def by (rule the1_equality, rule ex1I[of _ "- x"], auto simp: minus_unique) } note ainv = this thus inv: "a_inv ?r = uminus" by (intro ext) { fix x y :: 'a have "x \\<^bsub>?r\<^esub> y = x - y" apply (subst a_minus_def) using inv by auto } thus "(\x y. x \\<^bsub>?r\<^esub> y) = minus" by (intro ext) qed (auto simp: class_ring_simps) interpretation class_cring: cring "class_ring :: 'a :: comm_ring_1 ring" rewrites "carrier class_ring = UNIV" and "mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and "a_inv (class_ring :: 'a ring) = uminus" and "a_minus (class_ring :: 'a ring) = minus" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" and [class_ring_simps]: "finprod class_ring = prod" proof - let ?r = "class_ring :: 'a ring" interpret ring ?r .. show "cring ?r" by (unfold_locales, auto) then interpret cring ?r . show "a_inv (class_ring :: 'a ring) = uminus" and "a_minus (class_ring :: 'a ring) = minus" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" by (simp_all add: class_ring_simps) { fix f and A :: "'b set" have "finprod ?r f A = prod f A" by (induct A rule: infinite_finite_induct, auto) } thus "finprod ?r = prod" by (intro ext) qed (auto simp: class_ring_simps) definition div0 :: "'a :: {one,plus,times,zero}" where "div0 \ m_inv (class_ring :: 'a ring) 0" lemma class_field: "field (class_ring :: 'a :: field ring)" (is "field ?r") proof - interpret cring ?r .. { fix x :: 'a have "x \ 0 \ \xa. xa * x = 1 \ x * xa = 1" by (intro exI[of _ "inverse x"], auto) } note [simp] = this show "field ?r" by (unfold_locales, auto simp: Units_def) qed interpretation class_field: field "class_ring :: 'a :: field ring" rewrites "carrier class_ring = UNIV" and "mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and "a_inv class_ring = uminus" and "a_minus class_ring = minus" and "pow class_ring = (^)" and "finsum class_ring = sum" and "finprod class_ring = prod" and [class_ring_simps]: "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)" (* problem that m_inv ?r 0 = inverse 0 is not guaranteed *) proof - let ?r = "class_ring :: 'a ring" show "field ?r" using class_field. then interpret field ?r. show "a_inv ?r = uminus" and "a_minus ?r = minus" and "pow ?r = (^)" and "finsum ?r = sum" and "finprod ?r = prod" by (fact class_ring_simps)+ show "inv\<^bsub>?r\<^esub> x = (if x = 0 then div0 else inverse x)" proof (cases "x = 0") case True thus ?thesis unfolding div0_def by simp next case False thus ?thesis unfolding m_inv_def by (intro the1_equality ex1I[of _ "inverse x"], auto simp: inverse_unique) qed qed (auto simp: class_ring_simps) lemmas matrix_vs_simps = module_mat_simps class_ring_simps definition class_field :: "'a :: field ring" where [class_ring_simps]: "class_field \ class_ring" locale matrix_ring = fixes n :: nat and field_type :: "'a :: field itself" begin abbreviation R where "R \ ring_mat TYPE('a) n n" sublocale ring R rewrites "carrier R = carrier_mat n n" and "add R = (+)" and "mult R = (*)" and "one R = 1\<^sub>m n" and "zero R = 0\<^sub>m n n" using ring_mat by (auto simp: ring_mat_simps) end lemma matrix_vs: "vectorspace (class_ring :: 'a :: field ring) (module_mat TYPE('a) nr nc)" proof - interpret abelian_group "module_mat TYPE('a) nr nc" by (rule abelian_group_mat) show ?thesis unfolding class_field_def by (unfold_locales, unfold matrix_vs_simps, auto simp: add_smult_distrib_left_mat add_smult_distrib_right_mat) qed locale vec_module = fixes f_ty::"'a::comm_ring_1 itself" and n::"nat" begin abbreviation V where "V \ module_vec TYPE('a) n" sublocale Module.module "class_ring :: 'a ring" V rewrites "carrier V = carrier_vec n" and "add V = (+)" and "zero V = 0\<^sub>v n" and "module.smult V = (\\<^sub>v)" and "carrier class_ring = UNIV" and "monoid.mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and "a_inv (class_ring :: 'a ring) = uminus" and "a_minus (class_ring :: 'a ring) = (-)" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" and "finprod (class_ring :: 'a ring) = prod" and "\X. X \ UNIV = True" (* These rewrite rules will clean lemmas *) and "\x. x \ UNIV = True" and "\a A. a \ A \ UNIV \ True" and "\P. P \ True \ P" and "\P. (True \ P) \ Trueprop P" apply unfold_locales apply (auto simp: module_vec_simps class_ring_simps Units_def add_smult_distrib_vec smult_add_distrib_vec intro!:bexI[of _ "- _"]) done end locale matrix_vs = fixes nr :: nat and nc :: nat and field_type :: "'a :: field itself" begin abbreviation V where "V \ module_mat TYPE('a) nr nc" sublocale vectorspace class_ring V rewrites "carrier V = carrier_mat nr nc" and "add V = (+)" and "mult V = (*)" and "one V = 1\<^sub>m nr" and "zero V = 0\<^sub>m nr nc" and "smult V = (\\<^sub>m)" and "carrier class_ring = UNIV" and "mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and "a_inv (class_ring :: 'a ring) = uminus" and "a_minus (class_ring :: 'a ring) = minus" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" and "finprod (class_ring :: 'a ring) = prod" and "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)" by (rule matrix_vs, auto simp: matrix_vs_simps class_field_def) end lemma vec_module: "module (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)" proof - interpret abelian_group "module_vec TYPE('a) n" apply (unfold_locales) unfolding module_vec_def Units_def using add_inv_exists_vec by auto show ?thesis unfolding class_field_def apply (unfold_locales) unfolding class_ring_simps unfolding module_vec_simps using add_smult_distrib_vec by (auto simp: smult_add_distrib_vec) qed lemma vec_vs: "vectorspace (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)" unfolding vectorspace_def using vec_module class_field by (auto simp: class_field_def) locale vec_space = fixes f_ty::"'a::field itself" and n::"nat" begin sublocale vec_module f_ty n. sublocale vectorspace class_ring V rewrites cV[simp]: "carrier V = carrier_vec n" and [simp]: "add V = (+)" and [simp]: "zero V = 0\<^sub>v n" and [simp]: "smult V = (\\<^sub>v)" and "carrier class_ring = UNIV" and "mult class_ring = (*)" and "add class_ring = (+)" and "one class_ring = 1" and "zero class_ring = 0" and "a_inv (class_ring :: 'a ring) = uminus" and "a_minus (class_ring :: 'a ring) = minus" and "pow (class_ring :: 'a ring) = (^)" and "finsum (class_ring :: 'a ring) = sum" and "finprod (class_ring :: 'a ring) = prod" and "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)" using vec_vs unfolding class_field_def by (auto simp: module_vec_simps class_ring_simps) lemma finsum_vec[simp]: "finsum_vec TYPE('a) n = finsum V" by (force simp: finsum_vec_def monoid_vec_def finsum_def finprod_def) lemma finsum_scalar_prod_sum: assumes f: "f : U \ carrier_vec n" and w: "w: carrier_vec n" shows "finsum V f U \ w = sum (\u. f u \ w) U" using w f proof (induct U rule: infinite_finite_induct) case (insert u U) hence f: "f : U \ carrier_vec n" "f u : carrier_vec n" by auto show ?case unfolding finsum_insert[OF insert(1) insert(2) f] apply (subst add_scalar_prod_distrib) using insert by auto qed auto lemma vec_neg[simp]: assumes "x : carrier_vec n" shows "\\<^bsub>V\<^esub> x = - x" unfolding a_inv_def m_inv_def apply simp apply (rule the_equality, intro conjI) using assms apply auto using M.minus_unique uminus_carrier_vec uminus_r_inv_vec by blast lemma finsum_dim: "finite A \ f \ A \ carrier_vec n \ dim_vec (finsum V f A) = n" proof(induct set:finite) case (insert a A) hence dfa: "dim_vec (f a) = n" by auto have f: "f \ A \ carrier_vec n" using insert by auto hence fa: "f a \ carrier_vec n" using insert by auto show ?case unfolding finsum_insert[OF insert(1) insert(2) f fa] using insert by auto qed simp lemma lincomb_dim: assumes fin: "finite X" and X: "X \ carrier_vec n" shows "dim_vec (lincomb a X) = n" proof - let ?f = "\v. a v \\<^sub>v v" have f: "?f \ X \ carrier_vec n" apply rule using X by auto show ?thesis unfolding lincomb_def using finsum_dim[OF fin f]. qed lemma finsum_index: assumes i: "i < n" and f: "f \ X \ carrier_vec n" and X: "X \ carrier_vec n" shows "finsum V f X $ i = sum (\x. f x $ i) X" using X f proof (induct X rule: infinite_finite_induct) case empty then show ?case using i by simp next case (insert x X) then have Xf: "finite X" and xX: "x \ X" and x: "x \ carrier_vec n" and X: "X \ carrier_vec n" and fx: "f x \ carrier_vec n" and f: "f \ X \ carrier_vec n" by auto have i2: "i < dim_vec (finsum V f X)" using i finsum_closed[OF f] by auto have ix: "i < dim_vec x" using x i by auto show ?case unfolding finsum_insert[OF Xf xX f fx] unfolding sum.insert[OF Xf xX] unfolding index_add_vec(1)[OF i2] using insert lincomb_def by auto qed (insert i, auto) lemma lincomb_index: assumes i: "i < n" and X: "X \ carrier_vec n" shows "lincomb a X $ i = sum (\x. a x * x $ i) X" proof - let ?f = "\x. a x \\<^sub>v x" have f: "?f : X \ carrier_vec n" using X by auto have point: "\v. v \ X \ (a v \\<^sub>v v) $ i = a v * v $ i" using i X by auto show ?thesis unfolding lincomb_def unfolding finsum_index[OF i f X] using point X by simp qed lemma append_insert: "set (xs @ [x]) = insert x (set xs)" by simp lemma lincomb_units: assumes i: "i < n" shows "lincomb a (set (unit_vecs n)) $ i = a (unit_vec n i)" unfolding lincomb_index[OF i unit_vecs_carrier] unfolding unit_vecs_first proof - let ?f = "\m i. \x\set (unit_vecs_first n m). a x * x $ i" have zero:"\m j. m \ j \ j < n \ ?f m j = 0" proof - fix m show "\j. m \ j \ j < n \ ?f m j = 0" proof (induction m) case (Suc m) hence mj:"m\j" and mj':"m\j" and jn:"j set (unit_vecs_first n m)" apply(subst unit_vecs_first_distinct) by auto show ?case unfolding unit_vecs_first.simps unfolding append_insert unfolding sum.insert[OF finite_set mem] unfolding index_unit_vec(1)[OF mn jn] unfolding Suc(1)[OF mj jn] using mj' by simp qed simp qed { fix m have "i < m \ m \ n \ ?f m i = a (unit_vec n i)" proof (induction m arbitrary: i) case (Suc m) hence iSm: "i < Suc m" and i:"i set (unit_vecs_first n m)" apply(subst unit_vecs_first_distinct) by auto show ?case unfolding unit_vecs_first.simps unfolding append_insert unfolding sum.insert[OF finite_set mem] unfolding index_unit_vec(1)[OF mn i] using zero Suc by (cases "i = m",auto) qed auto } thus "?f n i = a (unit_vec n i)" using assms by auto qed lemma lincomb_coordinates: assumes v: "v : carrier_vec n" defines "a \ (\u. v $ (THE i. u = unit_vec n i))" shows "lincomb a (set (unit_vecs n)) = v" proof - have a: "a \ set (unit_vecs n) \ UNIV" by auto have fvu: "\i. i < n \ v $ i = a (unit_vec n i)" unfolding a_def using unit_vec_eq by auto show ?thesis apply rule unfolding lincomb_dim[OF finite_set unit_vecs_carrier] using v lincomb_units fvu by auto qed lemma span_unit_vecs_is_carrier: "span (set (unit_vecs n)) = carrier_vec n" (is "?L = ?R") proof (rule;rule) fix v assume vsU: "v \ ?L" show "v \ ?R" proof - obtain a where v: "v = lincomb a (set (unit_vecs n))" using vsU unfolding finite_span[OF finite_set unit_vecs_carrier] by auto thus ?thesis using lincomb_closed[OF unit_vecs_carrier] by auto qed next fix v::"'a vec" assume v: "v \ ?R" show "v \ ?L" unfolding span_def using lincomb_coordinates[OF v,symmetric] by auto qed lemma fin_dim[simp]: "fin_dim" unfolding fin_dim_def apply (intro eqTrueI exI conjI) using span_unit_vecs_is_carrier unit_vecs_carrier by auto lemma unit_vecs_basis: "basis (set (unit_vecs n))" unfolding basis_def span_unit_vecs_is_carrier proof (intro conjI) show "\ lin_dep (set (unit_vecs n))" proof assume "lin_dep (set (unit_vecs n))" from this[unfolded lin_dep_def] obtain A a v where fin: "finite A" and A: "A \ set (unit_vecs n)" and lc: "lincomb a A = 0\<^sub>v n" and v: "v \ A" and av: "a v \ 0" by auto from v A obtain i where i: "i < n" and vu: "v = unit_vec n i" unfolding unit_vecs_def by auto define b where "b = (\ x. if x \ A then a x else 0)" have id: "A \ (set (unit_vecs n) - A) = set (unit_vecs n)" using A by auto from lincomb_index[OF i unit_vecs_carrier] have "lincomb b (set (unit_vecs n)) $ i = (\x\ (A \ (set (unit_vecs n) - A)). b x * x $ i)" unfolding id . also have "\ = (\x\ A. b x * x $ i) + (\x\ set (unit_vecs n) - A. b x * x $ i)" by (rule sum.union_disjoint, insert fin, auto) also have "(\x\ A. b x * x $ i) = (\x\ A. a x * x $ i)" by (rule sum.cong, auto simp: b_def) also have "\ = lincomb a A $ i" by (subst lincomb_index[OF i], insert A unit_vecs_carrier, auto) also have "\ = 0" unfolding lc using i by simp also have "(\x\ set (unit_vecs n) - A. b x * x $ i) = 0" by (rule sum.neutral, auto simp: b_def) finally have "lincomb b (set (unit_vecs n)) $ i = 0" by simp from lincomb_units[OF i, of b, unfolded this] have "b v = 0" unfolding vu by simp with v av show False unfolding b_def by simp qed qed (insert unit_vecs_carrier, auto) lemma unit_vecs_length[simp]: "length (unit_vecs n) = n" unfolding unit_vecs_def by auto lemma unit_vecs_distinct: "distinct (unit_vecs n)" unfolding distinct_conv_nth unit_vecs_length proof (intro allI impI) fix i j assume *: "i < n" "j < n" "i \ j" show "unit_vecs n ! i \ unit_vecs n ! j" proof assume "unit_vecs n ! i = unit_vecs n ! j" from arg_cong[OF this, of "\ v. v $ i"] show False using * unfolding unit_vecs_def by auto qed qed lemma dim_is_n: "dim = n" unfolding dim_basis[OF finite_set unit_vecs_basis] unfolding distinct_card[OF unit_vecs_distinct] by simp end locale mat_space = vec_space f_ty nc for f_ty::"'a::field itself" and nc::"nat" + fixes nr :: "nat" begin abbreviation M where "M \ ring_mat TYPE('a) nc nr" end context vec_space begin lemma fin_dim_span: assumes "finite A" "A \ carrier V" shows "vectorspace.fin_dim class_ring (vs (span A))" proof - have "vectorspace class_ring (span_vs A)" using assms span_is_subspace subspace_def subspace_is_vs by simp have "A \ span A" using assms in_own_span by simp have "submodule class_ring (span A) V" using assms span_is_submodule by simp have "LinearCombinations.module.span class_ring (vs (span A)) A = carrier (vs (span A))" using span_li_not_depend(1)[OF \A \ span A\ \submodule class_ring (span A) V\] by auto then show ?thesis unfolding vectorspace.fin_dim_def[OF \vectorspace class_ring (span_vs A)\] using List.finite_set \A \ span A\ \vectorspace class_ring (vs (span A))\ vec_vs vectorspace.carrier_vs_is_self[OF \vectorspace class_ring (span_vs A)\] using assms(1) by auto qed lemma fin_dim_span_cols: assumes "A \ carrier_mat n nc" shows "vectorspace.fin_dim class_ring (vs (span (set (cols A))))" using fin_dim_span cols_dim List.finite_set assms carrier_matD(1) module_vec_simps(3) by force end context vec_module begin lemma lincomb_list_as_mat_mult: assumes "\w \ set ws. dim_vec w = n" shows "lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c" (is "?l ws c = ?r ws c") proof (insert assms, induct ws arbitrary: c) case Nil then show ?case by (auto simp: mult_mat_vec_def scalar_prod_def) next case (Cons w ws) { fix i assume i: "i < n" have "?l (w#ws) c = c 0 \\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \ Suc)" by (simp add: Cons o_def) also have "\ $ i = ?r (w#ws) c $ i" using Cons i index_smult_vec by (simp add: mat_of_cols_Cons_index_0 mat_of_cols_Cons_index_Suc o_def vec_Suc mult_mat_vec_def row_def length_Cons) finally have "?l (w#ws) c $ i = \". } with Cons show ?case by (intro eq_vecI, auto) qed lemma lincomb_vec_diff_add: assumes A: "A \ carrier_vec n" and BA: "B \ A" and fin_A: "finite A" and f: "f \ A \ UNIV" shows "lincomb f A = lincomb f (A-B) + lincomb f B" proof - have "A - B \ B = A" using BA by auto hence "lincomb f A = lincomb f (A - B \ B)" by simp also have "... = lincomb f (A-B) + lincomb f B" by (rule lincomb_union, insert assms, auto intro: finite_subset) finally show ?thesis . qed lemma dim_sumlist: assumes "\x\set xs. dim_vec x = n" shows "dim_vec (M.sumlist xs) = n" using assms by (induct xs, auto) lemma sumlist_nth: assumes "\x\set xs. dim_vec x = n" and "ij. (xs ! j) $ i) {0.. carrier_vec n" if x: "x\set xs" for x using snoc.prems x unfolding carrier_vec_def by auto have [simp]: "a \ carrier_vec n" using snoc.prems unfolding carrier_vec_def by auto have hyp: "M.sumlist xs $ i = (\j = 0..j = 0..j = 0.. carrier_vec n" and d: "distinct ws" shows "lincomb f (set ws) = lincomb_list (\i. f (ws ! i)) ws" proof (insert assms, induct ws) case Nil then show ?case by auto next case (Cons a ws) have [simp]: "\v. v \ set ws \ v \ carrier_vec n" using Cons.prems(1) by auto then have ws: "set ws \ carrier_vec n" by auto have hyp: "lincomb f (set (ws)) = lincomb_list (\i. f (ws ! i)) ws" proof (intro Cons.hyps ws) show "distinct ws" using Cons.prems(2) by auto qed have "(map (\i. f (ws ! i) \\<^sub>v ws ! i) [0..v. f v \\<^sub>v v) ws)" by (intro nth_equalityI, auto) with ws have sumlist_rw: "sumlist (map (\i. f (ws ! i) \\<^sub>v ws ! i) [0..v. f v \\<^sub>v v) ws)" by (subst (1 2) sumlist_as_summset, auto) have "lincomb f (set (a # ws)) = (\\<^bsub>V\<^esub>v\set (a # ws). f v \\<^sub>v v)" unfolding lincomb_def .. also have "... = (\\<^bsub>V\<^esub>v\ insert a (set ws). f v \\<^sub>v v)" by simp also have "... = (f a \\<^sub>v a) + (\\<^bsub>V\<^esub>v\ (set ws). f v \\<^sub>v v)" by (rule finsum_insert, insert Cons.prems, auto) also have "... = f a \\<^sub>v a + lincomb_list (\i. f (ws ! i)) ws" using hyp lincomb_def by auto also have "... = f a \\<^sub>v a + sumlist (map (\v. f v \\<^sub>v v) ws)" unfolding lincomb_list_def sumlist_rw by auto also have "... = sumlist (map (\v. f v \\<^sub>v v) (a # ws))" proof - let ?a = "(map (\v. f v \\<^sub>v v) [a])" have a: "a \ carrier_vec n" using Cons.prems(1) by auto have "f a \\<^sub>v a = sumlist (map (\v. f v \\<^sub>v v) [a])" using Cons.prems(1) by auto hence "f a \\<^sub>v a + sumlist (map (\v. f v \\<^sub>v v) ws) = sumlist ?a + sumlist (map (\v. f v \\<^sub>v v) ws)" by simp also have "... = sumlist (?a @ (map (\v. f v \\<^sub>v v) ws))" by (rule sumlist_append[symmetric], auto simp add: a) finally show ?thesis by auto qed also have "... = sumlist (map (\i. f ((a # ws) ! i) \\<^sub>v (a # ws) ! i) [0..i. f ((a # ws) ! i) \\<^sub>v (a # ws) ! i) [0..v. f v \\<^sub>v v) (a # ws))" - proof (intro nth_equalityI, goal_cases) - case (2 i) thus ?case by (smt length_map map_nth nth_map) - qed auto + by (smt (verit, del_insts) length_map map_equality_iff map_nth nth_map) show ?thesis unfolding u .. qed also have "... = lincomb_list (\i. f ((a # ws) ! i)) (a # ws)" unfolding lincomb_list_def .. finally show ?case . qed end locale idom_vec = vec_module f_ty for f_ty :: "'a :: idom itself" begin lemma lin_dep_cols_imp_det_0': fixes ws defines "A \ mat_of_cols n ws" assumes dimv_ws: "\w\set ws. dim_vec w = n" assumes A: "A \ carrier_mat n n" and ld_cols: "lin_dep (set (cols A))" shows "det A = 0" proof (cases "distinct ws") case False obtain i j where ij: "i\j" and c: "col A i = col A j" and i: "ix. x \ set ws \ x \ carrier_vec n" using dimv_ws by auto obtain A' f' v where f'_in: "f' \ A' \ UNIV" and lc_f': "lincomb f' A' = 0\<^sub>v n" and f'_v: "f' v \ 0" and v_A': "v \ A'" and A'_in_rows: "A' \ set (cols A)" using ld_cols unfolding lin_dep_def by auto define f where "f \ \x. if x \ A' then 0 else f' x" have f_in: "f \ (set (cols A)) \ UNIV" using f'_in by auto have A'_in_carrier: "A' \ carrier_vec n" by (metis (no_types) A'_in_rows A_def cols_dim carrier_matD(1) mat_of_cols_carrier(1) subset_trans) have lc_f: "lincomb f (set (cols A)) = 0\<^sub>v n" proof - have l1: "lincomb f (set (cols A) - A') = 0\<^sub>v n" by (rule lincomb_zero, auto simp add: f_def, insert A cols_dim, blast) have l2: "lincomb f A' = 0\<^sub>v n " using lc_f' unfolding f_def using A'_in_carrier by auto have "lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'" proof (rule lincomb_vec_diff_add) show "set (cols A) \ carrier_vec n" using A cols_dim by blast show "A' \ set (cols A)" using A'_in_rows by blast qed auto also have "... = 0\<^sub>v n" using l1 l2 by auto finally show ?thesis . qed have v_in: "v \ (set (cols A))" using v_A' A'_in_rows by auto have fv: "f v \ 0" using f'_v v_A' unfolding f_def by auto let ?c = "(\i. f (ws ! i))" have "lincomb f (set ws) = lincomb_list ?c ws" by (rule lincomb_as_lincomb_list_distinct[OF _ True], auto) have "\v. v \ carrier_vec n \ v \ 0\<^sub>v n \ A *\<^sub>v v = 0\<^sub>v n" proof (rule exI[of _ " vec (length ws) ?c"], rule conjI) show "vec (length ws) ?c \ carrier_vec n" using A A_def by auto have vec_not0: "vec (length ws) ?c \ 0\<^sub>v n" proof - obtain i where ws_i: "(ws ! i) = v" and i: "i 0" using fv by simp finally show ?thesis using A A_def i by fastforce qed have "A *\<^sub>v vec (length ws) ?c = mat_of_cols n ws *\<^sub>v vec (length ws) ?c" unfolding A_def .. also have "... = lincomb_list ?c ws" by (rule lincomb_list_as_mat_mult[symmetric, OF dimv_ws]) also have "... = lincomb f (set ws)" by (rule lincomb_as_lincomb_list_distinct[symmetric, OF _ True], auto) also have "... = 0\<^sub>v n" using lc_f unfolding A_def using A by (simp add: subset_code(1)) finally show "vec (length ws) (\i. f (ws ! i)) \ 0\<^sub>v n \ A *\<^sub>v vec (length ws) (\i. f (ws ! i)) = 0\<^sub>v n" using vec_not0 by fast qed thus ?thesis unfolding det_0_iff_vec_prod_zero[OF A] . qed lemma lin_dep_cols_imp_det_0: assumes A: "A \ carrier_mat n n" and ld: "lin_dep (set (cols A))" shows "det A = 0" proof - have col_rw: "(cols (mat_of_cols n (cols A))) = cols A" using A by auto have m: "mat_of_cols n (cols A) = A" using A by auto show ?thesis by (rule A lin_dep_cols_imp_det_0'[of "cols A", unfolded col_rw, unfolded m, OF _ A ld]) (metis A cols_dim carrier_matD(1) subsetCE carrier_vecD) qed corollary lin_dep_rows_imp_det_0: assumes A: "A \ carrier_mat n n" and ld: "lin_dep (set (rows A))" shows "det A = 0" by (subst det_transpose[OF A, symmetric], rule lin_dep_cols_imp_det_0, auto simp add: ld A) lemma det_not_0_imp_lin_indpt_rows: assumes A: "A \ carrier_mat n n" and det: "det A \ 0" shows "lin_indpt (set (rows A))" using lin_dep_rows_imp_det_0[OF A] det by auto lemma upper_triangular_imp_lin_indpt_rows: assumes A: "A \ carrier_mat n n" and tri: "upper_triangular A" and diag: "0 \ set (diag_mat A)" shows "lin_indpt (set (rows A))" using det_not_0_imp_lin_indpt_rows upper_triangular_imp_det_eq_0_iff assms by auto (* Connection from set-based to list-based *) lemma lincomb_as_lincomb_list: fixes ws f assumes s: "set ws \ carrier_vec n" shows "lincomb f (set ws) = lincomb_list (\i. if \jv. v \ set ws \ v \ carrier_vec n" using snoc.prems(1) by auto then have ws: "set ws \ carrier_vec n" by auto have hyp: "lincomb f (set ws) = lincomb_list ?f ws" by (intro snoc.hyps ws) show ?case proof (cases "a\set ws") case True have g_length: "?g (length ws) = 0\<^sub>v n" using True by (auto, metis in_set_conv_nth nth_append) have "(map ?g [0..v n]" using g_length by simp finally have map_rw: "(map ?g [0..v n]" . have "M.sumlist (map ?g2 [0..v n " by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws) also have "... = M.sumlist (map ?g [0..v n])" by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append) finally have summlist_rw: "M.sumlist (map ?g2 [0..v n])" . have "lincomb f (set (ws @ [a])) = lincomb f (set ws)" using True unfolding lincomb_def by (simp add: insert_absorb) thus ?thesis unfolding hyp lincomb_list_def map_rw summlist_rw by auto next case False have g_length: "?g (length ws) = f a \\<^sub>v a" using False by (auto simp add: nth_append) have "(map ?g [0..\<^sub>v a)]" using g_length by simp finally have map_rw: "(map ?g [0..\<^sub>v a)]" . have summlist_rw: "M.sumlist (map ?g2 [0..\<^bsub>V\<^esub>v\set (a # ws). f v \\<^sub>v v)" unfolding lincomb_def .. also have "... = (\\<^bsub>V\<^esub>v\ insert a (set ws). f v \\<^sub>v v)" by simp also have "... = (f a \\<^sub>v a) + (\\<^bsub>V\<^esub>v\ (set ws). f v \\<^sub>v v)" proof (rule finsum_insert) show "finite (set ws)" by auto show "a \ set ws" using False by auto show "(\v. f v \\<^sub>v v) \ set ws \ carrier_vec n" using snoc.prems(1) by auto show "f a \\<^sub>v a \ carrier_vec n" using snoc.prems by auto qed also have "... = (f a \\<^sub>v a) + lincomb f (set ws)" unfolding lincomb_def .. also have "... = (f a \\<^sub>v a) + lincomb_list ?f ws" using hyp by auto also have "... = lincomb_list ?f ws + (f a \\<^sub>v a)" using M.add.m_comm lincomb_list_carrier snoc.prems by auto also have "... = lincomb_list (\i. if \j carrier_vec n" using snoc.prems by (auto simp add: nth_append) show "f a \\<^sub>v a \ carrier_vec n" using snoc.prems by auto qed finally show ?thesis . qed qed auto lemma span_list_as_span: assumes "set vs \ carrier_vec n" shows "span_list vs = span (set vs)" using assms proof (auto simp: span_list_def span_def) fix f show "\a A. lincomb_list f vs = lincomb a A \ finite A \ A \ set vs" using assms lincomb_list_as_lincomb by auto next fix f::"'a vec \'a" and A assume fA: "finite A" and A: "A \ set vs" have [simp]: "x \ carrier_vec n" if x: "x \ A" for x using A x assms by auto have [simp]: "v \ carrier_vec n" if v: "v \ set vs" for v using assms v by auto have set_vs_Un: "((set vs) - A) \ A = set vs" using A by auto let ?f = "(\x. if x\(set vs) - A then 0 else f x)" have f0: "(\\<^bsub>V\<^esub>v\(set vs) - A. ?f v \\<^sub>v v) = 0\<^sub>v n" by (rule M.finsum_all0, auto) have "lincomb f A = lincomb ?f A" by (auto simp add: lincomb_def intro!: finsum_cong2) also have "... = (\\<^bsub>V\<^esub>v\(set vs) - A. ?f v \\<^sub>v v) + (\\<^bsub>V\<^esub>v\A. ?f v \\<^sub>v v)" unfolding f0 lincomb_def by auto also have "... = lincomb ?f (((set vs) - A) \ A)" unfolding lincomb_def by (rule M.finsum_Un_disjoint[symmetric], auto simp add: fA) also have "... = lincomb ?f (set vs)" using set_vs_Un by auto finally have "lincomb f A = lincomb ?f (set vs)" . with lincomb_as_lincomb_list[OF assms] show "\c. lincomb f A = lincomb_list c vs" by auto qed lemma in_spanI[intro]: assumes "v = lincomb a A" "finite A" "A \ W" shows "v \ span W" unfolding span_def using assms by auto lemma in_spanE: assumes "v \ span W" shows "\ a A. v = lincomb a A \ finite A \ A \ W" using assms unfolding span_def by auto declare in_own_span[intro] lemma smult_in_span: assumes "W \ carrier_vec n" and insp: "x \ span W" shows "c \\<^sub>v x \ span W" proof - from in_spanE[OF insp] obtain a A where a: "x = lincomb a A" "finite A" "A \ W" by blast have "c \\<^sub>v x = lincomb (\ x. c * a x) A" using a(1) unfolding lincomb_def a apply(subst finsum_smult) using assms a by (auto simp:smult_smult_assoc) thus "c \\<^sub>v x \ span W" using a(2,3) by auto qed lemma span_subsetI: assumes ws: "ws \ carrier_vec n" "us \ span ws" shows "span us \ span ws" by (simp add: assms(1) span_is_submodule span_is_subset subsetI ws) end context vec_space begin sublocale idom_vec. lemma sumlist_in_span: assumes W: "W \ carrier_vec n" shows "(\x. x \ set xs \ x \ span W) \ sumlist xs \ span W" proof (induct xs) case Nil thus ?case using W by force next case (Cons x xs) from span_is_subset2[OF W] Cons(2) have xs: "x \ carrier_vec n" "set xs \ carrier_vec n" by auto from span_add1[OF W Cons(2)[of x] Cons(1)[OF Cons(2)]] have "x + sumlist xs \ span W" by auto also have "x + sumlist xs = sumlist ([x] @ xs)" by (subst sumlist_append, insert xs, auto) finally show ?case by simp qed lemma span_span[simp]: assumes "W \ carrier_vec n" shows "span (span W) = span W" proof(standard,standard,goal_cases) case (1 x) with in_spanE obtain a A where a: "x = lincomb a A" "finite A" "A \ span W" by blast from a(3) assms have AC:"A \ carrier_vec n" by auto show ?case unfolding a(1)[unfolded lincomb_def] proof(insert a(3),atomize (full),rule finite_induct[OF a(2)],goal_cases) case 1 then show ?case using span_zero by auto next case (2 x F) { assume F:"insert x F \ span W" hence "a x \\<^sub>v x \ span W" by (intro smult_in_span[OF assms],auto) hence "a x \\<^sub>v x + (\\<^bsub>V\<^esub>v\F. a v \\<^sub>v v) \ span W" using span_add1 F 2 assms by auto hence "(\\<^bsub>V\<^esub>v\insert x F. a v \\<^sub>v v) \ span W" apply(subst M.finsum_insert[OF 2(1,2)]) using F assms by auto } then show ?case by auto qed next case 2 show ?case using assms by(intro in_own_span, auto) qed lemma upper_triangular_imp_basis: assumes A: "A \ carrier_mat n n" and tri: "upper_triangular A" and diag: "0 \ set (diag_mat A)" shows "basis (set (rows A))" using upper_triangular_imp_distinct[OF assms] using upper_triangular_imp_lin_indpt_rows[OF assms] A by (auto intro: dim_li_is_basis simp: distinct_card dim_is_n set_rows_carrier) lemma fin_dim_span_rows: assumes A: "A \ carrier_mat nr n" shows "vectorspace.fin_dim class_ring (vs (span (set (rows A))))" proof (rule fin_dim_span) show "set (rows A) \ carrier V" using A rows_carrier[of A] unfolding carrier_mat_def by auto show "finite (set (rows A))" by auto qed definition "row_space B = span (set (rows B))" definition "col_space B = span (set (cols B))" lemma row_space_eq_col_space_transpose: shows "row_space A = col_space A\<^sup>T" unfolding col_space_def row_space_def cols_transpose .. lemma col_space_eq_row_space_transpose: shows "col_space A = row_space A\<^sup>T" unfolding col_space_def row_space_def Matrix.rows_transpose .. lemma col_space_eq: assumes A: "A \ carrier_mat n nc" shows "col_space A = {y\carrier_vec (dim_row A). \x\carrier_vec (dim_col A). A *\<^sub>v x = y}" proof - let ?ws = "cols A" have set_cols_in: "set (cols A) \ carrier_vec n" using A unfolding cols_def by auto have "lincomb f S \ carrier_vec (dim_row A)" if "finite S" and S: "S \ set (cols A)" for f S using lincomb_closed A by (metis (full_types) S carrier_matD(1) cols_dim lincomb_closed subsetCE subsetI) moreover have "\x\carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S" if fin_S: "finite S" and S: "S \ set (cols A)" for f S proof - let ?g = "(\v. if v \ S then f v else 0)" let ?g' = "(\i. if \j ?Z" using S by auto have inter: "S \ ?Z = {}" by auto have "lincomb f S = lincomb ?g S" by (rule lincomb_cong, insert set_cols_in A S, auto) also have "... = lincomb ?g (S \ ?Z)" by (rule lincomb_clean[symmetric],insert set_cols_in A S fin_S, auto) also have "... = lincomb ?g (set ?ws)" using union by auto also have "... = lincomb_list ?g' ?ws" by (rule lincomb_as_lincomb_list[OF set_cols_in]) also have "... = mat_of_cols n ?ws *\<^sub>v vec (length ?ws) ?g'" by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto) also have "... = A *\<^sub>v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto finally show ?thesis by auto qed moreover have "\f S. A *\<^sub>v x = lincomb f S \ finite S \ S \ set (cols A)" if Ax: "A *\<^sub>v x \ carrier_vec (dim_row A)" and x: "x \ carrier_vec (dim_col A)" for x proof - let ?c = "\i. x $ i" have x_vec: "vec (length ?ws) ?c = x" using x by auto have "A *\<^sub>v x = mat_of_cols n ?ws *\<^sub>v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto also have "... = lincomb_list ?c ?ws" by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto) also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)" by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto) finally show ?thesis by auto qed ultimately show ?thesis unfolding col_space_def span_def by auto qed lemma vector_space_row_space: assumes A: "A \ carrier_mat nr n" shows "vectorspace class_ring (vs (row_space A))" proof - have fin: "finite (set (rows A))" by auto have s: "set (rows A) \ carrier V" using A unfolding rows_def by auto have "span_vs (set (rows A)) = vs (span (set (rows A)))" by auto moreover have "vectorspace class_ring (span_vs (set (rows A)))" using fin s span_is_subspace subspace_def subspace_is_vs by simp ultimately show ?thesis unfolding row_space_def by auto qed lemma row_space_eq: assumes A: "A \ carrier_mat nr n" shows "row_space A = {w\carrier_vec (dim_col A). \y\carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}" using A col_space_eq unfolding row_space_eq_col_space_transpose by auto lemma row_space_is_preserved: assumes inv_P: "invertible_mat P" and P: "P \ carrier_mat m m" and A: "A \ carrier_mat m n" shows "row_space (P*A) = row_space A" proof - have At: "A\<^sup>T \ carrier_mat n m" using A by auto have Pt: "P\<^sup>T \ carrier_mat m m" using P by auto have PA: "P*A \ carrier_mat m n" using P A by auto have "w \ row_space A" if w: "w \ row_space (P*A)" for w proof - have w_carrier: "w \ carrier_vec (dim_col (P*A))" using w mult_carrier_mat[OF P A] row_space_eq by auto from that and this obtain y where y: "y \ carrier_vec (dim_row (P * A))" and w_By: "w = (P*A)\<^sup>T *\<^sub>v y" unfolding row_space_eq[OF PA] by blast have ym: "y \ carrier_vec m" using y Pt by auto have "w=((P*A)\<^sup>T) *\<^sub>v y" using w_By . also have "... = (A\<^sup>T * P\<^sup>T) *\<^sub>v y" using transpose_mult[OF P A] by auto also have "... = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)" by (rule assoc_mult_mat_vec[OF At Pt], insert Pt y, auto) finally show "w \ row_space A" unfolding row_space_eq[OF A] using At Pt ym by auto qed moreover have "w \ row_space (P*A)" if w: "w \ row_space A" for w proof - have w_carrier: "w \ carrier_vec (dim_col A)" using w A unfolding row_space_eq[OF A] by auto obtain P' where PP': "inverts_mat P P'" and P'P: "inverts_mat P' P" using inv_P P unfolding invertible_mat_def by blast have P': "P' \ carrier_mat m m" using PP' P'P P unfolding inverts_mat_def by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_one_mat(3)) from that obtain y where y: "y \ carrier_vec (dim_row A)" and w_Ay: "w = A\<^sup>T *\<^sub>v y" unfolding row_space_eq[OF A] by blast have Py: "(P'\<^sup>T *\<^sub>v y) \ carrier_vec m" using P' y A by auto have "w = A\<^sup>T *\<^sub>v y" using w_Ay . also have "... = ((P' * P)*A)\<^sup>T *\<^sub>v y" using P'P left_mult_one_mat A P' unfolding inverts_mat_def by auto also have "... = ((P' * (P*A))\<^sup>T) *\<^sub>v y" using assoc_mult_mat_vec P' P A by auto also have "... = ((P*A)\<^sup>T * P'\<^sup>T) *\<^sub>v y" using transpose_mult P A P' mult_carrier_mat by metis - also have "... = (P*A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)" - using assoc_mult_mat_vec A P P' y mult_carrier_mat - by (smt carrier_matD(1) transpose_carrier_mat) + also have "... = (P*A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)" using A P' PA y by auto finally show "w \ row_space (P*A)" unfolding row_space_eq[OF PA] using Py w_carrier A P by fastforce qed ultimately show ?thesis by auto qed end context vec_module begin lemma R_sumlist[simp]: "R.sumlist = sum_list" proof (intro ext) fix xs show "R.sumlist xs = sum_list xs" by (induct xs, auto) qed lemma sumlist_dim: assumes "\ x. x \ set xs \ x \ carrier_vec n" shows "dim_vec (sumlist xs) = n" using sumlist_carrier assms by fastforce lemma sumlist_vec_index: assumes "\ x. x \ set xs \ x \ carrier_vec n" and "i < n" shows "sumlist xs $ i = sum_list (map (\ x. x $ i) xs)" unfolding M.sumlist_def using assms(1) proof(induct xs) case (Cons a xs) hence cond:"\ x. x \ set xs \ x \ carrier_vec n" by auto from Cons(1)[OF cond] have IH:"foldr (+) xs (0\<^sub>v n) $ i = (\x\xs. x $ i)" by auto have "(a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\x\xs. x $ i)" apply(subst index_add_vec) unfolding IH using sumlist_dim[OF cond,unfolded M.sumlist_def] assms by auto then show ?case by auto next case Nil thus ?case using assms by auto qed lemma scalar_prod_left_sum_distrib: assumes vs: "\ v. v \ set vvs \ v \ carrier_vec n" and w: "w \ carrier_vec n" shows "sumlist vvs \ w = sum_list (map (\ v. v \ w) vvs)" using vs proof (induct vvs) case (Cons v vs) from Cons have v: "v \ carrier_vec n" and vs: "sumlist vs \ carrier_vec n" by (auto intro!: sumlist_carrier) have "sumlist (v # vs) \ w = sumlist ([v] @ vs) \ w " by auto also have "\ = (v + sumlist vs) \ w" by (subst sumlist_append, insert Cons v vs, auto) also have "\ = v \ w + (sumlist vs \ w)" by (rule add_scalar_prod_distrib[OF v vs w]) finally show ?case using Cons by auto qed (insert w, auto) lemma scalar_prod_right_sum_distrib: assumes vs: "\ v. v \ set vvs \ v \ carrier_vec n" and w: "w \ carrier_vec n" shows "w \ sumlist vvs = sum_list (map (\ v. w \ v) vvs)" by (subst comm_scalar_prod[OF w sumlist_carrier], insert vs w, force, subst scalar_prod_left_sum_distrib[OF vs w], force, rule arg_cong[of _ _ sum_list], rule nth_equalityI, auto simp: set_conv_nth intro!: comm_scalar_prod) lemma lincomb_list_add_vec_2: assumes us: "set us \ carrier_vec n" and x: "x = lincomb_list lc (us [i := us ! i + c \\<^sub>v us ! j])" and i: "j < length us" "i < length us" "i \ j" shows "x = lincomb_list (lc (j := lc j + lc i * c)) us" (is "_ = ?x") proof - let ?xx = "lc j + lc i * c" let ?i = "us ! i" let ?j = "us ! j" let ?v = "?i + c \\<^sub>v ?j" let ?ws = "us [i := us ! i + c \\<^sub>v us ! j]" from us have usk: "k < length us \ us ! k \ carrier_vec n" for k by auto from usk i have ij: "?i \ carrier_vec n" "?j \ carrier_vec n" by auto hence v: "c \\<^sub>v ?j \ carrier_vec n" "?v \ carrier_vec n" by auto with us have ws: "set ?ws \ carrier_vec n" unfolding set_conv_nth using i by (auto, rename_tac k, case_tac "k = i", auto) from us have us': "\w\set us. dim_vec w = n" by auto from ws have ws': "\w\set ?ws. dim_vec w = n" by auto have mset: "mset_set {0.. {0 ..< length us}", auto) define M2 where "M2 = M.summset {#lc ia \\<^sub>v ?ws ! ia. ia \# mset_set ({0..\<^sub>v us ! i. i \# mset_set ({0.. carrier_vec n" unfolding M1_def using usk by fastforce have M2: "M1 = M2" unfolding M2_def M1_def by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto) have x1: "x = lc j \\<^sub>v ?j + (lc i \\<^sub>v ?i + lc i \\<^sub>v (c \\<^sub>v ?j) + M1)" unfolding x lincomb_list_def M2 M2_def apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, simp add: mset smult_add_distrib_vec[OF ij(1) v(1)]) by (subst M.summset_add_mset, auto)+ have x2: "?x = ?xx \\<^sub>v ?j + (lc i \\<^sub>v ?i + M1)" unfolding x lincomb_list_def M1_def apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, simp add: mset smult_add_distrib_vec[OF ij(1) v(1)]) by (subst M.summset_add_mset, auto)+ show ?thesis unfolding x1 x2 using M1 ij by (intro eq_vecI, auto simp: field_simps) qed lemma lincomb_list_add_vec_1: assumes us: "set us \ carrier_vec n" and x: "x = lincomb_list lc us" and i: "j < length us" "i < length us" "i \ j" shows "x = lincomb_list (lc (j := lc j - lc i * c)) (us [i := us ! i + c \\<^sub>v us ! j])" (is "_ = ?x") proof - let ?i = "us ! i" let ?j = "us ! j" let ?v = "?i + c \\<^sub>v ?j" let ?ws = "us [i := us ! i + c \\<^sub>v us ! j]" from us have usk: "k < length us \ us ! k \ carrier_vec n" for k by auto from usk i have ij: "?i \ carrier_vec n" "?j \ carrier_vec n" by auto hence v: "c \\<^sub>v ?j \ carrier_vec n" "?v \ carrier_vec n" by auto with us have ws: "set ?ws \ carrier_vec n" unfolding set_conv_nth using i by (auto, rename_tac k, case_tac "k = i", auto) from us have us': "\w\set us. dim_vec w = n" by auto from ws have ws': "\w\set ?ws. dim_vec w = n" by auto have mset: "mset_set {0.. {0 ..< length us}", auto) define M2 where "M2 = M.summset {#(if ia = j then lc j - lc i * c else lc ia) \\<^sub>v ?ws ! ia . ia \# mset_set ({0..\<^sub>v us ! i. i \# mset_set ({0.. carrier_vec n" unfolding M1_def using usk by fastforce have M2: "M1 = M2" unfolding M2_def M1_def by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto) have x1: "x = lc j \\<^sub>v ?j + (lc i \\<^sub>v ?i + M1)" unfolding x lincomb_list_def M1_def apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, simp add: mset smult_add_distrib_vec[OF ij(1) v(1)]) by (subst M.summset_add_mset, auto)+ have x2: "?x = (lc j - lc i * c) \\<^sub>v ?j + (lc i \\<^sub>v ?i + lc i \\<^sub>v (c \\<^sub>v ?j) + M1)" unfolding x lincomb_list_def M2 M2_def apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk, simp add: mset smult_add_distrib_vec[OF ij(1) v(1)]) by (subst M.summset_add_mset, auto)+ show ?thesis unfolding x1 x2 using M1 ij by (intro eq_vecI, auto simp: field_simps) qed end context vec_space begin lemma add_vec_span: assumes us: "set us \ carrier_vec n" and i: "j < length us" "i < length us" "i \ j" shows "span (set us) = span (set (us [i := us ! i + c \\<^sub>v us ! j]))" (is "_ = span (set ?ws)") proof - let ?i = "us ! i" let ?j = "us ! j" let ?v = "?i + c \\<^sub>v ?j" from us i have ij: "?i \ carrier_vec n" "?j \ carrier_vec n" by auto hence v: "?v \ carrier_vec n" by auto with us have ws: "set ?ws \ carrier_vec n" unfolding set_conv_nth using i by (auto, rename_tac k, case_tac "k = i", auto) have "span (set us) = span_list us" unfolding span_list_as_span[OF us] .. also have "\ = span_list ?ws" proof - { fix x assume "x \ span_list us" then obtain lc where "x = lincomb_list lc us" by (metis in_span_listE) from lincomb_list_add_vec_1[OF us this i, of c] have "x \ span_list ?ws" unfolding span_list_def by auto } moreover { fix x assume "x \ span_list ?ws" then obtain lc where "x = lincomb_list lc ?ws" by (metis in_span_listE) from lincomb_list_add_vec_2[OF us this i] have "x \ span_list us" unfolding span_list_def by auto } ultimately show ?thesis by blast qed also have "\ = span (set ?ws)" unfolding span_list_as_span[OF ws] .. finally show ?thesis . qed lemma prod_in_span[intro!]: assumes "b \ carrier_vec n" "S \ carrier_vec n" "a = 0 \ b \ span S" shows "a \\<^sub>v b \ span S" proof(cases "a = 0") case True then show ?thesis by (auto simp:lmult_0[OF assms(1)] span_zero) next case False with assms have "b \ span S" by auto from this[THEN in_spanE] obtain aa A where a[intro!]: "b = lincomb aa A" "finite A" "A \ S" by auto hence [intro!]:"(\v. aa v \\<^sub>v v) \ A \ carrier_vec n" using assms by auto show ?thesis proof show "a \\<^sub>v b = lincomb (\ v. a * aa v) A" using a(1) unfolding lincomb_def smult_smult_assoc[symmetric] by(subst finsum_smult[symmetric]) force+ qed auto qed lemma det_nonzero_congruence: assumes eq:"A * M = B * M" and det:"det (M::'a mat) \ 0" and M: "M \ carrier_mat n n" and carr:"A \ carrier_mat n n" "B \ carrier_mat n n" shows "A = B" proof - have "1\<^sub>m n \ carrier_mat n n" by auto from det_non_zero_imp_unit[OF M det] gauss_jordan_check_invertable[OF M this] have gj_fst:"(fst (gauss_jordan M (1\<^sub>m n)) = 1\<^sub>m n)" by metis define Mi where "Mi = snd (gauss_jordan M (1\<^sub>m n))" with gj_fst have gj:"gauss_jordan M (1\<^sub>m n) = (1\<^sub>m n, Mi)" unfolding fst_def snd_def by (auto split:prod.split) from gauss_jordan_compute_inverse(1,3)[OF M gj] have Mi: "Mi \ carrier_mat n n" and is1:"M * Mi = 1\<^sub>m n" by metis+ from arg_cong[OF eq, of "\ M. M * Mi"] show "A = B" unfolding carr[THEN assoc_mult_mat[OF _ M Mi]] is1 carr[THEN right_mult_one_mat]. qed lemma mat_of_rows_mult_as_finsum: assumes "v \ carrier_vec (length lst)" "\ i. i < length lst \ lst ! i \ carrier_vec n" defines "f l \ sum (\ i. if l = lst ! i then v $ i else 0) {0..v v = lincomb f (set lst)" proof - from assms have "\ i < length lst. lst ! i \ carrier_vec n" by blast note an = all_nth_imp_all_set[OF this] hence slc:"set lst \ carrier_vec n" by auto hence dn [simp]:"\ x. x \ set lst \ dim_vec x = n" by auto have dl [simp]:"dim_vec (lincomb f (set lst)) = n" using an by (intro lincomb_dim,auto) show ?thesis proof show "dim_vec (mat_of_cols n lst *\<^sub>v v) = dim_vec (lincomb f (set lst))" using assms(1,2) by auto fix i assume i:"i < dim_vec (lincomb f (set lst))" hence i':"i < n" by auto with an have fcarr:"(\v. f v \\<^sub>v v) \ set lst \ carrier_vec n" by auto from i' have "(mat_of_cols n lst *\<^sub>v v) $ i = row (mat_of_cols n lst) i \ v" by auto also have "\ = (\ia = 0.. = (\ia = 0.. = (\x\set lst. f x * x $ i)" unfolding f_def sum_distrib_right apply (subst sum.swap) apply(rule sum.cong[OF refl]) unfolding if_distrib if_distribR mult_zero_left sum.delta[OF finite_set] by auto also have "\ = (\x\set lst. (f x \\<^sub>v x) $ i)" apply(rule sum.cong[OF refl],subst index_smult_vec) using i slc by auto also have "\ = (\\<^bsub>V\<^esub>v\set lst. f v \\<^sub>v v) $ i" unfolding finsum_index[OF i' fcarr slc] by auto finally show "(mat_of_cols n lst *\<^sub>v v) $ i = lincomb f (set lst) $ i" by (auto simp:lincomb_def) qed qed end end diff --git a/thys/Polynomial_Interpolation/Missing_Polynomial.thy b/thys/Polynomial_Interpolation/Missing_Polynomial.thy --- a/thys/Polynomial_Interpolation/Missing_Polynomial.thy +++ b/thys/Polynomial_Interpolation/Missing_Polynomial.thy @@ -1,1381 +1,1381 @@ (* Author: René Thiemann Akihisa Yamada Jose Divason License: BSD *) section \Missing Polynomial\ text \The theory contains some basic results on polynomials which have not been detected in the distribution, especially on linear factors and degrees.\ theory Missing_Polynomial imports "HOL-Computational_Algebra.Polynomial_Factorial" Missing_Unsorted begin subsection \Basic Properties\ lemma degree_0_id: assumes "degree p = 0" shows "[: coeff p 0 :] = p" proof - have "\ x. 0 \ Suc x" by auto thus ?thesis using assms by (metis coeff_pCons_0 degree_pCons_eq_if pCons_cases) qed lemma degree0_coeffs: "degree p = 0 \ \ a. p = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) lemma degree1_coeffs: "degree p = 1 \ \ a b. p = [: b, a :] \ a \ 0" by (metis One_nat_def degree_pCons_eq_if nat.inject old.nat.distinct(2) pCons_0_0 pCons_cases) lemma degree2_coeffs: "degree p = 2 \ \ a b c. p = [: c, b, a :] \ a \ 0" by (metis Suc_1 Suc_neq_Zero degree1_coeffs degree_pCons_eq_if nat.inject pCons_cases) lemma poly_zero: fixes p :: "'a :: comm_ring_1 poly" assumes x: "poly p x = 0" shows "p = 0 \ degree p = 0" proof assume degp: "degree p = 0" hence "poly p x = coeff p (degree p)" by(subst degree_0_id[OF degp,symmetric], simp) hence "coeff p (degree p) = 0" using x by auto thus "p = 0" by auto qed auto lemma coeff_monom_Suc: "coeff (monom a (Suc d) * p) (Suc i) = coeff (monom a d * p) i" by (simp add: monom_Suc) lemma coeff_sum_monom: assumes n: "n \ d" shows "coeff (\i\d. monom (f i) i) n = f n" (is "?l = _") proof - have "?l = (\i\d. coeff (monom (f i) i) n)" (is "_ = sum ?cmf _") using coeff_sum. also have "{..d} = insert n ({..d}-{n})" using n by auto hence "sum ?cmf {..d} = sum ?cmf ..." by auto also have "... = sum ?cmf ({..d}-{n}) + ?cmf n" by (subst sum.insert,auto) also have "sum ?cmf ({..d}-{n}) = 0" by (subst sum.neutral, auto) finally show ?thesis by simp qed lemma linear_poly_root: "(a :: 'a :: comm_ring_1) \ set as \ poly (\ a \ as. [: - a, 1:]) a = 0" proof (induct as) case (Cons b as) show ?case proof (cases "a = b") case False with Cons have "a \ set as" by auto from Cons(1)[OF this] show ?thesis by simp qed simp qed simp lemma degree_lcoeff_sum: assumes deg: "degree (f q) = n" and fin: "finite S" and q: "q \ S" and degle: "\ p . p \ S - {q} \ degree (f p) < n" and cong: "coeff (f q) n = c" shows "degree (sum f S) = n \ coeff (sum f S) n = c" proof (cases "S = {q}") case True thus ?thesis using deg cong by simp next case False with q obtain p where "p \ S - {q}" by auto from degle[OF this] have n: "n > 0" by auto have "degree (sum f S) = degree (f q + sum f (S - {q}))" unfolding sum.remove[OF fin q] .. also have "\ = degree (f q)" proof (rule degree_add_eq_left) have "degree (sum f (S - {q})) \ n - 1" proof (rule degree_sum_le) fix p show "p \ S - {q} \ degree (f p) \ n - 1" using degle[of p] by auto qed (insert fin, auto) also have "\ < n" using n by simp finally show "degree (sum f (S - {q})) < degree (f q)" unfolding deg . qed finally show ?thesis unfolding deg[symmetric] cong[symmetric] proof (rule conjI) have id: "(\x\S - {q}. coeff (f x) (degree (f q))) = 0" by (rule sum.neutral, rule ballI, rule coeff_eq_0[OF degle[folded deg]]) show "coeff (sum f S) (degree (f q)) = coeff (f q) (degree (f q))" unfolding coeff_sum by (subst sum.remove[OF _ q], unfold id, insert fin, auto) qed qed lemma degree_sum_list_le: "(\ p . p \ set ps \ degree p \ n) \ degree (sum_list ps) \ n" proof (induct ps) case (Cons p ps) hence "degree (sum_list ps) \ n" "degree p \ n" by auto thus ?case unfolding sum_list.Cons by (metis degree_add_le) qed simp lemma degree_prod_list_le: "degree (prod_list ps) \ sum_list (map degree ps)" proof (induct ps) case (Cons p ps) show ?case unfolding prod_list.Cons by (rule order.trans[OF degree_mult_le], insert Cons, auto) qed simp lemma smult_sum: "smult (\i \ S. f i) p = (\i \ S. smult (f i) p)" by (induct S rule: infinite_finite_induct, auto simp: smult_add_left) lemma range_coeff: "range (coeff p) = insert 0 (set (coeffs p))" by (metis nth_default_coeffs_eq range_nth_default) lemma smult_power: "(smult a p) ^ n = smult (a ^ n) (p ^ n)" by (induct n, auto simp: field_simps) lemma poly_sum_list: "poly (sum_list ps) x = sum_list (map (\ p. poly p x) ps)" by (induct ps, auto) lemma poly_prod_list: "poly (prod_list ps) x = prod_list (map (\ p. poly p x) ps)" by (induct ps, auto) lemma sum_list_neutral: "(\ x. x \ set xs \ x = 0) \ sum_list xs = 0" by (induct xs, auto) lemma prod_list_neutral: "(\ x. x \ set xs \ x = 1) \ prod_list xs = 1" by (induct xs, auto) lemma (in comm_monoid_mult) prod_list_map_remove1: "x \ set xs \ prod_list (map f xs) = f x * prod_list (map f (remove1 x xs))" by (induct xs) (auto simp add: ac_simps) lemma poly_as_sum: fixes p :: "'a::comm_semiring_1 poly" shows "poly p x = (\i\degree p. x ^ i * coeff p i)" unfolding poly_altdef by (simp add: ac_simps) lemma poly_prod_0: "finite ps \ poly (prod f ps) x = (0 :: 'a :: field) \ (\ p \ ps. poly (f p) x = 0)" by (induct ps rule: finite_induct, auto) lemma coeff_monom_mult: shows "coeff (monom a d * p) i = (if d \ i then a * coeff p (i-d) else 0)" (is "?l = ?r") proof (cases "d \ i") case False thus ?thesis unfolding coeff_mult by simp next case True let ?f = "\j. coeff (monom a d) j * coeff p (i - j)" have "\j. j \ {0..i} - {d} \ ?f j = 0" by auto hence "0 = (\j \ {0..i} - {d}. ?f j)" by auto also have "... + ?f d = (\j \ insert d ({0..i} - {d}). ?f j)" by(subst sum.insert, auto) also have "... = (\j \ {0..i}. ?f j)" by (subst insert_Diff, insert True, auto) also have "... = (\j\i. ?f j)" by (rule sum.cong, auto) also have "... = ?l" unfolding coeff_mult .. finally show ?thesis using True by auto qed lemma poly_eqI2: assumes "degree p = degree q" and "\i. i \ degree p \ coeff p i = coeff q i" shows "p = q" apply(rule poly_eqI) by (metis assms le_degree) text \A nice extension rule for polynomials.\ lemma poly_ext[intro]: fixes p q :: "'a :: {ring_char_0, idom} poly" assumes "\x. poly p x = poly q x" shows "p = q" unfolding poly_eq_poly_eq_iff[symmetric] using assms by (rule ext) text \Copied from non-negative variants.\ lemma coeff_linear_power_neg[simp]: fixes a :: "'a::comm_ring_1" shows "coeff ([:a, -1:] ^ n) n = (-1)^n" apply (induct n, simp_all) apply (subst coeff_eq_0) apply (auto intro: le_less_trans degree_power_le) done lemma degree_linear_power_neg[simp]: fixes a :: "'a::{idom,comm_ring_1}" shows "degree ([:a, -1:] ^ n) = n" apply (rule order_antisym) apply (rule ord_le_eq_trans [OF degree_power_le], simp) apply (rule le_degree) unfolding coeff_linear_power_neg apply (auto) done subsection \Polynomial Composition\ lemmas [simp] = pcompose_pCons lemma pcompose_eq_0: fixes q :: "'a :: idom poly" assumes q: "degree q \ 0" shows "p \\<^sub>p q = 0 \ p = 0" proof (induct p) case 0 show ?case by auto next case (pCons a p) have id: "(pCons a p) \\<^sub>p q = [:a:] + q * (p \\<^sub>p q)" by simp show ?case proof (cases "p = 0") case True show ?thesis unfolding id unfolding True by simp next case False with pCons(2) have "p \\<^sub>p q \ 0" by auto from degree_mult_eq[OF _ this, of q] q have "degree (q * (p \\<^sub>p q)) \ 0" by force hence deg: "degree ([:a:] + q * (p \\<^sub>p q)) \ 0" by (subst degree_add_eq_right, auto) show ?thesis unfolding id using False deg by auto qed qed declare degree_pcompose[simp] subsection \Monic Polynomials\ abbreviation monic where "monic p \ coeff p (degree p) = 1" lemma unit_factor_field [simp]: "unit_factor (x :: 'a :: {field,normalization_semidom}) = x" by (cases "is_unit x") (auto simp: is_unit_unit_factor dvd_field_iff) lemma poly_gcd_monic: fixes p :: "'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes "p \ 0 \ q \ 0" shows "monic (gcd p q)" proof - from assms have "1 = unit_factor (gcd p q)" by (auto simp: unit_factor_gcd) also have "\ = [:lead_coeff (gcd p q):]" unfolding unit_factor_poly_def by (simp add: monom_0) finally show ?thesis by (metis coeff_pCons_0 degree_1 lead_coeff_1) qed lemma normalize_monic: "monic p \ normalize p = p" by (simp add: normalize_poly_eq_map_poly is_unit_unit_factor) lemma lcoeff_monic_mult: assumes monic: "monic (p :: 'a :: comm_semiring_1 poly)" shows "coeff (p * q) (degree p + degree q) = coeff q (degree q)" proof - let ?pqi = "\ i. coeff p i * coeff q (degree p + degree q - i)" have "coeff (p * q) (degree p + degree q) = (\i\degree p + degree q. ?pqi i)" unfolding coeff_mult by simp also have "\ = ?pqi (degree p) + (sum ?pqi ({.. degree p + degree q} - {degree p}))" by (subst sum.remove[of _ "degree p"], auto) also have "?pqi (degree p) = coeff q (degree q)" unfolding monic by simp also have "(sum ?pqi ({.. degree p + degree q} - {degree p})) = 0" proof (rule sum.neutral, intro ballI) fix d assume d: "d \ {.. degree p + degree q} - {degree p}" show "?pqi d = 0" proof (cases "d < degree p") case True hence "degree p + degree q - d > degree q" by auto hence "coeff q (degree p + degree q - d) = 0" by (rule coeff_eq_0) thus ?thesis by simp next case False with d have "d > degree p" by auto hence "coeff p d = 0" by (rule coeff_eq_0) thus ?thesis by simp qed qed finally show ?thesis by simp qed lemma degree_monic_mult: assumes monic: "monic (p :: 'a :: comm_semiring_1 poly)" and q: "q \ 0" shows "degree (p * q) = degree p + degree q" proof - have "degree p + degree q \ degree (p * q)" by (rule degree_mult_le) also have "degree p + degree q \ degree (p * q)" proof - from q have cq: "coeff q (degree q) \ 0" by auto hence "coeff (p * q) (degree p + degree q) \ 0" unfolding lcoeff_monic_mult[OF monic] . thus "degree (p * q) \ degree p + degree q" by (rule le_degree) qed finally show ?thesis . qed lemma degree_prod_sum_monic: assumes S: "finite S" and nzd: "0 \ (degree o f) ` S" and monic: "(\ a . a \ S \ monic (f a))" shows "degree (prod f S) = (sum (degree o f) S) \ coeff (prod f S) (sum (degree o f) S) = 1" proof - from S nzd monic have "degree (prod f S) = sum (degree \ f) S \ (S \ {} \ degree (prod f S) \ 0 \ prod f S \ 0) \ coeff (prod f S) (sum (degree o f) S) = 1" proof (induct S rule: finite_induct) case (insert a S) have IH1: "degree (prod f S) = sum (degree o f) S" using insert by auto have IH2: "coeff (prod f S) (degree (prod f S)) = 1" using insert by auto have id: "degree (prod f (insert a S)) = sum (degree \ f) (insert a S) \ coeff (prod f (insert a S)) (sum (degree o f) (insert a S)) = 1" proof (cases "S = {}") case False with insert have nz: "prod f S \ 0" by auto from insert have monic: "coeff (f a) (degree (f a)) = 1" by auto have id: "(degree \ f) a = degree (f a)" by simp show ?thesis unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] id unfolding degree_monic_mult[OF monic nz] unfolding IH1[symmetric] unfolding lcoeff_monic_mult[OF monic] IH2 by simp qed (insert insert, auto) show ?case using id unfolding sum.insert[OF insert(1-2)] using insert by auto qed simp thus ?thesis by auto qed lemma degree_prod_monic: assumes "\ i. i < n \ degree (f i :: 'a :: comm_semiring_1 poly) = 1" and "\ i. i < n \ coeff (f i) 1 = 1" shows "degree (prod f {0 ..< n}) = n \ coeff (prod f {0 ..< n}) n = 1" proof - from degree_prod_sum_monic[of "{0 ..< n}" f] show ?thesis using assms by force qed lemma degree_prod_sum_lt_n: assumes "\ i. i < n \ degree (f i :: 'a :: comm_semiring_1 poly) \ 1" and i: "i < n" and fi: "degree (f i) = 0" shows "degree (prod f {0 ..< n}) < n" proof - have "degree (prod f {0 ..< n}) \ sum (degree o f) {0 ..< n}" by (rule degree_prod_sum_le, auto) also have "sum (degree o f) {0 ..< n} = (degree o f) i + sum (degree o f) ({0 ..< n} - {i})" by (rule sum.remove, insert i, auto) also have "(degree o f) i = 0" using fi by simp also have "sum (degree o f) ({0 ..< n} - {i}) \ sum (\ _. 1) ({0 ..< n} - {i})" by (rule sum_mono, insert assms, auto) also have "\ = n - 1" using i by simp also have "\ < n" using i by simp finally show ?thesis by simp qed lemma degree_linear_factors: "degree (\ a \ as. [: f a, 1:]) = length as" proof (induct as) case (Cons b as) note IH = this have id: "(\a\b # as. [:f a, 1:]) = [:f b,1 :] * (\a\as. [:f a, 1:])" by simp show ?case unfolding id by (subst degree_monic_mult, insert IH, auto) qed simp lemma monic_mult: fixes p q :: "'a :: idom poly" assumes "monic p" "monic q" shows "monic (p * q)" proof - from assms have nz: "p \ 0" "q \ 0" by auto show ?thesis unfolding degree_mult_eq[OF nz] coeff_mult_degree_sum using assms by simp qed lemma monic_factor: fixes p q :: "'a :: idom poly" assumes "monic (p * q)" "monic p" shows "monic q" proof - from assms have nz: "p \ 0" "q \ 0" by auto from assms[unfolded degree_mult_eq[OF nz] coeff_mult_degree_sum \monic p\] show ?thesis by simp qed lemma monic_prod: fixes f :: "'a \ 'b :: idom poly" assumes "\ a. a \ as \ monic (f a)" shows "monic (prod f as)" using assms proof (induct as rule: infinite_finite_induct) case (insert a as) hence id: "prod f (insert a as) = f a * prod f as" and *: "monic (f a)" "monic (prod f as)" by auto show ?case unfolding id by (rule monic_mult[OF *]) qed auto lemma monic_prod_list: fixes as :: "'a :: idom poly list" assumes "\ a. a \ set as \ monic a" shows "monic (prod_list as)" using assms by (induct as, auto intro: monic_mult) lemma monic_power: assumes "monic (p :: 'a :: idom poly)" shows "monic (p ^ n)" by (induct n, insert assms, auto intro: monic_mult) lemma monic_prod_list_pow: "monic (\(x::'a::idom, i)\xis. [:- x, 1:] ^ Suc i)" proof (rule monic_prod_list, goal_cases) case (1 a) then obtain x i where a: "a = [:-x, 1:]^Suc i" by force show "monic a" unfolding a by (rule monic_power, auto) qed lemma monic_degree_0: "monic p \ (degree p = 0) = (p = 1)" using le_degree poly_eq_iff by force subsection \Roots\ text \The following proof structure is completely similar to the one of @{thm poly_roots_finite}.\ lemma poly_roots_degree: fixes p :: "'a::idom poly" shows "p \ 0 \ card {x. poly p x = 0} \ degree p" proof (induct n \ "degree p" arbitrary: p) case (0 p) then obtain a where "a \ 0" and "p = [:a:]" by (cases p, simp split: if_splits) then show ?case by simp next case (Suc n p) show ?case proof (cases "\x. poly p x = 0") case True then obtain a where a: "poly p a = 0" .. then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) then obtain k where k: "p = [:-a, 1:] * k" .. with \p \ 0\ have "k \ 0" by auto with k have "degree p = Suc (degree k)" by (simp add: degree_mult_eq del: mult_pCons_left) with \Suc n = degree p\ have "n = degree k" by simp from Suc.hyps(1)[OF this \k \ 0\] have le: "card {x. poly k x = 0} \ degree k" . have "card {x. poly p x = 0} = card {x. poly ([:-a, 1:] * k) x = 0}" unfolding k .. also have "{x. poly ([:-a, 1:] * k) x = 0} = insert a {x. poly k x = 0}" by auto also have "card \ \ Suc (card {x. poly k x = 0})" unfolding card_insert_if[OF poly_roots_finite[OF \k \ 0\]] by simp also have "\ \ Suc (degree k)" using le by auto finally show ?thesis using \degree p = Suc (degree k)\ by simp qed simp qed lemma poly_root_factor: "(poly ([: r, 1:] * q) (k :: 'a :: idom) = 0) = (k = -r \ poly q k = 0)" (is ?one) "(poly (q * [: r, 1:]) k = 0) = (k = -r \ poly q k = 0)" (is ?two) "(poly [: r, 1 :] k = 0) = (k = -r)" (is ?three) proof - have [simp]: "r + k = 0 \ k = - r" by (simp add: minus_unique) show ?one unfolding poly_mult by auto show ?two unfolding poly_mult by auto show ?three by auto qed lemma poly_root_constant: "c \ 0 \ (poly (p * [:c:]) (k :: 'a :: idom) = 0) = (poly p k = 0)" unfolding poly_mult by auto lemma poly_linear_exp_linear_factors_rev: "([:b,1:])^(length (filter ((=) b) as)) dvd (\ (a :: 'a :: comm_ring_1) \ as. [: a, 1:])" proof (induct as) case (Cons a as) let ?ls = "length (filter ((=) b) (a # as))" let ?l = "length (filter ((=) b) as)" have prod: "(\ a \ Cons a as. [: a, 1:]) = [: a, 1 :] * (\ a \ as. [: a, 1:])" by simp show ?case proof (cases "a = b") case False hence len: "?ls = ?l" by simp show ?thesis unfolding prod len using Cons by (rule dvd_mult) next case True hence len: "[: b, 1 :] ^ ?ls = [: a, 1 :] * [: b, 1 :] ^ ?l" by simp show ?thesis unfolding prod len using Cons using dvd_refl mult_dvd_mono by blast qed qed simp lemma order_max: assumes dvd: "[: -a, 1 :] ^ k dvd p" and p: "p \ 0" shows "k \ order a p" proof (rule ccontr) assume "\ ?thesis" hence "\ j. k = Suc (order a p + j)" by arith then obtain j where k: "k = Suc (order a p + j)" by auto have "[: -a, 1 :] ^ Suc (order a p) dvd p" by (rule power_le_dvd[OF dvd[unfolded k]], simp) with order_2[OF p, of a] show False by blast qed subsection \Divisibility\ context assumes "SORT_CONSTRAINT('a :: idom)" begin lemma poly_linear_linear_factor: assumes dvd: "[:b,1:] dvd (\ (a :: 'a) \ as. [: a, 1:])" shows "b \ set as" proof - let ?p = "\ as. (\ a \ as. [: a, 1:])" let ?b = "[:b,1:]" from assms[unfolded dvd_def] obtain p where id: "?p as = ?b * p" .. from arg_cong[OF id, of "\ p. poly p (-b)"] have "poly (?p as) (-b) = 0" by simp thus ?thesis proof (induct as) case (Cons a as) have "?p (a # as) = [:a,1:] * ?p as" by simp from Cons(2)[unfolded this] have "poly (?p as) (-b) = 0 \ (a - b) = 0" by simp with Cons(1) show ?case by auto qed simp qed lemma poly_linear_exp_linear_factors: assumes dvd: "([:b,1:])^n dvd (\ (a :: 'a) \ as. [: a, 1:])" shows "length (filter ((=) b) as) \ n" proof - let ?p = "\ as. (\ a \ as. [: a, 1:])" let ?b = "[:b,1:]" from dvd show ?thesis proof (induct n arbitrary: as) case (Suc n as) have bs: "?b ^ Suc n = ?b * ?b ^ n" by simp from poly_linear_linear_factor[OF dvd_mult_left[OF Suc(2)[unfolded bs]], unfolded in_set_conv_decomp] obtain as1 as2 where as: "as = as1 @ b # as2" by auto have "?p as = [:b,1:] * ?p (as1 @ as2)" unfolding as proof (induct as1) case (Cons a as1) have "?p (a # as1 @ b # as2) = [:a,1:] * ?p (as1 @ b # as2)" by simp also have "?p (as1 @ b # as2) = [:b,1:] * ?p (as1 @ as2)" unfolding Cons by simp also have "[:a,1:] * \ = [:b,1:] * ([:a,1:] * ?p (as1 @ as2))" by (metis (no_types, lifting) mult.left_commute) finally show ?case by simp qed simp from Suc(2)[unfolded bs this dvd_mult_cancel_left] have "?b ^ n dvd ?p (as1 @ as2)" by simp from Suc(1)[OF this] show ?case unfolding as by simp qed simp qed end lemma const_poly_dvd: "([:a:] dvd [:b:]) = (a dvd b)" proof assume "a dvd b" then obtain c where "b = a * c" unfolding dvd_def by auto hence "[:b:] = [:a:] * [: c:]" by (auto simp: ac_simps) thus "[:a:] dvd [:b:]" unfolding dvd_def by blast next assume "[:a:] dvd [:b:]" then obtain pc where "[:b:] = [:a:] * pc" unfolding dvd_def by blast from arg_cong[OF this, of "\ p. coeff p 0", unfolded coeff_mult] have "b = a * coeff pc 0" by auto thus "a dvd b" unfolding dvd_def by blast qed lemma const_poly_dvd_1 [simp]: "[:a:] dvd 1 \ a dvd 1" by (metis const_poly_dvd one_poly_eq_simps(2)) lemma poly_dvd_1: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" shows "p dvd 1 \ degree p = 0 \ coeff p 0 dvd 1" proof (cases "degree p = 0") case False with divides_degree[of p 1] show ?thesis by auto next case True from degree0_coeffs[OF this] obtain a where p: "p = [:a:]" by auto show ?thesis unfolding p by auto qed text \Degree based version of irreducibility.\ definition irreducible\<^sub>d :: "'a :: comm_semiring_1 poly \ bool" where "irreducible\<^sub>d p = (degree p > 0 \ (\ q r. degree q < degree p \ degree r < degree p \ p \ q * r))" lemma irreducible\<^sub>dI [intro]: assumes 1: "degree p > 0" and 2: "\q r. degree q > 0 \ degree q < degree p \ degree r > 0 \ degree r < degree p \ p = q * r \ False" shows "irreducible\<^sub>d p" proof (unfold irreducible\<^sub>d_def, intro conjI allI impI notI 1) fix q r assume "degree q < degree p" and "degree r < degree p" and "p = q * r" with degree_mult_le[of q r] show False by (intro 2, auto) qed lemma irreducible\<^sub>dI2: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes deg: "degree p > 0" and ndvd: "\ q. degree q > 0 \ degree q \ degree p div 2 \ \ q dvd p" shows "irreducible\<^sub>d p" proof (rule ccontr) assume "\ ?thesis" from this[unfolded irreducible\<^sub>d_def] deg obtain q r where dq: "degree q < degree p" and dr: "degree r < degree p" and p: "p = q * r" by auto from deg have p0: "p \ 0" by auto with p have "q \ 0" "r \ 0" by auto from degree_mult_eq[OF this] p have dp: "degree p = degree q + degree r" by simp show False proof (cases "degree q \ degree p div 2") case True from ndvd[OF _ True] dq dr dp p show False by auto next case False with dp have dr: "degree r \ degree p div 2" by auto from p have dvd: "r dvd p" by auto from ndvd[OF _ dr] dvd dp dq show False by auto qed qed lemma reducible\<^sub>dI: assumes "degree p > 0 \ \q r. degree q < degree p \ degree r < degree p \ p = q * r" shows "\ irreducible\<^sub>d p" using assms by (auto simp: irreducible\<^sub>d_def) lemma irreducible\<^sub>dE [elim]: assumes "irreducible\<^sub>d p" and "degree p > 0 \ (\q r. degree q < degree p \ degree r < degree p \ p \ q * r) \ thesis" shows thesis using assms by (auto simp: irreducible\<^sub>d_def) lemma reducible\<^sub>dE [elim]: assumes red: "\ irreducible\<^sub>d p" and 1: "degree p = 0 \ thesis" and 2: "\q r. degree q > 0 \ degree q < degree p \ degree r > 0 \ degree r < degree p \ p = q * r \ thesis" shows thesis using red[unfolded irreducible\<^sub>d_def de_Morgan_conj not_not not_all not_imp] proof (elim disjE exE conjE) show "\degree p > 0 \ thesis" using 1 by auto next fix q r assume "degree q < degree p" and "degree r < degree p" and "p = q * r" with degree_mult_le[of q r] show thesis by (intro 2, auto) qed lemma irreducible\<^sub>dD: assumes "irreducible\<^sub>d p" shows "degree p > 0" "\q r. degree q < degree p \ degree r < degree p \ p \ q * r" using assms unfolding irreducible\<^sub>d_def by auto theorem irreducible\<^sub>d_factorization_exists: assumes "degree p > 0" shows "\fs. fs \ [] \ (\f \ set fs. irreducible\<^sub>d f \ degree f \ degree p) \ p = prod_list fs" and "\irreducible\<^sub>d p \ \fs. length fs > 1 \ (\f \ set fs. irreducible\<^sub>d f \ degree f < degree p) \ p = prod_list fs" proof (atomize(full), insert assms, induct "degree p" arbitrary:p rule: less_induct) case less then have deg_f: "degree p > 0" by auto show ?case proof (cases "irreducible\<^sub>d p") case True then have "set [p] \ Collect irreducible\<^sub>d" "p = prod_list [p]" by auto with True show ?thesis by (auto intro: exI[of _ "[p]"]) next case False with deg_f obtain g h where deg_g: "degree g < degree p" "degree g > 0" and deg_h: "degree h < degree p" "degree h > 0" and f_gh: "p = g * h" by auto from less.hyps[OF deg_g] less.hyps[OF deg_h] obtain gs hs where emp: "length gs > 0" "length hs > 0" and "\f \ set gs. irreducible\<^sub>d f \ degree f \ degree g" "g = prod_list gs" and "\f \ set hs. irreducible\<^sub>d f \ degree f \ degree h" "h = prod_list hs" by auto with f_gh deg_g deg_h have len: "length (gs@hs) > 1" and mem: "\f \ set (gs@hs). irreducible\<^sub>d f \ degree f < degree p" and p: "p = prod_list (gs@hs)" by (auto simp del: length_greater_0_conv) with False show ?thesis by (auto intro!: exI[of _ "gs@hs"] simp: less_imp_le) qed qed lemma irreducible\<^sub>d_factor: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "degree p > 0" shows "\ q r. irreducible\<^sub>d q \ p = q * r \ degree r < degree p" using assms proof (induct "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "irreducible\<^sub>d p") case False with less(2) obtain q r where q: "degree q < degree p" "degree q > 0" and r: "degree r < degree p" "degree r > 0" and p: "p = q * r" by auto from less(1)[OF q] obtain s t where IH: "irreducible\<^sub>d s" "q = s * t" by auto from p have p: "p = s * (t * r)" unfolding IH by (simp add: ac_simps) from less(2) have "p \ 0" by auto hence "degree p = degree s + (degree (t * r))" unfolding p by (subst degree_mult_eq, insert p, auto) with irreducible\<^sub>dD[OF IH(1)] have "degree p > degree (t * r)" by auto with p IH show ?thesis by auto next case True show ?thesis by (rule exI[of _ p], rule exI[of _ 1], insert True less(2), auto) qed qed context mult_zero begin (* least class with times and zero *) definition zero_divisor where "zero_divisor a \ \b. b \ 0 \ a * b = 0" lemma zero_divisorI[intro]: assumes "b \ 0" and "a * b = 0" shows "zero_divisor a" using assms by (auto simp: zero_divisor_def) lemma zero_divisorE[elim]: assumes "zero_divisor a" and "\b. b \ 0 \ a * b = 0 \ thesis" shows thesis using assms by (auto simp: zero_divisor_def) end lemma zero_divisor_0[simp]: "zero_divisor (0::'a::{mult_zero,zero_neq_one})" (* No need for one! *) by (auto intro!: zero_divisorI[of 1]) lemma not_zero_divisor_1: "\ zero_divisor (1 :: 'a :: {monoid_mult,mult_zero})" (* No need for associativity! *) by auto lemma zero_divisor_iff_eq_0[simp]: fixes a :: "'a :: {semiring_no_zero_divisors, zero_neq_one}" shows "zero_divisor a \ a = 0" by auto lemma mult_eq_0_not_zero_divisor_left[simp]: fixes a b :: "'a :: mult_zero" assumes "\ zero_divisor a" shows "a * b = 0 \ b = 0" using assms unfolding zero_divisor_def by force lemma mult_eq_0_not_zero_divisor_right[simp]: fixes a b :: "'a :: {ab_semigroup_mult,mult_zero}" (* No need for associativity! *) assumes "\ zero_divisor b" shows "a * b = 0 \ a = 0" using assms unfolding zero_divisor_def by (force simp: ac_simps) lemma degree_smult_not_zero_divisor_left[simp]: assumes "\ zero_divisor c" shows "degree (smult c p) = degree p" proof(cases "p = 0") case False then have "coeff (smult c p) (degree p) \ 0" using assms by auto from le_degree[OF this] degree_smult_le[of c p] show ?thesis by auto qed auto lemma degree_smult_not_zero_divisor_right[simp]: assumes "\ zero_divisor (lead_coeff p)" shows "degree (smult c p) = (if c = 0 then 0 else degree p)" proof(cases "c = 0") case False then have "coeff (smult c p) (degree p) \ 0" using assms by auto from le_degree[OF this] degree_smult_le[of c p] show ?thesis by auto qed auto lemma irreducible\<^sub>d_smult_not_zero_divisor_left: assumes c0: "\ zero_divisor c" assumes L: "irreducible\<^sub>d (smult c p)" shows "irreducible\<^sub>d p" proof (intro irreducible\<^sub>dI) from L have "degree (smult c p) > 0" by auto also note degree_smult_le finally show "degree p > 0" by auto fix q r assume deg_q: "degree q < degree p" and deg_r: "degree r < degree p" and p_qr: "p = q * r" then have 1: "smult c p = smult c q * r" by auto note degree_smult_le[of c q] also note deg_q finally have 2: "degree (smult c q) < degree (smult c p)" using c0 by auto from deg_r have 3: "degree r < \" using c0 by auto from irreducible\<^sub>dD(2)[OF L 2 3] 1 show False by auto qed lemmas irreducible\<^sub>d_smultI = irreducible\<^sub>d_smult_not_zero_divisor_left [where 'a = "'a :: {comm_semiring_1,semiring_no_zero_divisors}", simplified] lemma irreducible\<^sub>d_smult_not_zero_divisor_right: assumes p0: "\ zero_divisor (lead_coeff p)" and L: "irreducible\<^sub>d (smult c p)" shows "irreducible\<^sub>d p" proof- from L have "c \ 0" by auto with p0 have [simp]: "degree (smult c p) = degree p" by simp show "irreducible\<^sub>d p" proof (intro iffI irreducible\<^sub>dI conjI) from L show "degree p > 0" by auto fix q r assume deg_q: "degree q < degree p" and deg_r: "degree r < degree p" and p_qr: "p = q * r" then have 1: "smult c p = smult c q * r" by auto note degree_smult_le[of c q] also note deg_q finally have 2: "degree (smult c q) < degree (smult c p)" by simp from deg_r have 3: "degree r < \" by simp from irreducible\<^sub>dD(2)[OF L 2 3] 1 show False by auto qed qed lemma zero_divisor_mult_left: fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}" assumes "zero_divisor a" shows "zero_divisor (a * b)" proof- from assms obtain c where c0: "c \ 0" and [simp]: "a * c = 0" by auto have "a * b * c = a * c * b" by (simp only: ac_simps) with c0 show ?thesis by auto qed lemma zero_divisor_mult_right: fixes a b :: "'a :: {semigroup_mult, mult_zero}" assumes "zero_divisor b" shows "zero_divisor (a * b)" proof- from assms obtain c where c0: "c \ 0" and [simp]: "b * c = 0" by auto have "a * b * c = a * (b * c)" by (simp only: ac_simps) with c0 show ?thesis by auto qed lemma not_zero_divisor_mult: fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}" assumes "\ zero_divisor (a * b)" shows "\ zero_divisor a" and "\ zero_divisor b" using assms by (auto dest: zero_divisor_mult_right zero_divisor_mult_left) lemma zero_divisor_smult_left: assumes "zero_divisor a" shows "zero_divisor (smult a f)" proof- from assms obtain b where b0: "b \ 0" and "a * b = 0" by auto then have "smult a f * [:b:] = 0" by (simp add: ac_simps) with b0 show ?thesis by (auto intro!: zero_divisorI[of "[:b:]"]) qed lemma unit_not_zero_divisor: fixes a :: "'a :: {comm_monoid_mult, mult_zero}" assumes "a dvd 1" shows "\zero_divisor a" proof from assms obtain b where ab: "1 = a * b" by (elim dvdE) assume "zero_divisor a" then have "zero_divisor (1::'a)" by (unfold ab, intro zero_divisor_mult_left) then show False by auto qed lemma linear_irreducible\<^sub>d: assumes "degree p = 1" shows "irreducible\<^sub>d p" by (rule irreducible\<^sub>dI, insert assms, auto) lemma irreducible\<^sub>d_dvd_smult: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "degree p > 0" "irreducible\<^sub>d q" "p dvd q" shows "\ c. c \ 0 \ q = smult c p" proof - from assms obtain r where q: "q = p * r" by (elim dvdE, auto) from degree_mult_eq[of p r] assms(1) q have "\ degree p < degree q" and nz: "p \ 0" "q \ 0" apply (metis assms(2) degree_mult_eq_0 gr_implies_not_zero irreducible\<^sub>dD(2) less_add_same_cancel2) using assms by auto hence deg: "degree p \ degree q" by auto from \p dvd q\ obtain k where q: "q = k * p" unfolding dvd_def by (auto simp: ac_simps) with nz have "k \ 0" by auto from deg[unfolded q degree_mult_eq[OF \k \ 0\ \p \ 0\ ]] have "degree k = 0" unfolding q by auto then obtain c where k: "k = [: c :]" by (metis degree_0_id) with \k \ 0\ have "c \ 0" by auto have "q = smult c p" unfolding q k by simp with \c \ 0\ show ?thesis by auto qed subsection \Map over Polynomial Coefficients\ lemma map_poly_simps: shows "map_poly f (pCons c p) = (if c = 0 \ p = 0 then 0 else pCons (f c) (map_poly f p))" proof (cases "c = 0") case True note c0 = this show ?thesis proof (cases "p = 0") case True thus ?thesis using c0 unfolding map_poly_def by simp next case False thus ?thesis unfolding map_poly_def by auto qed next case False thus ?thesis unfolding map_poly_def by auto qed lemma map_poly_pCons[simp]: assumes "c \ 0 \ p \ 0" shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" unfolding map_poly_simps using assms by auto lemma map_poly_map_poly: assumes f0: "f 0 = 0" shows "map_poly f (map_poly g p) = map_poly (f \ g) p" proof (induct p) case (pCons a p) show ?case proof(cases "g a \ 0 \ map_poly g p \ 0") case True show ?thesis unfolding map_poly_pCons[OF pCons(1)] unfolding map_poly_pCons[OF True] unfolding pCons(2) by simp next case False then show ?thesis unfolding map_poly_pCons[OF pCons(1)] unfolding pCons(2)[symmetric] by (simp add: f0) qed qed simp lemma map_poly_zero: assumes f: "\c. f c = 0 \ c = 0" shows [simp]: "map_poly f p = 0 \ p = 0" by (induct p; auto simp: map_poly_simps f) lemma map_poly_add: assumes h0: "h 0 = 0" and h_add: "\p q. h (p + q) = h p + h q" shows "map_poly h (p + q) = map_poly h p + map_poly h q" proof (induct p arbitrary: q) case (pCons a p) note pIH = this show ?case proof(induct "q") case (pCons b q) note qIH = this show ?case unfolding map_poly_pCons[OF qIH(1)] unfolding map_poly_pCons[OF pIH(1)] unfolding add_pCons unfolding pIH(2)[symmetric] unfolding h_add[rule_format,symmetric] unfolding map_poly_simps using h0 by auto qed auto qed auto subsection \Morphismic properties of @{term "pCons 0"}\ lemma monom_pCons_0_monom: "monom (pCons 0 (monom a n)) d = map_poly (pCons 0) (monom (monom a n) d)" apply (induct d) unfolding monom_0 unfolding map_poly_simps apply simp unfolding monom_Suc map_poly_simps by auto lemma pCons_0_add: "pCons 0 (p + q) = pCons 0 p + pCons 0 q" by auto lemma sum_pCons_0_commute: "sum (\i. pCons 0 (f i)) S = pCons 0 (sum f S)" by(induct S rule: infinite_finite_induct;simp) lemma pCons_0_as_mult: fixes p:: "'a :: comm_semiring_1 poly" shows "pCons 0 p = [:0,1:] * p" by auto subsection \Misc\ fun expand_powers :: "(nat \ 'a)list \ 'a list" where "expand_powers [] = []" | "expand_powers ((Suc n, a) # ps) = a # expand_powers ((n,a) # ps)" | "expand_powers ((0,a) # ps) = expand_powers ps" lemma expand_powers: fixes f :: "'a \ 'b :: comm_ring_1" shows "(\ (n,a) \ n_as. f a ^ n) = (\ a \ expand_powers n_as. f a)" by (rule sym, induct n_as rule: expand_powers.induct, auto) lemma poly_smult_zero_iff: fixes x :: "'a :: idom" shows "(poly (smult a p) x = 0) = (a = 0 \ poly p x = 0)" by simp lemma poly_prod_list_zero_iff: fixes x :: "'a :: idom" shows "(poly (prod_list ps) x = 0) = (\ p \ set ps. poly p x = 0)" by (induct ps, auto) lemma poly_mult_zero_iff: fixes x :: "'a :: idom" shows "(poly (p * q) x = 0) = (poly p x = 0 \ poly q x = 0)" by simp lemma poly_power_zero_iff: fixes x :: "'a :: idom" shows "(poly (p^n) x = 0) = (n \ 0 \ poly p x = 0)" by (cases n, auto) lemma sum_monom_0_iff: assumes fin: "finite S" and g: "\ i j. g i = g j \ i = j" shows "sum (\ i. monom (f i) (g i)) S = 0 \ (\ i \ S. f i = 0)" (is "?l = ?r") proof - { assume "\ ?r" then obtain i where i: "i \ S" and fi: "f i \ 0" by auto let ?g = "\ i. monom (f i) (g i)" have "coeff (sum ?g S) (g i) = f i + sum (\ j. coeff (?g j) (g i)) (S - {i})" by (unfold sum.remove[OF fin i], simp add: coeff_sum) also have "sum (\ j. coeff (?g j) (g i)) (S - {i}) = 0" by (rule sum.neutral, insert g, auto) finally have "coeff (sum ?g S) (g i) \ 0" using fi by auto hence "\ ?l" by auto } thus ?thesis by auto qed lemma degree_prod_list_eq: assumes "\ p. p \ set ps \ (p :: 'a :: idom poly) \ 0" shows "degree (prod_list ps) = sum_list (map degree ps)" using assms proof (induct ps) case (Cons p ps) show ?case unfolding prod_list.Cons by (subst degree_mult_eq, insert Cons, auto simp: prod_list_zero_iff) qed simp lemma degree_power_eq: assumes p: "p \ 0" shows "degree (p ^ n) = degree (p :: 'a :: idom poly) * n" proof (induct n) case (Suc n) from p have pn: "p ^ n \ 0" by auto show ?case using degree_mult_eq[OF p pn] Suc by auto qed simp lemma coeff_Poly: "coeff (Poly xs) i = (nth_default 0 xs i)" unfolding nth_default_coeffs_eq[of "Poly xs", symmetric] coeffs_Poly by simp lemma rsquarefree_def': "rsquarefree p = (p \ 0 \ (\a. order a p \ 1))" proof - have "\ a. order a p \ 1 \ order a p = 0 \ order a p = 1" by linarith thus ?thesis unfolding rsquarefree_def by auto qed lemma order_prod_list: "(\ p. p \ set ps \ p \ 0) \ order x (prod_list ps) = sum_list (map (order x) ps)" by (induct ps, auto, subst order_mult, auto simp: prod_list_zero_iff) lemma irreducible\<^sub>d_dvd_eq: fixes a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "irreducible\<^sub>d a" and "irreducible\<^sub>d b" and "a dvd b" and "monic a" and "monic b" shows "a = b" using assms by (metis (no_types, lifting) coeff_smult degree_smult_eq irreducible\<^sub>dD(1) irreducible\<^sub>d_dvd_smult mult.right_neutral smult_1_left) lemma monic_gcd_dvd: assumes fg: "f dvd g" and mon: "monic f" and gcd: "gcd g h \ {1, g}" shows "gcd f h \ {1, f}" proof (cases "coprime g h") case True with dvd_refl have "coprime f h" using fg by (blast intro: coprime_divisors) then show ?thesis by simp next case False with gcd have gcd: "gcd g h = g" by (simp add: coprime_iff_gcd_eq_1) with fg have "f dvd gcd g h" by simp then have "f dvd h" by simp then have "gcd f h = normalize f" by (simp add: gcd_proj1_iff) also have "normalize f = f" using mon by (rule normalize_monic) finally show ?thesis by simp qed lemma monom_power: "(monom a b)^n = monom (a^n) (b*n)" by (induct n, auto simp add: mult_monom) lemma poly_const_pow: "[:a:]^b = [:a^b:]" by (metis Groups.mult_ac(2) monom_0 monom_power mult_zero_right) lemma degree_pderiv_le: "degree (pderiv f) \ degree f - 1" proof (rule ccontr) assume "\ ?thesis" hence ge: "degree (pderiv f) \ Suc (degree f - 1)" by auto hence "pderiv f \ 0" by auto hence "coeff (pderiv f) (degree (pderiv f)) \ 0" by auto from this[unfolded coeff_pderiv] have "coeff f (Suc (degree (pderiv f))) \ 0" by auto moreover have "Suc (degree (pderiv f)) > degree f" using ge by auto ultimately show False by (simp add: coeff_eq_0) qed lemma map_div_is_smult_inverse: "map_poly (\x. x / (a :: 'a :: field)) p = smult (inverse a) p" unfolding smult_conv_map_poly by (simp add: divide_inverse_commute) lemma normalize_poly_old_def: "normalize (f :: 'a :: {normalization_semidom,field} poly) = smult (inverse (unit_factor (lead_coeff f))) f" by (simp add: normalize_poly_eq_map_poly map_div_is_smult_inverse) (* was in Euclidean_Algorithm in Number_Theory before, but has been removed *) lemma poly_dvd_antisym: fixes p q :: "'b::idom poly" assumes coeff: "coeff p (degree p) = coeff q (degree q)" assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" proof (cases "p = 0") case True with coeff show "p = q" by simp next case False with coeff have "q \ 0" by auto have degree: "degree p = degree q" using \p dvd q\ \q dvd p\ \p \ 0\ \q \ 0\ by (intro order_antisym dvd_imp_degree_le) from \p dvd q\ obtain a where a: "q = p * a" .. with \q \ 0\ have "a \ 0" by auto with degree a \p \ 0\ have "degree a = 0" by (simp add: degree_mult_eq) with coeff a show "p = q" by (cases a, auto split: if_splits) qed lemma coeff_f_0_code[code_unfold]: "coeff f 0 = (case coeffs f of [] \ 0 | x # _ \ x)" by (cases f, auto simp: cCons_def) lemma poly_compare_0_code[code_unfold]: "(f = 0) = (case coeffs f of [] \ True | _ \ False)" using coeffs_eq_Nil list.disc_eq_case(1) by blast text \Getting more efficient code for abbreviation @{term lead_coeff}"\ definition leading_coeff where [code_abbrev, simp]: "leading_coeff = lead_coeff" lemma leading_coeff_code [code]: "leading_coeff f = (let xs = coeffs f in if xs = [] then 0 else last xs)" by (simp add: last_coeffs_eq_coeff_degree) lemma nth_coeffs_coeff: "i < length (coeffs f) \ coeffs f ! i = coeff f i" by (metis nth_default_coeffs_eq nth_default_def) definition monom_mult :: "nat \ 'a :: comm_semiring_1 poly \ 'a poly" where "monom_mult n f = monom 1 n * f" lemma monom_mult_unfold [code_unfold]: "monom 1 n * f = monom_mult n f" "f * monom 1 n = monom_mult n f" by (auto simp: monom_mult_def ac_simps) lemma monom_mult_code [code abstract]: "coeffs (monom_mult n f) = (let xs = coeffs f in if xs = [] then xs else replicate n 0 @ xs)" by (rule coeffs_eqI) (auto simp add: Let_def monom_mult_def coeff_monom_mult nth_default_append nth_default_coeffs_eq) lemma coeff_pcompose_monom: fixes f :: "'a :: comm_ring_1 poly" assumes n: "j < n" shows "coeff (f \\<^sub>p monom 1 n) (n * i + j) = (if j = 0 then coeff f i else 0)" proof (induct f arbitrary: i) case (pCons a f i) note d = pcompose_pCons coeff_add coeff_monom_mult coeff_pCons show ?case proof (cases i) case 0 show ?thesis unfolding d 0 using n by (cases j, auto) next case (Suc ii) have id: "n * Suc ii + j - n = n * ii + j" using n by (simp add: diff_mult_distrib2) have id1: "(n \ n * Suc ii + j) = True" by auto have id2: "(case n * Suc ii + j of 0 \ a | Suc x \ coeff 0 x) = 0" using n by (cases "n * Suc ii + j", auto) show ?thesis unfolding d Suc id id1 id2 pCons(2) if_True by auto qed qed auto lemma coeff_pcompose_x_pow_n: fixes f :: "'a :: comm_ring_1 poly" assumes n: "n \ 0" shows "coeff (f \\<^sub>p monom 1 n) (n * i) = coeff f i" using coeff_pcompose_monom[of 0 n f i] n by auto lemma dvd_dvd_smult: "a dvd b \ f dvd g \ smult a f dvd smult b g" unfolding dvd_def by (metis mult_smult_left mult_smult_right smult_smult) definition sdiv_poly :: "'a :: idom_divide poly \ 'a \ 'a poly" where "sdiv_poly p a = (map_poly (\ c. c div a) p)" lemma smult_map_poly: "smult a = map_poly ((*) a)" by (rule ext, rule poly_eqI, subst coeff_map_poly, auto) lemma smult_exact_sdiv_poly: assumes "\ c. c \ set (coeffs p) \ a dvd c" shows "smult a (sdiv_poly p a) = p" unfolding smult_map_poly sdiv_poly_def by (subst map_poly_map_poly,simp,rule map_poly_idI, insert assms, auto) lemma coeff_sdiv_poly: "coeff (sdiv_poly f a) n = coeff f n div a" unfolding sdiv_poly_def by (rule coeff_map_poly, auto) lemma poly_pinfty_ge: fixes p :: "real poly" assumes "lead_coeff p > 0" "degree p \ 0" shows "\n. \ x \ n. poly p x \ b" proof - let ?p = "p - [:b - lead_coeff p :]" have id: "lead_coeff ?p = lead_coeff p" using assms(2) by (cases p, auto) with assms(1) have "lead_coeff ?p > 0" by auto from poly_pinfty_gt_lc[OF this, unfolded id] obtain n where "\ x. x \ n \ 0 \ poly p x - b" by auto thus ?thesis by auto qed lemma pderiv_sum: "pderiv (sum f I) = sum (\ i. (pderiv (f i))) I" by (induct I rule: infinite_finite_induct, auto simp: pderiv_add) lemma smult_sum2: "smult m (\i \ S. f i) = (\i \ S. smult m (f i))" by (induct S rule: infinite_finite_induct, auto simp add: smult_add_right) lemma degree_mult_not_eq: "degree (f * g) \ degree f + degree g \ lead_coeff f * lead_coeff g = 0" by (rule ccontr, auto simp: coeff_mult_degree_sum degree_mult_le le_antisym le_degree) lemma irreducible\<^sub>d_multD: fixes a b :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes l: "irreducible\<^sub>d (a*b)" shows "degree a = 0 \ a \ 0 \ irreducible\<^sub>d b \ degree b = 0 \ b \ 0 \ irreducible\<^sub>d a" proof- from l have a0: "a \ 0" and b0: "b \ 0" by auto note [simp] = degree_mult_eq[OF this] from l have "degree a = 0 \ degree b = 0" apply (unfold irreducible\<^sub>d_def) by force then show ?thesis proof(elim disjE) assume a: "degree a = 0" with l a0 have "irreducible\<^sub>d b" by (simp add: irreducible\<^sub>d_def) (metis degree_mult_eq degree_mult_eq_0 mult.left_commute plus_nat.add_0) with a a0 show ?thesis by auto next assume b: "degree b = 0" with l b0 have "irreducible\<^sub>d a" unfolding irreducible\<^sub>d_def - by (smt add_cancel_left_right degree_mult_eq degree_mult_eq_0 neq0_conv semiring_normalization_rules(16)) + by (smt (verit) add_cancel_left_right degree_mult_eq degree_mult_eq_0 neq0_conv semiring_normalization_rules(16)) with b b0 show ?thesis by auto qed qed lemma irreducible_connect_field[simp]: fixes f :: "'a :: field poly" shows "irreducible\<^sub>d f = irreducible f" (is "?l = ?r") proof show "?r \ ?l" apply (intro irreducible\<^sub>dI, force simp:is_unit_iff_degree) by (auto dest!: irreducible_multD simp: poly_dvd_1) next assume l: ?l show ?r proof (rule irreducibleI) from l show "f \ 0" "\ is_unit f" by (auto simp: poly_dvd_1) fix a b assume "f = a * b" from l[unfolded this] show "a dvd 1 \ b dvd 1" by (auto dest!: irreducible\<^sub>d_multD simp:is_unit_iff_degree) qed qed lemma is_unit_field_poly[simp]: fixes p :: "'a::field poly" shows "is_unit p \ p \ 0 \ degree p = 0" by (cases "p=0", auto simp: is_unit_iff_degree) lemma irreducible_smult_field[simp]: fixes c :: "'a :: field" shows "irreducible (smult c p) \ c \ 0 \ irreducible p" (is "?L \ ?R") proof (intro iffI conjI irreducible\<^sub>d_smult_not_zero_divisor_left[of c p, simplified]) assume "irreducible (smult c p)" then show "c \ 0" by auto next assume ?R then have c0: "c \ 0" and irr: "irreducible p" by auto show ?L proof (fold irreducible_connect_field, intro irreducible\<^sub>dI, unfold degree_smult_eq if_not_P[OF c0]) show "degree p > 0" using irr by auto fix q r from c0 have "p = smult (1/c) (smult c p)" by simp also assume "smult c p = q * r" finally have [simp]: "p = smult (1/c) \". assume main: "degree q < degree p" "degree r < degree p" have "\irreducible\<^sub>d p" by (rule reducible\<^sub>dI, rule exI[of _ "smult (1/c) q"], rule exI[of _ r], insert irr c0 main, simp) with irr show False by auto qed qed auto lemma irreducible_monic_factor: fixes p :: "'a :: field poly" assumes "degree p > 0" shows "\ q r. irreducible q \ p = q * r \ monic q" proof - from irreducible\<^sub>d_factorization_exists[OF assms] obtain fs where "fs \ []" and "set fs \ Collect irreducible" and "p = prod_list fs" by auto then have q: "irreducible (hd fs)" and p: "p = hd fs * prod_list (tl fs)" by (atomize(full), cases fs, auto) define c where "c = coeff (hd fs) (degree (hd fs))" from q have c: "c \ 0" unfolding c_def irreducible\<^sub>d_def by auto show ?thesis by (rule exI[of _ "smult (1/c) (hd fs)"], rule exI[of _ "smult c (prod_list (tl fs))"], unfold p, insert q c, auto simp: c_def) qed lemma monic_irreducible_factorization: fixes p :: "'a :: field poly" shows "monic p \ \ as f. finite as \ p = prod (\ a. a ^ Suc (f a)) as \ as \ {q. irreducible q \ monic q}" proof (induct "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "degree p > 0") case False with less(2) have "p = 1" by (simp add: coeff_eq_0 poly_eq_iff) thus ?thesis by (intro exI[of _ "{}"], auto) next case True from irreducible\<^sub>d_factor[OF this] obtain q r where p: "p = q * r" and q: "irreducible q" and deg: "degree r < degree p" by auto hence q0: "q \ 0" by auto define c where "c = coeff q (degree q)" let ?q = "smult (1/c) q" let ?r = "smult c r" from q0 have c: "c \ 0" "1 / c \ 0" unfolding c_def by auto hence p: "p = ?q * ?r" unfolding p by auto have deg: "degree ?r < degree p" using c deg by auto let ?Q = "{q. irreducible q \ monic (q :: 'a poly)}" have mon: "monic ?q" unfolding c_def using q0 by auto from monic_factor[OF \monic p\[unfolded p] this] have "monic ?r" . from less(1)[OF deg this] obtain f as where as: "finite as" "?r = (\ a \as. a ^ Suc (f a))" "as \ ?Q" by blast from q c have irred: "irreducible ?q" by simp show ?thesis proof (cases "?q \ as") case False let ?as = "insert ?q as" let ?f = "\ a. if a = ?q then 0 else f a" have "p = ?q * (\ a \as. a ^ Suc (f a))" unfolding p as by simp also have "(\ a \as. a ^ Suc (f a)) = (\ a \as. a ^ Suc (?f a))" by (rule prod.cong, insert False, auto) also have "?q * \ = (\ a \ ?as. a ^ Suc (?f a))" by (subst prod.insert, insert as False, auto) finally have p: "p = (\ a \ ?as. a ^ Suc (?f a))" . from as(1) have fin: "finite ?as" by auto from as mon irred have Q: "?as \ ?Q" by auto from fin p Q show ?thesis by(intro exI[of _ ?as] exI[of _ ?f], auto) next case True let ?f = "\ a. if a = ?q then Suc (f a) else f a" have "p = ?q * (\ a \as. a ^ Suc (f a))" unfolding p as by simp also have "(\ a \as. a ^ Suc (f a)) = ?q ^ Suc (f ?q) * (\ a \(as - {?q}). a ^ Suc (f a))" by (subst prod.remove[OF _ True], insert as, auto) also have "(\ a \(as - {?q}). a ^ Suc (f a)) = (\ a \(as - {?q}). a ^ Suc (?f a))" by (rule prod.cong, auto) also have "?q * (?q ^ Suc (f ?q) * \ ) = ?q ^ Suc (?f ?q) * \" by (simp add: ac_simps) also have "\ = (\ a \ as. a ^ Suc (?f a))" by (subst prod.remove[OF _ True], insert as, auto) finally have "p = (\ a \ as. a ^ Suc (?f a))" . with as show ?thesis by (intro exI[of _ as] exI[of _ ?f], auto) qed qed qed lemma monic_irreducible_gcd: "monic (f::'a::{field,euclidean_ring_gcd,semiring_gcd_mult_normalize, normalization_euclidean_semiring_multiplicative} poly) \ irreducible f \ gcd f u \ {1,f}" by (metis gcd_dvd1 irreducible_altdef insertCI is_unit_gcd_iff poly_dvd_antisym poly_gcd_monic) end