Re: [isabelle] Operations over sets in Isabelle



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





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