src/Pure/library.ML
changeset 33037 b22e44496dc2
parent 32978 a473ba9a221d
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/library.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -11,8 +11,7 @@
     1.4  infix 2 ?
     1.5  infix 3 o oo ooo oooo
     1.6  infix 4 ~~ upto downto
     1.7 -infix orf andf \ \\ mem mem_int mem_string union union_int
     1.8 -  union_string inter inter_int inter_string subset subset_int subset_string
     1.9 +infix orf andf \ \\ mem mem_int mem_string
    1.10  
    1.11  signature BASIC_LIBRARY =
    1.12  sig
    1.13 @@ -163,19 +162,8 @@
    1.14    val mem: ''a * ''a list -> bool
    1.15    val mem_int: int * int list -> bool
    1.16    val mem_string: string * string list -> bool
    1.17 -  val union: ''a list * ''a list -> ''a list
    1.18 -  val union_int: int list * int list -> int list
    1.19 -  val union_string: string list * string list -> string list
    1.20    val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.21    val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.22 -  val inter: ''a list * ''a list -> ''a list
    1.23 -  val inter_int: int list * int list -> int list
    1.24 -  val inter_string: string list * string list -> string list
    1.25 -  val subset: ''a list * ''a list -> bool
    1.26 -  val subset_int: int list * int list -> bool
    1.27 -  val subset_string: string list * string list -> bool
    1.28 -  val eq_set: ''a list * ''a list -> bool
    1.29 -  val eq_set_string: string list * string list -> bool
    1.30    val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.31    val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.32    val \ : ''a list * ''a -> ''a list
    1.33 @@ -811,70 +799,20 @@
    1.34  fun (x: string) mem_string xs = member (op =) xs x;
    1.35  
    1.36  (*union of sets represented as lists: no repetitions*)
    1.37 -fun xs union [] = xs
    1.38 -  | [] union ys = ys
    1.39 -  | (x :: xs) union ys = xs union (insert (op =) x ys);
    1.40 -
    1.41 -(*union of sets, optimized version for ints*)
    1.42 -fun (xs:int list) union_int [] = xs
    1.43 -  | [] union_int ys = ys
    1.44 -  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
    1.45 -
    1.46 -(*union of sets, optimized version for strings*)
    1.47 -fun (xs:string list) union_string [] = xs
    1.48 -  | [] union_string ys = ys
    1.49 -  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
    1.50 -
    1.51 -(*generalized union*)
    1.52  fun gen_union eq (xs, []) = xs
    1.53    | gen_union eq ([], ys) = ys
    1.54    | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
    1.55  
    1.56 -
    1.57  (*intersection*)
    1.58 -fun [] inter ys = []
    1.59 -  | (x :: xs) inter ys =
    1.60 -      if x mem ys then x :: (xs inter ys) else xs inter ys;
    1.61 -
    1.62 -(*intersection, optimized version for ints*)
    1.63 -fun ([]:int list) inter_int ys = []
    1.64 -  | (x :: xs) inter_int ys =
    1.65 -      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
    1.66 -
    1.67 -(*intersection, optimized version for strings *)
    1.68 -fun ([]:string list) inter_string ys = []
    1.69 -  | (x :: xs) inter_string ys =
    1.70 -      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
    1.71 -
    1.72 -(*generalized intersection*)
    1.73  fun gen_inter eq ([], ys) = []
    1.74    | gen_inter eq (x::xs, ys) =
    1.75        if member eq ys x then x :: gen_inter eq (xs, ys)
    1.76        else gen_inter eq (xs, ys);
    1.77  
    1.78 -
    1.79  (*subset*)
    1.80 -fun [] subset ys = true
    1.81 -  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
    1.82 -
    1.83 -(*subset, optimized version for ints*)
    1.84 -fun ([]: int list) subset_int ys = true
    1.85 -  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
    1.86 -
    1.87 -(*subset, optimized version for strings*)
    1.88 -fun ([]: string list) subset_string ys = true
    1.89 -  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
    1.90 +fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
    1.91  
    1.92  (*set equality*)
    1.93 -fun eq_set (xs, ys) =
    1.94 -  xs = ys orelse (xs subset ys andalso ys subset xs);
    1.95 -
    1.96 -(*set equality for strings*)
    1.97 -fun eq_set_string ((xs: string list), ys) =
    1.98 -  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
    1.99 -
   1.100 -fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
   1.101 -
   1.102  fun gen_eq_set eq (xs, ys) =
   1.103    eq_list eq (xs, ys) orelse
   1.104      (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));