*To*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] 3 new AFP entries*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Date*: Tue, 27 Sep 2011 18:26:24 +1000

We are please to announce the availability of 3 new AFP entries at [http://afp.sf.net]. This brings the number of AFP entries over 100! 1. Lattice Properties by Viorel Preoteasa This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are complete distributive lattices, modular and distributive lattices, as well as lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and distributive lattices in general. 2. Algebra of Monotonic Boolean Transformers by Viorel Preoteasa Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself). 3. Pseudo Hoops by George Georgescu, Laurentiu Leustean and Viorel Preoteasa Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equiv- alent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization. Cheers, Gerwin

**Follow-Ups**:**Re: [isabelle] 3 new AFP entries***From:*Victor Porton

- Previous by Date: Re: [isabelle] Instantiate schematic variable in apply-script
- Next by Date: Re: [isabelle] set quick_and_dirty mode when running Isabelle from the command line?
- Previous by Thread: Re: [isabelle] set quick_and_dirty mode when running Isabelle from the command line?
- Next by Thread: Re: [isabelle] 3 new AFP entries
- Cl-isabelle-users September 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list