# Theory Auxiliary

```theory Auxiliary
imports Main "HOL-Library.Extended_Nonnegative_Real"
begin

section ‹Auxiliary Material›

context
fixes S :: "'s set"
assumes "finite S"
begin

lemma Max_image_commute:
"(MAX x ∈ S. MAX y ∈ S. f x y) = (MAX y ∈ S. MAX x ∈ S. f x y)"
proof (rule Max_eq_if, goal_cases)
case 3
{ fix a assume "a ∈ S"
with Max_in[OF finite_imageI[OF ‹finite S›], of "f a"] have "Max (f a ` S) ∈ f a ` S"
by auto
then obtain b where "f a b = Max (f a ` S)" "b ∈ S"
by auto
from ‹a ∈ S› have "f a b ≤ (MAX a ∈ S. f a b)"
by (auto intro: Max_ge finite_imageI[OF ‹finite S›])
with ‹f a b = _› ‹b ∈ S› have "∃b∈S. Max (f a ` S) ≤ (MAX a ∈ S. f a b)"
by auto
}
then show ?case
by auto
next
case 4
{ fix b assume "b ∈ S"
with Max_in[OF finite_imageI[OF ‹finite S›], of "λ a. f a b"] have
"(MAX a ∈ S. f a b) ∈ (λa. f a b) ` S"
by auto
then obtain a where "f a b = (MAX a ∈ S. f a b)" "a ∈ S"
by auto
from ‹b ∈ S› have "f a b ≤ Max (f a ` S)"
by (auto intro: Max_ge finite_imageI[OF ‹finite S›])
with ‹f a b = _› ‹a ∈ S› have "∃a∈S. (MAX a ∈ S. f a b) ≤ Max (f a ` S)"
by auto
}
then show ?case
by auto
qed (use ‹finite S› in auto)

lemma Max_image_left_mult:
"(MAX x ∈ S. c * f x) = (c :: ennreal) * (MAX x ∈ S. f x)" if "S ≠ {}"
apply (rule Max_eqI)
subgoal
using ‹finite S› by auto
subgoal for y
using ‹finite S› by (auto intro: mult_left_mono)
subgoal
using Max_in[OF finite_imageI[OF ‹finite S›], of f] ‹S ≠ {}› by auto
done

end (* Finite set *)

lemma Max_to_image:
"Max {f t | t. t ∈ S} = Max (f ` S)"
by (rule arg_cong[where f = Max]) auto

lemma Max_to_image2:
"Max {f t | t. P t} = Max (f ` {t. P t})"
by (rule arg_cong[where f = Max]) auto

lemma Max_image_cong:
"Max (f ` S) = Max (g ` T)" if "S = T" "⋀x. x ∈ T ⟹ f x = g x"
by (intro arg_cong[where f = Max] image_cong[OF that])

lemma Max_image_cong_simp:
"Max (f ` S) = Max (g ` T)" if "S = T" "⋀x. x ∈ T =simp=> f x = g x"
using Max_image_cong[OF that[unfolded simp_implies_def]] .

lemma Max_eq_image_if:
assumes
"finite S" "finite T" "∀x ∈ S. ∃y ∈ T. f x ≤ g y" "∀x ∈ T. ∃y ∈ S. g x ≤ f y"
shows "Max (f ` S) = Max (g ` T)"
using assms by (auto intro: Max_eq_if)

theorem Max_in_image:
assumes "finite A" and "A ≠ {}"
obtains x where "x ∈ A" and "Max (f ` A) = f x"
proof -
from Max_in[of "f ` A"] assms have "Max (f ` A) ∈ f ` A"
by auto
then show ?thesis
by (auto intro: that)
qed

lemma Max_ge_image:
"Max (f ` S) ≥ f x" if "finite S" "x ∈ S"
using that by (auto intro: Max_ge)

lemma Max_image_pair:
assumes "finite S" "finite T" "T ≠ {}"
shows "(MAX s ∈ S. MAX t ∈ T. f s t) = (MAX (s, t) ∈ S × T. f s t)"
proof ((rule Max_eq_image_if; clarsimp?), goal_cases)
case (3 x)
from ‹finite T› ‹T ≠ {}› obtain y where "y ∈ T" and "Max (f x ` T) = f x y"
by (rule Max_in_image)
with ‹x ∈ S› show ?case
by auto
next
case (4 a b)
with ‹finite T› show ?case
by force
qed (use assms in auto)

fun argmax where
"argmax f (x # xs) =
List.fold (λ a (b, v). let w = f a in if w > v then (a, w) else (b, v)) xs (x, f x)"

lemma list_cases:
assumes "xs = [] ⟹ P []"
and "⋀ x. xs = [x] ⟹ P [x]"
and "⋀ x y ys. xs = (x # y # ys) ⟹ P (x # y # ys)"
shows "P xs"
apply (cases xs)
subgoal for y ys
by (cases ys; simp add: assms)
done

lemma argmax:
assumes "xs ≠ []"
shows
"fst (argmax f xs) ∈ set xs" (is "?A")
"f (fst (argmax f xs)) = snd (argmax f xs)" (is "?B")
"snd (argmax f xs) = (MAX x ∈ set xs. f x)" (is "?C")
proof -
let ?f = "λ a (b, v). let w = f a in if w > v then (a, w) else (b, v)"
have "fst (List.fold ?f xs (x, f x)) ∈ {x} ∪ set xs" if "xs ≠ []" for x xs
using that by (induction xs arbitrary: x rule: list_nonempty_induct)(auto simp: Let_def max_def)
with ‹xs ≠ []› show ?A
by (cases xs rule: list_cases; fastforce)
have "f (fst (List.fold ?f xs (x, f x))) = snd (List.fold ?f xs (x, f x))" if "xs ≠ []" for x xs
using that by (induction xs arbitrary: x rule: list_nonempty_induct)(auto simp: Let_def max_def)
with ‹xs ≠ []› show ?B
by (cases xs rule: list_cases; fastforce)
have "snd (List.fold ?f xs (x, f x)) = (MAX x ∈ {x} ∪ set xs. f x)"if "xs ≠ []" for x xs
using that by (induction xs arbitrary: x rule: list_nonempty_induct)(auto simp: Let_def max_def)
with ‹xs ≠ []› show ?C
by (cases xs rule: list_cases; fastforce)
qed

end (* Theory *)```