--- a/src/HOL/Algebra/Ideal.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy Tue Jul 15 16:50:09 2008 +0200
@@ -28,18 +28,21 @@
by (rule ideal_axioms)
lemma idealI:
- includes ring
+ fixes R (structure)
+ assumes "ring R"
assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
shows "ideal I R"
- apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
+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
-
+qed
subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
@@ -58,11 +61,14 @@
by (rule principalideal_axioms)
lemma principalidealI:
- includes ideal
+ fixes R (structure)
+ assumes "ideal I R"
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
shows "principalideal I R"
- by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
-
+proof -
+ interpret ideal [I R] by fact
+ show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
+qed
subsection {* Maximal Ideals *}
@@ -75,13 +81,16 @@
by (rule maximalideal_axioms)
lemma maximalidealI:
- includes ideal
+ fixes R
+ assumes "ideal I R"
assumes I_notcarr: "carrier R \<noteq> I"
and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
shows "maximalideal I R"
- by (intro maximalideal.intro maximalideal_axioms.intro)
+proof -
+ interpret ideal [I R] by fact
+ show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
(rule is_ideal, rule I_notcarr, rule I_maximal)
-
+qed
subsection {* Prime Ideals *}
@@ -94,31 +103,40 @@
by (rule primeideal_axioms)
lemma primeidealI:
- includes ideal
- includes cring
+ fixes R (structure)
+ assumes "ideal I R"
+ assumes "cring R"
assumes I_notcarr: "carrier R \<noteq> I"
and 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"
shows "primeideal I R"
- by (intro primeideal.intro primeideal_axioms.intro)
+proof -
+ interpret ideal [I R] by fact
+ interpret cring [R] by fact
+ show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
+qed
lemma primeidealI2:
- includes additive_subgroup I R
- includes cring
+ fixes R (structure)
+ assumes "additive_subgroup I R"
+ assumes "cring R"
assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
and I_notcarr: "carrier R \<noteq> I"
and 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"
shows "primeideal I R"
-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
-
+proof -
+ interpret additive_subgroup [I R] by fact
+ interpret cring [R] by fact
+ 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
+qed
section {* Properties of Ideals *}
@@ -185,9 +203,13 @@
text {* \paragraph{Intersection of two ideals} The intersection of any
two ideals is again an ideal in @{term R} *}
lemma (in ring) i_intersect:
- includes ideal I R
- includes ideal J R
+ assumes "ideal I R"
+ assumes "ideal J R"
shows "ideal (I \<inter> J) R"
+proof -
+ interpret ideal [I R] by fact
+ interpret ideal [J R] by fact
+ show ?thesis
apply (intro idealI subgroup.intro)
apply (rule is_ring)
apply (force simp add: a_subset)
@@ -199,7 +221,7 @@
apply (clarsimp, rule)
apply (fast intro: ideal.I_r_closed ideal.intro prems)+
done
-
+qed
subsubsection {* Intersection of a Set of Ideals *}
@@ -511,15 +533,18 @@
text {* @{const "cgenideal"} is minimal *}
lemma (in ring) cgenideal_minimal:
- includes ideal J R
+ assumes "ideal J R"
assumes aJ: "a \<in> J"
shows "PIdl a \<subseteq> J"
-unfolding cgenideal_def
-apply rule
-apply clarify
-using aJ
-apply (erule I_l_closed)
-done
+proof -
+ interpret ideal [J R] by fact
+ show ?thesis unfolding cgenideal_def
+ apply rule
+ apply clarify
+ using aJ
+ apply (erule I_l_closed)
+ done
+qed
lemma (in cring) cgenideal_eq_genideal:
assumes icarr: "i \<in> carrier R"
@@ -636,9 +661,10 @@
text {* Every principal ideal is a right coset of the carrier *}
lemma (in principalideal) rcos_generate:
- includes cring
+ assumes "cring R"
shows "\<exists>x\<in>I. I = carrier R #> x"
proof -
+ interpret cring [R] by fact
from generate
obtain i
where icarr: "i \<in> carrier R"
@@ -667,10 +693,11 @@
subsection {* Prime Ideals *}
lemma (in ideal) primeidealCD:
- includes cring
+ assumes "cring R"
assumes notprime: "\<not> primeideal I R"
shows "carrier R = I \<or> (\<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)"
proof (rule ccontr, clarsimp)
+ interpret cring [R] by fact
assume InR: "carrier R \<noteq> I"
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
hence 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
@@ -685,11 +712,16 @@
qed
lemma (in ideal) primeidealCE:
- includes cring
+ assumes "cring R"
assumes notprime: "\<not> primeideal I R"
obtains "carrier R = I"
| "\<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"
- using primeidealCD [OF R.is_cring notprime] by blast
+proof -
+ interpret R: cring [R] by fact
+ assume "carrier R = I ==> thesis"
+ and "\<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 \<Longrightarrow> thesis"
+ then show thesis using primeidealCD [OF R.is_cring notprime] by blast
+qed
text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
lemma (in cring) zeroprimeideal_domainI:
@@ -739,103 +771,108 @@
qed
lemma (in ideal) helper_max_prime:
- includes cring
+ assumes "cring R"
assumes acarr: "a \<in> carrier R"
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
-apply (rule idealI)
- apply (rule cring.axioms[OF is_cring])
- apply (rule subgroup.intro)
- apply (simp, fast)
+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
+ 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
+ qed
qed
text {* In a cring every maximal ideal is prime *}
lemma (in cring) maximalideal_is_prime:
- includes maximalideal
+ assumes "maximalideal I R"
shows "primeideal I R"
-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"
- from this
- 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"
+ 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"
+ from this
+ 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
- def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
-
- from R.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"
- from this and acarr
- have "a \<otimes> x \<in> I" by (intro I_l_closed)
- from xI[THEN a_Hcarr] this
- show "x \<in> J" unfolding J_def by fast
+ def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
+
+ from R.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"
+ from this and acarr
+ have "a \<otimes> x \<in> I" by (intro I_l_closed)
+ from xI[THEN a_Hcarr] this
+ show "x \<in> J" unfolding J_def by fast
+ qed
+
+ from abI and acarr bcarr
+ have "b \<in> J" unfolding J_def by fast
+ from bnI and this
+ have JnI: "J \<noteq> I" by fast
+ from acarr
+ have "a = a \<otimes> \<one>" by algebra
+ from this and anI
+ have "a \<otimes> \<one> \<notin> I" by simp
+ from one_closed and this
+ have "\<one> \<notin> J" unfolding J_def by fast
+ hence Jncarr: "J \<noteq> carrier R" by fast
+
+ 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
+
+ from this and JnI and Jncarr
+ show "False" by simp
qed
-
- from abI and acarr bcarr
- have "b \<in> J" unfolding J_def by fast
- from bnI and this
- have JnI: "J \<noteq> I" by fast
- from acarr
- have "a = a \<otimes> \<one>" by algebra
- from this and anI
- have "a \<otimes> \<one> \<notin> I" by simp
- from one_closed and this
- have "\<one> \<notin> J" unfolding J_def by fast
- hence Jncarr: "J \<noteq> carrier R" by fast
-
- 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
-
- from this and JnI and Jncarr
- show "False" by simp
qed
-
subsection {* Derived Theorems Involving Ideals *}
--"A non-zero cring that has only the two trivial ideals is a field"