[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