*To*: Tobias Nipkow <nipkow at in.tum.de>*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 13:52:34 +0100*Cc*: isabelle-users at cl.cam.ac.uk, Rafal Kolanski <rafalk at cse.unsw.edu.au>*In-reply-to*: <473C34EB.9070100@in.tum.de>*References*: <473BE428.8000008@cse.unsw.edu.au> <473C26FE.7060405@uni-muenster.de> <473C34EB.9070100@in.tum.de>*User-agent*: Thunderbird 1.5.0.9 (X11/20060911)

Tobias Nipkow wrote: > Peter, > > Your version has a critical pair: the internal term > "single a + single b" > can be rewritten first to > "{#a#} + single b" > at which point the other rule no longer applies. It should work if you > add one additional print translation, resulting in > > translations > "{#x, xs#}" == "single x + {#xs#}" > "{#x, xs#}" <= "{#x#} + {#xs#}" > "{#x#}" == "single x" > Also just the following two rules seem to work: "{#x, xs#}" == "{#x#} + {#xs#}" "{# x #}" == "single x" Thank you, Peter > 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. >>> >> >> > -- 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

**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

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

- Previous by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Date: [isabelle] CFA: 3rd Training School in Symbolic Computation
- 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