# HG changeset patch
# User nipkow
# Date 1097749132 -7200
# Node ID 5a21d9a8f14b620ec35b6a1edb5ff7de50f4fb0e
# Parent  9473137b35507bccfedfc94050abedb09cbf0306
Added a few lemmas

diff -r 9473137b3550 -r 5a21d9a8f14b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 13 07:40:13 2004 +0200
+++ b/src/HOL/List.thy	Thu Oct 14 12:18:52 2004 +0200
@@ -607,6 +607,9 @@
 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
 by (induct xs) auto
 
+lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
+by(induct xs) auto
+
 lemma set_rev [simp]: "set (rev xs) = set xs"
 by (induct xs) auto
 
@@ -1495,6 +1498,18 @@
 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
   by (induct_tac x, auto)
 
+lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
+by (induct xs) auto
+
+lemma length_remdups_eq[iff]:
+  "(length (remdups xs) = length xs) = (remdups xs = xs)"
+apply(induct xs)
+ apply auto
+apply(subgoal_tac "length (remdups xs) <= length xs")
+ apply arith
+apply(rule length_remdups_leq)
+done
+
 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
 by (induct xs) auto