multiset operations with canonical argument order
authorhaftmann
Thu Oct 22 16:52:06 2009 +0200 (2009-10-22)
changeset 330783aea60ca3900
parent 33077 3c9cf88ec841
child 33079 06a48bbeb22a
multiset operations with canonical argument order
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Oct 22 16:52:06 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Oct 22 16:52:06 2009 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4  
     1.5    (*lists as multisets*)
     1.6    val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
     1.7 -  val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.8 +  val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     1.9  
    1.10    (*orders*)
    1.11    val is_equal: order -> bool
    1.12 @@ -858,11 +858,10 @@
    1.13  
    1.14  (** lists as multisets **)
    1.15  
    1.16 -fun remove1 _ _ [] = raise Empty
    1.17 -  | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
    1.18 +fun remove1 eq x [] = []
    1.19 +  | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys;
    1.20  
    1.21 -fun submultiset _ ([], _)  = true
    1.22 -  | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
    1.23 +fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;
    1.24  
    1.25  
    1.26