Email Gateway (Aug 18 2022 at 16:39): Email Gateway (Aug 18 2022 at 16:39):From: Tjark Weber <webertj@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
Email Gateway (Aug 18 2022 at 16:41):From: Clemens Ballarin <ballarin@in.tum.de>
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@in.tum.de>:
Email Gateway (Aug 18 2022 at 16:41):From: Makarius <makarius@sketis.net>
Yes, it dates back to my version of the standard type class examples from
the early times around 1992/1993. Back then Tobias had a TYPES talk that
claimed that functors over type classes would not work. So I included
the dual constructor as a positive example when my version of axclasses
became available in 1994.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC