From 62292f3226b7703df008085db4114ae689faa892 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Fri, 13 Dec 2024 10:29:45 +1030
Subject: [PATCH] lib: add set_map_fst_filter_zip to Lib

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Lib.thy | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/lib/Lib.thy b/lib/Lib.thy
index e78997d520..1d677b7eba 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -2272,6 +2272,12 @@ lemma in_set_zipD:
   "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
   by (clarsimp simp add: set_zip)
 
+lemma set_map_fst_filter_zip:
+  "set (map fst (filter P (zip xs ys))) \<subseteq> set xs"
+  apply (induct xs, simp)
+  apply (case_tac ys; simp)
+  by (metis (mono_tags, lifting) image_Collect_subsetI insertI2 in_set_zipD)
+
 lemma map_zip_snd_take:
   "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)"
   apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp)