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

end