--- 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
--- 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
--- 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)"
--- 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)"