[isabelle-dev] List Comprehension
c-sterna at jaist.ac.jp
Mon Aug 6 10:00:33 CEST 2012
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
> 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  it looked very similar; just
out of curiosity, was there any specific reason for adding the
optimization in changeset 24476:f7ad9fbbeeaa )
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 7756 bytes
Desc: not available
More information about the isabelle-dev