Theory Misc

(* Title:     Parser_Monad
   Author:    Christian Sternagel
   Author:    René Thiemann
*)

section ‹More material on parsing›

theory Misc
  imports Main
begin

definition span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list"
  where [simp]: "span P xs = (takeWhile P xs, dropWhile P xs)"

lemma span_code [code]:
  "span P [] = ([], [])"
  "span P (x # xs) =
    (if P x then let (ys, zs) = span P xs in (x # ys, zs) else ([], x # xs))"
  by simp_all

definition splitter :: "char list ⇒ string ⇒ string × string"
where
  [code_unfold]: "splitter cs s = span (λc. c ∈ set cs) s"

end