src/HOL/Orderings.thy
changeset 66936 cf8d8fc23891
parent 65963 ca1e636fa716
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Orderings.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -1178,6 +1178,21 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma mono_strict_invE:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b::order"
     1.9 +  assumes "mono f"
    1.10 +  assumes "f x < f y"
    1.11 +  obtains "x < y"
    1.12 +proof
    1.13 +  show "x < y"
    1.14 +  proof (rule ccontr)
    1.15 +    assume "\<not> x < y"
    1.16 +    then have "y \<le> x" by simp
    1.17 +    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
    1.18 +    with \<open>f x < f y\<close> show False by simp
    1.19 +  qed
    1.20 +qed
    1.21 +
    1.22  lemma strict_mono_eq:
    1.23    assumes "strict_mono f"
    1.24    shows "f x = f y \<longleftrightarrow> x = y"
    1.25 @@ -1243,6 +1258,7 @@
    1.26    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.27  by(auto simp add: max_def min_def)
    1.28  
    1.29 +
    1.30  subsection \<open>(Unique) top and bottom elements\<close>
    1.31  
    1.32  class bot =