# HG changeset patch
# User haftmann
# Date 1751994824 -7200
# Node ID 7ddae44464d41ac9c25046b06138bde8952d7a00
# Parent  71cbfcda66d6df63084fd2f07a0b3911e70879ef
moved to more appropriate theory

diff -r 71cbfcda66d6 -r 7ddae44464d4 NEWS
--- a/NEWS	Sun Jul 06 10:01:32 2025 +0200
+++ b/NEWS	Tue Jul 08 19:13:44 2025 +0200
@@ -115,7 +115,7 @@
     discontinued in favour of a generic List.all_range
 
     const List.Bleast
-    discontinued in favour of more concise List.Least as variant of Min
+    discontinued in favour of more concise Lattices_Big.Least
 
     const [List.]map_tailrec ~ List.map_tailrec
     thm List.map_tailrec_eq [simp]
diff -r 71cbfcda66d6 -r 7ddae44464d4 src/HOL/Lattices_Big.thy
--- 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
diff -r 71cbfcda66d6 -r 7ddae44464d4 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Sun Jul 06 10:01:32 2025 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Tue Jul 08 19:13:44 2025 +0200
@@ -773,16 +773,16 @@
   by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
 
 lemma Least_code [code]:
-  \<open>List.Least (Set t) = (if RBT.is_empty t then List.Least_abort {} else Min (Set t))\<close>
-  apply (auto simp add: List.Least_abort_def simp flip: empty_Set)
+  \<open>Lattices_Big.Least (Set t) = (if RBT.is_empty t then Lattices_Big.Least_abort {} else Min (Set t))\<close>
+  apply (auto simp add: Lattices_Big.Least_abort_def simp flip: empty_Set)
   apply (subst Least_Min)
   using is_empty_Set
     apply auto
   done
 
 lemma Greatest_code [code]:
-  \<open>List.Greatest (Set t) = (if RBT.is_empty t then List.Greatest_abort {} else Max (Set t))\<close>
-  apply (auto simp add: List.Greatest_abort_def simp flip: empty_Set)
+  \<open>Lattices_Big.Greatest (Set t) = (if RBT.is_empty t then Lattices_Big.Greatest_abort {} else Max (Set t))\<close>
+  apply (auto simp add: Lattices_Big.Greatest_abort_def simp flip: empty_Set)
   apply (subst Greatest_Max)
   using is_empty_Set
     apply auto
diff -r 71cbfcda66d6 -r 7ddae44464d4 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Jul 06 10:01:32 2025 +0200
+++ b/src/HOL/List.thy	Tue Jul 08 19:13:44 2025 +0200
@@ -8502,45 +8502,6 @@
   "wf_code (set xs) = acyclic (set xs)"
   unfolding wf_code_def using wf_set .
 
-text \<open>\<open>LEAST\<close> and \<open>GREATEST\<close> operator.\<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
-
 
 subsubsection \<open>Pretty lists\<close>