Re: [isabelle] Isabelle 2016 RC1: multiset changes



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




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