--- a/src/HOL/Lattices_Big.thy Sun Jul 06 10:01:32 2025 +0200
+++ b/src/HOL/Lattices_Big.thy Tue Jul 08 19:13:44 2025 +0200
@@ -923,6 +923,46 @@
using that by (auto simp add: disjnt_def) (use Max_less_iff in blast)
+subsection \<open>An aside: code generation for \<open>LEAST\<close> and \<open>GREATEST\<close>\<close>
+
+context
+begin
+
+qualified definition Least :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
+ where Least_eq [code_abbrev, simp]: \<open>Least S = (LEAST x. x \<in> S)\<close>
+
+qualified lemma Least_filter_eq [code_abbrev]:
+ \<open>Least (Set.filter P S) = (LEAST x. x \<in> S \<and> P x)\<close>
+ by simp
+
+qualified definition Least_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
+ where \<open>Least_abort = Least\<close>
+
+declare [[code abort: Least_abort]]
+
+qualified lemma Least_code [code]:
+ \<open>Least A = (if finite A \<longrightarrow> Set.is_empty A then Least_abort A else Min A)\<close>
+ using Least_Min [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Least_abort_def)
+
+qualified definition Greatest :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
+ where Greatest_eq [code_abbrev, simp]: \<open>Greatest S = (GREATEST x. x \<in> S)\<close>
+
+qualified lemma Greatest_filter_eq [code_abbrev]:
+ \<open>Greatest (Set.filter P S) = (GREATEST x. x \<in> S \<and> P x)\<close>
+ by simp
+
+qualified definition Greatest_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
+ where \<open>Greatest_abort = Greatest\<close>
+
+declare [[code abort: Greatest_abort]]
+
+qualified lemma Greatest_code [code]:
+ \<open>Greatest A = (if finite A \<longrightarrow> Set.is_empty A then Greatest_abort A else Max A)\<close>
+ using Greatest_Max [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Greatest_abort_def)
+
+end
+
+
subsection \<open>Arg Min\<close>
context ord