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 autoqedend