--- 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)
--- a/src/HOL/Orderings.thy Wed Dec 25 15:52:25 2013 +0100
+++ b/src/HOL/Orderings.thy Wed Dec 25 15:52:25 2013 +0100
@@ -1102,7 +1102,7 @@
end
-subsection {* min and max *}
+subsection {* min and max -- fundamental *}
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
"min a b = (if a \<le> b then a else b)"
@@ -1110,64 +1110,17 @@
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
"max a b = (if a \<le> b then b else a)"
-context linorder
-begin
-
-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 min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"
-by (simp add: min_def)
+ by (simp add: min_def)
lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
-by (simp add: max_def)
+ by (simp add: max_def)
lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
-by (simp add:min_def)
+ by (simp add:min_def)
lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
-by (simp add: max_def)
+ by (simp add: max_def)
subsection {* (Unique) top and bottom elements *}