src/HOL/Orderings.thy
 changeset 30298 abefe1dfadbb parent 30107 f3b3b0e3d184 child 30510 4120fc59dd85
```     1.1 --- a/src/HOL/Orderings.thy	Fri Mar 06 09:35:43 2009 +0100
1.2 +++ b/src/HOL/Orderings.thy	Fri Mar 06 14:33:19 2009 +0100
1.3 @@ -968,9 +968,7 @@
1.4  context order
1.5  begin
1.6
1.7 -definition
1.8 -  mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
1.9 -where
1.10 +definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
1.11    "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
1.12
1.13  lemma monoI [intro?]:
1.14 @@ -983,11 +981,76 @@
1.15    shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
1.16    unfolding mono_def by iprover
1.17
1.18 +definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
1.19 +  "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
1.20 +
1.21 +lemma strict_monoI [intro?]:
1.22 +  assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
1.23 +  shows "strict_mono f"
1.24 +  using assms unfolding strict_mono_def by auto
1.25 +
1.26 +lemma strict_monoD [dest?]:
1.27 +  "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
1.28 +  unfolding strict_mono_def by auto
1.29 +
1.30 +lemma strict_mono_mono [dest?]:
1.31 +  assumes "strict_mono f"
1.32 +  shows "mono f"
1.33 +proof (rule monoI)
1.34 +  fix x y
1.35 +  assume "x \<le> y"
1.36 +  show "f x \<le> f y"
1.37 +  proof (cases "x = y")
1.38 +    case True then show ?thesis by simp
1.39 +  next
1.40 +    case False with `x \<le> y` have "x < y" by simp
1.41 +    with assms strict_monoD have "f x < f y" by auto
1.42 +    then show ?thesis by simp
1.43 +  qed
1.44 +qed
1.45 +
1.46  end
1.47
1.48  context linorder
1.49  begin
1.50
1.51 +lemma strict_mono_eq:
1.52 +  assumes "strict_mono f"
1.53 +  shows "f x = f y \<longleftrightarrow> x = y"
1.54 +proof
1.55 +  assume "f x = f y"
1.56 +  show "x = y" proof (cases x y rule: linorder_cases)
1.57 +    case less with assms strict_monoD have "f x < f y" by auto
1.58 +    with `f x = f y` show ?thesis by simp
1.59 +  next
1.60 +    case equal then show ?thesis .
1.61 +  next
1.62 +    case greater with assms strict_monoD have "f y < f x" by auto
1.63 +    with `f x = f y` show ?thesis by simp
1.64 +  qed
1.65 +qed simp
1.66 +
1.67 +lemma strict_mono_less_eq:
1.68 +  assumes "strict_mono f"
1.69 +  shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
1.70 +proof
1.71 +  assume "x \<le> y"
1.72 +  with assms strict_mono_mono monoD show "f x \<le> f y" by auto
1.73 +next
1.74 +  assume "f x \<le> f y"
1.75 +  show "x \<le> y" proof (rule ccontr)
1.76 +    assume "\<not> x \<le> y" then have "y < x" by simp
1.77 +    with assms strict_monoD have "f y < f x" by auto
1.78 +    with `f x \<le> f y` show False by simp
1.79 +  qed
1.80 +qed
1.81 +
1.82 +lemma strict_mono_less:
1.83 +  assumes "strict_mono f"
1.84 +  shows "f x < f y \<longleftrightarrow> x < y"
1.85 +  using assms
1.86 +    by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
1.87 +
1.88  lemma min_of_mono:
1.89    fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1.90    shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
```