some facts about min, max and add, diff

--- a/src/HOL/OrderedGroup.thy	Mon May 01 18:10:18 2006 +0200
+++ b/src/HOL/OrderedGroup.thy	Mon May 01 18:10:40 2006 +0200
@@ -335,6 +335,26 @@
   shows "[|0\<le>a; b<c|] ==> b < a + c"
 by (insert add_le_less_mono [of 0 a b c], simp)
 
+lemma max_add_distrib_left:
+  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+  shows  "(max x y) + z = max (x+z) (y+z)"
+by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
+
+lemma min_add_distrib_left:
+  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+  shows  "(min x y) + z = min (x+z) (y+z)"
+by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
+
+lemma max_diff_distrib_left:
+  fixes z :: "'a::pordered_ab_group_add"
+  shows  "(max x y) - z = max (x-z) (y-z)"
+by (simp add: diff_minus, rule max_add_distrib_left) 
+
+lemma min_diff_distrib_left:
+  fixes z :: "'a::pordered_ab_group_add"
+  shows  "(min x y) - z = min (x-z) (y-z)"
+by (simp add: diff_minus, rule min_add_distrib_left) 
+
 
 subsection {* Ordering Rules for Unary Minus *}
 

--- a/src/HOL/Orderings.thy	Mon May 01 18:10:18 2006 +0200
+++ b/src/HOL/Orderings.thy	Mon May 01 18:10:40 2006 +0200
@@ -68,14 +68,14 @@
   by (simp add: min_def)
 
 lemma min_of_mono:
-    "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
+    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
   by (simp add: min_def)
 
 lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
   by (simp add: max_def)
 
 lemma max_of_mono:
-    "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
+    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   by (simp add: max_def)