# HG changeset patch
# User haftmann
# Date 1756227546 -7200
# Node ID 9fbda8184ec70025926819640dbe117bb3b35c04
# Parent  308127f582bcf1b912d73f445573073e9b60ef02
preprocessing to execute bounded set comprehensions over tuples and triples

diff -r 308127f582bc -r 9fbda8184ec7 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 25 21:35:15 2025 +0200
+++ b/src/HOL/List.thy	Tue Aug 26 18:59:06 2025 +0200
@@ -8041,6 +8041,14 @@
   \<open>{x. List.member xs x \<and> P x} = Set.filter P (set xs)\<close>
   by simp
 
+qualified lemma Collect_pair_member [code_unfold, no_atp]: \<comment> \<open>make preprocessor setup confluent\<close>
+  \<open>{(x, y). List.member xs (x, y) \<and> P x y} = Set.filter (\<lambda>(x, y). P x y) (set xs)\<close>
+  by auto
+
+qualified lemma Collect_triple_member [code_unfold, no_atp]: \<comment> \<open>make preprocessor setup confluent\<close>
+  \<open>{(x, y, z). List.member xs (x, y, z) \<and> P x y z} = Set.filter (\<lambda>(x, y, z). P x y z) (set xs)\<close>
+  by auto 
+
 end
 
 lemma list_all_iff [code_abbrev]:
diff -r 308127f582bc -r 9fbda8184ec7 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Aug 25 21:35:15 2025 +0200
+++ b/src/HOL/Product_Type.thy	Tue Aug 26 18:59:06 2025 +0200
@@ -1328,6 +1328,23 @@
   using assms unfolding bij_betw_def inj_on_def by auto
 
 
+subsection \<open>Code generator setup for paired and tripled bounded set comprehension\<close>
+
+context
+begin
+
+qualified lemma paired_bounded_Collect_eq_filter [code_unfold, no_atp]:
+  \<open>{(x, y). (x, y) \<in> A \<and> P x y} = Set.filter (\<lambda>(x, y). P x y) A\<close>
+  by auto
+
+
+qualified lemma tripled_bounded_Collect_eq_filter [code_unfold, no_atp]:
+  \<open>{(x, y, z). (x, y, z) \<in> A \<and> P x y z} = Set.filter (\<lambda>(x, y, z). P x y z) A\<close>
+  by auto
+
+end
+
+
 subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close>
 
 ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>