[isabelle-dev] Multiset insert

[Tobias Nipkow]

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.

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

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
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160727/acd99288/attachment.bin>