# HG changeset patch
# User nipkow
# Date 886787718 -3600
# Node ID 579e0ef2df6bbc545a221e381f89c101124d02e1
# Parent  ff8eca799c8fe52ab24f7fc527e6a73fe5feee69
Added `remdups'
nodup -> nodups

diff -r ff8eca799c8f -r 579e0ef2df6b src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Feb 06 11:18:29 1998 +0100
+++ b/src/HOL/List.ML	Fri Feb 06 18:55:18 1998 +0100
@@ -350,6 +350,19 @@
 qed "set_map";
 Addsimps [set_map];
 
+goal thy "set(map f xs) = f``(set xs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "set_map";
+Addsimps [set_map];
+
+goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
+by (induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by(Blast_tac 1);
+qed "in_set_filter";
+Addsimps [in_set_filter];
+
 
 (** list_all **)
 
@@ -384,10 +397,22 @@
 qed "filter_append";
 Addsimps [filter_append];
 
-goal thy "size (filter P xs) <= size xs";
+goal thy "filter (%x. True) xs = xs";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "filter_True";
+Addsimps [filter_True];
+
+goal thy "filter (%x. False) xs = []";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "filter_False";
+Addsimps [filter_False];
+
+goal thy "length (filter P xs) <= length xs";
 by (induct_tac "xs" 1);
  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
-qed "filter_size";
+qed "length_filter";
 
 
 (** concat **)
@@ -715,6 +740,30 @@
 qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
 						      (K [Simp_tac 1]);
+
+(** nodups & remdups **)
+section "nodups & remdups";
+
+goal thy "set(remdups xs) = set xs";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
+                                 addsplits [expand_if]) 1);
+qed "set_remdups";
+Addsimps [set_remdups];
+
+goal thy "nodups(remdups xs)";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+qed "nodups_remdups";
+
+goal thy "nodups xs --> nodups (filter P xs)";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+qed_spec_mp "nodups_filter";
+
 (** replicate **)
 section "replicate";
 
diff -r ff8eca799c8f -r 579e0ef2df6b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 06 11:18:29 1998 +0100
+++ b/src/HOL/List.thy	Fri Feb 06 18:55:18 1998 +0100
@@ -27,7 +27,8 @@
   tl, butlast :: 'a list => 'a list
   rev         :: 'a list => 'a list
   zip	      :: "'a list => 'b list => ('a * 'b) list"
-  nodup	      :: "'a list => bool"
+  remdups     :: 'a list => 'a list
+  nodups      :: "'a list => bool"
   replicate   :: nat => 'a => 'a list
 
 syntax
@@ -117,9 +118,12 @@
 primrec zip list
   "zip xs []     = []"
   "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
-primrec nodup list
-  "nodup []     = True"
-  "nodup (x#xs) = (x ~: set xs & nodup xs)"
+primrec nodups list
+  "nodups []     = True"
+  "nodups (x#xs) = (x ~: set xs & nodups xs)"
+primrec remdups list
+  "remdups [] = []"
+  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
 primrec replicate nat
 replicate_0   "replicate 0 x       = []"
 replicate_Suc "replicate (Suc n) x = x # replicate n x"
diff -r ff8eca799c8f -r 579e0ef2df6b src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Feb 06 11:18:29 1998 +0100
+++ b/src/HOL/equalities.ML	Fri Feb 06 18:55:18 1998 +0100
@@ -45,6 +45,9 @@
 goal thy "!!a. a:A ==> insert a A = A";
 by (Blast_tac 1);
 qed "insert_absorb";
+(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
+   in case of nested inserts!
+*)
 
 goal thy "insert x (insert x A) = insert x A";
 by (Blast_tac 1);