# 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)"