# HG changeset patch
# User nipkow
# Date 1651641620 -7200
# Node ID 53a60eae475f720240e12bae9563b1dfa01d5fd1
# Parent  d1417d9c6debb0c5a3513d1912614fb82bc96bee
added lemma

diff -r d1417d9c6deb -r 53a60eae475f src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 22 16:55:48 2022 +0200
+++ b/src/HOL/List.thy	Wed May 04 07:20:20 2022 +0200
@@ -970,6 +970,8 @@
 lemma tl_append2 [simp]: "xs \<noteq> [] \<Longrightarrow> tl (xs @ ys) = tl xs @ ys"
 by (simp add: tl_append split: list.split)
 
+lemma tl_append_if: "tl (xs @ ys) = (if xs = [] then tl ys else tl xs @ ys)"
+by (simp)
 
 lemma Cons_eq_append_conv: "x#xs = ys@zs =
  (ys = [] \<and> x#xs = zs \<or> (\<exists>ys'. x#ys' = ys \<and> xs = ys'@zs))"