src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Mar 05 10:30:54 2021 +0100
+++ b/src/HOL/List.thy	Fri Mar 05 12:05:54 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>