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) apply (simp add: assms) 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 *)