*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Notation issues trying to make Multiset more convenient*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 15 Nov 2007 12:01:18 +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.9 (X11/20060911)

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. > -- Peter Lammich, Institut für Informatik Raum 715, Einsteinstrasse 62, 48149 Münster Mail: peter.lammich at uni-muenster.de Tel: 0251-83-32749 Mobil: 0163-5310380

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

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Tobias Nipkow

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

- Previous by Date: [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: [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