# HG changeset patch # User paulson # Date 1530608855 -3600 # Node ID ec4fe1032b6e03205a7a6ad1a9c7027388486d22 # Parent b9b9e29858782ba21c31d49417b9a7fc86da064a# Parent 654e73d05495c2f39b25ea2491c4dd9f977899d1 merged diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Algebra.thy --- a/src/HOL/Algebra/Algebra.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Algebra.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Algebra/Algebra *) +(* Title: HOL/Algebra/Algebra.thy *) theory Algebra imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Chinese_Remainder.thy --- a/src/HOL/Algebra/Chinese_Remainder.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Chinese_Remainder.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Chinese_Remainder.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Chinese_Remainder.thy + Author: Paulo Emílio de Vilhena +*) theory Chinese_Remainder imports QuotRing Ideal_Product - begin section \Chinese Remainder Theorem\ @@ -1204,4 +1202,4 @@ is_ring by (simp add: ring_hom_ringI2) qed -end \ No newline at end of file +end diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Coset.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,5 +1,6 @@ (* Title: HOL/Algebra/Coset.thy - Authors: Florian Kammueller, L C Paulson, Stephan Hohe + Authors: Florian Kammueller, L C Paulson, Stephan Hohe + With additional contributions from Martin Baillon and Paulo Emílio de Vilhena. *) diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Cycles.thy --- a/src/HOL/Algebra/Cycles.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Cycles.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Cycles.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Cycles.thy + Author: Paulo Emílio de Vilhena +*) theory Cycles imports "HOL-Library.Permutations" "HOL-Library.FuncSet" - begin section \Cycles\ @@ -753,4 +751,4 @@ shows "cycle_decomp S p" using assms cycle_decomposition_aux by blast -end \ No newline at end of file +end diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Embedded_Algebras.thy --- a/src/HOL/Algebra/Embedded_Algebras.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Embedded_Algebras.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Embedded_Algebras.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Embedded_Algebras.thy + Author: Paulo Emílio de Vilhena +*) theory Embedded_Algebras imports Subrings Generated_Groups - begin section \Definitions\ @@ -1315,4 +1313,4 @@ qed *) -end \ No newline at end of file +end diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Exact_Sequence.thy --- a/src/HOL/Algebra/Exact_Sequence.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Exact_Sequence.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Exact_Sequence.thy *) -(* Author: Martin Baillon *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Exact_Sequence.thy + Author: Martin Baillon +*) theory Exact_Sequence imports Group Coset Solvable_Groups - begin section \Exact Sequences\ @@ -176,4 +174,3 @@ using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast end - \ No newline at end of file diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Generated_Fields.thy --- a/src/HOL/Algebra/Generated_Fields.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Generated_Fields.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,12 +1,9 @@ -(* ************************************************************************** *) -(* Title: Generated_Fields.thy *) -(* Author: Martin Baillon *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Generated_Fields.thy + Author: Martin Baillon +*) theory Generated_Fields - imports Generated_Rings Subrings Multiplicative_Group - begin inductive_set @@ -184,7 +181,4 @@ subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)] by force - - end - diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Generated_Groups.thy --- a/src/HOL/Algebra/Generated_Groups.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Generated_Groups.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Generated_Groups.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Generated_Groups.thy + Author: Paulo Emílio de Vilhena +*) theory Generated_Groups imports Group Coset - begin section\Generated Groups\ diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Group_Action.thy --- a/src/HOL/Algebra/Group_Action.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Group_Action.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,9 +1,9 @@ -(* Title: Group_Action.thy *) -(* Author: Paulo Emílio de Vilhena *) +(* Title: HOL/Algebra/Group_Action.thy + Author: Paulo Emílio de Vilhena +*) theory Group_Action imports Bij Coset Congruence - begin section \Group Actions\ @@ -922,4 +922,4 @@ using induced_homomorphism assms group.subgroup_imp_group group_BijGroup group_hom group_hom.axioms(1) group_hom_axioms_def by blast -end \ No newline at end of file +end diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Ideal_Product.thy --- a/src/HOL/Algebra/Ideal_Product.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Ideal_Product.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Ideal_Product.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Ideal_Product.thy + Author: Paulo Emílio de Vilhena +*) theory Ideal_Product imports Ideal - begin section \Product of Ideals\ @@ -587,4 +585,4 @@ using assms is_cring by (simp add: primeidealI) qed -end \ No newline at end of file +end diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Module.thy --- a/src/HOL/Algebra/Module.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Module.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/Algebra/Module.thy Author: Clemens Ballarin, started 15 April 2003 - with contributions by Martin Baillon + with contributions by Martin Baillon *) theory Module diff -r 654e73d05495 -r ec4fe1032b6e src/HOL/Algebra/Polynomials.thy --- a/src/HOL/Algebra/Polynomials.thy Tue Jul 03 10:07:24 2018 +0100 +++ b/src/HOL/Algebra/Polynomials.thy Tue Jul 03 10:07:35 2018 +0100 @@ -1,11 +1,9 @@ -(* ************************************************************************** *) -(* Title: Polynomials.thy *) -(* Author: Paulo Emílio de Vilhena *) -(* ************************************************************************** *) +(* Title: HOL/Algebra/Polynomials.thy + Author: Paulo Emílio de Vilhena +*) theory Polynomials imports Ring Ring_Divisibility Subrings - begin section \Polynomials\ @@ -127,7 +125,7 @@ using degree_def[of "a # p"] by auto also have " ... = a # p" using Cons by simp - finally show ?case . + finally show ?case . qed lemma coeff_nth: "i < length p \ (coeff p) i = p ! (length p - 1 - i)" @@ -228,7 +226,7 @@ assume "p1 \ [] \ p2 \ []" hence "length p1 = length p2" using deg_eq unfolding degree_def - by (simp add: Nitpick.size_list_simp(2)) + by (simp add: Nitpick.size_list_simp(2)) thus ?thesis using coeff_iff_length_cond[of p1 p2] coeff_eq by simp next @@ -681,7 +679,7 @@ proof - let ?len = length and ?norm = normalize obtain a p' where p: "p = a # p'" - using assms(2) list.exhaust_sel by blast + using assms(2) list.exhaust_sel by blast hence a: "a \ carrier R - { \ }" and p': "set p' \ carrier R" using assms(1) unfolding p by (auto simp add: polynomial_def) hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'" @@ -742,7 +740,7 @@ next case (Cons a p1) let ?a_p2 = "(map (\b. a \ b) p2) @ (replicate (degree (a # p1)) \)" - + have "set (poly_mult p1 p2) \ carrier R" using Cons unfolding polynomial_def by auto @@ -775,7 +773,7 @@ lemma poly_mult_coeff: assumes "set p1 \ carrier R" "set p2 \ carrier R" shows "coeff (poly_mult p1 p2) = (\i. \ k \ {..i}. (coeff p1) k \ (coeff p2) (i - k))" - using assms(1) + using assms(1) proof (induction p1) case Nil thus ?case using assms(2) by auto next @@ -823,7 +821,7 @@ have "\k. k \ {..i} \ ?f2 k \\<^bsub>R\<^esub> ?f3 (i - k) = (if length p1 = k then a \ coeff p2 (i - k) else \)" using in_carrier by auto - hence "(\ k \ {..i}. ?f2 k \ ?f3 (i - k)) = + hence "(\ k \ {..i}. ?f2 k \ ?f3 (i - k)) = (\ k \ {..i}. (if length p1 = k then a \ coeff p2 (i - k) else \))" using in_carrier add.finprod_cong'[of "{..i}" "{..i}" "\k. ?f2 k \ ?f3 (i - k)" @@ -848,7 +846,7 @@ using in_carrier(1) assms(2) by auto moreover have "set (poly_mult p1 p2) \ carrier R" - using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto + using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto ultimately have "coeff (poly_mult (a # p1) p2) = (\i. ((coeff ?a_p2) i) \ ((coeff (poly_mult p1 p2)) i))" @@ -910,7 +908,7 @@ and "polynomial R (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier by auto ultimately show ?thesis - using coeff_iff_polynomial_cond by auto + using coeff_iff_polynomial_cond by auto qed lemma poly_mult_l_distr: @@ -938,7 +936,7 @@ normalize_replicate_zero[of "length p2 + length p1" "[]"] by auto finally show ?thesis by auto qed } note aux_lemma = this - + from assms show ?thesis proof (induction n) case 0 thus ?case by simp @@ -988,7 +986,7 @@ using inj_on_def by force moreover have "(\k. i - k) ` {..i} \ {..i}" by auto hence "(\k. i - k) ` {..i} = {..i}" - using reindex_inj endo_inj_surj[of "{..i}" "\k. i - k"] by simp + using reindex_inj endo_inj_surj[of "{..i}" "\k. i - k"] by simp ultimately have "(\k \ {..i}. ?f k) = (\k \ {..i}. ?f (i - k))" using add.finprod_reindex[of ?f "\k. i - k" "{..i}"] in_carrier by auto @@ -1041,7 +1039,7 @@ using poly_add_normalize(1)[of "replicate (length p + n) \" "[]"] normalize_replicate_zero[of "length p + n" "[]"] by auto also have " ... = []" by simp - finally show ?case . + finally show ?case . qed thus "poly_mult p (replicate n \) = []" using poly_mult_comm[OF assms in_carrier] by simp @@ -1061,9 +1059,9 @@ next case (Cons b ps) hence "a \ lead_coeff p \ \" - using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto + using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto thus ?thesis - using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto + using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto qed ultimately show ?thesis using poly_add_zero(1)[of "map (\b. a \ b) p"] by simp @@ -1086,7 +1084,7 @@ hence "lead_coeff ((map (\b. a \ b) p) @ (replicate n \)) \ \" using Cons assms integral[of a b] unfolding polynomial_def by auto moreover have "set ((map (\b. a \ b) p) @ (replicate n \)) \ carrier R" - using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto + using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto ultimately have is_polynomial: "polynomial R ((map (\b. a \ b) p) @ (replicate n \))" using Cons unfolding polynomial_def by auto @@ -1107,7 +1105,7 @@ shows "poly_mult [ \ ] p = p" and "poly_mult p [ \ ] = p" proof - have "map (\a. \ \ a) p = p" - using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE) + using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE) thus "poly_mult [ \ ] p = p" and "poly_mult p [ \ ] = p" using poly_mult_const[OF assms, of \] by auto qed @@ -1119,7 +1117,7 @@ have p1: "lead_coeff p1 \ carrier R - { \ }" and p2: "lead_coeff p2 \ carrier R - { \ }" using assms unfolding polynomial_def by auto - have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = + have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = (\ k \ {..((degree p1) + (degree p2))}. (coeff p1) k \ (coeff p2) ((degree p1) + (degree p2) - k))" using poly_mult_coeff assms(1-2) polynomial_in_carrier by auto @@ -1299,7 +1297,7 @@ also have " ... = (\i \ {..n - ?len}. (a \ ?c2 i) \ ?c3 (n - (i + ?len)))" unfolding h_def by simp also have " ... = (\i \ {..n - ?len}. a \ (?c2 i \ ?c3 (n - (i + ?len))))" - using in_carrier assms(3) by (simp add: m_assoc) + using in_carrier assms(3) by (simp add: m_assoc) also have " ... = a \ (\i \ {..n - ?len}. ?c2 i \ ?c3 (n - (i + ?len)))" using finsum_rdistr[of "{..n - ?len}" a "\i. ?c2 i \ ?c3 (n - (i + ?len))"] in_carrier(2-3) assms(3) by simp @@ -1427,10 +1425,10 @@ proof (auto) fix p assume p: "polynomial R p" have "polynomial R [ \ \ ]" - unfolding polynomial_def using r_neg by fastforce + unfolding polynomial_def using r_neg by fastforce hence cond0: "polynomial R (poly_mult [ \ \ ] p)" using poly_mult_closed[of "[ \ \ ]" p] p by simp - + have "poly_add p (poly_mult [ \ \ ] p) = poly_add (poly_mult [ \ ] p) (poly_mult [ \ \ ] p)" using poly_mult_one[OF p] by simp also have " ... = poly_mult (poly_add [ \ ] [ \ \ ]) p" @@ -1498,51 +1496,6 @@ (auto simp add: univ_poly_def domain.poly_mult_integral[OF assms]) qed -lemma (in domain) univ_poly_a_inv_def': - assumes "p \ carrier (univ_poly R)" - shows "\\<^bsub>(univ_poly R)\<^esub> p = map (\a. \ a) p" -proof - - have aux_lemma: - "\p. p \ carrier (univ_poly R) \ p \\<^bsub>(univ_poly R)\<^esub> (map (\a. \ a) p) = []" - "\p. p \ carrier (univ_poly R) \ (map (\a. \ a) p) \ carrier (univ_poly R)" - proof - - fix p assume p: "p \ carrier (univ_poly R)" - hence set_p: "set p \ carrier R" - unfolding univ_poly_def polynomial_def by auto - show "(map (\a. \ a) p) \ carrier (univ_poly R)" - proof (cases "p = []") - assume "p = []" thus ?thesis - unfolding univ_poly_def polynomial_def by auto - next - assume not_nil: "p \ []" - hence "lead_coeff p \ \" - using p unfolding univ_poly_def polynomial_def by auto - moreover have "lead_coeff (map (\a. \ a) p) = \ (lead_coeff p)" - using not_nil by (simp add: hd_map) - ultimately have "lead_coeff (map (\a. \ a) p) \ \" - using hd_in_set local.minus_zero not_nil set_p by force - moreover have "set (map (\a. \ a) p) \ carrier R" - using set_p by (induct p) (auto) - ultimately show ?thesis - unfolding univ_poly_def polynomial_def by auto - qed - - have "map2 (\) p (map (\a. \ a) p) = replicate (length p) \" - using set_p by (induct p) (auto simp add: r_neg) - thus "p \\<^bsub>(univ_poly R)\<^esub> (map (\a. \ a) p) = []" - unfolding univ_poly_def using normalize_replicate_zero[of "length p" "[]"] by auto - qed - - interpret UP: ring "univ_poly R" - using univ_poly_is_ring[OF domain_axioms] . - - from aux_lemma - have "\p. p \ carrier (univ_poly R) \ \\<^bsub>(univ_poly R)\<^esub> p = map (\a. \ a) p" - by (metis Nil_is_map_conv UP.add.inv_closed UP.l_zero UP.r_neg1 UP.r_zero UP.zero_closed) - thus ?thesis - using assms by simp -qed - subsection \Long Division Theorem\ @@ -1564,7 +1517,7 @@ proof (cases "length b > length p") assume "length b > length p" hence "p = [] \ degree p < degree b" unfolding degree_def - by (meson diff_less_mono length_0_conv less_one not_le) + by (meson diff_less_mono length_0_conv less_one not_le) hence "?long_division p [] p" using poly_add_zero[OF less(2)] less(2) zero_is_polynomial poly_mult_zero[OF less(3)] by simp @@ -1591,7 +1544,7 @@ hence s_coeff: "lead_coeff s = (\ a)" using poly_mult_lead_coeff[OF monon_is_polynomial[OF in_carrier] less(3)] a c unfolding monon_def s_def b using m_assoc by force - + have "degree s = degree (monon ((\ a) \ inv c) (?len p - ?len b)) + degree b" using poly_mult_degree_eq[OF monon_is_polynomial[OF in_carrier] less(3)] unfolding s_def b monon_def by auto @@ -1605,7 +1558,7 @@ by (simp add: Nitpick.size_list_simp(2) local.Cons) obtain s' where s: "s = (\ a) # s'" - using s_coeff len_eq by (metis \s \ []\ hd_Cons_tl) + using s_coeff len_eq by (metis \s \ []\ hd_Cons_tl) define p_diff where "p_diff = poly_add p s" hence "?len p_diff < ?len p" @@ -1623,7 +1576,7 @@ using s_def monon_is_polynomial[OF in_carrier(1)] by auto have in_univ_carrier: "p \ carrier (univ_poly R)" "m \ carrier (univ_poly R)" "b \ carrier (univ_poly R)" - "r' \ carrier (univ_poly R)" "q' \ carrier (univ_poly R)" + "r' \ carrier (univ_poly R)" "q' \ carrier (univ_poly R)" using r' q' less(2-3) m(1) unfolding univ_poly_def by auto hence "poly_add p (poly_mult m b) = poly_add (poly_mult b q') r'" @@ -1634,7 +1587,7 @@ "(p \\<^bsub>(univ_poly R)\<^esub> (m \\<^bsub>(univ_poly R)\<^esub> b)) \\<^bsub>(univ_poly R)\<^esub> (m \\<^bsub>(univ_poly R)\<^esub> b) = ((b \\<^bsub>(univ_poly R)\<^esub>q') \\<^bsub>(univ_poly R)\<^esub> r') \\<^bsub>(univ_poly R)\<^esub> (m \\<^bsub>(univ_poly R)\<^esub> b)" by simp - hence "p = (b \\<^bsub>(univ_poly R)\<^esub> (q' \\<^bsub>(univ_poly R)\<^esub> m)) \\<^bsub>(univ_poly R)\<^esub> r'" + hence "p = (b \\<^bsub>(univ_poly R)\<^esub> (q' \\<^bsub>(univ_poly R)\<^esub> m)) \\<^bsub>(univ_poly R)\<^esub> r'" using in_univ_carrier by algebra hence "p = poly_add (poly_mult b (q' \\<^bsub>(univ_poly R)\<^esub> m)) r'" unfolding univ_poly_def by simp @@ -1656,7 +1609,7 @@ using long_division_theorem[OF assms] assms lead_coeff_not_zero[of "hd b" "tl b"] by (simp add: field_Units) -theorem univ_poly_is_euclidean: +lemma univ_poly_is_euclidean_domain: assumes "field R" shows "euclidean_domain (univ_poly R) degree" proof - @@ -1668,16 +1621,6 @@ using field.field_long_division_theorem[OF assms] by auto qed -corollary univ_poly_is_principal: - assumes "field R" - shows "principal_domain (univ_poly R)" -proof - - interpret UP: euclidean_domain "univ_poly R" degree - using univ_poly_is_euclidean[OF assms] . - show ?thesis - using UP.principal_domain_axioms . -qed - subsection \Consistency Rules\ @@ -1707,7 +1650,7 @@ qed lemma (in ring) poly_add_consistent [simp]: - assumes "subring K R" shows "ring.poly_add (R \ carrier := K \) = poly_add" + assumes "subring K R" shows "ring.poly_add (R \ carrier := K \) = poly_add" proof - have "\p q. ring.poly_add (R \ carrier := K \) p q = poly_add p q" proof - @@ -1721,7 +1664,7 @@ assumes "subring K R" shows "ring.poly_mult (R \ carrier := K \) = poly_mult" proof - have "\p q. ring.poly_mult (R \ carrier := K \) p q = poly_mult p q" - proof - + proof - fix p q show "ring.poly_mult (R \ carrier := K \) p q = poly_mult p q" using ring.poly_mult.simps[OF subring_is_ring[OF assms]] poly_add_consistent[OF assms] by (induct p) (auto) @@ -1729,7 +1672,7 @@ thus ?thesis by auto qed -lemma (in ring) univ_poly_subring_def': +lemma (in ring) univ_poly_carrier_change_def': assumes "subring K R" shows "univ_poly (R \ carrier := K \) = (univ_poly R) \ carrier := { p. polynomial R p \ set p \ K } \" unfolding univ_poly_def polynomial_def @@ -1738,26 +1681,6 @@ subringE(1)[OF assms] by auto -lemma (in domain) univ_poly_subring_is_domain: - assumes "subring K R" - shows "domain (univ_poly (R \ carrier := K \))" -proof - - have "domain (R \ carrier := K \)" - using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] . - thus ?thesis - using univ_poly_is_domain[of "R \ carrier := K \"] by simp -qed - -lemma (in domain) univ_poly_subfield_is_euclidean: - assumes "subfield K R" - shows "euclidean_domain (univ_poly (R \ carrier := K \)) degree" - using univ_poly_is_euclidean[OF subfield_iff(2)[OF assms]] . - -lemma (in domain) univ_poly_subfield_is_principal: - assumes "subfield K R" - shows "principal_domain (univ_poly (R \ carrier := K \))" - using univ_poly_is_principal[OF subfield_iff(2)[OF assms]] . - subsection \The Evaluation Homomorphism\ @@ -1886,7 +1809,7 @@ hence "set (map ((\) b) q) \ carrier R" and "set (replicate n \) \ carrier R" using assms(2) by (induct q) (auto) hence "eval ((map ((\) b) q) @ (replicate n \)) a = (eval ((map ((\) b) q)) a) \ (a [^] n) \ \" - using eval_append[OF _ _ assms(3), of "map ((\) b) q" "replicate n \"] + using eval_append[OF _ _ assms(3), of "map ((\) b) q" "replicate n \"] eval_replicate[OF _ assms(3), of "[]"] by auto moreover have "eval (map ((\) b) q) a = b \ eval q a" using assms(2-3) eval_in_carrier b by(induct q) (auto simp add: degree_def m_assoc r_distr) @@ -1920,309 +1843,10 @@ proposition (in cring) eval_is_hom: assumes "subring K R" and "a \ carrier R" shows "(\p. (eval p) a) \ ring_hom (univ_poly (R \ carrier := K \)) R" - unfolding univ_poly_subring_def'[OF assms(1)] + unfolding univ_poly_carrier_change_def'[OF assms(1)] using polynomial_in_carrier eval_in_carrier eval_poly_add eval_poly_mult assms(2) by (auto intro!: ring_hom_memI simp add: univ_poly_def degree_def simp del: poly_add.simps poly_mult.simps) -theorem (in domain) eval_cring_hom: - assumes "subring K R" and "a \ carrier R" - shows "ring_hom_cring (univ_poly (R \ carrier := K \)) R (\p. (eval p) a)" - unfolding ring_hom_cring_def ring_hom_cring_axioms_def - using domain.axioms(1)[OF univ_poly_subring_is_domain[OF assms(1)]] - eval_is_hom[OF assms] cring_axioms by auto - -corollary (in domain) eval_ring_hom: - assumes "subring K R" and "a \ carrier R" - shows "ring_hom_ring (univ_poly (R \ carrier := K \)) R (\p. (eval p) a)" - using eval_cring_hom[OF assms] ring_hom_ringI2 - unfolding ring_hom_cring_def ring_hom_cring_axioms_def cring_def by auto - - -subsection \The Reduction Map and Uniqueness of The Evaluation Homomorphism\ - -definition (in ring) reduction_map :: "('c \ 'a) \ 'c list \ 'a list" - where "reduction_map h = (\p. normalize (map h p))" - -(* -lemma (in ring_hom_ring) - "(reduction_map h) \ ring_hom (univ_poly R) (univ_poly S)" - sorry -*) - - -subsection \Divisibility of Polynomials\ - -definition pirreducible :: "_ \ 'a list \ bool" - where "pirreducible R p \ irreducible (mult_of (univ_poly R)) p" - -definition pprime :: "_ \ 'a list \ bool" - where "pprime R p \ prime (mult_of (univ_poly R)) p" - -definition rupture :: "_ \ 'a list \ _" - where "rupture R p = (univ_poly R) Quot (PIdl\<^bsub>(univ_poly R)\<^esub> p)" - - -text \Be aware of Nil!\ -lemma (in domain) Nil_is_pirreducible: "pirreducible R []" - unfolding pirreducible_def using poly_mult_integral - by (auto intro!: irreducibleI simp add: Units_def univ_poly_def properfactor_def factor_def, force) - -lemma (in field) pprime_iff_ppirreducible: - assumes "polynomial R p" and "p \ []" - shows "pprime R p \ pirreducible R p" -proof - - have "p \ carrier (mult_of (univ_poly R))" - using assms unfolding univ_poly_def by auto - thus ?thesis - using principal_domain.primeness_condition[OF univ_poly_is_principal[OF field_axioms]] - unfolding pprime_def pirreducible_def by simp -qed - -lemma (in field) rupture_field: - assumes "polynomial R p" and "p \ []" - shows "field (rupture R p) \ pirreducible R p" -proof - - have "p \ carrier (mult_of (univ_poly R))" - using assms(1-2) unfolding univ_poly_def by auto - thus ?thesis - using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF field_axioms]] - pprime_iff_ppirreducible[OF assms] - unfolding pprime_def rupture_def by simp -qed - -lemma (in field) univ_poly_units: - "Units (univ_poly R) = { [ k ] | k. k \ carrier R - { \ } }" -proof - show "Units (univ_poly R) \ { [ k ] | k. k \ carrier R - { \ } }" - proof - fix p assume "p \ Units (univ_poly R)" - then obtain q where p: "polynomial R p" and q: "polynomial R q" and pq: "poly_mult p q = [ \ ]" - unfolding Units_def univ_poly_def by auto - hence not_nil: "p \ []" and "q \ []" - using poly_mult_integral[OF p q] poly_mult_zero[OF p] by auto - hence "degree p = 0" - using poly_mult_degree_eq[OF p q] unfolding pq degree_def by simp - hence "length p = 1" - using not_nil unfolding degree_def by (metis One_nat_def Suc_pred length_greater_0_conv) - then obtain k where k: "p = [ k ]" - by (metis One_nat_def length_0_conv length_Suc_conv) - hence "k \ carrier R - { \ }" - using p unfolding polynomial_def by auto - thus "p \ { [ k ] | k. k \ carrier R - { \ } }" - unfolding k by blast - qed -next - show "{ [ k ] | k. k \ carrier R - { \ } } \ Units (univ_poly R)" - proof (auto) - fix k assume k: "k \ carrier R" "k \ \" - hence inv_k: "inv k \ carrier R" "inv k \ \" and "k \ inv k = \" "inv k \ k = \" - using subfield_m_inv[OF carrier_is_subfield, of k] by auto - hence "poly_mult [ k ] [ inv k ] = [ \ ]" and "poly_mult [ inv k ] [ k ] = [ \ ]" - by (auto simp add: degree_def k) - moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]" - using const_is_polynomial k inv_k by auto - ultimately show "[ k ] \ Units (univ_poly R)" - unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps) - qed -qed - -corollary (in field) univ_poly_not_field: "\ field (univ_poly R)" -proof - - have "[ \, \ ] \ carrier (univ_poly R) - { \\<^bsub>(univ_poly R)\<^esub> }" - and "[ \, \ ] \ { [ k ] | k. k \ carrier R - { \ } }" - unfolding univ_poly_def polynomial_def by auto - thus ?thesis - using field.field_Units[of "univ_poly R"] - unfolding univ_poly_units by blast -qed - -text \A stronger version for one sense of rupture_field lemma.\ -corollary (in field) rupture_field_imp_pirreducible: - assumes "polynomial R p" and "field (rupture R p)" - shows "p \ []" and "pirreducible R p" -proof - - interpret UP: domain "univ_poly R" - using univ_poly_is_domain[OF domain_axioms] . - - show "p \ []" - proof (rule ccontr) - assume "\ p \ []" - hence nil: "p = []" "p = \\<^bsub>(univ_poly R)\<^esub>" - unfolding univ_poly_def by simp+ - hence "rupture R p = (univ_poly R) Quot { \\<^bsub>(univ_poly R)\<^esub> }" - unfolding rupture_def - using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] by simp - hence "rupture R p \ univ_poly R" - using UP.FactRing_zeroideal(1) by simp - then obtain h where h: "h \ ring_iso (rupture R p) (univ_poly R)" - unfolding is_ring_iso_def by blast - moreover have "ring (rupture R p)" - using assms(2) by (simp add: cring_def domain_def field_def) - ultimately interpret ring_hom_ring "rupture R p" "univ_poly R" h - unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def - using UP.is_ring by simp - have "field (univ_poly R)" - using field.ring_iso_imp_img_field[OF assms(2) h] by simp - thus False - using univ_poly_not_field by simp - qed - thus "pirreducible R p" - using rupture_field assms by simp -qed - -lemma (in field) associated_polynomials_iff: - assumes "polynomial R p" and "polynomial R q" - shows "p \\<^bsub>(univ_poly R)\<^esub> q \ (\k \ carrier R - { \ }. p = map (\a. k \ a) q)" -proof - interpret UP: principal_domain "univ_poly R" - using univ_poly_is_principal[OF field_axioms] . - - assume A: "p \\<^bsub>(univ_poly R)\<^esub> q" - then obtain r1 r2 - where r1: "polynomial R r1" "p = poly_mult q r1" - and r2: "polynomial R r2" "q = poly_mult p r2" - unfolding associated_def factor_def univ_poly_def by auto - - show "\k \ carrier R - { \ }. p = map (\a. k \ a) q" - proof (cases "p = []") - assume "p = []" thus ?thesis - using poly_mult_zero[OF r2(1)] r2(2) by auto - next - assume p: "p \ []" hence q: "q \ []" - using poly_mult_zero[OF r1(1)] r1(2) by auto - hence "p \ carrier (mult_of (univ_poly R))" and "q \ carrier (mult_of (univ_poly R))" - using p assms unfolding univ_poly_def by auto - moreover have "p \\<^bsub>mult_of (univ_poly R)\<^esub> q" - using p UP.assoc_imp_assoc_mult[OF _ _ A] assms unfolding univ_poly_def by auto - ultimately obtain r where r: "r \ Units (univ_poly R)" "p = q \\<^bsub>(univ_poly R)\<^esub> r" - using UP.mult_of.associatedD2[of p q] UP.Units_mult_eq_Units by blast - then obtain k where k: "k \ carrier R - { \ }" "r = [ k ]" - using univ_poly_units UP.m_comm[of q r] by auto - moreover have "p = poly_mult r q" - using r UP.m_comm[of q r] q assms unfolding Units_def univ_poly_def by auto - ultimately show ?thesis - using poly_mult_const(1)[OF assms(2) k(1)] unfolding k(2) by auto - qed -next - assume "\k \ carrier R - { \ }. p = map (\a. k \ a) q" - then obtain k where k: "k \ carrier R - { \ }" "p = map (\a. k \ a) q" - by blast - hence inv_k: "inv k \ carrier R - { \ }" "inv k \ k = \" - using subfield_m_inv[OF carrier_is_subfield k(1)] by simp+ - moreover have "map (\a. inv k \ a) (map (\a. k \ a) q) = q" - using inv_k polynomial_in_carrier[OF assms(2)] k(1) m_assoc m_comm by (induct q) (auto) - hence "q = map (\a. inv k \ a) p" - using k(2) by simp - ultimately have "p = poly_mult q [ k ]" and "q = poly_mult p [ inv k ]" - using poly_mult_const(2)[OF assms(2) k(1)] - poly_mult_const(2)[OF assms(1) inv_k(1)] k(2) by auto - moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]" - using const_is_polynomial k inv_k by auto - ultimately show "p \\<^bsub>(univ_poly R)\<^esub> q" - unfolding univ_poly_def associated_def factor_def - by (auto simp del: poly_mult.simps) -qed - -lemma (in cring) ideal_eq_carrier_iff: (* <- Move to Ideal.thy *) - assumes "a \ carrier R" - shows "carrier R = PIdl a \ a \ Units R" -proof - assume "carrier R = PIdl a" - hence "\ \ PIdl a" - by auto - then obtain b where "b \ carrier R" "\ = a \ b" "\ = b \ a" - unfolding cgenideal_def using m_comm[OF assms] by auto - thus "a \ Units R" - using assms unfolding Units_def by auto -next - assume "a \ Units R" - then have inv_a: "inv a \