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

Peter, Your version has a critical pair: the internal term "single a + single b" can be rewritten first to "{#a#} + single b"

translations "{#x, xs#}" == "single x + {#xs#}" "{#x, xs#}" <= "{#x#} + {#xs#}" "{#x#}" == "single x" Tobias 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" and then add: 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.

**Follow-Ups**:**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Peter Lammich

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

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Peter Lammich

- 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