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