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