[isabelle] How to State Class Duality?


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 MHonArc.