# HG changeset patch
# User nipkow
# Date 1499527991 -7200
# Node ID 3bc892346a6b1fbd4a4962957fb7f5914309ae7c
# Parent  5be685bbd16cba13938ee51a9b0703137c3fcfcb
revised lemma

diff -r 5be685bbd16c -r 3bc892346a6b src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jul 08 15:51:34 2017 +0200
+++ b/src/HOL/List.thy	Sat Jul 08 17:33:11 2017 +0200
@@ -1443,6 +1443,11 @@
   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
   by (induct xs) auto
 
+lemma append_Cons_eq_iff:
+  "\<lbrakk> x \<notin> set xs; x \<notin> set ys \<rbrakk> \<Longrightarrow>
+   xs @ x # ys = xs' @ x # ys' \<longleftrightarrow> (xs = xs' \<and> ys = ys')"
+by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2)
+
 
 subsubsection \<open>@{const filter}\<close>
 
@@ -3216,16 +3221,6 @@
   "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
 by (induct xs) auto
 
-lemma app_Cons_app_eqD:
-assumes "xs @ x # ys = xs' @ x # ys'" and "x \<notin> set xs" and "x \<notin> set ys"
-shows "xs = xs'" "ys = ys'"
-proof -
-  show "xs = xs'"
-    using assms
-    by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2)
-  with assms show "ys = ys'" by simp
-qed
-
 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
 by(induct xs) auto