# HG changeset patch
# User nipkow
# Date 1408975601 -7200
# Node ID 41ceac4450dc73b1006cc0a4c406187651da655c
# Parent  9a867afaab5a5786e6a050ae46b3eb78318a198f
added lemmas

diff -r 9a867afaab5a -r 41ceac4450dc src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 19 18:37:32 2014 +0200
+++ b/src/HOL/List.thy	Mon Aug 25 16:06:41 2014 +0200
@@ -3436,6 +3436,9 @@
 "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
 by force
 
+lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
+  by (induction xs rule: remdups_adj.induct) simp_all
+
 lemma remdups_adj_Cons: "remdups_adj (x # xs) =
   (case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
   by (induct xs arbitrary: x) (auto split: list.splits)
@@ -3444,6 +3447,13 @@
   "remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])"
   by (induct xs rule: remdups_adj.induct, simp_all)
 
+lemma remdups_adj_adjacent:
+  "Suc i < length (remdups_adj xs) \<Longrightarrow> remdups_adj xs ! i \<noteq> remdups_adj xs ! Suc i"
+proof (induction xs arbitrary: i rule: remdups_adj.induct)
+  case (3 x y xs i)
+  thus ?case by (cases i, cases "x = y") (simp, auto simp: hd_conv_nth[symmetric])
+qed simp_all
+
 lemma remdups_adj_rev[simp]: "remdups_adj (rev xs) = rev (remdups_adj xs)"
   by (induct xs rule: remdups_adj.induct, simp_all add: remdups_adj_append_two)