# HG changeset patch
# User desharna
# Date 1655715993 -7200
# Node ID d32201f08e98721aa8fbceafe285d25c56ee4d7d
# Parent  5bba3516ddb5fa32d24879825c978ce785821623
added lemma map_mono_strict_suffix

diff -r 5bba3516ddb5 -r d32201f08e98 NEWS
--- 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'
diff -r 5bba3516ddb5 -r d32201f08e98 src/HOL/Library/Sublist.thy
--- 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)