# HG changeset patch # User boehmes # Date 1256126884 -7200 # Node ID af06b784814dc25413cda1a580b4440e630392d5 # Parent 69780aef0531f5750f36212f39c513bfaeb1efe1# Parent 33aee615096990df7aa2a48c272d9e4dee757134 merged diff -r 69780aef0531 -r af06b784814d src/HOL/Fun.thy --- a/src/HOL/Fun.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Fun.thy Wed Oct 21 14:08:04 2009 +0200 @@ -78,6 +78,9 @@ lemma image_compose: "(f o g) ` r = f`(g`r)" by (simp add: comp_def, blast) +lemma vimage_compose: "(g \ f) -` x = f -` (g -` x)" + by auto + lemma UN_o: "UNION A (g o f) = UNION (f`A) g" by (unfold comp_def, blast) diff -r 69780aef0531 -r af06b784814d src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Wed Oct 21 14:08:04 2009 +0200 @@ -165,7 +165,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) val hol4_debug = Unsynchronized.ref false diff -r 69780aef0531 -r af06b784814d src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Wed Oct 21 14:08:04 2009 +0200 @@ -78,7 +78,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) fun print_shuffles thy = diff -r 69780aef0531 -r af06b784814d src/HOL/Library/Sum_Of_Squares.thy --- a/src/HOL/Library/Sum_Of_Squares.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Oct 21 14:08:04 2009 +0200 @@ -9,10 +9,10 @@ theory Sum_Of_Squares imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *) uses - ("positivstellensatz.ML") (* duplicate use!? -- cf. Euclidian_Space.thy *) - ("Sum_Of_Squares/sum_of_squares.ML") - ("Sum_Of_Squares/positivstellensatz_tools.ML") - ("Sum_Of_Squares/sos_wrapper.ML") + "positivstellensatz.ML" (* duplicate use!? -- cf. Euclidian_Space.thy *) + "Sum_Of_Squares/sum_of_squares.ML" + "Sum_Of_Squares/positivstellensatz_tools.ML" + "Sum_Of_Squares/sos_wrapper.ML" begin text {* @@ -28,13 +28,6 @@ without calling an external prover. *} -text {* setup sos tactic *} - -use "positivstellensatz.ML" -use "Sum_Of_Squares/positivstellensatz_tools.ML" -use "Sum_Of_Squares/sum_of_squares.ML" -use "Sum_Of_Squares/sos_wrapper.ML" - setup SOS_Wrapper.setup text {* Tests *} diff -r 69780aef0531 -r af06b784814d src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 14:08:04 2009 +0200 @@ -244,7 +244,7 @@ fun monomial_lcm m1 m2 = fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2))) - (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty); + (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1) (FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty); fun monomial_multidegree m = FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;; @@ -314,7 +314,7 @@ FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0; fun poly_variables p = - sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);; + sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);; (* Order monomials for human presentation. *) @@ -1059,8 +1059,8 @@ fun real_positivnullstellensatz_general prover linf d eqs leqs pol = let - val vars = fold_rev (curry (union (op aconvc)) o poly_variables) - (pol::eqs @ map fst leqs) [] + val vars = fold_rev (union (op aconvc) o poly_variables) + (pol :: eqs @ map fst leqs) [] val monoid = if linf then (poly_const rat_1,RealArith.Rational_lt rat_1):: (filter (fn (p,c) => multidegree p <= d) leqs) diff -r 69780aef0531 -r af06b784814d src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Library/normarith.ML Wed Oct 21 14:08:04 2009 +0200 @@ -286,7 +286,7 @@ val dests = distinct (op aconvc) (map snd rawdests) val srcfuns = map vector_lincomb sources val destfuns = map vector_lincomb dests - val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] + val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] val n = length srcfuns val nvs = 1 upto n val srccombs = srcfuns ~~ nvs diff -r 69780aef0531 -r af06b784814d src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 21 14:08:04 2009 +0200 @@ -620,7 +620,7 @@ | NONE => (case eqs of [] => let val vars = remove (op aconvc) one_tm - (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) + (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) in linear_ineqs vars (les,lts) end | (e,p)::es => if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else @@ -679,7 +679,7 @@ val le_pols = map rhs le val lt_pols = map rhs lt val aliens = filter is_alien - (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) + (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (eq_pols @ le_pols @ lt_pols) []) val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols) diff -r 69780aef0531 -r af06b784814d src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/SEQ.thy Wed Oct 21 14:08:04 2009 +0200 @@ -1089,10 +1089,10 @@ subsubsection {* Cauchy Sequences are Convergent *} -axclass complete_space \ metric_space - Cauchy_convergent: "Cauchy X \ convergent X" +class complete_space = + assumes Cauchy_convergent: "Cauchy X \ convergent X" -axclass banach \ real_normed_vector, complete_space +class banach = real_normed_vector + complete_space theorem LIMSEQ_imp_Cauchy: assumes X: "X ----> a" shows "Cauchy X" diff -r 69780aef0531 -r af06b784814d src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Set.thy Wed Oct 21 14:08:04 2009 +0200 @@ -458,7 +458,7 @@ unfolding mem_def by (erule le_funE, erule le_boolE) -- {* Rule in Modus Ponens style. *} -lemma rev_subsetD [intro?]: "c \ A ==> A \ B ==> c \ B" +lemma rev_subsetD [noatp,intro?]: "c \ A ==> A \ B ==> c \ B" -- {* The same, with reversed premises for use with @{text erule} -- cf @{text rev_mp}. *} by (rule subsetD) @@ -467,13 +467,13 @@ \medskip Converts @{prop "A \ B"} to @{prop "x \ A ==> x \ B"}. *} -lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" +lemma subsetCE [noatp,elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" -- {* Classical elimination rule. *} unfolding mem_def by (blast dest: le_funE le_boolE) -lemma subset_eq: "A \ B = (\x\A. x \ B)" by blast +lemma subset_eq [noatp]: "A \ B = (\x\A. x \ B)" by blast -lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" +lemma contra_subsetD [noatp]: "A \ B ==> c \ B ==> c \ A" by blast lemma subset_refl [simp]: "A \ A" @@ -488,8 +488,11 @@ lemma set_mp: "A \ B ==> x:A ==> x:B" by (rule subsetD) +lemma eq_mem_trans: "a=b ==> b \ A ==> a \ A" + by simp + lemmas basic_trans_rules [trans] = - order_trans_rules set_rev_mp set_mp + order_trans_rules set_rev_mp set_mp eq_mem_trans subsubsection {* Equality *} diff -r 69780aef0531 -r af06b784814d src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/SetInterval.thy Wed Oct 21 14:08:04 2009 +0200 @@ -395,6 +395,11 @@ lemma atLeastAtMostSuc_conv: "m \ Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) +lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast -lemma UN_finite2_subset: - assumes sb: "!!n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" -proof (rule UN_finite_subset) - fix n - have "(\i\{0.. (\i\{0.. (\n::nat. \i\{0..n. B n)" by (simp add: UN_UN_finite_eq) - finally show "(\i\{0.. (\n. B n)" . -qed +lemma UN_finite2_subset: + "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)" + apply (rule UN_finite_subset) + apply (subst UN_UN_finite_eq [symmetric, of B]) + apply blast + done lemma UN_finite2_eq: - "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" - by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE) + "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" + apply (rule subset_antisym) + apply (rule UN_finite2_subset, blast) + apply (rule UN_finite2_subset [where k=k]) + apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) + done subsubsection {* Cardinality *} diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 14:08:04 2009 +0200 @@ -257,7 +257,7 @@ fun get_nonrec_types descr sorts = map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) => Library.foldl (fn (Ts', (_, cargs)) => - union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr)); + union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr)); (* get all recursive types in datatype description *) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 14:08:04 2009 +0200 @@ -348,7 +348,7 @@ | Add(lin1,lin2) => let val lis1 = resolve_proof vars lin1 val lis2 = resolve_proof vars lin2 - val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2)) + val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2)) in map (fn n => let val a = these (AList.lookup (op =) lis1 n) val b = these (AList.lookup (op =) lis2 n) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 14:08:04 2009 +0200 @@ -1047,16 +1047,16 @@ (if with_generator then (case select_mode_prem thy gen_modes' vs ps of SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps) | _ => let val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length)) in case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of + (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (union (op =) (vs, generator_vs)) ps + (union (op =) vs generator_vs) ps | NONE => let val _ = tracing ("ps:" ^ (commas (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps))) @@ -1065,7 +1065,7 @@ else NONE) | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps)) val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); val in_vs = terms_vs in_ts; @@ -1073,7 +1073,7 @@ in if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' then - case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of + case check_mode_prems [] (union (op =) param_vs in_vs) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 14:08:04 2009 +0200 @@ -308,7 +308,7 @@ | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) | _ => (acc, dacc) val (cs,ds) = h ([],[]) p - val l = Integer.lcms (union (op =) (cs, ds)) + val l = Integer.lcms (union (op =) cs ds) fun cv k ct = let val (tm as b$s$t) = term_of ct in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/TFL/post.ML Wed Oct 21 14:08:04 2009 +0200 @@ -28,7 +28,7 @@ *--------------------------------------------------------------------------*) fun termination_goals rules = map (Type.freeze o HOLogic.dest_Trueprop) - (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules); + (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules); (*--------------------------------------------------------------------------- * Three postprocessors are applied to the definition. It @@ -79,7 +79,7 @@ val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) - val cntxt = union (op aconv) (cntxtl, cntxtr) + val cntxt = union (op aconv) cntxtl cntxtr in R.GEN_ALL (R.DISCH_ALL diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 14:08:04 2009 +0200 @@ -531,7 +531,7 @@ then writeln (cat_lines ("Extractants =" :: map (Display.string_of_thm_global thy) extractants)) else () - val TCs = List.foldr (union (op aconv)) [] TCl + val TCs = List.foldr (uncurry (union (op aconv))) [] TCl val full_rqt = WFR::TCs val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} val R'abs = S.rand R' diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 14:08:04 2009 +0200 @@ -222,7 +222,7 @@ | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of NONE => NONE | SOME (x, _) => check_mode_prems - (case x of Prem (us, _, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal x) ps)); val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts)); val in_vs = terms_vs in_ts; @@ -230,7 +230,7 @@ in forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' andalso - (case check_mode_prems (union (op =) (arg_vs, in_vs)) ps of + (case check_mode_prems (union (op =) arg_vs in_vs) ps of NONE => false | SOME vs => subset (op =) (concl_vs, vs)) end; diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Wed Oct 21 14:08:04 2009 +0200 @@ -631,7 +631,7 @@ let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith in {axioms = (mth, Meson.make_meta_clause ith) :: axioms, - tfrees = union (op =) (tfree_lits, tfrees)} + tfrees = union (op =) tfree_lits tfrees} end; val lmap0 = List.foldl (add_thm true) {axioms = [], tfrees = init_tfrees ctxt} cls diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/prop_logic.ML Wed Oct 21 14:08:04 2009 +0200 @@ -111,8 +111,8 @@ | indices False = [] | indices (BoolVar i) = [i] | indices (Not fm) = indices fm - | indices (Or (fm1, fm2)) = union (op =) (indices fm1, indices fm2) - | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2); + | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) + | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); (* ------------------------------------------------------------------------- *) (* maxidx: computes the maximal variable index occuring in a formula of *) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/refute.ML Wed Oct 21 14:08:04 2009 +0200 @@ -1154,7 +1154,7 @@ val axioms = collect_axioms thy u (* Term.typ list *) val types = Library.foldl (fn (acc, t') => - union (op =) (acc, (ground_types thy t'))) ([], u :: axioms) + uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms) val _ = tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ_global thy) types))) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Oct 21 14:08:04 2009 +0200 @@ -290,15 +290,6 @@ (* Retrieving and filtering lemmas *) (***************************************************************) -(*** white list and black list of lemmas ***) - -(*The rule subsetI is frequently omitted by the relevance filter.*) -val whitelist_fo = [subsetI]; -(* ext has been a 'helper clause', always given to the atps. - As such it was not passed to metis, but metis does not include ext (in contrast - to the other helper_clauses *) -val whitelist_ho = [ResHolClause.ext]; - (*** retrieve lemmas and filter them ***) (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) @@ -519,11 +510,8 @@ val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy isFO |> remove_unwanted_clauses - val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) - (* add whitelist *) - val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho)) in - white_cls @ axcls + relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) end; (* prepare for passing to writer, diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 14:08:04 2009 +0200 @@ -473,7 +473,7 @@ val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) (map Thm.term_of hyps) val fixed = OldTerm.term_frees (concl_of st) @ - List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) + List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps) in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Oct 21 14:08:04 2009 +0200 @@ -93,7 +93,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = List.foldl (union (op =)) [] xss; +fun union_all xss = List.foldl (uncurry (union (op =))) [] xss; (*Provide readable names for the more common symbolic functions*) val const_trans_table = @@ -263,7 +263,7 @@ | pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = List.foldl (union (op =)) [] (map sorts_on_typs Ts); +fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts); (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a @@ -373,7 +373,7 @@ val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) |> subtract (op =) classes |> subtract (op =) HOLogic.typeS val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses - in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end; + in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; fun make_arity_clauses_dfg dfg thy tycons classes = let val (classes', cpairs) = iter_type_class_pairs thy tycons classes diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 14:08:04 2009 +0200 @@ -155,7 +155,7 @@ | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q - in (CombApp(P',Q'), union (op =) (tsP, tsQ)) end + in (CombApp(P',Q'), union (op =) tsP tsQ) end | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t); fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) @@ -167,7 +167,7 @@ | literals_of_term1 dfg thy (lits,ts) P = let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) in - (Literal(pol,pred)::lits, union (op =) (ts, ts')) + (Literal(pol,pred)::lits, union (op =) ts ts') end; fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; @@ -476,7 +476,7 @@ val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) - val tfree_clss = map RC.tptp_tfree_clause (List.foldl (union (op =)) [] tfree_litss) + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) val _ = File.write_list file ( map (#1 o (clause2tptp params)) axclauses @ diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 14:08:04 2009 +0200 @@ -364,7 +364,7 @@ fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; fun replace_deps (old:int, new) (lno, t, deps) = - (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps)); + (lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps)); (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ only in type information.*) diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/sat_solver.ML Wed Oct 21 14:08:04 2009 +0200 @@ -472,7 +472,7 @@ | forced_vars (BoolVar i) = [i] | forced_vars (Not (BoolVar i)) = [~i] | forced_vars (Or (fm1, fm2)) = inter (op =) (forced_vars fm1, forced_vars fm2) - | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1, forced_vars fm2) + | forced_vars (And (fm1, fm2)) = union (op =) (forced_vars fm1) (forced_vars fm2) (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) (* precedence, and the next partial evaluation of the formula returns 'False'. *) | forced_vars _ = error "formula is not in negation normal form" diff -r 69780aef0531 -r af06b784814d src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/Tools/transfer.ML Wed Oct 21 14:08:04 2009 +0200 @@ -143,7 +143,7 @@ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2, hints = subtract (op = : string*string -> bool) hints0 - (union (op =) (hints1, hints2))} + (union (op =) hints1 hints2)} end; local @@ -151,7 +151,7 @@ in fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = - {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) (hints1, hints2)} + {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) hints1 hints2} end; fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) = diff -r 69780aef0531 -r af06b784814d src/HOL/ex/Codegenerator_Candidates.thy --- a/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 14:08:04 2009 +0200 @@ -26,7 +26,7 @@ "~~/src/HOL/ex/Records" begin -(*avoid popular infixes*) -code_reserved SML union inter upto +(*avoid popular infix*) +code_reserved SML upto end diff -r 69780aef0531 -r af06b784814d src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Wed Oct 21 14:08:04 2009 +0200 @@ -964,22 +964,22 @@ (if with_generator then (case select_mode_prem thy gen_modes' vs ps of SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps) | NONE => let val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length)) in case (find_first (fn generator_vs => is_some - (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of + (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) - (union (op =) (vs, generator_vs)) ps + (union (op =) vs generator_vs) ps | NONE => NONE end) else NONE) | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) - (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs) + (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs) (filter_out (equal p) ps)) val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts)); val in_vs = terms_vs in_ts; @@ -987,7 +987,7 @@ in if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso forall (is_eqT o fastype_of) in_ts' then - case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of + case check_mode_prems [] (union (op =) param_vs in_vs) ps of NONE => NONE | SOME (acc_ps, vs) => if with_generator then diff -r 69780aef0531 -r af06b784814d src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 14:08:04 2009 +0200 @@ -385,7 +385,7 @@ let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in if not (null eqs) then let val c = - fold (fn Lineq(_,_,l,_) => fn cs => union (op =) (l, cs)) eqs [] + fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |> filter (fn i => i <> 0) |> sort (int_ord o pairself abs) |> hd @@ -429,9 +429,8 @@ val warning_count = Unsynchronized.ref 0; val warning_count_max = 10; -val union_term = curry (union Pattern.aeconv); -val union_bterm = curry (union - (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'))); +val union_term = union Pattern.aeconv; +val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')); fun add_atoms (lhs, _, _, rhs, _, _) = union_term (map fst lhs) o union_term (map fst rhs); diff -r 69780aef0531 -r af06b784814d src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Wed Oct 21 14:08:04 2009 +0200 @@ -289,7 +289,7 @@ val _ = message "Collecting constraints..."; val (t, prf, cs, env, _) = make_constraints_cprf thy (Envir.empty (maxidx_proof cprf ~1)) cprf'; - val cs' = map (fn p => (true, p, union (op =) + val cs' = map (fn p => (true, p, uncurry (union (op =)) (pairself (map (fst o dest_Var) o OldTerm.term_vars) p))) (map (pairself (Envir.norm_term env)) ((t, prop')::cs)); val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); diff -r 69780aef0531 -r af06b784814d src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Oct 21 14:08:04 2009 +0200 @@ -101,7 +101,7 @@ val tos = connected_with chains' [lhs] [lhs]; in (copy_lookahead tos [], - union (op =) (if member (op =) lambdas lhs then tos else [], lambdas)) + union (op =) (if member (op =) lambdas lhs then tos else []) lambdas) end; (*test if new production can produce lambda @@ -109,7 +109,7 @@ val (new_lambda, lambdas') = if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id | (Terminal _) => false) rhs then - (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs])) + (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs])) else (false, lambdas'); @@ -125,7 +125,7 @@ (*get all known starting tokens for a nonterminal*) fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); - val token_union = union matching_tokens; + val token_union = uncurry (union matching_tokens); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = @@ -155,7 +155,7 @@ val added_tks' = token_union (new_tks, added_tks); - val nt_dependencies' = union (op =) (nts, nt_dependencies); + val nt_dependencies' = union (op =) nts nt_dependencies; (*associate production with new starting tokens*) fun copy ([]: token option list) nt_prods = nt_prods @@ -413,7 +413,7 @@ fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); val nt_prods = - Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @ + Library.foldl (uncurry (union (op =))) ([], map snd (snd (Array.sub (prods, tag)))) @ map prod_of_chain ((these o AList.lookup (op =) chains) tag); in map (pretty_prod name) nt_prods end; @@ -562,8 +562,8 @@ fun process_nt ~1 result = result | process_nt nt result = let - val nt_prods = Library.foldl (union op =) - ([], map snd (snd (Array.sub (prods2, nt)))); + val nt_prods = Library.foldl (uncurry (union (op =))) + ([], map snd (snd (Array.sub (prods2, nt)))); val lhs_tag = convert_tag nt; (*convert tags in rhs*) diff -r 69780aef0531 -r af06b784814d src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Wed Oct 21 14:08:04 2009 +0200 @@ -352,7 +352,7 @@ in SynExt { xprods = xprods, - consts = union (op =) (consts, mfix_consts), + consts = union (op =) consts mfix_consts, prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules' @ parse_rules, diff -r 69780aef0531 -r af06b784814d src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/codegen.ML Wed Oct 21 14:08:04 2009 +0200 @@ -599,8 +599,8 @@ else Pretty.block (separate (Pretty.brk 1) (p :: ps)); fun new_names t xs = Name.variant_list - (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t), - OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs); + (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t)) + (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs); fun new_name t x = hd (new_names t [x]); diff -r 69780aef0531 -r af06b784814d src/Pure/library.ML --- a/src/Pure/library.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/library.ML Wed Oct 21 14:08:04 2009 +0200 @@ -157,12 +157,12 @@ val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list + val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val mem: ''a * ''a list -> bool val mem_int: int * int list -> bool val mem_string: string * string list -> bool - val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool @@ -782,6 +782,7 @@ fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; fun update eq x xs = cons x (remove eq x xs); +fun union eq = fold (insert eq); fun subtract eq = fold (remove eq); fun merge eq (xs, ys) = @@ -796,11 +797,6 @@ fun (x: int) mem_int xs = member (op =) xs x; fun (x: string) mem_string xs = member (op =) xs x; -(*union of sets represented as lists: no repetitions*) -fun union eq (xs, []) = xs - | union eq ([], ys) = ys - | union eq (x :: xs, ys) = union eq (xs, insert eq x ys); - (*intersection*) fun inter eq ([], ys) = [] | inter eq (x::xs, ys) = diff -r 69780aef0531 -r af06b784814d src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Pure/proofterm.ML Wed Oct 21 14:08:04 2009 +0200 @@ -900,7 +900,7 @@ fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then - union (op =) (vs, map_filter (fn Var (ixn, T) => + union (op =) vs (map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; @@ -918,7 +918,7 @@ | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); -fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q) +fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); @@ -936,9 +936,9 @@ end; fun needed_vars prop = - union (op =) (Library.foldl (union (op =)) - ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))), - prop_vars prop); + union (op =) (Library.foldl (uncurry (union (op =))) + ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) + (prop_vars prop); fun gen_axm_proof c name prop = let @@ -975,7 +975,7 @@ let val p as (_, is', ch', prf') = shrink ls lev prf2; val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 - in (union (op =) (is, is'), ch orelse ch', ts', + in (union (op =) is is', ch orelse ch', ts', if ch orelse ch' then prf'' %% prf' else prf) end | shrink' ls lev ts prfs (prf as prf1 % t) = @@ -1004,15 +1004,15 @@ val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => insert (op =) ixn (case AList.lookup (op =) insts ixn of - SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns' - | _ => union (op =) (ixns, ixns'))) + SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' + | _ => union (op =) ixns ixns')) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); val insts' = map (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) | (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = - union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs) + union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) | needed (Var (ixn, _)) (_::_) _ = [ixn] | needed _ _ _ = []; in shrink end; diff -r 69780aef0531 -r af06b784814d src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 12:19:46 2009 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 14:08:04 2009 +0200 @@ -139,13 +139,11 @@ val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds); val (conds_tyvs,cond_vs) = Library.foldl (fn ((tyvs, vs), t) => - (union (op =) - (OldTerm.term_tvars t, tyvs), - union (op =) - (map Term.dest_Var (OldTerm.term_vars t), vs))) + (union (op =) (OldTerm.term_tvars t) tyvs, + union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs)) (([],[]), rule_conds); val termvars = map Term.dest_Var (OldTerm.term_vars tgt); - val vars_to_fix = union (op =) (termvars, cond_vs); + val vars_to_fix = union (op =) termvars cond_vs; val (renamings, names2) = List.foldr (fn (((n,i),ty), (vs, names')) => let val n' = Name.variant names' n in