Re: [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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev