*To*: Peter Gammie <peteg42 at gmail.com>*Subject*: Re: [isabelle] Operations over sets in Isabelle*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 4 May 2010 07:46:24 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <9E395EDD-A4FC-4305-8579-2D81373F92FA@gmail.com>*References*: <228851272907913@web132.yandex.ru> <9E395EDD-A4FC-4305-8579-2D81373F92FA@gmail.com>*Sender*: huffman.brian.c at gmail.com

On Tue, May 4, 2010 at 12:52 AM, Peter Gammie <peteg42 at gmail.com> wrote: > On 04/05/2010, at 12:31 AM, grechukbogdan wrote: > >> Also, can I use the same notations “+” and “*”? If so, how? > > Quick answer: I think you can. Check out my "WorkerWrapper" AFP entry - Nats.thy. Roughly you want to define your operations and then instantiate the plus class (untested, but you get the idea I hope): > > types 'a NumSet = "'a set" > > definition > "add xs ys = { x + y | x y. x : xs /\ y : ys }" > > instantiation set :: (plus) plus > begin > definition plus_set_def[simp]: "xs + ys \<equiv> add xs ys" > instance .. > end > > The instantiation line says "for any type 'a that has a plus instance, define a plus instance for 'a set". Unfortunately this instantiation command won't work in any version of Isabelle since 2008. For the past few years now, the type "'a set" is merely an abbreviation for "'a => bool". You can define overloaded operations at this type, but to do so you must define them uniformly for all function types "'a => 'b". (You can require the result type 'b to be in the type class of your choosing.) There are some examples of such instantiations in HOL/Lattices.thy. Here's the definition for subtraction on functions; when the result type is "bool" it is the set difference operation, but it also defines subtraction pointwise for types like "'a => int", etc. instantiation "fun" :: (type, minus) minus begin definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)" instance .. end This also brings up the point that many of the operations you want to define for sets (like subtraction) might already be defined in a different way. > > There are a bunch of other classes that just overload syntax like this. You could get more serious and try to crank the algebraic ones too. If you want to use all the existing classes with their syntax, you could do it by defining your own copy of the "set" type constructor, like this: typedef 'a myset = "UNIV :: 'a set set" .. instantation myset :: (plus) plus begin ... The drawback is that you will now have to explicitly convert values back and forth between types "'a set" and "'a myset", using the Rep_myset and Abs_myset functions. (Although you could create nice and concise syntax for those too, if you wanted.) Another workaround is to forget about the type classes, and define new functions that use the same syntax as the old overloaded functions. For example: no_notation plus (infixl "+" 65) definition myplus :: "'a::plus set => 'a set => 'a set" (infixl "+" 65) where "A + B = {plus x y |x y. x : A & y : B}" (Note that you must now use the name "plus" to refer to the old "+", since "+" now means "myplus".) As a final alternative (although I really don't recommend this method) you could do like above, but skip the no_notation command; now you will have two constants, "plus" and "myplus", with the same syntax. Isabelle will print a warning message every time it parses the "+" syntax, but as long as only one parse tree is type-correct, it will accept the input. Hope this helps, - Brian

**Follow-Ups**:**Re: [isabelle] Operations over sets in Isabelle***From:*Tobias Nipkow

**References**:**[isabelle] Operations over sets in Isabelle***From:*grechukbogdan

**Re: [isabelle] Operations over sets in Isabelle***From:*Peter Gammie

- Previous by Date: Re: [isabelle] Help to Build Latest Isabelle Release?
- Next by Date: [isabelle] print modes
- Previous by Thread: Re: [isabelle] Operations over sets in Isabelle
- Next by Thread: Re: [isabelle] Operations over sets in Isabelle
- Cl-isabelle-users May 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