src/HOL/Library/Sublist.thy
changeset 57499 7e22776f2d32
parent 57498 ea44ec62a574
child 57500 5a8b3e9d82a4
equal deleted inserted replaced
57498:ea44ec62a574 57499:7e22776f2d32
   432   for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
   432   for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
   433 where
   433 where
   434   list_emb_Nil [intro, simp]: "list_emb P [] ys"
   434   list_emb_Nil [intro, simp]: "list_emb P [] ys"
   435 | list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
   435 | list_emb_Cons [intro] : "list_emb P xs ys \<Longrightarrow> list_emb P xs (y#ys)"
   436 | list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
   436 | list_emb_Cons2 [intro]: "P x y \<Longrightarrow> list_emb P xs ys \<Longrightarrow> list_emb P (x#xs) (y#ys)"
       
   437 
       
   438 lemma list_emb_mono:                         
       
   439   assumes "\<And>x y. P x y \<longrightarrow> Q x y"
       
   440   shows "list_emb P xs ys \<longrightarrow> list_emb Q xs ys"
       
   441 proof                                        
       
   442   assume "list_emb P xs ys"                    
       
   443   then show "list_emb Q xs ys" by (induct) (auto simp: assms)
       
   444 qed 
   437 
   445 
   438 lemma list_emb_Nil2 [simp]:
   446 lemma list_emb_Nil2 [simp]:
   439   assumes "list_emb P xs []" shows "xs = []"
   447   assumes "list_emb P xs []" shows "xs = []"
   440   using assms by (cases rule: list_emb.cases) auto
   448   using assms by (cases rule: list_emb.cases) auto
   441 
   449