author nipkow Wed Dec 13 11:44:11 2017 +0100 (17 months ago) changeset 67169 1fabca1c2199 parent 67168 bea1258d9a27 child 67170 9bfe79084443
```     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"
```