--- a/src/HOL/List.thy Fri May 27 23:58:24 2016 +0200
+++ b/src/HOL/List.thy Sun May 29 14:10:48 2016 +0200
@@ -1002,6 +1002,12 @@
(ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
by(cases ys) auto
+lemma longest_common_prefix:
+ "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys'
+ \<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
+by (induct xs ys rule: list_induct2')
+ (blast, blast, blast,
+ metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
@@ -1961,6 +1967,12 @@
"xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
by fastforce
+corollary longest_common_suffix:
+ "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
+ \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
+using longest_common_prefix[of "rev xs" "rev ys"]
+unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+
subsubsection \<open>@{const take} and @{const drop}\<close>