# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1495101741 -7200
# Node ID a6ed757b858518304b68d109c29c22e78c0a574e
# Parent  f35abc25d7b1b301b0b450394dfcc4503884c17f
more on sublists

diff -r f35abc25d7b1 -r a6ed757b8585 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Wed May 17 23:13:56 2017 +0200
+++ b/src/HOL/Library/Sublist.thy	Thu May 18 12:02:21 2017 +0200
@@ -57,12 +57,12 @@
 subsection \<open>Basic properties of prefixes\<close>
 
 (* FIXME rm *)
-theorem Nil_prefix [iff]: "prefix [] xs"
-by(fact prefix_bot.bot_least)
+theorem Nil_prefix [simp]: "prefix [] xs"
+  by (fact prefix_bot.bot_least)
 
 (* FIXME rm *)
 theorem prefix_Nil [simp]: "(prefix xs []) = (xs = [])"
-by(fact prefix_bot.bot_unique)
+  by (fact prefix_bot.bot_unique)
 
 lemma prefix_snoc [simp]: "prefix xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefix xs ys"
 proof
@@ -88,7 +88,7 @@
 lemma same_prefix_prefix [simp]: "prefix (xs @ ys) (xs @ zs) = prefix ys zs"
   by (induct xs) simp_all
 
-lemma same_prefix_nil [iff]: "prefix (xs @ ys) xs = (ys = [])"
+lemma same_prefix_nil [simp]: "prefix (xs @ ys) xs = (ys = [])"
   by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI)
 
 lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)"
@@ -228,16 +228,57 @@
 qed
 
 lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1"
-by (induction xs) auto
+  by (induction xs) auto
+    
+lemma distinct_prefixes [intro]: "distinct (prefixes xs)"
+  by (induction xs) (auto simp: distinct_map)
+
+lemma prefixes_snoc [simp]: "prefixes (xs@[x]) = prefixes xs @ [xs@[x]]"
+  by (induction xs) auto
+
+lemma prefixes_not_Nil [simp]: "prefixes xs \<noteq> []"
+  by (cases xs) auto
 
-lemma prefixes_snoc[simp]:
-  "prefixes (xs@[x]) = prefixes xs @ [xs@[x]]"
-by (induction xs) auto
+lemma hd_prefixes [simp]: "hd (prefixes xs) = []"
+  by (cases xs) simp_all
 
-lemma prefixes_eq_Snoc:
+lemma last_prefixes [simp]: "last (prefixes xs) = xs"
+  by (induction xs) (simp_all add: last_map)
+    
+lemma prefixes_append: 
+  "prefixes (xs @ ys) = prefixes xs @ map (\<lambda>ys'. xs @ ys') (tl (prefixes ys))"
+proof (induction xs)
+  case Nil
+  thus ?case by (cases ys) auto
+qed simp_all
+
+lemma prefixes_eq_snoc:
   "prefixes ys = xs @ [x] \<longleftrightarrow>
   (ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = zs@[z] \<and> xs = prefixes zs)) \<and> x = ys"
-by (cases ys rule: rev_cases) auto
+  by (cases ys rule: rev_cases) auto
+
+lemma prefixes_tailrec [code]: 
+  "prefixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) ([],[[]]) xs))"
+proof -
+  have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, rev (x#acc1)#acc2)) (ys, rev ys # zs) xs =
+          (rev xs @ ys, rev (map (\<lambda>as. rev ys @ as) (prefixes xs)) @ zs)" for ys zs
+  proof (induction xs arbitrary: ys zs)
+    case (Cons x xs ys zs)
+    from Cons.IH[of "x # ys" "rev ys # zs"]
+      show ?case by (simp add: o_def)
+  qed simp_all
+  from this [of "[]" "[]"] show ?thesis by simp
+qed
+  
+lemma set_prefixes_eq: "set (prefixes xs) = {ys. prefix ys xs}"
+  by auto
+
+lemma card_set_prefixes [simp]: "card (set (prefixes xs)) = Suc (length xs)"
+  by (subst distinct_card) auto
+
+lemma set_prefixes_append: 
+  "set (prefixes (xs @ ys)) = set (prefixes xs) \<union> {xs @ ys' |ys'. ys' \<in> set (prefixes ys)}"
+  by (subst prefixes_append, cases ys) auto
 
 
 subsection \<open>Longest Common Prefix\<close>
@@ -435,11 +476,13 @@
   where "suffix xs ys = (\<exists>zs. ys = zs @ xs)"
 
 definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-  where "strict_suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"
+  where "strict_suffix xs ys \<longleftrightarrow> suffix xs ys \<and> xs \<noteq> ys"
 
-lemma strict_suffix_imp_suffix:
-  "strict_suffix xs ys \<Longrightarrow> suffix xs ys"
-  by (auto simp: suffix_def strict_suffix_def)
+interpretation suffix_order: order suffix strict_suffix
+  by standard (auto simp: suffix_def strict_suffix_def)
+
+interpretation suffix_bot: order_bot Nil suffix strict_suffix
+  by standard (simp add: suffix_def)
 
 lemma suffixI [intro?]: "ys = zs @ xs \<Longrightarrow> suffix xs ys"
   unfolding suffix_def by blast
@@ -449,27 +492,13 @@
   obtains zs where "ys = zs @ xs"
   using assms unfolding suffix_def by blast
 
-lemma suffix_refl [iff]: "suffix xs xs"
-  by (auto simp add: suffix_def)
-
-lemma suffix_trans:
-  "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"
-  by (auto simp: suffix_def)
-
-lemma strict_suffix_trans:
-  "\<lbrakk>strict_suffix xs ys; strict_suffix ys zs\<rbrakk> \<Longrightarrow> strict_suffix xs zs"
-by (auto simp add: strict_suffix_def)
-
-lemma suffix_antisym: "\<lbrakk>suffix xs ys; suffix ys xs\<rbrakk> \<Longrightarrow> xs = ys"
-  by (auto simp add: suffix_def)
-
 lemma suffix_tl [simp]: "suffix (tl xs) xs"
   by (induct xs) (auto simp: suffix_def)
 
 lemma strict_suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> strict_suffix (tl xs) xs"
-  by (induct xs) (auto simp: strict_suffix_def)
+  by (induct xs) (auto simp: strict_suffix_def suffix_def)
 
-lemma Nil_suffix [iff]: "suffix [] xs"
+lemma Nil_suffix [simp]: "suffix [] xs"
   by (simp add: suffix_def)
 
 lemma suffix_Nil [simp]: "(suffix xs []) = (xs = [])"
@@ -488,10 +517,10 @@
   by (auto simp add: suffix_def)
 
 lemma strict_suffix_set_subset: "strict_suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
-by (auto simp: strict_suffix_def)
+  by (auto simp: strict_suffix_def suffix_def)
 
 lemma suffix_set_subset: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
-by (auto simp: suffix_def)
+  by (auto simp: suffix_def)
 
 lemma suffix_ConsD2: "suffix (x # xs) (y # ys) \<Longrightarrow> suffix xs ys"
 proof -
@@ -514,6 +543,9 @@
   then have "ys = rev zs @ xs" by simp
   then show "suffix xs ys" ..
 qed
+  
+lemma strict_suffix_to_prefix [code]: "strict_suffix xs ys \<longleftrightarrow> strict_prefix (rev xs) (rev ys)"
+  by (auto simp: suffix_to_prefix strict_suffix_def strict_prefix_def)
 
 lemma distinct_suffix: "distinct ys \<Longrightarrow> suffix xs ys \<Longrightarrow> distinct xs"
   by (clarsimp elim!: suffixE)
@@ -522,20 +554,110 @@
   by (auto elim!: suffixE intro: suffixI)
 
 lemma suffix_drop: "suffix (drop n as) as"
-  unfolding suffix_def
-  apply (rule exI [where x = "take n as"])
-  apply simp
-  done
+  unfolding suffix_def by (rule exI [where x = "take n as"]) simp
 
 lemma suffix_take: "suffix xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
   by (auto elim!: suffixE)
 
 lemma strict_suffix_reflclp_conv: "strict_suffix\<^sup>=\<^sup>= = suffix"
-by (intro ext) (auto simp: suffix_def strict_suffix_def)
+  by (intro ext) (auto simp: suffix_def strict_suffix_def)
 
 lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
   unfolding suffix_def by auto
 
+lemma suffix_snoc [simp]: "suffix xs (ys @ [y]) \<longleftrightarrow> xs = [] \<or> (\<exists>zs. xs = zs @ [y] \<and> suffix zs ys)"
+  by (cases xs rule: rev_cases) (auto simp: suffix_def)
+
+lemma snoc_suffix_snoc [simp]: "suffix (xs @ [x]) (ys @ [y]) = (x = y \<and> suffix xs ys)"
+  by (auto simp add: suffix_def)
+
+lemma same_suffix_suffix [simp]: "suffix (ys @ xs) (zs @ xs) = suffix ys zs"
+  by (simp add: suffix_to_prefix)
+
+lemma same_suffix_nil [simp]: "suffix (ys @ xs) xs = (ys = [])"
+  by (simp add: suffix_to_prefix)
+
+theorem suffix_Cons: "suffix xs (y # ys) \<longleftrightarrow> xs = y # ys \<or> suffix xs ys"
+  unfolding suffix_def by (auto simp: Cons_eq_append_conv)
+
+theorem suffix_append: 
+  "suffix xs (ys @ zs) \<longleftrightarrow> suffix xs zs \<or> (\<exists>xs'. xs = xs' @ zs \<and> suffix xs' ys)"
+  by (auto simp: suffix_def append_eq_append_conv2)
+
+theorem suffix_length_le: "suffix xs ys \<Longrightarrow> length xs \<le> length ys"
+  by (auto simp add: suffix_def)
+
+lemma suffix_same_cases:
+  "suffix (xs\<^sub>1::'a list) ys \<Longrightarrow> suffix xs\<^sub>2 ys \<Longrightarrow> suffix xs\<^sub>1 xs\<^sub>2 \<or> suffix xs\<^sub>2 xs\<^sub>1"
+  unfolding suffix_def by (force simp: append_eq_append_conv2)
+
+lemma suffix_length_suffix:
+  "suffix ps xs \<Longrightarrow> suffix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> suffix ps qs"
+  by (auto simp: suffix_to_prefix intro: prefix_length_prefix)
+
+lemma suffix_length_less: "strict_suffix xs ys \<Longrightarrow> length xs < length ys"
+  by (auto simp: strict_suffix_def suffix_def)
+
+lemma suffix_ConsD': "suffix (x#xs) ys \<Longrightarrow> strict_suffix xs ys"
+  by (auto simp: strict_suffix_def suffix_def)
+
+lemma drop_strict_suffix: "strict_suffix xs ys \<Longrightarrow> strict_suffix (drop n xs) ys"
+proof (induct n arbitrary: xs ys)
+  case 0
+  then show ?case by (cases ys) simp_all
+next
+  case (Suc n)
+  then show ?case 
+    by (cases xs) (auto intro: Suc dest: suffix_ConsD' suffix_order.less_imp_le)
+qed
+
+lemma not_suffix_cases:
+  assumes pfx: "\<not> suffix ps ls"
+  obtains
+    (c1) "ps \<noteq> []" and "ls = []"
+  | (c2) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x = a" and "\<not> suffix as xs"
+  | (c3) a as x xs where "ps = as@[a]" and "ls = xs@[x]" and "x \<noteq> a"
+proof (cases ps rule: rev_cases)
+  case Nil
+  then show ?thesis using pfx by simp
+next
+  case (snoc as a)
+  note c = \<open>ps = as@[a]\<close>
+  show ?thesis
+  proof (cases ls rule: rev_cases)
+    case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_suffix_nil)
+  next
+    case (snoc xs x)
+    show ?thesis
+    proof (cases "x = a")
+      case True
+      have "\<not> suffix as xs" using pfx c snoc True by simp
+      with c snoc True show ?thesis by (rule c2)
+    next
+      case False
+      with c snoc show ?thesis by (rule c3)
+    qed
+  qed
+qed
+
+lemma not_suffix_induct [consumes 1, case_names Nil Neq Eq]:
+  assumes np: "\<not> suffix ps ls"
+    and base: "\<And>x xs. P (xs@[x]) []"
+    and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (xs@[x]) (ys@[y])"
+    and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> suffix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (xs@[x]) (ys@[y])"
+  shows "P ps ls" using np
+proof (induct ls arbitrary: ps rule: rev_induct)
+  case Nil
+  then show ?case by (cases ps rule: rev_cases) (auto intro: base)
+next
+  case (snoc y ys ps)
+  then have npfx: "\<not> suffix ps (ys @ [y])" by simp
+  then obtain x xs where pv: "ps = xs @ [x]"
+    by (rule not_suffix_cases) auto
+  show ?case by (metis snoc.hyps snoc_suffix_snoc npfx pv r1 r2)
+qed
+
+
 lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y"
   by blast
 
@@ -576,6 +698,85 @@
   qed
 qed
 
+subsection \<open>Suffixes\<close>
+
+fun suffixes where
+  "suffixes [] = [[]]"
+| "suffixes (x#xs) = suffixes xs @ [x # xs]"
+
+lemma in_set_suffixes [simp]: "xs \<in> set (suffixes ys) \<longleftrightarrow> suffix xs ys"
+  by (induction ys) (auto simp: suffix_def Cons_eq_append_conv)
+
+lemma distinct_suffixes [intro]: "distinct (suffixes xs)"
+  by (induction xs) (auto simp: suffix_def)
+
+lemma length_suffixes [simp]: "length (suffixes xs) = Suc (length xs)"
+  by (induction xs) auto
+
+lemma suffixes_snoc [simp]: "suffixes (xs @ [x]) = [] # map (\<lambda>ys. ys @ [x]) (suffixes xs)"
+  by (induction xs) auto
+
+lemma suffixes_not_Nil [simp]: "suffixes xs \<noteq> []"
+  by (cases xs) auto
+
+lemma hd_suffixes [simp]: "hd (suffixes xs) = []"
+  by (induction xs) simp_all
+
+lemma last_suffixes [simp]: "last (suffixes xs) = xs"
+  by (cases xs) simp_all
+
+lemma suffixes_append: 
+  "suffixes (xs @ ys) = suffixes ys @ map (\<lambda>xs'. xs' @ ys) (tl (suffixes xs))"
+proof (induction ys rule: rev_induct)
+  case Nil
+  thus ?case by (cases xs rule: rev_cases) auto
+next
+  case (snoc y ys)
+  show ?case
+    by (simp only: append.assoc [symmetric] suffixes_snoc snoc.IH) simp
+qed
+
+lemma suffixes_eq_snoc:
+  "suffixes ys = xs @ [x] \<longleftrightarrow>
+     (ys = [] \<and> xs = [] \<or> (\<exists>z zs. ys = z#zs \<and> xs = suffixes zs)) \<and> x = ys"
+  by (cases ys) auto
+
+lemma suffixes_tailrec [code]: 
+  "suffixes xs = rev (snd (foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) ([],[[]]) (rev xs)))"
+proof -
+  have "foldl (\<lambda>(acc1, acc2) x. (x#acc1, (x#acc1)#acc2)) (ys, ys # zs) (rev xs) =
+          (xs @ ys, rev (map (\<lambda>as. as @ ys) (suffixes xs)) @ zs)" for ys zs
+  proof (induction xs arbitrary: ys zs)
+    case (Cons x xs ys zs)
+    from Cons.IH[of ys zs]
+      show ?case by (simp add: o_def case_prod_unfold)
+  qed simp_all
+  from this [of "[]" "[]"] show ?thesis by simp
+qed
+  
+lemma set_suffixes_eq: "set (suffixes xs) = {ys. suffix ys xs}"
+  by auto
+    
+lemma card_set_suffixes [simp]: "card (set (suffixes xs)) = Suc (length xs)"
+  by (subst distinct_card) auto
+  
+lemma set_suffixes_append: 
+  "set (suffixes (xs @ ys)) = set (suffixes ys) \<union> {xs' @ ys |xs'. xs' \<in> set (suffixes xs)}"
+  by (subst suffixes_append, cases xs rule: rev_cases) auto
+
+
+lemma suffixes_conv_prefixes: "suffixes xs = map rev (prefixes (rev xs))"
+  by (induction xs) auto
+
+lemma prefixes_conv_suffixes: "prefixes xs = map rev (suffixes (rev xs))"
+  by (induction xs) auto
+    
+lemma prefixes_rev: "prefixes (rev xs) = map rev (suffixes xs)"
+  by (induction xs) auto
+    
+lemma suffixes_rev: "suffixes (rev xs) = map rev (prefixes xs)"
+  by (induction xs) auto
+
 
 subsection \<open>Homeomorphic embedding on lists\<close>
 
@@ -654,7 +855,7 @@
 lemma list_emb_strict_suffix:
   assumes "list_emb P xs ys" and "strict_suffix ys zs"
   shows "list_emb P xs zs"
-  using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def)
+  using assms(2) and list_emb_append2 [OF assms(1)] by (auto simp: strict_suffix_def suffix_def)
 
 lemma list_emb_suffix:
   assumes "list_emb P xs ys" and "suffix ys zs"
@@ -703,11 +904,30 @@
   obtains y where "y \<in> set ys" and "P x y"
   using assms by (induct) auto
 
+lemma list_emb_Cons_iff1 [simp]:
+  assumes "P x y"
+  shows   "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P xs ys"
+  using assms by (subst list_emb.simps) (auto dest: list_emb_ConsD)
+
+lemma list_emb_Cons_iff2 [simp]:
+  assumes "\<not>P x y"
+  shows   "list_emb P (x#xs) (y#ys) \<longleftrightarrow> list_emb P (x#xs) ys"
+  using assms by (subst list_emb.simps) auto
+
+lemma list_emb_code [code]:
+  "list_emb P [] ys \<longleftrightarrow> True"
+  "list_emb P (x#xs) [] \<longleftrightarrow> False"
+  "list_emb P (x#xs) (y#ys) \<longleftrightarrow> (if P x y then list_emb P xs ys else list_emb P (x#xs) ys)"
+  by simp_all
+  
+
 
 subsection \<open>Sublists (special case of homeomorphic embedding)\<close>
 
 abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
+  
+definition strict_sublist where "strict_sublist xs ys \<longleftrightarrow> xs \<noteq> ys \<and> sublisteq xs ys"
 
 lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
 
@@ -718,11 +938,6 @@
 lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
   by (metis list_emb_length linorder_not_less)
 
-lemma [code]:
-  "list_emb P [] ys \<longleftrightarrow> True"
-  "list_emb P (x#xs) [] \<longleftrightarrow> False"
-  by (simp_all)
-
 lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
   by (induct xs, simp, blast dest: list_emb_ConsD)
 
@@ -735,33 +950,50 @@
   shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
   using assms by (cases) auto
 
-lemma sublisteq_Cons2_iff [simp, code]:
+lemma sublisteq_Cons2_iff [simp]:
   "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
-  by (metis list_emb_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
+  by simp
 
 lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
   by (induct zs) simp_all
-
-lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
+    
+interpretation sublist_order: order sublisteq strict_sublist
+proof
+  fix xs ys :: "'a list"
+  {
+    assume "sublisteq xs ys" and "sublisteq ys xs"
+    thus "xs = ys"
+    proof (induct)
+      case list_emb_Nil
+      from list_emb_Nil2 [OF this] show ?case by simp
+    next
+      case list_emb_Cons2
+      thus ?case by simp
+    next
+      case list_emb_Cons
+      hence False using sublisteq_Cons' by fastforce
+      thus ?case ..
+    qed
+  }
+  thus "strict_sublist xs ys \<longleftrightarrow> (sublisteq xs ys \<and> \<not>sublisteq ys xs)"
+    by (auto simp: strict_sublist_def)
+qed (auto simp: list_emb_refl intro: list_emb_trans)
 
-lemma sublisteq_antisym:
-  assumes "sublisteq xs ys" and "sublisteq ys xs"
-  shows "xs = ys"
-using assms
-proof (induct)
-  case list_emb_Nil
-  from list_emb_Nil2 [OF this] show ?case by simp
+lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublisteq xs ys"
+proof
+  assume "xs \<in> set (sublists ys)"
+  thus "sublisteq xs ys"
+    by (induction ys arbitrary: xs) (auto simp: Let_def)
 next
-  case list_emb_Cons2
-  thus ?case by simp
-next
-  case list_emb_Cons
-  hence False using sublisteq_Cons' by fastforce
-  thus ?case ..
+  have [simp]: "[] \<in> set (sublists ys)" for ys :: "'a list" 
+    by (induction ys) (auto simp: Let_def)
+  assume "sublisteq xs ys"
+  thus "xs \<in> set (sublists ys)"
+    by (induction xs ys rule: list_emb.induct) (auto simp: Let_def)
 qed
 
-lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
-  by (rule list_emb_trans [of _ _ _ "op ="]) auto
+lemma set_sublists_eq: "set (sublists ys) = {xs. sublisteq xs ys}"
+  by auto
 
 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   by (auto dest: list_emb_length)
@@ -806,9 +1038,31 @@
   moreover assume ?l
   ultimately show ?r by blast
 next
-  assume ?r then show ?l by (metis list_emb_append_mono sublisteq_refl)
+  assume ?r then show ?l by (metis list_emb_append_mono sublist_order.order_refl)
 qed
 
+lemma sublisteq_append_iff: 
+  "sublisteq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> sublisteq xs1 ys \<and> sublisteq xs2 zs)"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs thus ?rhs
+  proof (induction xs "ys @ zs" arbitrary: ys zs rule: list_emb.induct)
+    case (list_emb_Cons xs ws y ys zs)
+    from list_emb_Cons(2)[of "tl ys" zs] and list_emb_Cons(2)[of "[]" "tl zs"] and list_emb_Cons(1,3)
+      show ?case by (cases ys) auto
+  next
+    case (list_emb_Cons2 x y xs ws ys zs)
+    from list_emb_Cons2(3)[of "tl ys" zs] and list_emb_Cons2(3)[of "[]" "tl zs"]
+       and list_emb_Cons2(1,2,4)
+    show ?case by (cases ys) (auto simp: Cons_eq_append_conv)
+  qed auto
+qed (auto intro: list_emb_append_mono)
+
+lemma sublisteq_appendE [case_names append]: 
+  assumes "sublisteq xs (ys @ zs)"
+  obtains xs1 xs2 where "xs = xs1 @ xs2" "sublisteq xs1 ys" "sublisteq xs2 zs"
+  using assms by (subst (asm) sublisteq_append_iff) auto
+
 lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   by (induct zs) auto
 
diff -r f35abc25d7b1 -r a6ed757b8585 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Wed May 17 23:13:56 2017 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Thu May 18 12:02:21 2017 +0200
@@ -35,9 +35,9 @@
   show "xs \<le> xs"
     by (simp add: less_eq_list_def)
   show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
-    using that unfolding less_eq_list_def by (rule sublisteq_antisym)
+    using that unfolding less_eq_list_def by (rule sublist_order.antisym)
   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
-    using that unfolding less_eq_list_def by (rule sublisteq_trans)
+    using that unfolding less_eq_list_def by (rule sublist_order.order_trans)
 qed
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =