Re: [isabelle] How to State Class Duality?
your observation is correct, although there must be more to the first
approach than merely storing a theorem in a locale.
What the sublocale command currently does not give you is the ability
to map constants from the structure to constants of the dual. Say, to
map max to min and vice versa.
There is yet another approach, explored by Makarius in an early
experiment in HOL/Lattice/Orders.thy. There the functor that maps the
structure to its dual is a type constructor, which is also lifted to
the term level. I believe this dates back to times when axclasses
were the tool of choice for such formalisations.
Quoting Tjark Weber <webertj at in.tum.de>:
Suppose I want to show that every semigroup_mult (cf. HOL/Groups.thy) is
again a semigroup_mult when one considers the dual operation, i.e.,
\<lambda>x y. y * x. I am aware of two different approaches. First,
lemma (in semigroup_mult) dual_semigroup_mult:
"class.semigroup_mult (\<lambda>x y. y * x)"
sublocale semigroup_mult < dual!: semigroup_mult "\<lambda>x y. y * x"
My understanding is that the second approach automatically makes the
dual of all semigroup_mult facts available. Are there other differences
that I should be aware of? I noticed that the first approach is used in
a few places in HOL/Lattices.thy.
Many thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and