--- a/src/HOL/Algebra/Multiplicative_Group.thy Tue Jul 03 00:15:16 2018 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Tue Jul 03 10:07:24 2018 +0100
@@ -609,16 +609,16 @@
definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
"mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"
-lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
+lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
by (simp add: mult_of_def)
-lemma mult_mult_of: "mult (mult_of R) = mult R"
+lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
by (simp add: mult_of_def)
lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
by (simp add: mult_of_def fun_eq_iff nat_pow_def)
-lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
+lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
by (simp add: mult_of_def)
lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
--- a/src/HOL/Algebra/Polynomials.thy Tue Jul 03 00:15:16 2018 +0100
+++ b/src/HOL/Algebra/Polynomials.thy Tue Jul 03 10:07:24 2018 +0100
@@ -127,7 +127,7 @@
using degree_def[of "a # p"] by auto
also have " ... = a # p"
using Cons by simp
- finally show ?case .
+ finally show ?case .
qed
lemma coeff_nth: "i < length p \<Longrightarrow> (coeff p) i = p ! (length p - 1 - i)"
@@ -228,7 +228,7 @@
assume "p1 \<noteq> [] \<and> p2 \<noteq> []"
hence "length p1 = length p2"
using deg_eq unfolding degree_def
- by (simp add: Nitpick.size_list_simp(2))
+ by (simp add: Nitpick.size_list_simp(2))
thus ?thesis
using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
next
@@ -681,7 +681,7 @@
proof -
let ?len = length and ?norm = normalize
obtain a p' where p: "p = a # p'"
- using assms(2) list.exhaust_sel by blast
+ using assms(2) list.exhaust_sel by blast
hence a: "a \<in> carrier R - { \<zero> }" and p': "set p' \<subseteq> carrier R"
using assms(1) unfolding p by (auto simp add: polynomial_def)
hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'"
@@ -742,7 +742,7 @@
next
case (Cons a p1)
let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
-
+
have "set (poly_mult p1 p2) \<subseteq> carrier R"
using Cons unfolding polynomial_def by auto
@@ -775,7 +775,7 @@
lemma poly_mult_coeff:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
shows "coeff (poly_mult p1 p2) = (\<lambda>i. \<Oplus> k \<in> {..i}. (coeff p1) k \<otimes> (coeff p2) (i - k))"
- using assms(1)
+ using assms(1)
proof (induction p1)
case Nil thus ?case using assms(2) by auto
next
@@ -823,7 +823,7 @@
have "\<And>k. k \<in> {..i} \<Longrightarrow>
?f2 k \<otimes>\<^bsub>R\<^esub> ?f3 (i - k) = (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>)"
using in_carrier by auto
- hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) =
+ hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) =
(\<Oplus> k \<in> {..i}. (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>))"
using in_carrier
add.finprod_cong'[of "{..i}" "{..i}" "\<lambda>k. ?f2 k \<otimes> ?f3 (i - k)"
@@ -848,7 +848,7 @@
using in_carrier(1) assms(2) by auto
moreover have "set (poly_mult p1 p2) \<subseteq> carrier R"
- using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto
+ using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto
ultimately
have "coeff (poly_mult (a # p1) p2) = (\<lambda>i. ((coeff ?a_p2) i) \<oplus> ((coeff (poly_mult p1 p2)) i))"
@@ -910,7 +910,7 @@
and "polynomial R (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier by auto
ultimately show ?thesis
- using coeff_iff_polynomial_cond by auto
+ using coeff_iff_polynomial_cond by auto
qed
lemma poly_mult_l_distr:
@@ -938,7 +938,7 @@
normalize_replicate_zero[of "length p2 + length p1" "[]"] by auto
finally show ?thesis by auto
qed } note aux_lemma = this
-
+
from assms show ?thesis
proof (induction n)
case 0 thus ?case by simp
@@ -988,7 +988,7 @@
using inj_on_def by force
moreover have "(\<lambda>k. i - k) ` {..i} \<subseteq> {..i}" by auto
hence "(\<lambda>k. i - k) ` {..i} = {..i}"
- using reindex_inj endo_inj_surj[of "{..i}" "\<lambda>k. i - k"] by simp
+ using reindex_inj endo_inj_surj[of "{..i}" "\<lambda>k. i - k"] by simp
ultimately have "(\<Oplus>k \<in> {..i}. ?f k) = (\<Oplus>k \<in> {..i}. ?f (i - k))"
using add.finprod_reindex[of ?f "\<lambda>k. i - k" "{..i}"] in_carrier by auto
@@ -1041,7 +1041,7 @@
using poly_add_normalize(1)[of "replicate (length p + n) \<zero>" "[]"]
normalize_replicate_zero[of "length p + n" "[]"] by auto
also have " ... = []" by simp
- finally show ?case .
+ finally show ?case .
qed
thus "poly_mult p (replicate n \<zero>) = []"
using poly_mult_comm[OF assms in_carrier] by simp
@@ -1061,9 +1061,9 @@
next
case (Cons b ps)
hence "a \<otimes> lead_coeff p \<noteq> \<zero>"
- using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto
+ using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto
thus ?thesis
- using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto
+ using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto
qed
ultimately show ?thesis
using poly_add_zero(1)[of "map (\<lambda>b. a \<otimes> b) p"] by simp
@@ -1086,7 +1086,7 @@
hence "lead_coeff ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<noteq> \<zero>"
using Cons assms integral[of a b] unfolding polynomial_def by auto
moreover have "set ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<subseteq> carrier R"
- using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto
+ using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto
ultimately have is_polynomial: "polynomial R ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
using Cons unfolding polynomial_def by auto
@@ -1107,7 +1107,7 @@
shows "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
proof -
have "map (\<lambda>a. \<one> \<otimes> a) p = p"
- using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE)
+ using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE)
thus "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
using poly_mult_const[OF assms, of \<one>] by auto
qed
@@ -1119,7 +1119,7 @@
have p1: "lead_coeff p1 \<in> carrier R - { \<zero> }" and p2: "lead_coeff p2 \<in> carrier R - { \<zero> }"
using assms unfolding polynomial_def by auto
- have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) =
+ have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) =
(\<Oplus> k \<in> {..((degree p1) + (degree p2))}.
(coeff p1) k \<otimes> (coeff p2) ((degree p1) + (degree p2) - k))"
using poly_mult_coeff assms(1-2) polynomial_in_carrier by auto
@@ -1299,7 +1299,7 @@
also have " ... = (\<Oplus>i \<in> {..n - ?len}. (a \<otimes> ?c2 i) \<otimes> ?c3 (n - (i + ?len)))"
unfolding h_def by simp
also have " ... = (\<Oplus>i \<in> {..n - ?len}. a \<otimes> (?c2 i \<otimes> ?c3 (n - (i + ?len))))"
- using in_carrier assms(3) by (simp add: m_assoc)
+ using in_carrier assms(3) by (simp add: m_assoc)
also have " ... = a \<otimes> (\<Oplus>i \<in> {..n - ?len}. ?c2 i \<otimes> ?c3 (n - (i + ?len)))"
using finsum_rdistr[of "{..n - ?len}" a "\<lambda>i. ?c2 i \<otimes> ?c3 (n - (i + ?len))"]
in_carrier(2-3) assms(3) by simp
@@ -1427,10 +1427,10 @@
proof (auto)
fix p assume p: "polynomial R p"
have "polynomial R [ \<ominus> \<one> ]"
- unfolding polynomial_def using r_neg by fastforce
+ unfolding polynomial_def using r_neg by fastforce
hence cond0: "polynomial R (poly_mult [ \<ominus> \<one> ] p)"
using poly_mult_closed[of "[ \<ominus> \<one> ]" p] p by simp
-
+
have "poly_add p (poly_mult [ \<ominus> \<one> ] p) = poly_add (poly_mult [ \<one> ] p) (poly_mult [ \<ominus> \<one> ] p)"
using poly_mult_one[OF p] by simp
also have " ... = poly_mult (poly_add [ \<one> ] [ \<ominus> \<one> ]) p"
@@ -1498,6 +1498,51 @@
(auto simp add: univ_poly_def domain.poly_mult_integral[OF assms])
qed
+lemma (in domain) univ_poly_a_inv_def':
+ assumes "p \<in> carrier (univ_poly R)"
+ shows "\<ominus>\<^bsub>(univ_poly R)\<^esub> p = map (\<lambda>a. \<ominus> a) p"
+proof -
+ have aux_lemma:
+ "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> p \<oplus>\<^bsub>(univ_poly R)\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
+ "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> (map (\<lambda>a. \<ominus> a) p) \<in> carrier (univ_poly R)"
+ proof -
+ fix p assume p: "p \<in> carrier (univ_poly R)"
+ hence set_p: "set p \<subseteq> carrier R"
+ unfolding univ_poly_def polynomial_def by auto
+ show "(map (\<lambda>a. \<ominus> a) p) \<in> carrier (univ_poly R)"
+ proof (cases "p = []")
+ assume "p = []" thus ?thesis
+ unfolding univ_poly_def polynomial_def by auto
+ next
+ assume not_nil: "p \<noteq> []"
+ hence "lead_coeff p \<noteq> \<zero>"
+ using p unfolding univ_poly_def polynomial_def by auto
+ moreover have "lead_coeff (map (\<lambda>a. \<ominus> a) p) = \<ominus> (lead_coeff p)"
+ using not_nil by (simp add: hd_map)
+ ultimately have "lead_coeff (map (\<lambda>a. \<ominus> a) p) \<noteq> \<zero>"
+ using hd_in_set local.minus_zero not_nil set_p by force
+ moreover have "set (map (\<lambda>a. \<ominus> a) p) \<subseteq> carrier R"
+ using set_p by (induct p) (auto)
+ ultimately show ?thesis
+ unfolding univ_poly_def polynomial_def by auto
+ qed
+
+ have "map2 (\<oplus>) p (map (\<lambda>a. \<ominus> a) p) = replicate (length p) \<zero>"
+ using set_p by (induct p) (auto simp add: r_neg)
+ thus "p \<oplus>\<^bsub>(univ_poly R)\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
+ unfolding univ_poly_def using normalize_replicate_zero[of "length p" "[]"] by auto
+ qed
+
+ interpret UP: ring "univ_poly R"
+ using univ_poly_is_ring[OF domain_axioms] .
+
+ from aux_lemma
+ have "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> \<ominus>\<^bsub>(univ_poly R)\<^esub> p = map (\<lambda>a. \<ominus> a) p"
+ by (metis Nil_is_map_conv UP.add.inv_closed UP.l_zero UP.r_neg1 UP.r_zero UP.zero_closed)
+ thus ?thesis
+ using assms by simp
+qed
+
subsection \<open>Long Division Theorem\<close>
@@ -1519,7 +1564,7 @@
proof (cases "length b > length p")
assume "length b > length p"
hence "p = [] \<or> degree p < degree b" unfolding degree_def
- by (meson diff_less_mono length_0_conv less_one not_le)
+ by (meson diff_less_mono length_0_conv less_one not_le)
hence "?long_division p [] p"
using poly_add_zero[OF less(2)] less(2) zero_is_polynomial
poly_mult_zero[OF less(3)] by simp
@@ -1546,7 +1591,7 @@
hence s_coeff: "lead_coeff s = (\<ominus> a)"
using poly_mult_lead_coeff[OF monon_is_polynomial[OF in_carrier] less(3)] a c
unfolding monon_def s_def b using m_assoc by force
-
+
have "degree s = degree (monon ((\<ominus> a) \<otimes> inv c) (?len p - ?len b)) + degree b"
using poly_mult_degree_eq[OF monon_is_polynomial[OF in_carrier] less(3)]
unfolding s_def b monon_def by auto
@@ -1560,7 +1605,7 @@
by (simp add: Nitpick.size_list_simp(2) local.Cons)
obtain s' where s: "s = (\<ominus> a) # s'"
- using s_coeff len_eq by (metis \<open>s \<noteq> []\<close> hd_Cons_tl)
+ using s_coeff len_eq by (metis \<open>s \<noteq> []\<close> hd_Cons_tl)
define p_diff where "p_diff = poly_add p s"
hence "?len p_diff < ?len p"
@@ -1578,7 +1623,7 @@
using s_def monon_is_polynomial[OF in_carrier(1)] by auto
have in_univ_carrier:
"p \<in> carrier (univ_poly R)" "m \<in> carrier (univ_poly R)" "b \<in> carrier (univ_poly R)"
- "r' \<in> carrier (univ_poly R)" "q' \<in> carrier (univ_poly R)"
+ "r' \<in> carrier (univ_poly R)" "q' \<in> carrier (univ_poly R)"
using r' q' less(2-3) m(1) unfolding univ_poly_def by auto
hence "poly_add p (poly_mult m b) = poly_add (poly_mult b q') r'"
@@ -1589,7 +1634,7 @@
"(p \<oplus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)) \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b) =
((b \<otimes>\<^bsub>(univ_poly R)\<^esub>q') \<oplus>\<^bsub>(univ_poly R)\<^esub> r') \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)"
by simp
- hence "p = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) \<oplus>\<^bsub>(univ_poly R)\<^esub> r'"
+ hence "p = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) \<oplus>\<^bsub>(univ_poly R)\<^esub> r'"
using in_univ_carrier by algebra
hence "p = poly_add (poly_mult b (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) r'"
unfolding univ_poly_def by simp
@@ -1611,7 +1656,7 @@
using long_division_theorem[OF assms] assms lead_coeff_not_zero[of "hd b" "tl b"]
by (simp add: field_Units)
-lemma univ_poly_is_euclidean_domain:
+theorem univ_poly_is_euclidean:
assumes "field R"
shows "euclidean_domain (univ_poly R) degree"
proof -
@@ -1623,6 +1668,16 @@
using field.field_long_division_theorem[OF assms] by auto
qed
+corollary univ_poly_is_principal:
+ assumes "field R"
+ shows "principal_domain (univ_poly R)"
+proof -
+ interpret UP: euclidean_domain "univ_poly R" degree
+ using univ_poly_is_euclidean[OF assms] .
+ show ?thesis
+ using UP.principal_domain_axioms .
+qed
+
subsection \<open>Consistency Rules\<close>
@@ -1652,7 +1707,7 @@
qed
lemma (in ring) poly_add_consistent [simp]:
- assumes "subring K R" shows "ring.poly_add (R \<lparr> carrier := K \<rparr>) = poly_add"
+ assumes "subring K R" shows "ring.poly_add (R \<lparr> carrier := K \<rparr>) = poly_add"
proof -
have "\<And>p q. ring.poly_add (R \<lparr> carrier := K \<rparr>) p q = poly_add p q"
proof -
@@ -1666,7 +1721,7 @@
assumes "subring K R" shows "ring.poly_mult (R \<lparr> carrier := K \<rparr>) = poly_mult"
proof -
have "\<And>p q. ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
- proof -
+ proof -
fix p q show "ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
using ring.poly_mult.simps[OF subring_is_ring[OF assms]] poly_add_consistent[OF assms]
by (induct p) (auto)
@@ -1674,7 +1729,7 @@
thus ?thesis by auto
qed
-lemma (in ring) univ_poly_carrier_change_def':
+lemma (in ring) univ_poly_subring_def':
assumes "subring K R"
shows "univ_poly (R \<lparr> carrier := K \<rparr>) = (univ_poly R) \<lparr> carrier := { p. polynomial R p \<and> set p \<subseteq> K } \<rparr>"
unfolding univ_poly_def polynomial_def
@@ -1683,6 +1738,26 @@
subringE(1)[OF assms]
by auto
+lemma (in domain) univ_poly_subring_is_domain:
+ assumes "subring K R"
+ shows "domain (univ_poly (R \<lparr> carrier := K \<rparr>))"
+proof -
+ have "domain (R \<lparr> carrier := K \<rparr>)"
+ using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] .
+ thus ?thesis
+ using univ_poly_is_domain[of "R \<lparr> carrier := K \<rparr>"] by simp
+qed
+
+lemma (in domain) univ_poly_subfield_is_euclidean:
+ assumes "subfield K R"
+ shows "euclidean_domain (univ_poly (R \<lparr> carrier := K \<rparr>)) degree"
+ using univ_poly_is_euclidean[OF subfield_iff(2)[OF assms]] .
+
+lemma (in domain) univ_poly_subfield_is_principal:
+ assumes "subfield K R"
+ shows "principal_domain (univ_poly (R \<lparr> carrier := K \<rparr>))"
+ using univ_poly_is_principal[OF subfield_iff(2)[OF assms]] .
+
subsection \<open>The Evaluation Homomorphism\<close>
@@ -1811,7 +1886,7 @@
hence "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
using assms(2) by (induct q) (auto)
hence "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval ((map ((\<otimes>) b) q)) a) \<otimes> (a [^] n) \<oplus> \<zero>"
- using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"]
+ using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"]
eval_replicate[OF _ assms(3), of "[]"] by auto
moreover have "eval (map ((\<otimes>) b) q) a = b \<otimes> eval q a"
using assms(2-3) eval_in_carrier b by(induct q) (auto simp add: degree_def m_assoc r_distr)
@@ -1845,11 +1920,309 @@
proposition (in cring) eval_is_hom:
assumes "subring K R" and "a \<in> carrier R"
shows "(\<lambda>p. (eval p) a) \<in> ring_hom (univ_poly (R \<lparr> carrier := K \<rparr>)) R"
- unfolding univ_poly_carrier_change_def'[OF assms(1)]
+ unfolding univ_poly_subring_def'[OF assms(1)]
using polynomial_in_carrier eval_in_carrier eval_poly_add eval_poly_mult assms(2)
by (auto intro!: ring_hom_memI
simp add: univ_poly_def degree_def
simp del: poly_add.simps poly_mult.simps)
+theorem (in domain) eval_cring_hom:
+ assumes "subring K R" and "a \<in> carrier R"
+ shows "ring_hom_cring (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. (eval p) a)"
+ unfolding ring_hom_cring_def ring_hom_cring_axioms_def
+ using domain.axioms(1)[OF univ_poly_subring_is_domain[OF assms(1)]]
+ eval_is_hom[OF assms] cring_axioms by auto
-end
\ No newline at end of file
+corollary (in domain) eval_ring_hom:
+ assumes "subring K R" and "a \<in> carrier R"
+ shows "ring_hom_ring (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. (eval p) a)"
+ using eval_cring_hom[OF assms] ring_hom_ringI2
+ unfolding ring_hom_cring_def ring_hom_cring_axioms_def cring_def by auto
+
+
+subsection \<open>The Reduction Map and Uniqueness of The Evaluation Homomorphism\<close>
+
+definition (in ring) reduction_map :: "('c \<Rightarrow> 'a) \<Rightarrow> 'c list \<Rightarrow> 'a list"
+ where "reduction_map h = (\<lambda>p. normalize (map h p))"
+
+(*
+lemma (in ring_hom_ring)
+ "(reduction_map h) \<in> ring_hom (univ_poly R) (univ_poly S)"
+ sorry
+*)
+
+
+subsection \<open>Divisibility of Polynomials\<close>
+
+definition pirreducible :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "pirreducible R p \<longleftrightarrow> irreducible (mult_of (univ_poly R)) p"
+
+definition pprime :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "pprime R p \<longleftrightarrow> prime (mult_of (univ_poly R)) p"
+
+definition rupture :: "_ \<Rightarrow> 'a list \<Rightarrow> _"
+ where "rupture R p = (univ_poly R) Quot (PIdl\<^bsub>(univ_poly R)\<^esub> p)"
+
+
+text \<open>Be aware of Nil!\<close>
+lemma (in domain) Nil_is_pirreducible: "pirreducible R []"
+ unfolding pirreducible_def using poly_mult_integral
+ by (auto intro!: irreducibleI simp add: Units_def univ_poly_def properfactor_def factor_def, force)
+
+lemma (in field) pprime_iff_ppirreducible:
+ assumes "polynomial R p" and "p \<noteq> []"
+ shows "pprime R p \<longleftrightarrow> pirreducible R p"
+proof -
+ have "p \<in> carrier (mult_of (univ_poly R))"
+ using assms unfolding univ_poly_def by auto
+ thus ?thesis
+ using principal_domain.primeness_condition[OF univ_poly_is_principal[OF field_axioms]]
+ unfolding pprime_def pirreducible_def by simp
+qed
+
+lemma (in field) rupture_field:
+ assumes "polynomial R p" and "p \<noteq> []"
+ shows "field (rupture R p) \<longleftrightarrow> pirreducible R p"
+proof -
+ have "p \<in> carrier (mult_of (univ_poly R))"
+ using assms(1-2) unfolding univ_poly_def by auto
+ thus ?thesis
+ using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF field_axioms]]
+ pprime_iff_ppirreducible[OF assms]
+ unfolding pprime_def rupture_def by simp
+qed
+
+lemma (in field) univ_poly_units:
+ "Units (univ_poly R) = { [ k ] | k. k \<in> carrier R - { \<zero> } }"
+proof
+ show "Units (univ_poly R) \<subseteq> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
+ proof
+ fix p assume "p \<in> Units (univ_poly R)"
+ then obtain q where p: "polynomial R p" and q: "polynomial R q" and pq: "poly_mult p q = [ \<one> ]"
+ unfolding Units_def univ_poly_def by auto
+ hence not_nil: "p \<noteq> []" and "q \<noteq> []"
+ using poly_mult_integral[OF p q] poly_mult_zero[OF p] by auto
+ hence "degree p = 0"
+ using poly_mult_degree_eq[OF p q] unfolding pq degree_def by simp
+ hence "length p = 1"
+ using not_nil unfolding degree_def by (metis One_nat_def Suc_pred length_greater_0_conv)
+ then obtain k where k: "p = [ k ]"
+ by (metis One_nat_def length_0_conv length_Suc_conv)
+ hence "k \<in> carrier R - { \<zero> }"
+ using p unfolding polynomial_def by auto
+ thus "p \<in> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
+ unfolding k by blast
+ qed
+next
+ show "{ [ k ] | k. k \<in> carrier R - { \<zero> } } \<subseteq> Units (univ_poly R)"
+ proof (auto)
+ fix k assume k: "k \<in> carrier R" "k \<noteq> \<zero>"
+ hence inv_k: "inv k \<in> carrier R" "inv k \<noteq> \<zero>" and "k \<otimes> inv k = \<one>" "inv k \<otimes> k = \<one>"
+ using subfield_m_inv[OF carrier_is_subfield, of k] by auto
+ hence "poly_mult [ k ] [ inv k ] = [ \<one> ]" and "poly_mult [ inv k ] [ k ] = [ \<one> ]"
+ by (auto simp add: degree_def k)
+ moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]"
+ using const_is_polynomial k inv_k by auto
+ ultimately show "[ k ] \<in> Units (univ_poly R)"
+ unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps)
+ qed
+qed
+
+corollary (in field) univ_poly_not_field: "\<not> field (univ_poly R)"
+proof -
+ have "[ \<one>, \<zero> ] \<in> carrier (univ_poly R) - { \<zero>\<^bsub>(univ_poly R)\<^esub> }"
+ and "[ \<one>, \<zero> ] \<notin> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
+ unfolding univ_poly_def polynomial_def by auto
+ thus ?thesis
+ using field.field_Units[of "univ_poly R"]
+ unfolding univ_poly_units by blast
+qed
+
+text \<open>A stronger version for one sense of rupture_field lemma.\<close>
+corollary (in field) rupture_field_imp_pirreducible:
+ assumes "polynomial R p" and "field (rupture R p)"
+ shows "p \<noteq> []" and "pirreducible R p"
+proof -
+ interpret UP: domain "univ_poly R"
+ using univ_poly_is_domain[OF domain_axioms] .
+
+ show "p \<noteq> []"
+ proof (rule ccontr)
+ assume "\<not> p \<noteq> []"
+ hence nil: "p = []" "p = \<zero>\<^bsub>(univ_poly R)\<^esub>"
+ unfolding univ_poly_def by simp+
+ hence "rupture R p = (univ_poly R) Quot { \<zero>\<^bsub>(univ_poly R)\<^esub> }"
+ unfolding rupture_def
+ using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] by simp
+ hence "rupture R p \<simeq> univ_poly R"
+ using UP.FactRing_zeroideal(1) by simp
+ then obtain h where h: "h \<in> ring_iso (rupture R p) (univ_poly R)"
+ unfolding is_ring_iso_def by blast
+ moreover have "ring (rupture R p)"
+ using assms(2) by (simp add: cring_def domain_def field_def)
+ ultimately interpret ring_hom_ring "rupture R p" "univ_poly R" h
+ unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def
+ using UP.is_ring by simp
+ have "field (univ_poly R)"
+ using field.ring_iso_imp_img_field[OF assms(2) h] by simp
+ thus False
+ using univ_poly_not_field by simp
+ qed
+ thus "pirreducible R p"
+ using rupture_field assms by simp
+qed
+
+lemma (in field) associated_polynomials_iff:
+ assumes "polynomial R p" and "polynomial R q"
+ shows "p \<sim>\<^bsub>(univ_poly R)\<^esub> q \<longleftrightarrow> (\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q)"
+proof
+ interpret UP: principal_domain "univ_poly R"
+ using univ_poly_is_principal[OF field_axioms] .
+
+ assume A: "p \<sim>\<^bsub>(univ_poly R)\<^esub> q"
+ then obtain r1 r2
+ where r1: "polynomial R r1" "p = poly_mult q r1"
+ and r2: "polynomial R r2" "q = poly_mult p r2"
+ unfolding associated_def factor_def univ_poly_def by auto
+
+ show "\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q"
+ proof (cases "p = []")
+ assume "p = []" thus ?thesis
+ using poly_mult_zero[OF r2(1)] r2(2) by auto
+ next
+ assume p: "p \<noteq> []" hence q: "q \<noteq> []"
+ using poly_mult_zero[OF r1(1)] r1(2) by auto
+ hence "p \<in> carrier (mult_of (univ_poly R))" and "q \<in> carrier (mult_of (univ_poly R))"
+ using p assms unfolding univ_poly_def by auto
+ moreover have "p \<sim>\<^bsub>mult_of (univ_poly R)\<^esub> q"
+ using p UP.assoc_imp_assoc_mult[OF _ _ A] assms unfolding univ_poly_def by auto
+ ultimately obtain r where r: "r \<in> Units (univ_poly R)" "p = q \<otimes>\<^bsub>(univ_poly R)\<^esub> r"
+ using UP.mult_of.associatedD2[of p q] UP.Units_mult_eq_Units by blast
+ then obtain k where k: "k \<in> carrier R - { \<zero> }" "r = [ k ]"
+ using univ_poly_units UP.m_comm[of q r] by auto
+ moreover have "p = poly_mult r q"
+ using r UP.m_comm[of q r] q assms unfolding Units_def univ_poly_def by auto
+ ultimately show ?thesis
+ using poly_mult_const(1)[OF assms(2) k(1)] unfolding k(2) by auto
+ qed
+next
+ assume "\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q"
+ then obtain k where k: "k \<in> carrier R - { \<zero> }" "p = map (\<lambda>a. k \<otimes> a) q"
+ by blast
+ hence inv_k: "inv k \<in> carrier R - { \<zero> }" "inv k \<otimes> k = \<one>"
+ using subfield_m_inv[OF carrier_is_subfield k(1)] by simp+
+ moreover have "map (\<lambda>a. inv k \<otimes> a) (map (\<lambda>a. k \<otimes> a) q) = q"
+ using inv_k polynomial_in_carrier[OF assms(2)] k(1) m_assoc m_comm by (induct q) (auto)
+ hence "q = map (\<lambda>a. inv k \<otimes> a) p"
+ using k(2) by simp
+ ultimately have "p = poly_mult q [ k ]" and "q = poly_mult p [ inv k ]"
+ using poly_mult_const(2)[OF assms(2) k(1)]
+ poly_mult_const(2)[OF assms(1) inv_k(1)] k(2) by auto
+ moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]"
+ using const_is_polynomial k inv_k by auto
+ ultimately show "p \<sim>\<^bsub>(univ_poly R)\<^esub> q"
+ unfolding univ_poly_def associated_def factor_def
+ by (auto simp del: poly_mult.simps)
+qed
+
+lemma (in cring) ideal_eq_carrier_iff: (* <- Move to Ideal.thy *)
+ assumes "a \<in> carrier R"
+ shows "carrier R = PIdl a \<longleftrightarrow> a \<in> Units R"
+proof
+ assume "carrier R = PIdl a"
+ hence "\<one> \<in> PIdl a"
+ by auto
+ then obtain b where "b \<in> carrier R" "\<one> = a \<otimes> b" "\<one> = b \<otimes> a"
+ unfolding cgenideal_def using m_comm[OF assms] by auto
+ thus "a \<in> Units R"
+ using assms unfolding Units_def by auto
+next
+ assume "a \<in> Units R"
+ then have inv_a: "inv a \<in> carrier R" "inv a \<otimes> a = \<one>"
+ by auto
+ have "carrier R \<subseteq> PIdl a"
+ proof
+ fix b assume "b \<in> carrier R"
+ hence "(b \<otimes> inv a) \<otimes> a = b" and "b \<otimes> inv a \<in> carrier R"
+ using m_assoc[OF _ inv_a(1) assms] inv_a by auto
+ thus "b \<in> PIdl a"
+ unfolding cgenideal_def by force
+ qed
+ thus "carrier R = PIdl a"
+ using assms by (simp add: cgenideal_eq_rcos r_coset_subset_G subset_antisym)
+qed
+
+text \<open>We don't suppose that x is algebraic, because, in our definition, [] is pirreducible.\<close>
+lemma (in field) exists_ker_generator_pirreducible:
+ assumes "x \<in> carrier R - { \<zero> }"
+ shows "\<exists>p. polynomial R p \<and>
+ pirreducible R p \<and>
+ a_kernel (univ_poly R) R (\<lambda>p. eval p x) = PIdl\<^bsub>(univ_poly R)\<^esub> p"
+ (is "\<exists>p. polynomial R p \<and> ?pirr R p \<and> ?a_ker p = ?PIdl p")
+proof -
+ interpret UP: principal_domain "univ_poly R"
+ using univ_poly_is_principal[OF field_axioms] by simp
+
+ have ker: "ideal (a_kernel (univ_poly R) R (\<lambda>p. eval p x)) (univ_poly R)"
+ using ring_hom_ring.kernel_is_ideal[OF eval_ring_hom[OF carrier_is_subring]] assms by simp
+ obtain p where in_carrier: "p \<in> carrier (univ_poly R)" and p: "?a_ker p = ?PIdl p"
+ using principalideal.generate[OF UP.principal_I[OF ker]] UP.cgenideal_eq_genideal by auto
+ hence poly: "polynomial R p"
+ unfolding univ_poly_def by simp
+
+ show ?thesis
+ proof (cases "p = []")
+ assume "p = []" thus ?thesis
+ using poly Nil_is_pirreducible p by auto
+ next
+ assume not_Nil: "p \<noteq> []"
+
+ have "eval (monon \<one> (Suc 0)) x = x"
+ using assms eval_monon[of \<one> x "Suc 0"] by auto
+ moreover have "monon \<one> (Suc 0) \<in> carrier (univ_poly R)"
+ using monon_is_polynomial unfolding univ_poly_def by auto
+ ultimately have "?a_ker p \<noteq> carrier (univ_poly R)"
+ unfolding a_kernel_def' using assms by force
+ hence not_unit: "p \<notin> Units (mult_of (univ_poly R))"
+ using p UP.ideal_eq_carrier_iff by auto
+
+ have "pprime R p"
+ unfolding pprime_def
+ proof (rule primeI[OF not_unit])
+ fix a b
+ assume "a \<in> carrier (mult_of (univ_poly R))"
+ and "b \<in> carrier (mult_of (univ_poly R))"
+ and "p divides\<^bsub>mult_of (univ_poly R)\<^esub> (a \<otimes>\<^bsub>mult_of (univ_poly R)\<^esub> b)"
+ then obtain c
+ where a: "polynomial R a" "a \<noteq> []" and b: "polynomial R b" "b \<noteq> []" and c: "polynomial R c" "c \<noteq> []"
+ and dvd: "poly_mult a b = poly_mult p c"
+ unfolding univ_poly_def factor_def by auto
+ hence "(eval a x) \<otimes> (eval b x) = (eval p x) \<otimes> (eval c x)"
+ using eval_poly_mult[of a b x] eval_poly_mult[of p c x] poly
+ polynomial_in_carrier assms by auto
+ moreover have "eval p x = \<zero>"
+ using p UP.cgenideal_self[OF in_carrier] unfolding a_kernel_def' by auto
+ ultimately have "(eval a x) \<otimes> (eval b x) = \<zero>"
+ using eval_in_carrier[OF polynomial_in_carrier[OF c(1)]] assms by auto
+ hence "(eval a x) = \<zero> \<or> (eval b x) = \<zero>"
+ using integral eval_in_carrier polynomial_in_carrier a b assms by auto
+ moreover
+ have "\<And>a. \<lbrakk> polynomial R a; a \<noteq> []; (eval a x) = \<zero> \<rbrakk> \<Longrightarrow> p divides\<^bsub>mult_of (univ_poly R)\<^esub> a"
+ proof -
+ fix a assume a: "polynomial R a" "a \<noteq> []" "(eval a x) = \<zero>"
+ hence "a \<in> ?PIdl p"
+ using p unfolding a_kernel_def' univ_poly_def by auto
+ hence "p divides\<^bsub>(univ_poly R)\<^esub> a"
+ using UP.m_comm[OF in_carrier] unfolding cgenideal_def factor_def by auto
+ thus "p divides\<^bsub>mult_of (univ_poly R)\<^esub> a"
+ using UP.divides_imp_divides_mult[OF in_carrier] a unfolding univ_poly_def by auto
+ qed
+ ultimately show "p divides\<^bsub>mult_of (univ_poly R)\<^esub> a \<or> p divides\<^bsub>mult_of (univ_poly R)\<^esub> b"
+ using a b by blast
+ qed
+ thus ?thesis
+ using poly p unfolding pprime_iff_ppirreducible[OF poly not_Nil] by auto
+ qed
+qed
+
+end
--- a/src/HOL/Algebra/QuotRing.thy Tue Jul 03 00:15:16 2018 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Tue Jul 03 10:07:24 2018 +0100
@@ -1022,6 +1022,18 @@
shows "R Quot (a_kernel R S h) \<simeq> S"
using FactRing_iso_set assms is_ring_iso_def by auto
+corollary (in ring) FactRing_zeroideal:
+ shows "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
+proof -
+ have "ring_hom_ring R R id"
+ using ring_axioms by (auto intro: ring_hom_ringI)
+ moreover have "a_kernel R R id = { \<zero> }"
+ unfolding a_kernel_def' by auto
+ ultimately show "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
+ using ring_hom_ring.FactRing_iso[of R R id]
+ ring_iso_sym[OF ideal.quotient_is_ring[OF zeroideal], of R] by auto
+qed
+
lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
proof -
let ?the_elem = "\<lambda>X. the_elem (h ` X)"
--- a/src/HOL/Algebra/Ring_Divisibility.thy Tue Jul 03 00:15:16 2018 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Tue Jul 03 10:07:24 2018 +0100
@@ -4,30 +4,10 @@
(* ************************************************************************** *)
theory Ring_Divisibility
-imports Ideal Divisibility QuotRing
+imports Ideal Divisibility QuotRing Multiplicative_Group
begin
-section \<open>Definitions ported from @{text "Multiplicative_Group.thy"}\<close>
-
-definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
- "mult_of R \<equiv> \<lparr> carrier = carrier R - { \<zero>\<^bsub>R\<^esub> }, mult = mult R, one = \<one>\<^bsub>R\<^esub> \<rparr>"
-
-lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - { \<zero>\<^bsub>R\<^esub> }"
- by (simp add: mult_of_def)
-
-lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
- by (simp add: mult_of_def)
-
-lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
- by (simp add: mult_of_def fun_eq_iff nat_pow_def)
-
-lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
- by (simp add: mult_of_def)
-
-lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
-
-
section \<open>The Arithmetic of Rings\<close>
text \<open>In this section we study the links between the divisibility theory and that of rings\<close>
@@ -127,14 +107,14 @@
lemma (in cring) to_contain_is_to_divide:
assumes "a \<in> carrier R" "b \<in> carrier R"
shows "(PIdl b \<subseteq> PIdl a) = (a divides b)"
-proof
+proof
show "PIdl b \<subseteq> PIdl a \<Longrightarrow> a divides b"
proof -
assume "PIdl b \<subseteq> PIdl a"
hence "b \<in> PIdl a"
by (meson assms(2) local.ring_axioms ring.cgenideal_self subsetCE)
thus ?thesis
- unfolding factor_def cgenideal_def using m_comm assms(1) by blast
+ unfolding factor_def cgenideal_def using m_comm assms(1) by blast
qed
show "a divides b \<Longrightarrow> PIdl b \<subseteq> PIdl a"
proof -
@@ -166,15 +146,23 @@
lemma (in domain) divides_imp_divides_mult [simp]:
"\<lbrakk> a \<in> carrier R; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
a divides\<^bsub>R\<^esub> b \<Longrightarrow> a divides\<^bsub>(mult_of R)\<^esub> b"
- unfolding factor_def using integral_iff by auto
+ unfolding factor_def using integral_iff by auto
lemma assoc_mult_imp_assoc [simp]: "a \<sim>\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>R\<^esub> b"
unfolding associated_def by simp
lemma (in domain) assoc_imp_assoc_mult [simp]:
- "\<lbrakk> a \<in> carrier R - { \<zero> } ; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
- a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
- unfolding associated_def by simp
+ assumes "a \<in> carrier R - { \<zero> }" and "b \<in> carrier R"
+ shows "a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+proof -
+ assume A: "a \<sim>\<^bsub>R\<^esub> b"
+ then obtain c where "c \<in> carrier R" "a = b \<otimes> c"
+ unfolding associated_def factor_def by auto
+ hence "b \<in> carrier R - { \<zero> }"
+ using assms integral by auto
+ thus "a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+ using A assms(1) unfolding associated_def by simp
+qed
lemma (in domain) Units_mult_eq_Units [simp]: "Units (mult_of R) = Units R"
unfolding Units_def using insert_Diff integral_iff by auto
@@ -198,7 +186,7 @@
using c A integral_iff by auto
thus "properfactor R b a"
using A divides_imp_divides_mult[of a b] unfolding properfactor_def
- by (meson DiffI divides_mult_imp_divides empty_iff insert_iff)
+ by (meson DiffI divides_mult_imp_divides empty_iff insert_iff)
qed
lemma (in domain) properfactor_imp_properfactor_mult:
@@ -269,7 +257,7 @@
qed
qed
moreover have "PIdl p \<noteq> carrier R" using A primeideal.I_notcarr by auto
- ultimately show False by simp
+ ultimately show False by simp
qed
next
{ fix a assume "a \<in> PIdl p" and a: "a \<noteq> \<zero>"
@@ -333,12 +321,12 @@
from \<open>finite S\<close> and \<open>S \<subseteq> (\<Union>i. I i)\<close> have "\<exists>n. S \<subseteq> I n"
proof (induct S set: "finite")
- case empty thus ?case by simp
+ case empty thus ?case by simp
next
case (insert x S')
then obtain n m where m: "S' \<subseteq> I m" and n: "x \<in> I n" by blast
hence "insert x S' \<subseteq> I (max m n)"
- by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans)
+ by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans)
thus ?case by blast
qed
then obtain n where "S \<subseteq> I n" by blast
@@ -427,7 +415,7 @@
using S_builder_incl[of R J] J S_def I_def
by (meson additive_subgroup.a_subset dual_order.trans ideal.axioms(1) subset_Idl_subset)
ultimately obtain n where "\<And>k. k \<ge> n \<Longrightarrow> I k = I n"
- using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le)
+ using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le)
hence "J = Idl (S_builder R J n)"
using S_builder_const1[OF J, of n] S_builder_const2[OF J, of n] I_def S_def
by (meson Suc_n_not_le_n le_cases)
@@ -436,7 +424,7 @@
by (meson J S_builder_incl ideal.Icarr set_rev_mp subsetI)
qed
thus ?thesis
- by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
+ by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
qed
lemma (in noetherian_domain) wfactors_exists:
@@ -450,7 +438,7 @@
have "\<not> irreducible (mult_of R) x"
proof (rule ccontr)
assume "\<not> (\<not> irreducible (mult_of R) x)" hence "irreducible (mult_of R) x" by simp
- hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto
+ hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto
thus False using A by auto
qed
moreover have "\<not> x \<in> Units (mult_of R)"
@@ -472,11 +460,11 @@
using fs_a fs_b a b mult_of.wfactors_mult by simp
moreover have "set (fs_a @ fs_b) \<subseteq> carrier (mult_of R)"
using fs_a fs_b by auto
- ultimately show False using A by blast
+ ultimately show False using A by blast
qed
thus ?thesis using a b b_properfactor mult_of.m_comm by blast
qed } note aux_lemma = this
-
+
assume A: "\<not> ?P x"
define f :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -485,7 +473,7 @@
where "factor_seq = rec_nat x (\<lambda>n y. (SOME a. f a y))"
define I where "I = (\<lambda>i. PIdl (factor_seq i))"
have factor_seq_props:
- "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and>
+ "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and>
(factor_seq n) \<in> carrier (mult_of R) \<and> \<not> ?P (factor_seq n)" (is "\<And>n. ?Q n")
proof -
fix n show "?Q n"
@@ -519,7 +507,7 @@
qed
have in_carrier: "\<And>i. factor_seq i \<in> carrier R"
- using factor_seq_props by simp
+ using factor_seq_props by simp
hence "\<And>i. ideal (I i) R"
using I_def by (simp add: cgenideal_ideal)
@@ -582,11 +570,12 @@
hence "q divides p"
using to_contain_is_to_divide[of q p] using assms(1) J(1-2) by simp
hence q_div_p: "q divides\<^bsub>(mult_of R)\<^esub> p"
- using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>)
+ using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>)
show "J = PIdl p \<or> J = carrier R"
proof (cases "q \<in> Units R")
case True thus ?thesis
- by (metis J(1) Units_r_inv_ex cgenideal_self ideal.I_r_closed ideal.one_imp_carrier q(1) q(2))
+ by (metis J(3) Unit_eq_dividesone cgenideal_eq_genideal genideal_one one_closed q
+ subset_antisym to_contain_is_to_divide)
next
case False
have q_in_carr: "q \<in> carrier (mult_of R)"
@@ -749,12 +738,12 @@
next
fix I assume I: "ideal I R" show "principalideal I R"
proof (cases "I = { \<zero> }")
- case True thus ?thesis by (simp add: zeropideal)
+ case True thus ?thesis by (simp add: zeropideal)
next
case False hence A: "I - { \<zero> } \<noteq> {}"
- using I additive_subgroup.zero_closed ideal.axioms(1) by auto
+ using I additive_subgroup.zero_closed ideal.axioms(1) by auto
define phi_img :: "nat set" where "phi_img = (\<phi> ` (I - { \<zero> }))"
- hence "phi_img \<noteq> {}" using A by simp
+ hence "phi_img \<noteq> {}" using A by simp
then obtain m where "m \<in> phi_img" "\<And>k. k \<in> phi_img \<Longrightarrow> m \<le> k"
using exists_least_iff[of "\<lambda>n. n \<in> phi_img"] not_less by force
then obtain a where a: "a \<in> I - { \<zero> }" "\<And>b. b \<in> I - { \<zero> } \<Longrightarrow> \<phi> a \<le> \<phi> b"
@@ -773,7 +762,7 @@
unfolding cgenideal_def using m_comm[of a] ideal.Icarr[OF I] a(1) by auto
hence 1: "\<phi> r < \<phi> a \<and> r \<noteq> \<zero>"
using eucl_div(4) b(2) by auto
-
+
have "r = (\<ominus> (a \<otimes> q)) \<oplus> b"
using eucl_div(1-3) a(1) b(1) ideal.Icarr[OF I] r_neg1 by auto
moreover have "\<ominus> (a \<otimes> q) \<in> I"
@@ -803,4 +792,4 @@
by blast
qed
-end
\ No newline at end of file
+end