# HG changeset patch
# User nipkow
# Date 1050524048 -7200
# Node ID b3ed67af04b8d4c12425f22cf471186c482bf0ee
# Parent  3c0a340be5143a8b8c8f3d71662da77cfdd1dcb8
Added take/dropWhile thms

diff -r 3c0a340be514 -r b3ed67af04b8 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Apr 15 12:55:31 2003 +0200
+++ b/src/HOL/List.thy	Wed Apr 16 22:14:08 2003 +0200
@@ -755,6 +755,14 @@
 
 declare take_Cons [simp del] and drop_Cons [simp del]
 
+lemma take_Suc_conv_app_nth:
+ "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
+apply(induct xs)
+ apply simp
+apply(case_tac i)
+apply auto
+done
+
 lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
 by (induct n) (auto, case_tac xs, auto)
 
@@ -887,6 +895,18 @@
 lemma set_take_whileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
 by (induct xs) (auto split: split_if_asm)
 
+lemma takeWhile_eq_all_conv[simp]:
+ "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
+by(induct xs, auto)
+
+lemma dropWhile_eq_Nil_conv[simp]:
+ "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
+by(induct xs, auto)
+
+lemma dropWhile_eq_Cons_conv:
+ "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
+by(induct xs, auto)
+
 
 subsection {* @{text zip} *}