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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
