# HG changeset patch
# User haftmann
# Date 1271921439 -7200
# Node ID c6ca9e258269fdc7a7492cf15cc4c59c36db9759
# Parent  42bd879dc1b00b43b814eaca6fe4ca356b5deb55
lemmas concerning remdups

diff -r 42bd879dc1b0 -r c6ca9e258269 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 22 09:30:36 2010 +0200
+++ b/src/HOL/List.thy	Thu Apr 22 09:30:39 2010 +0200
@@ -2906,6 +2906,10 @@
   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
 qed
 
+lemma remdups_remdups:
+  "remdups (remdups xs) = remdups xs"
+  by (induct xs) simp_all
+
 
 subsubsection {* @{const insert} *}
 
@@ -2929,6 +2933,10 @@
   "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
   by (simp add: List.insert_def)
 
+lemma insert_remdups:
+  "List.insert x (remdups xs) = remdups (List.insert x xs)"
+  by (simp add: List.insert_def)
+
 
 subsubsection {* @{text remove1} *}
 
@@ -2975,6 +2983,10 @@
 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
 by (induct xs) simp_all
 
+lemma remove1_remdups:
+  "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
+  by (induct xs) simp_all
+
 
 subsubsection {* @{text removeAll} *}