*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] lattices, typeclasses, notations?*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Sun, 29 May 2011 18:31:25 -0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4DE00F92.9040900@in.tum.de>*References*: <BANLkTim4NOUps-hmB2UK_bd-XMJp=FFqnQ@mail.gmail.com> <4DE00F92.9040900@in.tum.de>*Sender*: rpollack0 at gmail.com

Thanks Alex. I'm using "order" in HOL/Orderings.thy and "lattice" in HOL/Lattices.thy as Alex suggested. My typeclass instantiation works. 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;. This lemma is not even used to prove lemma dual_bounded_lattice in the same file. 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. Thanks, Randy --- On Fri, May 27, 2011 at 4:54 PM, Alexander Krauss <krauss at in.tum.de> wrote: > Hi Randy, > > [...] >> >> However as a typeclass instantiation I get stuck: >> >> instantiation policy::partial_order > > First of all, you seem to be using the partial_order class from HOL/Lattice > session. There is nothing wrong with this, but note that there is also a > similar class "order" in HOL/Orderings.thy and "lattice" in > HOL/Lattices.thy. These are already part of the HOL image, and I think they > are better integrated in terms of reasoning infrastructure, but I am not > sure. These classes use the symbol \<le> rather than \<sqsubseteq> and also > include a strict variant. > >> begin >> definition "leq = policyOrder" >> instance >> proof (intro_classes) >> >> The first goal is >> >> \<And>x. x \<sqsubseteq> x >> >> So I try >> >> fix x::policy show "x \<sqsubseteq> x" >> >> Already this is not accepted. Perhaps there is an ambiguity between >> the \<sqsubseteq> of policyOrder and the \<sqsubseteq> of the >> partial_order class (in spite of the explicit annotation (x::policy"). >> >> So I try >> >> fix x::policy show "leq x x" using policyOrderRfl . >> >> Here the "show" is accepted, but the last step "." still fails. >> >> What is my problem? Thanks for any info. > > You are confusing the two constants, "leq" and "policyOrder". They are > defined to be equal, but the definition must be used explicitly. Since you > have ambiguous notation, \<sqsubseteq> refers to policyOrder, which is why > the first attempt fails. In the second attempt, your goal is OK, but the > proof is not, because policyOrderRfl uses a different constant. You should > unfold the definition (I think in this context it will be called something > like leq_policy_def) explicitly. > > It may also be a good idea to get rid of the syntax for policyOrder. It > makes your grammar ambiguous (which produces tons of warnings), and once you > have the instance, you can use it anyway, since it is defined for the type > class. > > Hope this helps, > Alex > >

**Follow-Ups**:**Re: [isabelle] lattices, typeclasses, notations?***From:*Andreas Lochbihler

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

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

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