Re: [isabelle] How to State Class Duality?



Hi Tjark,

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.

Clemens


Quoting Tjark Weber <webertj at in.tum.de>:

Hi,

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)"
 sorry

Second,

 sublocale semigroup_mult < dual!: semigroup_mult "\<lambda>x y. y * x"
 sorry

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!

Tjark










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