# Re: [isabelle] Notation issues trying to make Multiset more convenient

```The following (due to Larry with a little tweak by me) does the job:

constdefs
cons :: "'a => 'a multiset => 'a multiset"
"cons a B == single a + B"

syntax
-- {* Multiset Enumeration *}
"@multiset" :: "args => 'a multiset"    ("{#(_)#}")

translations
"{#x, xs#}" == "cons x {#xs#}"
"{#x#}" == "CONST single x"

```
Most likely we'll add something like this in the near future, it is useful. The above formulation introduces an additional constant "cons", like "insert" for sets. A version without the constant I'll have to think about. Not quite sure which is better.
```
Tobias

Rafal Kolanski wrote:
```
```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.

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.