distributed theory Algebras to theories Groups and Lattices
authorhaftmann
Mon Feb 22 15:53:18 2010 +0100 (2010-02-22)
changeset 3530190e42f9ba4d1
parent 35300 ca05ceeeb9ab
child 35302 4bc6b4d70e08
distributed theory Algebras to theories Groups and Lattices
src/HOL/Algebras.thy
src/HOL/Groups.thy
src/HOL/IsaMakefile
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Prolog/Func.thy
     1.1 --- a/src/HOL/Algebras.thy	Mon Feb 22 11:13:30 2010 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,55 +0,0 @@
     1.4 -(*  Title:      HOL/Algebras.thy
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Generic algebraic structures and operations *}
     1.9 -
    1.10 -theory Algebras
    1.11 -imports HOL
    1.12 -begin
    1.13 -
    1.14 -text {*
    1.15 -  These locales provide basic structures for interpretation into
    1.16 -  bigger structures;  extensions require careful thinking, otherwise
    1.17 -  undesired effects may occur due to interpretation.
    1.18 -*}
    1.19 -
    1.20 -ML {*
    1.21 -structure Ac_Simps = Named_Thms(
    1.22 -  val name = "ac_simps"
    1.23 -  val description = "associativity and commutativity simplification rules"
    1.24 -)
    1.25 -*}
    1.26 -
    1.27 -setup Ac_Simps.setup
    1.28 -
    1.29 -locale semigroup =
    1.30 -  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    1.31 -  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    1.32 -
    1.33 -locale abel_semigroup = semigroup +
    1.34 -  assumes commute [ac_simps]: "a * b = b * a"
    1.35 -begin
    1.36 -
    1.37 -lemma left_commute [ac_simps]:
    1.38 -  "b * (a * c) = a * (b * c)"
    1.39 -proof -
    1.40 -  have "(b * a) * c = (a * b) * c"
    1.41 -    by (simp only: commute)
    1.42 -  then show ?thesis
    1.43 -    by (simp only: assoc)
    1.44 -qed
    1.45 -
    1.46 -end
    1.47 -
    1.48 -locale semilattice = abel_semigroup +
    1.49 -  assumes idem [simp]: "a * a = a"
    1.50 -begin
    1.51 -
    1.52 -lemma left_idem [simp]:
    1.53 -  "a * (a * b) = a * b"
    1.54 -  by (simp add: assoc [symmetric])
    1.55 -
    1.56 -end
    1.57 -
    1.58 -end
    1.59 \ No newline at end of file
     2.1 --- a/src/HOL/Groups.thy	Mon Feb 22 11:13:30 2010 +0100
     2.2 +++ b/src/HOL/Groups.thy	Mon Feb 22 15:53:18 2010 +0100
     2.3 @@ -9,6 +9,65 @@
     2.4  uses ("~~/src/Provers/Arith/abel_cancel.ML")
     2.5  begin
     2.6  
     2.7 +subsection {* Fact collections *}
     2.8 +
     2.9 +ML {*
    2.10 +structure Algebra_Simps = Named_Thms(
    2.11 +  val name = "algebra_simps"
    2.12 +  val description = "algebra simplification rules"
    2.13 +)
    2.14 +*}
    2.15 +
    2.16 +setup Algebra_Simps.setup
    2.17 +
    2.18 +text{* The rewrites accumulated in @{text algebra_simps} deal with the
    2.19 +classical algebraic structures of groups, rings and family. They simplify
    2.20 +terms by multiplying everything out (in case of a ring) and bringing sums and
    2.21 +products into a canonical form (by ordered rewriting). As a result it decides
    2.22 +group and ring equalities but also helps with inequalities.
    2.23 +
    2.24 +Of course it also works for fields, but it knows nothing about multiplicative
    2.25 +inverses or division. This is catered for by @{text field_simps}. *}
    2.26 +
    2.27 +
    2.28 +ML {*
    2.29 +structure Ac_Simps = Named_Thms(
    2.30 +  val name = "ac_simps"
    2.31 +  val description = "associativity and commutativity simplification rules"
    2.32 +)
    2.33 +*}
    2.34 +
    2.35 +setup Ac_Simps.setup
    2.36 +
    2.37 +
    2.38 +subsection {* Abstract structures *}
    2.39 +
    2.40 +text {*
    2.41 +  These locales provide basic structures for interpretation into
    2.42 +  bigger structures;  extensions require careful thinking, otherwise
    2.43 +  undesired effects may occur due to interpretation.
    2.44 +*}
    2.45 +
    2.46 +locale semigroup =
    2.47 +  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    2.48 +  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    2.49 +
    2.50 +locale abel_semigroup = semigroup +
    2.51 +  assumes commute [ac_simps]: "a * b = b * a"
    2.52 +begin
    2.53 +
    2.54 +lemma left_commute [ac_simps]:
    2.55 +  "b * (a * c) = a * (b * c)"
    2.56 +proof -
    2.57 +  have "(b * a) * c = (a * b) * c"
    2.58 +    by (simp only: commute)
    2.59 +  then show ?thesis
    2.60 +    by (simp only: assoc)
    2.61 +qed
    2.62 +
    2.63 +end
    2.64 +
    2.65 +
    2.66  subsection {* Generic operations *}
    2.67  
    2.68  class zero = 
    2.69 @@ -64,37 +123,6 @@
    2.70  
    2.71  use "~~/src/Provers/Arith/abel_cancel.ML"
    2.72  
    2.73 -text {*
    2.74 -  The theory of partially ordered groups is taken from the books:
    2.75 -  \begin{itemize}
    2.76 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    2.77 -  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    2.78 -  \end{itemize}
    2.79 -  Most of the used notions can also be looked up in 
    2.80 -  \begin{itemize}
    2.81 -  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    2.82 -  \item \emph{Algebra I} by van der Waerden, Springer.
    2.83 -  \end{itemize}
    2.84 -*}
    2.85 -
    2.86 -ML {*
    2.87 -structure Algebra_Simps = Named_Thms(
    2.88 -  val name = "algebra_simps"
    2.89 -  val description = "algebra simplification rules"
    2.90 -)
    2.91 -*}
    2.92 -
    2.93 -setup Algebra_Simps.setup
    2.94 -
    2.95 -text{* The rewrites accumulated in @{text algebra_simps} deal with the
    2.96 -classical algebraic structures of groups, rings and family. They simplify
    2.97 -terms by multiplying everything out (in case of a ring) and bringing sums and
    2.98 -products into a canonical form (by ordered rewriting). As a result it decides
    2.99 -group and ring equalities but also helps with inequalities.
   2.100 -
   2.101 -Of course it also works for fields, but it knows nothing about multiplicative
   2.102 -inverses or division. This is catered for by @{text field_simps}. *}
   2.103 -
   2.104  
   2.105  subsection {* Semigroups and Monoids *}
   2.106  
   2.107 @@ -144,19 +172,6 @@
   2.108  
   2.109  theorems mult_ac = mult_assoc mult_commute mult_left_commute
   2.110  
   2.111 -class ab_semigroup_idem_mult = ab_semigroup_mult +
   2.112 -  assumes mult_idem: "x * x = x"
   2.113 -
   2.114 -sublocale ab_semigroup_idem_mult < times!: semilattice times proof
   2.115 -qed (fact mult_idem)
   2.116 -
   2.117 -context ab_semigroup_idem_mult
   2.118 -begin
   2.119 -
   2.120 -lemmas mult_left_idem = times.left_idem
   2.121 -
   2.122 -end
   2.123 -
   2.124  class monoid_add = zero + semigroup_add +
   2.125    assumes add_0_left [simp]: "0 + a = a"
   2.126      and add_0_right [simp]: "a + 0 = a"
   2.127 @@ -411,6 +426,19 @@
   2.128  
   2.129  subsection {* (Partially) Ordered Groups *} 
   2.130  
   2.131 +text {*
   2.132 +  The theory of partially ordered groups is taken from the books:
   2.133 +  \begin{itemize}
   2.134 +  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   2.135 +  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   2.136 +  \end{itemize}
   2.137 +  Most of the used notions can also be looked up in 
   2.138 +  \begin{itemize}
   2.139 +  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   2.140 +  \item \emph{Algebra I} by van der Waerden, Springer.
   2.141 +  \end{itemize}
   2.142 +*}
   2.143 +
   2.144  class ordered_ab_semigroup_add = order + ab_semigroup_add +
   2.145    assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   2.146  begin
     3.1 --- a/src/HOL/IsaMakefile	Mon Feb 22 11:13:30 2010 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Feb 22 15:53:18 2010 +0100
     3.3 @@ -142,7 +142,6 @@
     3.4  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
     3.5  
     3.6  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
     3.7 -  Algebras.thy \
     3.8    Complete_Lattice.thy \
     3.9    Datatype.thy \
    3.10    Extraction.thy \
    3.11 @@ -386,7 +385,7 @@
    3.12  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
    3.13    Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy	\
    3.14    Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy			\
    3.15 -  Library/Sum_Of_Squares/sos_wrapper.ML					\
    3.16 +  Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML		
    3.17    Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
    3.18    Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy	\
    3.19    Library/Infinite_Set.thy Library/FuncSet.thy				\
     4.1 --- a/src/HOL/Lattices.thy	Mon Feb 22 11:13:30 2010 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Mon Feb 22 15:53:18 2010 +0100
     4.3 @@ -8,7 +8,42 @@
     4.4  imports Orderings Groups
     4.5  begin
     4.6  
     4.7 -subsection {* Lattices *}
     4.8 +subsection {* Abstract semilattice *}
     4.9 +
    4.10 +text {*
    4.11 +  This locales provide a basic structure for interpretation into
    4.12 +  bigger structures;  extensions require careful thinking, otherwise
    4.13 +  undesired effects may occur due to interpretation.
    4.14 +*}
    4.15 +
    4.16 +locale semilattice = abel_semigroup +
    4.17 +  assumes idem [simp]: "f a a = a"
    4.18 +begin
    4.19 +
    4.20 +lemma left_idem [simp]:
    4.21 +  "f a (f a b) = f a b"
    4.22 +  by (simp add: assoc [symmetric])
    4.23 +
    4.24 +end
    4.25 +
    4.26 +
    4.27 +subsection {* Idempotent semigroup *}
    4.28 +
    4.29 +class ab_semigroup_idem_mult = ab_semigroup_mult +
    4.30 +  assumes mult_idem: "x * x = x"
    4.31 +
    4.32 +sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    4.33 +qed (fact mult_idem)
    4.34 +
    4.35 +context ab_semigroup_idem_mult
    4.36 +begin
    4.37 +
    4.38 +lemmas mult_left_idem = times.left_idem
    4.39 +
    4.40 +end
    4.41 +
    4.42 +
    4.43 +subsection {* Conrete lattices *}
    4.44  
    4.45  notation
    4.46    less_eq  (infix "\<sqsubseteq>" 50) and
     5.1 --- a/src/HOL/Orderings.thy	Mon Feb 22 11:13:30 2010 +0100
     5.2 +++ b/src/HOL/Orderings.thy	Mon Feb 22 15:53:18 2010 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Abstract orderings *}
     5.5  
     5.6  theory Orderings
     5.7 -imports Algebras
     5.8 +imports HOL
     5.9  uses
    5.10    "~~/src/Provers/order.ML"
    5.11    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
     6.1 --- a/src/HOL/Prolog/Func.thy	Mon Feb 22 11:13:30 2010 +0100
     6.2 +++ b/src/HOL/Prolog/Func.thy	Mon Feb 22 15:53:18 2010 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Untyped functional language, with call by value semantics *}
     6.5  
     6.6  theory Func
     6.7 -imports HOHH Algebras
     6.8 +imports HOHH
     6.9  begin
    6.10  
    6.11  typedecl tm