--- 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 @ {}}
--- 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"
--- 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"