# HG changeset patch
# User wenzelm
# Date 1607553012 -3600
# Node ID a7fa680d82774eae30750bea7ee7a628b0817574
# Parent  7568a54aadcd9522993d4312beee74a5182d0668# Parent  3f5e6da0868780b66d7d9004bb378b179cc11005
merged

diff -r 3f5e6da08687 -r a7fa680d8277 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Dec 09 22:07:14 2020 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Dec 09 23:30:12 2020 +0100
@@ -265,13 +265,13 @@
 
 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
    invh (del x t) \<and>
-   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
-    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
+   (color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and>
+   (color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
 by(induct x t rule: del.induct)
   (auto simp: inv_baldL inv_baldR inv_join dest!: neq_LeafD)
 
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
-by (metis delete_def rbt_def color_paint_Black inv_del invc2I invh_paint)
+by (metis delete_def rbt_def color_paint_Black inv_del invh_paint)
 
 text \<open>Overall correctness:\<close>
 
diff -r 3f5e6da08687 -r a7fa680d8277 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 09 22:07:14 2020 +0100
+++ b/src/HOL/List.thy	Wed Dec 09 23:30:12 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)