theory Maximports Mainbeginsection {* 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 assmsproof(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 qednext case empty assume "{} \<noteq> {}" show ?case by autoqedlemma 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 autonext 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 qedqed 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 autonext from np show "f ` A \<noteq> {}" by autonext from fnt and seq show "finite (f ` B)" by autoqedlemma 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 .qedlemma 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 simpqedend