# Re: [isabelle] Operations over sets in Isabelle

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".
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.
cheers
peter
--
http://peteg.org/

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*