[isabelle-dev] Explicit representation of multisets

[Tobias Nipkow]

Although I suggested we do this, and still think logically it is the right thing 
to do, I see one issue, the naming of insert#. The canonical name is 
insert_mset, but this leads to the rather lengthy "insert_mset x M" as opposed 
to the current "{#x#} + M". This would come up in all inductive proofs. If we 
want to mimic sets, it actually seems unavoidable...

Tobias

On 10/03/2016 10:53, Florian Haftmann wrote:
> Hi all,
>
> in recent private discussion the question was raised whether the
> explicit representation of multisets should follow that of sets.
>
> For sets, we have:
> 	{a, b, c} = insert a (insert b (insert c empty))
>
> For multisets, we currently have:
> 	{#a, b, c#} = single a + single b + single c
>
> But the following would also be possible:
> 	{#a, b, c#} = insert# a (insert# b (insert# c empty#))
>
> Is there any evidence that we should not attempt this?
>
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> 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: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160313/0ad9078d/attachment.bin>