*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] lattices, typeclasses, notations?*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Mon, 30 May 2011 08:42:48 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Alexander Krauss <krauss at in.tum.de>*In-reply-to*: <BANLkTikaD8AsA2MzJz_vENXQ3QdDShapRA@mail.gmail.com>*References*: <BANLkTim4NOUps-hmB2UK_bd-XMJp=FFqnQ@mail.gmail.com> <4DE00F92.9040900@in.tum.de> <BANLkTikaD8AsA2MzJz_vENXQ3QdDShapRA@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Dear Randy,

Now I want to work with the dual of a given lattice. In HOL/Lattices.thy I see lemma dual_lattice: "class.lattice (op \<ge>) (op >) sup inf" by [...] What does that mean?

How can I use this lemma? Please point me to examples;.

Looking at the HOL/Lattice session I found the following kind of example datatype 'a dual = dual 'a primrec undual :: "'a dual \<Rightarrow> 'a" where undual_dual: "undual (dual x) = x" instantiation dual:: (lattice) lattice begin definition "inf_dual x y = dual (sup (undual x) (undual y))" [...] instance proof Now I get 12 subgoals (which I can probably prove) but I haven't taken advantage of lemma dual_lattice. Please explain how this is intended to be done.

Let me briefly compare the two approaches:

Hope this helps, Andreas

**References**:**[isabelle] lattices, typeclasses, notations?***From:*Randy Pollack

**Re: [isabelle] lattices, typeclasses, notations?***From:*Alexander Krauss

**Re: [isabelle] lattices, typeclasses, notations?***From:*Randy Pollack

- Previous by Date: Re: [isabelle] Can't access to a sublocale theorem
- Next by Date: Re: [isabelle] Can't access to a sublocale theorem
- Previous by Thread: Re: [isabelle] lattices, typeclasses, notations?
- Cl-isabelle-users May 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