--- 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>)"