src/HOL/Algebra/Divisibility.thy
 changeset 27717 21bbd410ba04 parent 27713 95b36bfe7fc4 child 28599 12d914277b8d
```--- 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) = ```