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

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

Mon, 18 Jun 2018 22:20:55 +0100 | |

changeset 68466 | 3ead36cbe6b7 |

parent 68463 | 410818a69ee3 |

child 68468 | ae42b0f6885d |

De-applied Ideal.thy

--- a/src/HOL/Algebra/Ideal.thy Mon Jun 18 11:15:46 2018 +0200 +++ b/src/HOL/Algebra/Ideal.thy Mon Jun 18 22:20:55 2018 +0100 @@ -38,12 +38,8 @@ shows "ideal I R" proof - interpret ring R by fact - show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI) - apply (rule a_subgroup) - apply (rule is_ring) - apply (erule (1) I_l_closed) - apply (erule (1) I_r_closed) - done + show ?thesis + by (auto simp: ideal.intro ideal_axioms.intro additive_subgroupI a_subgroup is_ring I_l_closed I_r_closed) qed @@ -132,14 +128,11 @@ proof - interpret additive_subgroup I R by fact interpret cring R by fact - show ?thesis apply (intro_locales) + show ?thesis apply intro_locales apply (intro ideal_axioms.intro) apply (erule (1) I_l_closed) apply (erule (1) I_r_closed) - apply (intro primeideal_axioms.intro) - apply (rule I_notcarr) - apply (erule (2) I_prime) - done + by (simp add: I_notcarr I_prime primeideal_axioms.intro) qed @@ -165,14 +158,11 @@ lemma (in ideal) one_imp_carrier: assumes I_one_closed: "\<one> \<in> I" shows "I = carrier R" - apply (rule) - apply (rule) - apply (rule a_Hcarr, simp) proof - fix x - assume xcarr: "x \<in> carrier R" - with I_one_closed have "x \<otimes> \<one> \<in> I" by (intro I_l_closed) - with xcarr show "x \<in> I" by simp + show "carrier R \<subseteq> I" + using I_r_closed assms by fastforce + show "I \<subseteq> carrier R" + by (rule a_subset) qed lemma (in ideal) Icarr: @@ -193,143 +183,82 @@ proof - interpret ideal I R by fact interpret ideal J R by fact + have IJ: "I \<inter> J \<subseteq> carrier R" + by (force simp: a_subset) show ?thesis apply (intro idealI subgroup.intro) - apply (rule is_ring) - apply (force simp add: a_subset) - apply (simp add: a_inv_def[symmetric]) - apply simp - apply (simp add: a_inv_def[symmetric]) - apply (clarsimp, rule) - apply (fast intro: ideal.I_l_closed ideal.intro assms)+ - apply (clarsimp, rule) - apply (fast intro: ideal.I_r_closed ideal.intro assms)+ + apply (simp_all add: IJ is_ring I_l_closed assms ideal.I_l_closed ideal.I_r_closed flip: a_inv_def) done qed -text \<open>The intersection of any Number of Ideals is again - an Ideal in @{term R}\<close> -lemma (in ring) i_Intersect: - assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" - and notempty: "S \<noteq> {}" - shows "ideal (\<Inter>S) R" - apply (unfold_locales) - apply (simp_all add: Inter_eq) - apply rule unfolding mem_Collect_eq defer 1 - apply rule defer 1 - apply rule defer 1 - apply (fold a_inv_def, rule) defer 1 - apply rule defer 1 - apply rule defer 1 -proof - - fix x y - assume "\<forall>I\<in>S. x \<in> I" - then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp - assume "\<forall>I\<in>S. y \<in> I" - then have yI: "\<And>I. I \<in> S \<Longrightarrow> y \<in> I" by simp - - fix J - assume JS: "J \<in> S" - interpret ideal J R by (rule Sideals[OF JS]) - from xI[OF JS] and yI[OF JS] show "x \<oplus> y \<in> J" by (rule a_closed) -next - fix J - assume JS: "J \<in> S" - interpret ideal J R by (rule Sideals[OF JS]) - show "\<zero> \<in> J" by simp -next - fix x - assume "\<forall>I\<in>S. x \<in> I" - then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp +text \<open>The intersection of any Number of Ideals is again an Ideal in @{term R}\<close> - fix J - assume JS: "J \<in> S" - interpret ideal J R by (rule Sideals[OF JS]) - - from xI[OF JS] show "\<ominus> x \<in> J" by (rule a_inv_closed) -next - fix x y - assume "\<forall>I\<in>S. x \<in> I" - then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp - assume ycarr: "y \<in> carrier R" - - fix J - assume JS: "J \<in> S" - interpret ideal J R by (rule Sideals[OF JS]) - - from xI[OF JS] and ycarr show "y \<otimes> x \<in> J" by (rule I_l_closed) -next - fix x y - assume "\<forall>I\<in>S. x \<in> I" - then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp - assume ycarr: "y \<in> carrier R" - - fix J - assume JS: "J \<in> S" - interpret ideal J R by (rule Sideals[OF JS]) - - from xI[OF JS] and ycarr show "x \<otimes> y \<in> J" by (rule I_r_closed) -next - fix x - assume "\<forall>I\<in>S. x \<in> I" - then have xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp - - from notempty have "\<exists>I0. I0 \<in> S" by blast - then obtain I0 where I0S: "I0 \<in> S" by auto - - interpret ideal I0 R by (rule Sideals[OF I0S]) - - from xI[OF I0S] have "x \<in> I0" . - with a_subset show "x \<in> carrier R" by fast -next - +lemma (in ring) i_Intersect: + assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}" + shows "ideal (\<Inter>S) R" +proof - + { fix x y J + assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S" + interpret ideal J R by (rule Sideals[OF JS]) + have "x \<oplus> y \<in> J" + by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) } + moreover + have "\<zero> \<in> J" if "J \<in> S" for J + by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1)) + moreover + { fix x J + assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S" + interpret ideal J R by (rule Sideals[OF JS]) + have "\<ominus> x \<in> J" + by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) } + moreover + { fix x y J + assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S" + interpret ideal J R by (rule Sideals[OF JS]) + have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" + using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ } + moreover + { fix x + assume "\<forall>I\<in>S. x \<in> I" + obtain I0 where I0S: "I0 \<in> S" + using notempty by blast + interpret ideal I0 R by (rule Sideals[OF I0S]) + have "x \<in> I0" + by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>) + with a_subset have "x \<in> carrier R" by fast } + ultimately show ?thesis + by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def) qed subsection \<open>Addition of Ideals\<close> lemma (in ring) add_ideals: - assumes idealI: "ideal I R" - and idealJ: "ideal J R" + assumes idealI: "ideal I R" and idealJ: "ideal J R" shows "ideal (I <+> J) R" - apply (rule ideal.intro) - apply (rule add_additive_subgroups) - apply (intro ideal.axioms[OF idealI]) - apply (intro ideal.axioms[OF idealJ]) - apply (rule is_ring) - apply (rule ideal_axioms.intro) - apply (simp add: set_add_defs, clarsimp) defer 1 - apply (simp add: set_add_defs, clarsimp) defer 1 -proof - - fix x i j - assume xcarr: "x \<in> carrier R" - and iI: "i \<in> I" - and jJ: "j \<in> J" - from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] - have c: "(i \<oplus> j) \<otimes> x = (i \<otimes> x) \<oplus> (j \<otimes> x)" - by algebra - from xcarr and iI have a: "i \<otimes> x \<in> I" - by (simp add: ideal.I_r_closed[OF idealI]) - from xcarr and jJ have b: "j \<otimes> x \<in> J" - by (simp add: ideal.I_r_closed[OF idealJ]) - from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. (i \<oplus> j) \<otimes> x = ha \<oplus> ka" - by fast -next - fix x i j - assume xcarr: "x \<in> carrier R" - and iI: "i \<in> I" - and jJ: "j \<in> J" - from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] - have c: "x \<otimes> (i \<oplus> j) = (x \<otimes> i) \<oplus> (x \<otimes> j)" by algebra - from xcarr and iI have a: "x \<otimes> i \<in> I" - by (simp add: ideal.I_l_closed[OF idealI]) - from xcarr and jJ have b: "x \<otimes> j \<in> J" - by (simp add: ideal.I_l_closed[OF idealJ]) - from a b c show "\<exists>ha\<in>I. \<exists>ka\<in>J. x \<otimes> (i \<oplus> j) = ha \<oplus> ka" - by fast +proof (rule ideal.intro) + show "additive_subgroup (I <+> J) R" + by (intro ideal.axioms[OF idealI] ideal.axioms[OF idealJ] add_additive_subgroups) + show "ring R" + by (rule is_ring) + show "ideal_axioms (I <+> J) R" + proof - + { fix x i j + assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" + from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] + have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k" + by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) } + moreover + { fix x i j + assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" + from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ] + have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k" + by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) } + ultimately show "ideal_axioms (I <+> J) R" + by (intro ideal_axioms.intro) (auto simp: set_add_defs) + qed qed - subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close> text \<open>@{term genideal} generates an ideal\<close> @@ -350,17 +279,13 @@ lemma (in ring) genideal_self': assumes carr: "i \<in> carrier R" shows "i \<in> Idl {i}" -proof - - from carr have "{i} \<subseteq> Idl {i}" by (fast intro!: genideal_self) - then show "i \<in> Idl {i}" by fast -qed + by (simp add: genideal_def) text \<open>@{term genideal} generates the minimal ideal\<close> lemma (in ring) genideal_minimal: - assumes a: "ideal I R" - and b: "S \<subseteq> I" + assumes "ideal I R" "S \<subseteq> I" shows "Idl S \<subseteq> I" - unfolding genideal_def by rule (elim InterD, simp add: a b) + unfolding genideal_def by rule (elim InterD, simp add: assms) text \<open>Generated ideals and subsets\<close> lemma (in ring) Idl_subset_ideal: @@ -383,40 +308,40 @@ and HI: "H \<subseteq> I" shows "Idl H \<subseteq> Idl I" proof - - from HI and genideal_self[OF Icarr] have HIdlI: "H \<subseteq> Idl I" - by fast - from Icarr have Iideal: "ideal (Idl I) R" by (rule genideal_ideal) from HI and Icarr have "H \<subseteq> carrier R" by fast with Iideal have "(H \<subseteq> Idl I) = (Idl H \<subseteq> Idl I)" by (rule Idl_subset_ideal[symmetric]) - - with HIdlI show "Idl H \<subseteq> Idl I" by simp + then show "Idl H \<subseteq> Idl I" + by (meson HI Icarr genideal_self order_trans) qed lemma (in ring) Idl_subset_ideal': assumes acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" - shows "(Idl {a} \<subseteq> Idl {b}) = (a \<in> Idl {b})" - apply (subst Idl_subset_ideal[OF genideal_ideal[of "{b}"], of "{a}"]) - apply (fast intro: bcarr, fast intro: acarr) - apply fast - done + shows "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> a \<in> Idl {b}" +proof - + have "Idl {a} \<subseteq> Idl {b} \<longleftrightarrow> {a} \<subseteq> Idl {b}" + by (simp add: Idl_subset_ideal acarr bcarr genideal_ideal) + also have "\<dots> \<longleftrightarrow> a \<in> Idl {b}" + by blast + finally show ?thesis . +qed lemma (in ring) genideal_zero: "Idl {\<zero>} = {\<zero>}" - apply rule - apply (rule genideal_minimal[OF zeroideal], simp) - apply (simp add: genideal_self') - done +proof + show "Idl {\<zero>} \<subseteq> {\<zero>}" + by (simp add: genideal_minimal zeroideal) + show "{\<zero>} \<subseteq> Idl {\<zero>}" + by (simp add: genideal_self') +qed lemma (in ring) genideal_one: "Idl {\<one>} = carrier R" proof - interpret ideal "Idl {\<one>}" "R" by (rule genideal_ideal) fast show "Idl {\<one>} = carrier R" - apply (rule, rule a_subset) - apply (simp add: one_imp_carrier genideal_self') - done + using genideal_self' one_imp_carrier by blast qed @@ -429,58 +354,24 @@ lemma (in cring) cgenideal_ideal: assumes acarr: "a \<in> carrier R" shows "ideal (PIdl a) R" - apply (unfold cgenideal_def) - apply (rule idealI[OF is_ring]) - apply (rule subgroup.intro) - apply simp_all - apply (blast intro: acarr) - apply clarsimp defer 1 - defer 1 - apply (fold a_inv_def, clarsimp) defer 1 - apply clarsimp defer 1 - apply clarsimp defer 1 -proof - - fix x y - assume xcarr: "x \<in> carrier R" - and ycarr: "y \<in> carrier R" - note carr = acarr xcarr ycarr - - from carr have "x \<otimes> a \<oplus> y \<otimes> a = (x \<oplus> y) \<otimes> a" - by (simp add: l_distr) - with carr show "\<exists>z. x \<otimes> a \<oplus> y \<otimes> a = z \<otimes> a \<and> z \<in> carrier R" - by fast -next - from l_null[OF acarr, symmetric] and zero_closed - show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" by fast -next - fix x - assume xcarr: "x \<in> carrier R" - note carr = acarr xcarr - - from carr have "\<ominus> (x \<otimes> a) = (\<ominus> x) \<otimes> a" - by (simp add: l_minus) - with carr show "\<exists>z. \<ominus> (x \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" - by fast -next - fix x y - assume xcarr: "x \<in> carrier R" - and ycarr: "y \<in> carrier R" - note carr = acarr xcarr ycarr - - from carr have "y \<otimes> a \<otimes> x = (y \<otimes> x) \<otimes> a" - by (simp add: m_assoc) (simp add: m_comm) - with carr show "\<exists>z. y \<otimes> a \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" - by fast -next - fix x y - assume xcarr: "x \<in> carrier R" - and ycarr: "y \<in> carrier R" - note carr = acarr xcarr ycarr - - from carr have "x \<otimes> (y \<otimes> a) = (x \<otimes> y) \<otimes> a" - by (simp add: m_assoc) - with carr show "\<exists>z. x \<otimes> (y \<otimes> a) = z \<otimes> a \<and> z \<in> carrier R" - by fast + unfolding cgenideal_def +proof (intro subgroup.intro idealI[OF is_ring], simp_all) + show "{x \<otimes> a |x. x \<in> carrier R} \<subseteq> carrier R" + by (blast intro: acarr) + show "\<And>x y. \<lbrakk>\<exists>u. x = u \<otimes> a \<and> u \<in> carrier R; \<exists>x. y = x \<otimes> a \<and> x \<in> carrier R\<rbrakk> + \<Longrightarrow> \<exists>v. x \<oplus> y = v \<otimes> a \<and> v \<in> carrier R" + by (metis assms cring.cring_simprules(1) is_cring l_distr) + show "\<exists>x. \<zero> = x \<otimes> a \<and> x \<in> carrier R" + by (metis assms l_null zero_closed) + show "\<And>x. \<exists>u. x = u \<otimes> a \<and> u \<in> carrier R + \<Longrightarrow> \<exists>v. inv\<^bsub>add_monoid R\<^esub> x = v \<otimes> a \<and> v \<in> carrier R" + by (metis a_inv_def add.inv_closed assms l_minus) + show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> + \<Longrightarrow> \<exists>z. x \<otimes> b = z \<otimes> a \<and> z \<in> carrier R" + by (metis assms m_assoc m_closed) + show "\<And>b x. \<lbrakk>\<exists>x. b = x \<otimes> a \<and> x \<in> carrier R; x \<in> carrier R\<rbrakk> + \<Longrightarrow> \<exists>z. b \<otimes> x = z \<otimes> a \<and> z \<in> carrier R" + by (metis assms m_assoc m_comm m_closed) qed lemma (in ring) cgenideal_self: @@ -504,119 +395,64 @@ interpret ideal J R by fact show ?thesis unfolding cgenideal_def - apply rule - apply clarify - using aJ - apply (erule I_l_closed) - done + using I_l_closed aJ by blast qed lemma (in cring) cgenideal_eq_genideal: assumes icarr: "i \<in> carrier R" shows "PIdl i = Idl {i}" - apply rule - apply (intro cgenideal_minimal) - apply (rule genideal_ideal, fast intro: icarr) - apply (rule genideal_self', fast intro: icarr) - apply (intro genideal_minimal) - apply (rule cgenideal_ideal [OF icarr]) - apply (simp, rule cgenideal_self [OF icarr]) - done +proof + show "PIdl i \<subseteq> Idl {i}" + by (simp add: cgenideal_minimal genideal_ideal genideal_self' icarr) + show "Idl {i} \<subseteq> PIdl i" + by (simp add: cgenideal_ideal cgenideal_self genideal_minimal icarr) +qed lemma (in cring) cgenideal_eq_rcos: "PIdl i = carrier R #> i" unfolding cgenideal_def r_coset_def by fast lemma (in cring) cgenideal_is_principalideal: - assumes icarr: "i \<in> carrier R" + assumes "i \<in> carrier R" shows "principalideal (PIdl i) R" - apply (rule principalidealI) - apply (rule cgenideal_ideal [OF icarr]) proof - - from icarr have "PIdl i = Idl {i}" - by (rule cgenideal_eq_genideal) - with icarr show "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" - by fast + have "\<exists>i'\<in>carrier R. PIdl i = Idl {i'}" + using cgenideal_eq_genideal assms by auto + then show ?thesis + by (simp add: cgenideal_ideal assms principalidealI) qed subsection \<open>Union of Ideals\<close> lemma (in ring) union_genideal: - assumes idealI: "ideal I R" - and idealJ: "ideal J R" + assumes idealI: "ideal I R" and idealJ: "ideal J R" shows "Idl (I \<union> J) = I <+> J" - apply rule - apply (rule ring.genideal_minimal) - apply (rule is_ring) - apply (rule add_ideals[OF idealI idealJ]) - apply (rule) - apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 - apply (rule) apply (simp add: set_add_defs genideal_def) apply clarsimp defer 1 -proof - - fix x - assume xI: "x \<in> I" - have ZJ: "\<zero> \<in> J" - by (intro additive_subgroup.zero_closed) (rule ideal.axioms[OF idealJ]) - from ideal.Icarr[OF idealI xI] have "x = x \<oplus> \<zero>" - by algebra - with xI and ZJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" - by fast +proof + show "Idl (I \<union> J) \<subseteq> I <+> J" + proof (rule ring.genideal_minimal [OF is_ring]) + show "ideal (I <+> J) R" + by (rule add_ideals[OF idealI idealJ]) + have "\<And>x. x \<in> I \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" + by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def local.idealI r_zero) + moreover have "\<And>x. x \<in> J \<Longrightarrow> \<exists>xa\<in>I. \<exists>xb\<in>J. x = xa \<oplus> xb" + by (metis additive_subgroup.zero_closed ideal.Icarr idealJ ideal_def l_zero local.idealI) + ultimately show "I \<union> J \<subseteq> I <+> J" + by (auto simp: set_add_defs) + qed next - fix x - assume xJ: "x \<in> J" - have ZI: "\<zero> \<in> I" - by (intro additive_subgroup.zero_closed, rule ideal.axioms[OF idealI]) - from ideal.Icarr[OF idealJ xJ] have "x = \<zero> \<oplus> x" - by algebra - with ZI and xJ show "\<exists>h\<in>I. \<exists>k\<in>J. x = h \<oplus> k" - by fast -next - fix i j K - assume iI: "i \<in> I" - and jJ: "j \<in> J" - and idealK: "ideal K R" - and IK: "I \<subseteq> K" - and JK: "J \<subseteq> K" - from iI and IK have iK: "i \<in> K" by fast - from jJ and JK have jK: "j \<in> K" by fast - from iK and jK show "i \<oplus> j \<in> K" - by (intro additive_subgroup.a_closed) (rule ideal.axioms[OF idealK]) + show "I <+> J \<subseteq> Idl (I \<union> J)" + by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp) qed - subsection \<open>Properties of Principal Ideals\<close> -text \<open>\<open>\<zero>\<close> generates the zero ideal\<close> -lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}" - apply rule - apply (simp add: genideal_minimal zeroideal) - apply (fast intro!: genideal_self) - done - -text \<open>\<open>\<one>\<close> generates the unit ideal\<close> -lemma (in ring) one_genideal: "Idl {\<one>} = carrier R" -proof - - have "\<one> \<in> Idl {\<one>}" - by (simp add: genideal_self') - then show "Idl {\<one>} = carrier R" - by (intro ideal.one_imp_carrier) (fast intro: genideal_ideal) -qed - - text \<open>The zero ideal is a principal ideal\<close> corollary (in ring) zeropideal: "principalideal {\<zero>} R" - apply (rule principalidealI) - apply (rule zeroideal) - apply (blast intro!: zero_genideal[symmetric]) - done + using genideal_zero principalidealI zeroideal by blast text \<open>The unit ideal is a principal ideal\<close> corollary (in ring) onepideal: "principalideal (carrier R) R" - apply (rule principalidealI) - apply (rule oneideal) - apply (blast intro!: one_genideal[symmetric]) - done - + using genideal_one oneideal principalidealI by blast text \<open>Every principal ideal is a right coset of the carrier\<close> lemma (in principalideal) rcos_generate: @@ -626,21 +462,13 @@ interpret cring R by fact from generate obtain i where icarr: "i \<in> carrier R" and I1: "I = Idl {i}" by fast+ - - from icarr and genideal_self[of "{i}"] have "i \<in> Idl {i}" - by fast - then have iI: "i \<in> I" by (simp add: I1) - - from I1 icarr have I2: "I = PIdl i" + then have "I = PIdl i" by (simp add: cgenideal_eq_genideal) - - have "PIdl i = carrier R #> i" + moreover have "i \<in> I" + by (simp add: I1 genideal_self' icarr) + moreover have "PIdl i = carrier R #> i" unfolding cgenideal_def r_coset_def by fast - - with I2 have "I = carrier R #> i" - by simp - - with iI show "\<exists>x\<in>I. I = carrier R #> x" + ultimately show "\<exists>x\<in>I. I = carrier R #> x" by fast qed @@ -698,11 +526,7 @@ then have I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp have "primeideal I R" - apply (rule primeideal.intro [OF is_ideal is_cring]) - apply (rule primeideal_axioms.intro) - apply (rule InR) - apply (erule (2) I_prime) - done + by (simp add: I_prime InR is_cring is_ideal primeidealI) with notprime show False by simp qed @@ -722,23 +546,15 @@ lemma (in cring) zeroprimeideal_domainI: assumes pi: "primeideal {\<zero>} R" shows "domain R" - apply (rule domain.intro, rule is_cring) - apply (rule domain_axioms.intro) -proof (rule ccontr, simp) - interpret primeideal "{\<zero>}" "R" by (rule pi) - assume "\<one> = \<zero>" - then have "carrier R = {\<zero>}" by (rule one_zeroD) - from this[symmetric] and I_notcarr show False - by simp -next - interpret primeideal "{\<zero>}" "R" by (rule pi) - fix a b - assume ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R" - from ab have abI: "a \<otimes> b \<in> {\<zero>}" - by fast - with carr have "a \<in> {\<zero>} \<or> b \<in> {\<zero>}" - by (rule I_prime) - then show "a = \<zero> \<or> b = \<zero>" by simp +proof (intro domain.intro is_cring domain_axioms.intro) + show "\<one> \<noteq> \<zero>" + using genideal_one genideal_zero pi primeideal.I_notcarr by force + show "a = \<zero> \<or> b = \<zero>" if ab: "a \<otimes> b = \<zero>" and carr: "a \<in> carrier R" "b \<in> carrier R" for a b + proof - + interpret primeideal "{\<zero>}" "R" by (rule pi) + show "a = \<zero> \<or> b = \<zero>" + using I_prime ab carr by blast + qed qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R" @@ -765,37 +581,18 @@ shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R" proof - interpret cring R by fact - show ?thesis apply (rule idealI) - apply (rule cring.axioms[OF is_cring]) - apply (rule subgroup.intro) - apply (simp, fast) - apply clarsimp apply (simp add: r_distr acarr) - apply (simp add: acarr) - apply (simp add: a_inv_def[symmetric], clarify) defer 1 - apply clarsimp defer 1 - apply (fast intro!: helper_I_closed acarr) - proof - - fix x - assume xcarr: "x \<in> carrier R" - and ax: "a \<otimes> x \<in> I" - from ax and acarr xcarr - have "\<ominus>(a \<otimes> x) \<in> I" by simp - also from acarr xcarr - have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra - finally show "a \<otimes> (\<ominus>x) \<in> I" . - from acarr have "a \<otimes> \<zero> = \<zero>" by simp - next - fix x y - assume xcarr: "x \<in> carrier R" - and ycarr: "y \<in> carrier R" - and ayI: "a \<otimes> y \<in> I" - from ayI and acarr xcarr ycarr have "a \<otimes> (y \<otimes> x) \<in> I" - by (simp add: helper_I_closed) - moreover - from xcarr ycarr have "y \<otimes> x = x \<otimes> y" - by (simp add: m_comm) - ultimately - show "a \<otimes> (x \<otimes> y) \<in> I" by simp + show ?thesis + proof (rule idealI, simp_all) + show "ring R" + by (simp add: local.ring_axioms) + show "subgroup {x \<in> carrier R. a \<otimes> x \<in> I} (add_monoid R)" + by (rule subgroup.intro) (auto simp: r_distr acarr r_minus simp flip: a_inv_def) + show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> + \<Longrightarrow> a \<otimes> (x \<otimes> b) \<in> I" + using acarr helper_I_closed m_comm by auto + show "\<And>b x. \<lbrakk>b \<in> carrier R \<and> a \<otimes> b \<in> I; x \<in> carrier R\<rbrakk> + \<Longrightarrow> a \<otimes> (b \<otimes> x) \<in> I" + by (simp add: acarr helper_I_closed) qed qed @@ -805,53 +602,27 @@ shows "primeideal I R" proof - interpret maximalideal I R by fact - show ?thesis apply (rule ccontr) - apply (rule primeidealCE) - apply (rule is_cring) - apply assumption - apply (simp add: I_notcarr) - proof - - assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I" - then obtain a b where - acarr: "a \<in> carrier R" and - bcarr: "b \<in> carrier R" and - abI: "a \<otimes> b \<in> I" and - anI: "a \<notin> I" and - bnI: "b \<notin> I" by fast + show ?thesis + proof (rule ccontr) + assume neg: "\<not> primeideal I R" + then obtain a b where acarr: "a \<in> carrier R" and bcarr: "b \<in> carrier R" + and abI: "a \<otimes> b \<in> I" and anI: "a \<notin> I" and bnI: "b \<notin> I" + using primeidealCE [OF is_cring] + by (metis I_notcarr) define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}" - from is_cring and acarr have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime) - have IsubJ: "I \<subseteq> J" - proof - fix x - assume xI: "x \<in> I" - with acarr have "a \<otimes> x \<in> I" - by (intro I_l_closed) - with xI[THEN a_Hcarr] show "x \<in> J" - unfolding J_def by fast - qed - + using I_l_closed J_def a_Hcarr acarr by blast from abI and acarr bcarr have "b \<in> J" unfolding J_def by fast with bnI have JnI: "J \<noteq> I" by fast - from acarr - have "a = a \<otimes> \<one>" by algebra - with anI have "a \<otimes> \<one> \<notin> I" by simp - with one_closed have "\<one> \<notin> J" - unfolding J_def by fast + have "\<one> \<notin> J" + unfolding J_def by (simp add: acarr anI) then have Jncarr: "J \<noteq> carrier R" by fast - - interpret ideal J R by (rule idealJ) - + interpret ideal J R by (rule idealJ) have "J = I \<or> J = carrier R" - apply (intro I_maximal) - apply (rule idealJ) - apply (rule IsubJ) - apply (rule a_subset) - done - + by (simp add: I_maximal IsubJ a_subset is_ideal) with JnI and Jncarr show False by simp qed qed @@ -859,54 +630,39 @@ subsection \<open>Derived Theorems\<close> -\<comment> \<open>A non-zero cring that has only the two trivial ideals is a field\<close> +text \<open>A non-zero cring that has only the two trivial ideals is a field\<close> lemma (in cring) trivialideals_fieldI: assumes carrnzero: "carrier R \<noteq> {\<zero>}" and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}" shows "field R" - apply (rule cring_fieldI) - apply (rule, rule, rule) - apply (erule Units_closed) - defer 1 - apply rule - defer 1 -proof (rule ccontr, simp) - assume zUnit: "\<zero> \<in> Units R" - then have a: "\<zero> \<otimes> inv \<zero> = \<one>" by (rule Units_r_inv) - from zUnit have "\<zero> \<otimes> inv \<zero> = \<zero>" - by (intro l_null) (rule Units_inv_closed) - with a[symmetric] have "\<one> = \<zero>" by simp - then have "carrier R = {\<zero>}" by (rule one_zeroD) - with carrnzero show False by simp -next - fix x - assume xcarr': "x \<in> carrier R - {\<zero>}" - then have xcarr: "x \<in> carrier R" by fast - from xcarr' have xnZ: "x \<noteq> \<zero>" by fast - from xcarr have xIdl: "ideal (PIdl x) R" - by (intro cgenideal_ideal) fast - - from xcarr have "x \<in> PIdl x" - by (intro cgenideal_self) fast - with xnZ have "PIdl x \<noteq> {\<zero>}" by fast - with haveideals have "PIdl x = carrier R" - by (blast intro!: xIdl) - then have "\<one> \<in> PIdl x" by simp - then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" - unfolding cgenideal_def by blast - then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x" - by fast+ - from ylinv and xcarr ycarr have yrinv: "\<one> = x \<otimes> y" - by (simp add: m_comm) - from ycarr and ylinv[symmetric] and yrinv[symmetric] - have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast - with xcarr show "x \<in> Units R" - unfolding Units_def by fast +proof (intro cring_fieldI equalityI) + show "Units R \<subseteq> carrier R - {\<zero>}" + by (metis Diff_empty Units_closed Units_r_inv_ex carrnzero l_null one_zeroD subsetI subset_Diff_insert) + show "carrier R - {\<zero>} \<subseteq> Units R" + proof + fix x + assume xcarr': "x \<in> carrier R - {\<zero>}" + then have xcarr: "x \<in> carrier R" and xnZ: "x \<noteq> \<zero>" by auto + from xcarr have xIdl: "ideal (PIdl x) R" + by (intro cgenideal_ideal) fast + have "PIdl x \<noteq> {\<zero>}" + using xcarr xnZ cgenideal_self by blast + with haveideals have "PIdl x = carrier R" + by (blast intro!: xIdl) + then have "\<one> \<in> PIdl x" by simp + then have "\<exists>y. \<one> = y \<otimes> x \<and> y \<in> carrier R" + unfolding cgenideal_def by blast + then obtain y where ycarr: " y \<in> carrier R" and ylinv: "\<one> = y \<otimes> x" + by fast + have "\<exists>y \<in> carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" + using m_comm xcarr ycarr ylinv by auto + with xcarr show "x \<in> Units R" + unfolding Units_def by fast + qed qed lemma (in field) all_ideals: "{I. ideal I R} = {{\<zero>}, carrier R}" - apply (rule, rule) -proof - +proof (intro equalityI subsetI) fix I assume a: "I \<in> {I. ideal I R}" then interpret ideal I R by simp @@ -916,41 +672,26 @@ case True then obtain a where aI: "a \<in> I" and anZ: "a \<noteq> \<zero>" by fast+ - from aI[THEN a_Hcarr] anZ have aUnit: "a \<in> Units R" - by (simp add: field_Units) + have aUnit: "a \<in> Units R" + by (simp add: aI anZ field_Units) then have a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv) from aI and aUnit have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv) then have oneI: "\<one> \<in> I" by (simp add: a[symmetric]) - have "carrier R \<subseteq> I" - proof - fix x - assume xcarr: "x \<in> carrier R" - with oneI have "\<one> \<otimes> x \<in> I" by (rule I_r_closed) - with xcarr show "x \<in> I" by simp - qed + using oneI one_imp_carrier by auto with a_subset have "I = carrier R" by fast then show "I \<in> {{\<zero>}, carrier R}" by fast next case False then have IZ: "\<And>a. a \<in> I \<Longrightarrow> a = \<zero>" by simp - have a: "I \<subseteq> {\<zero>}" - proof - fix x - assume "x \<in> I" - then have "x = \<zero>" by (rule IZ) - then show "x \<in> {\<zero>}" by fast - qed - + using False by auto have "\<zero> \<in> I" by simp - then have "{\<zero>} \<subseteq> I" by fast - with a have "I = {\<zero>}" by fast then show "I \<in> {{\<zero>}, carrier R}" by fast qed -qed (simp add: zeroideal oneideal) +qed (auto simp: zeroideal oneideal) \<comment>\<open>"Jacobson Theorem 2.2"\<close> lemma (in cring) trivialideals_eq_field: @@ -961,9 +702,7 @@ text \<open>Like zeroprimeideal for domains\<close> lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R" - apply (rule maximalidealI) - apply (rule zeroideal) -proof- +proof (intro maximalidealI zeroideal) from one_not_zero have "\<one> \<notin> {\<zero>}" by simp with one_closed show "carrier R \<noteq> {\<zero>}" by fast next @@ -977,20 +716,20 @@ lemma (in cring) zeromaximalideal_fieldI: assumes zeromax: "maximalideal {\<zero>} R" shows "field R" - apply (rule trivialideals_fieldI, rule maximalideal.I_notcarr[OF zeromax]) - apply rule apply clarsimp defer 1 - apply (simp add: zeroideal oneideal) -proof - - fix J - assume Jn0: "J \<noteq> {\<zero>}" - and idealJ: "ideal J R" - interpret ideal J R by (rule idealJ) - have "{\<zero>} \<subseteq> J" by (rule ccontr) simp - from zeromax and idealJ and this and a_subset - have "J = {\<zero>} \<or> J = carrier R" - by (rule maximalideal.I_maximal) - with Jn0 show "J = carrier R" - by simp +proof (intro trivialideals_fieldI maximalideal.I_notcarr[OF zeromax]) + have "J = carrier R" if Jn0: "J \<noteq> {\<zero>}" and idealJ: "ideal J R" for J + proof - + interpret ideal J R by (rule idealJ) + have "{\<zero>} \<subseteq> J" + by force + from zeromax idealJ this a_subset + have "J = {\<zero>} \<or> J = carrier R" + by (rule maximalideal.I_maximal) + with Jn0 show "J = carrier R" + by simp + qed + then show "{I. ideal I R} = {{\<zero>}, carrier R}" + by (auto simp: zeroideal oneideal) qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R"