# HG changeset patch
# User wenzelm
# Date 1494792436 -7200
# Node ID d081671d4a876b9a23bcc2d3d26b2ba795d5ecae
# Parent  8ee1799fb07674ec29500230c29aa08ed49415d8# Parent  30c2d78b5d3817d4a903ef4b375e6079bcf9abf8
merged

diff -r 30c2d78b5d38 -r d081671d4a87 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun May 14 22:04:52 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun May 14 22:07:16 2017 +0200
@@ -30,11 +30,14 @@
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
+definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
 
-abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv \<equiv> inv_into UNIV"
+lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
+by(simp add: inv_into_def)
+
+abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv \<equiv> inv_into UNIV"
 
 
 subsection \<open>Hilbert's Epsilon-operator\<close>
diff -r 30c2d78b5d38 -r d081671d4a87 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun May 14 22:04:52 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Sun May 14 22:07:16 2017 +0200
@@ -807,4 +807,39 @@
 
 end
 
+
+subsection \<open>Arg Min\<close>
+
+definition args_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+"args_min f S = {x \<in> S. \<not>(\<exists>y \<in> S. f y < f x)}"
+
+definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_min f S = (SOME x. x \<in> args_min f S)"
+
+lemma args_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
+shows "args_min f S = {x \<in> S. \<forall>y \<in> S. f x \<le> f y}"
+by(auto simp add: args_min_def)
+
+lemma arg_min_SOME_Min:
+  "finite S \<Longrightarrow> arg_min f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
+unfolding arg_min_def args_min_linorder
+apply(rule arg_cong[where f = Eps])
+apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
+done
+
+lemma arg_min_in: fixes f :: "'a \<Rightarrow> 'b :: linorder"
+shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> arg_min f S \<in> S"
+by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] inv_into_into)
+
+lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
+shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min f S) \<le> f y"
+by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
+
+lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order"
+shows "\<lbrakk> inj_on f S; a \<in> S; \<forall>y \<in> S. f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f S = a"
+apply(simp add: arg_min_def args_min_def)
+apply(rule someI2[of _ a])
+ apply (simp add: less_le_not_le)
+by (metis inj_on_eq_iff less_le)
+
 end