# HG changeset patch
# User nipkow
# Date 1587549023 -7200
# Node ID ad91684444d717a457b5c06c9679d742d98ddc07
# Parent  3875815f59677fc7a62589b1ae135b71f908fbc5
added lemmas

diff -r 3875815f5967 -r ad91684444d7 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Apr 21 22:19:59 2020 +0200
+++ b/src/HOL/List.thy	Wed Apr 22 11:50:23 2020 +0200
@@ -2373,9 +2373,16 @@
   "(\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
   by (induct xs) auto
 
+lemma takeWhile_append:
+  "takeWhile P (xs @ ys) = (if \<forall>x\<in>set xs. P x then xs @ takeWhile P ys else takeWhile P xs)"
+using takeWhile_append1[of _ xs P ys] takeWhile_append2[of xs P ys] by auto
+
 lemma takeWhile_tail: "\<not> P x \<Longrightarrow> takeWhile P (xs @ (x#l)) = takeWhile P xs"
   by (induct xs) auto
 
+lemma takeWhile_eq_Nil_iff: "takeWhile P xs = [] \<longleftrightarrow> xs = [] \<or> \<not>P (hd xs)"
+by (cases xs) auto
+
 lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
   by (metis nth_append takeWhile_dropWhile_id)
 
@@ -2398,6 +2405,10 @@
   "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
   by (induct xs) auto
 
+lemma dropWhile_append:
+  "dropWhile P (xs @ ys) = (if \<forall>x\<in>set xs. P x then dropWhile P ys else dropWhile P xs @ ys)"
+using dropWhile_append1[of _ xs P ys] dropWhile_append2[of xs P ys] by auto
+
 lemma dropWhile_last:
   "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
   by (auto simp add: dropWhile_append3 in_set_conv_decomp)
@@ -2420,6 +2431,9 @@
   "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \<and> \<not> P y)"
   by(induct xs, auto)
 
+lemma dropWhile_eq_self_iff: "dropWhile P xs = xs \<longleftrightarrow> xs = [] \<or> \<not>P (hd xs)"
+by (cases xs) (auto simp: dropWhile_eq_Cons_conv)
+
 lemma distinct_takeWhile[simp]: "distinct xs \<Longrightarrow> distinct (takeWhile P xs)"
   by (induct xs) (auto dest: set_takeWhileD)
 
@@ -3925,6 +3939,9 @@
 lemma remdups_adj_set[simp]: "set (remdups_adj xs) = set xs"
 by (induct xs rule: remdups_adj.induct, simp_all)
 
+lemma last_remdups_adj [simp]: "last (remdups_adj xs) = last xs"
+  by (induction xs rule: remdups_adj.induct) auto
+
 lemma remdups_adj_Cons_alt[simp]: "x # tl (remdups_adj (x # xs)) = remdups_adj (x # xs)"
 by (induct xs rule: remdups_adj.induct, auto)
 
@@ -4313,6 +4330,14 @@
     by (induct n) auto
 qed simp
 
+lemma takeWhile_replicate[simp]:
+  "takeWhile P (replicate n x) = (if P x then replicate n x else [])"
+using takeWhile_eq_Nil_iff by fastforce
+
+lemma dropWhile_replicate[simp]:
+  "dropWhile P (replicate n x) = (if P x then [] else replicate n x)"
+using dropWhile_eq_self_iff by fastforce
+
 lemma replicate_length_filter:
   "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
   by (induct xs) auto