# HG changeset patch
# User nipkow
# Date 1741245406 -3600
# Node ID 3505a7b02fc26fd5abfc0497e8de5893029785b6
# Parent  fba16c509af09b52617e31178685e584c7b706e1
Additions by Peter Gammie

diff -r fba16c509af0 -r 3505a7b02fc2 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Library/Saturated.thy	Thu Mar 06 08:16:46 2025 +0100
@@ -129,7 +129,7 @@
     case True thus ?thesis by (simp add: sat_eq_iff)
   next
     case False thus ?thesis
-      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2)
+      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc)
   qed
 qed (simp_all add: sat_eq_iff mult.commute)
 
@@ -251,4 +251,48 @@
     by (auto simp: bot_sat_def)
 qed
 
+
+subsection \<open>Enumeration\<close>
+
+lemma inj_on_sat_of_nat:
+  shows "inj_on (of_nat :: nat \<Rightarrow> 'a::len sat) {0..<LENGTH('a)}"
+by (rule inj_onI) (simp add: sat_eq_iff)
+
+lemma UNIV_sat_eq_of_nat:
+  shows "(UNIV :: 'a::len sat set) = of_nat ` {0..LENGTH('a)}" (is "?lhs = ?rhs")
+proof -
+  have "x \<in> ?rhs" for x :: "'a sat"
+    by (simp add: image_eqI[where x="nat_of x"] sat_eq_iff)
+  then show ?thesis
+    by blast
+qed
+
+instantiation sat :: (len) enum
+begin
+
+definition enum_sat :: "'a sat list" where
+  "enum_sat = map of_nat [0..<Suc(LENGTH('a))]"
+
+definition enum_all_sat :: "('a sat \<Rightarrow> bool) \<Rightarrow> bool" where
+  "enum_all_sat = All"
+
+definition enum_ex_sat :: "('a sat \<Rightarrow> bool) \<Rightarrow> bool" where
+  "enum_ex_sat = Ex"
+
+instance
+proof intro_classes
+  show "UNIV = set (enum_class.enum :: 'a sat list)"
+    by (simp only: enum_sat_def UNIV_sat_eq_of_nat set_map flip: atLeastAtMost_upt)
+  show "distinct (enum_class.enum :: 'a sat list)"
+    by (clarsimp simp: enum_sat_def distinct_map inj_on_sat_of_nat sat_eq_iff)
+qed (simp_all add: enum_all_sat_def enum_ex_sat_def)
+
 end
+
+lemma enum_sat_code [code]:
+  fixes P :: "'a::len sat \<Rightarrow> bool"
+  shows "Enum.enum_all P \<longleftrightarrow> list_all P Enum.enum"
+    and "Enum.enum_ex P \<longleftrightarrow> list_ex P Enum.enum"
+by (simp_all add: enum_all_sat_def enum_ex_sat_def enum_UNIV list_all_iff list_ex_iff)
+
+end