### Abstract

This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are modular, and lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and complete lattices in general.

### License

BSD License

### History

January 5, 2012
  Removed the theory about distributive complete lattices which is in the standard library now. Added a theory about well founded and transitive relations and a result about fixpoints in complete lattices and well founded relations. Moved the results about conjunctive and disjunctive functions to a new theory. Removed the syntactic classes for inf and sup which are in the standard library now.

### Topics

- Mathematics/Order

### Session LatticeProperties

- WellFoundedTransitive
- Complete_Lattice_Prop
- Conj_Disj
- Lattice_Prop
- Modular_Distrib_Lattice
- Lattice_Ordered_Group

### Used by

- Algebra of Monotonic Boolean Transformers
- Pseudo Hoops
- Semantics and Data Refinement of Invariant Based Programs

## Cite

×

LatticeProperties-AFP

    @article{LatticeProperties-AFP,
      author  = {Viorel Preoteasa},
      title   = {Lattice Properties},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2011},
      note    = {\url{https://isa-afp.org/entries/LatticeProperties.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 28, 2019 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Sep 27, 2011 : Isabelle2011