Email Gateway (Aug 22 2022 at 12:13): Email Gateway (Aug 22 2022 at 12:13):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
in commit f8a513fedb31, multiset inclusion was changed from an instance
of order to a set of custom orders. I'm wondering why this was done.
(This is not a complaint, but I didn't find any discussion about this.)
I noticed that the NEWS entry mentions that \<subset> and \<subseteq>
were changed to \<subset># and \<subseteq>#; I believe the former
should be #\<subset># and #\<subseteq>#.
Would it be possible to add abbreviations >#, >=# and \<ge># corresponding
to the existing (in Isabelle 2015) abbreviations >, >= and \<ge> for ord?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 12:14):From: Fleury Mathias <mathias.fleury12@gmail.com>
Hi Bertram,
2016-01-20 15:52 GMT+01:00 Bertram Felgenhauer via Cl-isabelle-users <
cl-isabelle-users@lists.cam.ac.uk>:
Hi,
in commit f8a513fedb31, multiset inclusion was changed from an instance
of order to a set of custom orders. I'm wondering why this was done.
(This is not a complaint, but I didn't find any discussion about this.)
There were some discussions 10 months ago:
http://fa.isabelle.narkive.com/Lv0NWbCa/isabelle-multiset-ordering-vs-subset-syntax
<http://fa.isabelle.narkive.com/Lv0NWbCa/isabelle-multiset-ordering-vs-subset-syntax>
I noticed that the NEWS entry mentions that \<subset> and \<subseteq>
were changed to \<subset># and \<subseteq>#; I believe the former
should be #\<subset># and #\<subseteq>#.
So far, there are two different orders over multisets: the multiset
inclusion (Isabelle2015: ⊂, Isabelle2016: ⊂#) and the multiset ordering
(since Isabelle2015: #⊂#). The long-term goal is to swap the symbols: ⊂
should be the multiset ordering and not as previously the multiset
inclusion. We did not want to swap the two ordering in a single release
(too hard for users).
Would it be possible to add abbreviations >#, >=# and \<ge># corresponding
to the existing (in Isabelle 2015) abbreviations >, >= and \<ge> for ord?
You can re-instantiate the multiset to be of sort ord (see for example
~~/src/HOL/UNITY/Follows.thy where this is done for the multiset ordering).
However, I do not think that introducing abbreviations would be a good idea
(issues would appear after the next release).
Cheers,
Mathias
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 12:14):From: Fleury Mathias <mathias.fleury12@gmail.com>
Hi Bertram,
I am sorry I misread your second question.
To be more clear about the symbols (in red the changes compared to previous year):
multiset inclusion multiset ordering
2014 < and ⊂ <# and ⊂#
2015 < and ⊂ #<# and #⊂#
2016 <# and ⊂# #<# and #⊂#
2016.1 <# and ⊂# < and ⊂ (expected)
So it is not a mistake in the NEWS file.
About your second question, it is an oversight: we completely forget the > symbols. Jasmin will add them soon (before the next RC).
Sorry about my misreading,
Mathias
Email Gateway (Aug 22 2022 at 12:14):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Matthias,
Thanks for your reply. I had not found the earlier discussion in my
search (I only checked back to May 2015; I should have dug a little
deeper). So the motivation for the change is to make the multiset
extension of an order on the elements the standard order for multisets.
I noticed that the NEWS entry mentions that \<subset> and \<subseteq>
were changed to \<subset># and \<subseteq>#; I believe the former
should be #\<subset># and #\<subseteq>#.
My mistake, \<subset># is just an alias for <#... so perhaps the former
two symbols should be < and \<ge>. The point is that \<subset> and
\<subseteq> do not work for multisets in Isabelle2015; they are
restricted to sets. This also applies to your next paragraph:
So far, there are two different orders over multisets: the multiset
inclusion (Isabelle2015: ⊂, Isabelle2016: ⊂#) and the multiset ordering
(since Isabelle2015: #⊂#). The long-term goal is to swap the symbols: ⊂
should be the multiset ordering and not as previously the multiset
inclusion. We did not want to swap the two ordering in a single release
(too hard for users).
Would it be possible to add abbreviations >#, >=# and \<ge># corresponding
to the existing (in Isabelle 2015) abbreviations >, >= and \<ge> for ord?You can re-instantiate the multiset to be of sort ord (see for example
~~/src/HOL/UNITY/Follows.thy where this is done for the multiset ordering).
However, I do not think that introducing abbreviations would be a good idea
(issues would appear after the next release).
What are those issues? As far as I understand, the relations <#, <=#
and \<le># will not be touched again. To be clear, I'm talking about
adding
abbreviation (input)
supseteq_mset (infix ">#" 50)
where "x ># y == y <# x"
etc.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 12:14):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Bertram,
I'll take over, together with Mathias, to avoid further confusion (hopefully). ;)
So the motivation for the change is to make the multiset extension of an order on the elements the standard order for multisets.
That's the main motivation, to allow nested multiset orders gracefully, among others. In addition, several people found the old (pre-Isabelle2014) notations confusing (especially \<subset># for the multiset order).
My mistake, \<subset># is just an alias for <#... so perhaps the former
two symbols should be < and \<ge>.
(We don't entirely understand the last part of this sentence. "Former" and "should be" can mean many things.)
The point is that \<subset> and \<subseteq> do not work for multisets in Isabelle2015;
We take this as meaning that the NEWS item is wrong. Indeed, it refers to some operators that don't exist in Isabelle2015. This will be fixed in the next release candidate.
You can re-instantiate the multiset to be of sort ord (see for example
~~/src/HOL/UNITY/Follows.thy where this is done for the multiset ordering).
However, I do not think that introducing abbreviations would be a good idea
(issues would appear after the next release).What are those issues? As far as I understand, the relations <#, <=#
and \<le># will not be touched again. To be clear, I'm talking about
adding
See Mathias's second email.
Unfortunately, his little table, which we had concocted together based on our recollection, was slightly wrong. Here is an updated one.
multiset inclusion multiset ordering
2014 < <# ⊂#
2015 ⊂# <# < #<# #⊂#
2016 ⊂# <# #<# #⊂#
2016-1 (expected) ⊂# (and <#?) <
I hope this clears up the confusion. One of our goals is that people who know what < and \<subset> mean for sets can reuse that knowledge with multisets, but with the usual # suffix.
Cheers,
Jasmin & Mathias
Email Gateway (Aug 22 2022 at 12:14):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Jasmin Blanchette wrote:
Thanks for the clarification, and also for adding the superset
versions of <# and ⊂# (in ad43b3ab06e4)!
Cheers,
Bertram
Last updated: Apr 30 2024 at 01:06 UTC