src/HOL/Orderings.thy
changeset 61630 608520e0e8e2
parent 61605 1bf7b186542e
child 61699 a81dc5c4d6a9
     1.1 --- a/src/HOL/Orderings.thy	Wed Nov 11 09:21:56 2015 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Nov 11 09:48:24 2015 +0100
     1.3 @@ -256,7 +256,6 @@
     1.4  unfolding Least_def by (rule theI2)
     1.5    (blast intro: assms antisym)+
     1.6  
     1.7 -
     1.8  text \<open>Dual order\<close>
     1.9  
    1.10  lemma dual_order:
    1.11 @@ -1171,6 +1170,10 @@
    1.12  lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
    1.13    by (simp add: max_def)
    1.14  
    1.15 +lemma max_min_same [simp]:
    1.16 +  fixes x y :: "'a :: linorder"
    1.17 +  shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
    1.18 +by(auto simp add: max_def min_def)
    1.19  
    1.20  subsection \<open>(Unique) top and bottom elements\<close>
    1.21