--- a/src/HOL/Algebra/Polynomials.thy Thu Jul 19 17:28:13 2018 +0200
+++ b/src/HOL/Algebra/Polynomials.thy Thu Jul 19 23:23:10 2018 +0200
@@ -4,6 +4,7 @@
theory Polynomials
imports Ring Ring_Divisibility Subrings
+
begin
section \<open>Polynomials\<close>
@@ -13,14 +14,14 @@
abbreviation lead_coeff :: "'a list \<Rightarrow> 'a"
where "lead_coeff \<equiv> hd"
-definition degree :: "'a list \<Rightarrow> nat"
- where "degree p = length p - 1"
+abbreviation degree :: "'a list \<Rightarrow> nat"
+ where "degree p \<equiv> length p - 1"
-definition polynomial :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
- where "polynomial R p \<longleftrightarrow> p = [] \<or> (set p \<subseteq> carrier R \<and> lead_coeff p \<noteq> \<zero>\<^bsub>R\<^esub>)"
+definition polynomial :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a list \<Rightarrow> bool" ("polynomial\<index>")
+ where "polynomial\<^bsub>R\<^esub> K p \<longleftrightarrow> p = [] \<or> (set p \<subseteq> K \<and> lead_coeff p \<noteq> \<zero>\<^bsub>R\<^esub>)"
-definition (in ring) monon :: "'a \<Rightarrow> nat \<Rightarrow> 'a list"
- where "monon a n = a # (replicate n \<zero>\<^bsub>R\<^esub>)"
+definition (in ring) monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a list"
+ where "monom a n = a # (replicate n \<zero>\<^bsub>R\<^esub>)"
fun (in ring) eval :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a"
where
@@ -57,7 +58,8 @@
else (dense_repr (tl p)))"
fun (in ring) of_dense :: "('a \<times> nat) list \<Rightarrow> 'a list"
- where "of_dense dl = foldr (\<lambda>(a, n) l. poly_add (monon a n) l) dl []"
+ where "of_dense dl = foldr (\<lambda>(a, n) l. poly_add (monom a n) l) dl []"
+
subsection \<open>Basic Properties\<close>
@@ -65,51 +67,45 @@
context ring
begin
-lemma polynomialI [intro]: "\<lbrakk> set p \<subseteq> carrier R; lead_coeff p \<noteq> \<zero> \<rbrakk> \<Longrightarrow> polynomial R p"
+lemma polynomialI [intro]: "\<lbrakk> set p \<subseteq> K; lead_coeff p \<noteq> \<zero> \<rbrakk> \<Longrightarrow> polynomial K p"
unfolding polynomial_def by auto
-lemma polynomial_in_carrier [intro]: "polynomial R p \<Longrightarrow> set p \<subseteq> carrier R"
+lemma polynomial_incl: "polynomial K p \<Longrightarrow> set p \<subseteq> K"
unfolding polynomial_def by auto
-lemma lead_coeff_not_zero [intro]: "polynomial R (a # p) \<Longrightarrow> a \<in> carrier R - { \<zero> }"
+lemma monom_in_carrier [intro]: "a \<in> carrier R \<Longrightarrow> set (monom a n) \<subseteq> carrier R"
+ unfolding monom_def by auto
+
+lemma lead_coeff_not_zero: "polynomial K (a # p) \<Longrightarrow> a \<in> K - { \<zero> }"
unfolding polynomial_def by simp
-lemma zero_is_polynomial [intro]: "polynomial R []"
+lemma zero_is_polynomial [intro]: "polynomial K []"
unfolding polynomial_def by simp
-lemma const_is_polynomial [intro]: "a \<in> carrier R - { \<zero> } \<Longrightarrow> polynomial R [ a ]"
+lemma const_is_polynomial [intro]: "a \<in> K - { \<zero> } \<Longrightarrow> polynomial K [ a ]"
unfolding polynomial_def by auto
-lemma monon_is_polynomial [intro]: "a \<in> carrier R - { \<zero> } \<Longrightarrow> polynomial R (monon a n)"
- unfolding polynomial_def monon_def by auto
-
-lemma monon_in_carrier [intro]: "a \<in> carrier R \<Longrightarrow> set (monon a n) \<subseteq> carrier R"
- unfolding monon_def by auto
-
-lemma normalize_gives_polynomial: "set p \<subseteq> carrier R \<Longrightarrow> polynomial R (normalize p)"
+lemma normalize_gives_polynomial: "set p \<subseteq> K \<Longrightarrow> polynomial K (normalize p)"
by (induction p) (auto simp add: polynomial_def)
lemma normalize_in_carrier: "set p \<subseteq> carrier R \<Longrightarrow> set (normalize p) \<subseteq> carrier R"
- using normalize_gives_polynomial polynomial_in_carrier by simp
+ by (induction p) (auto)
-lemma normalize_idem: "polynomial R p \<Longrightarrow> normalize p = p"
+lemma normalize_polynomial: "polynomial K p \<Longrightarrow> normalize p = p"
unfolding polynomial_def by (cases p) (auto)
+lemma normalize_idem: "normalize ((normalize p) @ q) = normalize (p @ q)"
+ by (induct p) (auto)
+
lemma normalize_length_le: "length (normalize p) \<le> length p"
by (induction p) (auto)
lemma eval_in_carrier: "\<lbrakk> set p \<subseteq> carrier R; x \<in> carrier R \<rbrakk> \<Longrightarrow> (eval p) x \<in> carrier R"
by (induction p) (auto)
-lemma eval_poly_in_carrier: "\<lbrakk> polynomial R p; x \<in> carrier R \<rbrakk> \<Longrightarrow> (eval p) x \<in> carrier R"
- using eval_in_carrier unfolding polynomial_def by auto
-
lemma coeff_in_carrier [simp]: "set p \<subseteq> carrier R \<Longrightarrow> (coeff p) i \<in> carrier R"
by (induction p) (auto)
-lemma poly_coeff_in_carrier [simp]: "polynomial R p \<Longrightarrow> coeff p i \<in> carrier R"
- using coeff_in_carrier unfolding polynomial_def by auto
-
lemma lead_coeff_simp [simp]: "p \<noteq> [] \<Longrightarrow> (coeff p) (degree p) = lead_coeff p"
by (metis coeff.simps(2) list.exhaust_sel)
@@ -119,10 +115,8 @@
next
case (Cons a p)
have "map (coeff (a # p)) (rev [0..<length (a # p)]) =
- map (coeff (a # p)) ((length p) # (rev [0..<length p]))"
- by simp
- also have " ... = a # (map (coeff p) (rev [0..<length p]))"
- using degree_def[of "a # p"] by auto
+ a # (map (coeff p) (rev [0..<length p]))"
+ by auto
also have " ... = a # p"
using Cons by simp
finally show ?case .
@@ -163,19 +157,19 @@
using coeff_list[of p] by (metis atLeast_upt image_set set_rev)
lemma coeff_length: "\<And>i. i \<ge> length p \<Longrightarrow> (coeff p) i = \<zero>"
- by (induction p) (auto simp add: degree_def)
+ by (induction p) (auto)
lemma coeff_degree: "\<And>i. i > degree p \<Longrightarrow> (coeff p) i = \<zero>"
- using coeff_length by (simp add: degree_def)
+ using coeff_length by (simp)
lemma replicate_zero_coeff [simp]: "coeff (replicate n \<zero>) = (\<lambda>_. \<zero>)"
by (induction n) (auto)
lemma scalar_coeff: "a \<in> carrier R \<Longrightarrow> coeff (map (\<lambda>b. a \<otimes> b) p) = (\<lambda>i. a \<otimes> (coeff p) i)"
- by (induction p) (auto simp add:degree_def)
+ by (induction p) (auto)
-lemma monon_coeff: "coeff (monon a n) = (\<lambda>i. if i = n then a else \<zero>)"
- unfolding monon_def by (induction n) (auto simp add: degree_def)
+lemma monom_coeff: "coeff (monom a n) = (\<lambda>i. if i = n then a else \<zero>)"
+ unfolding monom_def by (induction n) (auto)
lemma coeff_img:
"(coeff p) ` {..< length p} = set p"
@@ -184,18 +178,17 @@
using coeff_img_restrict
proof (simp)
show coeff_img_up: "(coeff p) ` { length p ..} = { \<zero> }"
- using coeff_length[of p] unfolding degree_def by force
+ using coeff_length[of p] by force
from coeff_img_up and coeff_img_restrict[of p]
show "(coeff p) ` UNIV = (set p) \<union> { \<zero> }"
by force
qed
lemma degree_def':
- assumes "polynomial R p"
+ assumes "polynomial K p"
shows "degree p = (LEAST n. \<forall>i. i > n \<longrightarrow> (coeff p) i = \<zero>)"
proof (cases p)
- case Nil thus ?thesis
- unfolding degree_def by auto
+ case Nil thus ?thesis by auto
next
define P where "P = (\<lambda>n. \<forall>i. i > n \<longrightarrow> (coeff p) i = \<zero>)"
@@ -212,7 +205,7 @@
qed
lemma coeff_iff_polynomial_cond:
- assumes "polynomial R p1" and "polynomial R p2"
+ assumes "polynomial K p1" and "polynomial K p2"
shows "p1 = p2 \<longleftrightarrow> coeff p1 = coeff p2"
proof
show "p1 = p2 \<Longrightarrow> coeff p1 = coeff p2"
@@ -225,12 +218,11 @@
proof (cases)
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))
+ using deg_eq by (simp add: Nitpick.size_list_simp(2))
thus ?thesis
using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
next
- { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial R p2"
+ { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2"
have "p2 = []"
proof (rule ccontr)
assume "p2 \<noteq> []"
@@ -338,11 +330,11 @@
next
case (Cons a p)
have "coeff (normalize p) (length p) = \<zero>"
- using normalize_length_le[of p] coeff_degree[of "normalize p"] unfolding degree_def
+ using normalize_length_le[of p] coeff_degree[of "normalize p"]
by (metis One_nat_def coeff.simps(1) diff_less length_0_conv
less_imp_diff_less nat_neq_iff neq0_conv not_le zero_less_Suc)
then show ?case
- using Cons by (cases "a = \<zero>") (auto simp add: degree_def)
+ using Cons by (cases "a = \<zero>") (auto)
qed
lemma append_coeff:
@@ -353,7 +345,7 @@
next
case (Cons a p)
have "coeff ((a # p) @ q) = (\<lambda>i. if i = length p + length q then a else (coeff (p @ q)) i)"
- by (auto simp add: degree_def)
+ by auto
also have " ... = (\<lambda>i. if i = length p + length q then a
else if i < length q then (coeff q) i
else (coeff p) (i - length q))"
@@ -365,76 +357,78 @@
else if i - length q = length p then a else (coeff p) (i - length q))"
by fastforce
also have " ... = (\<lambda>i. if i < length q then (coeff q) i else (coeff (a # p)) (i - length q))"
- by (auto simp add: degree_def)
+ by auto
finally show ?case .
qed
lemma prefix_replicate_zero_coeff: "coeff p = coeff ((replicate n \<zero>) @ p)"
using append_coeff[of "replicate n \<zero>" p] replicate_zero_coeff[of n] coeff_length[of p] by auto
-end
+(* ========================================================================== *)
+context
+ fixes K :: "'a set" assumes K: "subring K R"
+begin
+
+lemma polynomial_in_carrier [intro]: "polynomial K p \<Longrightarrow> set p \<subseteq> carrier R"
+ unfolding polynomial_def using subringE(1)[OF K] by auto
+
+lemma carrier_polynomial [intro]: "polynomial K p \<Longrightarrow> polynomial (carrier R) p"
+ unfolding polynomial_def using subringE(1)[OF K] by auto
+
+lemma append_is_polynomial: "\<lbrakk> polynomial K p; p \<noteq> [] \<rbrakk> \<Longrightarrow> polynomial K (p @ (replicate n \<zero>))"
+ unfolding polynomial_def using subringE(2)[OF K] by auto
+
+lemma lead_coeff_in_carrier: "polynomial K (a # p) \<Longrightarrow> a \<in> carrier R - { \<zero> }"
+ unfolding polynomial_def using subringE(1)[OF K] by auto
+
+lemma monom_is_polynomial [intro]: "a \<in> K - { \<zero> } \<Longrightarrow> polynomial K (monom a n)"
+ unfolding polynomial_def monom_def using subringE(2)[OF K] by auto
+
+lemma eval_poly_in_carrier: "\<lbrakk> polynomial K p; x \<in> carrier R \<rbrakk> \<Longrightarrow> (eval p) x \<in> carrier R"
+ using eval_in_carrier[OF polynomial_in_carrier] .
+
+lemma poly_coeff_in_carrier [simp]: "polynomial K p \<Longrightarrow> coeff p i \<in> carrier R"
+ using coeff_in_carrier[OF polynomial_in_carrier] .
+
+end (* of fixed K context. *)
+(* ========================================================================== *)
-subsection \<open>Polynomial addition\<close>
+subsection \<open>Polynomial Addition\<close>
-context ring
+(* ========================================================================== *)
+context
+ fixes K :: "'a set" assumes K: "subring K R"
begin
lemma poly_add_is_polynomial:
- assumes "set p1 \<subseteq> carrier R" and "set p2 \<subseteq> carrier R"
- shows "polynomial R (poly_add p1 p2)"
+ assumes "set p1 \<subseteq> K" and "set p2 \<subseteq> K"
+ shows "polynomial K (poly_add p1 p2)"
proof -
- { fix p1 p2 assume A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "length p1 \<ge> length p2"
- hence "polynomial R (poly_add p1 p2)"
+ { fix p1 p2 assume A: "set p1 \<subseteq> K" "set p2 \<subseteq> K" "length p1 \<ge> length p2"
+ hence "polynomial K (poly_add p1 p2)"
proof -
define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
- hence set_p2': "set p2' \<subseteq> carrier R"
- using A(2) by auto
- have "set (map (\<lambda>(a, b). a \<oplus> b) (zip p1 p2')) \<subseteq> carrier R"
- proof
- fix c assume "c \<in> set (map (\<lambda>(a, b). a \<oplus> b) (zip p1 p2'))"
- then obtain t where "t \<in> set (zip p1 p2')" and c: "c = fst t \<oplus> snd t"
- by auto
- then obtain a b where "a \<in> set p1" "a = fst t"
- and "b \<in> set p2'" "b = snd t"
- by (metis set_zip_leftD set_zip_rightD surjective_pairing)
- thus "c \<in> carrier R"
- using A(1) set_p2' c by auto
- qed
+ hence "set p2' \<subseteq> K" and "length p1 = length p2'"
+ using A(2-3) subringE(2)[OF K] by auto
+ hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
+ using A(1) subringE(7)[OF K]
+ by (induct p1) (auto, metis set_ConsD set_mp set_zip_leftD set_zip_rightD)
thus ?thesis
unfolding p2'_def using normalize_gives_polynomial A(3) by simp
qed }
thus ?thesis
- using assms by simp
+ using assms by auto
qed
-lemma poly_add_in_carrier:
- "\<lbrakk> set p1 \<subseteq> carrier R; set p2 \<subseteq> carrier R \<rbrakk> \<Longrightarrow> set (poly_add p1 p2) \<subseteq> carrier R"
- using poly_add_is_polynomial polynomial_in_carrier by simp
-
-lemma poly_add_closed: "\<lbrakk> polynomial R p1; polynomial R p2 \<rbrakk> \<Longrightarrow> polynomial R (poly_add p1 p2)"
- using poly_add_is_polynomial polynomial_in_carrier by auto
-
-lemma poly_add_length_le: "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
-proof -
- { fix p1 p2 :: "'a list" assume A: "length p1 \<ge> length p2"
- hence "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
- proof -
- let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
- have "length (map2 (\<oplus>) p1 ?p2) = length p1"
- using A by auto
- thus ?thesis
- using normalize_length_le[of "map2 (\<oplus>) p1 ?p2"] A by auto
- qed }
- thus ?thesis
- by (metis le_cases max.commute poly_add.simps)
-qed
+lemma poly_add_closed: "\<lbrakk> polynomial K p1; polynomial K p2 \<rbrakk> \<Longrightarrow> polynomial K (poly_add p1 p2)"
+ using poly_add_is_polynomial polynomial_incl by simp
lemma poly_add_length_eq:
- assumes "polynomial R p1" "polynomial R p2" and "length p1 \<noteq> length p2"
+ assumes "polynomial K p1" "polynomial K p2" and "length p1 \<noteq> length p2"
shows "length (poly_add p1 p2) = max (length p1) (length p2)"
proof -
- { fix p1 p2 assume A: "polynomial R p1" "polynomial R p2" "length p1 > length p2"
+ { fix p1 p2 assume A: "polynomial K p1" "polynomial K p2" "length p1 > length p2"
hence "length (poly_add p1 p2) = max (length p1) (length p2)"
proof -
let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
@@ -445,7 +439,7 @@
hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
by simp
moreover have "lead_coeff p1 \<in> carrier R"
- using p1 A(1) unfolding polynomial_def by auto
+ using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
using A(3) by auto
moreover have "lead_coeff p1 \<noteq> \<zero>"
@@ -459,15 +453,31 @@
using assms by auto
qed
-lemma poly_add_degree: "degree (poly_add p1 p2) \<le> max (degree p1) (degree p2)"
- unfolding degree_def using poly_add_length_le
- by (meson diff_le_mono le_max_iff_disj)
-
lemma poly_add_degree_eq:
- assumes "polynomial R p1" "polynomial R p2" and "degree p1 \<noteq> degree p2"
+ assumes "polynomial K p1" "polynomial K p2" and "degree p1 \<noteq> degree p2"
shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)"
using poly_add_length_eq[of p1 p2] assms
- by (metis (no_types, lifting) degree_def diff_le_mono max.absorb_iff1 max_def)
+ by (metis (no_types, lifting) diff_le_mono max.absorb_iff1 max_def)
+
+end (* of fixed K context. *)
+(* ========================================================================== *)
+
+lemma poly_add_in_carrier:
+ "\<lbrakk> set p1 \<subseteq> carrier R; set p2 \<subseteq> carrier R \<rbrakk> \<Longrightarrow> set (poly_add p1 p2) \<subseteq> carrier R"
+ using polynomial_incl[OF poly_add_is_polynomial[OF carrier_is_subring]] by simp
+
+lemma poly_add_length_le: "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+proof -
+ { fix p1 p2 :: "'a list" assume A: "length p1 \<ge> length p2"
+ let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+ have "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+ using normalize_length_le[of "map2 (\<oplus>) p1 ?p2"] A by auto }
+ thus ?thesis
+ by (metis le_cases max.commute poly_add.simps)
+qed
+
+lemma poly_add_degree: "degree (poly_add p1 p2) \<le> max (degree p1) (degree p2)"
+ using poly_add_length_le by (meson diff_le_mono le_max_iff_disj)
lemma poly_add_coeff_aux:
assumes "length p1 \<ge> length p2"
@@ -527,13 +537,43 @@
using poly_add_coeff[OF assms] poly_add_coeff[OF assms(2) assms(1)]
coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] add.m_comm by auto
thus ?thesis
- using coeff_iff_polynomial_cond poly_add_is_polynomial assms by auto
+ using coeff_iff_polynomial_cond[OF
+ poly_add_is_polynomial[OF carrier_is_subring assms]
+ poly_add_is_polynomial[OF carrier_is_subring assms(2,1)]] by simp
+qed
+
+lemma poly_add_monom:
+ assumes "set p \<subseteq> carrier R" and "a \<in> carrier R - { \<zero> }"
+ shows "poly_add (monom a (length p)) p = a # p"
+ unfolding monom_def using assms by (induction p) (auto)
+
+lemma poly_add_append_replicate:
+ assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R"
+ shows "poly_add (p @ (replicate (length q) \<zero>)) q = normalize (p @ q)"
+proof -
+ have "map2 (\<oplus>) (p @ (replicate (length q) \<zero>)) ((replicate (length p) \<zero>) @ q) = p @ q"
+ using assms by (induct p) (induct q, auto)
+ thus ?thesis by simp
qed
-lemma poly_add_monon:
- assumes "set p \<subseteq> carrier R" and "a \<in> carrier R - { \<zero> }"
- shows "poly_add (monon a (length p)) p = a # p"
- unfolding monon_def using assms by (induction p) (auto)
+lemma poly_add_append_zero:
+ assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R"
+ shows "poly_add (p @ [ \<zero> ]) (q @ [ \<zero> ]) = normalize ((poly_add p q) @ [ \<zero> ])"
+proof -
+ have in_carrier: "set (p @ [ \<zero> ]) \<subseteq> carrier R" "set (q @ [ \<zero> ]) \<subseteq> carrier R"
+ using assms by auto
+ have "coeff (poly_add (p @ [ \<zero> ]) (q @ [ \<zero> ])) = coeff ((poly_add p q) @ [ \<zero> ])"
+ using append_coeff[of p "[ \<zero> ]"] poly_add_coeff[OF in_carrier]
+ append_coeff[of q "[ \<zero> ]"] append_coeff[of "poly_add p q" "[ \<zero> ]"]
+ poly_add_coeff[OF assms] assms[THEN coeff_in_carrier] by auto
+ hence "coeff (poly_add (p @ [ \<zero> ]) (q @ [ \<zero> ])) = coeff (normalize ((poly_add p q) @ [ \<zero> ]))"
+ using normalize_coeff by simp
+ moreover have "set ((poly_add p q) @ [ \<zero> ]) \<subseteq> carrier R"
+ using poly_add_in_carrier[OF assms] by simp
+ ultimately show ?thesis
+ using coeff_iff_polynomial_cond[OF poly_add_is_polynomial[OF carrier_is_subring in_carrier]
+ normalize_gives_polynomial] by simp
+qed
lemma poly_add_normalize_aux:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
@@ -595,8 +635,7 @@
poly_add ((replicate (length p1 - length (normalize p1)) \<zero>) @ normalize p1) p2"
using normalize_def'[of p1] by simp
also have " ... = poly_add (normalize p1) p2"
- using aux_lemma[OF
- polynomial_in_carrier[OF normalize_gives_polynomial[OF assms(1)]] assms(2)] by simp
+ using aux_lemma[OF normalize_in_carrier[OF assms(1)] assms(2)] by simp
finally show ?thesis .
qed
@@ -607,48 +646,32 @@
and "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)"
proof -
show "poly_add p1 p2 = poly_add p1 (normalize p2)"
- using poly_add_normalize_aux[OF assms(2) assms(1)] poly_add_comm
- polynomial_in_carrier normalize_gives_polynomial assms by auto
+ unfolding poly_add_comm[OF assms] poly_add_normalize_aux[OF assms(2) assms(1)]
+ poly_add_comm[OF normalize_in_carrier[OF assms(2)] assms(1)] by simp
next
show "poly_add p1 p2 = poly_add (normalize p1) p2"
- using poly_add_normalize_aux[OF assms] by simp
- also have " ... = poly_add p2 (normalize p1)"
- using poly_add_comm polynomial_in_carrier normalize_gives_polynomial assms by auto
+ using poly_add_normalize_aux[OF assms] .
also have " ... = poly_add (normalize p2) (normalize p1)"
- using poly_add_normalize_aux polynomial_in_carrier normalize_gives_polynomial assms by auto
- also have " ... = poly_add (normalize p1) (normalize p2)"
- using poly_add_comm polynomial_in_carrier normalize_gives_polynomial assms by auto
- finally show "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)" .
+ unfolding poly_add_comm[OF normalize_in_carrier[OF assms(1)] assms(2)]
+ poly_add_normalize_aux[OF assms(2) normalize_in_carrier[OF assms(1)]] by simp
+ finally show "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)"
+ unfolding poly_add_comm[OF assms[THEN normalize_in_carrier]] .
qed
lemma poly_add_zero':
assumes "set p \<subseteq> carrier R"
shows "poly_add p [] = normalize p" and "poly_add [] p = normalize p"
proof -
- show "poly_add p [] = normalize p" using assms
- proof (induction p)
- case Nil thus ?case by simp
- next
- { fix p assume A: "set p \<subseteq> carrier R" "lead_coeff p \<noteq> \<zero>"
- hence "polynomial R p"
- unfolding polynomial_def by simp
- moreover have "coeff (poly_add p []) = coeff p"
- using poly_add_coeff[of p "[]"] A(1) by simp
- ultimately have "poly_add p [] = p"
- using coeff_iff_polynomial_cond[OF
- poly_add_is_polynomial[OF A(1), of "[]"], of p] by simp }
- note aux_lemma = this
- case (Cons a p) thus ?case
- using aux_lemma[of "a # p"] by auto
- qed
- thus "poly_add [] p = normalize p"
- using poly_add_comm[OF assms, of "[]"] by simp
+ have "map2 (\<oplus>) p (replicate (length p) \<zero>) = p"
+ using assms by (induct p) (auto)
+ thus "poly_add p [] = normalize p" and "poly_add [] p = normalize p"
+ using poly_add_comm[OF assms, of "[]"] by simp+
qed
lemma poly_add_zero:
- assumes "polynomial R p"
+ assumes "subring K R" "polynomial K p"
shows "poly_add p [] = p" and "poly_add [] p = p"
- using poly_add_zero' normalize_idem polynomial_in_carrier assms by auto
+ using poly_add_zero' normalize_polynomial polynomial_in_carrier assms by auto
lemma poly_add_replicate_zero':
assumes "set p \<subseteq> carrier R"
@@ -665,9 +688,10 @@
qed
lemma poly_add_replicate_zero:
- assumes "polynomial R p"
+ assumes "subring K R" "polynomial K p"
shows "poly_add p (replicate n \<zero>) = p" and "poly_add (replicate n \<zero>) p = p"
- using poly_add_replicate_zero' normalize_idem polynomial_in_carrier assms by auto
+ using poly_add_replicate_zero' normalize_polynomial polynomial_in_carrier assms by auto
+
subsection \<open>Dense Representation\<close>
@@ -675,14 +699,17 @@
lemma dense_repr_replicate_zero: "dense_repr ((replicate n \<zero>) @ p) = dense_repr p"
by (induction n) (auto)
+lemma dense_repr_normalize: "dense_repr (normalize p) = dense_repr p"
+ by (induct p) (auto)
+
lemma polynomial_dense_repr:
- assumes "polynomial R p" and "p \<noteq> []"
+ assumes "polynomial K p" and "p \<noteq> []"
shows "dense_repr p = (lead_coeff p, degree p) # dense_repr (normalize (tl p))"
proof -
let ?len = length and ?norm = normalize
obtain a p' where p: "p = a # p'"
using assms(2) list.exhaust_sel by blast
- hence a: "a \<in> carrier R - { \<zero> }" and p': "set p' \<subseteq> carrier R"
+ hence a: "a \<in> K - { \<zero> }" and p': "set p' \<subseteq> K"
using assms(1) unfolding p by (auto simp add: polynomial_def)
hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'"
unfolding p by simp
@@ -695,26 +722,26 @@
unfolding p by simp
qed
-lemma monon_decomp:
- assumes "polynomial R p"
+lemma monom_decomp:
+ assumes "subring K R" "polynomial K p"
shows "p = of_dense (dense_repr p)"
- using assms
+ using assms(2)
proof (induct "length p" arbitrary: p rule: less_induct)
case less thus ?case
proof (cases p)
case Nil thus ?thesis by simp
next
case (Cons a l)
- hence a: "a \<in> carrier R - { \<zero> }" and l: "set l \<subseteq> carrier R"
- using less(2) by (auto simp add: polynomial_def)
- hence "a # l = poly_add (monon a (degree (a # l))) l"
- using poly_add_monon by (simp add: degree_def)
- also have " ... = poly_add (monon a (degree (a # l))) (normalize l)"
- using poly_add_normalize(2)[of "monon a (degree (a # l))", OF _ l] a
- unfolding monon_def by force
- also have " ... = poly_add (monon a (degree (a # l))) (of_dense (dense_repr (normalize l)))"
- using less(1)[of "normalize l"] normalize_length_le normalize_gives_polynomial[OF l]
- unfolding Cons by (simp add: le_imp_less_Suc)
+ hence a: "a \<in> carrier R - { \<zero> }" and l: "set l \<subseteq> carrier R" "set l \<subseteq> K"
+ using less(2) subringE(1)[OF assms(1)] by (auto simp add: polynomial_def)
+ hence "a # l = poly_add (monom a (degree (a # l))) l"
+ using poly_add_monom[of l a] by simp
+ also have " ... = poly_add (monom a (degree (a # l))) (normalize l)"
+ using poly_add_normalize(2)[of "monom a (degree (a # l))", OF _ l(1)] a
+ unfolding monom_def by force
+ also have " ... = poly_add (monom a (degree (a # l))) (of_dense (dense_repr (normalize l)))"
+ using less(1)[OF _ normalize_gives_polynomial[OF l(2)]] normalize_length_le[of l]
+ unfolding Cons by simp
also have " ... = of_dense ((a, degree (a # l)) # dense_repr (normalize l))"
by simp
also have " ... = of_dense (dense_repr (a # l))"
@@ -724,18 +751,13 @@
qed
qed
-end
-
-subsection \<open>Polynomial multiplication\<close>
-
-context ring
-begin
+subsection \<open>Polynomial Multiplication\<close>
lemma poly_mult_is_polynomial:
- assumes "set p1 \<subseteq> carrier R" and "set p2 \<subseteq> carrier R"
- shows "polynomial R (poly_mult p1 p2)"
- using assms
+ assumes "subring K R" "set p1 \<subseteq> K" and "set p2 \<subseteq> K"
+ shows "polynomial K (poly_mult p1 p2)"
+ using assms(2-3)
proof (induction p1)
case Nil thus ?case
by (simp add: polynomial_def)
@@ -743,34 +765,23 @@
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"
+ have "set (poly_mult p1 p2) \<subseteq> K"
using Cons unfolding polynomial_def by auto
-
- moreover have "set ?a_p2 \<subseteq> carrier R"
- proof -
- have "set (map (\<lambda>b. a \<otimes> b) p2) \<subseteq> carrier R"
- proof
- fix c assume "c \<in> set (map (\<lambda>b. a \<otimes> b) p2)"
- then obtain b where "b \<in> set p2" "c = a \<otimes> b"
- by auto
- thus "c \<in> carrier R"
- using Cons(2-3) by auto
- qed
- thus ?thesis
- unfolding degree_def by auto
- qed
-
- ultimately have "polynomial R (poly_add ?a_p2 (poly_mult p1 p2))"
- using poly_add_is_polynomial by blast
+ moreover have "set ?a_p2 \<subseteq> K"
+ using assms(3) Cons(2) subringE(1-2,6)[OF assms(1)] by(induct p2) (auto)
+ ultimately have "polynomial K (poly_add ?a_p2 (poly_mult p1 p2))"
+ using poly_add_is_polynomial[OF assms(1)] by blast
thus ?case by simp
qed
+lemma poly_mult_closed:
+ assumes "subring K R"
+ shows "\<lbrakk> polynomial K p1; polynomial K p2 \<rbrakk> \<Longrightarrow> polynomial K (poly_mult p1 p2)"
+ using poly_mult_is_polynomial polynomial_incl assms by simp
+
lemma poly_mult_in_carrier:
"\<lbrakk> set p1 \<subseteq> carrier R; set p2 \<subseteq> carrier R \<rbrakk> \<Longrightarrow> set (poly_mult p1 p2) \<subseteq> carrier R"
- using poly_mult_is_polynomial polynomial_in_carrier by simp
-
-lemma poly_mult_closed: "\<lbrakk> polynomial R p1; polynomial R p2 \<rbrakk> \<Longrightarrow> polynomial R (poly_mult p1 p2)"
- using poly_mult_is_polynomial polynomial_in_carrier by simp
+ using poly_mult_is_polynomial polynomial_in_carrier carrier_is_subring by simp
lemma poly_mult_coeff:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
@@ -787,9 +798,9 @@
let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
have "coeff (replicate (degree (a # p1)) \<zero>) = (\<lambda>_. \<zero>)"
and "length (replicate (degree (a # p1)) \<zero>) = length p1"
- using prefix_replicate_zero_coeff[of "[]" "length p1"] unfolding degree_def by auto
+ using prefix_replicate_zero_coeff[of "[]" "length p1"] by auto
hence "coeff ?a_p2 = (\<lambda>i. if i < length p1 then \<zero> else (coeff (map (\<lambda>b. a \<otimes> b) p2)) (i - length p1))"
- using append_coeff[of "map (\<lambda>b. a \<otimes> b) p2" "replicate (length p1) \<zero>"] unfolding degree_def by auto
+ using append_coeff[of "map (\<lambda>b. a \<otimes> b) p2" "replicate (length p1) \<zero>"] by auto
also have " ... = (\<lambda>i. if i < length p1 then \<zero> else a \<otimes> ((coeff p2) (i - length p1)))"
proof -
have "\<And>i. i < length p2 \<Longrightarrow> (coeff (map (\<lambda>b. a \<otimes> b) p2)) i = a \<otimes> ((coeff p2) i)"
@@ -848,7 +859,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_in_carrier[OF _ assms(2)] Cons(2) by simp
ultimately
have "coeff (poly_mult (a # p1) p2) = (\<lambda>i. ((coeff ?a_p2) i) \<oplus> ((coeff (poly_mult p1 p2)) i))"
@@ -864,23 +875,21 @@
proof
fix i
have "\<And>k. ?f i k = ?g i k"
- using in_carrier coeff_length[of p1] by (auto simp add: degree_def)
+ using in_carrier coeff_length[of p1] by auto
thus "(\<Oplus> k \<in> {..i}. ?f i k) = (\<Oplus> k \<in> {..i}. ?g i k)" by simp
qed
finally show ?case .
qed
lemma poly_mult_zero:
- assumes "polynomial R p"
+ assumes "set p \<subseteq> carrier R"
shows "poly_mult [] p = []" and "poly_mult p [] = []"
-proof -
- show "poly_mult [] p = []" by simp
-next
+proof (simp)
have "coeff (poly_mult p []) = (\<lambda>_. \<zero>)"
- using poly_mult_coeff[OF polynomial_in_carrier[OF assms], of "[]"]
- poly_coeff_in_carrier[OF assms] by auto
+ using poly_mult_coeff[OF assms, of "[]"] coeff_in_carrier[OF assms] by auto
thus "poly_mult p [] = []"
- using coeff_iff_polynomial_cond[OF poly_mult_closed[OF assms, of "[]"]] zero_is_polynomial by auto
+ using coeff_iff_polynomial_cond[OF
+ poly_mult_is_polynomial[OF carrier_is_subring assms] zero_is_polynomial] by simp
qed
lemma poly_mult_l_distr':
@@ -906,19 +915,20 @@
poly_mult_in_carrier[OF assms(2-3)] by simp
finally have "coeff (poly_mult (poly_add p1 p2) p3) =
coeff (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" .
- moreover have "polynomial R (poly_mult (poly_add p1 p2) p3)"
- 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
+ moreover have "polynomial (carrier R) (poly_mult (poly_add p1 p2) p3)"
+ and "polynomial (carrier R) (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
+ using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier
+ carrier_is_subring by auto
ultimately show ?thesis
using coeff_iff_polynomial_cond by auto
qed
lemma poly_mult_l_distr:
- assumes "polynomial R p1" "polynomial R p2" "polynomial R p3"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K p3"
shows "poly_mult (poly_add p1 p2) p3 = poly_add (poly_mult p1 p3) (poly_mult p2 p3)"
using poly_mult_l_distr' polynomial_in_carrier assms by auto
-lemma poly_mult_append_replicate_zero:
+lemma poly_mult_prepend_replicate_zero:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
shows "poly_mult p1 p2 = poly_mult ((replicate n \<zero>) @ p1) p2"
proof -
@@ -929,13 +939,13 @@
have "?a_p2 = replicate (length p2 + length p1) \<zero>"
using A(2) by (induction p2) (auto)
hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
- by (simp add: degree_def)
+ by simp
also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
poly_mult_in_carrier[OF A] by force
also have " ... = poly_mult p1 p2"
- using poly_add_zero(2)[OF poly_mult_is_polynomial[OF A]]
- normalize_replicate_zero[of "length p2 + length p1" "[]"] by auto
+ using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring
+ normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
finally show ?thesis by auto
qed } note aux_lemma = this
@@ -955,13 +965,40 @@
let ?replicate = "replicate (length p1 - length (normalize p1)) \<zero>"
have "poly_mult p1 p2 = poly_mult (?replicate @ (normalize p1)) p2"
using normalize_def'[of p1] by simp
- also have " ... = poly_mult (normalize p1) p2"
- using poly_mult_append_replicate_zero polynomial_in_carrier
- normalize_gives_polynomial assms by auto
- finally show ?thesis .
+ thus ?thesis
+ using poly_mult_prepend_replicate_zero normalize_in_carrier assms by auto
qed
-end
+lemma poly_mult_append_zero:
+ assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R"
+ shows "poly_mult (p @ [ \<zero> ]) q = normalize ((poly_mult p q) @ [ \<zero> ])"
+ using assms(1)
+proof (induct p)
+ case Nil thus ?case
+ using poly_mult_normalize[OF _ assms(2), of "[] @ [ \<zero> ]"]
+ poly_mult_zero(1) poly_mult_zero(1)[of "q @ [ \<zero> ]"] assms(2) by auto
+next
+ case (Cons a p)
+ let ?q_a = "\<lambda>n. (map ((\<otimes>) a) q) @ (replicate n \<zero>)"
+ have set_q_a: "\<And>n. set (?q_a n) \<subseteq> carrier R"
+ using Cons(2) assms(2) by (induct q) (auto)
+ have set_poly_mult: "set ((poly_mult p q) @ [ \<zero> ]) \<subseteq> carrier R"
+ using poly_mult_in_carrier[OF _ assms(2)] Cons(2) by auto
+ have "poly_mult ((a # p) @ [\<zero>]) q = poly_add (?q_a (Suc (length p))) (poly_mult (p @ [\<zero>]) q)"
+ by auto
+ also have " ... = poly_add (?q_a (Suc (length p))) (normalize ((poly_mult p q) @ [ \<zero> ]))"
+ using Cons by simp
+ also have " ... = poly_add ((?q_a (length p)) @ [ \<zero> ]) ((poly_mult p q) @ [ \<zero> ])"
+ using poly_add_normalize(2)[OF set_q_a[of "Suc (length p)"] set_poly_mult]
+ by (simp add: replicate_append_same)
+ also have " ... = normalize ((poly_add (?q_a (length p)) (poly_mult p q)) @ [ \<zero> ])"
+ using poly_add_append_zero[OF set_q_a[of "length p"] poly_mult_in_carrier[OF _ assms(2)]] Cons(2) by auto
+ also have " ... = normalize ((poly_mult (a # p) q) @ [ \<zero> ])"
+ by auto
+ finally show ?case .
+qed
+
+end (* of ring context. *)
subsection \<open>Properties Within a Domain\<close>
@@ -969,8 +1006,8 @@
context domain
begin
-lemma one_is_polynomial [intro]: "polynomial R [ \<one> ]"
- unfolding polynomial_def by auto
+lemma one_is_polynomial [intro]: "subring K R \<Longrightarrow> polynomial K [ \<one> ]"
+ unfolding polynomial_def using subringE(3) by auto
lemma poly_mult_comm:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
@@ -1000,21 +1037,21 @@
by simp
qed
hence "coeff (poly_mult p1 p2) = coeff (poly_mult p2 p1)"
- using poly_mult_coeff[OF assms] poly_mult_coeff[OF assms(2) assms(1)] by simp
+ using poly_mult_coeff[OF assms] poly_mult_coeff[OF assms(2,1)] by simp
thus ?thesis
- using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF assms]
- poly_mult_is_polynomial[OF assms(2) assms(1)]] by simp
+ using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF _ assms]
+ poly_mult_is_polynomial[OF _ assms(2,1)]]
+ carrier_is_subring by simp
qed
lemma poly_mult_r_distr':
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "set p3 \<subseteq> carrier R"
shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)"
- using poly_mult_comm[OF assms(1-2)] poly_mult_l_distr'[OF assms(2-3) assms(1)]
- poly_mult_comm[OF assms(1) assms(3)] poly_add_is_polynomial[OF assms(2-3)]
- polynomial_in_carrier poly_mult_comm[OF assms(1), of "poly_add p2 p3"] by simp
+ unfolding poly_mult_comm[OF assms(1) poly_add_in_carrier[OF assms(2-3)]]
+ poly_mult_l_distr'[OF assms(2-3,1)] assms(2-3)[THEN poly_mult_comm[OF _ assms(1)]] ..
lemma poly_mult_r_distr:
- assumes "polynomial R p1" "polynomial R p2" "polynomial R p3"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K p3"
shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)"
using poly_mult_r_distr' polynomial_in_carrier assms by auto
@@ -1032,7 +1069,7 @@
hence "poly_mult (replicate (Suc n) \<zero>) p = poly_mult (\<zero> # (replicate n \<zero>)) p"
by simp
also have " ... = poly_add ((map (\<lambda>a. \<zero> \<otimes> a) p) @ (replicate n \<zero>)) []"
- using Suc by (simp add: degree_def)
+ using Suc by simp
also have " ... = poly_add ((map (\<lambda>a. \<zero>) p) @ (replicate n \<zero>)) []"
proof -
have "map ((\<otimes>) \<zero>) p = map (\<lambda>a. \<zero>) p"
@@ -1052,82 +1089,137 @@
using poly_mult_comm[OF assms in_carrier] by simp
qed
+lemma poly_mult_const':
+ assumes "set p \<subseteq> carrier R" "a \<in> carrier R"
+ shows "poly_mult [ a ] p = normalize (map (\<lambda>b. a \<otimes> b) p)"
+ and "poly_mult p [ a ] = normalize (map (\<lambda>b. a \<otimes> b) p)"
+proof -
+ have "map2 (\<oplus>) (map ((\<otimes>) a) p) (replicate (length p) \<zero>) = map ((\<otimes>) a) p"
+ using assms by (induction p) (auto)
+ thus "poly_mult [ a ] p = normalize (map (\<lambda>b. a \<otimes> b) p)" by simp
+ thus "poly_mult p [ a ] = normalize (map (\<lambda>b. a \<otimes> b) p)"
+ using poly_mult_comm[OF assms(1), of "[ a ]"] assms(2) by auto
+qed
+
lemma poly_mult_const:
- assumes "polynomial R p" "a \<in> carrier R - { \<zero> }"
- shows "poly_mult [ a ] p = map (\<lambda>b. a \<otimes> b) p" and "poly_mult p [ a ] = map (\<lambda>b. a \<otimes> b) p"
+ assumes "subring K R" "polynomial K p" "a \<in> K - { \<zero> }"
+ shows "poly_mult [ a ] p = map (\<lambda>b. a \<otimes> b) p"
+ and "poly_mult p [ a ] = map (\<lambda>b. a \<otimes> b) p"
proof -
+ have in_carrier: "set p \<subseteq> carrier R" "a \<in> carrier R"
+ using polynomial_in_carrier[OF assms(1-2)] assms(3) subringE(1)[OF assms(1)] by auto
+
show "poly_mult [ a ] p = map (\<lambda>b. a \<otimes> b) p"
- proof -
- have "poly_mult [ a ] p = poly_add (map (\<lambda>b. a \<otimes> b) p) []"
- by (simp add: degree_def)
- moreover have "polynomial R (map (\<lambda>b. a \<otimes> b) p)"
- proof (cases p)
- case Nil thus ?thesis by (simp add: polynomial_def)
- 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
- thus ?thesis
- 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
+ proof (cases p)
+ case Nil thus ?thesis
+ using poly_mult_const'(1) in_carrier by auto
+ next
+ case (Cons b q)
+ have "lead_coeff (map (\<lambda>b. a \<otimes> b) p) \<noteq> \<zero>"
+ using assms subringE(1)[OF assms(1)] integral[of a b] Cons lead_coeff_in_carrier by auto
+ hence "normalize (map (\<lambda>b. a \<otimes> b) p) = (map (\<lambda>b. a \<otimes> b) p)"
+ unfolding Cons by simp
+ thus ?thesis
+ using poly_mult_const'(1) in_carrier by auto
qed
thus "poly_mult p [ a ] = map (\<lambda>b. a \<otimes> b) p"
- using poly_mult_comm[of "[ a ]" p] polynomial_in_carrier[OF assms(1)] assms(2) by auto
+ using poly_mult_comm[OF in_carrier(1)] in_carrier(2) by auto
qed
-lemma poly_mult_monon:
- assumes "polynomial R p" "a \<in> carrier R - { \<zero> }"
- shows "poly_mult (monon a n) p =
- (if p = [] then [] else (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
+lemma poly_mult_semiassoc:
+ assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
+ shows "poly_mult (poly_mult [ a ] p) q = poly_mult [ a ] (poly_mult p q)"
+proof -
+ let ?cp = "coeff p" and ?cq = "coeff q"
+ have "coeff (poly_mult [ a ] p) = (\<lambda>i. (a \<otimes> ?cp i))"
+ using poly_mult_const'(1)[OF assms(1,3)] normalize_coeff scalar_coeff[OF assms(3)] by simp
+
+ hence "coeff (poly_mult (poly_mult [ a ] p) q) = (\<lambda>i. (\<Oplus>j \<in> {..i}. (a \<otimes> ?cp j) \<otimes> ?cq (i - j)))"
+ using poly_mult_coeff[OF poly_mult_in_carrier[OF _ assms(1)] assms(2), of "[ a ]"] assms(3) by auto
+ also have " ... = (\<lambda>i. a \<otimes> (\<Oplus>j \<in> {..i}. ?cp j \<otimes> ?cq (i - j)))"
+ proof
+ fix i show "(\<Oplus>j \<in> {..i}. (a \<otimes> ?cp j) \<otimes> ?cq (i - j)) = a \<otimes> (\<Oplus>j \<in> {..i}. ?cp j \<otimes> ?cq (i - j))"
+ using finsum_rdistr[OF _ assms(3), of _ "\<lambda>j. ?cp j \<otimes> ?cq (i - j)"]
+ assms(1-2)[THEN coeff_in_carrier] by (simp add: assms(3) m_assoc)
+ qed
+ also have " ... = coeff (poly_mult [ a ] (poly_mult p q))"
+ unfolding poly_mult_const'(1)[OF poly_mult_in_carrier[OF assms(1-2)] assms(3)]
+ using scalar_coeff[OF assms(3), of "poly_mult p q"]
+ poly_mult_coeff[OF assms(1-2)] normalize_coeff by simp
+ finally have "coeff (poly_mult (poly_mult [ a ] p) q) = coeff (poly_mult [ a ] (poly_mult p q))" .
+ moreover have "polynomial (carrier R) (poly_mult (poly_mult [ a ] p) q)"
+ and "polynomial (carrier R) (poly_mult [ a ] (poly_mult p q))"
+ using poly_mult_is_polynomial[OF _ poly_mult_in_carrier[OF _ assms(1)] assms(2)]
+ poly_mult_is_polynomial[OF _ _ poly_mult_in_carrier[OF assms(1-2)]]
+ carrier_is_subring assms(3) by (auto simp del: poly_mult.simps)
+ ultimately show ?thesis
+ using coeff_iff_polynomial_cond by simp
+qed
+
+
+text \<open>Note that "polynomial (carrier R) p" and "subring K p; polynomial K p" are "equivalent"
+ assumptions for any lemma in ring which the result doesn't depend on K, because carrier
+ is a subring and a polynomial for a subset of the carrier is a carrier polynomial. The
+ decision between one of them should be based on how the lemma is going to be used and
+ proved. These are some tips:
+ (a) Lemmas about the algebraic structure of polynomials should use the latter option.
+ (b) Also, if the lemma deals with lots of polynomials, then the latter option is preferred.
+ (c) If the proof is going to be much easier with the first option, do not hesitate. \<close>
+
+lemma poly_mult_monom':
+ assumes "set p \<subseteq> carrier R" "a \<in> carrier R"
+ shows "poly_mult (monom a n) p = normalize ((map ((\<otimes>) a) p) @ (replicate n \<zero>))"
+proof -
+ have set_map: "set ((map ((\<otimes>) a) p) @ (replicate n \<zero>)) \<subseteq> carrier R"
+ using assms by (induct p) (auto)
+ show ?thesis
+ using poly_mult_replicate_zero(1)[OF assms(1), of n]
+ poly_add_zero'(1)[OF set_map]
+ unfolding monom_def by simp
+qed
+
+lemma poly_mult_monom:
+ assumes "polynomial (carrier R) p" "a \<in> carrier R - { \<zero> }"
+ shows "poly_mult (monom a n) p =
+ (if p = [] then [] else (poly_mult [ a ] p) @ (replicate n \<zero>))"
proof (cases p)
case Nil thus ?thesis
- using poly_mult_zero(2)[OF monon_is_polynomial[OF assms(2)]] by simp
+ using poly_mult_zero(2)[of "monom a n"] assms(2) monom_def by fastforce
next
case (Cons b ps)
- hence "lead_coeff ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) = a \<otimes> b"
- by simp
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
- ultimately have is_polynomial: "polynomial R ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
- using Cons unfolding polynomial_def by auto
+ thus ?thesis
+ using poly_mult_monom'[OF polynomial_incl[OF assms(1)], of a n] assms(2) Cons
+ unfolding poly_mult_const(1)[OF carrier_is_subring assms] by simp
+qed
- have "poly_mult (a # replicate n \<zero>) p =
- poly_add ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) (poly_mult (replicate n \<zero>) p)"
- by (simp add: degree_def)
- also have " ... = poly_add ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) []"
- using poly_mult_replicate_zero(1)[OF polynomial_in_carrier[OF assms(1)]] by simp
- also have " ... = (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)"
- using poly_add_zero(1)[OF is_polynomial] .
- also have " ... = (if p = [] then [] else (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
- using Cons by auto
- finally show ?thesis unfolding monon_def .
+lemma poly_mult_one':
+ assumes "set p \<subseteq> carrier R"
+ shows "poly_mult [ \<one> ] p = normalize p" and "poly_mult p [ \<one> ] = normalize p"
+proof -
+ have "map2 (\<oplus>) (map ((\<otimes>) \<one>) p) (replicate (length p) \<zero>) = p"
+ using assms by (induct p) (auto)
+ thus "poly_mult [ \<one> ] p = normalize p" and "poly_mult p [ \<one> ] = normalize p"
+ using poly_mult_comm[OF assms, of "[ \<one> ]"] by auto
qed
lemma poly_mult_one:
- assumes "polynomial R p"
+ assumes "subring K R" "polynomial K p"
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)
- thus "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
- using poly_mult_const[OF assms, of \<one>] by auto
-qed
+ using poly_mult_one'[OF polynomial_in_carrier[OF assms]] normalize_polynomial[OF assms(2)] by auto
lemma poly_mult_lead_coeff_aux:
- assumes "polynomial R p1" "polynomial R p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
shows "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
proof -
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
+ using assms(2-5) lead_coeff_in_carrier[OF assms(1)] by (metis list.collapse)+
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
+ using poly_mult_coeff[OF assms(2-3)[THEN polynomial_in_carrier[OF assms(1)]]] by simp
also have " ... = (lead_coeff p1) \<otimes> (lead_coeff p2)"
proof -
let ?f = "\<lambda>i. (coeff p1) i \<otimes> (coeff p2) ((degree p1) + (degree p2) - i)"
@@ -1138,7 +1230,7 @@
moreover have "\<And>i. i > degree p1 \<Longrightarrow> ?f i = \<zero>"
using coeff_degree[of p1] in_carrier by auto
moreover have "?f (degree p1) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
- using assms(3-4) by simp
+ using assms(4-5) lead_coeff_simp by simp
ultimately have "?f = (\<lambda>i. if degree p1 = i then (lead_coeff p1) \<otimes> (lead_coeff p2) else \<zero>)"
using nat_neq_iff by auto
thus ?thesis
@@ -1149,24 +1241,24 @@
qed
lemma poly_mult_degree_eq:
- assumes "polynomial R p1" "polynomial R p2"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2"
shows "degree (poly_mult p1 p2) = (if p1 = [] \<or> p2 = [] then 0 else (degree p1) + (degree p2))"
proof (cases p1)
- case Nil thus ?thesis by (simp add: degree_def)
+ case Nil thus ?thesis by simp
next
case (Cons a p1') note p1 = Cons
show ?thesis
proof (cases p2)
case Nil thus ?thesis
- using poly_mult_zero(2)[OF assms(1)] by (simp add: degree_def)
+ using poly_mult_zero(2)[OF polynomial_in_carrier[OF assms(1-2)]] by simp
next
case (Cons b p2') note p2 = Cons
have a: "a \<in> carrier R" and b: "b \<in> carrier R"
- using p1 p2 polynomial_in_carrier[OF assms(1)] polynomial_in_carrier[OF assms(2)] by auto
+ using p1 p2 polynomial_in_carrier[OF assms(1-2)] polynomial_in_carrier[OF assms(1,3)] by auto
have "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) = a \<otimes> b"
using poly_mult_lead_coeff_aux[OF assms] p1 p2 by simp
hence neq0: "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \<noteq> \<zero>"
- using assms p1 p2 integral[of a b] unfolding polynomial_def by auto
+ using assms(2-3) integral[of a b] lead_coeff_in_carrier[OF assms(1)] p1 p2 by auto
moreover have eq0: "\<And>i. i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
proof -
have aux_lemma: "degree (poly_mult p1 p2) \<le> (degree p1) + (degree p2)"
@@ -1180,213 +1272,205 @@
hence "degree (poly_mult (a # p1) p2) \<le> max (degree ?a_p2) (degree (poly_mult p1 p2))"
using poly_add_degree[of ?a_p2 "poly_mult p1 p2"] by simp
also have " ... \<le> max ((degree (a # p1)) + (degree p2)) (degree (poly_mult p1 p2))"
- unfolding degree_def by auto
+ by auto
also have " ... \<le> max ((degree (a # p1)) + (degree p2)) ((degree p1) + (degree p2))"
using Cons by simp
also have " ... \<le> (degree (a # p1)) + (degree p2)"
- unfolding degree_def by auto
+ by auto
finally show ?case .
qed
fix i show "i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
using coeff_degree aux_lemma by simp
qed
+ moreover have "polynomial K (poly_mult p1 p2)"
+ by (simp add: assms poly_mult_closed)
ultimately have "degree (poly_mult p1 p2) = degree p1 + degree p2"
- by (metis eq0 neq0 assms coeff.simps(1) coeff_degree lead_coeff_simp length_greater_0_conv
- normalize_idem normalize_length_lt not_less_iff_gr_or_eq poly_mult_closed)
+ by (metis (no_types) assms(1) coeff.simps(1) coeff_degree domain.poly_mult_one(1) domain_axioms eq0 lead_coeff_simp length_greater_0_conv neq0 normalize_length_lt not_less_iff_gr_or_eq poly_mult_one'(1) polynomial_in_carrier)
thus ?thesis
using p1 p2 by auto
qed
qed
lemma poly_mult_integral:
- assumes "polynomial R p1" "polynomial R p2"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2"
shows "poly_mult p1 p2 = [] \<Longrightarrow> p1 = [] \<or> p2 = []"
proof (rule ccontr)
assume A: "poly_mult p1 p2 = []" "\<not> (p1 = [] \<or> p2 = [])"
hence "degree (poly_mult p1 p2) = degree p1 + degree p2"
using poly_mult_degree_eq[OF assms] by simp
hence "length p1 = 1 \<and> length p2 = 1"
- unfolding degree_def using A Suc_diff_Suc by fastforce
+ using A Suc_diff_Suc by fastforce
then obtain a b where p1: "p1 = [ a ]" and p2: "p2 = [ b ]"
by (metis One_nat_def length_0_conv length_Suc_conv)
hence "a \<in> carrier R - { \<zero> }" and "b \<in> carrier R - { \<zero> }"
- using assms unfolding polynomial_def by auto
+ using assms lead_coeff_in_carrier by auto
hence "poly_mult [ a ] [ b ] = [ a \<otimes> b ]"
- using A assms(2) poly_mult_const(1) p1 by fastforce
+ using integral by auto
thus False using A(1) p1 p2 by simp
qed
lemma poly_mult_lead_coeff:
- assumes "polynomial R p1" "polynomial R p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
+ assumes "subring K R" "polynomial K p1" "polynomial K p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
shows "lead_coeff (poly_mult p1 p2) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
proof -
have "poly_mult p1 p2 \<noteq> []"
- using poly_mult_integral[OF assms(1-2)] assms(3-4) by auto
+ using poly_mult_integral[OF assms(1-3)] assms(4-5) by auto
hence "lead_coeff (poly_mult p1 p2) = (coeff (poly_mult p1 p2)) (degree p1 + degree p2)"
- using poly_mult_degree_eq[OF assms(1-2)] assms(3-4) by (metis coeff.simps(2) list.collapse)
+ using poly_mult_degree_eq[OF assms(1-3)] assms(4-5) by (metis coeff.simps(2) list.collapse)
thus ?thesis
using poly_mult_lead_coeff_aux[OF assms] by simp
qed
-end
+lemma poly_mult_append_zero_lcancel:
+ assumes "subring K R" and "polynomial K p" "polynomial K q"
+ shows "poly_mult (p @ [ \<zero> ]) q = r @ [ \<zero> ] \<Longrightarrow> poly_mult p q = r"
+proof -
+ note in_carrier = assms(2-3)[THEN polynomial_in_carrier[OF assms(1)]]
+
+ assume pmult: "poly_mult (p @ [ \<zero> ]) q = r @ [ \<zero> ]"
+ have "poly_mult (p @ [ \<zero> ]) q = []" if "q = []"
+ using poly_mult_zero(2)[of "p @ [ \<zero> ]"] that in_carrier(1) by auto
+ moreover have "poly_mult (p @ [ \<zero> ]) q = []" if "p = []"
+ using poly_mult_normalize[OF _ in_carrier(2), of "p @ [ \<zero> ]"] poly_mult_zero[OF in_carrier(2)]
+ unfolding that by auto
+ ultimately have "p \<noteq> []" and "q \<noteq> []"
+ using pmult by auto
+ hence "poly_mult p q \<noteq> []"
+ using poly_mult_integral[OF assms] by auto
+ hence "normalize ((poly_mult p q) @ [ \<zero> ]) = (poly_mult p q) @ [ \<zero> ]"
+ using normalize_polynomial[OF append_is_polynomial[OF assms(1) poly_mult_closed[OF assms], of "Suc 0"]] by auto
+ thus "poly_mult p q = r"
+ using poly_mult_append_zero[OF assms(2-3)[THEN polynomial_in_carrier[OF assms(1)]]] pmult by simp
+qed
+
+lemma poly_mult_append_zero_rcancel:
+ assumes "subring K R" and "polynomial K p" "polynomial K q"
+ shows "poly_mult p (q @ [ \<zero> ]) = r @ [ \<zero> ] \<Longrightarrow> poly_mult p q = r"
+ using poly_mult_append_zero_lcancel[OF assms(1,3,2)]
+ poly_mult_comm[of p "q @ [ \<zero> ]"] poly_mult_comm[of p q]
+ assms(2-3)[THEN polynomial_in_carrier[OF assms(1)]]
+ by auto
+
+end (* of domain context. *)
subsection \<open>Algebraic Structure of Polynomials\<close>
-definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow> ('a list) ring"
- where "univ_poly R =
- \<lparr> carrier = { p. polynomial R p },
- monoid.mult = ring.poly_mult R,
+definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring" ("_ [X]\<index>" 80)
+ where "univ_poly R K =
+ \<lparr> carrier = { p. polynomial\<^bsub>R\<^esub> K p },
+ mult = ring.poly_mult R,
one = [ \<one>\<^bsub>R\<^esub> ],
zero = [],
add = ring.poly_add R \<rparr>"
+
+text \<open>These lemmas allow you to unfold one field of the record at a time. \<close>
+
+lemma univ_poly_carrier: "polynomial\<^bsub>R\<^esub> K p \<longleftrightarrow> p \<in> carrier (K[X]\<^bsub>R\<^esub>)"
+ unfolding univ_poly_def by simp
+
+lemma univ_poly_mult: "mult (K[X]\<^bsub>R\<^esub>) = ring.poly_mult R"
+ unfolding univ_poly_def by simp
+
+lemma univ_poly_one: "one (K[X]\<^bsub>R\<^esub>) = [ \<one>\<^bsub>R\<^esub> ]"
+ unfolding univ_poly_def by simp
+
+lemma univ_poly_zero: "zero (K[X]\<^bsub>R\<^esub>) = []"
+ unfolding univ_poly_def by simp
+
+lemma univ_poly_add: "add (K[X]\<^bsub>R\<^esub>) = ring.poly_add R"
+ unfolding univ_poly_def by simp
+
+
context domain
begin
-lemma poly_mult_assoc_aux:
+lemma poly_mult_monom_assoc:
assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
- shows "poly_mult ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) q =
- poly_mult (monon a n) (poly_mult p q)"
-proof -
- let ?len = "n"
- let ?a_p = "(map (\<lambda>b. a \<otimes> b) p) @ (replicate ?len \<zero>)"
- let ?c2 = "coeff p" and ?c3 = "coeff q"
- have coeff_a_p:
- "coeff ?a_p = (\<lambda>i. if i < ?len then \<zero> else a \<otimes> ?c2 (i - ?len))" (is
- "coeff ?a_p = (\<lambda>i. ?f i)")
- using append_coeff[of "map ((\<otimes>) a) p" "replicate ?len \<zero>"]
- replicate_zero_coeff[of ?len] scalar_coeff[OF assms(3), of p] by auto
- have in_carrier:
- "set ?a_p \<subseteq> carrier R" "\<And>i. ?c2 i \<in> carrier R" "\<And>i. ?c3 i \<in> carrier R"
- "\<And>i. coeff (poly_mult p q) i \<in> carrier R"
- using assms poly_mult_in_carrier by auto
- have "coeff (poly_mult ?a_p q) = (\<lambda>n. (\<Oplus>i \<in> {..n}. (coeff ?a_p) i \<otimes> ?c3 (n - i)))"
- using poly_mult_coeff[OF in_carrier(1) assms(2)] .
- also have " ... = (\<lambda>n. (\<Oplus>i \<in> {..n}. (?f i) \<otimes> ?c3 (n - i)))"
- using coeff_a_p by simp
- also have " ... = (\<lambda>n. (\<Oplus>i \<in> {..n}. (if i = ?len then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i)))"
- (is "(\<lambda>n. (\<Oplus>i \<in> {..n}. ?side1 n i)) = (\<lambda>n. (\<Oplus>i \<in> {..n}. ?side2 n i))")
- proof
- fix n
- have in_carrier': "\<And>i. ?side1 n i \<in> carrier R" "\<And>i. ?side2 n i \<in> carrier R"
- using in_carrier assms coeff_in_carrier poly_mult_in_carrier by auto
- show "(\<Oplus>i \<in> {..n}. ?side1 n i) = (\<Oplus>i \<in> {..n}. ?side2 n i)"
- proof (cases "n < ?len")
- assume "n < ?len"
- hence "\<And>i. i \<le> n \<Longrightarrow> ?side1 n i = ?side2 n i"
- using in_carrier assms coeff_in_carrier poly_mult_in_carrier by simp
- thus ?thesis
- using add.finprod_cong'[of "{..n}" "{..n}" "?side1 n" "?side2 n"] in_carrier'
- by (metis (no_types, lifting) Pi_I' atMost_iff)
- next
- assume "\<not> n < ?len"
- hence n_ge: "n \<ge> ?len" by simp
- define h where "h = (\<lambda>i. if i < ?len then \<zero> else (a \<otimes> ?c2 (i - ?len)) \<otimes> ?c3 (n - i))"
- hence h_in_carrier: "\<And>i. h i \<in> carrier R"
- using assms(3) in_carrier by auto
- have "\<And>i. (?f i) \<otimes> ?c3 (n - i) = h i"
- using in_carrier(2-3) assms(3) h_def by auto
- hence "(\<Oplus>i \<in> {..n}. ?side1 n i) = (\<Oplus>i \<in> {..n}. h i)"
- by simp
- also have " ... = (\<Oplus>i \<in> {..<?len}. h i) \<oplus> (\<Oplus>i \<in> {?len..n}. h i)"
- using add.finprod_Un_disjoint[of "{..<?len}" "{?len..n}" h] h_in_carrier n_ge
- by (simp add: ivl_disj_int_one(4) ivl_disj_un_one(4))
- also have " ... = (\<Oplus>i \<in> {..<?len}. \<zero>) \<oplus> (\<Oplus>i \<in> {?len..n}. h i)"
- using add.finprod_cong'[of "{..<?len}" "{..<?len}" h "\<lambda>_. \<zero>"] h_in_carrier
- unfolding h_def by auto
- also have " ... = (\<Oplus>i \<in> {?len..n}. h i)"
- using add.finprod_one h_in_carrier by simp
- also have " ... = (\<Oplus>i \<in> (\<lambda>i. i + ?len) ` {..n - ?len}. h i)"
- using n_ge atLeast0AtMost image_add_atLeastAtMost'[of ?len 0 "n - ?len"] by auto
- also have " ... = (\<Oplus>i \<in> {..n - ?len}. h (i + ?len))"
- using add.finprod_reindex[of h "\<lambda>i. i + ?len" "{..n - ?len}"] h_in_carrier by simp
- 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)
- 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
- also have " ... = a \<otimes> (coeff (poly_mult p q)) (n - ?len)"
- using poly_mult_coeff[OF assms(1-2)] n_ge by (simp add: add.commute)
- also have " ... =
- (\<Oplus>i \<in> {..n}. if ?len = i then a \<otimes> (coeff (poly_mult p q)) (n - i) else \<zero>)"
- using add.finprod_singleton[of ?len "{..n}" "\<lambda>i. a \<otimes> (coeff (poly_mult p q)) (n - i)"]
- n_ge in_carrier(2-4) assms by simp
- also have " ... = (\<Oplus>i \<in> {..n}. (if ?len = i then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i))"
- using in_carrier(2-4) assms(3) add.finprod_cong'[of "{..n}" "{..n}"] by simp
- also have " ... = (\<Oplus>i \<in> {..n}. ?side2 n i)"
- proof -
- have "(\<lambda>i. (if ?len = i then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i)) = ?side2 n" by auto
- thus ?thesis by simp
- qed
- finally show ?thesis .
- qed
- qed
- also have " ... = coeff (poly_mult (monon a n) (poly_mult p q))"
- using monon_coeff[of a "n"] poly_mult_coeff[of "monon a n" "poly_mult p q"]
- poly_mult_in_carrier[OF assms(1-2)] assms(3) unfolding monon_def by force
- finally
- have "coeff (poly_mult ?a_p q) = coeff (poly_mult (monon a n) (poly_mult p q))" .
- moreover have "polynomial R (poly_mult ?a_p q)"
- using poly_mult_is_polynomial[OF in_carrier(1) assms(2)] by simp
- moreover have "polynomial R (poly_mult (monon a n) (poly_mult p q))"
- using poly_mult_is_polynomial[of "monon a n" "poly_mult p q"]
- poly_mult_in_carrier[OF assms(1-2)] assms(3) unfolding monon_def
- using in_carrier(1) by auto
- ultimately show ?thesis
- using coeff_iff_polynomial_cond by simp
+ shows "poly_mult (poly_mult (monom a n) p) q =
+ poly_mult (monom a n) (poly_mult p q)"
+proof (induct n)
+ case 0 thus ?case
+ unfolding monom_def using poly_mult_semiassoc[OF assms] by (auto simp del: poly_mult.simps)
+next
+ case (Suc n)
+ have "poly_mult (poly_mult (monom a (Suc n)) p) q =
+ poly_mult (normalize ((poly_mult (monom a n) p) @ [ \<zero> ])) q"
+ using poly_mult_append_zero[OF monom_in_carrier[OF assms(3), of n] assms(1)]
+ unfolding monom_def by (auto simp del: poly_mult.simps simp add: replicate_append_same)
+ also have " ... = normalize ((poly_mult (poly_mult (monom a n) p) q) @ [ \<zero> ])"
+ using poly_mult_normalize[OF _ assms(2)] poly_mult_append_zero[OF _ assms(2)]
+ poly_mult_in_carrier[OF monom_in_carrier[OF assms(3), of n] assms(1)] by auto
+ also have " ... = normalize ((poly_mult (monom a n) (poly_mult p q)) @ [ \<zero> ])"
+ using Suc by simp
+ also have " ... = poly_mult (monom a (Suc n)) (poly_mult p q)"
+ using poly_mult_append_zero[OF monom_in_carrier[OF assms(3), of n]
+ poly_mult_in_carrier[OF assms(1-2)]]
+ unfolding monom_def by (simp add: replicate_append_same)
+ finally show ?case .
qed
-lemma univ_poly_is_monoid: "monoid (univ_poly R)"
- unfolding univ_poly_def using poly_mult_one
-proof (auto simp add: poly_add_closed poly_mult_closed one_is_polynomial monoid_def)
+
+context
+ fixes K :: "'a set" assumes K: "subring K R"
+begin
+
+lemma univ_poly_is_monoid: "monoid (K[X])"
+ unfolding univ_poly_def using poly_mult_one[OF K]
+proof (auto simp add: K poly_add_closed poly_mult_closed one_is_polynomial monoid_def)
fix p1 p2 p3
let ?P = "poly_mult (poly_mult p1 p2) p3 = poly_mult p1 (poly_mult p2 p3)"
- assume A: "polynomial R p1" "polynomial R p2" "polynomial R p3"
- show ?P using polynomial_in_carrier[OF A(1)]
+ assume A: "polynomial K p1" "polynomial K p2" "polynomial K p3"
+ show ?P using polynomial_in_carrier[OF K A(1)]
proof (induction p1)
case Nil thus ?case by simp
next
+next
case (Cons a p1) thus ?case
proof (cases "a = \<zero>")
assume eq_zero: "a = \<zero>"
have p1: "set p1 \<subseteq> carrier R"
using Cons(2) by simp
have "poly_mult (poly_mult (a # p1) p2) p3 = poly_mult (poly_mult p1 p2) p3"
- using poly_mult_append_replicate_zero[OF p1 polynomial_in_carrier[OF A(2)], of "Suc 0"]
+ using poly_mult_prepend_replicate_zero[OF p1 polynomial_in_carrier[OF K A(2)], of "Suc 0"]
eq_zero by simp
also have " ... = poly_mult p1 (poly_mult p2 p3)"
using p1[THEN Cons(1)] by simp
also have " ... = poly_mult (a # p1) (poly_mult p2 p3)"
- using poly_mult_append_replicate_zero[OF p1
- poly_mult_in_carrier[OF A(2-3)[THEN polynomial_in_carrier]], of "Suc 0"] eq_zero by simp
+ using poly_mult_prepend_replicate_zero[OF p1
+ poly_mult_in_carrier[OF A(2-3)[THEN polynomial_in_carrier[OF K]]], of "Suc 0"] eq_zero
+ by simp
finally show ?thesis .
next
assume "a \<noteq> \<zero>" hence in_carrier:
"set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "set p3 \<subseteq> carrier R" "a \<in> carrier R - { \<zero> }"
- using A(2-3) polynomial_in_carrier Cons by auto
+ using A(2-3) polynomial_in_carrier[OF K] Cons by auto
let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (length p1) \<zero>)"
have a_p2_in_carrier: "set ?a_p2 \<subseteq> carrier R"
using in_carrier by auto
have "poly_mult (poly_mult (a # p1) p2) p3 = poly_mult (poly_add ?a_p2 (poly_mult p1 p2)) p3"
- by (simp add: degree_def)
+ by simp
also have " ... = poly_add (poly_mult ?a_p2 p3) (poly_mult (poly_mult p1 p2) p3)"
using poly_mult_l_distr'[OF a_p2_in_carrier poly_mult_in_carrier[OF in_carrier(1-2)] in_carrier(3)] .
also have " ... = poly_add (poly_mult ?a_p2 p3) (poly_mult p1 (poly_mult p2 p3))"
using Cons(1)[OF in_carrier(1)] by simp
+ also have " ... = poly_add (poly_mult (normalize ?a_p2) p3) (poly_mult p1 (poly_mult p2 p3))"
+ using poly_mult_normalize[OF a_p2_in_carrier in_carrier(3)] by simp
+ also have " ... = poly_add (poly_mult (poly_mult (monom a (length p1)) p2) p3)
+ (poly_mult p1 (poly_mult p2 p3))"
+ using poly_mult_monom'[OF in_carrier(2), of a "length p1"] in_carrier(4) by simp
also have " ... = poly_add (poly_mult (a # (replicate (length p1) \<zero>)) (poly_mult p2 p3))
(poly_mult p1 (poly_mult p2 p3))"
- using poly_mult_assoc_aux[of p2 p3 a "length p1"] in_carrier unfolding monon_def by simp
+ using poly_mult_monom_assoc[of p2 p3 a "length p1"] in_carrier unfolding monom_def by simp
also have " ... = poly_mult (poly_add (a # (replicate (length p1) \<zero>)) p1) (poly_mult p2 p3)"
using poly_mult_l_distr'[of "a # (replicate (length p1) \<zero>)" p1 "poly_mult p2 p3"]
poly_mult_in_carrier[OF in_carrier(2-3)] in_carrier by force
also have " ... = poly_mult (a # p1) (poly_mult p2 p3)"
- using poly_add_monon[OF in_carrier(1) in_carrier(4)] unfolding monon_def by simp
+ using poly_add_monom[OF in_carrier(1) in_carrier(4)] unfolding monom_def by simp
finally show ?thesis .
qed
qed
@@ -1394,18 +1478,18 @@
declare poly_add.simps[simp del]
-lemma univ_poly_is_abelian_monoid: "abelian_monoid (univ_poly R)"
+lemma univ_poly_is_abelian_monoid: "abelian_monoid (K[X])"
unfolding univ_poly_def
- using poly_add_closed poly_add_zero zero_is_polynomial
+ using poly_add_closed poly_add_zero zero_is_polynomial K
proof (auto simp add: abelian_monoid_def comm_monoid_def monoid_def comm_monoid_axioms_def)
fix p1 p2 p3
let ?c = "\<lambda>p. coeff p"
- assume A: "polynomial R p1" "polynomial R p2" "polynomial R p3"
+ assume A: "polynomial K p1" "polynomial K p2" "polynomial K p3"
hence
p1: "\<And>i. (?c p1) i \<in> carrier R" "set p1 \<subseteq> carrier R" and
p2: "\<And>i. (?c p2) i \<in> carrier R" "set p2 \<subseteq> carrier R" and
p3: "\<And>i. (?c p3) i \<in> carrier R" "set p3 \<subseteq> carrier R"
- using polynomial_in_carrier by auto
+ using A[THEN polynomial_in_carrier[OF K]] coeff_in_carrier by auto
have "?c (poly_add (poly_add p1 p2) p3) = (\<lambda>i. (?c p1 i \<oplus> ?c p2 i) \<oplus> (?c p3 i))"
using poly_add_coeff[OF poly_add_in_carrier[OF p1(2) p2(2)] p3(2)]
poly_add_coeff[OF p1(2) p2(2)] by simp
@@ -1416,30 +1500,30 @@
poly_add_coeff[OF p2(2) p3(2)] by simp
finally have "?c (poly_add (poly_add p1 p2) p3) = ?c (poly_add p1 (poly_add p2 p3))" .
thus "poly_add (poly_add p1 p2) p3 = poly_add p1 (poly_add p2 p3)"
- using coeff_iff_polynomial_cond poly_add_closed A by auto
+ using coeff_iff_polynomial_cond poly_add_closed[OF K] A by meson
show "poly_add p1 p2 = poly_add p2 p1"
using poly_add_comm[OF p1(2) p2(2)] .
qed
-lemma univ_poly_is_abelian_group: "abelian_group (univ_poly R)"
+lemma univ_poly_is_abelian_group: "abelian_group (K[X])"
proof -
- interpret abelian_monoid "univ_poly R"
+ interpret abelian_monoid "K[X]"
using univ_poly_is_abelian_monoid .
show ?thesis
proof (unfold_locales)
- show "carrier (add_monoid (univ_poly R)) \<subseteq> Units (add_monoid (univ_poly R))"
+ show "carrier (add_monoid (K[X])) \<subseteq> Units (add_monoid (K[X]))"
unfolding univ_poly_def Units_def
proof (auto)
- fix p assume p: "polynomial R p"
- have "polynomial R [ \<ominus> \<one> ]"
- 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
+ fix p assume p: "polynomial K p"
+ have "polynomial K [ \<ominus> \<one> ]"
+ unfolding polynomial_def using r_neg subringE(3,5)[OF K] by force
+ hence cond0: "polynomial K (poly_mult [ \<ominus> \<one> ] p)"
+ using poly_mult_closed[OF K, 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
+ using poly_mult_one[OF K p] by simp
also have " ... = poly_mult (poly_add [ \<one> ] [ \<ominus> \<one> ]) p"
- using poly_mult_l_distr' polynomial_in_carrier[OF p] by auto
+ using poly_mult_l_distr' polynomial_in_carrier[OF K p] by auto
also have " ... = poly_mult [] p"
using poly_add.simps[of "[ \<one> ]" "[ \<ominus> \<one> ]"]
by (simp add: case_prod_unfold r_neg)
@@ -1447,193 +1531,208 @@
finally have cond1: "poly_add p (poly_mult [ \<ominus> \<one> ] p) = []" .
have "poly_add (poly_mult [ \<ominus> \<one> ] p) p = poly_add (poly_mult [ \<ominus> \<one> ] p) (poly_mult [ \<one> ] p)"
- using poly_mult_one[OF p] by simp
+ using poly_mult_one[OF K p] by simp
also have " ... = poly_mult (poly_add [ \<ominus> \<one> ] [ \<one> ]) p"
- using poly_mult_l_distr' polynomial_in_carrier[OF p] by auto
+ using poly_mult_l_distr' polynomial_in_carrier[OF K p] by auto
also have " ... = poly_mult [] p"
using \<open>poly_mult (poly_add [\<one>] [\<ominus> \<one>]) p = poly_mult [] p\<close> poly_add_comm by auto
also have " ... = []" by simp
finally have cond2: "poly_add (poly_mult [ \<ominus> \<one> ] p) p = []" .
- from cond0 cond1 cond2 show "\<exists>q. polynomial R q \<and> poly_add q p = [] \<and> poly_add p q = []"
+ from cond0 cond1 cond2 show "\<exists>q. polynomial K q \<and> poly_add q p = [] \<and> poly_add p q = []"
by auto
qed
qed
qed
-declare poly_add.simps[simp]
-
-end
-
-lemma univ_poly_is_ring:
- assumes "domain R"
- shows "ring (univ_poly R)"
+lemma univ_poly_is_ring: "ring (K[X])"
proof -
- interpret abelian_group "univ_poly R" + monoid "univ_poly R"
- using domain.univ_poly_is_abelian_group[OF assms] domain.univ_poly_is_monoid[OF assms] .
- have R: "ring R"
- using assms unfolding domain_def cring_def by simp
+ interpret UP: abelian_group "K[X]" + monoid "K[X]"
+ using univ_poly_is_abelian_group univ_poly_is_monoid .
show ?thesis
- apply unfold_locales
- apply (auto simp add: univ_poly_def assms domain.poly_mult_r_distr ring.poly_mult_l_distr[OF R])
- done
+ by (unfold_locales)
+ (auto simp add: univ_poly_def poly_mult_r_distr[OF K] poly_mult_l_distr[OF K])
qed
-lemma univ_poly_is_cring:
- assumes "domain R"
- shows "cring (univ_poly R)"
+lemma univ_poly_is_cring: "cring (K[X])"
proof -
- interpret ring "univ_poly R"
- using univ_poly_is_ring[OF assms] by simp
- have "\<And>p q. \<lbrakk> p \<in> carrier (univ_poly R); q \<in> carrier (univ_poly R) \<rbrakk> \<Longrightarrow>
- p \<otimes>\<^bsub>univ_poly R\<^esub> q = q \<otimes>\<^bsub>univ_poly R\<^esub> p"
- unfolding univ_poly_def polynomial_def using domain.poly_mult_comm[OF assms] by auto
+ interpret UP: ring "K[X]"
+ using univ_poly_is_ring .
+ have "\<And>p q. \<lbrakk> p \<in> carrier (K[X]); q \<in> carrier (K[X]) \<rbrakk> \<Longrightarrow> p \<otimes>\<^bsub>K[X]\<^esub> q = q \<otimes>\<^bsub>K[X]\<^esub> p"
+ unfolding univ_poly_def using poly_mult_comm polynomial_in_carrier[OF K] by auto
thus ?thesis
by unfold_locales auto
qed
-lemma univ_poly_is_domain:
- assumes "domain R"
- shows "domain (univ_poly R)"
+lemma univ_poly_is_domain: "domain (K[X])"
+proof -
+ interpret UP: cring "K[X]"
+ using univ_poly_is_cring .
+ show ?thesis
+ by (unfold_locales, auto simp add: univ_poly_def poly_mult_integral[OF K])
+qed
+
+declare poly_add.simps[simp]
+
+lemma univ_poly_a_inv_def':
+ assumes "p \<in> carrier (K[X])"
+ shows "\<ominus>\<^bsub>K[X]\<^esub> p = map (\<lambda>a. \<ominus> a) p"
proof -
- interpret cring "univ_poly R"
- using univ_poly_is_cring[OF assms] by simp
- show ?thesis
- by unfold_locales
- (auto simp add: univ_poly_def domain.poly_mult_integral[OF assms])
+ have aux_lemma:
+ "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> p \<oplus>\<^bsub>K[X]\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
+ "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> (map (\<lambda>a. \<ominus> a) p) \<in> carrier (K[X])"
+ proof -
+ fix p assume p: "p \<in> carrier (K[X])"
+ hence set_p: "set p \<subseteq> K"
+ unfolding univ_poly_def using polynomial_incl by auto
+ show "(map (\<lambda>a. \<ominus> a) p) \<in> carrier (K[X])"
+ 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 subringE(1)[OF K] by force
+ moreover have "set (map (\<lambda>a. \<ominus> a) p) \<subseteq> K"
+ using set_p subringE(5)[OF K] by (induct p) (auto)
+ ultimately show ?thesis
+ unfolding univ_poly_def polynomial_def by simp
+ qed
+
+ have "map2 (\<oplus>) p (map (\<lambda>a. \<ominus> a) p) = replicate (length p) \<zero>"
+ using set_p subringE(1)[OF K] by (induct p) (auto simp add: r_neg)
+ thus "p \<oplus>\<^bsub>K[X]\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
+ unfolding univ_poly_def using normalize_replicate_zero[of "length p" "[]"] by auto
+ qed
+
+ interpret UP: ring "K[X]"
+ using univ_poly_is_ring .
+
+ from aux_lemma
+ have "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> \<ominus>\<^bsub>K[X]\<^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>
-lemma (in domain) long_division_theorem:
- assumes "polynomial R p" "polynomial R b" and "b \<noteq> []" and "lead_coeff b \<in> Units R"
- shows "\<exists>q r. polynomial R q \<and> polynomial R r \<and>
- p = poly_add (poly_mult b q) r \<and> (r = [] \<or> degree r < degree b)"
+lemma long_division_theorem:
+ assumes "polynomial K p" and "polynomial K b" "b \<noteq> []"
+ and "lead_coeff b \<in> Units (R \<lparr> carrier := K \<rparr>)"
+ shows "\<exists>q r. polynomial K q \<and> polynomial K r \<and>
+ p = (b \<otimes>\<^bsub>K[X]\<^esub> q) \<oplus>\<^bsub>K[X]\<^esub> r \<and> (r = [] \<or> degree r < degree b)"
(is "\<exists>q r. ?long_division p q r")
- using assms
+ using assms(1)
proof (induct "length p" arbitrary: p rule: less_induct)
case less thus ?case
proof (cases p)
case Nil
hence "?long_division p [] []"
- using zero_is_polynomial poly_mult_zero[OF less(3)] by (simp add: degree_def)
+ using zero_is_polynomial poly_mult_zero[OF polynomial_in_carrier[OF K assms(2)]]
+ by (simp add: univ_poly_def)
thus ?thesis by blast
next
case (Cons a p') thus ?thesis
proof (cases "length b > length p")
assume "length b > length p"
- hence "p = [] \<or> degree p < degree b" unfolding degree_def
+ hence "p = [] \<or> degree p < degree b"
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
+ using poly_mult_zero(2)[OF polynomial_in_carrier[OF K assms(2)]]
+ poly_add_zero(2)[OF K less(2)] zero_is_polynomial less(2)
+ by (simp add: univ_poly_def)
thus ?thesis by blast
next
- interpret UP: cring "univ_poly R"
- using univ_poly_is_cring[OF is_domain] .
+ interpret UP: cring "K[X]"
+ using univ_poly_is_cring .
assume "\<not> length b > length p"
hence len_ge: "length p \<ge> length b" by simp
obtain c b' where b: "b = c # b'"
- using less(4) list.exhaust_sel by blast
- hence c: "c \<in> Units R" "c \<in> carrier R - { \<zero> }" and a: "a \<in> carrier R - { \<zero> }"
- using assms(4) less(2-3) Cons unfolding polynomial_def by auto
- hence "(\<ominus> a) \<in> carrier R - { \<zero> }"
- using r_neg by force
- hence in_carrier: "(\<ominus> a) \<otimes> inv c \<in> carrier R - { \<zero> }"
- using a c(2) Units_inv_closed[OF c(1)] Units_l_inv[OF c(1)]
- empty_iff insert_iff integral_iff m_closed
- by (metis Diff_iff zero_not_one)
+ using assms(3) list.exhaust_sel by blast
+ then obtain c' where c': "c' \<in> carrier R" "c' \<in> K" "c' \<otimes> c = \<one>" "c \<otimes> c' = \<one>"
+ using assms(4) subringE(1)[OF K] unfolding Units_def by auto
+ have c: "c \<in> carrier R" "c \<in> K" "c \<noteq> \<zero>" and a: "a \<in> carrier R" "a \<in> K" "a \<noteq> \<zero>"
+ using less(2) assms(2) lead_coeff_not_zero subringE(1)[OF K] b Cons by auto
+ hence lc: "c' \<otimes> (\<ominus> a) \<in> K - { \<zero> }"
+ using subringE(5-6)[OF K] c' add.inv_solve_right integral_iff by fastforce
let ?len = "length"
- define s where "s = poly_mult (monon ((\<ominus> a) \<otimes> inv c) (?len p - ?len b)) b"
- 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
- hence "?len s - 1 = ?len p - 1"
- using len_ge unfolding b Cons by (simp add: monon_def degree_def)
- moreover have "s \<noteq> []"
- using poly_mult_integral[OF monon_is_polynomial[OF in_carrier] less(3)]
- unfolding s_def monon_def b by blast
- hence "?len s > 0" by simp
- ultimately have len_eq: "?len s = ?len p"
- 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)
+ define s where "s = monom (c' \<otimes> (\<ominus> a)) (?len p - ?len b)"
+ hence s: "polynomial K s" "s \<noteq> []" "degree s = ?len p - ?len b" "length s \<ge> 1"
+ using monom_is_polynomial[OF K lc] unfolding monom_def by auto
+ hence is_polynomial: "polynomial K (p \<oplus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s))"
+ using poly_add_closed[OF K less(2) poly_mult_closed[OF K assms(2), of s]]
+ by (simp add: univ_poly_def)
- define p_diff where "p_diff = poly_add p s"
- hence "?len p_diff < ?len p"
- using len_eq s_coeff in_carrier a c unfolding s Cons apply simp
- by (metis le_imp_less_Suc length_map map_fst_zip normalize_length_le r_neg)
- moreover have "polynomial R p_diff" unfolding p_diff_def s_def
- using poly_mult_closed[OF monon_is_polynomial[OF in_carrier(1)] less(3)]
- poly_add_closed[OF less(2)] by simp
- ultimately
- obtain q' r' where l_div: "?long_division p_diff q' r'"
- using less(1)[of p_diff] less(3-5) by blast
- hence r': "polynomial R r'" and q': "polynomial R q'" by auto
-
- obtain m where m: "polynomial R m" "s = poly_mult m b"
- 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)"
- using r' q' less(2-3) m(1) unfolding univ_poly_def by auto
+ have "lead_coeff (b \<otimes>\<^bsub>K[X]\<^esub> s) = \<ominus> a"
+ using poly_mult_lead_coeff[OF K assms(2) s(1) assms(3) s(2)] c c' a
+ unfolding b s_def monom_def univ_poly_def by (auto simp del: poly_mult.simps, algebra)
+ then obtain s' where s': "b \<otimes>\<^bsub>K[X]\<^esub> s = (\<ominus> a) # s'"
+ using poly_mult_integral[OF K assms(2) s(1)] assms(2-3) s(2)
+ by (simp add: univ_poly_def, metis hd_Cons_tl)
+ moreover have "degree p = degree (b \<otimes>\<^bsub>K[X]\<^esub> s)"
+ using poly_mult_degree_eq[OF K assms(2) s(1)] assms(3) s(2-4) len_ge b Cons
+ by (auto simp add: univ_poly_def)
+ hence "?len p = ?len (b \<otimes>\<^bsub>K[X]\<^esub> s)"
+ unfolding Cons s' by simp
+ hence "?len (p \<oplus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s)) < ?len p"
+ unfolding Cons s' using a normalize_length_le[of "map2 (\<oplus>) p' s'"]
+ by (auto simp add: univ_poly_def r_neg)
+ then obtain q' r' where l_div: "?long_division (p \<oplus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s)) q' r'"
+ using less(1)[OF _ is_polynomial] by blast
- hence "poly_add p (poly_mult m b) = poly_add (poly_mult b q') r'"
- using m l_div unfolding p_diff_def by simp
- hence "p \<oplus>\<^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'"
- unfolding univ_poly_def by auto
- hence
- "(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'"
- using in_univ_carrier by algebra
- hence "p = poly_add (poly_mult b (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) r'"
+ have in_carrier:
+ "p \<in> carrier (K[X])" "b \<in> carrier (K[X])" "s \<in> carrier (K[X])"
+ "q' \<in> carrier (K[X])" "r' \<in> carrier (K[X])"
+ using l_div assms less(2) s unfolding univ_poly_def by auto
+ have "(p \<oplus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s)) \<ominus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s) =
+ ((b \<otimes>\<^bsub>K[X]\<^esub> q') \<oplus>\<^bsub>K[X]\<^esub> r') \<ominus>\<^bsub>K[X]\<^esub> (b \<otimes>\<^bsub>K[X]\<^esub> s)"
+ using l_div by simp
+ hence "p = (b \<otimes>\<^bsub>K[X]\<^esub> (q' \<ominus>\<^bsub>K[X]\<^esub> s)) \<oplus>\<^bsub>K[X]\<^esub> r'"
+ using in_carrier by algebra
+ moreover have "q' \<ominus>\<^bsub>K[X]\<^esub> s \<in> carrier (K[X])"
+ using in_carrier by algebra
+ hence "polynomial K (q' \<ominus>\<^bsub>K[X]\<^esub> s)"
unfolding univ_poly_def by simp
- moreover have "q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m \<in> carrier (univ_poly R)"
- using UP.ring_simprules in_univ_carrier by simp
- hence "polynomial R (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)"
- unfolding univ_poly_def by simp
- ultimately have "?long_division p (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m) r'"
- using l_div r' by simp
+ ultimately have "?long_division p (q' \<ominus>\<^bsub>K[X]\<^esub> s) r'"
+ using l_div by auto
thus ?thesis by blast
qed
qed
qed
-lemma (in field) field_long_division_theorem:
- assumes "polynomial R p" "polynomial R b" and "b \<noteq> []"
- shows "\<exists>q r. polynomial R q \<and> polynomial R r \<and>
- p = poly_add (poly_mult b q) r \<and> (r = [] \<or> degree r < degree b)"
- using long_division_theorem[OF assms] assms lead_coeff_not_zero[of "hd b" "tl b"]
- by (simp add: field_Units)
+end (* of fixed K context. *)
+
+end (* of domain context. *)
-lemma univ_poly_is_euclidean_domain:
- assumes "field R"
- shows "euclidean_domain (univ_poly R) degree"
-proof -
- interpret domain "univ_poly R"
- using univ_poly_is_domain assms field_def by blast
- show ?thesis
- apply (rule euclidean_domainI)
- unfolding univ_poly_def
- using field.field_long_division_theorem[OF assms] by auto
-qed
+lemma (in field) field_long_division_theorem:
+ assumes "subfield K R" "polynomial K p" and "polynomial K b" "b \<noteq> []"
+ shows "\<exists>q r. polynomial K q \<and> polynomial K r \<and>
+ p = (b \<otimes>\<^bsub>K[X]\<^esub> q) \<oplus>\<^bsub>K[X]\<^esub> r \<and> (r = [] \<or> degree r < degree b)"
+ using long_division_theorem[OF subfieldE(1)[OF assms(1)] assms(2-4)] assms(3-4)
+ subfield.subfield_Units[OF assms(1)] lead_coeff_not_zero[of K "hd b" "tl b"]
+ by simp
+
+text \<open>The same theorem as above, but now, everything is in a shell. \<close>
+lemma (in field) field_long_division_theorem_shell:
+ assumes "subfield K R" "p \<in> carrier (K[X])" and "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>"
+ shows "\<exists>q r. q \<in> carrier (K[X]) \<and> r \<in> carrier (K[X]) \<and>
+ p = (b \<otimes>\<^bsub>K[X]\<^esub> q) \<oplus>\<^bsub>K[X]\<^esub> r \<and> (r = \<zero>\<^bsub>K[X]\<^esub> \<or> degree r < degree b)"
+ using field_long_division_theorem assms by (auto simp add: univ_poly_def)
subsection \<open>Consistency Rules\<close>
-lemma (in ring) subring_is_ring: (* <- Move to Subrings.thy *)
- assumes "subring K R" shows "ring (R \<lparr> carrier := K \<rparr>)"
- using assms unfolding subring_iff[OF subringE(1)[OF assms]] .
+lemma polynomial_consistent [simp]:
+ shows "polynomial\<^bsub>(R \<lparr> carrier := K \<rparr>)\<^esub> K p \<Longrightarrow> polynomial\<^bsub>R\<^esub> K p"
+ unfolding polynomial_def by auto
lemma (in ring) eval_consistent [simp]:
assumes "subring K R" shows "ring.eval (R \<lparr> carrier := K \<rparr>) = eval"
@@ -1679,9 +1778,26 @@
thus ?thesis by auto
qed
-lemma (in ring) univ_poly_carrier_change_def':
+lemma (in domain) univ_poly_a_inv_consistent:
+ assumes "subring K R" "p \<in> carrier (K[X])"
+ shows "\<ominus>\<^bsub>K[X]\<^esub> p = \<ominus>\<^bsub>(carrier R)[X]\<^esub> p"
+proof -
+ have in_carrier: "p \<in> carrier ((carrier R)[X])"
+ using assms carrier_polynomial by (auto simp add: univ_poly_def)
+ show ?thesis
+ using univ_poly_a_inv_def'[OF assms]
+ univ_poly_a_inv_def'[OF carrier_is_subring in_carrier] by simp
+qed
+
+lemma (in domain) univ_poly_a_minus_consistent:
+ assumes "subring K R" "q \<in> carrier (K[X])"
+ shows "p \<ominus>\<^bsub>K[X]\<^esub> q = p \<ominus>\<^bsub>(carrier R)[X]\<^esub> q"
+ using univ_poly_a_inv_consistent[OF assms]
+ unfolding a_minus_def univ_poly_def by auto
+
+lemma (in ring) univ_poly_consistent:
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>"
+ shows "univ_poly (R \<lparr> carrier := K \<rparr>) = univ_poly R"
unfolding univ_poly_def polynomial_def
using poly_add_consistent[OF assms]
poly_mult_consistent[OF assms]
@@ -1689,6 +1805,36 @@
by auto
+subsubsection \<open>Corollaries\<close>
+
+corollary (in ring) subfield_long_division_theorem_shell:
+ assumes "subfield K R" "p \<in> carrier (K[X])" and "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>"
+ shows "\<exists>q r. q \<in> carrier (K[X]) \<and> r \<in> carrier (K[X]) \<and>
+ p = (b \<otimes>\<^bsub>K[X]\<^esub> q) \<oplus>\<^bsub>K[X]\<^esub> r \<and> (r = \<zero>\<^bsub>K[X]\<^esub> \<or> degree r < degree b)"
+ using field.field_long_division_theorem_shell[OF subfield_iff(2)[OF assms(1)]
+ field.carrier_is_subfield[OF subfield_iff(2)[OF assms(1)]]]
+ univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] assms(2-4)
+ by auto
+
+corollary (in domain) univ_poly_is_euclidean:
+ assumes "subfield K R" shows "euclidean_domain (K[X]) degree"
+proof -
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF subfieldE(1)[OF assms]] field_def by blast
+ show ?thesis
+ using subfield_long_division_theorem_shell[OF assms]
+ by (auto intro!: UP.euclidean_domainI)
+qed
+
+corollary (in domain) univ_poly_is_principal:
+ assumes "subfield K R" shows "principal_domain (K[X])"
+proof -
+ interpret UP: euclidean_domain "K[X]" degree
+ using univ_poly_is_euclidean[OF assms] .
+ show ?thesis ..
+qed
+
+
subsection \<open>The Evaluation Homomorphism\<close>
lemma (in ring) eval_replicate:
@@ -1708,8 +1854,7 @@
have "eval (map2 (\<oplus>) p q) a = (eval p a) \<oplus> (eval q a)"
using assms
proof (induct p arbitrary: q)
- case Nil
- then show ?case by simp
+ case Nil thus ?case by simp
next
case (Cons b1 p')
then obtain b2 q' where q: "q = b2 # q'"
@@ -1717,7 +1862,7 @@
show ?case
using eval_in_carrier[OF _ Cons(5), of q']
eval_in_carrier[OF _ Cons(5), of p'] Cons unfolding q
- by (auto simp add: degree_def ring_simprules(7,13,22))
+ by (auto simp add: ring_simprules(7,13,22))
qed
moreover have "set (map2 (\<oplus>) p q) \<subseteq> carrier R"
using assms(1-2)
@@ -1752,13 +1897,13 @@
shows "eval (p @ [ b ]) a = ((eval p a) \<otimes> a) \<oplus> b"
using assms(1)
proof (induct p)
- case Nil thus ?case by (auto simp add: degree_def assms(2-3))
+ case Nil thus ?case by (auto simp add: assms(2-3))
next
case (Cons l q)
have "a [^] length q \<in> carrier R" "eval q a \<in> carrier R"
using eval_in_carrier Cons(2) assms(2-3) by auto
thus ?case
- using Cons assms(2-3) by (auto simp add: degree_def, algebra)
+ using Cons assms(2-3) by (auto, algebra)
qed
lemma (in ring) eval_append:
@@ -1787,18 +1932,18 @@
finally show ?case .
qed
-lemma (in ring) eval_monon:
+lemma (in ring) eval_monom:
assumes "b \<in> carrier R" and "a \<in> carrier R"
- shows "eval (monon b n) a = b \<otimes> (a [^] n)"
+ shows "eval (monom b n) a = b \<otimes> (a [^] n)"
proof (induct n)
case 0 thus ?case
- using assms unfolding monon_def by (auto simp add: degree_def)
+ using assms unfolding monom_def by auto
next
case (Suc n)
- have "monon b (Suc n) = (monon b n) @ [ \<zero> ]"
- unfolding monon_def by (simp add: replicate_append_same)
- hence "eval (monon b (Suc n)) a = ((eval (monon b n) a) \<otimes> a) \<oplus> \<zero>"
- using eval_append_aux[OF monon_in_carrier[OF assms(1)] zero_closed assms(2), of n] by simp
+ have "monom b (Suc n) = (monom b n) @ [ \<zero> ]"
+ unfolding monom_def by (simp add: replicate_append_same)
+ hence "eval (monom b (Suc n)) a = ((eval (monom b n) a) \<otimes> a) \<oplus> \<zero>"
+ using eval_append_aux[OF monom_in_carrier[OF assms(1)] zero_closed assms(2), of n] by simp
also have " ... = b \<otimes> (a [^] (Suc n))"
using Suc assms m_assoc by auto
finally show ?case .
@@ -1819,41 +1964,372 @@
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)
+ using assms(2-3) eval_in_carrier b by(induct q) (auto simp add: m_assoc r_distr)
ultimately have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (b \<otimes> eval q a) \<otimes> (a [^] n) \<oplus> \<zero>"
by simp
also have " ... = (b \<otimes> (a [^] n)) \<otimes> (eval q a)"
using eval_in_carrier[OF assms(2-3)] b assms(3) m_assoc m_comm by auto
- finally have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monon b n) a) \<otimes> (eval q a)"
- using eval_monon[OF b assms(3)] by simp }
+ finally have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monom b n) a) \<otimes> (eval q a)"
+ using eval_monom[OF b assms(3)] by simp }
note aux_lemma = this
case (Cons b p)
hence in_carrier:
- "eval (monon b (length p)) a \<in> carrier R" "eval p a \<in> carrier R" "eval q a \<in> carrier R" "b \<in> carrier R"
- using eval_in_carrier monon_in_carrier assms by auto
+ "eval (monom b (length p)) a \<in> carrier R" "eval p a \<in> carrier R" "eval q a \<in> carrier R" "b \<in> carrier R"
+ using eval_in_carrier monom_in_carrier assms by auto
have set_map: "set ((map ((\<otimes>) b) q) @ (replicate (length p) \<zero>)) \<subseteq> carrier R"
using in_carrier(4) assms(2) by (induct q) (auto)
have set_poly: "set (poly_mult p q) \<subseteq> carrier R"
using poly_mult_in_carrier[OF _ assms(2), of p] Cons(2) by auto
have "eval (poly_mult (b # p) q) a =
- ((eval (monon b (length p)) a) \<otimes> (eval q a)) \<oplus> ((eval p a) \<otimes> (eval q a))"
+ ((eval (monom b (length p)) a) \<otimes> (eval q a)) \<oplus> ((eval p a) \<otimes> (eval q a))"
using eval_poly_add[OF set_map set_poly assms(3)] aux_lemma[OF in_carrier(4), of "length p"] Cons
- by (auto simp del: poly_add.simps simp add: degree_def)
- also have " ... = ((eval (monon b (length p)) a) \<oplus> (eval p a)) \<otimes> (eval q a)"
+ by (auto simp del: poly_add.simps)
+ also have " ... = ((eval (monom b (length p)) a) \<oplus> (eval p a)) \<otimes> (eval q a)"
using l_distr[OF in_carrier(1-3)] by simp
also have " ... = (eval (b # p) a) \<otimes> (eval q a)"
- unfolding eval_monon[OF in_carrier(4) assms(3), of "length p"] by (auto simp add: degree_def)
+ unfolding eval_monom[OF in_carrier(4) assms(3), of "length p"] by auto
finally show ?case .
qed
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)]
- using polynomial_in_carrier eval_in_carrier eval_poly_add eval_poly_mult assms(2)
+ shows "(\<lambda>p. (eval p) a) \<in> ring_hom (K[X]) R"
+ unfolding univ_poly_def
+ using polynomial_in_carrier[OF assms(1)] 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 add: univ_poly_carrier
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 (K[X]) R (\<lambda>p. (eval p) a)"
+ unfolding ring_hom_cring_def ring_hom_cring_axioms_def
+ using domain.axioms(1)[OF univ_poly_is_domain[OF assms(1)]]
+ eval_is_hom[OF assms] cring_axioms by auto
+
+corollary (in domain) eval_ring_hom:
+ assumes "subring K R" and "a \<in> carrier R"
+ shows "ring_hom_ring (K[X]) 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 X Variable\<close>
+
+definition var :: "_ \<Rightarrow> 'a list" ("X\<index>")
+ where "X\<^bsub>R\<^esub> = [ \<one>\<^bsub>R\<^esub>, \<zero>\<^bsub>R\<^esub> ]"
+
+lemma (in ring) eval_var:
+ assumes "x \<in> carrier R" shows "eval X x = x"
+ using assms unfolding var_def by auto
+
+lemma (in domain) var_closed:
+ assumes "subring K R" shows "X \<in> carrier (K[X])" and "polynomial K X"
+ using subringE(2-3)[OF assms]
+ by (auto simp add: var_def univ_poly_def polynomial_def)
+
+lemma (in domain) poly_mult_var':
+ assumes "set p \<subseteq> carrier R"
+ shows "poly_mult X p = normalize (p @ [ \<zero> ])"
+ and "poly_mult p X = normalize (p @ [ \<zero> ])"
+proof -
+ from \<open>set p \<subseteq> carrier R\<close> have "poly_mult [ \<one> ] p = normalize p"
+ using poly_mult_one' by simp
+ thus "poly_mult X p = normalize (p @ [ \<zero> ])"
+ using poly_mult_append_zero[OF _ assms, of "[ \<one> ]"] normalize_idem
+ unfolding var_def by (auto simp del: poly_mult.simps)
+ thus "poly_mult p X = normalize (p @ [ \<zero> ])"
+ using poly_mult_comm[OF assms] unfolding var_def by simp
+qed
+
+lemma (in domain) poly_mult_var:
+ assumes "subring K R" "p \<in> carrier (K[X])"
+ shows "p \<otimes>\<^bsub>K[X]\<^esub> X = (if p = [] then [] else p @ [ \<zero> ])"
+proof -
+ have is_poly: "polynomial K p"
+ using assms(2) unfolding univ_poly_def by simp
+ hence "polynomial K (p @ [ \<zero> ])" if "p \<noteq> []"
+ using that subringE(2)[OF assms(1)] unfolding polynomial_def by auto
+ thus ?thesis
+ using poly_mult_var'(2)[OF polynomial_in_carrier[OF assms(1) is_poly]]
+ normalize_polynomial[of K "p @ [ \<zero> ]"]
+ by (auto simp add: univ_poly_mult[of R K])
+qed
+
+lemma (in domain) var_pow_closed:
+ assumes "subring K R" shows "X [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
+ using monoid.nat_pow_closed[OF univ_poly_is_monoid[OF assms] var_closed(1)[OF assms]] .
+
+lemma (in domain) unitary_monom_eq_var_pow:
+ assumes "subring K R" shows "monom \<one> n = X [^]\<^bsub>K[X]\<^esub> n"
+ using poly_mult_var[OF assms var_pow_closed[OF assms]] unfolding nat_pow_def monom_def
+ by (induct n) (auto simp add: univ_poly_one, metis append_Cons replicate_append_same)
+
+lemma (in domain) monom_eq_var_pow:
+ assumes "subring K R" "a \<in> carrier R - { \<zero> }"
+ shows "monom a n = [ a ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> n)"
+proof -
+ have "monom a n = map ((\<otimes>) a) (monom \<one> n)"
+ unfolding monom_def using assms(2) by (induct n) (auto)
+ also have " ... = poly_mult [ a ] (monom \<one> n)"
+ using poly_mult_const(1)[OF _ monom_is_polynomial assms(2)] carrier_is_subring by simp
+ also have " ... = [ a ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> n)"
+ unfolding unitary_monom_eq_var_pow[OF assms(1)] univ_poly_mult[of R K] by simp
+ finally show ?thesis .
+qed
+
+lemma (in ring) dense_repr_set_fst:
+ assumes "set p \<subseteq> K" shows "fst ` (set (dense_repr p)) \<subseteq> K - { \<zero> }"
+ using assms by (induct p) (auto)
+
+lemma (in ring) dense_repr_set_snd:
+ shows "snd ` (set (dense_repr p)) \<subseteq> {..< length p}"
+ by (induct p) (auto)
+
+lemma (in domain) dense_repr_monom_closed:
+ assumes "subring K R" "set p \<subseteq> K"
+ shows "t \<in> set (dense_repr p) \<Longrightarrow> monom (fst t) (snd t) \<in> carrier (K[X])"
+ using dense_repr_set_fst[OF assms(2)] monom_is_polynomial[OF assms(1)]
+ by (auto simp add: univ_poly_carrier)
+
+lemma (in domain) monom_finsum_decomp:
+ assumes "subring K R" "p \<in> carrier (K[X])"
+ shows "p = (\<Oplus>\<^bsub>K[X]\<^esub> t \<in> set (dense_repr p). monom (fst t) (snd t))"
+proof -
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF assms(1)] .
+
+ from \<open>p \<in> carrier (K[X])\<close> show ?thesis
+ proof (induct "length p" arbitrary: p rule: less_induct)
+ case less thus ?case
+ proof (cases p)
+ case Nil thus ?thesis
+ using UP.finsum_empty univ_poly_zero[of R K] by simp
+ next
+ case (Cons a l)
+ hence in_carrier:
+ "normalize l \<in> carrier (K[X])" "polynomial K (normalize l)" "polynomial K (a # l)"
+ using normalize_gives_polynomial polynomial_incl[of K p] less(2)
+ unfolding univ_poly_carrier by auto
+ have len_lt: "length (local.normalize l) < length p"
+ using normalize_length_le by (simp add: Cons le_imp_less_Suc)
+
+ have a: "a \<in> K - { \<zero> }"
+ using less(2) subringE(1)[OF assms(1)] unfolding Cons univ_poly_def polynomial_def by auto
+ hence "p = (monom a (length l)) \<oplus>\<^bsub>K[X]\<^esub> (of_dense (dense_repr (normalize l)))"
+ using monom_decomp[OF assms(1), of p] less(2) dense_repr_normalize
+ unfolding univ_poly_add univ_poly_carrier Cons by (auto simp del: poly_add.simps)
+ also have " ... = (monom a (length l)) \<oplus>\<^bsub>K[X]\<^esub> (normalize l)"
+ using monom_decomp[OF assms(1) in_carrier(2)] by simp
+ finally have "p = monom a (length l) \<oplus>\<^bsub>K[X]\<^esub>
+ (\<Oplus>\<^bsub>K[X]\<^esub> t \<in> set (dense_repr l). monom (fst t) (snd t))"
+ using less(1)[OF len_lt in_carrier(1)] dense_repr_normalize by simp
+
+ moreover have "(a, (length l)) \<notin> set (dense_repr l)"
+ using dense_repr_set_snd[of l] by auto
+ moreover have "monom a (length l) \<in> carrier (K[X])"
+ using monom_is_polynomial[OF assms(1) a] unfolding univ_poly_carrier by simp
+ moreover have "\<And>t. t \<in> set (dense_repr l) \<Longrightarrow> monom (fst t) (snd t) \<in> carrier (K[X])"
+ using dense_repr_monom_closed[OF assms(1)] polynomial_incl[OF in_carrier(3)] by auto
+ ultimately have "p = (\<Oplus>\<^bsub>K[X]\<^esub> t \<in> set (dense_repr (a # l)). monom (fst t) (snd t))"
+ using UP.add.finprod_insert a by auto
+ thus ?thesis unfolding Cons .
+ qed
+ qed
+qed
+
+lemma (in domain) var_pow_finsum_decomp:
+ assumes "subring K R" "p \<in> carrier (K[X])"
+ shows "p = (\<Oplus>\<^bsub>K[X]\<^esub> t \<in> set (dense_repr p). [ fst t ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> (snd t)))"
+proof -
+ let ?f = "\<lambda>t. monom (fst t) (snd t)"
+ let ?g = "\<lambda>t. [ fst t ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> (snd t))"
+
+ interpret UP: domain "K[X]"
+ using univ_poly_is_domain[OF assms(1)] .
+
+ have set_p: "set p \<subseteq> K"
+ using polynomial_incl assms(2) by (simp add: univ_poly_carrier)
+ hence f: "?f \<in> set (dense_repr p) \<rightarrow> carrier (K[X])"
+ using dense_repr_monom_closed[OF assms(1)] by auto
+
+ moreover
+ have "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> fst t \<in> carrier R - { \<zero> }"
+ using dense_repr_set_fst[OF set_p] subringE(1)[OF assms(1)] by auto
+ hence "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> monom (fst t) (snd t) = [ fst t ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> (snd t))"
+ using monom_eq_var_pow[OF assms(1)] by auto
+
+ ultimately show ?thesis
+ using UP.add.finprod_cong[of _ _ ?f ?g] monom_finsum_decomp[OF assms] by auto
+qed
+
+corollary (in domain) hom_var_pow_finsum:
+ assumes "subring K R" and "p \<in> carrier (K[X])" "ring_hom_ring (K[X]) A h"
+ shows "h p = (\<Oplus>\<^bsub>A\<^esub> t \<in> set (dense_repr p). h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t)))"
+proof -
+ let ?f = "\<lambda>t. [ fst t ] \<otimes>\<^bsub>K[X]\<^esub> (X [^]\<^bsub>K[X]\<^esub> (snd t))"
+ let ?g = "\<lambda>t. h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t))"
+
+ interpret UP: domain "K[X]" + A: ring A
+ using univ_poly_is_domain[OF assms(1)] ring_hom_ring.axioms(2)[OF assms(3)] by simp+
+
+ have const_in_carrier:
+ "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> [ fst t ] \<in> carrier (K[X])"
+ using dense_repr_set_fst[OF polynomial_incl, of K p] assms(2) const_is_polynomial[of _ K]
+ by (auto simp add: univ_poly_carrier)
+ hence f: "?f: set (dense_repr p) \<rightarrow> carrier (K[X])"
+ using UP.m_closed[OF _ var_pow_closed[OF assms(1)]] by auto
+ hence h: "h \<circ> ?f: set (dense_repr p) \<rightarrow> carrier A"
+ using ring_hom_memE(1)[OF ring_hom_ring.homh[OF assms(3)]] by (auto simp add: Pi_def)
+
+ have hp: "h p = (\<Oplus>\<^bsub>A\<^esub> t \<in> set (dense_repr p). (h \<circ> ?f) t)"
+ using ring_hom_ring.hom_finsum[OF assms(3) f] var_pow_finsum_decomp[OF assms(1-2)]
+ by (auto, meson o_apply)
+ have eq: "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t)) = (h \<circ> ?f) t"
+ using ring_hom_memE(2)[OF ring_hom_ring.homh[OF assms(3)]
+ const_in_carrier var_pow_closed[OF assms(1)]]
+ ring_hom_ring.nat_pow_hom[OF assms(3) var_closed(1)[OF assms(1)]] by auto
+ show ?thesis
+ using A.add.finprod_cong'[OF _ h eq] hp by simp
+qed
+
+corollary (in domain) determination_of_hom:
+ assumes "subring K R"
+ and "ring_hom_ring (K[X]) A h" "ring_hom_ring (K[X]) A g"
+ and "\<And>k. k \<in> K \<Longrightarrow> h [ k ] = g [ k ]" and "h X = g X"
+ shows "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> h p = g p"
+proof -
+ interpret A: ring A
+ using ring_hom_ring.axioms(2)[OF assms(2)] by simp
+
+ fix p assume p: "p \<in> carrier (K[X])"
+ hence
+ "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow> [ fst t ] \<in> carrier (K[X])"
+ using dense_repr_set_fst[OF polynomial_incl, of K p] const_is_polynomial[of _ K]
+ by (auto simp add: univ_poly_carrier)
+ hence f: "(\<lambda>t. h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t))): set (dense_repr p) \<rightarrow> carrier A"
+ using ring_hom_memE(1)[OF ring_hom_ring.homh[OF assms(2)]] var_closed(1)[OF assms(1)]
+ A.m_closed[OF _ A.nat_pow_closed]
+ by auto
+
+ have eq: "\<And>t. t \<in> set (dense_repr p) \<Longrightarrow>
+ g [ fst t ] \<otimes>\<^bsub>A\<^esub> (g X [^]\<^bsub>A\<^esub> (snd t)) = h [ fst t ] \<otimes>\<^bsub>A\<^esub> (h X [^]\<^bsub>A\<^esub> (snd t))"
+ using dense_repr_set_fst[OF polynomial_incl, of K p] p assms(4-5)
+ by (auto simp add: univ_poly_carrier)
+ show "h p = g p"
+ unfolding assms(2-3)[THEN hom_var_pow_finsum[OF assms(1) p]]
+ using A.add.finprod_cong'[OF _ f eq] by simp
+qed
+
+corollary (in domain) eval_as_unique_hom:
+ assumes "subring K R" "x \<in> carrier R"
+ and "ring_hom_ring (K[X]) R h"
+ and "\<And>k. k \<in> K \<Longrightarrow> h [ k ] = k" and "h X = x"
+ shows "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> h p = eval p x"
+ using determination_of_hom[OF assms(1,3) eval_ring_hom[OF assms(1-2)]]
+ eval_var[OF assms(2)] assms(4-5) subringE(1)[OF assms(1)]
+ by fastforce
+
+
+subsection \<open>The Constant Term\<close>
+
+definition (in ring) const_term :: "'a list \<Rightarrow> 'a"
+ where "const_term p = eval p \<zero>"
+
+lemma (in ring) const_term_eq_last:
+ assumes "set p \<subseteq> carrier R" and "a \<in> carrier R"
+ shows "const_term (p @ [ a ]) = a"
+ using assms by (induct p) (auto simp add: const_term_def)
+
+lemma (in ring) const_term_not_zero:
+ assumes "const_term p \<noteq> \<zero>" shows "p \<noteq> []"
+ using assms by (auto simp add: const_term_def)
+
+lemma (in ring) const_term_explicit:
+ assumes "set p \<subseteq> carrier R" "p \<noteq> []" and "const_term p = a"
+ obtains p' where "set p' \<subseteq> carrier R" and "p = p' @ [ a ]"
+proof -
+ obtain a' p' where p: "p = p' @ [ a' ]"
+ using assms(2) rev_exhaust by blast
+ have p': "set p' \<subseteq> carrier R" and a: "a = a'"
+ using assms const_term_eq_last[of p' a'] unfolding p by auto
+ show thesis
+ using p p' that unfolding a by blast
+qed
+
+lemma (in ring) const_term_zero:
+ assumes "subring K R" "polynomial K p" "p \<noteq> []" and "const_term p = \<zero>"
+ obtains p' where "polynomial K p'" "p' \<noteq> []" and "p = p' @ [ \<zero> ]"
+proof -
+ obtain p' where p': "p = p' @ [ \<zero> ]"
+ using const_term_explicit[OF polynomial_in_carrier[OF assms(1-2)] assms(3-4)] by auto
+ have "polynomial K p'" "p' \<noteq> []"
+ using assms(2) unfolding p' polynomial_def by auto
+ thus thesis using p' ..
+qed
+
+lemma (in cring) const_term_simprules:
+ shows "\<And>p. set p \<subseteq> carrier R \<Longrightarrow> const_term p \<in> carrier R"
+ and "\<And>p q. \<lbrakk> set p \<subseteq> carrier R; set q \<subseteq> carrier R \<rbrakk> \<Longrightarrow>
+ const_term (poly_mult p q) = const_term p \<otimes> const_term q"
+ and "\<And>p q. \<lbrakk> set p \<subseteq> carrier R; set q \<subseteq> carrier R \<rbrakk> \<Longrightarrow>
+ const_term (poly_add p q) = const_term p \<oplus> const_term q"
+ using eval_poly_mult eval_poly_add eval_in_carrier zero_closed
+ unfolding const_term_def by auto
+
+lemma (in domain) const_term_simprules_shell:
+ assumes "subring K R"
+ shows "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> const_term p \<in> K"
+ and "\<And>p q. \<lbrakk> p \<in> carrier (K[X]); q \<in> carrier (K[X]) \<rbrakk> \<Longrightarrow>
+ const_term (p \<otimes>\<^bsub>K[X]\<^esub> q) = const_term p \<otimes> const_term q"
+ and "\<And>p q. \<lbrakk> p \<in> carrier (K[X]); q \<in> carrier (K[X]) \<rbrakk> \<Longrightarrow>
+ const_term (p \<oplus>\<^bsub>K[X]\<^esub> q) = const_term p \<oplus> const_term q"
+ and "\<And>p. p \<in> carrier (K[X]) \<Longrightarrow> const_term (\<ominus>\<^bsub>K[X]\<^esub> p) = \<ominus> (const_term p)"
+ using eval_is_hom[OF assms(1) zero_closed]
+ unfolding ring_hom_def const_term_def
+proof (auto)
+ fix p assume p: "p \<in> carrier (K[X])"
+ hence "set p \<subseteq> carrier R"
+ using polynomial_in_carrier[OF assms(1)] by (auto simp add: univ_poly_def)
+ thus "eval (\<ominus>\<^bsub>K [X]\<^esub> p) \<zero> = \<ominus> local.eval p \<zero>"
+ unfolding univ_poly_a_inv_def'[OF assms(1) p]
+ by (induct p) (auto simp add: eval_in_carrier l_minus local.minus_add)
+
+ have "set p \<subseteq> K"
+ using p by (auto simp add: univ_poly_def polynomial_def)
+ thus "eval p \<zero> \<in> K"
+ using subringE(1-2,6-7)[OF assms]
+ by (induct p) (auto, metis assms nat_pow_0 nat_pow_zero subringE(3))
+qed
+
+
+subsection \<open>The Canonical Embedding of K in K[X]\<close>
+
+lemma (in field) univ_poly_carrier_subfield_of_consts:
+ "subfield { p \<in> carrier ((carrier R)[X]). degree p = 0 } ((carrier R)[X])"
+proof -
+ have ring_hom: "ring_hom_ring R ((carrier R)[X]) (\<lambda>k. normalize [ k ])"
+ by (rule ring_hom_ringI[OF ring_axioms univ_poly_is_ring[OF carrier_is_subring]])
+ (auto simp add: univ_poly_def)
+ have subfield: "subfield ((\<lambda>k. normalize [ k ]) ` (carrier R)) ((carrier R)[X])"
+ using ring_hom_ring.img_is_subfield(2)[OF ring_hom carrier_is_subfield]
+ unfolding univ_poly_def by auto
+
+ have "(\<lambda>k. normalize [ k ]) ` (carrier R) = insert [] { [ k ] | k. k \<in> carrier R - { \<zero> } }"
+ by auto
+ also have " ... = { p \<in> carrier ((carrier R)[X]). degree p = 0 }"
+ unfolding univ_poly_def polynomial_def
+ by (auto, metis le_Suc_eq le_zero_eq length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subsetCE)
+ finally have "(\<lambda>k. normalize [ k ]) ` (carrier R) = { p \<in> carrier ((carrier R)[X]). degree p = 0 }" .
+ thus ?thesis
+ using subfield by auto
+qed
+
+proposition (in ring) univ_poly_subfield_of_consts:
+ assumes "subfield K R" shows "subfield { p \<in> carrier (K[X]). degree p = 0 } (K[X])"
+ using field.univ_poly_carrier_subfield_of_consts[OF subfield_iff(2)[OF assms]]
+ univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto
+
end
--- a/src/HOL/Algebra/Ring_Divisibility.thy Thu Jul 19 17:28:13 2018 +0200
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Thu Jul 19 23:23:10 2018 +0200
@@ -3,28 +3,9 @@
*)
theory Ring_Divisibility
-imports Ideal Divisibility QuotRing
-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)
+imports Ideal Divisibility QuotRing Multiplicative_Group HOL.Zorn
-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
-
+begin
section \<open>The Arithmetic of Rings\<close>
@@ -36,81 +17,40 @@
locale factorial_domain = domain + factorial_monoid "mult_of R"
locale noetherian_ring = ring +
- assumes finetely_gen: "ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+ assumes finetely_gen: "ideal I R \<Longrightarrow> \<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A"
locale noetherian_domain = noetherian_ring + domain
locale principal_domain = domain +
- assumes principal_I: "ideal I R \<Longrightarrow> principalideal I R"
+ assumes exists_gen: "ideal I R \<Longrightarrow> \<exists>a \<in> carrier R. I = PIdl a"
-locale euclidean_domain = R?: domain R for R (structure) + fixes \<phi> :: "'a \<Rightarrow> nat"
+locale euclidean_domain =
+ domain R for R (structure) + fixes \<phi> :: "'a \<Rightarrow> nat"
assumes euclidean_function:
" \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
\<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
-lemma (in domain) mult_of_is_comm_monoid: "comm_monoid (mult_of R)"
- apply (rule comm_monoidI)
- apply (auto simp add: integral_iff m_assoc)
- apply (simp add: m_comm)
- done
+definition ring_irreducible :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> bool" ("ring'_irreducible\<index>")
+ where "ring_irreducible\<^bsub>R\<^esub> a \<longleftrightarrow> (a \<noteq> \<zero>\<^bsub>R\<^esub>) \<and> (irreducible R a)"
-lemma (in domain) cancel_property: "comm_monoid_cancel (mult_of R)"
- by (rule comm_monoid_cancelI) (auto simp add: mult_of_is_comm_monoid m_rcancel)
+definition ring_prime :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> bool" ("ring'_prime\<index>")
+ where "ring_prime\<^bsub>R\<^esub> a \<longleftrightarrow> (a \<noteq> \<zero>\<^bsub>R\<^esub>) \<and> (prime R a)"
+
-sublocale domain < mult_of: comm_monoid_cancel "(mult_of R)"
+subsection \<open>The cancellative monoid of a domain. \<close>
+
+sublocale domain < mult_of: comm_monoid_cancel "mult_of R"
rewrites "mult (mult_of R) = mult R"
- and "one (mult_of R) = one R"
- using cancel_property by auto
-
-sublocale noetherian_domain \<subseteq> domain ..
-
-sublocale principal_domain \<subseteq> domain ..
-
-sublocale euclidean_domain \<subseteq> domain ..
-
-lemma (in factorial_monoid) is_factorial_monoid: "factorial_monoid G" ..
+ and "one (mult_of R) = one R"
+ using m_comm m_assoc
+ by (auto intro!: comm_monoid_cancelI comm_monoidI
+ simp add: m_rcancel integral_iff)
sublocale factorial_domain < mult_of: factorial_monoid "mult_of R"
rewrites "mult (mult_of R) = mult R"
- and "one (mult_of R) = one R"
+ and "one (mult_of R) = one R"
using factorial_monoid_axioms by auto
-lemma (in domain) factorial_domainI:
- assumes "\<And>a. a \<in> carrier (mult_of R) \<Longrightarrow>
- \<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs a"
- and "\<And>a fs fs'. \<lbrakk> a \<in> carrier (mult_of R);
- set fs \<subseteq> carrier (mult_of R);
- set fs' \<subseteq> carrier (mult_of R);
- wfactors (mult_of R) fs a;
- wfactors (mult_of R) fs' a \<rbrakk> \<Longrightarrow>
- essentially_equal (mult_of R) fs fs'"
- shows "factorial_domain R"
- unfolding factorial_domain_def using mult_of.factorial_monoidI assms domain_axioms by auto
-
-lemma (in domain) is_domain: "domain R" ..
-
-lemma (in ring) noetherian_ringI:
- assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
- shows "noetherian_ring R"
- unfolding noetherian_ring_def noetherian_ring_axioms_def using assms is_ring by simp
-
-lemma (in domain) noetherian_domainI:
- assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
- shows "noetherian_domain R"
- unfolding noetherian_domain_def noetherian_ring_def noetherian_ring_axioms_def
- using assms is_ring is_domain by simp
-
-lemma (in domain) principal_domainI:
- assumes "\<And>I. ideal I R \<Longrightarrow> principalideal I R"
- shows "principal_domain R"
- unfolding principal_domain_def principal_domain_axioms_def using is_domain assms by auto
-
-lemma (in domain) principal_domainI2:
- assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>a \<in> carrier R. I = PIdl a"
- shows "principal_domain R"
- unfolding principal_domain_def principal_domain_axioms_def
- using is_domain assms principalidealI cgenideal_eq_genideal by auto
-
lemma (in domain) euclidean_domainI:
assumes "\<And>a b. \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
\<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
@@ -118,13 +58,297 @@
using assms by unfold_locales auto
-subsection \<open>Basic Properties\<close>
+subsection \<open>Passing from R to mult_of R and vice-versa. \<close>
+
+lemma divides_mult_imp_divides [simp]: "a divides\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a divides\<^bsub>R\<^esub> b"
+ unfolding factor_def by auto
+
+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
+
+lemma (in cring) divides_one:
+ assumes "a \<in> carrier R"
+ shows "a divides \<one> \<longleftrightarrow> a \<in> Units R"
+ using assms m_comm unfolding factor_def Units_def by force
+
+lemma (in ring) one_divides:
+ assumes "a \<in> carrier R" shows "\<one> divides a"
+ using assms unfolding factor_def by simp
+
+lemma (in ring) divides_zero:
+ assumes "a \<in> carrier R" shows "a divides \<zero>"
+ using r_null[OF assms] unfolding factor_def by force
+
+lemma (in ring) zero_divides:
+ shows "\<zero> divides a \<longleftrightarrow> a = \<zero>"
+ unfolding factor_def by auto
+
+lemma (in domain) divides_mult_zero:
+ assumes "a \<in> carrier R" shows "a divides\<^bsub>(mult_of R)\<^esub> \<zero> \<Longrightarrow> a = \<zero>"
+ using integral[OF _ assms] unfolding factor_def by auto
+
+lemma (in ring) divides_mult:
+ assumes "a \<in> carrier R" "c \<in> carrier R"
+ shows "a divides b \<Longrightarrow> (c \<otimes> a) divides (c \<otimes> b)"
+ using m_assoc[OF assms(2,1)] unfolding factor_def by auto
+
+lemma (in domain) mult_divides:
+ assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R - { \<zero> }"
+ shows "(c \<otimes> a) divides (c \<otimes> b) \<Longrightarrow> a divides b"
+ using assms m_assoc[of c] unfolding factor_def by (simp add: m_lcancel)
+
+lemma (in domain) assoc_iff_assoc_mult:
+ assumes "a \<in> carrier R" and "b \<in> carrier R"
+ shows "a \<sim> b \<longleftrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+proof
+ assume "a \<sim>\<^bsub>(mult_of R)\<^esub> b" thus "a \<sim> b"
+ unfolding associated_def factor_def by auto
+next
+ assume A: "a \<sim> b"
+ then obtain c1 c2
+ where c1: "c1 \<in> carrier R" "a = b \<otimes> c1" and c2: "c2 \<in> carrier R" "b = a \<otimes> c2"
+ unfolding associated_def factor_def by auto
+ show "a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+ proof (cases "a = \<zero>")
+ assume a: "a = \<zero>" then have b: "b = \<zero>"
+ using c2 by auto
+ show ?thesis
+ unfolding associated_def factor_def a b by auto
+ next
+ assume a: "a \<noteq> \<zero>"
+ hence b: "b \<noteq> \<zero>" and c1_not_zero: "c1 \<noteq> \<zero>"
+ using c1 assms by auto
+ hence c2_not_zero: "c2 \<noteq> \<zero>"
+ using c2 assms by auto
+ show ?thesis
+ unfolding associated_def factor_def using c1 c2 c1_not_zero c2_not_zero a b by auto
+ qed
+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
+
+lemma (in domain) ring_associated_iff:
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "a \<sim> b \<longleftrightarrow> (\<exists>u \<in> Units R. a = u \<otimes> b)"
+proof (cases "a = \<zero>")
+ assume [simp]: "a = \<zero>" show ?thesis
+ proof
+ assume "a \<sim> b" thus "\<exists>u \<in> Units R. a = u \<otimes> b"
+ using zero_divides unfolding associated_def by force
+ next
+ assume "\<exists>u \<in> Units R. a = u \<otimes> b" then have "b = \<zero>"
+ by (metis Units_closed Units_l_cancel \<open>a = \<zero>\<close> assms r_null)
+ thus "a \<sim> b"
+ using zero_divides[of \<zero>] by auto
+ qed
+next
+ assume a: "a \<noteq> \<zero>" show ?thesis
+ proof (cases "b = \<zero>")
+ assume "b = \<zero>" thus ?thesis
+ using assms a zero_divides[of a] r_null unfolding associated_def by blast
+ next
+ assume b: "b \<noteq> \<zero>"
+ have "(\<exists>u \<in> Units R. a = u \<otimes> b) \<longleftrightarrow> (\<exists>u \<in> Units R. a = b \<otimes> u)"
+ using m_comm[OF assms(2)] Units_closed by auto
+ thus ?thesis
+ using mult_of.associated_iff[of a b] a b assms
+ unfolding assoc_iff_assoc_mult[OF assms] Units_mult_eq_Units
+ by auto
+ qed
+qed
+
+lemma (in domain) properfactor_mult_imp_properfactor:
+ "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor (mult_of R) b a \<Longrightarrow> properfactor R b a"
+proof -
+ assume A: "a \<in> carrier R" "b \<in> carrier R" "properfactor (mult_of R) b a"
+ then obtain c where c: "c \<in> carrier (mult_of R)" "a = b \<otimes> c"
+ unfolding properfactor_def factor_def by auto
+ have "a \<noteq> \<zero>"
+ proof (rule ccontr)
+ assume a: "\<not> a \<noteq> \<zero>"
+ hence "b = \<zero>" using c A integral[of b c] by auto
+ hence "b = a \<otimes> \<one>" using a A by simp
+ hence "a divides\<^bsub>(mult_of R)\<^esub> b"
+ unfolding factor_def by auto
+ thus False using A unfolding properfactor_def by simp
+ qed
+ hence "b \<noteq> \<zero>"
+ 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)
+qed
+
+lemma (in domain) properfactor_imp_properfactor_mult:
+ "\<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor R b a \<Longrightarrow> properfactor (mult_of R) b a"
+ unfolding properfactor_def factor_def by auto
+
+lemma (in domain) properfactor_of_zero:
+ assumes "b \<in> carrier R"
+ shows "\<not> properfactor (mult_of R) b \<zero>" and "properfactor R b \<zero> \<longleftrightarrow> b \<noteq> \<zero>"
+ using divides_mult_zero[OF assms] divides_zero[OF assms] unfolding properfactor_def by auto
+
+
+subsection \<open>Irreducible\<close>
+
+text \<open>The following lemmas justify the need for a definition of irreducible specific to rings:
+ for "irreducible R", we need to suppose we are not in a field (which is plausible,
+ but "\<not> field R" is an assumption we want to avoid; for "irreducible (mult_of R)", zero
+ is allowed. \<close>
-text \<open>Links between domains and commutative cancellative monoids\<close>
+lemma (in domain) zero_is_irreducible_mult:
+ shows "irreducible (mult_of R) \<zero>"
+ unfolding irreducible_def Units_def properfactor_def factor_def
+ using integral_iff by fastforce
+
+lemma (in domain) zero_is_irreducible_iff_field:
+ shows "irreducible R \<zero> \<longleftrightarrow> field R"
+proof
+ assume irr: "irreducible R \<zero>"
+ have "\<And>a. \<lbrakk> a \<in> carrier R; a \<noteq> \<zero> \<rbrakk> \<Longrightarrow> properfactor R a \<zero>"
+ unfolding properfactor_def factor_def by (auto, metis r_null zero_closed)
+ hence "carrier R - { \<zero> } = Units R"
+ using irr unfolding irreducible_def by auto
+ thus "field R"
+ using field.intro[OF domain_axioms] unfolding field_axioms_def by simp
+next
+ assume field: "field R" show "irreducible R \<zero>"
+ using field.field_Units[OF field]
+ unfolding irreducible_def properfactor_def factor_def by blast
+qed
+
+lemma (in domain) irreducible_imp_irreducible_mult:
+ "\<lbrakk> a \<in> carrier R; irreducible R a \<rbrakk> \<Longrightarrow> irreducible (mult_of R) a"
+ using zero_is_irreducible_mult Units_mult_eq_Units properfactor_mult_imp_properfactor
+ by (cases "a = \<zero>") (auto simp add: irreducible_def)
+
+lemma (in domain) irreducible_mult_imp_irreducible:
+ "\<lbrakk> a \<in> carrier R - { \<zero> }; irreducible (mult_of R) a \<rbrakk> \<Longrightarrow> irreducible R a"
+ unfolding irreducible_def using properfactor_imp_properfactor_mult properfactor_divides by fastforce
+
+lemma (in domain) ring_irreducibleE:
+ assumes "r \<in> carrier R" and "ring_irreducible r"
+ shows "r \<noteq> \<zero>" "irreducible R r" "irreducible (mult_of R) r" "r \<notin> Units R"
+ and "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> r = a \<otimes> b \<Longrightarrow> a \<in> Units R \<or> b \<in> Units R"
+proof -
+ show "irreducible (mult_of R) r" "irreducible R r"
+ using assms irreducible_imp_irreducible_mult unfolding ring_irreducible_def by auto
+ show "r \<noteq> \<zero>" "r \<notin> Units R"
+ using assms unfolding ring_irreducible_def irreducible_def by auto
+next
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and r: "r = a \<otimes> b"
+ show "a \<in> Units R \<or> b \<in> Units R"
+ proof (cases "properfactor R a r")
+ assume "properfactor R a r" thus ?thesis
+ using a assms(2) unfolding ring_irreducible_def irreducible_def by auto
+ next
+ assume not_proper: "\<not> properfactor R a r"
+ hence "r divides a"
+ using r b unfolding properfactor_def by auto
+ then obtain c where c: "c \<in> carrier R" "a = r \<otimes> c"
+ unfolding factor_def by auto
+ have "\<one> = c \<otimes> b"
+ using r c(1) b assms m_assoc m_lcancel[OF _ assms(1) one_closed m_closed[OF c(1) b]]
+ unfolding c(2) ring_irreducible_def by auto
+ thus ?thesis
+ using c(1) b m_comm unfolding Units_def by auto
+ qed
+qed
+
+lemma (in domain) ring_irreducibleI:
+ assumes "r \<in> carrier R - { \<zero> }" "r \<notin> Units R"
+ and "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> r = a \<otimes> b \<Longrightarrow> a \<in> Units R \<or> b \<in> Units R"
+ shows "ring_irreducible r"
+ unfolding ring_irreducible_def
+proof
+ show "r \<noteq> \<zero>" using assms(1) by blast
+next
+ show "irreducible R r"
+ proof (rule irreducibleI[OF assms(2)])
+ fix a assume a: "a \<in> carrier R" "properfactor R a r"
+ then obtain b where b: "b \<in> carrier R" "r = a \<otimes> b"
+ unfolding properfactor_def factor_def by blast
+ hence "a \<in> Units R \<or> b \<in> Units R"
+ using assms(3)[OF a(1) b(1)] by simp
+ thus "a \<in> Units R"
+ proof (auto)
+ assume "b \<in> Units R"
+ hence "r \<otimes> inv b = a" and "inv b \<in> carrier R"
+ using b a by (simp add: m_assoc)+
+ thus ?thesis
+ using a(2) unfolding properfactor_def factor_def by blast
+ qed
+ qed
+qed
+
+lemma (in domain) ring_irreducibleI':
+ assumes "r \<in> carrier R - { \<zero> }" "irreducible (mult_of R) r"
+ shows "ring_irreducible r"
+ unfolding ring_irreducible_def
+ using irreducible_mult_imp_irreducible[OF assms] assms(1) by auto
+
+
+subsection \<open>Primes\<close>
+
+lemma (in domain) zero_is_prime: "prime R \<zero>" "prime (mult_of R) \<zero>"
+ using integral unfolding prime_def factor_def Units_def by auto
+
+lemma (in domain) prime_eq_prime_mult:
+ assumes "p \<in> carrier R"
+ shows "prime R p \<longleftrightarrow> prime (mult_of R) p"
+proof (cases "p = \<zero>", auto simp add: zero_is_prime)
+ assume "p \<noteq> \<zero>" "prime R p" thus "prime (mult_of R) p"
+ unfolding prime_def
+ using divides_mult_imp_divides Units_mult_eq_Units mult_mult_of
+ by (metis DiffD1 assms carrier_mult_of divides_imp_divides_mult)
+next
+ assume p: "p \<noteq> \<zero>" "prime (mult_of R) p" show "prime R p"
+ proof (rule primeI)
+ show "p \<notin> Units R"
+ using p(2) Units_mult_eq_Units unfolding prime_def by simp
+ next
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and dvd: "p divides a \<otimes> b"
+ then obtain c where c: "c \<in> carrier R" "a \<otimes> b = p \<otimes> c"
+ unfolding factor_def by auto
+ show "p divides a \<or> p divides b"
+ proof (cases "a \<otimes> b = \<zero>")
+ case True thus ?thesis
+ using integral[OF _ a b] c unfolding factor_def by force
+ next
+ case False
+ hence "p divides\<^bsub>(mult_of R)\<^esub> (a \<otimes> b)"
+ using divides_imp_divides_mult[OF assms _ dvd] m_closed[OF a b] by simp
+ moreover have "a \<noteq> \<zero>" "b \<noteq> \<zero>" "c \<noteq> \<zero>"
+ using False a b c p l_null integral_iff by (auto, simp add: assms)
+ ultimately show ?thesis
+ using a b p unfolding prime_def
+ by (auto, metis Diff_iff divides_mult_imp_divides singletonD)
+ qed
+ qed
+qed
+
+lemma (in domain) ring_primeE:
+ assumes "p \<in> carrier R" "ring_prime p"
+ shows "p \<noteq> \<zero>" "prime (mult_of R) p" "prime R p"
+ using assms prime_eq_prime_mult unfolding ring_prime_def by auto
+
+lemma (in ring) ring_primeI: (* in ring only to avoid instantiating R *)
+ assumes "p \<noteq> \<zero>" "prime R p" shows "ring_prime p"
+ using assms unfolding ring_prime_def by auto
+
+lemma (in domain) ring_primeI':
+ assumes "p \<in> carrier R - { \<zero> }" "prime (mult_of R) p"
+ shows "ring_prime p"
+ using assms prime_eq_prime_mult unfolding ring_prime_def by auto
+
+
+subsection \<open>Basic Properties\<close>
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)"
+ shows "PIdl b \<subseteq> PIdl a \<longleftrightarrow> a divides b"
proof
show "PIdl b \<subseteq> PIdl a \<Longrightarrow> a divides b"
proof -
@@ -153,393 +377,289 @@
lemma (in cring) associated_iff_same_ideal:
assumes "a \<in> carrier R" "b \<in> carrier R"
- shows "(a \<sim> b) = (PIdl a = PIdl b)"
+ shows "a \<sim> b \<longleftrightarrow> PIdl a = PIdl b"
unfolding associated_def
using to_contain_is_to_divide[OF assms]
- to_contain_is_to_divide[OF assms(2) assms(1)] by auto
-
-lemma divides_mult_imp_divides [simp]: "a divides\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a divides\<^bsub>R\<^esub> b"
- unfolding factor_def by auto
-
-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
-
-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
-
-lemma (in domain) Units_mult_eq_Units [simp]: "Units (mult_of R) = Units R"
- unfolding Units_def using insert_Diff integral_iff by auto
+ to_contain_is_to_divide[OF assms(2,1)] by auto
-lemma (in domain) properfactor_mult_imp_properfactor:
- "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor (mult_of R) b a \<Longrightarrow> properfactor R b a"
-proof -
- assume A: "a \<in> carrier R" "b \<in> carrier R" "properfactor (mult_of R) b a"
- then obtain c where c: "c \<in> carrier (mult_of R)" "a = b \<otimes> c"
- unfolding properfactor_def factor_def by auto
- have "a \<noteq> \<zero>"
- proof (rule ccontr)
- assume a: "\<not> a \<noteq> \<zero>"
- hence "b = \<zero>" using c A integral[of b c] by auto
- hence "b = a \<otimes> \<one>" using a A by simp
- hence "a divides\<^bsub>(mult_of R)\<^esub> b"
- unfolding factor_def by auto
- thus False using A unfolding properfactor_def by simp
+lemma (in cring) ideal_eq_carrier_iff:
+ 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
- hence "b \<noteq> \<zero>"
- 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)
+ thus "carrier R = PIdl a"
+ using assms by (simp add: cgenideal_eq_rcos r_coset_subset_G subset_antisym)
qed
-lemma (in domain) properfactor_imp_properfactor_mult:
- "\<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor R b a \<Longrightarrow> properfactor (mult_of R) b a"
- unfolding properfactor_def factor_def by auto
-
lemma (in domain) primeideal_iff_prime:
- assumes "p \<in> carrier (mult_of R)"
- shows "(primeideal (PIdl p) R) = (prime (mult_of R) p)"
-proof
- show "prime (mult_of R) p \<Longrightarrow> primeideal (PIdl p) R"
- proof (rule primeidealI)
- assume A: "prime (mult_of R) p"
- show "ideal (PIdl p) R" and "cring R"
- using assms is_cring by (auto simp add: cgenideal_ideal)
- show "carrier R \<noteq> PIdl p"
- proof (rule ccontr)
- assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp
- then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>"
- unfolding cginideal_def' by (metis (no_types, lifting) image_iff one_closed)
- hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto
- thus False using A unfolding prime_def by simp
- qed
- fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> PIdl p"
- thus "a \<in> PIdl p \<or> b \<in> PIdl p"
- proof (cases "a = \<zero> \<or> b = \<zero>")
- case True thus "a \<in> PIdl p \<or> b \<in> PIdl p" using ab a b by auto
+ assumes "p \<in> carrier R - { \<zero> }"
+ shows "primeideal (PIdl p) R \<longleftrightarrow> ring_prime p"
+proof
+ assume PIdl: "primeideal (PIdl p) R" show "ring_prime p"
+ proof (rule ring_primeI)
+ show "p \<noteq> \<zero>" using assms by simp
+ next
+ show "prime R p"
+ proof (rule primeI)
+ show "p \<notin> Units R"
+ using ideal_eq_carrier_iff[of p] assms primeideal.I_notcarr[OF PIdl] by auto
next
- { fix a assume "a \<in> carrier R" "p divides\<^bsub>mult_of R\<^esub> a"
- then obtain c where "c \<in> carrier R" "a = p \<otimes> c"
- unfolding factor_def by auto
- hence "a \<in> PIdl p" unfolding cgenideal_def using assms m_comm by auto }
- note aux_lemma = this
-
- case False hence "a \<noteq> \<zero> \<and> b \<noteq> \<zero>" by simp
- hence diff_zero: "a \<otimes> b \<noteq> \<zero>" using a b integral by blast
- then obtain c where c: "c \<in> carrier R" "a \<otimes> b = p \<otimes> c"
- using assms ab m_comm unfolding cgenideal_def by auto
- hence "c \<noteq> \<zero>" using c assms diff_zero by auto
- hence "p divides\<^bsub>(mult_of R)\<^esub> (a \<otimes> b)"
- unfolding factor_def using ab c by auto
- hence "p divides\<^bsub>(mult_of R)\<^esub> a \<or> p divides\<^bsub>(mult_of R)\<^esub> b"
- using A a b False unfolding prime_def by auto
- thus "a \<in> PIdl p \<or> b \<in> PIdl p" using a b aux_lemma by blast
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and dvd: "p divides a \<otimes> b"
+ hence "a \<otimes> b \<in> PIdl p"
+ by (meson assms DiffD1 cgenideal_self contra_subsetD m_closed to_contain_is_to_divide)
+ hence "a \<in> PIdl p \<or> b \<in> PIdl p"
+ using primeideal.I_prime[OF PIdl a b] by simp
+ thus "p divides a \<or> p divides b"
+ using assms a b Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
qed
qed
next
- show "primeideal (PIdl p) R \<Longrightarrow> prime (mult_of R) p"
- proof -
- assume A: "primeideal (PIdl p) R" show "prime (mult_of R) p"
- proof (rule primeI)
- show "p \<notin> Units (mult_of R)"
- proof (rule ccontr)
- assume "\<not> p \<notin> Units (mult_of R)"
- hence p: "p \<in> Units (mult_of R)" by simp
- then obtain q where q: "q \<in> carrier R - { \<zero> }" "p \<otimes> q = \<one>" "q \<otimes> p = \<one>"
- unfolding Units_def apply simp by blast
- have "PIdl p = carrier R"
- proof
- show "PIdl p \<subseteq> carrier R"
- by (simp add: assms A additive_subgroup.a_subset ideal.axioms(1) primeideal.axioms(1))
- next
- show "carrier R \<subseteq> PIdl p"
- proof
- fix r assume r: "r \<in> carrier R" hence "r = (r \<otimes> q) \<otimes> p"
- using p q m_assoc unfolding Units_def by simp
- thus "r \<in> PIdl p" unfolding cgenideal_def using q r m_closed by blast
- qed
- qed
- moreover have "PIdl p \<noteq> carrier R" using A primeideal.I_notcarr by auto
- ultimately show False by simp
- qed
- next
- { fix a assume "a \<in> PIdl p" and a: "a \<noteq> \<zero>"
- then obtain c where c: "c \<in> carrier R" "a = p \<otimes> c"
- unfolding cgenideal_def using m_comm assms by auto
- hence "c \<noteq> \<zero>" using assms a by auto
- hence "p divides\<^bsub>mult_of R\<^esub> a" unfolding factor_def using c by auto }
- note aux_lemma = this
-
- fix a b
- assume a: "a \<in> carrier (mult_of R)" and b: "b \<in> carrier (mult_of R)"
- and p: "p divides\<^bsub>mult_of R\<^esub> a \<otimes>\<^bsub>mult_of R\<^esub> b"
- then obtain c where "c \<in> carrier R" "a \<otimes> b = c \<otimes> p"
- unfolding factor_def using m_comm assms by auto
- hence "a \<otimes> b \<in> PIdl p" unfolding cgenideal_def by blast
- hence "a \<in> PIdl p \<or> b \<in> PIdl p" using A primeideal.I_prime[OF A] a b by auto
- thus "p divides\<^bsub>mult_of R\<^esub> a \<or> p divides\<^bsub>mult_of R\<^esub> b"
- using a b aux_lemma by auto
- qed
+ assume prime: "ring_prime p" show "primeideal (PIdl p) R"
+ proof (rule primeidealI[OF cgenideal_ideal cring_axioms])
+ show "p \<in> carrier R" and "carrier R \<noteq> PIdl p"
+ using ideal_eq_carrier_iff[of p] assms prime
+ unfolding ring_prime_def prime_def by auto
+ next
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" "a \<otimes> b \<in> PIdl p"
+ hence "p divides a \<otimes> b"
+ using assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
+ hence "p divides a \<or> p divides b"
+ using a b assms primeE[OF ring_primeE(3)[OF _ prime]] by auto
+ thus "a \<in> PIdl p \<or> b \<in> PIdl p"
+ using a b assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
qed
qed
subsection \<open>Noetherian Rings\<close>
-lemma (in noetherian_ring) trivial_ideal_seq:
- assumes "\<And>i :: nat. ideal (I i) R"
- and "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
- shows "\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n"
-proof -
- have "ideal (\<Union>i. I i) R"
- proof
- show "(\<Union>i. I i) \<subseteq> carrier (add_monoid R)"
- using additive_subgroup.a_subset assms(1) ideal.axioms(1) by fastforce
- have "\<one>\<^bsub>add_monoid R\<^esub> \<in> I 0"
- by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
- thus "\<one>\<^bsub>add_monoid R\<^esub> \<in> (\<Union>i. I i)" by blast
- next
- fix x y assume x: "x \<in> (\<Union>i. I i)" and y: "y \<in> (\<Union>i. I i)"
- then obtain i j where i: "x \<in> I i" and j: "y \<in> I j" by blast
- hence "inv\<^bsub>add_monoid R\<^esub> x \<in> I i"
- by (simp add: additive_subgroup.a_subgroup assms(1) ideal.axioms(1) subgroup.m_inv_closed)
- thus "inv\<^bsub>add_monoid R\<^esub> x \<in> (\<Union>i. I i)" by blast
- have "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> I (max i j)"
- by (metis add.subgroupE(4) additive_subgroup.a_subgroup assms(1-2) i j ideal.axioms(1)
- max.cobounded1 max.cobounded2 monoid.select_convs(1) rev_subsetD)
- thus "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> (\<Union>i. I i)" by blast
+lemma (in ring) chain_Union_is_ideal:
+ assumes "subset.chain { I. ideal I R } C"
+ shows "ideal (if C = {} then { \<zero> } else (\<Union>C)) R"
+proof (cases "C = {}")
+ case True thus ?thesis by (simp add: zeroideal)
+next
+ case False have "ideal (\<Union>C) R"
+ proof (rule idealI[OF ring_axioms])
+ show "subgroup (\<Union>C) (add_monoid R)"
+ proof
+ show "\<Union>C \<subseteq> carrier (add_monoid R)"
+ using assms subgroup.subset[OF additive_subgroup.a_subgroup]
+ unfolding pred_on.chain_def ideal_def by auto
+
+ obtain I where I: "I \<in> C" "ideal I R"
+ using False assms unfolding pred_on.chain_def by auto
+ thus "\<one>\<^bsub>add_monoid R\<^esub> \<in> \<Union>C"
+ using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF I(2)]] by auto
+ next
+ fix x y assume "x \<in> \<Union>C" "y \<in> \<Union>C"
+ then obtain I where I: "I \<in> C" "x \<in> I" "y \<in> I"
+ using assms unfolding pred_on.chain_def by blast
+ hence ideal: "ideal I R"
+ using assms unfolding pred_on.chain_def by auto
+ thus "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> \<Union>C"
+ using UnionI I additive_subgroup.a_closed unfolding ideal_def by fastforce
+
+ show "inv\<^bsub>add_monoid R\<^esub> x \<in> \<Union>C"
+ using UnionI I additive_subgroup.a_inv_closed ideal unfolding ideal_def a_inv_def by metis
+ qed
next
- fix x a assume x: "x \<in> carrier R" and a: "a \<in> (\<Union>i. I i)"
- then obtain i where i: "a \<in> I i" by blast
- hence "x \<otimes> a \<in> I i" and "a \<otimes> x \<in> I i"
- by (simp_all add: assms(1) ideal.I_l_closed ideal.I_r_closed x)
- thus "x \<otimes> a \<in> (\<Union>i. I i)"
- and "a \<otimes> x \<in> (\<Union>i. I i)" by blast+
+ fix a x assume a: "a \<in> \<Union>C" and x: "x \<in> carrier R"
+ then obtain I where I: "ideal I R" "a \<in> I" and "I \<in> C"
+ using assms unfolding pred_on.chain_def by auto
+ thus "x \<otimes> a \<in> \<Union>C" and "a \<otimes> x \<in> \<Union>C"
+ using ideal.I_l_closed[OF I x] ideal.I_r_closed[OF I x] by auto
qed
-
- then obtain S where S: "S \<subseteq> carrier R" "finite S" "(\<Union>i. I i) = Idl S"
- by (meson finetely_gen)
- hence "S \<subseteq> (\<Union>i. I i)"
- by (simp add: genideal_self)
-
- 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
- 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)
- thus ?case by blast
- qed
- then obtain n where "S \<subseteq> I n" by blast
- hence "I n = (\<Union>i. I i)"
- by (metis S(3) Sup_upper assms(1) genideal_minimal range_eqI subset_antisym)
thus ?thesis
- by (metis (full_types) Sup_upper assms(2) range_eqI subset_antisym)
+ using False by simp
qed
-lemma increasing_set_seq_iff:
- "(\<And>i. I i \<subseteq> I (Suc i)) == (\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j)"
-proof
- fix i j :: "nat"
- assume A: "\<And>i. I i \<subseteq> I (Suc i)" and "i \<le> j"
- then obtain k where k: "j = i + k"
- using le_Suc_ex by blast
- have "I i \<subseteq> I (i + k)"
- by (induction k) (simp_all add: A lift_Suc_mono_le)
- thus "I i \<subseteq> I j" using k by simp
-next
- fix i assume "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
- thus "I i \<subseteq> I (Suc i)" by simp
-qed
-
-
-text \<open>Helper definition for the proofs below\<close>
-fun S_builder :: "_ \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set" where
- "S_builder R J 0 = {}" |
- "S_builder R J (Suc n) =
- (let diff = (J - Idl\<^bsub>R\<^esub> (S_builder R J n)) in
- (if diff \<noteq> {} then insert (SOME x. x \<in> diff) (S_builder R J n) else (S_builder R J n)))"
-
-lemma S_builder_incl: "S_builder R J n \<subseteq> J"
- by (induction n) (simp_all, (metis (no_types, lifting) some_eq_ex subsetI))
-
-lemma (in ring) S_builder_const1:
- assumes "ideal J R" "S_builder R J (Suc n) = S_builder R J n"
- shows "J = Idl (S_builder R J n)"
+lemma (in noetherian_ring) ideal_chain_is_trivial:
+ assumes "C \<noteq> {}" "subset.chain { I. ideal I R } C"
+ shows "\<Union>C \<in> C"
proof -
- have "J - Idl (S_builder R J n) = {}"
- proof (rule ccontr)
- assume "J - Idl (S_builder R J n) \<noteq> {}"
- hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)"
- by simp
- moreover have "(S_builder R J n) \<subseteq> Idl (S_builder R J n)"
- using S_builder_incl assms(1)
- by (metis additive_subgroup.a_subset dual_order.trans genideal_self ideal.axioms(1))
- ultimately have "S_builder R J (Suc n) \<noteq> S_builder R J n"
- by (metis Diff_iff \<open>J - Idl S_builder R J n \<noteq> {}\<close> insert_subset some_in_eq)
- thus False using assms(2) by simp
- qed
- thus "J = Idl (S_builder R J n)"
- by (meson S_builder_incl[of R J n] Diff_eq_empty_iff assms(1) genideal_minimal subset_antisym)
-qed
+ { fix S assume "finite S" "S \<subseteq> \<Union>C"
+ hence "\<exists>I. I \<in> C \<and> S \<subseteq> I"
+ proof (induct S)
+ case empty thus ?case
+ using assms(1) by blast
+ next
+ case (insert s S)
+ then obtain I where I: "I \<in> C" "S \<subseteq> I"
+ by blast
+ moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
+ using insert(4) by blast
+ ultimately have "I \<subseteq> I' \<or> I' \<subseteq> I"
+ using assms unfolding pred_on.chain_def by blast
+ thus ?case
+ using I I' by blast
+ qed } note aux_lemma = this
-lemma (in ring) S_builder_const2:
- assumes "ideal J R" "Idl (S_builder R J (Suc n)) = Idl (S_builder R J n)"
- shows "S_builder R J (Suc n) = S_builder R J n"
-proof (rule ccontr)
- assume "S_builder R J (Suc n) \<noteq> S_builder R J n"
- hence A: "J - Idl (S_builder R J n) \<noteq> {}" by auto
- hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)" by simp
- then obtain x where x: "x \<in> (J - Idl (S_builder R J n))"
- and S: "S_builder R J (Suc n) = insert x (S_builder R J n)"
- using A some_in_eq by blast
- have "x \<notin> Idl (S_builder R J n)" using x by blast
- moreover have "x \<in> Idl (S_builder R J (Suc n))"
- by (metis (full_types) S S_builder_incl additive_subgroup.a_subset
- assms(1) dual_order.trans genideal_self ideal.axioms(1) insert_subset)
- ultimately show False using assms(2) by blast
+ obtain S where S: "finite S" "S \<subseteq> carrier R" "\<Union>C = Idl S"
+ using finetely_gen[OF chain_Union_is_ideal[OF assms(2)]] assms(1) by auto
+ then obtain I where I: "I \<in> C" and "S \<subseteq> I"
+ using aux_lemma[OF S(1)] genideal_self[OF S(2)] by blast
+ hence "Idl S \<subseteq> I"
+ using assms unfolding pred_on.chain_def
+ by (metis genideal_minimal mem_Collect_eq rev_subsetD)
+ hence "\<Union>C = I"
+ using S(3) I by auto
+ thus ?thesis
+ using I by simp
qed
-lemma (in ring) trivial_ideal_seq_imp_noetherian:
- assumes "\<And>I. \<lbrakk> \<And>i :: nat. ideal (I i) R; \<And>i j. i \<le> j \<Longrightarrow> (I i) \<subseteq> (I j) \<rbrakk> \<Longrightarrow>
- (\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n)"
+lemma (in ring) trivial_ideal_chain_imp_noetherian:
+ assumes "\<And>C. \<lbrakk> C \<noteq> {}; subset.chain { I. ideal I R } C \<rbrakk> \<Longrightarrow> \<Union>C \<in> C"
shows "noetherian_ring R"
-proof -
- have "\<And>J. ideal J R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
- proof -
- fix J assume J: "ideal J R"
- define S and I where "S = (\<lambda>i. S_builder R J i)" and "I = (\<lambda>i. Idl (S i))"
- hence "\<And>i. ideal (I i) R"
- by (meson J S_builder_incl additive_subgroup.a_subset genideal_ideal ideal.axioms(1) subset_trans)
- moreover have "\<And>n. S n \<subseteq> S (Suc n)" using S_def by auto
- hence "\<And>n. I n \<subseteq> I (Suc n)"
- 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)
- 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)
- moreover have "finite (S_builder R J n)" by (induction n) (simp_all)
- ultimately show "\<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
- by (meson J S_builder_incl ideal.Icarr set_rev_mp subsetI)
+proof (auto simp add: noetherian_ring_def noetherian_ring_axioms_def ring_axioms)
+ fix I assume I: "ideal I R"
+ have in_carrier: "I \<subseteq> carrier R" and add_subgroup: "additive_subgroup I R"
+ using ideal.axioms(1)[OF I] additive_subgroup.a_subset by auto
+
+ define S where "S = { Idl S' | S'. S' \<subseteq> I \<and> finite S' }"
+ have "\<exists>M \<in> S. \<forall>S' \<in> S. M \<subseteq> S' \<longrightarrow> S' = M"
+ proof (rule subset_Zorn)
+ fix C assume C: "subset.chain S C"
+ show "\<exists>U \<in> S. \<forall>S' \<in> C. S' \<subseteq> U"
+ proof (cases "C = {}")
+ case True
+ have "{ \<zero> } \<in> S"
+ using additive_subgroup.zero_closed[OF add_subgroup] genideal_zero
+ by (auto simp add: S_def)
+ thus ?thesis
+ using True by auto
+ next
+ case False
+ have "S \<subseteq> { I. ideal I R }"
+ using additive_subgroup.a_subset[OF add_subgroup] genideal_ideal
+ by (auto simp add: S_def)
+ hence "subset.chain { I. ideal I R } C"
+ using C unfolding pred_on.chain_def by auto
+ then have "\<Union>C \<in> C"
+ using assms False by simp
+ thus ?thesis
+ by (meson C Union_upper pred_on.chain_def subsetCE)
+ qed
qed
- thus ?thesis
- by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
+ then obtain M where M: "M \<in> S" "\<And>S'. \<lbrakk>S' \<in> S; M \<subseteq> S' \<rbrakk> \<Longrightarrow> S' = M"
+ by auto
+ then obtain S' where S': "S' \<subseteq> I" "finite S'" "M = Idl S'"
+ by (auto simp add: S_def)
+ hence "M \<subseteq> I"
+ using I genideal_minimal by (auto simp add: S_def)
+ moreover have "I \<subseteq> M"
+ proof (rule ccontr)
+ assume "\<not> I \<subseteq> M"
+ then obtain a where a: "a \<in> I" "a \<notin> M"
+ by auto
+ have "M \<subseteq> Idl (insert a S')"
+ using S' a(1) genideal_minimal[of "Idl (insert a S')" S']
+ in_carrier genideal_ideal genideal_self
+ by (meson insert_subset subset_trans)
+ moreover have "Idl (insert a S') \<in> S"
+ using a(1) S' by (auto simp add: S_def)
+ ultimately have "M = Idl (insert a S')"
+ using M(2) by auto
+ hence "a \<in> M"
+ using genideal_self S'(1) a (1) in_carrier by (meson insert_subset subset_trans)
+ from \<open>a \<in> M\<close> and \<open>a \<notin> M\<close> show False by simp
+ qed
+ ultimately have "M = I" by simp
+ thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A"
+ using S' in_carrier by blast
qed
-lemma (in noetherian_domain) wfactors_exists:
- assumes "x \<in> carrier (mult_of R)"
- shows "\<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs x" (is "?P x")
+lemma (in noetherian_domain) factorization_property:
+ assumes "a \<in> carrier R - { \<zero> }" "a \<notin> Units R"
+ shows "\<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs a" (is "?factorizable a")
proof (rule ccontr)
- { fix x
- assume A: "x \<in> carrier (mult_of R)" "\<not> ?P x"
- have "\<exists>a. a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a"
- proof -
- 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
- thus False using A by auto
- qed
- moreover have "\<not> x \<in> Units (mult_of R)"
- using A monoid.unit_wfactors[OF mult_of.monoid_axioms, of x] by auto
- ultimately
- obtain a where a: "a \<in> carrier (mult_of R)" "properfactor (mult_of R) a x" "a \<notin> Units (mult_of R)"
- unfolding irreducible_def by blast
- then obtain b where b: "b \<in> carrier (mult_of R)" "x = a \<otimes> b"
- unfolding properfactor_def by auto
- hence b_properfactor: "properfactor (mult_of R) b x"
- using A a mult_of.m_comm mult_of.properfactorI3 by blast
- have "\<not> ?P a \<or> \<not> ?P b"
- proof (rule ccontr)
- assume "\<not> (\<not> ?P a \<or> \<not> ?P b)"
- then obtain fs_a fs_b
- where fs_a: "wfactors (mult_of R) fs_a a" "set fs_a \<subseteq> carrier (mult_of R)"
- and fs_b: "wfactors (mult_of R) fs_b b" "set fs_b \<subseteq> carrier (mult_of R)" by blast
- hence "wfactors (mult_of R) (fs_a @ fs_b) x"
- 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
- 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"
- where "f = (\<lambda>a x. (a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a))"
- define factor_seq :: "nat \<Rightarrow> 'a"
- 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>
- (factor_seq n) \<in> carrier (mult_of R) \<and> \<not> ?P (factor_seq n)" (is "\<And>n. ?Q n")
+ assume a: "\<not> ?factorizable a"
+ define S where "S = { PIdl r | r. r \<in> carrier R - { \<zero> } \<and> r \<notin> Units R \<and> \<not> ?factorizable r }"
+ then obtain C where C: "subset.maxchain S C"
+ using subset.Hausdorff by blast
+ hence chain: "subset.chain S C"
+ using pred_on.maxchain_def by blast
+ moreover have "S \<subseteq> { I. ideal I R }"
+ using cgenideal_ideal by (auto simp add: S_def)
+ ultimately have "subset.chain { I. ideal I R } C"
+ by (meson dual_order.trans pred_on.chain_def)
+ moreover have "PIdl a \<in> S"
+ using assms a by (auto simp add: S_def)
+ hence "subset.chain S { PIdl a }"
+ unfolding pred_on.chain_def by auto
+ hence "C \<noteq> {}"
+ using C unfolding pred_on.maxchain_def by auto
+ ultimately have "\<Union>C \<in> C"
+ using ideal_chain_is_trivial by simp
+ hence "\<Union>C \<in> S"
+ using chain unfolding pred_on.chain_def by auto
+ then obtain r where r: "\<Union>C = PIdl r" "r \<in> carrier R - { \<zero> }" "r \<notin> Units R" "\<not> ?factorizable r"
+ by (auto simp add: S_def)
+ have "\<exists>p. p \<in> carrier R - { \<zero> } \<and> p \<notin> Units R \<and> \<not> ?factorizable p \<and> p divides r \<and> \<not> r divides p"
proof -
- fix n show "?Q n"
- proof (induct n)
- case 0
- have x: "factor_seq 0 = x"
- using factor_seq_def by simp
- hence "factor_seq (Suc 0) = (SOME a. f a x)"
- by (simp add: factor_seq_def)
- moreover have "\<exists>a. f a x"
- using aux_lemma[OF assms] A f_def by blast
- ultimately have "f (factor_seq (Suc 0)) x"
- using tfl_some by metis
- thus ?case using f_def A assms x by simp
- next
- case (Suc n)
- have "factor_seq (Suc n) = (SOME a. f a (factor_seq n))"
- by (simp add: factor_seq_def)
- moreover have "\<exists>a. f a (factor_seq n)"
- using aux_lemma f_def Suc.hyps by blast
- ultimately have Step0: "f (factor_seq (Suc n)) (factor_seq n)"
- using tfl_some by metis
- hence "\<exists>a. f a (factor_seq (Suc n))"
- using aux_lemma f_def by blast
- moreover have "factor_seq (Suc (Suc n)) = (SOME a. f a (factor_seq (Suc n)))"
- by (simp add: factor_seq_def)
- ultimately have Step1: "f (factor_seq (Suc (Suc n))) (factor_seq (Suc n))"
- using tfl_some by metis
- show ?case using Step0 Step1 f_def by simp
+ have "wfactors (mult_of R) [ r ] r" if "irreducible (mult_of R) r"
+ using r(2) that unfolding wfactors_def by auto
+ hence "\<not> irreducible (mult_of R) r"
+ using r(2,4) by auto
+ hence "\<not> ring_irreducible r"
+ using ring_irreducibleE(3) r(2) by auto
+ then obtain p1 p2
+ where p1_p2: "p1 \<in> carrier R" "p2 \<in> carrier R" "r = p1 \<otimes> p2" "p1 \<notin> Units R" "p2 \<notin> Units R"
+ using ring_irreducibleI[OF r(2-3)] by auto
+ hence in_carrier: "p1 \<in> carrier (mult_of R)" "p2 \<in> carrier (mult_of R)"
+ using r(2) by auto
+
+ have "\<lbrakk> ?factorizable p1; ?factorizable p2 \<rbrakk> \<Longrightarrow> ?factorizable r"
+ using mult_of.wfactors_mult[OF _ _ in_carrier] p1_p2(3) by (metis le_sup_iff set_append)
+ hence "\<not> ?factorizable p1 \<or> \<not> ?factorizable p2"
+ using r(4) by auto
+
+ moreover
+ have "\<And>p1 p2. \<lbrakk> p1 \<in> carrier R; p2 \<in> carrier R; r = p1 \<otimes> p2; r divides p1 \<rbrakk> \<Longrightarrow> p2 \<in> Units R"
+ proof -
+ fix p1 p2 assume A: "p1 \<in> carrier R" "p2 \<in> carrier R" "r = p1 \<otimes> p2" "r divides p1"
+ then obtain c where c: "c \<in> carrier R" "p1 = r \<otimes> c"
+ unfolding factor_def by blast
+ hence "\<one> = c \<otimes> p2"
+ using A m_lcancel[OF _ _ one_closed, of r "c \<otimes> p2"] r(2) by (auto, metis m_assoc m_closed)
+ thus "p2 \<in> Units R"
+ unfolding Units_def using c A(2) m_comm[OF c(1) A(2)] by auto
qed
- qed
-
- have in_carrier: "\<And>i. factor_seq i \<in> carrier R"
- using factor_seq_props by simp
- hence "\<And>i. ideal (I i) R"
- using I_def by (simp add: cgenideal_ideal)
+ hence "\<not> r divides p1" and "\<not> r divides p2"
+ using p1_p2 m_comm[OF p1_p2(1-2)] by blast+
- moreover
- have "\<And>i. factor_seq (Suc i) divides factor_seq i"
- using factor_seq_props unfolding properfactor_def by auto
- hence "\<And>i. PIdl (factor_seq i) \<subseteq> PIdl (factor_seq (Suc i))"
- using in_carrier to_contain_is_to_divide by simp
- hence "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
- using increasing_set_seq_iff[of I] unfolding I_def by auto
-
- ultimately obtain n where "\<And>k. n \<le> k \<Longrightarrow> I n = I k"
- by (metis trivial_ideal_seq)
- hence "I (Suc n) \<subseteq> I n" by (simp add: equalityD2)
- hence "factor_seq n divides factor_seq (Suc n)"
- using in_carrier I_def to_contain_is_to_divide by simp
- moreover have "\<not> factor_seq n divides\<^bsub>(mult_of R)\<^esub> factor_seq (Suc n)"
- using factor_seq_props[of n] unfolding properfactor_def by simp
- hence "\<not> factor_seq n divides factor_seq (Suc n)"
- using divides_imp_divides_mult[of "factor_seq n" "factor_seq (Suc n)"]
- in_carrier[of n] factor_seq_props[of "Suc n"] by auto
- ultimately show False by simp
+ ultimately show ?thesis
+ using p1_p2 in_carrier by (metis carrier_mult_of dividesI' m_comm)
+ qed
+ then obtain p
+ where p: "p \<in> carrier R - { \<zero> }" "p \<notin> Units R" "\<not> ?factorizable p" "p divides r" "\<not> r divides p"
+ by blast
+ hence "PIdl p \<in> S"
+ unfolding S_def by auto
+ moreover have "\<Union>C \<subset> PIdl p"
+ using p r to_contain_is_to_divide unfolding r(1) by (metis Diff_iff psubsetI)
+ ultimately have "subset.chain S (insert (PIdl p) C)" and "C \<subset> (insert (PIdl p) C)"
+ unfolding pred_on.chain_def by (metis C psubsetE subset_maxchain_max, blast)
+ thus False
+ using C unfolding pred_on.maxchain_def by blast
qed
@@ -549,195 +669,154 @@
proof
fix I assume "ideal I R"
then obtain i where "i \<in> carrier R" "I = Idl { i }"
- using principal_I principalideal.generate by blast
- thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A" by blast
+ using exists_gen cgenideal_eq_genideal by auto
+ thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A"
+ by blast
qed
lemma (in principal_domain) irreducible_imp_maximalideal:
- assumes "p \<in> carrier (mult_of R)"
- and "irreducible (mult_of R) p"
+ assumes "p \<in> carrier R"
+ and "ring_irreducible p"
shows "maximalideal (PIdl p) R"
proof (rule maximalidealI)
show "ideal (PIdl p) R"
using assms(1) by (simp add: cgenideal_ideal)
next
show "carrier R \<noteq> PIdl p"
- proof (rule ccontr)
- assume "\<not> carrier R \<noteq> PIdl p"
- hence "carrier R = PIdl p" by simp
- then obtain c where "c \<in> carrier R" "\<one> = c \<otimes> p"
- unfolding cgenideal_def using one_closed by auto
- hence "p \<in> Units R"
- unfolding Units_def using assms(1) m_comm by auto
- thus False
- using assms unfolding irreducible_def by auto
- qed
+ using ideal_eq_carrier_iff[OF assms(1)] ring_irreducibleE(4)[OF assms] by auto
next
fix J assume J: "ideal J R" "PIdl p \<subseteq> J" "J \<subseteq> carrier R"
then obtain q where q: "q \<in> carrier R" "J = PIdl q"
- using principal_I[OF J(1)] cgenideal_eq_rcos is_cring
- principalideal.rcos_generate by (metis contra_subsetD)
+ using exists_gen[OF J(1)] cgenideal_eq_rcos by metis
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>)
- 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))
+ then obtain r where r: "r \<in> carrier R" "p = q \<otimes> r"
+ unfolding factor_def by auto
+ hence "q \<in> Units R \<or> r \<in> Units R"
+ using ring_irreducibleE(5)[OF assms q(1)] by auto
+ thus "J = PIdl p \<or> J = carrier R"
+ proof
+ assume "q \<in> Units R" thus ?thesis
+ using ideal_eq_carrier_iff[OF q(1)] q(2) by auto
next
- case False
- have q_in_carr: "q \<in> carrier (mult_of R)"
- using q_div_p unfolding factor_def using assms(1) q(1) by auto
- hence "p divides\<^bsub>(mult_of R)\<^esub> q"
- using q_div_p False assms(2) unfolding irreducible_def properfactor_def by auto
- hence "p \<sim> q" using q_div_p
- unfolding associated_def by simp
- thus ?thesis using associated_iff_same_ideal[of p q] assms(1) q_in_carr q by simp
+ assume "r \<in> Units R" hence "p \<sim> q"
+ using assms(1) r q(1) associatedI2' by blast
+ thus ?thesis
+ unfolding associated_iff_same_ideal[OF assms(1) q(1)] q(2) by auto
qed
qed
corollary (in principal_domain) primeness_condition:
- assumes "p \<in> carrier (mult_of R)"
- shows "(irreducible (mult_of R) p) \<longleftrightarrow> (prime (mult_of R) p)"
+ assumes "p \<in> carrier R"
+ shows "ring_irreducible p \<longleftrightarrow> ring_prime p"
proof
- show "irreducible (mult_of R) p \<Longrightarrow> prime (mult_of R) p"
- using irreducible_imp_maximalideal maximalideal_prime primeideal_iff_prime assms by auto
+ show "ring_irreducible p \<Longrightarrow> ring_prime p"
+ using maximalideal_prime[OF irreducible_imp_maximalideal] ring_irreducibleE(1)
+ primeideal_iff_prime assms by auto
next
- show "prime (mult_of R) p \<Longrightarrow> irreducible (mult_of R) p"
- using mult_of.prime_irreducible by simp
+ show "ring_prime p \<Longrightarrow> ring_irreducible p"
+ using mult_of.prime_irreducible ring_primeI[of p] ring_irreducibleI' assms
+ unfolding ring_prime_def prime_eq_prime_mult[OF assms] by auto
qed
lemma (in principal_domain) domain_iff_prime:
assumes "a \<in> carrier R - { \<zero> }"
- shows "domain (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+ shows "domain (R Quot (PIdl a)) \<longleftrightarrow> ring_prime a"
using quot_domain_iff_primeideal[of "PIdl a"] primeideal_iff_prime[of a]
cgenideal_ideal[of a] assms by auto
lemma (in principal_domain) field_iff_prime:
assumes "a \<in> carrier R - { \<zero> }"
- shows "field (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+ shows "field (R Quot (PIdl a)) \<longleftrightarrow> ring_prime a"
proof
- show "prime (mult_of R) a \<Longrightarrow> field (R Quot (PIdl a))"
+ show "ring_prime a \<Longrightarrow> field (R Quot (PIdl a))"
using primeness_condition[of a] irreducible_imp_maximalideal[of a]
maximalideal.quotient_is_field[of "PIdl a" R] is_cring assms by auto
next
- show "field (R Quot (PIdl a)) \<Longrightarrow> prime (mult_of R) a"
+ show "field (R Quot (PIdl a)) \<Longrightarrow> ring_prime a"
unfolding field_def using domain_iff_prime[of a] assms by auto
qed
-sublocale principal_domain < mult_of: primeness_condition_monoid "(mult_of R)"
+
+sublocale principal_domain < mult_of: primeness_condition_monoid "mult_of R"
rewrites "mult (mult_of R) = mult R"
and "one (mult_of R) = one R"
- unfolding primeness_condition_monoid_def
- primeness_condition_monoid_axioms_def
- using mult_of.is_comm_monoid_cancel primeness_condition by auto
+ unfolding primeness_condition_monoid_def
+ primeness_condition_monoid_axioms_def
+proof (auto simp add: mult_of.is_comm_monoid_cancel)
+ fix a assume a: "a \<in> carrier R" "a \<noteq> \<zero>" "irreducible (mult_of R) a"
+ show "prime (mult_of R) a"
+ using primeness_condition[OF a(1)] irreducible_mult_imp_irreducible[OF _ a(3)] a(1-2)
+ unfolding ring_prime_def ring_irreducible_def prime_eq_prime_mult[OF a(1)] by auto
+qed
-sublocale principal_domain < mult_of: factorial_monoid "(mult_of R)"
+sublocale principal_domain < mult_of: factorial_monoid "mult_of R"
rewrites "mult (mult_of R) = mult R"
and "one (mult_of R) = one R"
- apply (rule mult_of.factorial_monoidI)
- using mult_of.wfactors_unique wfactors_exists mult_of.is_comm_monoid_cancel by auto
+ using mult_of.wfactors_unique factorization_property mult_of.is_comm_monoid_cancel
+ by (auto intro!: mult_of.factorial_monoidI)
sublocale principal_domain \<subseteq> factorial_domain
- unfolding factorial_domain_def using is_domain mult_of.is_factorial_monoid by simp
+ unfolding factorial_domain_def using domain_axioms mult_of.factorial_monoid_axioms by simp
lemma (in principal_domain) ideal_sum_iff_gcd:
- assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)" "d \<in> carrier (mult_of R)"
- shows "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)) \<longleftrightarrow> (d gcdof\<^bsub>(mult_of R)\<^esub> a b)"
-proof
- assume A: "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)" show "d gcdof\<^bsub>(mult_of R)\<^esub> a b"
- proof -
- have "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
- using assms
- by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal local.ring_axioms
- ring.genideal_self ring.oneideal ring.union_genideal A)
- hence "d divides a \<and> d divides b"
- using assms apply simp
- using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] by auto
- hence "d divides\<^bsub>(mult_of R)\<^esub> a \<and> d divides\<^bsub>(mult_of R)\<^esub> b"
- using assms by simp
+ assumes "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+ shows "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<longleftrightarrow> d gcdof a b"
+proof -
+ { fix a b d
+ assume in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+ and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+ have "d gcdof a b"
+ proof (auto simp add: isgcd_def)
+ have "a \<in> PIdl d" and "b \<in> PIdl d"
+ using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
+ in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
+ unfolding ideal_eq set_add_def' by force+
+ thus "d divides a" and "d divides b"
+ using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
+ cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
+ next
+ fix c assume c: "c \<in> carrier R" "c divides a" "c divides b"
+ hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
+ using to_contain_is_to_divide in_carrier by auto
+ hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl c"
+ by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
+ thus "c divides d"
+ using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
+ qed } note aux_lemma = this
- moreover
- have "\<And>c. \<lbrakk> c \<in> carrier (mult_of R); c divides\<^bsub>(mult_of R)\<^esub> a; c divides\<^bsub>(mult_of R)\<^esub> b \<rbrakk> \<Longrightarrow>
- c divides\<^bsub>(mult_of R)\<^esub> d"
- proof -
- fix c assume c: "c \<in> carrier (mult_of R)"
- and "c divides\<^bsub>(mult_of R)\<^esub> a" "c divides\<^bsub>(mult_of R)\<^esub> b"
- hence "c divides a" "c divides b" by auto
- hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)"
- using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] c assms by simp
- hence "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) \<subseteq> (PIdl c)"
- using assms c
- by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
- Idl_subset_ideal oneideal union_genideal)
- hence incl: "(PIdl d) \<subseteq> (PIdl c)" using A by simp
- hence "c divides d"
- using c assms(3) apply simp
- using to_contain_is_to_divide[of c d] by blast
- thus "c divides\<^bsub>(mult_of R)\<^esub> d" using c assms(3) by simp
- qed
+ have "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<Longrightarrow> d gcdof a b"
+ using aux_lemma assms by simp
- ultimately show ?thesis unfolding isgcd_def by simp
+ moreover
+ have "d gcdof a b \<Longrightarrow> PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+ proof -
+ assume d: "d gcdof a b"
+ obtain c where c: "c \<in> carrier R" "PIdl c = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+ using exists_gen[OF add_ideals[OF assms(1-2)[THEN cgenideal_ideal]]] by blast
+ hence "c gcdof a b"
+ using aux_lemma assms by simp
+ from \<open>d gcdof a b\<close> and \<open>c gcdof a b\<close> have "d \<sim> c"
+ using assms c(1) by (simp add: associated_def isgcd_def)
+ thus ?thesis
+ using c(2) associated_iff_same_ideal[OF assms(3) c(1)] by simp
qed
-next
- assume A:"d gcdof\<^bsub>mult_of R\<^esub> a b" show "PIdl a <+>\<^bsub>R\<^esub> PIdl b = PIdl d"
- proof
- have "d divides a" "d divides b"
- using A unfolding isgcd_def by auto
- hence "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
- using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] assms by simp
- thus "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl d" using assms
- by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
- Idl_subset_ideal oneideal union_genideal)
- next
- have "ideal ((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) R"
- using assms by (simp add: cgenideal_ideal local.ring_axioms ring.add_ideals)
- then obtain c where c: "c \<in> carrier R" "(PIdl c) = (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
- using cgenideal_eq_genideal principal_I principalideal.generate by force
- hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)" using assms
- by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
- genideal_self oneideal union_genideal)
- hence "c divides a \<and> c divides b" using c(1) assms apply simp
- using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] by blast
- hence "c divides\<^bsub>(mult_of R)\<^esub> a \<and> c divides\<^bsub>(mult_of R)\<^esub> b"
- using assms(1-2) c(1) by simp
- moreover have neq_zero: "c \<noteq> \<zero>"
- proof (rule ccontr)
- assume "\<not> c \<noteq> \<zero>" hence "PIdl c = { \<zero> }"
- using cgenideal_eq_genideal genideal_zero by auto
- moreover have "\<one> \<otimes> a \<in> PIdl a \<and> \<zero> \<otimes> b \<in> PIdl b"
- unfolding cgenideal_def using assms one_closed zero_closed by blast
- hence "(\<one> \<otimes> a) \<oplus> (\<zero> \<otimes> b) \<in> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
- unfolding set_add_def' by auto
- hence "a \<in> PIdl c"
- using c assms by simp
- ultimately show False
- using assms(1) by simp
- qed
-
- ultimately have "c divides\<^bsub>(mult_of R)\<^esub> d"
- using A c(1) unfolding isgcd_def by simp
- hence "(PIdl d) \<subseteq> (PIdl c)"
- using to_contain_is_to_divide[of c d] c(1) assms(3) by simp
- thus "PIdl d \<subseteq> PIdl a <+>\<^bsub>R\<^esub> PIdl b" using c by simp
- qed
+ ultimately show ?thesis by auto
qed
lemma (in principal_domain) bezout_identity:
- assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)"
- shows "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl (somegcd (mult_of R) a b))"
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "PIdl a <+>\<^bsub>R\<^esub> PIdl b = PIdl (somegcd R a b)"
proof -
- have "(somegcd (mult_of R) a b) \<in> carrier (mult_of R)"
- using mult_of.gcd_exists[OF assms] by simp
- hence "\<And>x. x = somegcd (mult_of R) a b \<Longrightarrow> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl x)"
- using mult_of.gcd_isgcd[OF assms] ideal_sum_iff_gcd[OF assms] by simp
+ have "\<exists>d \<in> carrier R. d gcdof a b"
+ using exists_gen[OF add_ideals[OF assms(1-2)[THEN cgenideal_ideal]]]
+ ideal_sum_iff_gcd[OF assms(1-2)] by auto
thus ?thesis
- using mult_of.gcd_exists[OF assms] by blast
+ using ideal_sum_iff_gcd[OF assms(1-2)] somegcd_def
+ by (metis (no_types, lifting) tfl_some)
qed
-
subsection \<open>Euclidean Domains\<close>
sublocale euclidean_domain \<subseteq> principal_domain
@@ -745,7 +824,7 @@
proof (auto)
show "domain R" by (simp add: domain_axioms)
next
- fix I assume I: "ideal I R" show "principalideal I R"
+ fix I assume I: "ideal I R" have "principalideal I R"
proof (cases "I = { \<zero> }")
case True thus ?thesis by (simp add: zeropideal)
next
@@ -786,12 +865,16 @@
thus ?thesis
by (meson DiffD1 I cgenideal_is_principalideal ideal.Icarr local.a(1))
qed
+ thus "\<exists>a \<in> carrier R. I = PIdl a"
+ by (simp add: cgenideal_eq_genideal principalideal.generate)
qed
+
sublocale field \<subseteq> euclidean_domain R "\<lambda>_. 0"
proof (rule euclidean_domainI)
fix a b
let ?eucl_div = "\<lambda>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = b \<otimes> q \<oplus> r \<and> (r = \<zero> \<or> 0 < 0)"
+
assume a: "a \<in> carrier R - { \<zero> }" and b: "b \<in> carrier R - { \<zero> }"
hence "a = b \<otimes> ((inv b) \<otimes> a) \<oplus> \<zero>"
by (metis DiffD1 Units_inv_closed Units_r_inv field_Units l_one m_assoc r_zero)
@@ -801,4 +884,4 @@
by blast
qed
-end
+end
\ No newline at end of file