# HG changeset patch
# User haftmann
# Date 1749136707 0
# Node ID b391142bd2d2934e36f8b3f74008dc9bdfbbb65a
# Parent  97b9ac57751e8f24dd4b8d783c6f2c7781518823
prefer already existing operation to calculate minimum

diff -r 97b9ac57751e -r b391142bd2d2 NEWS
--- a/NEWS	Wed Jun 04 19:43:13 2025 +0000
+++ b/NEWS	Thu Jun 05 15:18:27 2025 +0000
@@ -95,6 +95,9 @@
     const List.all_interval_nat List.all_interval_int
     discontinued in favour of a generic List.all_range
 
+    const List.Bleast
+    discontinued in favour of more concise List.Least as variant of Min
+
 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
diff -r 97b9ac57751e -r b391142bd2d2 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Jun 04 19:43:13 2025 +0000
+++ b/src/HOL/Lattices_Big.thy	Thu Jun 05 15:18:27 2025 +0000
@@ -813,6 +813,24 @@
   } from this [of "{a. P a}"] assms show ?thesis by simp
 qed
 
+lemma Greatest_Max:
+  assumes "finite {a. P a}" and "\<exists>a. P a"
+  shows "(GREATEST a. P a) = Max {a. P a}"
+proof -
+  { fix A :: "'a set"
+    assume A: "finite A" "A \<noteq> {}"
+    have "(GREATEST a. a \<in> A) = Max A"
+    using A proof (induct A rule: finite_ne_induct)
+      case singleton show ?case by (rule Greatest_equality) simp_all
+    next
+      case (insert a A)
+      have "(GREATEST b. b = a \<or> b \<in> A) = max a (GREATEST a. a \<in> A)"
+        by (auto intro!: Greatest_equality simp add: max_def not_le insert.hyps)
+      with insert show ?case by simp
+    qed
+  } from this [of "{a. P a}"] assms show ?thesis by simp
+qed
+
 lemma infinite_growing:
   assumes "X \<noteq> {}"
   assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
diff -r 97b9ac57751e -r b391142bd2d2 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Wed Jun 04 19:43:13 2025 +0000
+++ b/src/HOL/Library/RBT_Set.thy	Thu Jun 05 15:18:27 2025 +0000
@@ -33,7 +33,7 @@
   card the_elem Pow sum prod Product_Type.product Id_on
   Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin
   "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
-  sorted_list_of_set List.map_project List.Bleast]]
+  sorted_list_of_set List.map_project List.Least List.Greatest]]
 
 
 section \<open>Lemmas\<close>
@@ -769,34 +769,24 @@
 
 end
 
-lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
+lemma sorted_list_set [code]: "sorted_list_of_set (Set t) = RBT.keys t"
   by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
 
-lemma Bleast_code [code]:
-  "Bleast (Set t) P =
-    (case List.filter P (RBT.keys t) of
-      x # xs \<Rightarrow> x
-    | [] \<Rightarrow> abort_Bleast (Set t) P)"
-proof (cases "List.filter P (RBT.keys t)")
-  case Nil
-  thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
-next
-  case (Cons x ys)
-  have "(LEAST x. x \<in> Set t \<and> P x) = x"
-  proof (rule Least_equality)
-    show "x \<in> Set t \<and> P x"
-      using Cons[symmetric]
-      by (auto simp add: set_keys Cons_eq_filter_iff)
-    next
-      fix y
-      assume "y \<in> Set t \<and> P y"
-      then show "x \<le> y"
-        using Cons[symmetric]
-        by(auto simp add: set_keys Cons_eq_filter_iff)
-          (metis sorted_wrt.simps(2) sorted_append sorted_keys)
-  qed
-  thus ?thesis using Cons by (simp add: Bleast_def)
-qed
+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)
+  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)
+  apply (subst Greatest_Max)
+  using is_empty_Set
+    apply auto
+  done
 
 hide_const (open) RBT_Set.Set RBT_Set.Coset
 
diff -r 97b9ac57751e -r b391142bd2d2 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 04 19:43:13 2025 +0000
+++ b/src/HOL/List.thy	Thu Jun 05 15:18:27 2025 +0000
@@ -8099,40 +8099,6 @@
 end
 
 
-text \<open>Bounded \<open>LEAST\<close> operator.\<close>
-
-definition Bleast :: \<open>'a::ord set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a\<close>
-  where \<open>Bleast S P = (LEAST x. x \<in> S \<and> P x)\<close>
-
-declare Bleast_def [symmetric, code_unfold]
-
-definition abort_Bleast :: \<open>'a::ord set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a\<close>
-  where \<open>abort_Bleast S P = (LEAST x. x \<in> S \<and> P x)\<close>
-
-declare [[code abort: abort_Bleast]]
-
-lemma Bleast_code [code]:
-  \<open>Bleast (set xs) P = (case filter P (sort xs) of
-    x # xs \<Rightarrow> x |
-    [] \<Rightarrow> abort_Bleast (set xs) P)\<close>
-proof (cases "filter P (sort xs)")
-  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
-next
-  case (Cons x ys)
-  have "(LEAST x. x \<in> set xs \<and> P x) = x"
-  proof (rule Least_equality)
-    show "x \<in> set xs \<and> P x"
-      by (metis Cons Cons_eq_filter_iff in_set_conv_decomp set_sort)
-    next
-      fix y assume "y \<in> set xs \<and> P y"
-      hence "y \<in> set (filter P xs)" by auto
-      thus "x \<le> y"
-        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted_wrt.simps(2) sorted_sort)
-  qed
-  thus ?thesis using Cons by (simp add: Bleast_def)
-qed
-
-
 subsubsection \<open>Special implementations\<close>
 
 text \<open>
@@ -8345,6 +8311,45 @@
 lemma wf_code_set[code]: "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 Min_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>