# HG changeset patch
# User noschinl
# Date 1324302068 -3600
# Node ID 99cf6e4708164887986746153517e48b2a95dc03
# Parent  2a882ef2cd73ffe6920d629e1c22f8e849b2f4eb
weaken preconditions on lemmas

diff -r 2a882ef2cd73 -r 99cf6e470816 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -721,10 +721,10 @@
 by (rule monoI) simp
 
 lemma min_0L [simp]: "min 0 n = (0::nat)"
-by (rule min_leastL) simp
+by (rule min_absorb1) simp
 
 lemma min_0R [simp]: "min n 0 = (0::nat)"
-by (rule min_leastR) simp
+by (rule min_absorb2) simp
 
 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
 by (simp add: mono_Suc min_of_mono)
@@ -738,10 +738,10 @@
 by (simp split: nat.split)
 
 lemma max_0L [simp]: "max 0 n = (n::nat)"
-by (rule max_leastL) simp
+by (rule max_absorb2) simp
 
 lemma max_0R [simp]: "max n 0 = (n::nat)"
-by (rule max_leastR) simp
+by (rule max_absorb1) simp
 
 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
 by (simp add: mono_Suc max_of_mono)
diff -r 2a882ef2cd73 -r 99cf6e470816 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Dec 19 14:41:08 2011 +0100
+++ b/src/HOL/Orderings.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -1050,33 +1050,20 @@
 
 end
 
-lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
+lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"
 by (simp add: min_def)
 
-lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
+lemma max_absorb2: "x \<le> y ==> max x y = y"
 by (simp add: max_def)
 
-lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
-by (simp add: min_def) (blast intro: antisym)
-
-lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
-by (simp add: max_def) (blast intro: antisym)
-
-lemma min_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> min greatest x = x"
-by (simp add: min_def) (blast intro: antisym)
+lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
+by (simp add:min_def)
 
-lemma max_greatestL: "(\<And>x::'a::order. x \<le> greatest) \<Longrightarrow> max greatest x = greatest"
-by (simp add: max_def) (blast intro: antisym)
-
-lemma min_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> min x greatest = x"
-by (simp add: min_def)
-
-lemma max_greatestR: "(\<And>x. x \<le> greatest) \<Longrightarrow> max x greatest = greatest"
+lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
 by (simp add: max_def)
 
 
 
-
 subsection {* (Unique) top and bottom elements *}
 
 class bot = order +