--- a/NEWS Wed Jun 15 16:55:10 2022 +0200
+++ b/NEWS Mon Jun 20 11:06:33 2022 +0200
@@ -94,6 +94,9 @@
image_mset_filter_mset_swap
multp_image_mset_image_msetD
+* Theory "HOL-Library.Sublist":
+ - Added lemma map_mono_strict_suffix.
+
* Sledgehammer:
- Redesigned multithreading to provide more fine grained prover schedules.
The binary option 'slice' has been replaced by a numeric value 'slices'
--- a/src/HOL/Library/Sublist.thy Wed Jun 15 16:55:10 2022 +0200
+++ b/src/HOL/Library/Sublist.thy Mon Jun 20 11:06:33 2022 +0200
@@ -609,6 +609,9 @@
lemma map_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (map f xs) (map f ys)"
by (auto elim!: suffixE intro: suffixI)
+lemma map_mono_strict_suffix: "strict_suffix xs ys \<Longrightarrow> strict_suffix (map f xs) (map f ys)"
+ by (auto simp: strict_suffix_def suffix_def)
+
lemma filter_mono_suffix: "suffix xs ys \<Longrightarrow> suffix (filter P xs) (filter P ys)"
by (auto simp: suffix_def)