equal
deleted
inserted
replaced
289 subsection {* @{const min}/@{const max} on linear orders as |
289 subsection {* @{const min}/@{const max} on linear orders as |
290 special case of @{const inf}/@{const sup} *} |
290 special case of @{const inf}/@{const sup} *} |
291 |
291 |
292 lemma (in linorder) distrib_lattice_min_max: |
292 lemma (in linorder) distrib_lattice_min_max: |
293 "distrib_lattice (op \<le>) (op <) min max" |
293 "distrib_lattice (op \<le>) (op <) min max" |
294 proof unfold_locales |
294 proof |
295 have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" |
295 have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" |
296 by (auto simp add: less_le antisym) |
296 by (auto simp add: less_le antisym) |
297 fix x y z |
297 fix x y z |
298 show "max x (min y z) = min (max x y) (max x z)" |
298 show "max x (min y z) = min (max x y) (max x z)" |
299 unfolding min_def max_def |
299 unfolding min_def max_def |