--- a/Max.thy	Fri Oct 07 21:15:35 2016 +0100
+++ b/Max.thy	Fri Oct 21 14:47:01 2016 +0100
@@ -75,4 +75,76 @@
 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