# HG changeset patch
# User wenzelm
# Date 1180905408 -7200
# Node ID 9e04da929160b7f14017697f9eed8ff242fea170
# Parent  87ad6e8a5f2cd0cac4460fc51d4886372d215b8b
added flip (from General/basics.ML);
renamed gen_submultiset to submultiset;
moved downto0 to pattern.ML;
moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML;
moved plural to HOL/Tools/fundef_lib.ML;
removed obsolete seq;
simplified chop, fold2;

diff -r 87ad6e8a5f2c -r 9e04da929160 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Jun 03 23:16:47 2007 +0200
+++ b/src/Pure/library.ML	Sun Jun 03 23:16:48 2007 +0200
@@ -21,6 +21,7 @@
   (*functions*)
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
+  val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
@@ -129,7 +130,6 @@
   val dec: int ref -> int
   val upto: int * int -> int list
   val downto: int * int -> int list
-  val downto0: int list * int -> bool
   val radixpand: int * int -> int list
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
@@ -159,7 +159,6 @@
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
   val unsuffix: string -> string -> string
-  val plural: 'a -> 'a -> 'b list -> 'a
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
 
@@ -193,14 +192,9 @@
   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
 
-  (* lists as multisets *)
+  (*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
-  val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
+  val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
 
   (*balanced trees*)
   exception Balance
@@ -256,7 +250,6 @@
   val take: int * 'a list -> 'a list
   val drop: int * 'a list -> 'a list
   val last_elem: 'a list -> 'a
-  val seq: ('a -> unit) -> 'a list -> unit
 end;
 
 structure Library: LIBRARY =
@@ -266,6 +259,7 @@
 
 fun I x = x;
 fun K x = fn _ => x;
+fun flip f x y = f y x;
 fun curry f x y = f (x, y);
 fun uncurry f (x, y) = f x y;
 
@@ -346,7 +340,6 @@
 
 fun swap (x, y) = (y, x);
 
-(*apply function to components*)
 fun apfst f (x, y) = (f x, y);
 fun apsnd f (x, y) = (x, f y);
 fun pairself f (x, y) = (f x, f y);
@@ -457,7 +450,9 @@
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
 
-fun chop n xs = unfold_rev n dest xs;
+fun chop 0 xs = ([], xs)
+  | chop _ [] = ([], [])
+  | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
 (*take the first n elements from a list*)
 fun take (n, []) = []
@@ -541,10 +536,6 @@
 fun fold_burrow f xss s =
   apfst (unflat xss) (f (flat xss) s);
 
-(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
-  (proc x1; ...; proc xn) for side effects*)
-val seq = List.app;
-
 (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
 fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
   | separate _ xs = xs;
@@ -586,12 +577,9 @@
   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
   | map2 _ _ _ = raise UnequalLengths;
 
-fun fold2 f =
-  let
-    fun fold_aux [] [] z = z
-      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
-      | fold_aux _ _ _ = raise UnequalLengths;
-  in fold_aux end;
+fun fold2 f [] [] z = z
+  | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
+  | fold2 f _ _ _ = raise UnequalLengths;
 
 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
@@ -625,10 +613,10 @@
 
 fun chop_prefix eq ([], ys) = ([], ([], ys))
   | chop_prefix eq (xs, []) = ([], (xs, []))
-  | chop_prefix eq (xs as x::xs', ys as y::ys') =
+  | chop_prefix eq (xs as x :: xs', ys as y :: ys') =
       if eq (x, y) then
         let val (ps', xys'') = chop_prefix eq (xs', ys')
-        in (x::ps', xys'') end
+        in (x :: ps', xys'') end
       else ([], (xs, ys));
 
 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
@@ -647,6 +635,8 @@
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
 
+
+
 (** integers **)
 
 fun gcd (x, y) =
@@ -670,10 +660,6 @@
 fun (i downto j) =
   if i < j then [] else i :: (i - 1 downto j);
 
-(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
-fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
-  | downto0 ([], n) = n = ~1;
-
 
 (* convert integers to strings *)
 
@@ -699,8 +685,8 @@
 fun signed_string_of_int i =
   if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
 
-fun string_of_indexname (a,0) = a
-  | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
+fun string_of_indexname (a, 0) = a
+  | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i;
 
 
 (* read integers *)
@@ -797,10 +783,6 @@
   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   else raise Fail "unsuffix";
 
-(* Ex: "The variable" ^ plural " is" "s are" vs *)
-fun plural sg pl [x] = sg
-  | plural sg pl _ = pl
-
 fun replicate_string 0 _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =
@@ -808,6 +790,7 @@
       else replicate_string (k div 2) (a ^ a) ^ a;
 
 
+
 (** lists as sets -- see also Pure/General/ord_list.ML **)
 
 (*canonical member, insert, remove*)
@@ -935,24 +918,15 @@
   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);
-
+  | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
 
-(** association lists -- legacy operations **)
+fun submultiset _ ([], _)  = true
+  | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
 
-fun gen_merge_lists _ xs [] = xs
-  | gen_merge_lists _ [] ys = ys
-  | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
-
-fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
-fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
 
 
 (** balanced trees **)
@@ -1093,6 +1067,7 @@
   in pick (random_range 1 sum) xs end;
 
 
+
 (** current directory **)
 
 val cd = OS.FileSys.chDir;