# HG changeset patch
# User nipkow
# Date 1393607377 -3600
# Node ID fd31d0e70eb8959852579a98e3fb074ec200ba56
# Parent  f4e9517657b124c7937dbd8b265dc0a1c69183d1
added function "List.extract"

diff -r f4e9517657b1 -r fd31d0e70eb8 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 28 15:20:18 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 28 18:09:37 2014 +0100
@@ -182,6 +182,15 @@
 
 hide_const (open) find
 
+definition
+   "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
+where "extract P xs =
+  (case dropWhile (Not o P) xs of
+     [] \<Rightarrow> None |
+     y#ys \<Rightarrow> Some(takeWhile (Not o P) xs, y, ys))"
+
+hide_const (open) "extract"
+
 primrec those :: "'a option list \<Rightarrow> 'a list option"
 where
 "those [] = Some []" |
@@ -287,6 +296,8 @@
 @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
 @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
 @{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
+@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
+@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@@ -3648,6 +3659,34 @@
   by (induct xs) simp_all
 
 
+subsubsection {* @{const List.extract} *}
+
+lemma extract_None_iff: "List.extract P xs = None \<longleftrightarrow> \<not> (\<exists> x\<in>set xs. P x)"
+by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
+  (metis in_set_conv_decomp)
+
+lemma extract_SomeE:
+ "List.extract P xs = Some (ys, y, zs) \<Longrightarrow>
+  xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
+by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
+
+lemma extract_Some_iff:
+  "List.extract P xs = Some (ys, y, zs) \<longleftrightarrow>
+   xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
+by(auto simp: extract_def dropWhile_eq_Cons_conv dest: set_takeWhileD split: list.splits)
+
+lemma extract_Nil_code[code]: "List.extract P [] = None"
+by(simp add: extract_def)
+
+lemma extract_Cons_code[code]:
+  "List.extract P (x # xs) = (if P x then Some ([], x, xs) else
+   (case List.extract P xs of
+      None \<Rightarrow> None |
+      Some (ys, y, zs) \<Rightarrow> Some (x#ys, y, zs)))"
+by(auto simp add: extract_def split: list.splits)
+  (metis comp_def dropWhile_eq_Nil_conv list.distinct(1))
+
+
 subsubsection {* @{const remove1} *}
 
 lemma remove1_append: