# HG changeset patch
# User traytel
# Date 1407342031 -7200
# Node ID 19f54b090cdd894a4c93c82fbe1d838db97e1adc
# Parent  9c065009cd8acfa621909af2955fa0d26aa3cf0f# Parent  84748234de9d842fe3637efd401accc260cb330b
merged

diff -r 9c065009cd8a -r 19f54b090cdd src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Aug 06 16:00:11 2014 +0200
+++ b/src/HOL/Lattices_Big.thy	Wed Aug 06 18:20:31 2014 +0200
@@ -633,6 +633,16 @@
 
 end
 
+lemma Max_eq_if:
+  assumes "finite A"  "finite B"  "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b"  "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
+  shows "Max A = Max B"
+proof cases
+  assume "A = {}" thus ?thesis using assms by simp
+next
+  assume "A \<noteq> {}" thus ?thesis using assms
+    by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
+qed
+
 lemma Min_antimono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"