equal
deleted
inserted
replaced
835 abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where |
835 abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where |
836 "arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)" |
836 "arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)" |
837 |
837 |
838 syntax |
838 syntax |
839 "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" |
839 "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" |
840 ("(3ARG'_MIN _ _./ _)" [0, 0, 10] 10) |
840 ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10) |
841 translations |
841 translations |
842 "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)" |
842 "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)" |
843 |
843 |
844 lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" |
844 lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" |
845 shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))" |
845 shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))" |
943 abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where |
943 abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where |
944 "arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)" |
944 "arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)" |
945 |
945 |
946 syntax |
946 syntax |
947 "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" |
947 "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" |
948 ("(3ARG'_MAX _ _./ _)" [0, 0, 10] 10) |
948 ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10) |
949 translations |
949 translations |
950 "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)" |
950 "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)" |
951 |
951 |
952 lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" |
952 lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" |
953 shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))" |
953 shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))" |