--- a/src/HOL/List.ML Wed Feb 13 10:48:29 2002 +0100
+++ b/src/HOL/List.ML Thu Feb 14 11:50:52 2002 +0100
@@ -1277,8 +1277,14 @@
qed_spec_mp "take_equalityI";
-(** nodups & remdups **)
-section "nodups & remdups";
+(** distinct & remdups **)
+section "distinct & remdups";
+
+Goal "distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})";
+by(induct_tac "xs" 1);
+by Auto_tac;
+qed "distinct_append";
+Addsimps [distinct_append];
Goal "set(remdups xs) = set xs";
by (induct_tac "xs" 1);
@@ -1287,15 +1293,15 @@
qed "set_remdups";
Addsimps [set_remdups];
-Goal "nodups(remdups xs)";
+Goal "distinct(remdups xs)";
by (induct_tac "xs" 1);
by Auto_tac;
-qed "nodups_remdups";
+qed "distinct_remdups";
-Goal "nodups xs --> nodups (filter P xs)";
+Goal "distinct xs --> distinct (filter P xs)";
by (induct_tac "xs" 1);
by Auto_tac;
-qed_spec_mp "nodups_filter";
+qed_spec_mp "distinct_filter";
(** replicate **)
section "replicate";
--- a/src/HOL/List.thy Wed Feb 13 10:48:29 2002 +0100
+++ b/src/HOL/List.thy Thu Feb 14 11:50:52 2002 +0100
@@ -31,8 +31,8 @@
rev :: 'a list => 'a list
zip :: "'a list => 'b list => ('a * 'b) list"
upt :: nat => nat => nat list ("(1[_../_'(])")
- remdups :: 'a list => 'a list
- null, nodups :: "'a list => bool"
+ remdups :: "'a list => 'a list"
+ null, "distinct" :: "'a list => bool"
replicate :: nat => 'a => 'a list
nonterminals
@@ -158,8 +158,8 @@
upt_0 "[i..0(] = []"
upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
primrec
- "nodups [] = True"
- "nodups (x#xs) = (x ~: set xs & nodups xs)"
+ "distinct [] = True"
+ "distinct (x#xs) = (x ~: set xs & distinct xs)"
primrec
"remdups [] = []"
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"