Re: [isabelle] List.span
On 08/14/2013 04:08 PM, Tobias Nipkow wrote:
Am 13/08/2013 08:51, schrieb Christian Sternagel:
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.
No I'm not sure. I'm just guessing that since GHC uses this definition
of "span", it does make sense at least for Haskell (but of course you
are right about it not making a big difference for efficiency).
Moreover, I have no strong opinion about adding "span" (I just stumbled
across it, since we reinvented a specialized variant of "span" for
"string"s in IsaFoR and I recalled "span" from the Haskell Prelude).
It is also thinkable to set up the code generator such that
"(takeWhile P xs, dropWhile P xs)" is replaced by "span" (for Haskell)
then the user does not have to know about it.
One (tiny) pro is that "span P xs" is shorter to type than "(takeWhile P
xs, dropWhile P xs)". I'm not sure how often this pattern occurs in
actual formalizations though.
This archive was generated by a fusion of
Pipermail (Mailman edition) and