# HG changeset patch
# User haftmann
# Date 1265634406 -3600
# Node ID 8103ea95b1426daeb7fc35b59678f02b43fabade
# Parent  e47934673b74138cfc2508b4d4a9d2844fe65d29
added lemmas involving Min, Max, uminus

diff -r e47934673b74 -r 8103ea95b142 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Feb 08 14:06:43 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 08 14:06:46 2010 +0100
@@ -3324,6 +3324,19 @@
 
 end
 
+context linordered_ab_group_add
+begin
+
+lemma minus_Max_eq_Min [simp]:
+  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
+  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
+
+lemma minus_Min_eq_Max [simp]:
+  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
+  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
+
+end
+
 
 subsection {* Expressing set operations via @{const fold} *}