src/HOL/Lattices_Big.thy
changeset 67169 1fabca1c2199
parent 67036 783c901a62cb
child 67525 5d04d7bcd5f6
     1.1 --- a/src/HOL/Lattices_Big.thy	Wed Dec 13 09:04:43 2017 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Wed Dec 13 11:44:11 2017 +0100
     1.3 @@ -832,8 +832,8 @@
     1.4  definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
     1.5  "arg_min f P = (SOME x. is_arg_min f P x)"
     1.6  
     1.7 -abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
     1.8 -"arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)"
     1.9 +definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
    1.10 +"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
    1.11  
    1.12  syntax
    1.13    "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
    1.14 @@ -908,7 +908,7 @@
    1.15  
    1.16  lemma arg_min_SOME_Min:
    1.17    "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
    1.18 -unfolding arg_min_def is_arg_min_linorder
    1.19 +unfolding arg_min_on_def arg_min_def is_arg_min_linorder
    1.20  apply(rule arg_cong[where f = Eps])
    1.21  apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
    1.22  done
    1.23 @@ -917,7 +917,7 @@
    1.24  assumes "finite S" "S \<noteq> {}"
    1.25  shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
    1.26  using ex_is_arg_min_if_finite[OF assms, of f]
    1.27 -unfolding arg_min_def is_arg_min_def
    1.28 +unfolding arg_min_on_def arg_min_def is_arg_min_def
    1.29  by(auto dest!: someI_ex)
    1.30  
    1.31  lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
    1.32 @@ -940,8 +940,8 @@
    1.33  definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    1.34  "arg_max f P = (SOME x. is_arg_max f P x)"
    1.35  
    1.36 -abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
    1.37 -"arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)"
    1.38 +definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
    1.39 +"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
    1.40  
    1.41  syntax
    1.42    "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"