# HG changeset patch
# User haftmann
# Date 1266850398 -3600
# Node ID 90e42f9ba4d104f709100398a5c7156947a4bb22
# Parent  ca05ceeeb9abd76de16858e7b88d48c5ecf161af
distributed theory Algebras to theories Groups and Lattices

diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/Algebras.thy
--- a/src/HOL/Algebras.thy	Mon Feb 22 11:13:30 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(*  Title:      HOL/Algebras.thy
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Generic algebraic structures and operations *}
-
-theory Algebras
-imports HOL
-begin
-
-text {*
-  These locales provide basic structures for interpretation into
-  bigger structures;  extensions require careful thinking, otherwise
-  undesired effects may occur due to interpretation.
-*}
-
-ML {*
-structure Ac_Simps = Named_Thms(
-  val name = "ac_simps"
-  val description = "associativity and commutativity simplification rules"
-)
-*}
-
-setup Ac_Simps.setup
-
-locale semigroup =
-  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
-
-locale abel_semigroup = semigroup +
-  assumes commute [ac_simps]: "a * b = b * a"
-begin
-
-lemma left_commute [ac_simps]:
-  "b * (a * c) = a * (b * c)"
-proof -
-  have "(b * a) * c = (a * b) * c"
-    by (simp only: commute)
-  then show ?thesis
-    by (simp only: assoc)
-qed
-
-end
-
-locale semilattice = abel_semigroup +
-  assumes idem [simp]: "a * a = a"
-begin
-
-lemma left_idem [simp]:
-  "a * (a * b) = a * b"
-  by (simp add: assoc [symmetric])
-
-end
-
-end
\ No newline at end of file
diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Feb 22 11:13:30 2010 +0100
+++ b/src/HOL/Groups.thy	Mon Feb 22 15:53:18 2010 +0100
@@ -9,6 +9,65 @@
 uses ("~~/src/Provers/Arith/abel_cancel.ML")
 begin
 
+subsection {* Fact collections *}
+
+ML {*
+structure Algebra_Simps = Named_Thms(
+  val name = "algebra_simps"
+  val description = "algebra simplification rules"
+)
+*}
+
+setup Algebra_Simps.setup
+
+text{* The rewrites accumulated in @{text algebra_simps} deal with the
+classical algebraic structures of groups, rings and family. They simplify
+terms by multiplying everything out (in case of a ring) and bringing sums and
+products into a canonical form (by ordered rewriting). As a result it decides
+group and ring equalities but also helps with inequalities.
+
+Of course it also works for fields, but it knows nothing about multiplicative
+inverses or division. This is catered for by @{text field_simps}. *}
+
+
+ML {*
+structure Ac_Simps = Named_Thms(
+  val name = "ac_simps"
+  val description = "associativity and commutativity simplification rules"
+)
+*}
+
+setup Ac_Simps.setup
+
+
+subsection {* Abstract structures *}
+
+text {*
+  These locales provide basic structures for interpretation into
+  bigger structures;  extensions require careful thinking, otherwise
+  undesired effects may occur due to interpretation.
+*}
+
+locale semigroup =
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
+
+locale abel_semigroup = semigroup +
+  assumes commute [ac_simps]: "a * b = b * a"
+begin
+
+lemma left_commute [ac_simps]:
+  "b * (a * c) = a * (b * c)"
+proof -
+  have "(b * a) * c = (a * b) * c"
+    by (simp only: commute)
+  then show ?thesis
+    by (simp only: assoc)
+qed
+
+end
+
+
 subsection {* Generic operations *}
 
 class zero = 
@@ -64,37 +123,6 @@
 
 use "~~/src/Provers/Arith/abel_cancel.ML"
 
-text {*
-  The theory of partially ordered groups is taken from the books:
-  \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
-  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
-  \end{itemize}
-  Most of the used notions can also be looked up in 
-  \begin{itemize}
-  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
-  \item \emph{Algebra I} by van der Waerden, Springer.
-  \end{itemize}
-*}
-
-ML {*
-structure Algebra_Simps = Named_Thms(
-  val name = "algebra_simps"
-  val description = "algebra simplification rules"
-)
-*}
-
-setup Algebra_Simps.setup
-
-text{* The rewrites accumulated in @{text algebra_simps} deal with the
-classical algebraic structures of groups, rings and family. They simplify
-terms by multiplying everything out (in case of a ring) and bringing sums and
-products into a canonical form (by ordered rewriting). As a result it decides
-group and ring equalities but also helps with inequalities.
-
-Of course it also works for fields, but it knows nothing about multiplicative
-inverses or division. This is catered for by @{text field_simps}. *}
-
 
 subsection {* Semigroups and Monoids *}
 
@@ -144,19 +172,6 @@
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
-class ab_semigroup_idem_mult = ab_semigroup_mult +
-  assumes mult_idem: "x * x = x"
-
-sublocale ab_semigroup_idem_mult < times!: semilattice times proof
-qed (fact mult_idem)
-
-context ab_semigroup_idem_mult
-begin
-
-lemmas mult_left_idem = times.left_idem
-
-end
-
 class monoid_add = zero + semigroup_add +
   assumes add_0_left [simp]: "0 + a = a"
     and add_0_right [simp]: "a + 0 = a"
@@ -411,6 +426,19 @@
 
 subsection {* (Partially) Ordered Groups *} 
 
+text {*
+  The theory of partially ordered groups is taken from the books:
+  \begin{itemize}
+  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
+  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
+  \end{itemize}
+  Most of the used notions can also be looked up in 
+  \begin{itemize}
+  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+  \item \emph{Algebra I} by van der Waerden, Springer.
+  \end{itemize}
+*}
+
 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
 begin
diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Feb 22 11:13:30 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 22 15:53:18 2010 +0100
@@ -142,7 +142,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
-  Algebras.thy \
   Complete_Lattice.thy \
   Datatype.thy \
   Extraction.thy \
@@ -386,7 +385,7 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy	\
   Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy			\
-  Library/Sum_Of_Squares/sos_wrapper.ML					\
+  Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML		
   Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
   Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy	\
   Library/Infinite_Set.thy Library/FuncSet.thy				\
diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Feb 22 11:13:30 2010 +0100
+++ b/src/HOL/Lattices.thy	Mon Feb 22 15:53:18 2010 +0100
@@ -8,7 +8,42 @@
 imports Orderings Groups
 begin
 
-subsection {* Lattices *}
+subsection {* Abstract semilattice *}
+
+text {*
+  This locales provide a basic structure for interpretation into
+  bigger structures;  extensions require careful thinking, otherwise
+  undesired effects may occur due to interpretation.
+*}
+
+locale semilattice = abel_semigroup +
+  assumes idem [simp]: "f a a = a"
+begin
+
+lemma left_idem [simp]:
+  "f a (f a b) = f a b"
+  by (simp add: assoc [symmetric])
+
+end
+
+
+subsection {* Idempotent semigroup *}
+
+class ab_semigroup_idem_mult = ab_semigroup_mult +
+  assumes mult_idem: "x * x = x"
+
+sublocale ab_semigroup_idem_mult < times!: semilattice times proof
+qed (fact mult_idem)
+
+context ab_semigroup_idem_mult
+begin
+
+lemmas mult_left_idem = times.left_idem
+
+end
+
+
+subsection {* Conrete lattices *}
 
 notation
   less_eq  (infix "\<sqsubseteq>" 50) and
diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Feb 22 11:13:30 2010 +0100
+++ b/src/HOL/Orderings.thy	Mon Feb 22 15:53:18 2010 +0100
@@ -5,7 +5,7 @@
 header {* Abstract orderings *}
 
 theory Orderings
-imports Algebras
+imports HOL
 uses
   "~~/src/Provers/order.ML"
   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
diff -r ca05ceeeb9ab -r 90e42f9ba4d1 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Mon Feb 22 11:13:30 2010 +0100
+++ b/src/HOL/Prolog/Func.thy	Mon Feb 22 15:53:18 2010 +0100
@@ -5,7 +5,7 @@
 header {* Untyped functional language, with call by value semantics *}
 
 theory Func
-imports HOHH Algebras
+imports HOHH
 begin
 
 typedecl tm