src/HOL/Library/Sublist.thy
changeset 57499 7e22776f2d32
parent 57498 ea44ec62a574
child 57500 5a8b3e9d82a4
     1.1 --- a/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
     1.3 @@ -435,6 +435,14 @@
     1.4  | list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
     1.5  | list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
     1.6  
     1.7 +lemma list_emb_mono:                         
     1.8 +  assumes "\<And>x y. P x y \<longrightarrow> Q x y"
     1.9 +  shows "list_emb P xs ys \<longrightarrow> list_emb Q xs ys"
    1.10 +proof                                        
    1.11 +  assume "list_emb P xs ys"                    
    1.12 +  then show "list_emb Q xs ys" by (induct) (auto simp: assms)
    1.13 +qed 
    1.14 +
    1.15  lemma list_emb_Nil2 [simp]:
    1.16    assumes "list_emb P xs []" shows "xs = []"
    1.17    using assms by (cases rule: list_emb.cases) auto