1100 by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq) |
1100 by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq) |
1101 |
1101 |
1102 end |
1102 end |
1103 |
1103 |
1104 |
1104 |
1105 subsection {* min and max *} |
1105 subsection {* min and max -- fundamental *} |
1106 |
1106 |
1107 definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
1107 definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
1108 "min a b = (if a \<le> b then a else b)" |
1108 "min a b = (if a \<le> b then a else b)" |
1109 |
1109 |
1110 definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
1110 definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
1111 "max a b = (if a \<le> b then b else a)" |
1111 "max a b = (if a \<le> b then b else a)" |
1112 |
1112 |
1113 context linorder |
|
1114 begin |
|
1115 |
|
1116 lemma min_le_iff_disj: |
|
1117 "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" |
|
1118 unfolding min_def using linear by (auto intro: order_trans) |
|
1119 |
|
1120 lemma le_max_iff_disj: |
|
1121 "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" |
|
1122 unfolding max_def using linear by (auto intro: order_trans) |
|
1123 |
|
1124 lemma min_less_iff_disj: |
|
1125 "min x y < z \<longleftrightarrow> x < z \<or> y < z" |
|
1126 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
|
1127 |
|
1128 lemma less_max_iff_disj: |
|
1129 "z < max x y \<longleftrightarrow> z < x \<or> z < y" |
|
1130 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
|
1131 |
|
1132 lemma min_less_iff_conj [simp]: |
|
1133 "z < min x y \<longleftrightarrow> z < x \<and> z < y" |
|
1134 unfolding min_def le_less using less_linear by (auto intro: less_trans) |
|
1135 |
|
1136 lemma max_less_iff_conj [simp]: |
|
1137 "max x y < z \<longleftrightarrow> x < z \<and> y < z" |
|
1138 unfolding max_def le_less using less_linear by (auto intro: less_trans) |
|
1139 |
|
1140 lemma split_min [no_atp]: |
|
1141 "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" |
|
1142 by (simp add: min_def) |
|
1143 |
|
1144 lemma split_max [no_atp]: |
|
1145 "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" |
|
1146 by (simp add: max_def) |
|
1147 |
|
1148 lemma min_of_mono: |
|
1149 fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder" |
|
1150 shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" |
|
1151 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) |
|
1152 |
|
1153 lemma max_of_mono: |
|
1154 fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder" |
|
1155 shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" |
|
1156 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) |
|
1157 |
|
1158 end |
|
1159 |
|
1160 lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x" |
1113 lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x" |
1161 by (simp add: min_def) |
1114 by (simp add: min_def) |
1162 |
1115 |
1163 lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y" |
1116 lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y" |
1164 by (simp add: max_def) |
1117 by (simp add: max_def) |
1165 |
1118 |
1166 lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y" |
1119 lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y" |
1167 by (simp add:min_def) |
1120 by (simp add:min_def) |
1168 |
1121 |
1169 lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x" |
1122 lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x" |
1170 by (simp add: max_def) |
1123 by (simp add: max_def) |
1171 |
1124 |
1172 |
1125 |
1173 subsection {* (Unique) top and bottom elements *} |
1126 subsection {* (Unique) top and bottom elements *} |
1174 |
1127 |
1175 class bot = |
1128 class bot = |