--- 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
--- 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
--- 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 \
--- 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
--- 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? *)
--- 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