# HG changeset patch
# User nipkow
# Date 1169382404 -3600
# Node ID 2b54aa7586e2c5c72493f91345fa8aba2a2c997d
# Parent  a91334ece12a19e0181077cffa29f5335923d129
Added lists-as-multisets functions

diff -r a91334ece12a -r 2b54aa7586e2 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jan 20 14:27:46 2007 +0100
+++ b/src/Pure/library.ML	Sun Jan 21 13:26:44 2007 +0100
@@ -194,6 +194,10 @@
   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
 
+  (* lists as multisets *)
+  val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
+  val gen_submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+
   (*lists as tables -- see also Pure/General/alist.ML*)
   val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   val merge_lists: ''a list -> ''a list -> ''a list
@@ -650,7 +654,6 @@
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
 
-
 (** integers **)
 
 fun gcd (x, y) =
@@ -933,6 +936,16 @@
   in dups end;
 
 
+(** lists as multisets **)
+
+fun remove1 _ _ [] = raise Empty
+  | remove1 eq y (x::xs) = if eq(y,x) then xs else x :: remove1 eq y xs;
+
+fun gen_submultiset _  ([],    _)  = true
+  | gen_submultiset eq (x::xs, ys) =
+      member eq ys x  andalso  gen_submultiset eq (xs, remove1 eq x ys);
+
+
 (** association lists -- legacy operations **)
 
 fun gen_merge_lists _ xs [] = xs