# HG changeset patch # User paulson # Date 1556554286 -3600 # Node ID 58191e01f0b13afc56347175854118a0af4ce8f7 # Parent ff8386fc191d026863a78ad85b22fa6286ce48bd moving around some material from Algebraic_Closure diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Algebra/Algebraic_Closure.thy --- a/src/HOL/Algebra/Algebraic_Closure.thy Mon Apr 29 16:50:34 2019 +0100 +++ b/src/HOL/Algebra/Algebraic_Closure.thy Mon Apr 29 17:11:26 2019 +0100 @@ -39,11 +39,6 @@ subsection \Basic Properties\ -(* ========== *) -lemma (in field) is_ring: "ring R" - using ring_axioms . -(* ========== *) - lemma law_restrict_carrier: "carrier (law_restrict R) = carrier R" by (simp add: law_restrict_def ring.defs) @@ -371,12 +366,6 @@ subsection \Zorn\ -(* ========== *) -lemma Chains_relation_of: - assumes "C \ Chains (relation_of P A)" shows "C \ A" - using assms unfolding Chains_def relation_of_def by auto -(* ========== *) - lemma (in ring) exists_core_chain: assumes "C \ Chains (relation_of (\) \)" obtains C' where "C' \ extensions" and "C = law_restrict ` C'" using Chains_relation_of[OF assms] by (meson subset_image_iff) @@ -646,41 +635,6 @@ unfolding is_root_def by simp qed -(* MOVE TO Polynomial_Dvisibility.thy ================== *) -lemma (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *) - assumes "subring K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" - shows "p \\<^bsub>K[X]\<^esub> q \ length p = length q" -proof - - { fix p q - assume p: "p \ carrier (K[X])" and q: "q \ carrier (K[X])" and "p \\<^bsub>K[X]\<^esub> q" - have "length p \ length q" - proof (cases "q = []") - case True with \p \\<^bsub>K[X]\<^esub> q\ have "p = []" - unfolding associated_def True factor_def univ_poly_def by auto - thus ?thesis - using True by simp - next - case False - from \p \\<^bsub>K[X]\<^esub> q\ have "p divides\<^bsub>K [X]\<^esub> q" - unfolding associated_def by simp - hence "p divides\<^bsub>poly_ring R\<^esub> q" - using carrier_polynomial[OF assms(1)] - unfolding factor_def univ_poly_carrier univ_poly_mult by auto - with \q \ []\ have "degree p \ degree q" - using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp - with \q \ []\ show ?thesis - by (cases "p = []", auto simp add: Suc_leI le_diff_iff) - qed - } note aux_lemma = this - - interpret UP: domain "K[X]" - using univ_poly_is_domain[OF assms(1)] . - - assume "p \\<^bsub>K[X]\<^esub> q" thus ?thesis - using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp -qed -(* ================================================= *) - lemma (in domain) associated_polynomials_imp_same_is_root: assumes "p \ carrier (poly_ring R)" and "q \ carrier (poly_ring R)" and "p \\<^bsub>poly_ring R\<^esub> q" shows "is_root p x \ is_root q x" @@ -1454,19 +1408,6 @@ using assms(3)[of a] by auto qed -(* REPLACE th following lemmas on Divisibility.thy ============= *) -(* the only difference is the locale *) -lemma (in monoid) mult_cong_r: - assumes "b \ b'" "a \ carrier G" "b \ carrier G" "b' \ carrier G" - shows "a \ b \ a \ b'" - by (meson assms associated_def divides_mult_lI) - -lemma (in comm_monoid) mult_cong_l: - assumes "a \ a'" "a \ carrier G" "a' \ carrier G" "b \ carrier G" - shows "a \ b \ a' \ b" - using assms m_comm mult_cong_r by auto -(* ============================================================= *) - lemma (in field) associated_polynomials_imp_same_roots: assumes "p \ carrier (poly_ring R)" "p \ []" and "q \ carrier (poly_ring R)" "q \ []" shows "roots (p \\<^bsub>poly_ring R\<^esub> q) = roots p + roots q" @@ -1555,12 +1496,6 @@ qed qed -(* MOVE to Divisibility.thy ======== *) -lemma divides_irreducible_condition: - assumes "irreducible G r" and "a \ carrier G" - shows "a divides\<^bsub>G\<^esub> r \ a \ Units G \ a \\<^bsub>G\<^esub> r" - using assms unfolding irreducible_def properfactor_def associated_def - by (cases "r divides\<^bsub>G\<^esub> a", auto) (* MOVE to Polynomial_Divisibility.thy ======== *) lemma (in ring) divides_pirreducible_condition: diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon Apr 29 16:50:34 2019 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Mon Apr 29 17:11:26 2019 +0100 @@ -398,12 +398,12 @@ subsubsection \Multiplication and associativity\ -lemma (in monoid_cancel) mult_cong_r: +lemma (in monoid) mult_cong_r: assumes "b \ b'" "a \ carrier G" "b \ carrier G" "b' \ carrier G" shows "a \ b \ a \ b'" by (meson assms associated_def divides_mult_lI) -lemma (in comm_monoid_cancel) mult_cong_l: +lemma (in comm_monoid) mult_cong_l: assumes "a \ a'" "a \ carrier G" "a' \ carrier G" "b \ carrier G" shows "a \ b \ a' \ b" using assms m_comm mult_cong_r by auto @@ -723,6 +723,11 @@ qed qed +lemma divides_irreducible_condition: + assumes "irreducible G r" and "a \ carrier G" + shows "a divides\<^bsub>G\<^esub> r \ a \ Units G \ a \\<^bsub>G\<^esub> r" + using assms unfolding irreducible_def properfactor_def associated_def + by (cases "r divides\<^bsub>G\<^esub> a", auto) subsubsection \Prime elements\ diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Algebra/Polynomial_Divisibility.thy --- a/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Apr 29 16:50:34 2019 +0100 +++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Apr 29 17:11:26 2019 +0100 @@ -727,12 +727,37 @@ unfolding univ_poly_units[OF assms(1)] by auto corollary (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *) - assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" + assumes "subring K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" shows "p \\<^bsub>K[X]\<^esub> q \ length p = length q" - unfolding associated_polynomials_iff[OF assms] - using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)],of q] assms(3) - by (auto simp add: univ_poly_carrier univ_poly_mult simp del: poly_mult.simps) +proof - + { fix p q + assume p: "p \ carrier (K[X])" and q: "q \ carrier (K[X])" and "p \\<^bsub>K[X]\<^esub> q" + have "length p \ length q" + proof (cases "q = []") + case True with \p \\<^bsub>K[X]\<^esub> q\ have "p = []" + unfolding associated_def True factor_def univ_poly_def by auto + thus ?thesis + using True by simp + next + case False + from \p \\<^bsub>K[X]\<^esub> q\ have "p divides\<^bsub>K [X]\<^esub> q" + unfolding associated_def by simp + hence "p divides\<^bsub>poly_ring R\<^esub> q" + using carrier_polynomial[OF assms(1)] + unfolding factor_def univ_poly_carrier univ_poly_mult by auto + with \q \ []\ have "degree p \ degree q" + using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp + with \q \ []\ show ?thesis + by (cases "p = []", auto simp add: Suc_leI le_diff_iff) + qed + } note aux_lemma = this + interpret UP: domain "K[X]" + using univ_poly_is_domain[OF assms(1)] . + + assume "p \\<^bsub>K[X]\<^esub> q" thus ?thesis + using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp +qed subsection \Ideals\ @@ -772,6 +797,8 @@ have "\r. \ r \ carrier (K[X]); lead_coeff r = \; I = PIdl\<^bsub>K[X]\<^esub> r \ \ r = p" proof - fix r assume r: "r \ carrier (K[X])" "lead_coeff r = \" "I = PIdl\<^bsub>K[X]\<^esub> r" + have "subring K R" + by (simp add: \subfield K R\ subfieldE(1)) obtain k where k: "k \ K - { \ }" "r = [ k ] \\<^bsub>K[X]\<^esub> p" using UP.associated_iff_same_ideal[OF r(1) in_carrier] PIdl_p r(3) associated_polynomials_iff[OF assms(1) r(1) in_carrier] @@ -780,7 +807,7 @@ unfolding polynomial_def by simp moreover have "p \ []" using not_nil UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) PIdl_p - associated_polynomials_imp_same_length[OF assms(1) in_carrier q(1)] by auto + associated_polynomials_imp_same_length[OF \subring K R\ in_carrier q(1)] by auto ultimately have "lead_coeff r = k \ (lead_coeff p)" using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)]] in_carrier k(2) unfolding univ_poly_def by (auto simp del: poly_mult.simps) diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Mon Apr 29 16:50:34 2019 +0100 +++ b/src/HOL/Algebra/Ring.thy Mon Apr 29 17:11:26 2019 +0100 @@ -643,6 +643,9 @@ text \Field would not need to be derived from domain, the properties for domain follow from the assumptions of field\ +lemma (in field) is_ring: "ring R" + using ring_axioms . + lemma fieldE : fixes R (structure) assumes "field R" diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Zorn.thy --- a/src/HOL/Zorn.thy Mon Apr 29 16:50:34 2019 +0100 +++ b/src/HOL/Zorn.thy Mon Apr 29 17:11:26 2019 +0100 @@ -475,6 +475,10 @@ shows "Chains r = {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}" using assms Chains_subset Chains_subset' by blast +lemma Chains_relation_of: + assumes "C \ Chains (relation_of P A)" shows "C \ A" + using assms unfolding Chains_def relation_of_def by auto + lemma pairwise_chain_Union: assumes P: "\S. S \ \ \ pairwise R S" and "chain\<^sub>\ \" shows "pairwise R (\\)"