[isabelle-dev] Multiset insert

[Mathias Fleury]

> On 27 Jul 2016, at 08:00, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> No, we keep talking about it (internally), but nobody at TUM has done anything about it. It would be great if you want to take this on. It is potentially tedious because there are many existing uses of multisets.

Indeed, it will probably be tedious.


> Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read.

There was some discussion in March: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-March/006743.html>, but I don't see an explicit conclusion on the best name. 

I don't remember any other discussion.


Mathias

> 
> Tobias
> 
> 
> On 26/07/2016 13:59, Mathias Fleury wrote:
>> Hello all,
>> 
>> (Relaunching this nearly-one-and-a-half-years-old thread.)
>> 
>> 
>> Before I start working on it, has anyone already done some work towards adding insert_mset?
>> 
>> 
>> Thanks,
>> Mathias
>> 
>>> On 08 Apr 2015, at 11:12, Larry Paulson <lp15 at cam.ac.uk> wrote:
>>> 
>>> Sounds logical to me.
>>> Larry
>>> 
>>>> On 8 Apr 2015, at 08:13, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>>> 
>>>> Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and union. Although induction already has only two cases (empty and union with singleton), it would be nicer to have only two constructors, like for finite sets: empty and insert. In particular, this often avoids the use of ac_simps for union because representations are more canonical. The singleton constructor would be retained as an abbreviation for "insert_mset _ {#}" but "M + {#x#}" would be simplified to "insert_mset x M", like for sets.
>>>> 
>>>> Any views?
>>>> 
>>>> Tobias
>>>> 
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>> 
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160727/18b34e2d/attachment-0002.html>