--- a/src/HOL/Algebra/Ideal.thy Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy Fri Aug 01 18:10:52 2008 +0200
@@ -10,7 +10,9 @@
section {* Ideals *}
-subsection {* General definition *}
+subsection {* Definitions *}
+
+subsubsection {* General definition *}
locale ideal = additive_subgroup I R + ring R +
assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
@@ -44,14 +46,14 @@
done
qed
-subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
+subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
constdefs (structure R)
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
"genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
-subsection {* Principal Ideals *}
+subsubsection {* Principal Ideals *}
locale principalideal = ideal +
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
@@ -70,7 +72,7 @@
show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
qed
-subsection {* Maximal Ideals *}
+subsubsection {* Maximal Ideals *}
locale maximalideal = ideal +
assumes I_notcarr: "carrier R \<noteq> I"
@@ -92,7 +94,7 @@
(rule is_ideal, rule I_notcarr, rule I_maximal)
qed
-subsection {* Prime Ideals *}
+subsubsection {* Prime Ideals *}
locale primeideal = ideal + cring +
assumes I_notcarr: "carrier R \<noteq> I"
@@ -138,8 +140,6 @@
done
qed
-section {* Properties of Ideals *}
-
subsection {* Special Ideals *}
lemma (in ring) zeroideal:
@@ -223,8 +223,6 @@
done
qed
-subsubsection {* Intersection of a Set of Ideals *}
-
text {* The intersection of any Number of Ideals is again
an Ideal in @{term R} *}
lemma (in ring) i_Intersect:
@@ -352,8 +350,6 @@
subsection {* Ideals generated by a subset of @{term [locale=ring]
"carrier R"} *}
-subsubsection {* Generation of Ideals in General Rings *}
-
text {* @{term genideal} generates an ideal *}
lemma (in ring) genideal_ideal:
assumes Scarr: "S \<subseteq> carrier R"
@@ -455,7 +451,7 @@
qed
-subsubsection {* Generation of Principal Ideals in Commutative Rings *}
+text {* Generation of Principal Ideals in Commutative Rings *}
constdefs (structure R)
cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
@@ -873,7 +869,7 @@
qed
qed
-subsection {* Derived Theorems Involving Ideals *}
+subsection {* Derived Theorems *}
--"A non-zero cring that has only the two trivial ideals is a field"
lemma (in cring) trivialideals_fieldI: