Re: [isabelle] Isabelle 2016 RC1: multiset changes



Hi Bertram,


2016-01-20 15:52 GMT+01:00 Bertram Felgenhauer via Cl-isabelle-users <
cl-isabelle-users at 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
>
>
>


-- 
Mathias Fleury
MPI - INF



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