src/HOL/Lattices.thy
changeset 35301 90e42f9ba4d1
parent 35121 36c0a6dd8c6f
child 35724 178ad68f93ed
     1.1 --- a/src/HOL/Lattices.thy	Mon Feb 22 11:13:30 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Mon Feb 22 15:53:18 2010 +0100
     1.3 @@ -8,7 +8,42 @@
     1.4  imports Orderings Groups
     1.5  begin
     1.6  
     1.7 -subsection {* Lattices *}
     1.8 +subsection {* Abstract semilattice *}
     1.9 +
    1.10 +text {*
    1.11 +  This locales provide a basic structure for interpretation into
    1.12 +  bigger structures;  extensions require careful thinking, otherwise
    1.13 +  undesired effects may occur due to interpretation.
    1.14 +*}
    1.15 +
    1.16 +locale semilattice = abel_semigroup +
    1.17 +  assumes idem [simp]: "f a a = a"
    1.18 +begin
    1.19 +
    1.20 +lemma left_idem [simp]:
    1.21 +  "f a (f a b) = f a b"
    1.22 +  by (simp add: assoc [symmetric])
    1.23 +
    1.24 +end
    1.25 +
    1.26 +
    1.27 +subsection {* Idempotent semigroup *}
    1.28 +
    1.29 +class ab_semigroup_idem_mult = ab_semigroup_mult +
    1.30 +  assumes mult_idem: "x * x = x"
    1.31 +
    1.32 +sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    1.33 +qed (fact mult_idem)
    1.34 +
    1.35 +context ab_semigroup_idem_mult
    1.36 +begin
    1.37 +
    1.38 +lemmas mult_left_idem = times.left_idem
    1.39 +
    1.40 +end
    1.41 +
    1.42 +
    1.43 +subsection {* Conrete lattices *}
    1.44  
    1.45  notation
    1.46    less_eq  (infix "\<sqsubseteq>" 50) and