# HG changeset patch
# User nipkow
# Date 1607507505 -3600
# Node ID 7568a54aadcd9522993d4312beee74a5182d0668
# Parent  f0fa51227a235f95499550487677b2a8de5cf2b6
added lemmas

diff -r f0fa51227a23 -r 7568a54aadcd src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Dec 08 17:40:43 2020 +0100
+++ b/src/HOL/List.thy	Wed Dec 09 10:51:45 2020 +0100
@@ -2128,6 +2128,12 @@
 lemma drop_all [simp]: "length xs \<le> n \<Longrightarrow> drop n xs = []"
   by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
+lemma take_all_iff [simp]: "take n xs = xs \<longleftrightarrow> length xs \<le> n"
+by (metis length_take min.order_iff take_all)
+
+lemma drop_all_iff [simp]: "drop n xs = [] \<longleftrightarrow> length xs \<le> n"
+by (metis diff_is_0_eq drop_all length_drop list.size(3))
+
 lemma take_append [simp]:
   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
   by (induct n arbitrary: xs) (auto, case_tac xs, auto)