Added take/dropWhile thms
authornipkow
Wed Apr 16 22:14:08 2003 +0200 (2003-04-16)
changeset 13913b3ed67af04b8
parent 13912 3c0a340be514
child 13914 026866537fae
Added take/dropWhile thms
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Apr 15 12:55:31 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Apr 16 22:14:08 2003 +0200
     1.3 @@ -755,6 +755,14 @@
     1.4  
     1.5  declare take_Cons [simp del] and drop_Cons [simp del]
     1.6  
     1.7 +lemma take_Suc_conv_app_nth:
     1.8 + "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
     1.9 +apply(induct xs)
    1.10 + apply simp
    1.11 +apply(case_tac i)
    1.12 +apply auto
    1.13 +done
    1.14 +
    1.15  lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
    1.16  by (induct n) (auto, case_tac xs, auto)
    1.17  
    1.18 @@ -887,6 +895,18 @@
    1.19  lemma set_take_whileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
    1.20  by (induct xs) (auto split: split_if_asm)
    1.21  
    1.22 +lemma takeWhile_eq_all_conv[simp]:
    1.23 + "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
    1.24 +by(induct xs, auto)
    1.25 +
    1.26 +lemma dropWhile_eq_Nil_conv[simp]:
    1.27 + "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
    1.28 +by(induct xs, auto)
    1.29 +
    1.30 +lemma dropWhile_eq_Cons_conv:
    1.31 + "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
    1.32 +by(induct xs, auto)
    1.33 +
    1.34  
    1.35  subsection {* @{text zip} *}
    1.36