src/HOL/List.thy

   "\<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)
 
+lemma butlast_rev [simp]: "butlast (rev xs) = rev (tl xs)"
+  by (cases xs) simp_all
+
 
 subsubsection \<open>\<^const>\<open>take\<close> and \<^const>\<open>drop\<close>\<close>
 
 lemma take_0: "take 0 xs = []"
   by (induct xs) auto

   by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
 
 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
   by(simp add:upt_conv_Cons)
 
-lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
+lemma tl_upt [simp]: "tl [m..<n] = [Suc m..<n]"
   by (simp add: upt_rec)
 
 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
   by(cases j)(auto simp: upt_Suc_append)