*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Notation issues trying to make Multiset more convenient*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 15 Nov 2007 12:37:01 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <473BE428.8000008@cse.unsw.edu.au>*References*: <473BE428.8000008@cse.unsw.edu.au>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

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"

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 itto 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-bracketsymbol.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 ina 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.

**References**:**[isabelle] Notation issues trying to make Multiset more convenient***From:*Rafal Kolanski

- Previous by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Previous by Thread: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Thread: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list