# HG changeset patch
# User desharna
# Date 1679332890 -3600
# Node ID 51ed312cabeb724551994be0e50cf9ed74b03ede
# Parent  f35cbb4da88a69eb74ab5de9f270e24332656c0d
added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element

diff -r f35cbb4da88a -r 51ed312cabeb NEWS
--- a/NEWS	Mon Mar 20 15:02:17 2023 +0100
+++ b/NEWS	Mon Mar 20 18:21:30 2023 +0100
@@ -67,6 +67,8 @@
   - Imported Relation instead of Product_Type, Sum_Type, and Fields.
     Minor INCOMPATIBILITY.
   - Added lemmas.
+      Finite_Set.bex_greatest_element
+      Finite_Set.bex_least_element
       Finite_Set.bex_max_element
       Finite_Set.bex_min_element
       is_max_element_in_set_iff
diff -r f35cbb4da88a -r 51ed312cabeb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Mar 20 15:02:17 2023 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 20 18:21:30 2023 +0100
@@ -2571,6 +2571,103 @@
   "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)
 
+context begin
+
+qualified lemma
+  assumes "finite A" and "A \<noteq> {}" and "transp_on A R" and "totalp_on A R"
+  shows
+    bex_least_element: "\<exists>l \<in> A. \<forall>x \<in> A. x \<noteq> l \<longrightarrow> R l x" and
+    bex_greatest_element: "\<exists>g \<in> A. \<forall>x \<in> A. x \<noteq> g \<longrightarrow> R x g"
+  unfolding atomize_conj
+  using assms
+proof (induction A rule: finite_induct)
+  case empty
+  hence False by simp
+  thus ?case ..
+next
+  case (insert a A')
+
+  from insert.prems(2) have transp_on_A': "transp_on A' R"
+    by (auto intro: transp_onI dest: transp_onD)
+
+  from insert.prems(3) have
+    totalp_on_a_A'_raw: "\<forall>y \<in> A'. a \<noteq> y \<longrightarrow> R a y \<or> R y a" and
+    totalp_on_A': "totalp_on A' R"
+    by (simp_all add: totalp_on_def)
+
+  show ?case
+  proof (cases "A' = {}")
+    case True
+    thus ?thesis by simp
+  next
+    case False
+    then obtain least greatest where
+      "least \<in> A'" and least_of_A': "\<forall>x\<in>A'. x \<noteq> least \<longrightarrow> R least x" and
+      "greatest \<in> A'" and greatest_of_A': "\<forall>x\<in>A'. x \<noteq> greatest \<longrightarrow> R x greatest"
+      using insert.IH[OF _ transp_on_A' totalp_on_A'] by auto
+
+    show ?thesis
+    proof (rule conjI)
+      show "\<exists>l\<in>insert a A'. \<forall>x\<in>insert a A'. x \<noteq> l \<longrightarrow> R l x"
+      proof (cases "R a least")
+        case True
+        show ?thesis
+        proof (intro bexI ballI impI)
+          show "a \<in> insert a A'"
+            by simp
+        next
+          fix x
+          show "\<And>x. x \<in> insert a A' \<Longrightarrow> x \<noteq> a \<Longrightarrow> R a x"
+            using True \<open>least \<in> A'\<close> least_of_A'
+            using insert.prems(2)[THEN transp_onD, of a least]
+            by auto
+        qed
+      next
+        case False
+        show ?thesis
+        proof (intro bexI ballI impI)
+          show "least \<in> insert a A'"
+            using \<open>least \<in> A'\<close> by simp
+        next
+          fix x
+          show "x \<in> insert a A' \<Longrightarrow> x \<noteq> least \<Longrightarrow> R least x"
+            using False \<open>least \<in> A'\<close> least_of_A' totalp_on_a_A'_raw
+            by (cases "x = a") auto
+        qed
+      qed
+    next
+      show "\<exists>g \<in> insert a A'. \<forall>x \<in> insert a A'. x \<noteq> g \<longrightarrow> R x g"
+      proof (cases "R greatest a")
+        case True
+        show ?thesis
+        proof (intro bexI ballI impI)
+          show "a \<in> insert a A'"
+            by simp
+        next
+          fix x
+          show "\<And>x. x \<in> insert a A' \<Longrightarrow> x \<noteq> a \<Longrightarrow> R x a"
+            using True \<open>greatest \<in> A'\<close> greatest_of_A'
+            using insert.prems(2)[THEN transp_onD, of _ greatest a]
+            by auto
+        qed
+      next
+        case False
+        show ?thesis
+        proof (intro bexI ballI impI)
+          show "greatest \<in> insert a A'"
+            using \<open>greatest \<in> A'\<close> by simp
+        next
+          fix x
+          show "x \<in> insert a A' \<Longrightarrow> x \<noteq> greatest \<Longrightarrow> R x greatest"
+            using False \<open>greatest \<in> A'\<close> greatest_of_A' totalp_on_a_A'_raw
+            by (cases "x = a") auto
+        qed
+      qed
+    qed
+  qed
+qed
+
+end
 
 subsubsection \<open>Finite orders\<close>