[isabelle-dev] Multiset membership revisited

[Florian Haftmann]

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
further.

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.

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