src/Pure/library.ML
changeset 22142 2b54aa7586e2
parent 21962 279b129498b6
child 22256 23f3ca04d3b3
     1.1 --- a/src/Pure/library.ML	Sat Jan 20 14:27:46 2007 +0100
     1.2 +++ b/src/Pure/library.ML	Sun Jan 21 13:26:44 2007 +0100
     1.3 @@ -194,6 +194,10 @@
     1.4    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
     1.5    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
     1.6  
     1.7 +  (* lists as multisets *)
     1.8 +  val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
     1.9 +  val gen_submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.10 +
    1.11    (*lists as tables -- see also Pure/General/alist.ML*)
    1.12    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.13    val merge_lists: ''a list -> ''a list -> ''a list
    1.14 @@ -650,7 +654,6 @@
    1.15  fun suffixes1 xs = map rev (prefixes1 (rev xs));
    1.16  fun suffixes xs = [] :: suffixes1 xs;
    1.17  
    1.18 -
    1.19  (** integers **)
    1.20  
    1.21  fun gcd (x, y) =
    1.22 @@ -933,6 +936,16 @@
    1.23    in dups end;
    1.24  
    1.25  
    1.26 +(** lists as multisets **)
    1.27 +
    1.28 +fun remove1 _ _ [] = raise Empty
    1.29 +  | remove1 eq y (x::xs) = if eq(y,x) then xs else x :: remove1 eq y xs;
    1.30 +
    1.31 +fun gen_submultiset _  ([],    _)  = true
    1.32 +  | gen_submultiset eq (x::xs, ys) =
    1.33 +      member eq ys x  andalso  gen_submultiset eq (xs, remove1 eq x ys);
    1.34 +
    1.35 +
    1.36  (** association lists -- legacy operations **)
    1.37  
    1.38  fun gen_merge_lists _ xs [] = xs