# HG changeset patch
# User nipkow
# Date 1601996156 -7200
# Node ID b037517c815bad1b9002eadb8154993f334cd169
# Parent  698b58513fd1021d9ad5c6549183b3313cec57c8
added lemmas; internalized defn in class

diff -r 698b58513fd1 -r b037517c815b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Oct 05 22:53:40 2020 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Oct 06 16:55:56 2020 +0200
@@ -2057,6 +2057,58 @@
   qed
 qed
 
+subsubsection \<open>Finite orders\<close>
+
+context order
+begin
+
+lemma finite_has_maximal:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists> m \<in> A. \<forall> b \<in> A. m \<le> b \<longrightarrow> m = b"
+proof (induction rule: finite_psubset_induct)
+  case (psubset A)
+  from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by auto
+  let ?B = "{b \<in> A. a < b}"
+  show ?case
+  proof cases
+    assume "?B = {}"
+    hence "\<forall> b \<in> A. a \<le> b \<longrightarrow> a = b" using le_neq_trans by blast
+    thus ?thesis using \<open>a \<in> A\<close> by blast
+  next
+    assume "?B \<noteq> {}"
+    have "a \<notin> ?B" by auto
+    hence "?B \<subset> A" using \<open>a \<in> A\<close> by blast
+    from psubset.IH[OF this \<open>?B \<noteq> {}\<close>] show ?thesis using order.strict_trans2 by blast
+  qed
+qed
+
+lemma finite_has_maximal2:
+  "\<lbrakk> finite A; a \<in> A \<rbrakk> \<Longrightarrow> \<exists> m \<in> A. a \<le> m \<and> (\<forall> b \<in> A. m \<le> b \<longrightarrow> m = b)"
+using finite_has_maximal[of "{b \<in> A. a \<le> b}"] by fastforce
+
+lemma finite_has_minimal:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists> m \<in> A. \<forall> b \<in> A. b \<le> m \<longrightarrow> m = b"
+proof (induction rule: finite_psubset_induct)
+  case (psubset A)
+  from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by auto
+  let ?B = "{b \<in> A. b < a}"
+  show ?case
+  proof cases
+    assume "?B = {}"
+    hence "\<forall> b \<in> A. b \<le> a \<longrightarrow> a = b" using le_neq_trans by blast
+    thus ?thesis using \<open>a \<in> A\<close> by blast
+  next
+    assume "?B \<noteq> {}"
+    have "a \<notin> ?B" by auto
+    hence "?B \<subset> A" using \<open>a \<in> A\<close> by blast
+    from psubset.IH[OF this \<open>?B \<noteq> {}\<close>] show ?thesis using order.strict_trans1 by blast
+  qed
+qed
+
+lemma finite_has_minimal2:
+  "\<lbrakk> finite A; a \<in> A \<rbrakk> \<Longrightarrow> \<exists> m \<in> A. m \<le> a \<and> (\<forall> b \<in> A. b \<le> m \<longrightarrow> m = b)"
+using finite_has_minimal[of "{b \<in> A. b \<le> a}"] by fastforce
+
+end
 
 subsubsection \<open>Relating injectivity and surjectivity\<close>
 
diff -r 698b58513fd1 -r b037517c815b src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Oct 05 22:53:40 2020 +0100
+++ b/src/HOL/Lattices_Big.thy	Tue Oct 06 16:55:56 2020 +0200
@@ -868,17 +868,22 @@
 
 subsection \<open>Arg Min\<close>
 
-definition is_arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
+context ord
+begin
+
+definition is_arg_min :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))"
 
-definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+definition arg_min :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b" where
 "arg_min f P = (SOME x. is_arg_min f P x)"
 
-definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+definition arg_min_on :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b" where
 "arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
 
+end
+
 syntax
-  "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
+  "_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
     ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
 translations
   "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
@@ -980,17 +985,22 @@
 
 subsection \<open>Arg Max\<close>
 
-definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
+context ord
+begin
+
+definition is_arg_max :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))"
 
-definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+definition arg_max :: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'b" where
 "arg_max f P = (SOME x. is_arg_max f P x)"
 
-definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+definition arg_max_on :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b" where
 "arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
 
+end
+
 syntax
-  "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
+  "_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
     ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
 translations
   "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"