author haftmann Fri, 06 Mar 2009 20:29:37 +0100 changeset 30325 b3ae84c6e509 parent 30308 23935abfb549 child 30326 a01b2de0e3e1
equalities for Min, Max
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- 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"```