# HG changeset patch
# User nipkow
# Date 1502947637 -7200
# Node ID 050bc74d55edd5a425b6f65033bb6d3cf5dc1d72
# Parent  b9468503742a13c4d761de82d2dbc63219a735ff
added lemma

diff -r b9468503742a -r 050bc74d55ed src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 16 21:14:11 2017 +0200
+++ b/src/HOL/List.thy	Thu Aug 17 07:27:17 2017 +0200
@@ -4886,6 +4886,10 @@
       (meson assms transpD)
 qed simp_all
 
+lemma sorted_wrt_mono:
+  "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
+by(induction xs rule: sorted_wrt_induct)(auto)
+
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
 
 lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"