# HG changeset patch
# User nipkow
# Date 1513161851 -3600
# Node ID 1fabca1c2199eea72b61d36b1b2c5a135c8178b3
# Parent  bea1258d9a27fc803fcee911dbd0e36082bdc34b
made arg_min_on definition

diff -r bea1258d9a27 -r 1fabca1c2199 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Dec 13 09:04:43 2017 +0100
+++ b/src/HOL/Lattices_Big.thy	Wed Dec 13 11:44:11 2017 +0100
@@ -832,8 +832,8 @@
 definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
 "arg_min f P = (SOME x. is_arg_min f P x)"
 
-abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
-"arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)"
+definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
 
 syntax
   "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
@@ -908,7 +908,7 @@
 
 lemma arg_min_SOME_Min:
   "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
-unfolding arg_min_def is_arg_min_linorder
+unfolding arg_min_on_def arg_min_def is_arg_min_linorder
 apply(rule arg_cong[where f = Eps])
 apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
 done
@@ -917,7 +917,7 @@
 assumes "finite S" "S \<noteq> {}"
 shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
 using ex_is_arg_min_if_finite[OF assms, of f]
-unfolding arg_min_def is_arg_min_def
+unfolding arg_min_on_def arg_min_def is_arg_min_def
 by(auto dest!: someI_ex)
 
 lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
@@ -940,8 +940,8 @@
 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)"
+definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
 
 syntax
   "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"