Re: [isabelle] finite order allows maxima

> There are quite a few missing lemmas for arg_max that do exist for
> arg_min, otherwise I would have replied to just use arg_max to the
> original question.

Are these lemmas missing for any other reason than "nobody bothered
yet"? I happened to need the arg_max variants of those today, so I
adjusted some proofs:

theory Scratch

lemma ex_max_if_finite:
  "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x > (m::'a::order))"
by(induction rule: finite.induct) (auto intro: order.strict_trans)

lemma ex_is_arg_max_if_finite: fixes f :: "'a ⇒ 'b :: order"
shows "⟦ finite S; S ≠ {} ⟧ ⟹ ∃x. is_arg_max f (λx. x ∈ S) x"
unfolding is_arg_max_def
using ex_max_if_finite[of "f ` S"]
by auto

lemma arg_max_SOME_Max:
  "finite S ⟹ arg_max_on f S = (SOME y. y ∈ S ∧ f y = Max(f ` S))"
unfolding arg_max_on_def arg_max_def is_arg_max_linorder
apply(rule arg_cong[where f = Eps])
apply (auto simp: fun_eq_iff intro: Max_eqI[symmetric])

lemma arg_max_if_finite: fixes f :: "'a ⇒ 'b :: order"
assumes "finite S" "S ≠ {}"
shows  "arg_max_on f S ∈ S" and "¬(∃x∈S. f x > f (arg_max_on f S))"
using ex_is_arg_max_if_finite[OF assms, of f]
unfolding arg_max_on_def arg_max_def is_arg_max_def
by(auto dest!: someI_ex)

lemma arg_max_greatest: fixes f :: "'a ⇒ 'b :: linorder"
shows "⟦ finite S;  S ≠ {};  y ∈ S ⟧ ⟹ f(arg_max_on f S) ≥ f y"
by(simp add: arg_max_SOME_Max inv_into_def2[symmetric] f_inv_into_f)

lemma arg_max_inj_eq: fixes f :: "'a ⇒ 'b :: order"
shows "⟦ inj_on f {x. P x}; P a; ∀y. P y ⟶ f a ≥ f y ⟧ ⟹ arg_max f P = a"
apply(simp add: arg_max_def is_arg_max_def)
apply(rule someI2[of _ a])
 apply (simp add: less_le_not_le)
by (metis inj_on_eq_iff less_le mem_Collect_eq)

It might've been cleaner to prove these using the equivalent arg_min
theorems by defining an 'inverse' order, but I have no idea how to do

Jakub Kądziołka

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.