*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] How to State Class Duality?*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Tue, 14 Dec 2010 22:20:07 +0100*In-reply-to*: <1291817506.2360.47.camel@weber>*References*: <1291817506.2360.47.camel@weber>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

Hi Tjark,

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

**Follow-Ups**:**Re: [isabelle] How to State Class Duality?***From:*Makarius

**References**:**[isabelle] How to State Class Duality?***From:*Tjark Weber

- Previous by Date: [isabelle] Multiple equivalences
- Next by Date: [isabelle] Modifying Isabelle/ZF core?
- Previous by Thread: [isabelle] How to State Class Duality?
- Next by Thread: Re: [isabelle] How to State Class Duality?
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list