[isabelle-dev] List Comprehension

[Christian Sternagel]

On 08/06/2012 03:43 PM, Tobias Nipkow wrote:
> Am 06/08/2012 04:33, schrieb Christian Sternagel:
>> Why is an optimized translation desirable at all? Isn't that just a matter of
>> installing appropriate simplification rules afterwards.
>
> Why is it desirable to require simplification in such trivial cases? Isn't it
> just a matter installing appropriate translation functions or rules?
>
> Frankly I don't see that one method is superior to the other. If it can all be
> done with simp rules, and those rules don't have unpleasant global effects,
> sure, you can do it that way.
I get your point. I guess it depends on your perspective, if you are 
currently about to write a parse translation (as I was), it's nice if 
the implementation is easy/short. I was merely comparing the complexity of

   lemma concat_map_singleton [simp]:
     "concat (map (λx. [e x]) xs) = map (λx. e x) xs"
     by (induct xs) simp_all

(which is an existing lemma anyway) versus the implementation of lc_tr 
from List.thy.

> This is a question about case translations. I agree fully with their behaviour.
> See my recent support for the changed behavour of fun-definitions which brought
> them in line with case: such redundancy should not be accepted because it can
> confuse other readers no end.
I see. From that perspective I completely agree.

> [If one could distinguish user input from machine-generated text reliably, one could try and treat them differently.]
That would be nice.

>> Considering the above, why not implement list comprehension by the "easy"
>> translations that are present as comment in List.thy and just use a parse
>> translation for the hard case (i.e., generating "(%x. case x of p => [e] | _ =>
>> [])")?
>
> That may actually work. Try it out.
I did. The attached diff would work (meaning, I did a successful 
'isabelle build -g doc' afterwards). The resulting parse translation is 
a bit easier, but we lost the optimization.

(BTW: in changeset 24349:0dd8782fb02d [1] it looked very similar; just 
out of curiosity, was there any specific reason for adding the 
optimization in changeset 24476:f7ad9fbbeeaa [2])

[1] http://isabelle.in.tum.de/repos/isabelle/rev/0dd8782fb02d
[2] http://isabelle.in.tum.de/repos/isabelle/rev/f7ad9fbbeeaa

cheers

chris

-------------- next part --------------
A non-text attachment was scrubbed...
Name: listcompr.diff
Type: text/x-patch
Size: 7756 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120806/04e2a1f8/attachment-0002.bin>