# HG changeset patch # User desharna # Date 1614942354 -3600 # Node ID b867b436f37276ab22e9562084966b21e57d6b1d # Parent 10f5f5b880f4596fcf056e250b0fed361d61748f added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI diff -r 10f5f5b880f4 -r b867b436f372 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 \ size xs \ nth xs ` {0.. list_all P (drop n xs) \ 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 \\<^const>\takeWhile\ and \<^const>\dropWhile\\ @@ -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) \ list_all P (dropWhile Q xs) \ 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 \\<^const>\zip\\