[isabelle] List.span

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? 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]

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



Attachment: Span.thy
Description: application/example

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