--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Max.thy	Thu May 22 17:40:39 2014 +0100
@@ -0,0 +1,78 @@
+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
\ No newline at end of file