Email Gateway (Aug 19 2022 at 15:23): Email Gateway (Aug 19 2022 at 15:23):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi all,
When playing with multisets, I stumbled upon the following annoying behavior. Formulas of the form "~ x :# M" are rewritten to "count M a = 0" due to the simp rule "not_gr0". This is easy to see once we look at how ":#" is introduced:
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == 0 < count M a"
The issue wouldn't arise if the definition were
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == count M a = 0"
instead. Apart from compatibility, is there a reason not to do so?
Thanks.
Jasmin
Email Gateway (Aug 19 2022 at 15:24):From: Tobias Nipkow <nipkow@in.tum.de>
On 12/08/2014 19:38, Jasmin Christian Blanchette wrote:
Hi all,
When playing with multisets, I stumbled upon the following annoying behavior. Formulas of the form "~ x :# M" are rewritten to "count M a = 0" due to the simp rule "not_gr0". This is easy to see once we look at how ":#" is introduced:
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == 0 < count M a"The issue wouldn't arise if the definition were
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == count M a = 0"
I hope you meant ~= ?
I believe I defined it that way because a long time ago linear arithmetic
preferred "> 0" over "~= 0". This is no longer the case and I don't think we
have a strong preference either way wrt proofs. Thus a change is likely to cause
few ill effects, although of course that needs to be checked.
Tobias
instead. Apart from compatibility, is there a reason not to do so?
Thanks.
Jasmin
Email Gateway (Aug 19 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A more radical answer would be
abbreviation Melem :: "'a => 'a multiset => bool"
("(_/ :# _)" [50, 51] 50)
where
"a :# M == a : set_of M"
i.e. reduce membership on multisets to membership on sets.
It is similar to membership on lists, and requires only a notion about
the functorial structure of multisets.
This also suggests a lemma [simp]:
"count M a = 0 <--> a \<notin> set_of M"
which seems to be absent from Multiset.thy
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:24):From: Tobias Nipkow <nipkow@in.tum.de>
There are variations. Hence this requires a clear design of which notions get
reduced to which, and a library that follows the design. Or at least an
empirical proof that some newly proposed design improves matters.
Tobias
Email Gateway (Aug 19 2022 at 15:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
There are variations. Hence this requires a clear design of which notions get
reduced to which, and a library that follows the design.
The design principle is simply to follow the established convention on
lists. Here we do not have any abbreviation for membership but simply write
x : set xs
Transferring this to multisets, we end up with
x : set_of M
for which you can argue that almost-well-established mathematical
notation exists also, hence the abbreviation
x :# M == x : set_of M
With the proposal
x :# M == not (count M x = 0)
you would end up with the problem of double negation (try »not (x :# m)«
mentally).
There is also a strong algebraic argument: membership abstracts over
structure (order) and repetition. This is what »set« does for lists,
and »set_of« for multisets (where structure anyway is irrelevant).
»count« does not abstract over anything.
Or at least an
empirical proof that some newly proposed design improves matters.
The simp rules surely need some refinement and augmentation, like
"count M x = 0 <--> not (x :# M)"
"x :# (M inter N) <--> x :# M && y :# N"
if not present yet.
But this is the usual iteration cycle of analysis and empirical checking.
Hope this makes things more explicit,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:25):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Florian,
Am 13.08.2014 um 20:35 schrieb Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>:
The design principle is simply to follow the established convention on
lists. Here we do not have any abbreviation for membership but simply writex : set xs
Transferring this to multisets, we end up with
x : set_of M
for which you can argue that almost-well-established mathematical
notation exists also, hence the abbreviationx :# M == x : set_of M
Good point. The design for "List", other parts of the library, and the BNF (co)datatypes, is in favor of "_ : set_of _" rather than "predicators" (?). It seems to have worked well and should probably be imitated. Apart from the fact that multisets are not a free datatype, they are otherwise very much like lists and should feel that way too (while keeping the set-like syntactic sugar).
With the proposal
x :# M == not (count M x = 0)
you would end up with the problem of double negation (try »not (x :# m)«
mentally).
My original proposal didn't have the double negation issue, but it had another blemish, as noted by Tobias. ;)
Hope this makes things more explicit,
Yes. In the coming weeks or months, Dmitriy and I should be making some contributions to the "Multiset" theory. This would be a good opportunity to clean it up, to the extend to which it can be done without breaking existing applications beyond repair.
Two more things:
You circulated privately some renaming proposals, with "_mset" as a fairly systematic suffix (no more "m" or "M" prefixes). This is also something we would look into.
There are currently two (provably identical) map functions -- the traditional "image_mset" and the Popescuesque "mmap". This needs to be consolidated.
Jasmin
Email Gateway (Aug 19 2022 at 15:32):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi René,
Thanks. I have just added them to my repository and pushed them to the testboard.
The IsaFoR project seems to have much more to offer in terms of multiset support. If you have other contributions or ideas, please let us know.
Incidentally, the refactoring Dmitriy and I (and Florian) have in mind will probably not happen in the immediate future. We're using multisets in a formalization that we would like to submit to the AFP, so we'd like it to work with both Isabelle2014 and the repository version (as much as possible). Once it's published, we'll start playing with the "Multiset" theory.
Incidentally, our formalization happens to be not too remote from IsaFoR thematically -- our multisets are clauses or collections of clauses in a formalized theorem prover. We'll probably need to talk. ;)
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 15:33):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
there's also a "copy" of Multiset (called Multiset_Extension) in the AFP
entry Well-Quasi-Orders. The point here was to have the multiset
extension of an arbitrary order (given as predicate of type "'a => 'a =>
bool") over a fixed carrier set (not a full type).
This theory is not polished at all, but maybe it contains something
useful. At some point I'll have to clean this up ...
cheers
chris
Email Gateway (Aug 19 2022 at 15:34):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Christian,
We did need a multiset extension of the multiset order itself, so Dmitriy had to develop similar stuff in our private "Multiset_More" theory. We need to look more closely into this, but a priori we are interested.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 15:34):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Christian,
We did need a multiset extension of the multiset order itself, so Dmitriy had to develop similar stuff in our private "Multiset_More" theory. We need to look more closely into this, but a priori we are interested.
Cheers,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC