# HG changeset patch
# User nipkow
# Date 1495951660 -7200
# Node ID dec96cb3fbe0c185dec69316fffd71ea973248dd
# Parent  32b3feb6f9650044a81da9e7153ec86f6871af2d
removed LeastM; is now arg_min

diff -r 32b3feb6f965 -r dec96cb3fbe0 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sat May 27 22:52:08 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sun May 28 08:07:40 2017 +0200
@@ -63,6 +63,7 @@
 @{const Orderings.Least} & @{typeof Orderings.Least}\\
 @{const Orderings.min} & @{typeof Orderings.min}\\
 @{const Orderings.max} & @{typeof Orderings.max}\\
+@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
 @{const[source] top} & @{typeof Orderings.top}\\
 @{const[source] bot} & @{typeof Orderings.bot}\\
 @{const Orderings.mono} & @{typeof Orderings.mono}\\
@@ -78,6 +79,7 @@
 @{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
 @{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
+@{term "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\
 \end{supertabular}
 
 
@@ -410,6 +412,21 @@
 \end{supertabular}
 
 
+\section*{Lattices\_Big}
+
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+@{const Lattices_Big.Min} & @{typeof Lattices_Big.Min}\\
+@{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\
+@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+@{term "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\
+\end{supertabular}
+
+
 \section*{Groups\_Big}
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
diff -r 32b3feb6f965 -r dec96cb3fbe0 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat May 27 22:52:08 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun May 28 08:07:40 2017 +0200
@@ -523,64 +523,6 @@
   by (blast intro: someI)
 
 
-subsection \<open>Least value operator\<close>
-
-definition LeastM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
-  where "LeastM m P \<equiv> (SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y))"
-
-syntax
-  "_LeastM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("LEAST _ WRT _. _" [0, 4, 10] 10)
-translations
-  "LEAST x WRT m. P" \<rightleftharpoons> "CONST LeastM m (\<lambda>x. P)"
-
-lemma LeastMI2:
-  "P x \<Longrightarrow>
-    (\<And>y. P y \<Longrightarrow> m x \<le> m y) \<Longrightarrow>
-    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m x \<le> m y \<Longrightarrow> Q x) \<Longrightarrow>
-    Q (LeastM m P)"
-  apply (simp add: LeastM_def)
-  apply (rule someI2_ex)
-   apply blast
-  apply blast
-  done
-
-lemma LeastM_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = m k"
-  for m :: "_ \<Rightarrow> 'a::order"
-  apply (rule LeastMI2)
-    apply assumption
-   apply blast
-  apply (blast intro!: order_antisym)
-  done
-
-lemma wf_linord_ex_has_least:
-  "wf r \<Longrightarrow> \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>* \<Longrightarrow> P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
-  apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
-  apply (drule_tac x = "m ` Collect P" in spec)
-  apply force
-  done
-
-lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
-  for m :: "'a \<Rightarrow> nat"
-  apply (simp only: pred_nat_trancl_eq_le [symmetric])
-  apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
-   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
-  apply assumption
-  done
-
-lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> m y)"
-  for m :: "'a \<Rightarrow> nat"
-  apply (simp add: LeastM_def)
-  apply (rule someI_ex)
-  apply (erule ex_has_least_nat)
-  done
-
-lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
-
-lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> m x"
-  for m :: "'a \<Rightarrow> nat"
-  by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
-
-
 subsection \<open>Greatest value operator\<close>
 
 definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
diff -r 32b3feb6f965 -r dec96cb3fbe0 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sat May 27 22:52:08 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Sun May 28 08:07:40 2017 +0200
@@ -841,13 +841,27 @@
 done
 
 lemma arg_min_equality:
-  "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> f k \<le> f x) \<Longrightarrow> f (arg_min f P) = f k"
+  "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
   for f :: "_ \<Rightarrow> 'a::order"
 apply (rule arg_minI)
   apply assumption
  apply (simp add: less_le_not_le)
 by (metis le_less)
 
+lemma wf_linord_ex_has_least:
+  "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
+   \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
+apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
+apply (drule_tac x = "m ` Collect P" in spec)
+by force
+
+lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
+  for m :: "'a \<Rightarrow> nat"
+apply (simp only: pred_nat_trancl_eq_le [symmetric])
+apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
+ apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
+by assumption
+
 lemma arg_min_nat_lemma:
   "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
   for m :: "'a \<Rightarrow> nat"