merged
authorhaftmann
Wed Oct 21 12:12:21 2009 +0200 (2009-10-21)
changeset 33050fe166e8b9f07
parent 33043 ff71cadefb14
parent 33049 c38f02fdf35d
child 33051 3797ae7ffe3c
merged
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/sat_solver.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 12:08:52 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 12:12:21 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
     1.5    (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
     1.6  
     1.7 -fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     1.8 +fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     1.9  
    1.10  val fresh_prod = thm "fresh_prod";
    1.11  
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 12:08:52 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 12:12:21 2009 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4      [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
     2.5       @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
     2.6  
     2.7 -fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
     2.8 +fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     2.9  
    2.10  val perm_bool = mk_meta_eq (thm "perm_bool");
    2.11  val perm_boolI = thm "perm_boolI";
     3.1 --- a/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 12:08:52 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 12:12:21 2009 +0200
     3.3 @@ -90,7 +90,7 @@
     3.4        IntGraph.empty
     3.5          |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
     3.6          |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
     3.7 -               if i = j orelse null (inter (op =) (c1, t2))
     3.8 +               if i = j orelse null (inter (op =) c1 t2)
     3.9                 then I else IntGraph.add_edge_acyclic (i,j))
    3.10               num_branches num_branches
    3.11      end
     4.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 12:08:52 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 12:12:21 2009 +0200
     4.3 @@ -101,7 +101,7 @@
     4.4            let
     4.5              val t = Pattern.rewrite_term thy sigma [] feq1
     4.6            in
     4.7 -            fold_rev Logic.all (inter (op =) (map Free (frees_in_term ctx t), vs')) t
     4.8 +            fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
     4.9            end
    4.10      in
    4.11        map instantiate substs
     5.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:08:52 2009 +0200
     5.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:12:21 2009 +0200
     5.3 @@ -884,7 +884,7 @@
     5.4   fun isolate_monomials vars tm =
     5.5   let 
     5.6    val (cmons,vmons) =
     5.7 -    List.partition (fn m => null (inter op aconvc (frees m, vars)))
     5.8 +    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
     5.9                     (striplist ring_dest_add tm)
    5.10    val cofactors = map (fn v => find_multipliers v vmons) vars
    5.11    val cnc = if null cmons then zero_tm
     6.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:08:52 2009 +0200
     6.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:12:21 2009 +0200
     6.3 @@ -482,7 +482,7 @@
     6.4  fun constrain cs [] = []
     6.5    | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
     6.6        NONE => xs
     6.7 -    | SOME xs' => inter (op =) (xs, xs')) :: constrain cs ys;
     6.8 +    | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
     6.9  
    6.10  fun mk_extra_defs thy defs gr dep names module ts =
    6.11    Library.foldl (fn (gr, name) =>
     7.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Oct 21 12:08:52 2009 +0200
     7.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 21 12:12:21 2009 +0200
     7.3 @@ -209,7 +209,7 @@
     7.4        (case optf of
     7.5           NONE => fs
     7.6         | SOME f => AList.update op = (u, the_default f
     7.7 -           (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs));
     7.8 +           (Option.map (fn g => inter (op =) g f) (AList.lookup op = fs u))) fs));
     7.9  
    7.10  
    7.11  (**************************************************************)
     8.1 --- a/src/HOL/Tools/record.ML	Wed Oct 21 12:08:52 2009 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Wed Oct 21 12:12:21 2009 +0200
     8.3 @@ -1834,7 +1834,7 @@
     8.4      val extN = full bname;
     8.5      val types = map snd fields;
     8.6      val alphas_fields = fold Term.add_tfree_namesT types [];
     8.7 -    val alphas_ext = inter (op =) (alphas, alphas_fields);
     8.8 +    val alphas_ext = inter (op =) alphas_fields alphas;
     8.9      val len = length fields;
    8.10      val variants =
    8.11        Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
     9.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:08:52 2009 +0200
     9.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:12:21 2009 +0200
     9.3 @@ -471,7 +471,7 @@
     9.4          | forced_vars False             = []
     9.5          | forced_vars (BoolVar i)       = [i]
     9.6          | forced_vars (Not (BoolVar i)) = [~i]
     9.7 -        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
     9.8 +        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1) (forced_vars fm2)
     9.9          | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1) (forced_vars fm2)
    9.10          (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
    9.11          (* precedence, and the next partial evaluation of the formula returns 'False'. *)
    10.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 12:08:52 2009 +0200
    10.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 12:12:21 2009 +0200
    10.3 @@ -74,7 +74,7 @@
    10.4  fun proc ss t =
    10.5    let val (divs,mods) = coll_div_mod t ([],[])
    10.6    in if null divs orelse null mods then NONE
    10.7 -     else case inter (op =) (divs, mods) of
    10.8 +     else case inter (op =) mods divs of
    10.9              pq :: _ => SOME (cancel ss t pq)
   10.10            | [] => NONE
   10.11    end
    11.1 --- a/src/Pure/General/name_space.ML	Wed Oct 21 12:08:52 2009 +0200
    11.2 +++ b/src/Pure/General/name_space.ML	Wed Oct 21 12:12:21 2009 +0200
    11.3 @@ -145,7 +145,7 @@
    11.4        space
    11.5        |> add_name' name name
    11.6        |> fold (del_name name)
    11.7 -        (if fully then names else inter (op =) (names, [Long_Name.base_name name]))
    11.8 +        (if fully then names else inter (op =) [Long_Name.base_name name] names)
    11.9        |> fold (del_name_extra name) (get_accesses space name)
   11.10      end;
   11.11  
    12.1 --- a/src/Pure/General/path.ML	Wed Oct 21 12:08:52 2009 +0200
    12.2 +++ b/src/Pure/General/path.ML	Wed Oct 21 12:12:21 2009 +0200
    12.3 @@ -42,7 +42,7 @@
    12.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    12.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    12.6    | check_elem chs =
    12.7 -      (case inter (op =) (["/", "\\", "$", ":"], chs) of
    12.8 +      (case inter (op =) ["/", "\\", "$", ":"] chs of
    12.9          [] => chs
   12.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
   12.11  
    13.1 --- a/src/Pure/library.ML	Wed Oct 21 12:08:52 2009 +0200
    13.2 +++ b/src/Pure/library.ML	Wed Oct 21 12:12:21 2009 +0200
    13.3 @@ -159,11 +159,11 @@
    13.4    val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    13.5    val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    13.6    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
    13.7 +  val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
    13.8    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    13.9    val mem: ''a * ''a list -> bool
   13.10    val mem_int: int * int list -> bool
   13.11    val mem_string: string * string list -> bool
   13.12 -  val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   13.13    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   13.14    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   13.15    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   13.16 @@ -782,6 +782,8 @@
   13.17  fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
   13.18  fun update eq x xs = cons x (remove eq x xs);
   13.19  
   13.20 +fun inter eq xs = filter (member eq xs);
   13.21 +
   13.22  fun union eq = fold (insert eq);
   13.23  fun subtract eq = fold (remove eq);
   13.24  
   13.25 @@ -797,16 +799,11 @@
   13.26  fun (x: int) mem_int xs = member (op =) xs x;
   13.27  fun (x: string) mem_string xs = member (op =) xs x;
   13.28  
   13.29 -(*intersection*)
   13.30 -fun inter eq ([], ys) = []
   13.31 -  | inter eq (x::xs, ys) =
   13.32 -      if member eq ys x then x :: inter eq (xs, ys)
   13.33 -      else inter eq (xs, ys);
   13.34  
   13.35 -(*subset*)
   13.36 +(* subset and set equality *)
   13.37 +
   13.38  fun subset eq (xs, ys) = forall (member eq ys) xs;
   13.39  
   13.40 -(*set equality*)
   13.41  fun eq_set eq (xs, ys) =
   13.42    eq_list eq (xs, ys) orelse
   13.43      (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
    14.1 --- a/src/Pure/pattern.ML	Wed Oct 21 12:08:52 2009 +0200
    14.2 +++ b/src/Pure/pattern.ML	Wed Oct 21 12:12:21 2009 +0200
    14.3 @@ -219,7 +219,7 @@
    14.4              if subset (op =) (js, is)
    14.5              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    14.6                   in Envir.update (((F, Fty), t), env) end
    14.7 -            else let val ks = inter (op =) (is, js)
    14.8 +            else let val ks = inter (op =) js is
    14.9                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
   14.10                       val (env',H) = Envir.genvar a (env,Hty)
   14.11                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    15.1 --- a/src/Pure/thm.ML	Wed Oct 21 12:08:52 2009 +0200
    15.2 +++ b/src/Pure/thm.ML	Wed Oct 21 12:12:21 2009 +0200
    15.3 @@ -1463,7 +1463,7 @@
    15.4      (case duplicates (op =) cs of
    15.5        a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
    15.6      | [] =>
    15.7 -      (case inter (op =) (cs, freenames) of
    15.8 +      (case inter (op =) cs freenames of
    15.9          a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
   15.10        | [] =>
   15.11          Thm (der,
    16.1 --- a/src/Pure/variable.ML	Wed Oct 21 12:08:52 2009 +0200
    16.2 +++ b/src/Pure/variable.ML	Wed Oct 21 12:12:21 2009 +0200
    16.3 @@ -301,7 +301,7 @@
    16.4      val names = names_of ctxt;
    16.5      val (xs', names') =
    16.6        if is_body ctxt then Name.variants xs names |>> map Name.skolem
    16.7 -      else (no_dups (inter (op =) (xs, ys)); no_dups (inter (op =) (xs, zs));
    16.8 +      else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs);
    16.9          (xs, fold Name.declare xs names));
   16.10    in ctxt |> new_fixes names' xs xs' end;
   16.11  
    17.1 --- a/src/Sequents/prover.ML	Wed Oct 21 12:08:52 2009 +0200
    17.2 +++ b/src/Sequents/prover.ML	Wed Oct 21 12:12:21 2009 +0200
    17.3 @@ -31,14 +31,14 @@
    17.4         dups);
    17.5  
    17.6  fun (Pack(safes,unsafes)) add_safes ths   = 
    17.7 -    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
    17.8 +    let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
    17.9          val ths' = subtract Thm.eq_thm_prop dups ths
   17.10      in
   17.11          Pack(sort (make_ord less) (ths'@safes), unsafes)
   17.12      end;
   17.13  
   17.14  fun (Pack(safes,unsafes)) add_unsafes ths = 
   17.15 -    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
   17.16 +    let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
   17.17          val ths' = subtract Thm.eq_thm_prop dups ths
   17.18      in
   17.19          Pack(safes, sort (make_ord less) (ths'@unsafes))