Tuned Library/Sublist.thy
authoreberlm <eberlm@in.tum.de>
Mon May 29 16:40:56 2017 +0200 (2017-05-29)
changeset 65957558ba6b37f5c
parent 65956 639eb3617a86
child 65962 d7bc93a467bd
Tuned Library/Sublist.thy
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/Sublist.thy	Mon May 29 09:14:15 2017 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Mon May 29 16:40:56 2017 +0200
     1.3 @@ -492,7 +492,7 @@
     1.4    assumes "suffix xs ys"
     1.5    obtains zs where "ys = zs @ xs"
     1.6    using assms unfolding suffix_def by blast
     1.7 -
     1.8 +    
     1.9  lemma suffix_tl [simp]: "suffix (tl xs) xs"
    1.10    by (induct xs) (auto simp: suffix_def)
    1.11  
    1.12 @@ -1003,11 +1003,13 @@
    1.13  
    1.14  lemma list_emb_append_mono:
    1.15    "\<lbrakk> list_emb P xs xs'; list_emb P ys ys' \<rbrakk> \<Longrightarrow> list_emb P (xs@ys) (xs'@ys')"
    1.16 -  apply (induct rule: list_emb.induct)
    1.17 -    apply (metis eq_Nil_appendI list_emb_append2)
    1.18 -   apply (metis append_Cons list_emb_Cons)
    1.19 -  apply (metis append_Cons list_emb_Cons2)
    1.20 -  done
    1.21 +  by (induct rule: list_emb.induct) auto
    1.22 +
    1.23 +lemma prefix_imp_subseq [intro]: "prefix xs ys \<Longrightarrow> subseq xs ys"
    1.24 +  by (auto simp: prefix_def)
    1.25 +
    1.26 +lemma suffix_imp_subseq [intro]: "suffix xs ys \<Longrightarrow> subseq xs ys"
    1.27 +  by (auto simp: suffix_def)
    1.28  
    1.29  
    1.30  subsection \<open>Appending elements\<close>
    1.31 @@ -1275,6 +1277,9 @@
    1.32    "sublist xs (ys @ [y]) \<longleftrightarrow> suffix xs (ys @ [y]) \<or> sublist xs ys"
    1.33    by (subst (1 2) sublist_rev [symmetric])
    1.34       (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)     
    1.35 +     
    1.36 +lemma sublist_imp_subseq [intro]: "sublist xs ys \<Longrightarrow> subseq xs ys"
    1.37 +  by (auto simp: sublist_def)
    1.38  
    1.39  subsection \<open>Parametricity\<close>
    1.40