theory Max

imports Main

begin

section {* Some generic facts about Max *}

lemma Max_insert:

  assumes "finite B"

  and  "B \<noteq> {}"

  shows "Max ({x} \<union> B) = max x (Max B)"

using assms by (simp add: Lattices_Big.Max.insert)

lemma Max_Union:

  assumes fc: "finite C"

  and ne: "C \<noteq> {}"

  and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"

  shows "Max (\<Union>C) = Max (Max ` C)"

using assms

proof(induct rule: finite_induct)

  case (insert x F)

  assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"

    and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"

  show ?case (is "?L = ?R")

  proof(cases "F = {}")

    case False

    from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp

    also have "\<dots> = max (Max x) (Max(\<Union> F))"

    proof(rule Max_Un)

      from h[of x] show "finite x" by auto

    next

      from h[of x] show "x \<noteq> {}" by auto

    next

      show "finite (\<Union>F)"

        by (metis (full_types) finite_Union h insert.hyps(1) insertCI)

    next

      from False and h show "\<Union>F \<noteq> {}" by auto

    qed

    also have "\<dots> = ?R"

    proof -

      have "?R = Max (Max ` ({x} \<union> F))" by simp

      also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp

      also have "\<dots> = max (Max x) (Max (\<Union>F))"

      proof -

        have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"

        proof(rule Max_Un)

          show "finite {Max x}" by simp

        next

          show "{Max x} \<noteq> {}" by simp

        next

          from insert show "finite (Max ` F)" by auto

        next

          from False show "Max ` F \<noteq> {}" by auto

        qed

        moreover have "Max {Max x} = Max x" by simp

        moreover have "Max (\<Union>F) = Max (Max ` F)"

        proof(rule ih)

          show "F \<noteq> {}" by fact

        next

          from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"

            by auto

        qed

        ultimately show ?thesis by auto

      qed

      finally show ?thesis by simp

    qed

    finally show ?thesis by simp

  next

    case True

    thus ?thesis by auto

  qed

next

  case empty

  assume "{} \<noteq> {}" show ?case by auto

qed

lemma Max_fg_mono:

  assumes "finite A"

  and "\<forall> a \<in> A. f a \<le> g a"

  shows "Max (f ` A) \<le> Max (g ` A)"

proof(cases "A = {}")

  case True

  thus ?thesis by auto

next

  case False

  show ?thesis

  proof(rule Max.boundedI)

    from assms show "finite (f ` A)" by auto

  next

    from False show "f ` A \<noteq> {}" by auto

  next

    fix fa

    assume "fa \<in> f ` A"

    then obtain a where h_fa: "a \<in> A" "fa = f a" by auto

    show "fa \<le> Max (g ` A)"

    proof(rule Max_ge_iff[THEN iffD2])

      from assms show "finite (g ` A)" by auto

    next

      from False show "g ` A \<noteq> {}" by auto

    next

      from h_fa have "g a \<in> g ` A" by auto

      moreover have "fa \<le> g a" using h_fa assms(2) by auto

      ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto

    qed

  qed

qed 

lemma Max_f_mono:

  assumes seq: "A \<subseteq> B"

  and np: "A \<noteq> {}"

  and fnt: "finite B"

  shows "Max (f ` A) \<le> Max (f ` B)"

proof(rule Max_mono)

  from seq show "f ` A \<subseteq> f ` B" by auto

next

  from np show "f ` A \<noteq> {}" by auto

next

  from fnt and seq show "finite (f ` B)" by auto

qed

lemma Max_UNION: 

  assumes "finite A"

  and "A \<noteq> {}"

  and "\<forall> M \<in> f ` A. finite M"

  and "\<forall> M \<in> f ` A. M \<noteq> {}"

  shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")

  using assms[simp]

proof -

  have "?L = Max (\<Union>(f ` A))"

    by (fold Union_image_eq, simp)

  also have "... = ?R"

    by (subst Max_Union, simp+)

  finally show ?thesis .

qed

lemma max_Max_eq:

  assumes "finite A"

    and "A \<noteq> {}"

    and "x = y"

  shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")

proof -

  have "?R = Max (insert y A)" by simp

  also from assms have "... = ?L"

      by (subst Max.insert, simp+)

  finally show ?thesis by simp

qed

end