*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] the state of the lattice theories*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 29 Jul 2011 07:58:34 +0200*In-reply-to*: <80A7BCBE-C1F8-4C2B-AB4F-4DF1C1B1B941@gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <80A7BCBE-C1F8-4C2B-AB4F-4DF1C1B1B941@gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.18) Gecko/20110617 Lightning/1.0b2 Thunderbird/3.1.11

Hi Peter, first of all, HOL-Lattice is more an example than a library. I would guess that the lattice in HOL-Algebra is what you want to start an. The order development in HOLCF is traditionally something specific apart. > Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth? Well, there *has* been a lots of effort to reduce the number of lattice developments to effectively two. For the background, I quote here from an e-mail from isabelle-dev: > a few years > ago, around 2006, when I entered this type class adventure in more deep, > I came to the conclusion that it is usually better to have > »constructive« type classes, e.g. if we specify a semilattice as type > class, we don't assume »there exists a inf such that …« but we add an > explicit parameter »inf« which a corresponding set of properties. > > Otherwise we would define »inf« with »THE x. …«, and this means that for > particular instances of lattices (sets, nats, …) you have to derive > type-specific primitive rules (e.g. inf on 0/Suc representation, inf on > {}/insert representation) manually starting with a »THE x. …« > definition. In practice, it is much more straightforward to define inf > on particular types directly and then prove that this instance conforms > to its axiomatic specification. As a side effect, you get reasonable > code equations, something which can hardly be achieved if inf would be a > generic polymorphic operation rather than a class parameter. > > Of course, these constructive type classes are more specific than the > mathematical concept they represent, but for meta-theory a > record/locale-based approach with explicit carrier sets as in > HOL-Algebra is much more feasible anyway. But see also the funny lemma > http://isabelle.in.tum.de/repos/isabelle/file/7270ae921cf2/src/HOL/Lattices.thy#l447 > which shows how even the contructive type classes are able to talk about > uniqueness. Cheers, Florian -- PGP available: http://www.haftmann-online.de/florian/florian_at_haftmann_online_de -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] the state of the lattice theories***From:*Peter Gammie

**References**:**[isabelle] the state of the lattice theories***From:*Peter Gammie

- Previous by Date: Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
- Next by Date: [isabelle] Termination of function with let-binding on left-nested tuples
- Previous by Thread: Re: [isabelle] the state of the lattice theories
- Next by Thread: Re: [isabelle] the state of the lattice theories
- Cl-isabelle-users July 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