src/HOL/Orderings.thy

--- 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 *}