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



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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.