# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1496068856 -7200
# Node ID 558ba6b37f5c764b89c35963b28ffe6add9fd21f
# Parent  639eb3617a86fed35f64d1ecb964dcd3b7fd5a4a
Tuned Library/Sublist.thy

diff -r 639eb3617a86 -r 558ba6b37f5c src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Mon May 29 09:14:15 2017 +0200
+++ b/src/HOL/Library/Sublist.thy	Mon May 29 16:40:56 2017 +0200
@@ -492,7 +492,7 @@
   assumes "suffix xs ys"
   obtains zs where "ys = zs @ xs"
   using assms unfolding suffix_def by blast
-
+    
 lemma suffix_tl [simp]: "suffix (tl xs) xs"
   by (induct xs) (auto simp: suffix_def)
 
@@ -1003,11 +1003,13 @@
 
 lemma list_emb_append_mono:
   "\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')"
-  apply (induct rule: list_emb.induct)
-    apply (metis eq_Nil_appendI list_emb_append2)
-   apply (metis append_Cons list_emb_Cons)
-  apply (metis append_Cons list_emb_Cons2)
-  done
+  by (induct rule: list_emb.induct) auto
+
+lemma prefix_imp_subseq [intro]: "prefix xs ys \<Longrightarrow> subseq xs ys"
+  by (auto simp: prefix_def)
+
+lemma suffix_imp_subseq [intro]: "suffix xs ys \<Longrightarrow> subseq xs ys"
+  by (auto simp: suffix_def)
 
 
 subsection \<open>Appending elements\<close>
@@ -1275,6 +1277,9 @@
   "sublist xs (ys @ [y]) \<longleftrightarrow> suffix xs (ys @ [y]) \<or> sublist xs ys"
   by (subst (1 2) sublist_rev [symmetric])
      (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)     
+     
+lemma sublist_imp_subseq [intro]: "sublist xs ys \<Longrightarrow> subseq xs ys"
+  by (auto simp: sublist_def)
 
 subsection \<open>Parametricity\<close>