# HG changeset patch
# User noschinl
# Date 1323961844 -3600
# Node ID e7dbb27c13083ef00b65c58405d14189516faffe
# Parent  8dcf6692433f33f295b3649f823bc5f81cd2596a
add complementary lemmas for {min,max}_least

diff -r 8dcf6692433f -r e7dbb27c1308 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Dec 15 15:55:39 2011 +0100
+++ b/src/HOL/Orderings.thy	Thu Dec 15 16:10:44 2011 +0100
@@ -1057,14 +1057,24 @@
 by (simp add: max_def)
 
 lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
-apply (simp add: min_def)
-apply (blast intro: antisym)
-done
+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"
-apply (simp add: max_def)
-apply (blast intro: antisym)
-done
+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 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"
+by (simp add: max_def)
+
+
 
 
 subsection {* (Unique) top and bottom elements *}