--- 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
--- 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"
--- 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
--- 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>