[isabelle-dev] Explicit representation of multisets

[Florian Haftmann]

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160310/97a5d9fe/attachment.asc>