added strict_mono predicate
authorhaftmann
Fri Mar 06 14:33:19 2009 +0100 (2009-03-06)
changeset 30298abefe1dfadbb
parent 30294 d6bffd97d8d5
child 30299 51797bcf4fd1
added strict_mono predicate
NEWS
src/HOL/Orderings.thy
     1.1 --- a/NEWS	Fri Mar 06 09:35:43 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 06 14:33:19 2009 +0100
     1.3 @@ -220,6 +220,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New predicate "strict_mono" classifies strict functions on partial orders.
     1.8 +With strict functions on linear orders, reasoning about (in)equalities is
     1.9 +facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq".
    1.10 +
    1.11  * Auxiliary class "itself" has disappeared -- classes without any parameter
    1.12  are treated as expected by the 'class' command.
    1.13  
     2.1 --- a/src/HOL/Orderings.thy	Fri Mar 06 09:35:43 2009 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Fri Mar 06 14:33:19 2009 +0100
     2.3 @@ -968,9 +968,7 @@
     2.4  context order
     2.5  begin
     2.6  
     2.7 -definition
     2.8 -  mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
     2.9 -where
    2.10 +definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    2.11    "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
    2.12  
    2.13  lemma monoI [intro?]:
    2.14 @@ -983,11 +981,76 @@
    2.15    shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
    2.16    unfolding mono_def by iprover
    2.17  
    2.18 +definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    2.19 +  "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
    2.20 +
    2.21 +lemma strict_monoI [intro?]:
    2.22 +  assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
    2.23 +  shows "strict_mono f"
    2.24 +  using assms unfolding strict_mono_def by auto
    2.25 +
    2.26 +lemma strict_monoD [dest?]:
    2.27 +  "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
    2.28 +  unfolding strict_mono_def by auto
    2.29 +
    2.30 +lemma strict_mono_mono [dest?]:
    2.31 +  assumes "strict_mono f"
    2.32 +  shows "mono f"
    2.33 +proof (rule monoI)
    2.34 +  fix x y
    2.35 +  assume "x \<le> y"
    2.36 +  show "f x \<le> f y"
    2.37 +  proof (cases "x = y")
    2.38 +    case True then show ?thesis by simp
    2.39 +  next
    2.40 +    case False with `x \<le> y` have "x < y" by simp
    2.41 +    with assms strict_monoD have "f x < f y" by auto
    2.42 +    then show ?thesis by simp
    2.43 +  qed
    2.44 +qed
    2.45 +
    2.46  end
    2.47  
    2.48  context linorder
    2.49  begin
    2.50  
    2.51 +lemma strict_mono_eq:
    2.52 +  assumes "strict_mono f"
    2.53 +  shows "f x = f y \<longleftrightarrow> x = y"
    2.54 +proof
    2.55 +  assume "f x = f y"
    2.56 +  show "x = y" proof (cases x y rule: linorder_cases)
    2.57 +    case less with assms strict_monoD have "f x < f y" by auto
    2.58 +    with `f x = f y` show ?thesis by simp
    2.59 +  next
    2.60 +    case equal then show ?thesis .
    2.61 +  next
    2.62 +    case greater with assms strict_monoD have "f y < f x" by auto
    2.63 +    with `f x = f y` show ?thesis by simp
    2.64 +  qed
    2.65 +qed simp
    2.66 +
    2.67 +lemma strict_mono_less_eq:
    2.68 +  assumes "strict_mono f"
    2.69 +  shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
    2.70 +proof
    2.71 +  assume "x \<le> y"
    2.72 +  with assms strict_mono_mono monoD show "f x \<le> f y" by auto
    2.73 +next
    2.74 +  assume "f x \<le> f y"
    2.75 +  show "x \<le> y" proof (rule ccontr)
    2.76 +    assume "\<not> x \<le> y" then have "y < x" by simp
    2.77 +    with assms strict_monoD have "f y < f x" by auto
    2.78 +    with `f x \<le> f y` show False by simp
    2.79 +  qed
    2.80 +qed
    2.81 +  
    2.82 +lemma strict_mono_less:
    2.83 +  assumes "strict_mono f"
    2.84 +  shows "f x < f y \<longleftrightarrow> x < y"
    2.85 +  using assms
    2.86 +    by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
    2.87 +
    2.88  lemma min_of_mono:
    2.89    fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
    2.90    shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"