# HG changeset patch
# User wenzelm
# Date 1614975998 -3600
# Node ID 3c5a7746ffa4b22590b1cd221c55c77e6f1ef6d2
# Parent  3fdb94d87e0e819044e99b5b49e8ac10fcac555b# Parent  f3378101f555d44005cbf49ef6534cc3d1c7928d
merged

diff -r f3378101f555 -r 3c5a7746ffa4 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Fri Mar 05 20:52:08 2021 +0100
+++ b/src/HOL/Library/Sublist.thy	Fri Mar 05 21:26:38 2021 +0100
@@ -138,6 +138,9 @@
 lemma take_is_prefix: "prefix (take n xs) xs"
   unfolding prefix_def by (metis append_take_drop_id)
 
+lemma takeWhile_is_prefix: "prefix (takeWhile P xs) xs"
+  unfolding prefix_def by (metis takeWhile_dropWhile_id)
+
 lemma prefixeq_butlast: "prefix (butlast xs) xs"
 by (simp add: butlast_conv_take take_is_prefix)
 
@@ -595,7 +598,10 @@
 by (auto simp: suffix_def)
 
 lemma suffix_drop: "suffix (drop n as) as"
-  unfolding suffix_def by (rule exI [where x = "take n as"]) simp
+  unfolding suffix_def by (metis append_take_drop_id)
+
+lemma suffix_dropWhile: "suffix (dropWhile P xs) xs"
+  unfolding suffix_def by (metis takeWhile_dropWhile_id)
 
 lemma suffix_take: "suffix xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
   by (auto elim!: suffixE)
@@ -1293,10 +1299,16 @@
   by (auto simp: sublist_def suffix_def intro: exI[of _ "[]"])
 
 lemma sublist_take [simp, intro]: "sublist (take n xs) xs"
-  by (rule prefix_imp_sublist) (simp_all add: take_is_prefix)
+  by (rule prefix_imp_sublist[OF take_is_prefix])
+
+lemma sublist_takeWhile [simp, intro]: "sublist (takeWhile P xs) xs"
+  by (rule prefix_imp_sublist[OF takeWhile_is_prefix])
 
 lemma sublist_drop [simp, intro]: "sublist (drop n xs) xs"
-  by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
+  by (rule suffix_imp_sublist[OF suffix_drop])
+
+lemma sublist_dropWhile [simp, intro]: "sublist (dropWhile P xs) xs"
+  by (rule suffix_imp_sublist[OF suffix_dropWhile])
     
 lemma sublist_tl [simp, intro]: "sublist (tl xs) xs"
   by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
@@ -1373,6 +1385,12 @@
     by (simp add: ys zs1 zs2)
 qed
 
+lemma sublist_list_all: "sublist xs ys \<Longrightarrow> list_all P ys \<Longrightarrow> list_all P xs"
+  by (auto simp: sublist_def)
+
+lemmas prefix_list_all = prefix_imp_sublist[THEN sublist_list_all]
+lemmas suffix_list_all = suffix_imp_sublist[THEN sublist_list_all]
+
 subsubsection \<open>\<open>sublists\<close>\<close>
 
 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
diff -r f3378101f555 -r 3c5a7746ffa4 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Mar 05 20:52:08 2021 +0100
+++ b/src/HOL/List.thy	Fri Mar 05 21:26:38 2021 +0100
@@ -2386,6 +2386,21 @@
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
 
+lemma list_all_take_drop_conv:
+  "list_all P (take n xs) \<and> list_all P (drop n xs) \<longleftrightarrow> list_all P xs"
+proof (induction xs arbitrary: n)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases n) simp_all
+qed
+
+lemmas list_all_takeI = list_all_take_drop_conv[THEN iffD2, THEN conjunct1]
+lemmas list_all_dropI = list_all_take_drop_conv[THEN iffD2, THEN conjunct2]
+lemmas list_all_take_dropD = conjI[THEN list_all_take_drop_conv[THEN iffD1]]
+
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
 
@@ -2574,6 +2589,14 @@
   "dropWhile P (dropWhile P xs) = dropWhile P xs"
   by (induct xs) auto
 
+lemma list_all_takeWhile_dropWhile_conv:
+  "list_all P (takeWhile Q xs) \<and> list_all P (dropWhile Q xs) \<longleftrightarrow> list_all P xs"
+  by (induction xs; simp)
+
+lemmas list_all_takeWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct1]
+lemmas list_all_dropWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct2]
+lemmas list_all_takeWhile_dropWhileD = conjI[THEN list_all_takeWhile_dropWhile_conv[THEN iffD1]]
+
 
 subsubsection \<open>\<^const>\<open>zip\<close>\<close>