--- a/NEWS Mon Apr 29 17:11:26 2019 +0100
+++ b/NEWS Tue Apr 30 11:57:45 2019 +0100
@@ -266,7 +266,7 @@
at the level of abstract topological spaces.
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
-proofs towards algebraic closure by de Vilhena and Baillon.
+ algebraic closure of a field by de Vilhena and Baillon.
* Session HOL-Homology has been added. It is a port of HOL Light's
homology library, with new proofs of "invariance of domain" and related
--- a/src/HOL/Algebra/Algebraic_Closure.thy Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Algebraic_Closure.thy Tue Apr 30 11:57:45 2019 +0100
@@ -61,7 +61,7 @@
lemma (in field) law_restrict_is_field: "field (law_restrict R)"
proof -
have "comm_monoid_axioms (law_restrict R)"
- using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
+ using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
then interpret L: cring "law_restrict R"
using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto
have "Units R = Units (law_restrict R)"
@@ -69,7 +69,7 @@
thus ?thesis
using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp
qed
-
+
lemma law_restrict_iso_imp_eq:
assumes "id \<in> ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B"
shows "law_restrict A = law_restrict B"
@@ -108,33 +108,33 @@
subsection \<open>Partial Order\<close>
-lemma iso_incl_backwards:
+lemma iso_incl_backwards:
assumes "A \<lesssim> B" shows "id \<in> ring_hom A B"
using assms by cases
-lemma iso_incl_antisym_aux:
+lemma iso_incl_antisym_aux:
assumes "A \<lesssim> B" and "B \<lesssim> A" shows "id \<in> ring_iso A B"
-proof -
- have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
+proof -
+ have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
using assms(1-2)[THEN iso_incl_backwards] by auto
- thus ?thesis
+ thus ?thesis
using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def)
qed
-lemma iso_incl_refl: "A \<lesssim> A"
+lemma iso_incl_refl: "A \<lesssim> A"
by (rule iso_inclI[OF ring_hom_memI], auto)
-lemma iso_incl_trans:
+lemma iso_incl_trans:
assumes "A \<lesssim> B" and "B \<lesssim> C" shows "A \<lesssim> C"
using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto
lemma (in ring) iso_incl_antisym:
assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
-proof -
- obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
+proof -
+ obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
using assms(1-2) field.is_ring by (auto simp add: extensions_def)
- thus ?thesis
+ thus ?thesis
using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
qed
@@ -190,7 +190,7 @@
subsection \<open>Chains\<close>
definition union_ring :: "(('a, 'c) ring_scheme) set \<Rightarrow> 'a ring"
- where "union_ring C =
+ where "union_ring C =
\<lparr> carrier = (\<Union>(carrier ` C)),
monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)),
one = one (SOME R. R \<in> C),
@@ -277,7 +277,7 @@
using field_chain by simp
show "a \<otimes>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
- using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
+ using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
show "(a \<otimes>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = a \<otimes>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
and "a \<otimes>\<^bsub>union_ring C\<^esub> b = b \<otimes>\<^bsub>union_ring C\<^esub> a"
and "\<one>\<^bsub>union_ring C\<^esub> \<otimes>\<^bsub>union_ring C\<^esub> a = a"
@@ -286,7 +286,7 @@
next
show "\<one>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1)
- unfolding union_ring_carrier by auto
+ unfolding union_ring_carrier by auto
qed
lemma union_ring_is_abelian_group:
@@ -304,7 +304,7 @@
show "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = (a \<otimes>\<^bsub>union_ring C\<^esub> c) \<oplus>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
and "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<oplus>\<^bsub>union_ring C\<^esub> c = a \<oplus>\<^bsub>union_ring C\<^esub> (b \<oplus>\<^bsub>union_ring C\<^esub> c)"
and "a \<oplus>\<^bsub>union_ring C\<^esub> b = b \<oplus>\<^bsub>union_ring C\<^esub> a"
- and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
+ and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto
have "\<exists>a' \<in> carrier R. a' \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp
@@ -330,7 +330,7 @@
using field_chain by simp
from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> Units R"
- unfolding same_one_same_zero[OF R(1)] field_Units by auto
+ unfolding same_one_same_zero[OF R(1)] field_Units by auto
hence "\<exists>a' \<in> carrier R. a' \<otimes>\<^bsub>union_ring C\<^esub> a = \<one>\<^bsub>union_ring C\<^esub> \<and> a \<otimes>\<^bsub>union_ring C\<^esub> a' = \<one>\<^bsub>union_ring C\<^esub>"
using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto
with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_ring C)"
@@ -457,11 +457,11 @@
hence "set (map h p) \<subseteq> carrier S"
by (induct p) (auto)
moreover have "h a = \<zero>\<^bsub>S\<^esub> \<Longrightarrow> a = \<zero>\<^bsub>R\<^esub>" if "a \<in> carrier R" for a
- using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
+ using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
using lc[OF that] that by (cases p) (auto)
ultimately show ?thesis
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
qed
lemma (in ring_hom_ring) subfield_polynomial_hom:
@@ -482,1147 +482,6 @@
qed
-(* MOVE ========== *)
-subsection \<open>Roots and Multiplicity\<close>
-
-definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
- where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
-
-definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
- where "alg_mult p x =
- (if p = [] then 0 else
- (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
-
-definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
- where "roots p = Abs_multiset (alg_mult p)"
-
-definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
- where "roots_on K p = roots p \<inter># mset_set K"
-
-definition (in ring) splitted :: "'a list \<Rightarrow> bool"
- where "splitted p \<longleftrightarrow> size (roots p) = degree p"
-
-definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
- where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
-
-lemma (in domain) polynomial_pow_not_zero:
- assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
- shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- from assms UP.integral show ?thesis
- unfolding sym[OF univ_poly_zero[of R "carrier R"]]
- by (induction n, auto)
-qed
-
-lemma (in domain) subring_polynomial_pow_not_zero:
- assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
- shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
- using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
- unfolding univ_poly_consistent[OF assms(1)] by simp
-
-lemma (in domain) polynomial_pow_degree:
- assumes "p \<in> carrier (poly_ring R)"
- shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- show ?thesis
- proof (induction n)
- case 0 thus ?case
- using UP.nat_pow_0 unfolding univ_poly_one by auto
- next
- let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
- case (Suc n) thus ?case
- proof (cases "p = []")
- case True thus ?thesis
- using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
- next
- case False
- hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
- using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
- thus ?thesis
- using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
- unfolding univ_poly_carrier univ_poly_zero
- by (auto simp add: add.commute univ_poly_mult)
- qed
- qed
-qed
-
-lemma (in domain) polynomial_pow_division:
- assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
- shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
-
- have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
- using assms(1) by (simp add: UP.nat_pow_mult)
- thus ?thesis
- using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
- unfolding pdivides_def by auto
-qed
-
-lemma (in domain) degree_zero_imp_not_is_root:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
-proof (cases "p = []", simp add: is_root_def)
- case False with \<open>degree p = 0\<close> have "length p = Suc 0"
- using le_SucE by fastforce
- then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
- using assms unfolding sym[OF univ_poly_carrier] polynomial_def
- by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
- thus ?thesis
- unfolding is_root_def by auto
-qed
-
-lemma (in domain) is_root_imp_pdivides:
- assumes "p \<in> carrier (poly_ring R)"
- shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
-proof -
- let ?b = "[ \<one> , \<ominus> x ]"
-
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
- unfolding is_root_def by auto
- hence b: "?b \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
- and long_divides: "p = (?b \<otimes>\<^bsub>poly_ring R\<^esub> q) \<oplus>\<^bsub>poly_ring R\<^esub> r" "r = [] \<or> degree r < degree ?b"
- using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
-
- show ?thesis
- proof (cases "r = []")
- case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
- unfolding univ_poly_zero[of R "carrier R"] .
- thus ?thesis
- using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
- next
- case False then have "length r = Suc 0"
- using long_divides(2) le_SucE by fastforce
- then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
- using r unfolding sym[OF univ_poly_carrier] polynomial_def
- by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
-
- have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
- using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
- also have " ... = eval r x"
- using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
- finally have "a = \<zero>"
- using a unfolding \<open>r = [ a ]\<close> is_root by simp
- with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
- qed
-qed
-
-lemma (in domain) pdivides_imp_is_root:
- assumes "p \<noteq> []" and "x \<in> carrier R"
- shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
-proof -
- assume "[ \<one>, \<ominus> x ] pdivides p"
- then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
- unfolding pdivides_def by auto
- moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
- ultimately have "eval p x = \<zero>"
- using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
- with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
- unfolding is_root_def 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"
-proof (cases "p = []")
- case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
- unfolding associated_def True factor_def univ_poly_def by auto
- thus ?thesis
- using True unfolding is_root_def by simp
-next
- case False
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- { fix p q
- assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
- have "is_root p x \<Longrightarrow> is_root q x"
- proof -
- assume is_root: "is_root p x"
- then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
- using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
- moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
- ultimately have "[ \<one>, \<ominus> x ] pdivides q"
- using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
- with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
- using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
- pdivides_imp_is_root[of q x]
- by fastforce
- qed
- }
-
- then show ?thesis
- using assms UP.associated_sym[OF assms(3)] by blast
-qed
-
-lemma (in ring) monic_degree_one_root_condition:
- assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
- using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
-
-lemma (in field) degree_one_root_condition:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
- shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
- by simp
- then obtain a b where p: "p = [ a, b ]"
- by (metis length_0_conv length_Cons list.exhaust nat.inject)
- hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
- using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
- using subfield_m_inv[OF carrier_is_subfield, of a] by auto
- hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
- using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-
- have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
- proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
- have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
- using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
- also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
- using UP.m_comm[OF in_carrier, of "[ a ]"] a
- by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
- finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
- next
- from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
- unfolding univ_poly_units[OF carrier_is_subfield] by simp
- qed
-
- moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
- and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
- using inv_a a b unfolding p const_term_def by auto
-
- ultimately show ?thesis
- using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
- monic_degree_one_root_condition
- by (metis add.inv_closed)
-qed
-
-lemma (in domain) is_root_imp_is_root_poly_mult:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "q \<noteq> []"
- shows "is_root p x \<Longrightarrow> is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- assume "is_root p x" then have x: "x \<in> carrier R" and eval: "eval p x = \<zero>" and not_zero: "p \<noteq> []"
- unfolding is_root_def by simp+
- hence "p \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
- using assms UP.integral unfolding sym[OF univ_poly_zero[of R "carrier R"]] by blast
- moreover have "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
- using assms eval ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by auto
- ultimately show ?thesis
- using x unfolding is_root_def by simp
-qed
-
-lemma (in domain) is_root_poly_mult_imp_is_root:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
- shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
- hence "p \<noteq> []" and "q \<noteq> []"
- unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
- using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
- moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
- using is_root unfolding is_root_def by simp+
- hence "eval p x = \<zero> \<or> eval q x = \<zero>"
- using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
- ultimately show "(is_root p x) \<or> (is_root q x)"
- using x unfolding is_root_def by auto
-qed
-
-(*
-lemma (in domain)
- assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
- shows "pprime K p"
-proof (rule pprimeI[OF assms(1-2)])
- from \<open>degree p = 1\<close> show "p \<noteq> []" and "p \<notin> Units (K [X])"
- unfolding univ_poly_units[OF assms(1)] by auto
-next
- fix q r
- assume "q \<in> carrier (K[X])" and "r \<in> carrier (K[X])"
- and pdiv: "p pdivides q \<otimes>\<^bsub>K [X]\<^esub> r"
- hence "q \<in> carrier (poly_ring R)" and "r \<in> carrier (poly_ring R)"
- using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
- moreover obtain b where b: "b \<in>"
-qed
-*)
-
-lemma (in domain) finite_number_of_roots:
- assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
- using assms
-proof (induction "degree p" arbitrary: p)
- case 0 thus ?case
- by (simp add: degree_zero_imp_not_is_root)
-next
- case (Suc n) show ?case
- proof (cases "{ x. is_root p x } = {}")
- case True thus ?thesis
- by (simp add: True)
- next
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- case False
- then obtain a where is_root: "is_root p a"
- by blast
- hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
- unfolding is_root_def by auto
- hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-
- obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
- using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
- with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
- using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
- by metis
- hence "degree q = n"
- using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
- in_carrier q p_not_zero p Suc(2)
- unfolding univ_poly_carrier
- by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
- list.size(3-4) plus_1_eq_Suc univ_poly_mult)
- hence "finite { x. is_root q x }"
- using Suc(1)[OF _ q] by simp
-
- moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
- using is_root_poly_mult_imp_is_root[OF in_carrier q]
- monic_degree_one_root_condition[OF a]
- unfolding p by auto
-
- ultimately show ?thesis
- using finite_subset by auto
- qed
-qed
-
-lemma (in domain) alg_multE:
- assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
- shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
- and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
-
- define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
- have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
- using UP.nat_pow_0 by simp
- hence "0 \<in> S"
- using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
- hence "S \<noteq> {}"
- by auto
-
- moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
- proof -
- have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence "?ppow n \<in> carrier (poly_ring R)"
- using assms unfolding univ_poly_zero by auto
- with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
- using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
- with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
- using polynomial_pow_degree by simp
- qed
- hence "finite S"
- using finite_nat_set_iff_bounded_le by blast
-
- ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
- using Max_ge[of S] Max_in[of S] by auto
- with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
- using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
- unfolding S_def alg_mult_def by auto
- thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
- and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
- using MaxS unfolding S_def by auto
-qed
-
-lemma (in domain) le_alg_mult_imp_pdivides:
- assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
- shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- assume le_alg_mult: "n \<le> alg_mult p x"
- have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence ppow_pdivides:
- "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
- ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
- using polynomial_pow_division[OF _ le_alg_mult] by simp
-
- show ?thesis
- proof (cases "p = []")
- case True thus ?thesis
- using in_carrier pdivides_zero[OF carrier_is_subring] by auto
- next
- case False thus ?thesis
- using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
- unfolding pdivides_def by meson
- qed
-qed
-
-lemma (in domain) alg_mult_gt_zero_iff_is_root:
- assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
- show ?thesis
- proof
- assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
- unfolding is_root_def by auto
- have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
- using x unfolding univ_poly_def by auto
- thus "alg_mult p x > 0"
- using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
- next
- assume gt_zero: "alg_mult p x > 0"
- hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
- unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
- hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
- using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
- thus "is_root p x"
- using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
- qed
-qed
-
-lemma (in domain) alg_mult_in_multiset:
- assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p \<in> multiset"
- using assms alg_mult_gt_zero_iff_is_root finite_number_of_roots unfolding multiset_def by auto
-
-lemma (in domain) alg_mult_eq_count_roots:
- assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
- using alg_mult_in_multiset[OF assms] by (simp add: roots_def)
-
-lemma (in domain) roots_mem_iff_is_root:
- assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
- using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
- unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
-
-lemma (in domain) degree_zero_imp_empty_roots:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
-proof -
- have "alg_mult p = (\<lambda>x. 0)"
- proof (cases "p = []")
- case True thus ?thesis
- using assms unfolding alg_mult_def by auto
- next
- case False hence "length p = Suc 0"
- using assms(2) by (simp add: le_Suc_eq)
- then obtain a where "a \<in> carrier R" and "a \<noteq> \<zero>" and p: "p = [ a ]"
- using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def
- by (metis Suc_length_conv hd_in_set length_0_conv list.sel(1) subset_code(1))
- show ?thesis
- proof (rule ccontr)
- assume "alg_mult p \<noteq> (\<lambda>x. 0)"
- then obtain x where "alg_mult p x > 0"
- by auto
- with \<open>p \<noteq> []\<close> have "eval p x = \<zero>"
- using alg_mult_gt_zero_iff_is_root[OF assms(1), of x] unfolding is_root_def by simp
- with \<open>a \<in> carrier R\<close> have "a = \<zero>"
- unfolding p by auto
- with \<open>a \<noteq> \<zero>\<close> show False ..
- qed
- qed
- thus ?thesis
- by (simp add: roots_def zero_multiset.abs_eq)
-qed
-
-lemma (in domain) degree_zero_imp_splitted:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
- unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
-
-lemma (in domain) roots_inclI':
- assumes "p \<in> carrier (poly_ring R)" and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> alg_mult p a \<le> count m a"
- shows "roots p \<subseteq># m"
-proof (intro mset_subset_eqI)
- fix a show "count (roots p) a \<le> count m a"
- using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
- by (cases "p = []", simp, cases "a \<in> carrier R", auto)
-qed
-
-lemma (in domain) roots_inclI:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
- and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
- shows "roots p \<subseteq># roots q"
- using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
- unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
-
-lemma (in domain) pdivides_imp_roots_incl:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
- shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
-proof (rule roots_inclI[OF assms])
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- fix a assume "p pdivides q" and a: "a \<in> carrier R"
- hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by simp
- with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
- using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
- by (auto simp add: pdivides_def)
-qed
-
-lemma (in domain) associated_polynomials_imp_same_roots:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
- shows "roots p = roots q"
- using assms pdivides_imp_roots_incl zero_pdivides
- unfolding pdivides_def associated_def
- by (metis subset_mset.eq_iff)
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in comm_monoid_cancel) prime_pow_divides_iff:
- assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
- shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
-proof
- assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
- using divides_prod_l[of "p [^] n" b a] assms by simp
-next
- assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
- proof (induction n)
- case 0 with \<open>b \<in> carrier G\<close> show ?case
- by (simp add: unit_divides)
- next
- case (Suc n)
- hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
- using assms(1) divides_prod_r by auto
- with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
- where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
- and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
- using assms by blast
- hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
- using assms by (simp add: m_assoc m_lcomm)
- hence "a \<otimes> c = p \<otimes> d"
- using c d assms(1) assms(2) l_cancel by blast
- with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
- by (metis assms(2) c d dividesI' prime_divides)
- with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
- using assms(1) c by simp
- qed
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) pirreducible_pow_pdivides_iff:
- assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
- and "pirreducible K p" and "\<not> (p pdivides q)"
- shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<longleftrightarrow> (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
-proof -
- interpret UP: principal_domain "K[X]"
- using univ_poly_is_principal[OF assms(1)] .
- show ?thesis
- proof (cases "r = []")
- case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
- unfolding sym[OF univ_poly_zero[of R K]] by auto
- thus ?thesis
- using pdivides_zero[OF subfieldE(1),of K] assms by auto
- next
- case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
- using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
- UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
- from \<open>p \<noteq> []\<close>
- have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
- using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
- have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
- using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
- have prime: "prime (mult_of (K[X])) p"
- using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
- unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
- have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
- if "a \<in> carrier (K[X])" "a \<noteq> \<zero>\<^bsub>K[X]\<^esub>" "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>" for a b
- using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
- unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
- thus ?thesis
- using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
- unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
- by (metis DiffI UP.m_closed singletonD)
- qed
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) univ_poly_units':
- assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
- unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
- by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) subring_degree_one_imp_pirreducible:
- assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
- shows "pirreducible K [ a, b ]"
-proof (rule pirreducibleI[OF assms(1)])
- have "a \<in> K" and "a \<noteq> \<zero>"
- using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
- thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
- using univ_poly_units_incl[OF assms(1)] assms(2-3)
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-next
- interpret UP: domain "K[X]"
- using univ_poly_is_domain[OF assms(1)] .
-
- { fix q r
- assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
- hence not_zero: "q \<noteq> []" "r \<noteq> []"
- by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
- have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
- using not_zero poly_mult_degree_eq[OF assms(1)] q r
- by (simp add: univ_poly_carrier univ_poly_mult)
- with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
- using not_zero by auto
- } note aux_lemma1 = this
-
- { fix q r
- assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
- and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
- hence "length q = Suc (Suc 0)" and "length r = Suc 0"
- by (linarith, metis add.right_neutral add_eq_if length_0_conv)
- from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
- by (metis length_0_conv length_Cons list.exhaust nat.inject)
- from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
- by (metis length_0_conv length_Suc_conv)
- from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
- have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
- using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
- using poly_mult_lead_coeff[OF assms(1), of q r]
- unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
- obtain inv_a where a: "a \<in> K" and inv_a: "inv_a \<in> K" "a \<otimes> inv_a = \<one>" "inv_a \<otimes> a = \<one>"
- using assms(2) unfolding Units_def by auto
- hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
- using subringE(1)[OF assms(1)] integral_iff by auto
- with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
- using subringE(1,6)[OF assms(1)] inv_a integral
- unfolding sym[OF univ_poly_carrier] polynomial_def
- by (auto, meson subsetD)
- moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
- using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
- unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
- ultimately have "r \<in> Units (K[X])"
- using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
- } note aux_lemma2 = this
-
- fix q r
- assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
- thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
- using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) degree_one_imp_pirreducible:
- assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
- shows "pirreducible K p"
-proof -
- from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
- by simp
- then obtain a b where p: "p = [ a, b ]"
- by (metis length_0_conv length_Suc_conv)
- with \<open>p \<in> carrier (K[X])\<close> show ?thesis
- using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
- subfield.subfield_Units[OF assms(1)]
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in ring) degree_oneE[elim]:
- assumes "p \<in> carrier (K[X])" and "degree p = 1"
- and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
- shows P
-proof -
- from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
- by simp
- then obtain a b where "p = [ a, b ]"
- by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
- with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- with \<open>p = [ a, b ]\<close> show ?thesis
- using assms(3) by simp
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) subring_degree_one_associatedI:
- assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
- shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
-proof -
- from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
- using subringE(1)[OF assms(1)] assms(2-3) by auto
- hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
- using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
- unfolding univ_poly_mult by fastforce
- moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
- using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- moreover have "[ a ] \<in> Units (K[X])"
- proof -
- from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
- using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- moreover have "a' \<otimes> a = \<one>"
- using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
- hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
- using assms unfolding univ_poly_mult by auto
- ultimately show ?thesis
- unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
- qed
- ultimately show ?thesis
- using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) degree_one_associatedI:
- assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
- shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
-proof -
- from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
- obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
- by auto
- thus ?thesis
- using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
- subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
- unfolding const_term_def
- by auto
-qed
-
-lemma (in domain) monic_degree_one_roots:
- assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
-proof -
- let ?p = "[ \<one> , \<ominus> a ]"
-
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by simp
- show ?thesis
- proof (rule subset_mset.antisym)
- show "{# a #} \<subseteq># roots ?p"
- using roots_mem_iff_is_root[OF in_carrier]
- monic_degree_one_root_condition[OF assms]
- by simp
- next
- show "roots ?p \<subseteq># {# a #}"
- proof (rule mset_subset_eqI, auto)
- fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
- using alg_mult_gt_zero_iff_is_root[OF in_carrier]
- monic_degree_one_root_condition[OF assms]
- unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
- by fastforce
- next
- have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
- using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
- hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
- using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
- thus "count (roots ?p) a \<le> Suc 0"
- using polynomial_pow_degree[OF in_carrier]
- unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
- by auto
- qed
- qed
-qed
-
-lemma (in domain) degree_one_roots:
- assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
- shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
-proof -
- have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
- using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- thus ?thesis
- using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
- monic_degree_one_roots associated_polynomials_imp_same_roots
- by (metis add.inv_closed local.minus_minus m_closed)
-qed
-
-lemma (in field) degree_one_imp_singleton_roots:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
- shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
-proof -
- from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
- obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
- by auto
- thus ?thesis
- using degree_one_roots[of a "inv a" b]
- by (auto simp add: const_term_def field_Units)
-qed
-
-lemma (in field) degree_one_imp_splitted:
- assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
- using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
-
-lemma (in field) no_roots_imp_same_roots:
- assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
- shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
- proof (intro subset_mset.antisym)
- have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
- using UP.divides_prod_l assms unfolding pdivides_def by blast
- show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
- using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
- degree_zero_imp_empty_roots[OF assms(3)]
- by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
- next
- show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
- proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
- case True thus ?thesis
- using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
- next
- case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
- by (metis UP.r_null assms(1) univ_poly_zero)
- show ?thesis
- proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
- fix a assume a: "a \<in> carrier R"
- hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
- using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
- moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
- using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
- moreover
- have "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
- using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
- ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
- using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
- qed
- qed
- qed
-qed
-
-lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
- assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
- shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-
- show ?thesis
- proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
- show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
- using in_carrier assms(2) by simp
- next
- fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
- hence not_zero: "p \<noteq> []"
- unfolding univ_poly_def by auto
- from \<open>b \<in> carrier R\<close> have in_carrier': "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
- unfolding sym[OF univ_poly_carrier] polynomial_def by simp
- show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
- proof (cases "a = b")
- case False
- hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
- using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
- moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
- using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
- ultimately
- have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
- using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
- pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
- by auto
- with \<open>a \<noteq> b\<close> show ?thesis
- using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
- next
- case True
- have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
- using dividesI[OF assms(2)] unfolding pdivides_def by auto
- with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
- have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
- using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
- then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
- using Suc_le_D by blast
- hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
- ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
- using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
- in_carrier assms UP.nat_pow_Suc2 by force
- hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
- using UP.mult_divides in_carrier assms(2)
- unfolding univ_poly_zero pdivides_def factor_def
- by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
- with \<open>a = b\<close> show ?thesis
- using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
- alg_multE(2)[OF assms(1) _ not_zero] m
- by auto
- qed
- next
- fix b
- have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
- using assms in_carrier univ_poly_zero[of R] UP.integral by auto
-
- show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
- proof (cases "a = b")
- case True
- have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
- ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
- using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
- by (auto simp add: pdivides_def)
- with \<open>a = b\<close> show ?thesis
- using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
- alg_multE(2)[OF assms(1) _ not_zero]
- by auto
- next
- case False
- have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
- using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
- thus ?thesis
- using False pdivides_imp_roots_incl assms in_carrier not_zero
- by (simp add: subseteq_mset_def)
- qed
- qed
-qed
-
-lemma (in domain) not_empty_rootsE[elim]:
- assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
- and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
- [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
- shows P
-proof -
- from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
- by blast
- with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
- and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
- using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
- unfolding sym[OF univ_poly_carrier] polynomial_def by auto
- with \<open>a \<in># roots p\<close> show ?thesis
- using assms(3)[of a] by auto
-qed
-
-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"
-proof -
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
- from assms show ?thesis
- proof (induction "degree p" arbitrary: p rule: less_induct)
- case less show ?case
- proof (cases "roots p = {#}")
- case True thus ?thesis
- using no_roots_imp_same_roots[of p q] less by simp
- next
- case False with \<open>p \<in> carrier (poly_ring R)\<close>
- obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
- and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- by blast
- show ?thesis
- proof (cases "degree p = 1")
- case True with \<open>p \<in> carrier (poly_ring R)\<close>
- obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
- by auto
- with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
- and lead: "lead_coeff p = b" and const: "const_term p = c"
- using degree_one_imp_singleton_roots[of p] less(2) field_Units
- unfolding const_term_def by auto
- hence "(p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<sim>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
- using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
- by (auto simp add: a lead const)
- hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
- using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
- thus ?thesis
- unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
- next
- case False
- from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
- obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
- unfolding pdivides_def by auto
- with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
- using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
- with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
- using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
- unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
- with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
- using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
- hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
- using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
- UP.m_assoc[OF in_carrier r less(4)] p by auto
- also have " ... = add_mset a (roots r + roots q)"
- using less(1)[OF _ r not_zero less(4-5)] deg by simp
- also have " ... = (add_mset a (roots r)) + roots q"
- by simp
- also have " ... = roots p + roots q"
- using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
- finally show ?thesis .
- qed
- qed
- qed
-qed
-
-lemma (in field) size_roots_le_degree:
- assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
- using assms
-proof (induction "degree p" arbitrary: p rule: less_induct)
- case less show ?case
- proof (cases "roots p = {#}", simp)
- interpret UP: domain "poly_ring R"
- using univ_poly_is_domain[OF carrier_is_subring] .
-
- case False with \<open>p \<in> carrier (poly_ring R)\<close>
- obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
- and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- by blast
- then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
- unfolding pdivides_def by auto
- with \<open>a \<in># roots p\<close> have "p \<noteq> []"
- using degree_zero_imp_empty_roots[OF less(2)] by auto
- hence not_zero: "q \<noteq> []"
- using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
- hence "degree p = Suc (degree q)"
- using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
- unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
- with \<open>q \<noteq> []\<close> show ?thesis
- using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
- by (metis Suc_le_mono lessI size_add_mset)
- qed
-qed
-
-
-(* MOVE to Polynomial_Divisibility.thy ======== *)
-lemma (in ring) divides_pirreducible_condition:
- assumes "pirreducible K q" and "p \<in> carrier (K[X])"
- shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
- using divides_irreducible_condition[of "K[X]" q p] assms
- unfolding ring_irreducible_def by auto
-
-lemma (in domain) pirreducible_roots:
- assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
- shows "roots p = {#}"
-proof (rule ccontr)
- assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
- obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
- and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- by blast
- hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
- using divides_pirreducible_condition[OF assms(2) in_carrier]
- univ_poly_units_incl[OF carrier_is_subring]
- unfolding pdivides_def by auto
- hence "degree p = 1"
- using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
- with \<open>degree p \<noteq> 1\<close> show False ..
-qed
-
-lemma (in field) pirreducible_imp_not_splitted:
- assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
- shows "\<not> splitted p"
- using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
- by (simp add: splitted_def)
-
-lemma (in field)
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
- and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
- shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
- using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
- unfolding ring_irreducible_def univ_poly_zero by auto
-
-lemma (in field) trivial_factors_imp_splitted:
- assumes "p \<in> carrier (poly_ring R)"
- and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
- shows "splitted p"
- using assms
-proof (induction "degree p" arbitrary: p rule: less_induct)
- interpret UP: principal_domain "poly_ring R"
- using univ_poly_is_principal[OF carrier_is_subfield] .
- case less show ?case
- proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
- case False show ?thesis
- proof (cases "roots p = {#}")
- case True
- from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
- using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
- then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
- using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
- with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
- using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
- pdivides_imp_roots_incl[OF _ less(2), of q]
- pirreducible_degree[OF carrier_is_subfield, of q]
- by force
- from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
- by simp
- thus ?thesis ..
- next
- case False with \<open>p \<in> carrier (poly_ring R)\<close>
- obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
- and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
- by blast
- then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
- unfolding pdivides_def by blast
- with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
- by auto
- with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
- using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
- with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> and \<open>p \<noteq> []\<close> have "degree p = Suc (degree q)"
- using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
- unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
- moreover have "q pdivides p"
- using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
- hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
- and "r pdivides q" for r
- using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
- pirreducible_degree[OF carrier_is_subfield that(1-2)]
- by (auto simp add: pdivides_def)
- ultimately have "splitted q"
- using less(1)[OF _ q] by auto
- with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
- using poly_mult_degree_one_monic_imp_same_roots[OF a q]
- unfolding sym[OF p] splitted_def
- by simp
- qed
- qed
-qed
-
-lemma (in field) pdivides_imp_splitted:
- assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
- shows "p pdivides q \<Longrightarrow> splitted p"
-proof (cases "p = []")
- case True thus ?thesis
- using degree_zero_imp_splitted[OF assms(1)] by simp
-next
- interpret UP: principal_domain "poly_ring R"
- using univ_poly_is_principal[OF carrier_is_subfield] .
-
- case False
- assume "p pdivides q"
- then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
- unfolding pdivides_def by auto
- with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
- using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
- hence "degree p + degree b = size (roots p) + size (roots b)"
- using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
- poly_mult_degree_eq[OF carrier_is_subring,of p b]
- unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
- by auto
- moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
- using size_roots_le_degree assms(1) b by auto
- ultimately show ?thesis
- unfolding splitted_def by linarith
-qed
-
-lemma (in field) splitted_imp_trivial_factors:
- assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
- shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
- using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
- by auto
-
lemma (in field) exists_root:
assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
and "P \<in> carrier (poly_ring R)"
@@ -1664,7 +523,7 @@
qed
then obtain i :: nat where "\<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
by blast
-
+
then have hyps:
\<comment> \<open>i\<close> "field M"
\<comment> \<open>ii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
@@ -1760,7 +619,7 @@
obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
using exists_maximal_extension iso_incl_hom by blast
thus ?thesis
- using exists_root[of M] by auto
+ using exists_root[of M] by auto
qed
@@ -1773,9 +632,9 @@
locale algebraically_closed = field L for L (structure) +
assumes roots_over_carrier: "P \<in> carrier (poly_ring L) \<Longrightarrow> splitted P"
-definition (in field) closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
- where "closure = (SOME L \<comment> \<open>such that\<close>.
- \<comment> \<open>i\<close> algebraic_closure L (indexed_const ` (carrier R)) \<and>
+definition (in field) alg_closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
+ where "alg_closure = (SOME L \<comment> \<open>such that\<close>.
+ \<comment> \<open>i\<close> algebraic_closure L (indexed_const ` (carrier R)) \<and>
\<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"
lemma algebraic_hom:
@@ -1961,7 +820,7 @@
with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
have "degree R = 1"
using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
- Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
+ Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
thus ?thesis
by simp
qed
@@ -1978,11 +837,26 @@
using that by auto
qed
-lemma (in field) closureE:
- shows "algebraic_closure \<Omega> (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R \<Omega>"
- using exists_closure unfolding closure_def
+lemma (in field) alg_closureE:
+ shows "algebraic_closure alg_closure (indexed_const ` (carrier R))"
+ and "indexed_const \<in> ring_hom R alg_closure"
+ using exists_closure unfolding alg_closure_def
by (metis (mono_tags, lifting) someI2)+
+lemma (in field) algebraically_closedI':
+ assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> splitted p"
+ shows "algebraically_closed R"
+proof
+ fix p assume "p \<in> carrier (poly_ring R)" show "splitted p"
+ proof (cases "degree p \<le> 1")
+ case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+ using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+ using assms by fastforce
+ qed
+qed
+
lemma (in field) algebraically_closedI:
assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier R. eval p x = \<zero>"
shows "algebraically_closed R"
@@ -2014,13 +888,13 @@
moreover have "roots p = add_mset a (roots q)"
using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp
ultimately show ?thesis
- unfolding splitted_def deg by simp
+ unfolding splitted_def deg by simp
qed
qed
qed
sublocale algebraic_closure \<subseteq> algebraically_closed
-proof (rule algebraically_closedI)
+proof (rule algebraically_closedI')
fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_one: "degree P > 1"
then have gt_zero: "degree P > 0"
by simp
@@ -2074,11 +948,11 @@
univ_poly_subfield_of_consts[OF subfield_axioms] by auto
moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
- using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
+ using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
ultimately
have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
- using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
+ using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
proof (intro Rupt.telescopic_base_dim(1)[where
@@ -2113,7 +987,7 @@
ultimately
have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
- using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
+ using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
@@ -2129,14 +1003,11 @@
unfolding cgenideal_def by blast
with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q"
using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp
- hence "splitted P"
+ thus "splitted P"
using pdivides_imp_splitted[OF in_carrier
carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2)
- roots_over_subfield[OF Q(1)]] Q by simp
- with \<open>degree P > 1\<close> obtain a where "a \<in># roots P"
- unfolding splitted_def by force
- thus "\<exists>x\<in>carrier L. eval P x = \<zero>"
- unfolding roots_mem_iff_is_root[OF in_carrier] is_root_def by blast
+ roots_over_subfield[OF Q(1)]] Q
+ by simp
qed
end
--- a/src/HOL/Algebra/Divisibility.thy Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Tue Apr 30 11:57:45 2019 +0100
@@ -780,6 +780,36 @@
using A(1) Units_one_closed b'(1) unit_factor by presburger
qed
+lemma (in comm_monoid_cancel) prime_pow_divides_iff:
+ assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
+ shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
+proof
+ assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
+ using divides_prod_l[of "p [^] n" b a] assms by simp
+next
+ assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
+ proof (induction n)
+ case 0 with \<open>b \<in> carrier G\<close> show ?case
+ by (simp add: unit_divides)
+ next
+ case (Suc n)
+ hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
+ using assms(1) divides_prod_r by auto
+ with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
+ where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
+ and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
+ using assms by blast
+ hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
+ using assms by (simp add: m_assoc m_lcomm)
+ hence "a \<otimes> c = p \<otimes> d"
+ using c d assms(1) assms(2) l_cancel by blast
+ with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
+ by (metis assms(2) c d dividesI' prime_divides)
+ with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
+ using assms(1) c by simp
+ qed
+qed
+
subsection \<open>Factorization and Factorial Monoids\<close>
--- a/src/HOL/Algebra/Finite_Extensions.thy Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Finite_Extensions.thy Tue Apr 30 11:57:45 2019 +0100
@@ -293,8 +293,11 @@
using assms(1) lin(2) unfolding polynomial_def by auto
hence "eval (normalize (p @ [ k2 ])) x = k1 \<otimes> x \<oplus> k2"
using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto
- thus ?case
- using normalize_gives_polynomial[of "p @ [ k2 ]"] polynomial_incl[OF p(2)] lin(2)
+ moreover have "set (p @ [k2]) \<subseteq> K"
+ using polynomial_incl[OF p(2)] \<open>k2 \<in> K\<close> by auto
+ then have "local.normalize (p @ [k2]) \<in> carrier (K [X])"
+ using normalize_gives_polynomial univ_poly_carrier by blast
+ ultimately show ?case
unfolding univ_poly_carrier by force
qed
qed
@@ -720,91 +723,4 @@
qed
qed
-
-(*
-proposition (in domain) finite_extension_is_subfield:
- assumes "subfield K R" "set xs \<subseteq> carrier R"
- shows "subfield (finite_extension K xs) R \<longleftrightarrow> (algebraic_set over K) (set xs)"
-proof
- have "(\<And>x. x \<in> set xs \<Longrightarrow> (algebraic over K) x) \<Longrightarrow> subfield (finite_extension K xs) R"
- using simple_extension_is_subfield algebraic_mono assms
- by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1))
- thus "(algebraic_set over K) (set xs) \<Longrightarrow> subfield (finite_extension K xs) R"
- unfolding algebraic_set_def over_def by auto
-next
- { fix x xs
- assume x: "x \<in> carrier R" and xs: "set xs \<subseteq> carrier R"
- and is_subfield: "subfield (finite_extension K (x # xs)) R"
- hence "(algebraic over K) x" sorry }
-
- assume "subfield (finite_extension K xs) R" thus "(algebraic_set over K) (set xs)"
- using assms(2)
- proof (induct xs)
- case Nil thus ?case
- unfolding algebraic_set_def over_def by simp
- next
- case (Cons x xs)
- have "(algebraic over K) x"
- using simple_extension_subfield_imp_algebraic[OF
- finite_extension_is_subring[of K xs], of x]
-
- then show ?case sorry
- qed
-qed
-*)
-
-(*
-lemma (in ring) transcendental_imp_trivial_ker:
- assumes "x \<in> carrier R"
- shows "(transcendental over K) x \<Longrightarrow> (\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = [])"
-proof -
- fix p assume "(transcendental over K) x" "polynomial R p" "eval p x = \<zero>" "set p \<subseteq> K"
- moreover have "eval [] x = \<zero>" and "polynomial R []"
- using assms zero_is_polynomial by auto
- ultimately show "p = []"
- unfolding over_def transcendental_def inj_on_def by auto
-qed
-
-lemma (in domain) trivial_ker_imp_transcendental:
- assumes "subring K R" and "x \<in> carrier R"
- shows "(\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []) \<Longrightarrow> (transcendental over K) x"
-proof -
- assume "\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []"
- hence "a_kernel (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. local.eval p x) = { [] }"
- unfolding a_kernel_def' univ_poly_subring_def'[OF assms(1)] by auto
- moreover have "[] = \<zero>\<^bsub>(univ_poly (R \<lparr> carrier := K \<rparr>))\<^esub>"
- unfolding univ_poly_def by auto
- ultimately have "inj_on (\<lambda>p. local.eval p x) (carrier (univ_poly (R \<lparr> carrier := K \<rparr>)))"
- using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] by auto
- thus "(transcendental over K) x"
- unfolding over_def transcendental_def univ_poly_subring_def'[OF assms(1)] by simp
-qed
-
-lemma (in ring) non_trivial_ker_imp_algebraic:
- assumes "x \<in> carrier R"
- and "p \<noteq> []" "polynomial R p" "set p \<subseteq> K" "eval p x = \<zero>"
- shows "(algebraic over K) x"
- using transcendental_imp_trivial_ker[OF assms(1) _ assms(3-5)] assms(2)
- unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_imp_non_trivial_ker:
- assumes "subring K R" "x \<in> carrier R"
- shows "(algebraic over K) x \<Longrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
- using trivial_ker_imp_transcendental[OF assms]
- unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_iff:
- assumes "subring K R" "x \<in> carrier R"
- shows "(algebraic over K) x \<longleftrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
- using non_trivial_ker_imp_algebraic[OF assms(2)] algebraic_imp_non_trivial_ker[OF assms] by auto
-*)
-
-
-(*
-lemma (in field)
- assumes "subfield K R"
- shows "subfield (simple_extension K x) R \<longleftrightarrow> (algebraic over K) x"
- sorry
-
-*)
end
\ No newline at end of file
--- a/src/HOL/Algebra/Ideal.thy Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Ideal.thy Tue Apr 30 11:57:45 2019 +0100
@@ -193,7 +193,7 @@
qed
-subsection \<open>General Ideal Properies\<close>
+subsection \<open>General Ideal Properties\<close>
lemma (in ideal) one_imp_carrier:
assumes I_one_closed: "\<one> \<in> I"
@@ -210,6 +210,30 @@
shows "i \<in> carrier R"
using iI by (rule a_Hcarr)
+lemma (in ring) quotient_eq_iff_same_a_r_cos:
+ assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
+ shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
+proof
+ assume "I +> a = I +> b"
+ then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
+ unfolding a_r_coset_def' by blast
+ hence "a \<ominus> b = i"
+ using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
+ with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
+ by simp
+next
+ assume "a \<ominus> b \<in> I"
+ then obtain i where "i \<in> I" and "a = i \<oplus> b"
+ using ideal.Icarr[OF assms(1)] assms(2-3)
+ by (metis a_minus_def add.inv_solve_right)
+ hence "I +> a = (I +> i) +> b"
+ using ideal.Icarr[OF assms(1)] assms(3)
+ by (simp add: a_coset_add_assoc subsetI)
+ with \<open>i \<in> I\<close> show "I +> a = I +> b"
+ using a_rcos_zero[OF assms(1)] by simp
+qed
+
subsection \<open>Intersection of Ideals\<close>
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Tue Apr 30 11:57:45 2019 +0100
@@ -122,6 +122,11 @@
using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto
+lemma (in domain) univ_poly_units':
+ assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
+ unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
+ by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
+
corollary (in domain) rupture_one_not_zero:
assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p > 0"
shows "\<one>\<^bsub>Rupt K p\<^esub> \<noteq> \<zero>\<^bsub>Rupt K p\<^esub>"
@@ -759,6 +764,255 @@
using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
qed
+lemma (in ring) divides_pirreducible_condition:
+ assumes "pirreducible K q" and "p \<in> carrier (K[X])"
+ shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
+ using divides_irreducible_condition[of "K[X]" q p] assms
+ unfolding ring_irreducible_def by auto
+
+subsection \<open>Polynomial Power\<close>
+
+lemma (in domain) polynomial_pow_not_zero:
+ assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+ shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from assms UP.integral show ?thesis
+ unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+ by (induction n, auto)
+qed
+
+lemma (in domain) subring_polynomial_pow_not_zero:
+ assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
+ shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
+ using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
+ unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_degree:
+ assumes "p \<in> carrier (poly_ring R)"
+ shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ show ?thesis
+ proof (induction n)
+ case 0 thus ?case
+ using UP.nat_pow_0 unfolding univ_poly_one by auto
+ next
+ let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+ case (Suc n) thus ?case
+ proof (cases "p = []")
+ case True thus ?thesis
+ using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
+ next
+ case False
+ hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
+ using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
+ thus ?thesis
+ using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
+ unfolding univ_poly_carrier univ_poly_zero
+ by (auto simp add: add.commute univ_poly_mult)
+ qed
+ qed
+qed
+
+lemma (in domain) subring_polynomial_pow_degree:
+ assumes "subring K R" and "p \<in> carrier (K[X])"
+ shows "degree (p [^]\<^bsub>K[X]\<^esub> n) = n * degree p"
+ using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
+ unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_division:
+ assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
+ shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+
+ have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
+ using assms(1) by (simp add: UP.nat_pow_mult)
+ thus ?thesis
+ using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
+ unfolding pdivides_def by auto
+qed
+
+lemma (in domain) subring_polynomial_pow_division:
+ assumes "subring K R" and "p \<in> carrier (K[X])" and "(n::nat) \<le> m"
+ shows "(p [^]\<^bsub>K[X]\<^esub> n) divides\<^bsub>K[X]\<^esub> (p [^]\<^bsub>K[X]\<^esub> m)"
+ using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
+ unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp
+
+lemma (in domain) pirreducible_pow_pdivides_iff:
+ assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
+ and "pirreducible K p" and "\<not> (p pdivides q)"
+ shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<longleftrightarrow> (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
+proof -
+ interpret UP: principal_domain "K[X]"
+ using univ_poly_is_principal[OF assms(1)] .
+ show ?thesis
+ proof (cases "r = []")
+ case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
+ unfolding sym[OF univ_poly_zero[of R K]] by auto
+ thus ?thesis
+ using pdivides_zero[OF subfieldE(1),of K] assms by auto
+ next
+ case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
+ using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
+ UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
+ from \<open>p \<noteq> []\<close>
+ have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
+ using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
+ have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
+ using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
+ have prime: "prime (mult_of (K[X])) p"
+ using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
+ unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
+ have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
+ if "a \<in> carrier (K[X])" "a \<noteq> \<zero>\<^bsub>K[X]\<^esub>" "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>" for a b
+ using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
+ unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
+ thus ?thesis
+ using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
+ unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
+ by (metis DiffI UP.m_closed singletonD)
+ qed
+qed
+
+lemma (in domain) subring_degree_one_imp_pirreducible:
+ assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
+ shows "pirreducible K [ a, b ]"
+proof (rule pirreducibleI[OF assms(1)])
+ have "a \<in> K" and "a \<noteq> \<zero>"
+ using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
+ thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
+ using univ_poly_units_incl[OF assms(1)] assms(2-3)
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+next
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF assms(1)] .
+
+ { fix q r
+ assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+ hence not_zero: "q \<noteq> []" "r \<noteq> []"
+ by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
+ have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
+ using not_zero poly_mult_degree_eq[OF assms(1)] q r
+ by (simp add: univ_poly_carrier univ_poly_mult)
+ with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
+ using not_zero by auto
+ } note aux_lemma1 = this
+
+ { fix q r
+ assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
+ and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
+ hence "length q = Suc (Suc 0)" and "length r = Suc 0"
+ by (linarith, metis add.right_neutral add_eq_if length_0_conv)
+ from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
+ by (metis length_0_conv length_Cons list.exhaust nat.inject)
+ from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
+ by (metis length_0_conv length_Suc_conv)
+ from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
+ have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
+ using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
+ using poly_mult_lead_coeff[OF assms(1), of q r]
+ unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
+ obtain inv_a where a: "a \<in> K" and inv_a: "inv_a \<in> K" "a \<otimes> inv_a = \<one>" "inv_a \<otimes> a = \<one>"
+ using assms(2) unfolding Units_def by auto
+ hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
+ using subringE(1)[OF assms(1)] integral_iff by auto
+ with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
+ using subringE(1,6)[OF assms(1)] inv_a integral
+ unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (auto, meson subsetD)
+ moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
+ using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
+ unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
+ ultimately have "r \<in> Units (K[X])"
+ using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
+ } note aux_lemma2 = this
+
+ fix q r
+ assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+ thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
+ using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
+qed
+
+lemma (in domain) degree_one_imp_pirreducible:
+ assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+ shows "pirreducible K p"
+proof -
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where p: "p = [ a, b ]"
+ by (metis length_0_conv length_Suc_conv)
+ with \<open>p \<in> carrier (K[X])\<close> show ?thesis
+ using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
+ subfield.subfield_Units[OF assms(1)]
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+qed
+
+lemma (in ring) degree_oneE[elim]:
+ assumes "p \<in> carrier (K[X])" and "degree p = 1"
+ and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
+ shows P
+proof -
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where "p = [ a, b ]"
+ by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
+ with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>p = [ a, b ]\<close> show ?thesis
+ using assms(3) by simp
+qed
+
+lemma (in domain) subring_degree_one_associatedI:
+ assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
+ shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+proof -
+ from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
+ using subringE(1)[OF assms(1)] assms(2-3) by auto
+ hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+ using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
+ unfolding univ_poly_mult by fastforce
+ moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
+ using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ moreover have "[ a ] \<in> Units (K[X])"
+ proof -
+ from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
+ using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ moreover have "a' \<otimes> a = \<one>"
+ using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
+ hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
+ using assms unfolding univ_poly_mult by auto
+ ultimately show ?thesis
+ unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
+ qed
+ ultimately show ?thesis
+ using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
+qed
+
+lemma (in domain) degree_one_associatedI:
+ assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+ shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
+proof -
+ from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
+ obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
+ by auto
+ thus ?thesis
+ using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
+ subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
+ unfolding const_term_def
+ by auto
+qed
+
subsection \<open>Ideals\<close>
lemma (in domain) exists_unique_gen:
@@ -882,6 +1136,26 @@
subsection \<open>Roots and Multiplicity\<close>
+definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
+
+definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
+ where "alg_mult p x =
+ (if p = [] then 0 else
+ (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
+
+definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
+ where "roots p = Abs_multiset (alg_mult p)"
+
+definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
+ where "roots_on K p = roots p \<inter># mset_set K"
+
+definition (in ring) splitted :: "'a list \<Rightarrow> bool"
+ where "splitted p \<longleftrightarrow> size (roots p) = degree p"
+
+definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
+
lemma (in domain) pdivides_imp_root_sharing:
assumes "p \<in> carrier (poly_ring R)" "p pdivides q" and "a \<in> carrier R"
shows "eval p a = \<zero> \<Longrightarrow> eval q a = \<zero>"
@@ -922,6 +1196,782 @@
show "inv (lead_coeff p) \<otimes> (const_term p) \<in> K"
using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
qed
+lemma (in domain) is_root_imp_pdivides:
+ assumes "p \<in> carrier (poly_ring R)"
+ shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
+proof -
+ let ?b = "[ \<one> , \<ominus> x ]"
+
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
+ unfolding is_root_def by auto
+ hence b: "?b \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
+ and long_divides: "p = (?b \<otimes>\<^bsub>poly_ring R\<^esub> q) \<oplus>\<^bsub>poly_ring R\<^esub> r" "r = [] \<or> degree r < degree ?b"
+ using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
+
+ show ?thesis
+ proof (cases "r = []")
+ case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
+ unfolding univ_poly_zero[of R "carrier R"] .
+ thus ?thesis
+ using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
+ next
+ case False then have "length r = Suc 0"
+ using long_divides(2) le_SucE by fastforce
+ then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
+ using r unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+
+ have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
+ using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
+ also have " ... = eval r x"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
+ finally have "a = \<zero>"
+ using a unfolding \<open>r = [ a ]\<close> is_root by simp
+ with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
+ qed
+qed
+
+lemma (in domain) pdivides_imp_is_root:
+ assumes "p \<noteq> []" and "x \<in> carrier R"
+ shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
+proof -
+ assume "[ \<one>, \<ominus> x ] pdivides p"
+ then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+ unfolding pdivides_def by auto
+ moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ ultimately have "eval p x = \<zero>"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
+ with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
+ unfolding is_root_def 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"
+proof (cases "p = []")
+ case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
+ unfolding associated_def True factor_def univ_poly_def by auto
+ thus ?thesis
+ using True unfolding is_root_def by simp
+next
+ case False
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ { fix p q
+ assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ have "is_root p x \<Longrightarrow> is_root q x"
+ proof -
+ assume is_root: "is_root p x"
+ then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
+ using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
+ moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
+ ultimately have "[ \<one>, \<ominus> x ] pdivides q"
+ using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
+ with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
+ using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
+ pdivides_imp_is_root[of q x]
+ by fastforce
+ qed
+ }
+
+ then show ?thesis
+ using assms UP.associated_sym[OF assms(3)] by blast
+qed
+
+lemma (in ring) monic_degree_one_root_condition:
+ assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
+ using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
+
+lemma (in field) degree_one_root_condition:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+ shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+ by simp
+ then obtain a b where p: "p = [ a, b ]"
+ by (metis length_0_conv length_Cons list.exhaust nat.inject)
+ hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
+ using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
+ using subfield_m_inv[OF carrier_is_subfield, of a] by auto
+ hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
+ using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+ have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
+ proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
+ have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
+ using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
+ also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
+ using UP.m_comm[OF in_carrier, of "[ a ]"] a
+ by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
+ finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
+ next
+ from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
+ unfolding univ_poly_units[OF carrier_is_subfield] by simp
+ qed
+
+ moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
+ and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
+ using inv_a a b unfolding p const_term_def by auto
+
+ ultimately show ?thesis
+ using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
+ monic_degree_one_root_condition
+ by (metis add.inv_closed)
+qed
+
+lemma (in domain) is_root_poly_mult_imp_is_root:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+ shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
+ hence "p \<noteq> []" and "q \<noteq> []"
+ unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
+ using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
+ moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
+ using is_root unfolding is_root_def by simp+
+ hence "eval p x = \<zero> \<or> eval q x = \<zero>"
+ using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
+ ultimately show "(is_root p x) \<or> (is_root q x)"
+ using x unfolding is_root_def by auto
+qed
+
+lemma (in domain) degree_zero_imp_not_is_root:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
+proof (cases "p = []", simp add: is_root_def)
+ case False with \<open>degree p = 0\<close> have "length p = Suc 0"
+ using le_SucE by fastforce
+ then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def
+ by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+ thus ?thesis
+ unfolding is_root_def by auto
+qed
+
+lemma (in domain) finite_number_of_roots:
+ assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
+ using assms
+proof (induction "degree p" arbitrary: p)
+ case 0 thus ?case
+ by (simp add: degree_zero_imp_not_is_root)
+next
+ case (Suc n) show ?case
+ proof (cases "{ x. is_root p x } = {}")
+ case True thus ?thesis
+ by (simp add: True)
+ next
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ case False
+ then obtain a where is_root: "is_root p a"
+ by blast
+ hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
+ unfolding is_root_def by auto
+ hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+ obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+ using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
+ with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+ using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+ by metis
+ hence "degree q = n"
+ using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
+ in_carrier q p_not_zero p Suc(2)
+ unfolding univ_poly_carrier
+ by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
+ list.size(3-4) plus_1_eq_Suc univ_poly_mult)
+ hence "finite { x. is_root q x }"
+ using Suc(1)[OF _ q] by simp
+
+ moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
+ using is_root_poly_mult_imp_is_root[OF in_carrier q]
+ monic_degree_one_root_condition[OF a]
+ unfolding p by auto
+
+ ultimately show ?thesis
+ using finite_subset by auto
+ qed
+qed
+
+lemma (in domain) alg_multE:
+ assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+ shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+ and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
+
+ define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
+ have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
+ using UP.nat_pow_0 by simp
+ hence "0 \<in> S"
+ using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
+ hence "S \<noteq> {}"
+ by auto
+
+ moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
+ proof -
+ have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "?ppow n \<in> carrier (poly_ring R)"
+ using assms unfolding univ_poly_zero by auto
+ with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
+ using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
+ with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
+ using polynomial_pow_degree by simp
+ qed
+ hence "finite S"
+ using finite_nat_set_iff_bounded_le by blast
+
+ ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
+ using Max_ge[of S] Max_in[of S] by auto
+ with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
+ using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
+ unfolding S_def alg_mult_def by auto
+ thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+ and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+ using MaxS unfolding S_def by auto
+qed
+
+lemma (in domain) le_alg_mult_imp_pdivides:
+ assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
+ shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume le_alg_mult: "n \<le> alg_mult p x"
+ have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence ppow_pdivides:
+ "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
+ ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
+ using polynomial_pow_division[OF _ le_alg_mult] by simp
+
+ show ?thesis
+ proof (cases "p = []")
+ case True thus ?thesis
+ using in_carrier pdivides_zero[OF carrier_is_subring] by auto
+ next
+ case False thus ?thesis
+ using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
+ unfolding pdivides_def by meson
+ qed
+qed
+
+lemma (in domain) alg_mult_gt_zero_iff_is_root:
+ assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+ show ?thesis
+ proof
+ assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+ unfolding is_root_def by auto
+ have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
+ using x unfolding univ_poly_def by auto
+ thus "alg_mult p x > 0"
+ using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
+ next
+ assume gt_zero: "alg_mult p x > 0"
+ hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+ unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
+ hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
+ using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
+ thus "is_root p x"
+ using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
+ qed
+qed
+
+lemma (in domain) alg_mult_eq_count_roots:
+ assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
+ using finite_number_of_roots[OF assms]
+ unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
+ by (simp add: multiset_def roots_def)
+
+lemma (in domain) roots_mem_iff_is_root:
+ assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
+ using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
+ unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
+
+lemma (in domain) degree_zero_imp_empty_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
+ using degree_zero_imp_not_is_root[of p] roots_mem_iff_is_root[of p] assms by auto
+
+lemma (in domain) degree_zero_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
+ unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
+
+lemma (in domain) roots_inclI':
+ assumes "p \<in> carrier (poly_ring R)" and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> alg_mult p a \<le> count m a"
+ shows "roots p \<subseteq># m"
+proof (intro mset_subset_eqI)
+ fix a show "count (roots p) a \<le> count m a"
+ using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
+ by (cases "p = []", simp, cases "a \<in> carrier R", auto)
+qed
+
+lemma (in domain) roots_inclI:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+ and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+ shows "roots p \<subseteq># roots q"
+ using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
+ unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
+
+lemma (in domain) pdivides_imp_roots_incl:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+ shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
+proof (rule roots_inclI[OF assms])
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ fix a assume "p pdivides q" and a: "a \<in> carrier R"
+ hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+ using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
+ by (auto simp add: pdivides_def)
+qed
+
+lemma (in domain) associated_polynomials_imp_same_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ shows "roots p = roots q"
+ using assms pdivides_imp_roots_incl zero_pdivides
+ unfolding pdivides_def associated_def
+ by (metis subset_mset.eq_iff)
+
+lemma (in domain) monic_degree_one_roots:
+ assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
+proof -
+ let ?p = "[ \<one> , \<ominus> a ]"
+
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ show ?thesis
+ proof (rule subset_mset.antisym)
+ show "{# a #} \<subseteq># roots ?p"
+ using roots_mem_iff_is_root[OF in_carrier]
+ monic_degree_one_root_condition[OF assms]
+ by simp
+ next
+ show "roots ?p \<subseteq># {# a #}"
+ proof (rule mset_subset_eqI, auto)
+ fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
+ using alg_mult_gt_zero_iff_is_root[OF in_carrier]
+ monic_degree_one_root_condition[OF assms]
+ unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+ by fastforce
+ next
+ have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
+ using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
+ hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
+ using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
+ thus "count (roots ?p) a \<le> Suc 0"
+ using polynomial_pow_degree[OF in_carrier]
+ unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+ by auto
+ qed
+ qed
+qed
+
+lemma (in domain) degree_one_roots:
+ assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
+ shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
+proof -
+ have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
+ using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ thus ?thesis
+ using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
+ monic_degree_one_roots associated_polynomials_imp_same_roots
+ by (metis add.inv_closed local.minus_minus m_closed)
+qed
+
+lemma (in field) degree_one_imp_singleton_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+ shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
+proof -
+ from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
+ obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
+ by auto
+ thus ?thesis
+ using degree_one_roots[of a "inv a" b]
+ by (auto simp add: const_term_def field_Units)
+qed
+
+lemma (in field) degree_one_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
+ using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
+
+lemma (in field) no_roots_imp_same_roots:
+ assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
+ shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+ proof (intro subset_mset.antisym)
+ have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using UP.divides_prod_l assms unfolding pdivides_def by blast
+ show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
+ degree_zero_imp_empty_roots[OF assms(3)]
+ by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
+ next
+ show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
+ proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
+ case True thus ?thesis
+ using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
+ next
+ case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+ by (metis UP.r_null assms(1) univ_poly_zero)
+ show ?thesis
+ proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
+ fix a assume a: "a \<in> carrier R"
+ hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
+ using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
+ moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
+ using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
+ moreover
+ have "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
+ ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
+ using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
+ qed
+ qed
+ qed
+qed
+
+lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
+ assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
+ shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+
+ show ?thesis
+ proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
+ show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
+ using in_carrier assms(2) by simp
+ next
+ fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+ hence not_zero: "p \<noteq> []"
+ unfolding univ_poly_def by auto
+ from \<open>b \<in> carrier R\<close> have in_carrier': "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
+ unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+ show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
+ proof (cases "a = b")
+ case False
+ hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
+ using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
+ moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
+ using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
+ ultimately
+ have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
+ using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
+ pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
+ by auto
+ with \<open>a \<noteq> b\<close> show ?thesis
+ using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
+ next
+ case True
+ have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using dividesI[OF assms(2)] unfolding pdivides_def by auto
+ with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
+ have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
+ using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
+ then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
+ using Suc_le_D by blast
+ hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
+ ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
+ in_carrier assms UP.nat_pow_Suc2 by force
+ hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
+ using UP.mult_divides in_carrier assms(2)
+ unfolding univ_poly_zero pdivides_def factor_def
+ by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
+ with \<open>a = b\<close> show ?thesis
+ using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
+ alg_multE(2)[OF assms(1) _ not_zero] m
+ by auto
+ qed
+ next
+ fix b
+ have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+ using assms in_carrier univ_poly_zero[of R] UP.integral by auto
+
+ show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
+ proof (cases "a = b")
+ case True
+ have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
+ ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
+ by (auto simp add: pdivides_def)
+ with \<open>a = b\<close> show ?thesis
+ using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
+ alg_multE(2)[OF assms(1) _ not_zero]
+ by auto
+ next
+ case False
+ have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+ using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
+ thus ?thesis
+ using False pdivides_imp_roots_incl assms in_carrier not_zero
+ by (simp add: subseteq_mset_def)
+ qed
+ qed
+qed
+
+lemma (in domain) not_empty_rootsE[elim]:
+ assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
+ and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
+ [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
+ shows P
+proof -
+ from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
+ by blast
+ with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
+ and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
+ using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
+ unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+ with \<open>a \<in># roots p\<close> show ?thesis
+ using assms(3)[of a] by auto
+qed
+
+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"
+proof -
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+ from assms show ?thesis
+ proof (induction "degree p" arbitrary: p rule: less_induct)
+ case less show ?case
+ proof (cases "roots p = {#}")
+ case True thus ?thesis
+ using no_roots_imp_same_roots[of p q] less by simp
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ show ?thesis
+ proof (cases "degree p = 1")
+ case True with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
+ by auto
+ with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
+ and lead: "lead_coeff p = b" and const: "const_term p = c"
+ using degree_one_imp_singleton_roots[of p] less(2) field_Units
+ unfolding const_term_def by auto
+ hence "(p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<sim>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
+ by (auto simp add: a lead const)
+ hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+ using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
+ thus ?thesis
+ unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
+ next
+ case False
+ from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
+ obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by auto
+ with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
+ using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
+ hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
+ using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
+ UP.m_assoc[OF in_carrier r less(4)] p by auto
+ also have " ... = add_mset a (roots r + roots q)"
+ using less(1)[OF _ r not_zero less(4-5)] deg by simp
+ also have " ... = (add_mset a (roots r)) + roots q"
+ by simp
+ also have " ... = roots p + roots q"
+ using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
+ finally show ?thesis .
+ qed
+ qed
+ qed
+qed
+
+lemma (in field) size_roots_le_degree:
+ assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case less show ?case
+ proof (cases "roots p = {#}", simp)
+ interpret UP: domain "poly_ring R"
+ using univ_poly_is_domain[OF carrier_is_subring] .
+
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by auto
+ with \<open>a \<in># roots p\<close> have "p \<noteq> []"
+ using degree_zero_imp_empty_roots[OF less(2)] by auto
+ hence not_zero: "q \<noteq> []"
+ using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
+ hence "degree p = Suc (degree q)"
+ using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ with \<open>q \<noteq> []\<close> show ?thesis
+ using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
+ by (metis Suc_le_mono lessI size_add_mset)
+ qed
+qed
+
+lemma (in domain) pirreducible_roots:
+ assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "roots p = {#}"
+proof (rule ccontr)
+ assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
+ using divides_pirreducible_condition[OF assms(2) in_carrier]
+ univ_poly_units_incl[OF carrier_is_subring]
+ unfolding pdivides_def by auto
+ hence "degree p = 1"
+ using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
+ with \<open>degree p \<noteq> 1\<close> show False ..
+qed
+
+lemma (in field) pirreducible_imp_not_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "\<not> splitted p"
+ using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
+ by (simp add: splitted_def)
+
+lemma (in field)
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+ and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+ shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+ using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
+ unfolding ring_irreducible_def univ_poly_zero by auto
+
+lemma (in field) trivial_factors_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)"
+ and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
+ shows "splitted p"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ interpret UP: principal_domain "poly_ring R"
+ using univ_poly_is_principal[OF carrier_is_subfield] .
+ case less show ?case
+ proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
+ case False show ?thesis
+ proof (cases "roots p = {#}")
+ case True
+ from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
+ using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
+ then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
+ using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
+ with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
+ using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
+ pdivides_imp_roots_incl[OF _ less(2), of q]
+ pirreducible_degree[OF carrier_is_subfield, of q]
+ by force
+ from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
+ by simp
+ thus ?thesis ..
+ next
+ case False with \<open>p \<in> carrier (poly_ring R)\<close>
+ obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+ and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+ by blast
+ then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+ unfolding pdivides_def by blast
+ with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
+ by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
+ using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+ with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> and \<open>p \<noteq> []\<close> have "degree p = Suc (degree q)"
+ using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+ moreover have "q pdivides p"
+ using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
+ hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
+ and "r pdivides q" for r
+ using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
+ pirreducible_degree[OF carrier_is_subfield that(1-2)]
+ by (auto simp add: pdivides_def)
+ ultimately have "splitted q"
+ using less(1)[OF _ q] by auto
+ with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
+ using poly_mult_degree_one_monic_imp_same_roots[OF a q]
+ unfolding sym[OF p] splitted_def
+ by simp
+ qed
+ qed
+qed
+
+lemma (in field) pdivides_imp_splitted:
+ assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
+ shows "p pdivides q \<Longrightarrow> splitted p"
+proof (cases "p = []")
+ case True thus ?thesis
+ using degree_zero_imp_splitted[OF assms(1)] by simp
+next
+ interpret UP: principal_domain "poly_ring R"
+ using univ_poly_is_principal[OF carrier_is_subfield] .
+
+ case False
+ assume "p pdivides q"
+ then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
+ unfolding pdivides_def by auto
+ with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
+ using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+ hence "degree p + degree b = size (roots p) + size (roots b)"
+ using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
+ poly_mult_degree_eq[OF carrier_is_subring,of p b]
+ unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
+ by auto
+ moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
+ using size_roots_le_degree assms(1) b by auto
+ ultimately show ?thesis
+ unfolding splitted_def by linarith
+qed
+
+lemma (in field) splitted_imp_trivial_factors:
+ assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
+ shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
+ using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
+ by auto
subsection \<open>Link between @{term \<open>(pmod)\<close>} and @{term rupture_surj}\<close>
@@ -970,32 +2020,6 @@
qed
qed
-(* Move to Ideal.thy ========================================================= *)
-lemma (in ring) quotient_eq_iff_same_a_r_cos:
- assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
- shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
-proof
- assume "I +> a = I +> b"
- then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
- using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
- unfolding a_r_coset_def' by blast
- hence "a \<ominus> b = i"
- using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
- with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
- by simp
-next
- assume "a \<ominus> b \<in> I"
- then obtain i where "i \<in> I" and "a = i \<oplus> b"
- using ideal.Icarr[OF assms(1)] assms(2-3)
- by (metis a_minus_def add.inv_solve_right)
- hence "I +> a = (I +> i) +> b"
- using ideal.Icarr[OF assms(1)] assms(3)
- by (simp add: a_coset_add_assoc subsetI)
- with \<open>i \<in> I\<close> show "I +> a = I +> b"
- using a_rcos_zero[OF assms(1)] by simp
-qed
-(* ========================================================================== *)
-
lemma (in domain) rupture_surj_inj_on:
assumes "subfield K R" and "p \<in> carrier (K[X])"
shows "inj_on (rupture_surj K p) ((\<lambda>q. q pmod p) ` (carrier (K[X])))"
--- a/src/HOL/Algebra/Pred_Zorn.thy Mon Apr 29 17:11:26 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-theory Pred_Zorn
- imports HOL.Zorn
-
-begin
-
-(* ========== *)
-lemma partial_order_onE:
- assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
- using assms unfolding partial_order_on_def preorder_on_def by auto
-(* ========== *)
-
-abbreviation rel_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
- where "rel_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
-
-lemma Field_rel_of:
- assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A"
- using assms unfolding refl_on_def Field_def by auto
-
-(* ========== *)
-lemma Chains_rel_of:
- assumes "C \<in> Chains (rel_of P A)" shows "C \<subseteq> A"
- using assms unfolding Chains_def by auto
-(* ========== *)
-
-lemma partial_order_on_rel_ofI:
- assumes refl: "\<And>a. a \<in> A \<Longrightarrow> P a a"
- and trans: "\<And>a b c. \<lbrakk> a \<in> A; b \<in> A; c \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b c \<Longrightarrow> P a c"
- and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
- shows "partial_order_on A (rel_of P A)"
-proof -
- from refl have "refl_on A (rel_of P A)"
- unfolding refl_on_def by auto
- moreover have "trans (rel_of P A)" and "antisym (rel_of P A)"
- by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
- ultimately show ?thesis
- unfolding partial_order_on_def preorder_on_def by simp
-qed
-
-lemma Partial_order_rel_ofI:
- assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)"
- using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] .
-
-lemma predicate_Zorn:
- assumes "partial_order_on A (rel_of P A)"
- and "\<forall>C \<in> Chains (rel_of P A). \<exists>u \<in> A. \<forall>a \<in> C. P a u"
- shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
-proof -
- have "a \<in> A" if "a \<in> C" and "C \<in> Chains (rel_of P A)" for C a
- using that Chains_rel_of by auto
- moreover have "(a, u) \<in> rel_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
- using that by auto
- ultimately show ?thesis
- using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2)
- unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto
-qed
-
-end
\ No newline at end of file