--- a/NEWS Mon Mar 20 15:01:12 2023 +0100
+++ b/NEWS Mon Mar 20 15:01:59 2023 +0100
@@ -66,6 +66,11 @@
* Theory "HOL.Finite_Set"
- Imported Relation instead of Product_Type, Sum_Type, and Fields.
Minor INCOMPATIBILITY.
+ - Added lemmas.
+ Finite_Set.bex_max_element
+ Finite_Set.bex_min_element
+ is_max_element_in_set_iff
+ is_min_element_in_set_iff
* Theory "HOL.Relation":
- Imported Product_Type, Sum_Type, and Fields instead of Finite_Set.
--- a/src/HOL/Finite_Set.thy Mon Mar 20 15:01:12 2023 +0100
+++ b/src/HOL/Finite_Set.thy Mon Mar 20 15:01:59 2023 +0100
@@ -2465,6 +2465,113 @@
qed
qed
+
+subsection \<open>Minimal and maximal elements of finite sets\<close>
+
+context begin
+
+qualified lemma
+ assumes "finite A" and "A \<noteq> {}" and "transp_on A R" and "asymp_on A R"
+ shows
+ bex_min_element: "\<exists>m \<in> A. \<forall>x \<in> A. x \<noteq> m \<longrightarrow> \<not> R x m" and
+ bex_max_element: "\<exists>m \<in> A. \<forall>x \<in> A. x \<noteq> m \<longrightarrow> \<not> R m x"
+ unfolding atomize_conj
+ using assms
+proof (induction A rule: finite_induct)
+ case empty
+ hence False
+ by simp
+ thus ?case ..
+next
+ case (insert a A')
+ show ?case
+ proof (cases "A' = {}")
+ case True
+ show ?thesis
+ proof (intro conjI bexI)
+ show "\<forall>x\<in>insert a A'. x \<noteq> a \<longrightarrow> \<not> R x a" and "\<forall>x\<in>insert a A'. x \<noteq> a \<longrightarrow> \<not> R a x"
+ using True by blast+
+ qed simp_all
+ next
+ case False
+ moreover have "transp_on A' R"
+ using insert.prems transp_on_subset by blast
+ moreover have "asymp_on A' R"
+ using insert.prems asymp_on_subset by blast
+ ultimately obtain min max where
+ "min \<in> A'" and "max \<in> A'" and
+ min_is_min: "\<forall>x\<in>A'. x \<noteq> min \<longrightarrow> \<not> R x min" and
+ max_is_max: "\<forall>x\<in>A'. x \<noteq> max \<longrightarrow> \<not> R max x"
+ using insert.IH by auto
+
+ show ?thesis
+ proof (rule conjI)
+ show "\<exists>min\<in>insert a A'. \<forall>x\<in>insert a A'. x \<noteq> min \<longrightarrow> \<not> R x min"
+ proof (cases "R a min")
+ case True
+ show ?thesis
+ proof (intro bexI ballI impI)
+ show "a \<in> insert a A'"
+ by simp
+ next
+ fix x
+ show "x \<in> insert a A' \<Longrightarrow> x \<noteq> a \<Longrightarrow> \<not> R x a"
+ using True \<open>min \<in> A'\<close> min_is_min[rule_format, of x] insert.prems(2,3)
+ by (auto dest: asymp_onD transp_onD)
+ qed
+ next
+ case False
+ show ?thesis
+ proof (rule bexI)
+ show "min \<in> insert a A'"
+ using \<open>min \<in> A'\<close> by auto
+ next
+ show "\<forall>x\<in>insert a A'. x \<noteq> min \<longrightarrow> \<not> R x min"
+ using False min_is_min by blast
+ qed
+ qed
+ next
+ show "\<exists>max\<in>insert a A'. \<forall>x\<in>insert a A'. x \<noteq> max \<longrightarrow> \<not> R max x"
+ proof (cases "R max a")
+ case True
+ show ?thesis
+ proof (intro bexI ballI impI)
+ show "a \<in> insert a A'"
+ by simp
+ next
+ fix x
+ show "x \<in> insert a A' \<Longrightarrow> x \<noteq> a \<Longrightarrow> \<not> R a x"
+ using True \<open>max \<in> A'\<close> max_is_max[rule_format, of x] insert.prems(2,3)
+ by (auto dest: asymp_onD transp_onD)
+ qed
+ next
+ case False
+ show ?thesis
+ proof (rule bexI)
+ show "max \<in> insert a A'"
+ using \<open>max \<in> A'\<close> by auto
+ next
+ show "\<forall>x\<in>insert a A'. x \<noteq> max \<longrightarrow> \<not> R max x"
+ using False max_is_max by blast
+ qed
+ qed
+ qed
+ qed
+qed
+
+end
+
+text \<open>The following alternative form might sometimes be easier to work with.\<close>
+
+lemma is_min_element_in_set_iff:
+ "asymp_on A R \<Longrightarrow> (\<forall>y \<in> A. y \<noteq> x \<longrightarrow> \<not> R y x) \<longleftrightarrow> (\<forall>y. R y x \<longrightarrow> y \<notin> A)"
+ by (auto dest: asymp_onD)
+
+lemma is_max_element_in_set_iff:
+ "asymp_on A R \<Longrightarrow> (\<forall>y \<in> A. y \<noteq> x \<longrightarrow> \<not> R x y) \<longleftrightarrow> (\<forall>y. R x y \<longrightarrow> y \<notin> A)"
+ by (auto dest: asymp_onD)
+
+
subsubsection \<open>Finite orders\<close>
context order