summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson <lp15@cam.ac.uk> |

Mon, 29 Apr 2019 17:11:26 +0100 | |

changeset 70214 | 58191e01f0b1 |

parent 70213 | ff8386fc191d |

child 70215 | 8371a25ca177 |

moving around some material from Algebraic_Closure

--- 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 \<open>Basic Properties\<close> -(* ========== *) -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 \<open>Zorn\<close> -(* ========== *) -lemma Chains_relation_of: - assumes "C \<in> Chains (relation_of P A)" shows "C \<subseteq> A" - using assms unfolding Chains_def relation_of_def by auto -(* ========== *) - lemma (in ring) exists_core_chain: assumes "C \<in> Chains (relation_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> 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 \<in> carrier (K[X])" and "q \<in> carrier (K[X])" - shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> length p = length q" -proof - - { fix p q - assume p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q" - have "length p \<le> length q" - proof (cases "q = []") - case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []" - unfolding associated_def True factor_def univ_poly_def by auto - thus ?thesis - using True by simp - next - case False - from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> 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 \<open>q \<noteq> []\<close> have "degree p \<le> degree q" - using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp - with \<open>q \<noteq> []\<close> 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 \<sim>\<^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 \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q" shows "is_root p x \<longleftrightarrow> 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 \<sim> b'" "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" - shows "a \<otimes> b \<sim> a \<otimes> b'" - by (meson assms associated_def divides_mult_lI) - -lemma (in comm_monoid) mult_cong_l: - assumes "a \<sim> a'" "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" - shows "a \<otimes> b \<sim> a' \<otimes> b" - using assms m_comm mult_cong_r by auto -(* ============================================================= *) - lemma (in field) associated_polynomials_imp_same_roots: assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" shows "roots (p \<otimes>\<^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 \<in> carrier G" - shows "a divides\<^bsub>G\<^esub> r \<Longrightarrow> a \<in> Units G \<or> a \<sim>\<^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:

--- 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 \<open>Multiplication and associativity\<close> -lemma (in monoid_cancel) mult_cong_r: +lemma (in monoid) mult_cong_r: assumes "b \<sim> b'" "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" shows "a \<otimes> b \<sim> a \<otimes> 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 \<sim> a'" "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" shows "a \<otimes> b \<sim> a' \<otimes> 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 \<in> carrier G" + shows "a divides\<^bsub>G\<^esub> r \<Longrightarrow> a \<in> Units G \<or> a \<sim>\<^bsub>G\<^esub> r" + using assms unfolding irreducible_def properfactor_def associated_def + by (cases "r divides\<^bsub>G\<^esub> a", auto) subsubsection \<open>Prime elements\<close>

--- 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 \<in> carrier (K[X])" "q \<in> carrier (K[X])" + assumes "subring K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])" shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> 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 \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q" + have "length p \<le> length q" + proof (cases "q = []") + case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []" + unfolding associated_def True factor_def univ_poly_def by auto + thus ?thesis + using True by simp + next + case False + from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> 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 \<open>q \<noteq> []\<close> have "degree p \<le> degree q" + using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp + with \<open>q \<noteq> []\<close> 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 \<sim>\<^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 \<open>Ideals\<close> @@ -772,6 +797,8 @@ have "\<And>r. \<lbrakk> r \<in> carrier (K[X]); lead_coeff r = \<one>; I = PIdl\<^bsub>K[X]\<^esub> r \<rbrakk> \<Longrightarrow> r = p" proof - fix r assume r: "r \<in> carrier (K[X])" "lead_coeff r = \<one>" "I = PIdl\<^bsub>K[X]\<^esub> r" + have "subring K R" + by (simp add: \<open>subfield K R\<close> subfieldE(1)) obtain k where k: "k \<in> K - { \<zero> }" "r = [ k ] \<otimes>\<^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 \<noteq> []" 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 \<open>subring K R\<close> in_carrier q(1)] by auto ultimately have "lead_coeff r = k \<otimes> (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)

--- 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 \<open>Field would not need to be derived from domain, the properties for domain follow from the assumptions of field\<close> +lemma (in field) is_ring: "ring R" + using ring_axioms . + lemma fieldE : fixes R (structure) assumes "field R"

--- 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 (\<lambda>x y. (x, y) \<in> r) C}" using assms Chains_subset Chains_subset' by blast +lemma Chains_relation_of: + assumes "C \<in> Chains (relation_of P A)" shows "C \<subseteq> A" + using assms unfolding Chains_def relation_of_def by auto + lemma pairwise_chain_Union: assumes P: "\<And>S. S \<in> \<C> \<Longrightarrow> pairwise R S" and "chain\<^sub>\<subseteq> \<C>" shows "pairwise R (\<Union>\<C>)"