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
```