Email Gateway (Aug 18 2022 at 11:00): Email Gateway (Aug 18 2022 at 11:00):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi,
As you know, {a,b,c} works for sets, and [a,b,c] works for lists.
I'm in need of this sort of thing for Multisets, but I just can't get it
to work.
Firstly, syntax issues ... anything along the lines of:
translations
"{# x, xs #}" == "{# x #} + {# xs #}"
fails due to a parse error, even if I replace # with any non-bracket symbol.
On the other hand, bracket symbols work:
translations
"[{x, xs}]" == "{# x #} + {# xs #}"
but this redefines the "one set in a list" syntax.
What I can do is specify some unary operator for multiset_of and pass in
a list:
notation
multiset_of ("\<kappa> _" [40] 40)
but then I lose the nice simplification of:
lemma "a :# ({# b #} + {# a #})" by simp
as this won't work:
lemma "a #\<in> \<kappa>[b, a, c]" by simp
I am not sure how to proceed from here. Could you offer any advice?
Sincerely,
Rafal Kolanski.
Last updated: Nov 21 2024 at 12:39 UTC