Re: [isabelle] lattices, typeclasses, notations?
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.
Now I want to work with the dual of a given lattice. In HOL/Lattices.thy I see
"class.lattice (op \<ge>) (op >) sup inf"
What does that mean?
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.
How can I use this lemma? Please point me to
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).
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.
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
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