--- a/src/HOL/Finite_Set.thy Fri Mar 06 15:51:18 2009 +0100
+++ b/src/HOL/Finite_Set.thy Fri Mar 06 20:29:37 2009 +0100
@@ -3060,6 +3060,30 @@
by (simp add: Max fold1_strict_below_iff [folded dual_max])
qed
+lemma Min_eqI:
+ assumes "finite A"
+ assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
+ and "x \<in> A"
+ shows "Min A = x"
+proof (rule antisym)
+ from `x \<in> A` have "A \<noteq> {}" by auto
+ with assms show "Min A \<ge> x" by simp
+next
+ from assms show "x \<ge> Min A" by simp
+qed
+
+lemma Max_eqI:
+ assumes "finite A"
+ assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
+ and "x \<in> A"
+ shows "Max A = x"
+proof (rule antisym)
+ from `x \<in> A` have "A \<noteq> {}" by auto
+ with assms show "Max A \<le> x" by simp
+next
+ from assms show "x \<le> Max A" by simp
+qed
+
lemma Min_antimono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Min N \<le> Min M"