# 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 \ 'b\order) \ bool"
-where
+definition mono :: "('a \ 'b\order) \ bool" where
"mono f \ (\x y. x \ y \ f x \ f y)"
lemma monoI [intro?]:
@@ -983,11 +981,76 @@
shows "mono f \ x \ y \ f x \ f y"
unfolding mono_def by iprover
+definition strict_mono :: "('a \ 'b\order) \ bool" where
+ "strict_mono f \ (\x y. x < y \ f x < f y)"
+
+lemma strict_monoI [intro?]:
+ assumes "\x y. x < y \ f x < f y"
+ shows "strict_mono f"
+ using assms unfolding strict_mono_def by auto
+
+lemma strict_monoD [dest?]:
+ "strict_mono f \ x < y \ 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 \ y"
+ show "f x \ f y"
+ proof (cases "x = y")
+ case True then show ?thesis by simp
+ next
+ case False with `x \ 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 \ 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 \ f y \ x \ y"
+proof
+ assume "x \ y"
+ with assms strict_mono_mono monoD show "f x \ f y" by auto
+next
+ assume "f x \ f y"
+ show "x \ y" proof (rule ccontr)
+ assume "\ x \ y" then have "y < x" by simp
+ with assms strict_monoD have "f y < f x" by auto
+ with `f x \ f y` show False by simp
+ qed
+qed
+
+lemma strict_mono_less:
+ assumes "strict_mono f"
+ shows "f x < f y \ 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 \ 'b\linorder"
shows "mono f \ min (f m) (f n) = f (min m n)"