Email Gateway (Aug 18 2022 at 15:52): Email Gateway (Aug 18 2022 at 15:52):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
I have to prove that for n convex sets in an Euclidean space A_1 A_2 ,..., A_n we have
rel_interior (A_1 + A_2 + … + A_n ) = (rel_interior A_1 + rel_interior A_2 + … + rel_interior A_n )
(for this letter, it is not important what rel_interior is).
My first problem, is how to write this down conveniently. Notation for sum of TWO sets is defined in SetsAndFunctions.thy
definition
set_plus :: "('a::plus) set => 'a set => 'a set" (infixl "\oplus" 65) where
"A \oplus B == {c. EX a:A. EX b:B. c = a + b}"
Now I need to write it for n sets. Let I be finite index set. If I try
lemma test:
assumes "finite I"
assumes "!i:I. convex ((S i) :: ('n::euclidean_space) set)"
shows "setsum S I=..."
I have error “No type arity bool :: comm_monoid_add”. This is unpleasant: addition is defined for sets (see above), and setsum should be defined for any type in which addition is defined. Why I cannot use a convenient notation “setsum S I”? Can I correct this and make it work? Or should I introduce new definition for this? If so, do you have any suggestions how it should look like?
Next, I have already proved my lemma for two sets:
rel_interior (A \oplus B ) = (rel_interior A \oplus rel_interior B)
Also, I have lemma linear_setsum, stating that if for function f we have f(a+b)=f(a)+f(b), then we have f(a_1+...+a_n)=f(a_1)+...+f(a_n). Implication of this lemma would immediately finish the proof. And my feeling that it should work. The system should just recognize \oplus as a regular addition. How can I tell it to do so?
Sincerely,
Bogdan.
Email Gateway (Aug 18 2022 at 15:52):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
grechukbogdan wrote:
Well, you need to tell Isabelle that your type of sets of things is in
the class comm_monoid_add, thus:
instance set :: (comm_monoid_add) comm_monoid_add
Then you can do definitions such as:
consts
sss :: "('a => 'b::comm_monoid_add set)
=> 'a set => 'b::comm_monoid_add set"
defs (overloaded)
sss_def : "sss f S == setsum f S"
However I suspect that this won't work from (I think) Isabelle2008 onwards, there were messages at the time about the changes to the way the set type is defined. So try it on Isabelle<=2007
Jeremy
Email Gateway (Aug 18 2022 at 15:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Bogdan,
the SetsAndFunctions theory already contains (among others) the following:
interpretation set_comm_monoid_add: comm_monoid_add "op ⊕ ::
('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
I.e., the comm_monoid_add structure is interpreted on the set
operations, which gives you plenty of theorems:
find_theorems name: set_comm_monoid_add
A little bit unfortunate, the setsum on sets is represented as
"comm_monoid_add.setsum set_plus {0}" (*), but you can syntactically fix
this by introducing an abbreviation:
abbreviation "set_setsum ≡ comm_monoid_add.setsum set_plus {0}"
Now everything looks quite fine
find_theorems name: set_comm_monoid_add
If this abbreviation does not solve your issue, I can provide you with a
modified theory where set_setsum is a proper constant (this will be part
of the next Isabelle release).
Hope this helps,
Florian
(*) called a foundational term in Isabelle parlance
signature.asc
Last updated: Apr 23 2024 at 20:15 UTC