# HG changeset patch
# User Christian Sternagel
# Date 1404374115 -7200
# Node ID 7e22776f2d3271ce5f7f9ddf6ba7489b6f93f798
# Parent  ea44ec62a574a3fcfda82cb44d1399e3e3730170
added monotonicity lemma for list embedding

diff -r ea44ec62a574 -r 7e22776f2d32 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
+++ b/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
@@ -435,6 +435,14 @@
 | list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
 | list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
 
+lemma list_emb_mono:                         
+  assumes "\<And>x y. P x y \<longrightarrow> Q x y"
+  shows "list_emb P xs ys \<longrightarrow> list_emb Q xs ys"
+proof                                        
+  assume "list_emb P xs ys"                    
+  then show "list_emb Q xs ys" by (induct) (auto simp: assms)
+qed 
+
 lemma list_emb_Nil2 [simp]:
   assumes "list_emb P xs []" shows "xs = []"
   using assms by (cases rule: list_emb.cases) auto