Email Gateway (Aug 18 2022 at 15:13): Email Gateway (Aug 18 2022 at 15:13):From: Peter Gammie <peteg42@gmail.com>
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
Email Gateway (Aug 18 2022 at 15:13):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, May 4, 2010 at 12:52 AM, Peter Gammie <peteg42@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 ..
endThe 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,
Email Gateway (Aug 18 2022 at 15:14):From: Tobias Nipkow <nipkow@in.tum.de>
Brian Huffman schrieb:
How about using a different symbol, eg:
definition setplus :: "'a::plus set => 'a set => 'a set" (infixl "{+}" 65)
where "A {+} B = {x + y |x y. x : A & y : B}"
You can still make use of type classes, eg
interpretation setplus_sg:
semigroup "op {+} :: 'a::semigroup_add set => 'a set => 'a set"
proof .... qed
which yields the generic thm setplus_sg.assoc that works on all
semigroups with +.
Tobias
Email Gateway (Aug 18 2022 at 15:17):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
I need to use (introduce?) operations over sets in Isabelle. For example, if operation “+” is defined for elements of sets, then we can define sum A+B as a set {c. c=a+b & a\in A & b \in B} (for example, sum of sets {a,b,c} and {d,e} will be set {a+d, a+e, b+d, b+e, c+d, c+e}). Similarly, if we can multiply elements of set by a constant c, then we can multiply any set A by this constant with definition cA={d. d=ca & a\in A}.
I need to use these operations in R^n, but they can be defined in a more general setting (in a vector space over any field).
The question is, if such operations are already defined in Isabelle? I do not want to redefine such basic concepts, if it already exists. But I cannot find something like this in the Library...
If not, is there any suggestions how exactly I should define this (for example, if such a definition exists in HOL light, it would be better to define them in Isabelle similarly).
Also, can I use the same notations “+” and “*”? If so, how?
Sincerely,
Bogdan Grechuk.
Email Gateway (Aug 18 2022 at 15:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Bogdan,
as far as I understand, you want to take the product of two sets and
then apply a binary operator on it. This can be done using the existing
image (`) and product operators (<*>), e.g.
(\<lambda>(a, b). a + b) ` (A <*> N)
form the sum of two sets.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:21):From: Jeremy Avigad <avigad@cmu.edu>
In fact, the operations are defined in the file "SetsAndFunctions" in
Library, with useful rewrite rules for appropriately general type classes.
Best wishes,
Jeremy
Florian Haftmann wrote:
Last updated: Apr 25 2024 at 01:08 UTC