--- a/src/HOL/Algebra/Divisibility.thy Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Fri Aug 01 18:10:52 2008 +0200
@@ -3,14 +3,16 @@
Id: $Id$
Author: Clemens Ballarin, started 18 July 2008
-Based on work by Stefan Hohe.
+Based on work by Stephan Hohe.
*)
theory Divisibility
imports Permutation Coset Group
begin
-subsection {* Monoid with cancelation law *}
+section {* Factorial Monoids *}
+
+subsection {* Monoids with Cancellation Law *}
locale monoid_cancel = monoid +
assumes l_cancel:
@@ -56,7 +58,7 @@
by unfold_locales
-subsection {* Products of units in monoids *}
+subsection {* Products of Units in Monoids *}
lemma (in monoid) Units_m_closed[simp, intro]:
assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
@@ -150,7 +152,7 @@
show "a \<in> Units G" by (simp add: Units_def, fast)
qed
-subsection {* Divisibility and association *}
+subsection {* Divisibility and Association *}
subsubsection {* Function definitions *}
@@ -811,7 +813,7 @@
by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
-subsection {* Irreducible elements and primes *}
+subsection {* Irreducible Elements and Primes *}
subsubsection {* Irreducible elements *}
@@ -1031,11 +1033,7 @@
qed
-subsection {* Factorization and factorial monoids *}
-
-(*
-hide (open) const mult (* Multiset.mult, conflicting with monoid.mult *)
-*)
+subsection {* Factorization and Factorial Monoids *}
subsubsection {* Function definitions *}
@@ -1891,7 +1889,7 @@
qed (blast intro: factors_wfactors wfactors_unique)
-subsection {* Factorizations as multisets *}
+subsection {* Factorizations as Multisets *}
text {* Gives useful operations like intersection *}
@@ -2370,7 +2368,7 @@
qed
-subsection {* Irreducible elements are prime *}
+subsection {* Irreducible Elements are Prime *}
lemma (in factorial_monoid) irreducible_is_prime:
assumes pirr: "irreducible G p"
@@ -2610,7 +2608,7 @@
qed
-subsection {* Greatest common divisors and lowest common multiples *}
+subsection {* Greatest Common Divisors and Lowest Common Multiples *}
subsubsection {* Definitions *}
@@ -2907,7 +2905,7 @@
qed
-subsection {* Conditions for factoriality *}
+subsection {* Conditions for Factoriality *}
subsubsection {* Gcd condition *}
@@ -3891,7 +3889,7 @@
qed
-subsection {* Factoriality theorems *}
+subsection {* Factoriality Theorems *}
theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) =