[isabelle-dev] Multiset membership revisited
florian.haftmann at informatik.tu-muenchen.de
Thu Feb 18 18:12:18 CET 2016
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev