--- a/src/HOL/List.thy Fri Jul 07 11:32:06 2017 +0200
+++ b/src/HOL/List.thy Sat Jul 08 15:51:29 2017 +0200
@@ -3216,30 +3216,14 @@
"distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
by (induct xs) auto
-text \<open>Contributed by Stephan Merz:\<close>
-lemma distinct_split_list:
- assumes "distinct (xs @ x # ys)" and "xs @ x # ys = xs' @ x # ys'"
- shows "xs = xs'" "ys = ys'"
+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'"
- proof (rule ccontr)
- assume c: "xs \<noteq> xs'"
- show "False"
- proof (cases "size xs < size xs'")
- case True
- with assms(2) have "x \<in> set xs'"
- by (metis in_set_conv_nth nth_append nth_append_length)
- with assms show ?thesis by auto
- next
- case False
- with c assms(2) have "size xs' < size xs"
- by (meson append_eq_append_conv linorder_neqE_nat)
- with assms(2) have "x \<in> set xs"
- by (metis in_set_conv_nth nth_append nth_append_length)
- with assms(1) show ?thesis by auto
- qed
- qed
- with assms(2) show "ys = ys'" by simp
+ 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"