[isabelle-dev] List Comprehension

[Christian Sternagel]

Dear all,

I was wondering about the reasons for implementing list comprehension as is:

Why is an optimized translation desirable at all? Isn't that just a 
matter of installing appropriate simplification rules afterwards.

The optimizations I could identify are:

1) If in "[e . p <- xs, ...]", p is just a variable, then use "(%p. e)" 
(instead of the default "(%x. case x of p => [e] | _ => [])". I guess 
the reason for handling this case in a special way is that something like

   term "(case x of y => a | z => b)"

results in

   Error in case expression:
   The following clauses are redundant (covered by preceding clauses):
   z => b

But why? Wouldn't it be less surprising (meaning, less special cases), 
if we could add redundant cases without obtaining an error?

2) Again, if p is a variable, translate "[e. p <- xs]" into "map (%p. e) 
xs" (instead of "concat (map (%x. case x of p => [e] | _ => []) xs)"). 
Isn't this optimization completely irrelevant inside the logic? What 
about applying it later by an appropriate simp rule or code equation?

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] | _ => [])")?

Thanks for any comments.

cheers

chris