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

```Thanks, Peter.

```
Now at least there's a nice way to input them, even if it needs more massaging. I'll examine this tomorrow.
```
```
Yes, the error with the simplification failing is my fault, I'm afraid. I had added xsymbol "#\<in>" for ":#" and somehow confused things. The simplification of "x :# multiset_of [a,b,x,d,e]" works just fine.
```
Sincerely,

Rafal Kolanski.

Peter Lammich wrote:
```
```Nice idea to add this syntax to Multisets, I'm also tired writing
{#a#}+{#b#}+...

I can only partially reproduce your error.
The problem seems to be the predefined syntax for the single-function
"{#_#}" in Multiset.thy.

The following works for me (at least in one direction):

In Multiset.thy, replace:

-  single :: "'a => 'a multiset"    ("{#_#}")

+   single :: "'a => 'a multiset"

syntax

"@multiset" :: "args => 'a multiset" ("{#(_)#}")

translations

"{# x, xs #}" == "single x + {#xs#}" (* Note that xs seems to be the syntactic rest of the argument list, not yet translated *)

"{# x #}" == "single x"

This works as far as "{# a,b,c #}" is correctly parsed as
"{#a#}+({#b#}+{#c#})", but the backward translations seems not to work, i.e.
{# a,b,c #} is output as "{#a#}+({#b#}+{#c#})", although it should be
output as "{# a,b,c #}". Any ideas ?

Regards,
Peter

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.