src/HOL/Orderings.thy
 changeset 54861 00d551179872 parent 54860 69b3e46d8fbe child 54868 bab6cade3cc5
1.1 --- a/src/HOL/Orderings.thy	Wed Dec 25 15:52:25 2013 +0100
1.2 +++ b/src/HOL/Orderings.thy	Wed Dec 25 15:52:25 2013 +0100
1.3 @@ -1102,7 +1102,7 @@
1.4  end
1.7 -subsection {* min and max *}
1.8 +subsection {* min and max -- fundamental *}
1.10  definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.11    "min a b = (if a \<le> b then a else b)"
1.12 @@ -1110,64 +1110,17 @@
1.13  definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.14    "max a b = (if a \<le> b then b else a)"
1.16 -context linorder
1.17 -begin
1.18 -
1.19 -lemma min_le_iff_disj:
1.20 -  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
1.21 -unfolding min_def using linear by (auto intro: order_trans)
1.22 -
1.23 -lemma le_max_iff_disj:
1.24 -  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
1.25 -unfolding max_def using linear by (auto intro: order_trans)
1.26 -
1.27 -lemma min_less_iff_disj:
1.28 -  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
1.29 -unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.30 -
1.31 -lemma less_max_iff_disj:
1.32 -  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
1.33 -unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.34 -
1.35 -lemma min_less_iff_conj [simp]:
1.36 -  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
1.37 -unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.38 -
1.39 -lemma max_less_iff_conj [simp]:
1.40 -  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
1.41 -unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.42 -
1.43 -lemma split_min [no_atp]:
1.44 -  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
1.46 -
1.47 -lemma split_max [no_atp]:
1.48 -  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
1.50 -
1.51 -lemma min_of_mono:
1.52 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1.53 -  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
1.54 -  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
1.55 -
1.56 -lemma max_of_mono:
1.57 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1.58 -  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
1.59 -  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
1.60 -
1.61 -end
1.62 -
1.63  lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x"