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)
   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 *)