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.5  
     1.6  
     1.7 -subsection {* min and max *}
     1.8 +subsection {* min and max -- fundamental *}
     1.9  
    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.15  
    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.45 -by (simp add: min_def)
    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.49 -by (simp add: max_def)
    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"
    1.64 -by (simp add: min_def)
    1.65 +  by (simp add: min_def)
    1.66  
    1.67  lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y"
    1.68 -by (simp add: max_def)
    1.69 +  by (simp add: max_def)
    1.70  
    1.71  lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"
    1.72 -by (simp add:min_def)
    1.73 +  by (simp add:min_def)
    1.74  
    1.75  lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x"
    1.76 -by (simp add: max_def)
    1.77 +  by (simp add: max_def)
    1.78  
    1.79  
    1.80  subsection {* (Unique) top and bottom elements *}