Re: [isabelle] lattices, typeclasses, notations?

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?
This lemma is proven in the context lattice, i.e. it holds for all instances of the lattice type class. Thus, this means that the assumptions of the type class lattice (expressed by the predicate class.lattice) hold for the operations >=, >, sup, inf for all instances of the lattice type class. Less formally: Whenever <=, <, inf, sup form a lattice, so do >=, >, sup, inf.

How can I use this lemma?  Please point me to
There is just one example in HOL/Lattices for dual_lattice (in the proof of dual_distrib_lattice). But there are more examples for dual_semilattice, which is essentially the same concept. Lemmas less_supI1 and less_supI2 show how it is meant to use this lemma.

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
definition "inf_dual x y = dual (sup (undual x) (undual y))"

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.
The HOL/Lattice development and Lattices.thy are not compatible connected to each other. This is just another way of dealing with dual lattices (or symmetric instances of type classes, in general).

Let me briefly compare the two approaches:
On the one hand, Lattices.thy assumes that you mainly work with the normal type class instantiation. In case you need the dual, the recommended scheme is as in lemmas less_supI1 and less_supI2, i.e. interpret the local context that is associated with the type class with the operations instantiated for the dual lattice. Then, use these theorems to prove your goal. This works nicely in terms of tool support, but you have to do the local interpretation for every lemma that needs the dual. Moreover, you do not get a dual instance for type class instances.

On the other hand, the dual type in HOL/Lattice provides a type wrapper for dual lattices. In Isabelle, every type may instantiate a type class only once. Hence, you cannot have instantiations of a lattice and its dual for the same type. Instead, the type dual instantiates the lattice type classes for the dual lattice operations. Suppose you are working on a concrete type my_type which instantiates the lattice type class. Then, if you need the operations from the lattice, work in type my_type. If you need to work in the dual lattice, transfer your statement to type "my_type dual". An example how this can be used, is in HOL/Lattice/Lattices.thy in lemmas join_assoc and join_commute.

Hope this helps,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.