src/HOL/Orderings.thy
changeset 54860 69b3e46d8fbe
parent 54857 5c05f7c5f8ae
child 54861 00d551179872
     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 @@ -342,47 +342,6 @@
     1.4    "class.linorder (op \<ge>) (op >)"
     1.5  by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
     1.6  
     1.7 -
     1.8 -text {* min/max *}
     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 -
    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 -lemma min_le_iff_disj:
    1.17 -  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    1.18 -unfolding min_def using linear by (auto intro: order_trans)
    1.19 -
    1.20 -lemma le_max_iff_disj:
    1.21 -  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
    1.22 -unfolding max_def using linear by (auto intro: order_trans)
    1.23 -
    1.24 -lemma min_less_iff_disj:
    1.25 -  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
    1.26 -unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.27 -
    1.28 -lemma less_max_iff_disj:
    1.29 -  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
    1.30 -unfolding max_def le_less using less_linear by (auto intro: less_trans)
    1.31 -
    1.32 -lemma min_less_iff_conj [simp]:
    1.33 -  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
    1.34 -unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.35 -
    1.36 -lemma max_less_iff_conj [simp]:
    1.37 -  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
    1.38 -unfolding max_def le_less using less_linear by (auto intro: less_trans)
    1.39 -
    1.40 -lemma split_min [no_atp]:
    1.41 -  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
    1.42 -by (simp add: min_def)
    1.43 -
    1.44 -lemma split_max [no_atp]:
    1.45 -  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
    1.46 -by (simp add: max_def)
    1.47 -
    1.48  end
    1.49  
    1.50  
    1.51 @@ -1028,7 +987,7 @@
    1.52  *)
    1.53  
    1.54  
    1.55 -subsection {* Monotonicity, least value operator and min/max *}
    1.56 +subsection {* Monotonicity *}
    1.57  
    1.58  context order
    1.59  begin
    1.60 @@ -1140,6 +1099,52 @@
    1.61    using assms
    1.62      by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
    1.63  
    1.64 +end
    1.65 +
    1.66 +
    1.67 +subsection {* min and max *}
    1.68 +
    1.69 +definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.70 +  "min a b = (if a \<le> b then a else b)"
    1.71 +
    1.72 +definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.73 +  "max a b = (if a \<le> b then b else a)"
    1.74 +
    1.75 +context linorder
    1.76 +begin
    1.77 +
    1.78 +lemma min_le_iff_disj:
    1.79 +  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    1.80 +unfolding min_def using linear by (auto intro: order_trans)
    1.81 +
    1.82 +lemma le_max_iff_disj:
    1.83 +  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
    1.84 +unfolding max_def using linear by (auto intro: order_trans)
    1.85 +
    1.86 +lemma min_less_iff_disj:
    1.87 +  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
    1.88 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.89 +
    1.90 +lemma less_max_iff_disj:
    1.91 +  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
    1.92 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
    1.93 +
    1.94 +lemma min_less_iff_conj [simp]:
    1.95 +  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
    1.96 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
    1.97 +
    1.98 +lemma max_less_iff_conj [simp]:
    1.99 +  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   1.100 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
   1.101 +
   1.102 +lemma split_min [no_atp]:
   1.103 +  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   1.104 +by (simp add: min_def)
   1.105 +
   1.106 +lemma split_max [no_atp]:
   1.107 +  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   1.108 +by (simp add: max_def)
   1.109 +
   1.110  lemma min_of_mono:
   1.111    fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
   1.112    shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   1.113 @@ -1503,7 +1508,7 @@
   1.114    unfolding le_fun_def by simp
   1.115  
   1.116  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   1.117 -  unfolding le_fun_def by simp
   1.118 +  by (rule le_funE)
   1.119  
   1.120  
   1.121  subsection {* Order on unary and binary predicates *}