[isabelle] How to State Class Duality?



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.