# HG changeset patch # User wenzelm # Date 1723568004 -7200 # Node ID 39cd50407f79bed069647140ccdb148b8b353b2b # Parent f6c6d0988fba224a5a700980602371d8b974c002 tuned: prefer canonical argument order; diff -r f6c6d0988fba -r 39cd50407f79 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Tue Aug 13 18:31:40 2024 +0200 +++ b/src/FOL/FOL.thy Tue Aug 13 18:53:24 2024 +0200 @@ -346,7 +346,8 @@ val IFOL_ss = put_simpset FOL_basic_ss \<^context> addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all} - addsimprocs [\<^simproc>\defined_All\, \<^simproc>\defined_Ex\] + |> Simplifier.add_proc \<^simproc>\defined_All\ + |> Simplifier.add_proc \<^simproc>\defined_Ex\ |> Simplifier.add_cong @{thm imp_cong} |> simpset_of; diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/HOL.thy Tue Aug 13 18:53:24 2024 +0200 @@ -1567,11 +1567,12 @@ | _ => NONE)\ declaration \ - K (Induct.map_simpset (fn ss => ss - addsimprocs [\<^simproc>\swap_induct_false\, \<^simproc>\induct_equal_conj_curry\] - |> Simplifier.set_mksimps (fn ctxt => - Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> - map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) + K (Induct.map_simpset + (Simplifier.add_proc \<^simproc>\swap_induct_false\ #> + Simplifier.add_proc \<^simproc>\induct_equal_conj_curry\ #> + Simplifier.set_mksimps (fn ctxt => + Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> + map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) \ text \Pre-simplification of induction and cases rules\ @@ -1942,7 +1943,7 @@ \<^Const_>\HOL.eq T\ => if is_Type T then SOME @{thm eq_equal} else NONE | _ => NONE)\ -setup \Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\equal\])\ +setup \Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\equal\)\ subsubsection \Generic code generator foundation\ diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Product_Type.thy Tue Aug 13 18:53:24 2024 +0200 @@ -492,7 +492,7 @@ simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] - addsimprocs [\<^simproc>\unit_eq\]); + |> Simplifier.add_proc \<^simproc>\unit_eq\); in fun split_all_tac ctxt = SUBGOAL (fn (t, i) => if exists_paired_all t then safe_full_simp_tac (put_simpset ss ctxt) i else no_tac); @@ -1313,7 +1313,7 @@ simproc_setup passive set_comprehension ("Collect P") = \K Set_Comprehension_Pointfree.code_proc\ -setup \Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\set_comprehension\])\ +setup \Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\set_comprehension\)\ subsection \Lemmas about disjointness\ diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Aug 13 18:53:24 2024 +0200 @@ -30,7 +30,7 @@ fun special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps = ALLGOALS (CONVERSION Thm.eta_long_conversion) THEN HEADGOAL (simp_tac (ss_only @{thms pred_fun_True_id} ctxt - addsimprocs [\<^simproc>\NO_MATCH\])) THEN + |> Simplifier.add_proc \<^simproc>\NO_MATCH\)) THEN unfold_thms_tac ctxt (nested_simps @ map (unfold_thms ctxt @{thms id_def}) (fp_nesting_map_ident0s @ fp_nesting_map_comps @ fp_nesting_pred_maps)) THEN diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Aug 13 18:53:24 2024 +0200 @@ -541,7 +541,8 @@ fun nnf_ss simp_options = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps (nnf_extra_simps simp_options) - addsimprocs [\<^simproc>\defined_All\, \<^simproc>\defined_Ex\, \<^simproc>\neq\, \<^simproc>\let_simp\]) + |> fold Simplifier.add_proc + [\<^simproc>\defined_All\, \<^simproc>\defined_Ex\, \<^simproc>\neq\, \<^simproc>\let_simp\]) val presimplified_consts = [\<^const_name>\simp_implies\, \<^const_name>\False\, \<^const_name>\True\, diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Aug 13 18:53:24 2024 +0200 @@ -833,7 +833,8 @@ div_0 mod_0 div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1 ac_simps} - addsimprocs [\<^simproc>\cancel_div_mod_nat\, \<^simproc>\cancel_div_mod_int\]) + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_nat\ + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_int\) val splits_ss = simpset_of (put_simpset comp_ss \<^context> addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 13 18:53:24 2024 +0200 @@ -149,9 +149,9 @@ fun regularize_tac ctxt = let val simpset = - mk_minimal_simpset ctxt - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [regularize_simproc] + (mk_minimal_simpset ctxt + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + |> Simplifier.add_proc regularize_simproc) addSolver equiv_solver addSolver quotient_solver val eq_eqvs = eq_imp_rel_get ctxt in diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/SMT/lethe_replay_methods.ML --- a/src/HOL/Tools/SMT/lethe_replay_methods.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML Tue Aug 13 18:53:24 2024 +0200 @@ -1018,7 +1018,8 @@ Method.insert_tac ctxt prems THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt) addsimps @{thms HOL.simp_thms HOL.all_simps} - addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}]) + |> Simplifier.add_proc @{simproc HOL.defined_All} + |> Simplifier.add_proc @{simproc HOL.defined_Ex}) THEN' TRY' (Blast.blast_tac ctxt) THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [])) diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/SMT/smt_replay.ML --- a/src/HOL/Tools/SMT/smt_replay.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/SMT/smt_replay.ML Tue Aug 13 18:53:24 2024 +0200 @@ -154,7 +154,7 @@ simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} - addsimprocs [\<^simproc>\numeral_divmod\, fast_int_arith_simproc, + |> fold Simplifier.add_proc [\<^simproc>\numeral_divmod\, fast_int_arith_simproc, antisym_le_simproc, antisym_less_simproc]) structure Simpset = Generic_Data @@ -166,8 +166,7 @@ in fun add_simproc simproc context = - Simpset.map (simpset_map (Context.proof_of context) - (fn ctxt => ctxt addsimprocs [simproc])) context + Simpset.map (simpset_map (Context.proof_of context) (Simplifier.add_proc simproc)) context fun make_simpset ctxt rules = simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules) diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/SMT/smt_replay_arith.ML --- a/src/HOL/Tools/SMT/smt_replay_arith.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_arith.ML Tue Aug 13 18:53:24 2024 +0200 @@ -84,7 +84,8 @@ |> put_simpset HOL_basic_ss |> (fn ctxt => ctxt addsimps thms addsimps arith_thms - addsimprocs [@{simproc int_div_cancel_numeral_factors}, @{simproc int_combine_numerals}, + |> fold Simplifier.add_proc + [@{simproc int_div_cancel_numeral_factors}, @{simproc int_combine_numerals}, @{simproc divide_cancel_numeral_factor}, @{simproc intle_cancel_numerals}, @{simproc field_combine_numerals}, @{simproc intless_cancel_numerals}]) |> asm_full_simplify diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/groebner.ML Tue Aug 13 18:53:24 2024 +0200 @@ -789,7 +789,7 @@ val poly_eq_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms} - addsimprocs [poly_eq_simproc]) + |> Simplifier.add_proc poly_eq_simproc) local fun is_defined v t = diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/inductive.ML Tue Aug 13 18:53:24 2024 +0200 @@ -876,8 +876,9 @@ funpow n (fn thm => thm RS @{thm meta_fun_cong}) thm RS @{thm Pure.symmetric}) ns rec_preds_defs; val simps = simp_thms3 @ pred_defs_sym; - val simprocs = [Simplifier.the_simproc ctxt "HOL.defined_All"]; - val simplify = asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt addsimprocs simprocs); + val simproc = Simplifier.the_simproc ctxt "HOL.defined_All"; + val simplify = + asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt |> Simplifier.add_proc simproc); val coind = (mono RS (fp_def RS @{thm def_coinduct})) |> infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt R)] |> simplify; @@ -898,7 +899,8 @@ reorder_bound_goals; val coinduction = Goal.prove_sorry ctxt [] prems concl (fn {context = ctxt, prems = CIH} => HEADGOAL (full_simp_tac - (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt addsimprocs simprocs) THEN' + (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt + |> Simplifier.add_proc simproc) THEN' resolve_tac ctxt [coind]) THEN ALLGOALS (REPEAT_ALL_NEW (REPEAT_DETERM o resolve_tac ctxt [allI, impI, conjI] THEN' REPEAT_DETERM o eresolve_tac ctxt [exE, conjE] THEN' diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/inductive_set.ML Tue Aug 13 18:53:24 2024 +0200 @@ -242,7 +242,7 @@ in Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv} - addsimprocs [\<^simproc>\Collect_mem\]) thm'' + |> Simplifier.add_proc \<^simproc>\Collect_mem\) thm'' |> zero_var_indexes |> eta_contract_thm ctxt (equal p) end; @@ -349,9 +349,10 @@ in thm |> Thm.instantiate (TVars.empty, Vars.make insts) |> - Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs - [to_pred_simproc - (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |> + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_proc + (to_pred_simproc + (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps))) |> eta_contract_thm ctxt (is_pred pred_arities) |> Rule_Cases.save thm end; @@ -387,8 +388,10 @@ in thm |> Thm.instantiate (TVars.empty, Vars.make insts) |> - Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps - addsimprocs [strong_ind_simproc pred_arities, \<^simproc>\Collect_mem\]) |> + Simplifier.full_simplify + (put_simpset HOL_basic_ss ctxt addsimps to_set_simps + |> Simplifier.add_proc (strong_ind_simproc pred_arities) + |> Simplifier.add_proc \<^simproc>\Collect_mem\) |> Rule_Cases.save thm end; diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/int_arith.ML Tue Aug 13 18:53:24 2024 +0200 @@ -57,7 +57,8 @@ @{thms of_int_add of_int_mult of_int_diff of_int_minus of_int_less_iff of_int_le_iff of_int_eq_iff} - |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc]) + |> Simplifier.add_proc zero_to_of_int_zero_simproc + |> Simplifier.add_proc one_to_of_int_one_simproc |> simpset_of; val zero_one_idom_simproc = diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Tue Aug 13 18:53:24 2024 +0200 @@ -719,8 +719,8 @@ inverse_divide divide_inverse_commute [symmetric] simp_thms} - addsimprocs field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] + |> fold Simplifier.add_proc field_cancel_numeral_factors + |> fold Simplifier.add_proc [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] |> Simplifier.add_cong @{thm if_weak_cong}) in diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Aug 13 18:31:40 2024 +0200 +++ b/src/HOL/Tools/record.ML Tue Aug 13 18:53:24 2024 +0200 @@ -1384,7 +1384,8 @@ SOME (Goal.prove_sorry_global thy [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset (get_simpset thy) ctxt' - addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) + addsimps @{thms simp_thms} + |> Simplifier.add_proc (split_simproc (K ~1))) 1)) end handle TERM _ => NONE) | _ => NONE) end; @@ -1466,7 +1467,7 @@ | is_all _ = 0; in if has_rec goal then - full_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs [split_simproc is_all]) i + full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_proc (split_simproc is_all)) i else no_tac end);