# HG changeset patch # User desharna # Date 1615287011 -3600 # Node ID 8a1c6c7909c991c61290ce2f4464230c9ad226ca # Parent 6a96e9406e5349f17e1f2cfcd07192c109cd50ae Backed out changeset b867b436f372 diff -r 6a96e9406e53 -r 8a1c6c7909c9 src/HOL/List.thy --- a/src/HOL/List.thy Sun Mar 07 08:26:02 2021 +0100 +++ b/src/HOL/List.thy Tue Mar 09 11:50:11 2021 +0100 @@ -2386,21 +2386,6 @@ 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\\ @@ -2589,14 +2574,6 @@ "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\\