# HG changeset patch
# User nipkow
# Date 1495972663 -7200
# Node ID 431024edc9cfccdc0ab2929429ea1d4e2d83ac85
# Parent  440fe0937b92a4884c79562291dfb3f5d6732893
introduced arg_max

diff -r 440fe0937b92 -r 431024edc9cf src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun May 28 11:32:15 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sun May 28 13:57:43 2017 +0200
@@ -79,7 +79,6 @@
 @{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}
 
 
@@ -419,12 +418,17 @@
 @{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\
 @{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
 @{const Lattices_Big.is_arg_min} & @{typeof Lattices_Big.is_arg_min}\\
+@{const Lattices_Big.arg_max} & @{typeof Lattices_Big.arg_max}\\
+@{const Lattices_Big.is_arg_max} & @{typeof Lattices_Big.is_arg_max}\\
+@{const Lattices_Big.Greatest} & @{typeof Lattices_Big.Greatest}\\
 \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)"}\\
+@{term "ARG_MAX f x. P"} & @{term[source]"arg_max f (\<lambda>x. P)"}\\
+@{term "GREATEST x. P"} & @{term[source]"Greatest (\<lambda>x. P)"}\\
 \end{supertabular}
 
 
diff -r 440fe0937b92 -r 431024edc9cf src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun May 28 11:32:15 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun May 28 13:57:43 2017 +0200
@@ -522,7 +522,7 @@
 lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
   by (blast intro: someI)
 
-
+(*
 subsection \<open>Greatest value operator\<close>
 
 definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
@@ -607,7 +607,7 @@
   apply (rule GreatestI)
    apply assumption+
   done
-
+*)
 
 subsection \<open>An aside: bounded accessible part\<close>
 
diff -r 440fe0937b92 -r 431024edc9cf src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun May 28 11:32:15 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Sun May 28 13:57:43 2017 +0200
@@ -915,4 +915,102 @@
  apply (simp add: less_le_not_le)
 by (metis inj_on_eq_iff less_le mem_Collect_eq)
 
+
+subsection \<open>Arg Max\<close>
+
+definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<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
+"arg_max f P = (SOME x. is_arg_max f P x)"
+
+abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)"
+
+syntax
+  "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
+    ("(3ARG'_MAX _ _./ _)" [0, 0, 10] 10)
+translations
+  "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
+
+lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
+shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))"
+by(auto simp add: is_arg_max_def)
+
+lemma arg_maxI:
+  "P x \<Longrightarrow>
+    (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
+    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
+    Q (arg_max f P)"
+apply (simp add: arg_max_def is_arg_max_def)
+apply (rule someI2_ex)
+ apply blast
+apply blast
+done
+
+lemma arg_max_equality:
+  "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
+  for f :: "_ \<Rightarrow> 'a::order"
+apply (rule arg_maxI [where f = f])
+  apply assumption
+ apply (simp add: less_le_not_le)
+by (metis le_less)
+
+lemma ex_has_greatest_nat_lemma:
+  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x) \<Longrightarrow> \<exists>y. P y \<and> \<not> f y < f k + n"
+  for f :: "'a \<Rightarrow> nat"
+by (induct n) (force simp: le_Suc_eq)+
+
+lemma ex_has_greatest_nat:
+  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
+  for f :: "'a \<Rightarrow> nat"
+apply (rule ccontr)
+apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma)
+  apply (subgoal_tac [3] "f k \<le> b")
+   apply auto
+done
+
+lemma arg_max_nat_lemma:
+  "\<lbrakk> P k;  \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
+  \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
+  for f :: "'a \<Rightarrow> nat"
+apply (simp add: arg_max_def is_arg_max_linorder)
+apply (rule someI_ex)
+apply (erule (1) ex_has_greatest_nat)
+done
+
+lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]
+
+lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
+  for f :: "'a \<Rightarrow> nat"
+by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
+
+
+text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
+
+(* LEAST ? *)
+definition Greatest :: "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "GREATEST " 10)
+where "Greatest \<equiv> arg_max (\<lambda>x. x)"
+
+lemma Greatest_equality:
+  "\<lbrakk> P k;  \<And>x. P x \<Longrightarrow> x \<le> k \<rbrakk> \<Longrightarrow> (Greatest P) = k"
+  for k :: "'a::order"
+apply (simp add: Greatest_def)
+apply (erule arg_max_equality)
+apply blast
+done
+
+lemma GreatestI: "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (Greatest P)"
+  for k :: nat
+unfolding Greatest_def by (rule arg_max_natI) auto
+
+lemma Greatest_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> x \<le> (Greatest P)"
+  for x :: nat
+unfolding Greatest_def by (rule arg_max_nat_le) auto
+
+lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (Greatest P)"
+apply (erule exE)
+apply (erule (1) GreatestI)
+done
+
 end
diff -r 440fe0937b92 -r 431024edc9cf src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Sun May 28 11:32:15 2017 +0200
+++ b/src/HOL/Library/Sublist.thy	Sun May 28 13:57:43 2017 +0200
@@ -284,7 +284,7 @@
 subsection \<open>Longest Common Prefix\<close>
 
 definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
-"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
+"Longest_common_prefix L = (ARG_MAX length ps. \<forall>xs \<in> L. prefix ps xs)"
 
 lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
   \<exists>ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
@@ -339,17 +339,17 @@
  "\<lbrakk> L \<noteq> {};  \<forall>xs \<in> L. prefix ps xs;
     \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
   \<Longrightarrow> Longest_common_prefix L = ps"
-unfolding Longest_common_prefix_def GreatestM_def
+unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
 by(rule some1_equality[OF Longest_common_prefix_unique]) auto
 
 lemma Longest_common_prefix_prefix:
   "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
-unfolding Longest_common_prefix_def GreatestM_def
+unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
 by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
 
 lemma Longest_common_prefix_longest:
   "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
-unfolding Longest_common_prefix_def GreatestM_def
+unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
 by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
 
 lemma Longest_common_prefix_max_prefix: