(takeWhile p xs) ++ (dropWhile p xs) = xs

takeWhile               :: (a -> Bool) -> [a] -> [a]
takeWhile _ []          =  []
takeWhile p (x:xs) 
            | p x       =  x : takeWhile p xs
            | otherwise =  []

(++) :: [a] -> [a] -> [a]
(++) []     ys = ys
(++) (x:xs) ys = x : xs ++ ys

dropWhile               :: (a -> Bool) -> [a] -> [a]
dropWhile _ []          =  []
dropWhile p xs@(x:xs')
            | p x       =  dropWhile p xs'
            | otherwise =  xs

theory takedrop
imports Main
begin
fun takeWhile :: "('a => bool) => 'a list => 'a list" where
  "takeWhile p [] = []" |
  "takeWhile p (x # xs) = (if p x then x # takeWhile p xs else [])"

fun dropWhile :: "('a => bool) => 'a list => 'a list" where
  "dropWhile p [] = []" |
  "dropWhile p (x # xs) = (if p x then dropWhile p xs else (x # xs))"

lemma "((takeWhile p xs) @ (dropWhile p xs)) = xs"
  apply(induct xs arbitrary: p)
  apply(auto)
done
end