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.