# HG changeset patch
# User haftmann
# Date 1746441760 -7200
# Node ID 700f9b01c9d9996fb0434fae6ed689f135d095ca
# Parent  43f4f9c5c6bdd2fcd6a3335ffebf77a87062d1e3
more theorems

diff -r 43f4f9c5c6bd -r 700f9b01c9d9 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun May 04 21:03:04 2025 +0100
+++ b/src/HOL/Map.thy	Mon May 05 12:42:40 2025 +0200
@@ -297,6 +297,10 @@
   "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
   by (induct xs) (auto simp: fun_eq_iff)
 
+lemma map_of_filter:
+  "map_of (filter (\<lambda>x. P (fst x)) xs) = map_of xs |` Collect P"
+  by (induct xs) (simp_all add: fun_eq_iff restrict_map_def)
+
 lemma dom_map_option:
   "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   by (simp add: dom_def)