Re: [isabelle] Isabelle 2016 RC1: multiset changes



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




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