[isabelle-dev] Multiset membership revisited

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Feb 18 18:12:18 CET 2016

Hi all,

while working on material related to unique factorizations, I came again
across the multiset membership issue.

I would still be in favour of original proposal:

	‹a ∈# M› abbreviates ‹a ∈ set_mset M›
	‹a ∉# M› abbreviates ‹a ∉ set_mset M›

This is structurally similar to membership on lists ‹a ∈ set xs›.

I checked this against Multiset.thy, using an additional default simp
rule ‹count M a > 0 ↔ a ∈# M›. Except some very foundational proofs
involving »count« directly, proofs got indeed simpler, particularly
involving odd »add: set_mset_def« simplifications.

If there is no striking argument against I would like to pursue that

Note that I decided against making ‹count M a = 0 ↔ a ∉# M› a default
simp rule since the negation on the rhs makes it difficult to argue that
this is necessarily »simpler« than the lhs. I considered to formulate ‹a
∉# M› as abbreviation for ‹count M a = 0› but then ‹a ∉# M› would be
different from ‹¬ a ∈# M›, which is definitely not a good idea.



PGP available:

-------------- 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/20160218/06f484ac/attachment.asc>

More information about the isabelle-dev mailing list