# HG changeset patch
# User haftmann
# Date 1236367777 -3600
# Node ID b3ae84c6e509f4d06e85a5e23de789b8bc9dc53d
# Parent  23935abfb549dc5d42abfa61acbad7fa5794fa7c
equalities for Min, Max

diff -r 23935abfb549 -r b3ae84c6e509 src/HOL/Finite_Set.thy
--- 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"