Re: [isabelle-dev] Explicit representation of multisets
> 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...
With completion, it might actually be easier to type "insert_mset x M" than
"{#x#} + M". (The former is visually longer, for sure.)
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Explicit representation of multisets
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
[isabelle-dev] Explicit representation of multisets
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
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
