diff -r 69b3e46d8fbe -r 00d551179872 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
+++ b/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -712,10 +712,57 @@
 
 subsection {* @{text "min/max"} as special case of lattice *}
 
-sublocale linorder < min!: semilattice_order min less_eq less
+context linorder
+begin
+
+sublocale min!: semilattice_order min less_eq less
   + max!: semilattice_order max greater_eq greater
   by default (auto simp add: min_def max_def)
 
+lemma min_le_iff_disj:
+  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
+  unfolding min_def using linear by (auto intro: order_trans)
+
+lemma le_max_iff_disj:
+  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
+  unfolding max_def using linear by (auto intro: order_trans)
+
+lemma min_less_iff_disj:
+  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
+  unfolding min_def le_less using less_linear by (auto intro: less_trans)
+
+lemma less_max_iff_disj:
+  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
+  unfolding max_def le_less using less_linear by (auto intro: less_trans)
+
+lemma min_less_iff_conj [simp]:
+  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
+  unfolding min_def le_less using less_linear by (auto intro: less_trans)
+
+lemma max_less_iff_conj [simp]:
+  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
+  unfolding max_def le_less using less_linear by (auto intro: less_trans)
+
+lemma split_min [no_atp]:
+  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
+  by (simp add: min_def)
+
+lemma split_max [no_atp]:
+  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
+  by (simp add: max_def)
+
+lemma min_of_mono:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
+  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
+  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
+
+lemma max_of_mono:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
+  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
+  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
+
+end
+
 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (auto intro: antisym simp add: min_def fun_eq_iff)