combinator List.those;
simprule for case distinction on Option.map expression

--- a/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -162,6 +162,13 @@
 
 hide_const (open) find
 
+primrec those :: "'a option list \<Rightarrow> 'a list option"
+where
+"those [] = Some []" |
+"those (x # xs) = (case x of
+  None \<Rightarrow> None
+| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
+
 primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "remove1 x [] = []" |
 "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"

--- a/src/HOL/Option.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Option.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -101,6 +101,10 @@
   qed
 qed
 
+lemma option_case_map [simp]:
+  "option_case g h (Option.map f x) = option_case g (h \<circ> f) x"
+  by (cases x) simp_all
+
 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
 bind_lzero: "bind None f = None" |
 bind_lunit: "bind (Some x) f = f x"