[isabelle-dev] code abbreviation for mapping over a fixed range

[Bertram Felgenhauer]

Hi Florian,
> > This email refers to the following commit:
> > 
> >   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
> > 
> >   code abbreviation for mapping over a fixed range
> > 
> > Is there a specific reason for this code equation:
> > 
> >   "map_range f (Suc n) = map_range f n @ [f n]"
> > 
> > It seems rather inefficient. Anyway, what's the purpose of "map_range".
> 
> the idea of map_range is to avoid building a list first and then mapping it.

Please don't forget about this.

The new definition actually causes *more* allocation than the original
one, except for very short lists, because every call of @ copies its
first argument. Note that the code equation for [_..<_] is

  lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"

which has no calls to @ at all; a corresponding code equation for
a fused "map_upt f i j = map f [i..<j]" would be

  "map_upt f i j = if i < j then f i # map_upt f (Suc i) j else []"

which could be used to define map_range:

  "map_range f n = map_upt f 0 n"

Cheers,

Bertram