# HG changeset patch
# User haftmann
# Date 1752943315 -7200
# Node ID 8d1e295aab7080a8a1cc0ebd969372508c55bff7
# Parent  5d2a599f88af56a2b5e72e6d563c2d69716d8bb8
clarified name and status of auxiliary operation

diff -r 5d2a599f88af -r 8d1e295aab70 NEWS
--- a/NEWS	Thu Jul 17 21:06:22 2025 +0100
+++ b/NEWS	Sat Jul 19 18:41:55 2025 +0200
@@ -136,6 +136,9 @@
     const [List.]maps → List.maps
     thm maps_def → List.maps_eq [simp]
 
+    const [List.]map_project → Option.image_filter
+    thm map_project_def → Option.image_filter_eq
+
 The _def suffix for characteristic theorems is avoided to emphasize that these
 auxiliary operations are candidates for unfolding since they are variants
 of existing logical concepts. The [simp] declarations try to move the attention
diff -r 5d2a599f88af -r 8d1e295aab70 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu Jul 17 21:06:22 2025 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Sat Jul 19 18:41:55 2025 +0200
@@ -788,7 +788,15 @@
     apply auto
   done
 
-declare [[code drop: Set.can_select List.map_project Wellfounded.acc pred_of_set
+lemma [code]:
+  \<open>Option.these A = the ` Set.filter (Not \<circ> Option.is_none) A\<close>
+  by (fact Option.these_eq)
+
+lemma [code]:
+  \<open>Option.image_filter f A = Option.these (image f A)\<close>
+  by (fact Option.image_filter_eq)
+
+declare [[code drop: Set.can_select Wellfounded.acc pred_of_set
   \<open>Inf :: _ \<Rightarrow> 'a Predicate.pred\<close> \<open>Sup :: _ \<Rightarrow> 'a Predicate.pred\<close>]]
 
 hide_const (open) RBT_Set.Set RBT_Set.Coset
diff -r 5d2a599f88af -r 8d1e295aab70 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jul 17 21:06:22 2025 +0100
+++ b/src/HOL/List.thy	Sat Jul 19 18:41:55 2025 +0200
@@ -8461,14 +8461,15 @@
   "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
   by (simp_all add: Pow_insert Let_def)
 
-definition map_project :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a set \<Rightarrow> 'b set" where
-  "map_project f A = {b. \<exists> a \<in> A. f a = Some b}"
-
-lemma [code]:
-  "map_project f (set xs) = set (List.map_filter f xs)"
-  by (auto simp add: map_project_def map_filter_def image_def)
-
-hide_const (open) map_project
+lemma these_set_code [code]:
+  \<open>Option.these (set xs) = set (List.map_filter (\<lambda>x. x) xs)\<close>
+  by (simp add: Option.these_eq Option.is_none_def set_eq_iff map_filter_def)
+
+lemma image_filter_set_eq [code]:
+  \<open>Option.image_filter f (set xs) = set (List.map_filter f xs)\<close>
+  apply (simp add: Option.image_filter_eq these_set_code set_eq_iff flip: set_map)
+  apply (auto simp add: map_filter_def image_iff)
+  done
 
 lemma can_select_set_list_ex1 [code]:
   "Set.can_select P (set A) = list_ex1 P A"
@@ -8482,9 +8483,11 @@
   "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   by (auto simp add: Id_on_def)
 
-lemma [code]:
-  "R `` S = List.map_project (\<lambda>(x, y). if x \<in> S then Some y else None) R"
-  by (auto simp add: map_project_def split: prod.split if_split_asm)
+lemma Image_code [code]:
+  "R `` S = Option.image_filter (\<lambda>(x, y). if x \<in> S then Some y else None) R"
+  apply (simp add: Option.image_filter_eq case_prod_unfold Option.these_eq)
+  apply force
+  done
 
 lemma trancl_set_ntrancl [code]:
   "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
diff -r 5d2a599f88af -r 8d1e295aab70 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Thu Jul 17 21:06:22 2025 +0100
+++ b/src/HOL/Option.thy	Sat Jul 19 18:41:55 2025 +0200
@@ -277,6 +277,14 @@
 qualified definition these :: "'a option set \<Rightarrow> 'a set"
   where "these A = the ` {x \<in> A. x \<noteq> None}"
 
+qualified lemma these_eq [code]:
+  \<open>these A = the ` (Set.filter (Not \<circ> Option.is_none) A)\<close>
+  by (simp add: these_def Option.is_none_def)
+
+qualified lemma these_unfold:
+  \<open>these A = {x. \<exists>y \<in> A. y = Some x}\<close>
+  by (auto simp add: these_def set_eq_iff image_iff)
+
 lemma these_empty [simp]: "these {} = {}"
   by (simp add: these_def)
 
@@ -312,6 +320,9 @@
 lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   by (auto simp add: these_empty_eq)
 
+qualified definition image_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a set \<Rightarrow> 'b set"
+  where image_filter_eq: "image_filter f A = these (f ` A)"
+
 end
 
 lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"