Re: [isabelle] List.span

Am 13/08/2013 08:51, schrieb Christian Sternagel:
> Dear all,
> maybe this was discussed already (I could not find such a discussion though).
> What is the reason for not having List.span in List.thy?

I didn't even know about it but see that it is part of the Haskell prelude.

> For code generation it
> might be nice to have a setup like
>   fun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where
>     "span P (x # xs) =
>       (if P x then let (ys, zs) = span P xs in (x # ys, zs)
>       else ([], x # xs))" |
>     "span _ [] = ([], [])"
>   lemma span_takeWhile_dropWhile [simp]:
>     "span P xs = (takeWhile P xs, dropWhile P xs)"
>     by (induct xs) simp_all
>   declare span.simps [simp del]

It should be the other way around: the lemma should be the definition and the
two fun-equations should be code lemmas.

Are you sure it is worth adding it? The only reason is that if you know about
span, you get more efficient code. But is is really more efficient? You only
traverse the list once, but there is a chance (depending on the compiler) that
you create as many intermediate pairs as there are list elements. But if
somebody feels strongly about it, I'm happy to add it.


> (see also the attached Span.thy) in the "standard library"?
> cheers
> chris

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