src/HOL/Orderings.thy
changeset 56020 f92479477c52
parent 54868 bab6cade3cc5
child 56508 af08160c5a4c
     1.1 --- a/src/HOL/Orderings.thy	Mon Mar 10 17:14:57 2014 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 10 20:04:40 2014 +0100
     1.3 @@ -1010,6 +1010,28 @@
     1.4    from assms show "f x \<le> f y" by (simp add: mono_def)
     1.5  qed
     1.6  
     1.7 +definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
     1.8 +  "antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
     1.9 +
    1.10 +lemma antimonoI [intro?]:
    1.11 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.12 +  shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f"
    1.13 +  unfolding antimono_def by iprover
    1.14 +
    1.15 +lemma antimonoD [dest?]:
    1.16 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.17 +  shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
    1.18 +  unfolding antimono_def by iprover
    1.19 +
    1.20 +lemma antimonoE:
    1.21 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    1.22 +  assumes "antimono f"
    1.23 +  assumes "x \<le> y"
    1.24 +  obtains "f x \<ge> f y"
    1.25 +proof
    1.26 +  from assms show "f x \<ge> f y" by (simp add: antimono_def)
    1.27 +qed
    1.28 +
    1.29  definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    1.30    "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
    1.31