# HG changeset patch
# User paulson
# Date 1146499840 -7200
# Node ID 9b5c38e8e780da90b2c36a385fc41deef4c69c88
# Parent  90fb9e092e66697dfa250cc9945f541b462c3889
some facts about min, max and add, diff

diff -r 90fb9e092e66 -r 9b5c38e8e780 src/HOL/OrderedGroup.thy
--- 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 *}
 
diff -r 90fb9e092e66 -r 9b5c38e8e780 src/HOL/Orderings.thy
--- 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)