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



PS And remove the ("{#_#}") in the defn of "single". In case single is defined by constdefs in the version of Multiset you use, you can drop the CONST in the translation.

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.