# HG changeset patch
# User haftmann
# Date 1236346422 -3600
# Node ID 51797bcf4fd108524a59caa57ad38c7ff7bb1929
# Parent  41957d25a8b665292cf1a4bdc8b5d116ea96704d# Parent  abefe1dfadbbd0458a09722c71b14fd1a458e6f4
merged

diff -r 41957d25a8b6 -r 51797bcf4fd1 NEWS
--- a/NEWS	Fri Mar 06 11:50:32 2009 +0100
+++ b/NEWS	Fri Mar 06 14:33:42 2009 +0100
@@ -220,6 +220,10 @@
 
 *** HOL ***
 
+* New predicate "strict_mono" classifies strict functions on partial orders.
+With strict functions on linear orders, reasoning about (in)equalities is
+facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq".
+
 * Auxiliary class "itself" has disappeared -- classes without any parameter
 are treated as expected by the 'class' command.
 
diff -r 41957d25a8b6 -r 51797bcf4fd1 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 06 11:50:32 2009 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 06 14:33:42 2009 +0100
@@ -968,9 +968,7 @@
 context order
 begin
 
-definition
-  mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
-where
+definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
   "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
 
 lemma monoI [intro?]:
@@ -983,11 +981,76 @@
   shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   unfolding mono_def by iprover
 
+definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
+  "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
+
+lemma strict_monoI [intro?]:
+  assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
+  shows "strict_mono f"
+  using assms unfolding strict_mono_def by auto
+
+lemma strict_monoD [dest?]:
+  "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
+  unfolding strict_mono_def by auto
+
+lemma strict_mono_mono [dest?]:
+  assumes "strict_mono f"
+  shows "mono f"
+proof (rule monoI)
+  fix x y
+  assume "x \<le> y"
+  show "f x \<le> f y"
+  proof (cases "x = y")
+    case True then show ?thesis by simp
+  next
+    case False with `x \<le> y` have "x < y" by simp
+    with assms strict_monoD have "f x < f y" by auto
+    then show ?thesis by simp
+  qed
+qed
+
 end
 
 context linorder
 begin
 
+lemma strict_mono_eq:
+  assumes "strict_mono f"
+  shows "f x = f y \<longleftrightarrow> x = y"
+proof
+  assume "f x = f y"
+  show "x = y" proof (cases x y rule: linorder_cases)
+    case less with assms strict_monoD have "f x < f y" by auto
+    with `f x = f y` show ?thesis by simp
+  next
+    case equal then show ?thesis .
+  next
+    case greater with assms strict_monoD have "f y < f x" by auto
+    with `f x = f y` show ?thesis by simp
+  qed
+qed simp
+
+lemma strict_mono_less_eq:
+  assumes "strict_mono f"
+  shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
+proof
+  assume "x \<le> y"
+  with assms strict_mono_mono monoD show "f x \<le> f y" by auto
+next
+  assume "f x \<le> f y"
+  show "x \<le> y" proof (rule ccontr)
+    assume "\<not> x \<le> y" then have "y < x" by simp
+    with assms strict_monoD have "f y < f x" by auto
+    with `f x \<le> f y` show False by simp
+  qed
+qed
+  
+lemma strict_mono_less:
+  assumes "strict_mono f"
+  shows "f x < f y \<longleftrightarrow> x < y"
+  using assms
+    by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
+
 lemma min_of_mono:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
   shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"