# HG changeset patch # User wenzelm # Date 1754595603 -7200 # Node ID 73af47bc277c4c780384c0bfb8dce446cde268c7 # Parent 55a71dd13ca0f0fef4a38321d539338627ff772d avoid legacy operations; diff -r 55a71dd13ca0 -r 73af47bc277c src/CCL/CCL.thy --- a/src/CCL/CCL.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/CCL/CCL.thy Thu Aug 07 21:40:03 2025 +0200 @@ -207,7 +207,7 @@ CHANGED (REPEAT (assume_tac ctxt i ORELSE resolve_tac ctxt @{thms iffI allI conjI} i ORELSE eresolve_tac ctxt inj_lemmas i ORELSE - asm_simp_tac (ctxt addsimps rews) i)) + asm_simp_tac (ctxt |> Simplifier.add_simps rews) i)) end; \ @@ -279,7 +279,7 @@ Goal.prove_global thy [] [] (Syntax.read_prop ctxt s) (fn _ => rewrite_goals_tac ctxt defs THEN - simp_tac (ctxt addsimps (rls @ inj_rls)) 1) + simp_tac (ctxt |> Simplifier.add_simps (rls @ inj_rls)) 1) in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end fun mkall_dstnct_thms ctxt defs i_rls xss = maps (mk_dstnct_thms ctxt defs i_rls) xss diff -r 55a71dd13ca0 -r 73af47bc277c src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/FOL/FOL.thy Thu Aug 07 21:40:03 2025 +0200 @@ -345,7 +345,7 @@ (*intuitionistic simprules only*) val IFOL_ss = put_simpset FOL_basic_ss \<^context> - addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all} + |> Simplifier.add_simps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all} |> Simplifier.add_proc \<^simproc>\defined_All\ |> Simplifier.add_proc \<^simproc>\defined_Ex\ |> Simplifier.add_cong @{thm imp_cong} @@ -354,7 +354,7 @@ (*classical simprules too*) val FOL_ss = put_simpset IFOL_ss \<^context> - addsimps @{thms cla_simps cla_ex_simps cla_all_simps} + |> Simplifier.add_simps @{thms cla_simps cla_ex_simps cla_all_simps} |> simpset_of; \ diff -r 55a71dd13ca0 -r 73af47bc277c src/FOL/ex/Miniscope.thy --- a/src/FOL/ex/Miniscope.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/FOL/ex/Miniscope.thy Thu Aug 07 21:40:03 2025 +0200 @@ -68,7 +68,7 @@ lemmas mini_simps = demorgans nnf_simps ex_simps all_simps ML \ -val mini_ss = simpset_of (\<^context> addsimps @{thms mini_simps}); +val mini_ss = simpset_of (\<^context> |> Simplifier.add_simps @{thms mini_simps}); fun mini_tac ctxt = resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); \ diff -r 55a71dd13ca0 -r 73af47bc277c src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/FOL/simpdata.ML Thu Aug 07 21:40:03 2025 +0200 @@ -133,7 +133,7 @@ |> simpset_of; fun unfold_tac ctxt ths = - ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths)); + ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) |> Simplifier.add_simps ths)); (*** integration of simplifier with classical reasoner ***) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Thu Aug 07 21:40:03 2025 +0200 @@ -48,7 +48,9 @@ | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops; in asm_full_simp_tac - (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_term_ord (Term_Ord.term_lpo ord)) + (put_simpset HOL_ss ctxt + |> Simplifier.add_simps simps + |> Simplifier.set_term_ord (Term_Ord.term_lpo ord)) end; fun algebra_tac ctxt = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Aug 07 21:40:03 2025 +0200 @@ -765,22 +765,23 @@ let val ss1 = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm sum.distrib} RS sym, - @{thm sum_subtractf} RS sym, @{thm sum_distrib_left}, - @{thm sum_distrib_right}, @{thm sum_negf} RS sym]) + |> Simplifier.add_simps [@{thm sum.distrib} RS sym, + @{thm sum_subtractf} RS sym, @{thm sum_distrib_left}, + @{thm sum_distrib_right}, @{thm sum_negf} RS sym]) val ss2 = - simpset_of (\<^context> addsimps - [@{thm plus_vec_def}, @{thm times_vec_def}, - @{thm minus_vec_def}, @{thm uminus_vec_def}, - @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, - @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}]) + simpset_of (\<^context> + |> Simplifier.add_simps + [@{thm plus_vec_def}, @{thm times_vec_def}, + @{thm minus_vec_def}, @{thm uminus_vec_def}, + @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, + @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}]) fun vector_arith_tac ctxt ths = simp_tac (put_simpset ss1 ctxt) THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i ORELSE resolve_tac ctxt @{thms sum.neutral} i - ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) + ORELSE simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm vec_eq_iff}) i) (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) - THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths) + THEN' asm_full_simp_tac (put_simpset ss2 ctxt |> Simplifier.add_simps ths) in Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths)) end diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Analysis/ex/Approximations.thy --- a/src/HOL/Analysis/ex/Approximations.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Analysis/ex/Approximations.thy Thu Aug 07 21:40:03 2025 +0200 @@ -472,7 +472,7 @@ ML \ fun machin_term_conv ctxt ct = let - val ctxt' = ctxt addsimps @{thms arctan_double' arctan_add_small} + val ctxt' = ctxt |> Simplifier.add_simps @{thms arctan_double' arctan_add_small} in case Thm.term_of ct of Const (\<^const_name>\MACHIN_TAG\, _) $ _ $ @@ -494,7 +494,7 @@ Local_Defs.unfold_tac ctxt @{thms tag_machin[THEN eq_reflection] numeral_horner_MACHIN_TAG[THEN eq_reflection]} THEN REPEAT (CHANGED (HEADGOAL (CONVERSION conv)))) - THEN' Simplifier.simp_tac (ctxt addsimps @{thms arctan_add_small arctan_diff_small}) + THEN' Simplifier.simp_tac (ctxt |> Simplifier.add_simps @{thms arctan_add_small arctan_diff_small}) end \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Analysis/metric_arith.ML Thu Aug 07 21:40:03 2025 +0200 @@ -44,7 +44,7 @@ fun prenex_tac ctxt = let val prenex_simps = Proof_Context.get_thms ctxt @{named_theorems metric_prenex} - val prenex_ctxt = put_simpset HOL_basic_ss ctxt addsimps prenex_simps + val prenex_ctxt = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps prenex_simps in simp_tac prenex_ctxt THEN' K (trace_tac ctxt "Prenex form") @@ -53,25 +53,25 @@ fun nnf_tac ctxt = let val nnf_simps = Proof_Context.get_thms ctxt @{named_theorems metric_nnf} - val nnf_ctxt = put_simpset HOL_basic_ss ctxt addsimps nnf_simps + val nnf_ctxt = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps nnf_simps in simp_tac nnf_ctxt THEN' K (trace_tac ctxt "NNF form") end fun unfold_tac ctxt = - asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( - Proof_Context.get_thms ctxt @{named_theorems metric_unfold})) + asm_full_simp_tac (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps (Proof_Context.get_thms ctxt @{named_theorems metric_unfold})) fun pre_arith_tac ctxt = - simp_tac (put_simpset HOL_basic_ss ctxt addsimps ( - Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN' + simp_tac (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps (Proof_Context.get_thms ctxt @{named_theorems metric_pre_arith})) THEN' K (trace_tac ctxt "Prepared for decision procedure") fun dist_refl_sym_tac ctxt = let val refl_sym_simps = @{thms dist_self dist_commute add_0_right add_0_left simp_thms} - val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt addsimps refl_sym_simps + val refl_sym_ctxt = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps refl_sym_simps in simp_tac refl_sym_ctxt THEN' K (trace_tac ctxt ("Simplified using " ^ @{make_string} refl_sym_simps)) @@ -143,20 +143,25 @@ val (x, y) = Thm.dest_binop ct val solve_prems = rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt - addsimps @{thms finite.emptyI finite_insert empty_iff insert_iff}))) + |> Simplifier.add_simps @{thms finite.emptyI finite_insert empty_iff insert_iff}))) val image_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms image_empty image_insert}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms image_empty image_insert}) val dist_refl_sym_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms dist_commute dist_self}) val algebra_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps + Simplifier.rewrite (put_simpset HOL_ss ctxt |> Simplifier.add_simps @{thms diff_self diff_0_right diff_0 abs_zero abs_minus_cancel abs_minus_commute}) val insert_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms insert_absorb2 insert_commute}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms insert_absorb2 insert_commute}) val sup_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms cSup_singleton Sup_insert_insert}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms cSup_singleton Sup_insert_insert}) val real_abs_dist_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms real_abs_dist}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms real_abs_dist}) val maxdist_thm = \<^instantiate>\'a = \Thm.ctyp_of_cterm x\ and x and y and s = fset_ct in lemma \finite s \ x \ s \ y \ s \ dist x y \ SUP a\s. \dist x a - dist a y\\ @@ -182,12 +187,13 @@ val (x, y) = Thm.dest_binop ct val solve_prems = rule_by_tactic ctxt (ALLGOALS (simp_tac (put_simpset HOL_ss ctxt - addsimps @{thms empty_iff insert_iff}))) + |> Simplifier.add_simps @{thms empty_iff insert_iff}))) val ball_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps - @{thms Set.ball_empty ball_insert}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms Set.ball_empty ball_insert}) val dist_refl_sym_simp = - Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self}) + Simplifier.rewrite (put_simpset HOL_ss ctxt + |> Simplifier.add_simps @{thms dist_commute dist_self}) val metric_eq_thm = \<^instantiate>\'a = \Thm.ctyp_of_cterm x\ and x and y and s = fset_ct in lemma \x \ s \ y \ s \ x = y \ \a\s. dist x a = dist y a\ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Analysis/normarith.ML --- a/src/HOL/Analysis/normarith.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Analysis/normarith.ML Thu Aug 07 21:40:03 2025 +0200 @@ -386,7 +386,7 @@ fun init_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt - addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus}, + |> Simplifier.add_simps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})) then_conv Numeral_Simprocs.field_comp_conv ctxt then_conv nnf_conv ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/OtwayReesBella.thy --- a/src/HOL/Auth/OtwayReesBella.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/OtwayReesBella.thy Thu Aug 07 21:40:03 2025 +0200 @@ -239,9 +239,9 @@ val analz_image_freshK_ss = simpset_of - (\<^context> delsimps @{thms image_insert image_Un} - delsimps @{thms imp_disjL} (*reduces blow-up*) - addsimps @{thms analz_image_freshK_simps}) + (\<^context> |> Simplifier.del_simps @{thms image_insert image_Un} + |> Simplifier.del_simps @{thms imp_disjL} (*reduces blow-up*) + |> Simplifier.add_simps @{thms analz_image_freshK_simps}) end \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/Public.thy Thu Aug 07 21:40:03 2025 +0200 @@ -407,9 +407,9 @@ val analz_image_freshK_ss = simpset_of - (\<^context> delsimps @{thms image_insert image_Un} - delsimps @{thms imp_disjL} (*reduces blow-up*) - addsimps @{thms analz_image_freshK_simps}) + (\<^context> |> Simplifier.del_simps @{thms image_insert image_Un} + |> Simplifier.del_simps @{thms imp_disjL} (*reduces blow-up*) + |> Simplifier.add_simps @{thms analz_image_freshK_simps}) (*Tactic for possibility theorems*) fun possibility_tac ctxt = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/Shared.thy Thu Aug 07 21:40:03 2025 +0200 @@ -218,9 +218,9 @@ val analz_image_freshK_ss = simpset_of - (\<^context> delsimps @{thms image_insert image_Un} - delsimps @{thms imp_disjL} (*reduces blow-up*) - addsimps @{thms analz_image_freshK_simps}) + (\<^context> |> Simplifier.del_simps @{thms image_insert image_Un} + |> Simplifier.del_simps @{thms imp_disjL} (*reduces blow-up*) + |> Simplifier.add_simps @{thms analz_image_freshK_simps}) end \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Aug 07 21:40:03 2025 +0200 @@ -820,7 +820,7 @@ (resolve_tac ctxt @{thms allI ballI impI}), REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt - addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy}, + |> Simplifier.add_simps [@{thm knows_Spy_Inputs_secureM_sr_Spy}, @{thm knows_Spy_Outpts_secureM_sr_Spy}, @{thm shouprubin_assumes_securemeans}, @{thm analz_image_Key_Un_Nonce}]))])))\ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Aug 07 21:40:03 2025 +0200 @@ -829,7 +829,7 @@ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}), REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt - addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy}, + |> Simplifier.add_simps [@{thm knows_Spy_Inputs_secureM_srb_Spy}, @{thm knows_Spy_Outpts_secureM_srb_Spy}, @{thm shouprubin_assumes_securemeans}, @{thm analz_image_Key_Un_Nonce}]))])))\ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Aug 07 21:40:03 2025 +0200 @@ -383,9 +383,9 @@ val analz_image_freshK_ss = simpset_of - (\<^context> delsimps @{thms image_insert image_Un} - delsimps @{thms imp_disjL} (*reduces blow-up*) - addsimps @{thms analz_image_freshK_simps}) + (\<^context> |> Simplifier.del_simps @{thms image_insert image_Un} + |> Simplifier.del_simps @{thms imp_disjL} (*reduces blow-up*) + |> Simplifier.add_simps @{thms analz_image_freshK_simps}) end \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Bali/Basis.thy Thu Aug 07 21:40:03 2025 +0200 @@ -178,7 +178,7 @@ ML \ fun sum3_instantiate ctxt thm = map (fn s => - simplify (ctxt delsimps @{thms not_None_eq}) + simplify (ctxt |> Simplifier.del_simps @{thms not_None_eq}) (Rule_Insts.read_instantiate ctxt [((("t", 0), Position.none), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"] \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Bali/Example.thy Thu Aug 07 21:40:03 2025 +0200 @@ -1192,7 +1192,8 @@ Base_foo_defs [simp] ML \ML_Thms.bind_thms ("eval_intros", map - (simplify (\<^context> delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o + (simplify (\<^context> |> Simplifier.del_simps @{thms Skip_eq} + |> Simplifier.add_simps @{thms lvar_def}) o rewrite_rule \<^context> [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros})\ lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/HOL.thy Thu Aug 07 21:40:03 2025 +0200 @@ -2185,7 +2185,8 @@ local val nnf_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps}); + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps @{thms simp_thms nnf_simps}); in fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt); end diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Thu Aug 07 21:40:03 2025 +0200 @@ -115,10 +115,10 @@ (**Simp_tacs**) fun before_set2pred_simp_tac ctxt = - simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]); + simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm Collect_conj_eq} RS sym, @{thm Compl_Collect}]); fun split_simp_tac ctxt = - simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]); + simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm split_conv}]); (*****************************************************************************) (** set_to_pred_tac transforms sets inclusion into predicates implication, **) @@ -140,7 +140,7 @@ dresolve_tac ctxt @{thms CollectD} i, TRY (split_all_tac ctxt i) THEN_MAYBE (rename_tac var_names i THEN - full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]); + full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm split_conv}) i)]); (*******************************************************************************) (** basic_simp_tac is called to simplify all verification conditions. It does **) @@ -157,7 +157,7 @@ fun basic_simp_tac ctxt var_names tac = simp_tac (put_simpset HOL_basic_ss ctxt - addsimps @{thms mem_Collect_eq split_conv} |> Simplifier.add_proc Record.simproc) + |> Simplifier.add_simps @{thms mem_Collect_eq split_conv} |> Simplifier.add_proc Record.simproc) THEN_MAYBE' max_simp_tac ctxt var_names tac; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/Cancellation/cancel.ML --- a/src/HOL/Library/Cancellation/cancel.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/Cancellation/cancel.ML Thu Aug 07 21:40:03 2025 +0200 @@ -50,7 +50,7 @@ val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt - addsimps Named_Theorems.get ctxt \<^named_theorems>\cancelation_simproc_pre\ + |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\cancelation_simproc_pre\) |> Simplifier.add_proc \<^simproc>\NO_MATCH\) (Thm.cterm_of ctxt t'); val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct) val export = singleton (Variable.export ctxt' ctxt) @@ -69,7 +69,7 @@ fun add_post_simplification thm = let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt - addsimps Named_Theorems.get ctxt \<^named_theorems>\cancelation_simproc_post\ + |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\cancelation_simproc_post\) |> Simplifier.add_proc \<^simproc>\NO_MATCH\) (Thm.rhs_of thm) in @{thm Pure.transitive} OF [thm, post_simplified_ct] end in diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/Cancellation/cancel_data.ML --- a/src/HOL/Library/Cancellation/cancel_data.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/Cancellation/cancel_data.ML Thu Aug 07 21:40:03 2025 +0200 @@ -42,7 +42,7 @@ map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0}; val numeral_sym_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps numeral_syms); + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps numeral_syms); fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const | mk_number n = HOLogic.mk_number HOLogic.natT n; @@ -145,20 +145,19 @@ val trans_tac = Numeral_Simprocs.trans_tac; val norm_ss1 = - simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> addsimps - numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps}); + simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> + |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps})); val norm_ss2 = - simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> addsimps - bin_simps @ - @{thms ac_simps}); + simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> + |> Simplifier.add_simps (bin_simps @ @{thms ac_simps})); fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)); val mset_simps_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps bin_simps); + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps bin_simps); fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt)); diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Thu Aug 07 21:40:03 2025 +0200 @@ -528,7 +528,7 @@ val trans_tac = Numeral_Simprocs.trans_tac val norm_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms ac_simps add_0_left add_0_right}) + |> Simplifier.add_simps @{thms ac_simps add_0_left add_0_right}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) fun simplify_meta_eq ctxt cancel_th th = Arith_Data.simplify_meta_eq [] ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Aug 07 21:40:03 2025 +0200 @@ -397,7 +397,7 @@ val trans_tac = Numeral_Simprocs.trans_tac val norm_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms ac_simps add_0_left add_0_right}) + |> Simplifier.add_simps @{thms ac_simps add_0_left add_0_right}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) fun simplify_meta_eq ctxt cancel_th th = Arith_Data.simplify_meta_eq [] ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Aug 07 21:40:03 2025 +0200 @@ -352,15 +352,16 @@ poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv, absconv1,absconv2,prover) = let - val pre_ss = put_simpset HOL_basic_ss ctxt addsimps - @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib - all_conj_distrib if_bool_eq_disj} - val prenex_ss = put_simpset HOL_basic_ss ctxt addsimps prenex_simps - val skolemize_ss = put_simpset HOL_basic_ss ctxt addsimps [choice_iff] + val pre_ss = put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps + @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib + all_conj_distrib if_bool_eq_disj} + val prenex_ss = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps prenex_simps + val skolemize_ss = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp choice_iff val presimp_conv = Simplifier.rewrite pre_ss val prenex_conv = Simplifier.rewrite prenex_ss val skolemize_conv = Simplifier.rewrite skolemize_ss - val weak_dnf_ss = put_simpset HOL_basic_ss ctxt addsimps weak_dnf_simps + val weak_dnf_ss = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps weak_dnf_simps val weak_dnf_conv = Simplifier.rewrite weak_dnf_ss fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI} fun oprconv cv ct = @@ -716,7 +717,7 @@ local val absmaxmin_elim_ss1 = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps real_abs_thms1) + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps real_abs_thms1) fun absmaxmin_elim_conv1 ctxt = Simplifier.rewrite (put_simpset absmaxmin_elim_ss1 ctxt) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/code_lazy.ML --- a/src/HOL/Library/code_lazy.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/code_lazy.ML Thu Aug 07 21:40:03 2025 +0200 @@ -350,7 +350,7 @@ let val binding = Binding.name name fun tac {context, ...} = Simplifier.simp_tac - (put_simpset HOL_basic_ss context addsimps thms) + (put_simpset HOL_basic_ss context |> Simplifier.add_simps thms) 1 val thm = Goal.prove lthy [] [] term tac val (_, lthy1) = lthy @@ -500,14 +500,10 @@ val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms val case_thm_abs = Drule.abs_def (case_lazy_thm RS @{thm eq_reflection}) - val add_simps = Code_Preproc.map_pre - (fn ctxt => ctxt addsimps (case_thm_abs :: ctr_thms_abs)) - val del_simps = Code_Preproc.map_pre - (fn ctxt => ctxt delsimps (case_thm_abs :: ctr_thms_abs)) - val add_post = Code_Preproc.map_post - (fn ctxt => ctxt addsimps ctr_post) - val del_post = Code_Preproc.map_post - (fn ctxt => ctxt delsimps ctr_post) + val add_simps = Code_Preproc.map_pre (Simplifier.add_simps (case_thm_abs :: ctr_thms_abs)) + val del_simps = Code_Preproc.map_pre (Simplifier.del_simps (case_thm_abs :: ctr_thms_abs)) + val add_post = Code_Preproc.map_post (Simplifier.add_simps ctr_post) + val del_post = Code_Preproc.map_post (Simplifier.del_simps ctr_post) in Local_Theory.exit_global lthy10 |> Laziness_Data.map (Symtab.update (type_name, diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/datatype_records.ML --- a/src/HOL/Library/datatype_records.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/datatype_records.ML Thu Aug 07 21:40:03 2025 +0200 @@ -70,7 +70,7 @@ fun simp_only_tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}) THEN' - asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp_thms) + asm_full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps simp_thms) fun prove ctxt defs ts n = let diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Library/old_recdef.ML Thu Aug 07 21:40:03 2025 +0200 @@ -1234,7 +1234,7 @@ (Variable.declare_term (Thm.term_of ctm) ctxt) ctm; fun simpl_conv ctxt thl ctm = - HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm); + HOLogic.mk_obj_eq (rew_conv (ctxt |> Simplifier.add_simps thl) ctm); fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc}; @@ -1582,7 +1582,7 @@ val names = Misc_Legacy.add_term_names (Thm.term_of ctm, []) val th1 = Simplifier.rewrite_cterm (false, true, false) - (prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm + (prover names) (ctxt0 |> Simplifier.add_simp cut_lemma' |> fold Simplifier.add_eqcong congs) ctm val th2 = Thm.equal_elim th1 th in (th2, filter_out restricted (!tc_list)) @@ -2061,7 +2061,7 @@ slow.*) val case_simpset = put_simpset HOL_basic_ss ctxt - addsimps case_rewrites + |> Simplifier.add_simps case_rewrites |> fold (Simplifier.add_cong o #case_cong_weak o snd) (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting])) val corollaries' = map (Simplifier.simplify case_simpset) corollaries @@ -2572,7 +2572,7 @@ val dummy = (Prim.trace_thms ctxt "solved =" solved; Prim.trace_thms ctxt "simplified' =" simplified') fun rewr th = - full_simplify (Variable.declare_thm th ctxt addsimps (solved @ simplified')) th; + full_simplify (Variable.declare_thm th ctxt |> Simplifier.add_simps (solved @ simplified')) th; val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction] val induction' = rewr induction val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules] @@ -2794,13 +2794,13 @@ NONE => ctxt | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt)); val {simps, congs, wfs} = get_hints ctxt'; - val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong}; + val ctxt'' = ctxt' |> Simplifier.add_simps simps |> Simplifier.del_cong @{thm imp_cong}; in ((rev (map snd congs), wfs), ctxt'') end; fun prepare_hints_i () ctxt = let val {simps, congs, wfs} = get_hints ctxt; - val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; + val ctxt' = ctxt |> Simplifier.add_simps simps |> Simplifier.del_cong @{thm imp_cong}; in ((rev (map snd congs), wfs), ctxt') end; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/List.thy --- a/src/HOL/List.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/List.thy Thu Aug 07 21:40:03 2025 +0200 @@ -1063,7 +1063,7 @@ val rearr_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); + |> Simplifier.add_simps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) = let diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Product_Type.thy Thu Aug 07 21:40:03 2025 +0200 @@ -500,7 +500,7 @@ val ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] + |> Simplifier.add_simps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] |> Simplifier.add_proc \<^simproc>\unit_eq\); in fun split_all_tac ctxt = SUBGOAL (fn (t, i) => @@ -538,7 +538,7 @@ ML \ local val cond_case_prod_eta_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms cond_case_prod_eta}); + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps @{thms cond_case_prod_eta}); fun Pair_pat k 0 (Bound m) = (m = k) | Pair_pat k i (Const (\<^const_name>\Pair\, _) $ Bound m $ t) = i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t @@ -647,7 +647,9 @@ in fun split_conv_tac ctxt = SUBGOAL (fn (t, i) => if exists_p_split t - then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i + then + safe_full_simp_tac + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms case_prod_conv}) i else no_tac); end; \ @@ -1367,7 +1369,7 @@ let val simp = full_simp_tac (put_simpset HOL_basic_ss ctxt - addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1 + |> Simplifier.add_simps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1 in SOME (Goal.prove ctxt [] [] \<^Const>\Pure.eq \<^Type>\set A\ for S S'\ (K (EVERY diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/SMT.thy --- a/src/HOL/SMT.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/SMT.thy Thu Aug 07 21:40:03 2025 +0200 @@ -21,7 +21,7 @@ REPEAT o EqSubst.eqsubst_tac ctxt [0] @{thms choice_iff[symmetric] bchoice_iff[symmetric]} THEN' TRY o Simplifier.asm_full_simp_tac - (clear_simpset ctxt addsimps @{thms all_simps ex_simps ex_iff_push}) THEN_ALL_NEW + (clear_simpset ctxt |> Simplifier.add_simps @{thms all_simps ex_simps ex_iff_push}) THEN_ALL_NEW Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] \ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Aug 07 21:40:03 2025 +0200 @@ -2219,7 +2219,7 @@ let val remove_domain_condition = full_simplify (put_simpset HOL_basic_ss lthy' - addsimps (@{thm True_implies_equals} :: termin_thms)); + |> Simplifier.add_simps (@{thm True_implies_equals} :: termin_thms)); in def_fun (@{apply 3} (map remove_domain_condition) inner_fp_triple) (const_transfers @ const_transfers') diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Thu Aug 07 21:40:03 2025 +0200 @@ -130,19 +130,19 @@ val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) distrib_consts; val case_sum_distribs = map (mk_case_sum_distrib_of ctxt) distrib_consts; - val simp_ctxt = (ctxt - |> Context_Position.set_visible false - |> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\Main\)) - |> Simplifier.add_cong @{thm if_cong}) - addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def :: + val simp_ctxt = ctxt + |> Context_Position.set_visible false + |> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\Main\)) + |> Simplifier.add_cong @{thm if_cong} + |> Simplifier.add_simps (pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def :: @{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @ fp_nesting_k_map_disc_sels' @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ case_sum_distribs @ - shared_simps; + shared_simps); fun mk_main_simp const_pointful_naturals_maybe_sym' = - simp_tac (simp_ctxt addsimps const_pointful_naturals_maybe_sym'); + simp_tac (simp_ctxt |> Simplifier.add_simps const_pointful_naturals_maybe_sym'); in unfold_thms_tac ctxt [eq_corecUU] THEN HEADGOAL (REPEAT_DETERM o rtac ctxt ext THEN' diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 07 21:40:03 2025 +0200 @@ -71,7 +71,8 @@ HEADGOAL Goal.conjunction_tac THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt - addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))))); + |> Simplifier.add_simps + (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))))); fun proves goals = goals |> Logic.mk_conjunction_balanced diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Aug 07 21:40:03 2025 +0200 @@ -242,7 +242,7 @@ val parse_binding_colon = Parse.binding --| \<^keyword>\:\; val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; -fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; +fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) |> Simplifier.add_simps thms; val eqTrueI = @{thm iffD2[OF eq_True]}; val eqFalseI = @{thm iffD2[OF eq_False]}; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/function.ML Thu Aug 07 21:40:03 2025 +0200 @@ -191,7 +191,7 @@ val totality = Thm.close_derivation \<^here> raw_totality val remove_domain_condition = full_simplify (put_simpset HOL_basic_ss lthy1 - addsimps [totality, @{thm True_implies_equals}]) + |> Simplifier.add_simps [totality, @{thm True_implies_equals}]) val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts val telims = map (map remove_domain_condition) pelims diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/function_context_tree.ML --- a/src/HOL/Tools/Function/function_context_tree.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/function_context_tree.ML Thu Aug 07 21:40:03 2025 +0200 @@ -266,7 +266,8 @@ |> map (fn u_eq => (u_eq RS sym) RS eq_reflection) |> filter_out Thm.is_reflexive - val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes + val assumes' = + map (simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps used)) assumes val (subeq, x') = rewrite_help (fix @ fixes) (h_as @ assumes') x st diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Thu Aug 07 21:40:03 2025 +0200 @@ -333,7 +333,8 @@ val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs - val ih_intro_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro + val ih_intro_case = + full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp case_hyp) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas @@ -370,7 +371,7 @@ [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness - |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) + |> simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp (case_hyp RS sym)) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs @@ -582,7 +583,7 @@ |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP valthm) |> Thm.implies_intr lhs_acc - |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) + |> asm_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp f_iff) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end @@ -735,7 +736,7 @@ val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, qglr=(oqs, _, _, _), ...} = clause - val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp + val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp case_hyp) ihyp fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = let @@ -837,7 +838,7 @@ |> Thm.forall_intr R' |> Thm.forall_elim inrel_R |> curry op RS wf_in_rel - |> full_simplify (put_simpset HOL_basic_ss ctxt' addsimps [in_rel_def]) + |> full_simplify (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simp in_rel_def) |> Thm.forall_intr_name ("R", Rrel) end diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Thu Aug 07 21:40:03 2025 +0200 @@ -253,7 +253,7 @@ val ags = map (Thm.assume o Thm.cterm_of ctxt) gs val replace_x_simpset = - put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps) + put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps (branch_hyp :: case_hyps) val sih = full_simplify replace_x_simpset aihyp fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Aug 07 21:40:03 2025 +0200 @@ -207,7 +207,7 @@ fun lexicographic_order_tac quiet ctxt = TRY (Function_Common.termination_rule_tac ctxt 1) THEN lex_order_tac quiet ctxt - (auto_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\termination_simp\))) + (auto_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\termination_simp\))) val _ = Theory.setup diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Thu Aug 07 21:40:03 2025 +0200 @@ -227,7 +227,7 @@ val induct_inst = Thm.forall_elim (Thm.cterm_of ctxt case_exp) induct |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) - |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) + |> full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps all_f_defs) fun project rule (MutualPart {cargTs, i, ...}) k = let @@ -285,7 +285,7 @@ fun mk_mpsimp fqgar sum_psimp = in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp - val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs + val rew_simpset = put_simpset HOL_basic_ss lthy |> Simplifier.add_simps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m val mcases = map (mutual_cases_rule lthy cases_rule n ST) parts diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Thu Aug 07 21:40:03 2025 +0200 @@ -151,15 +151,15 @@ val curry_uncurry_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}]) + |> Simplifier.add_simps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}]) val split_conv_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm Product_Type.split_conv}]); + |> Simplifier.add_simps [@{thm Product_Type.split_conv}]); val curry_K_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm Product_Type.curry_K}]); + |> Simplifier.add_simps [@{thm Product_Type.curry_K}]); (* instantiate generic fixpoint induction and eliminate the canonical assumptions; curry induction predicate *) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Aug 07 21:40:03 2025 +0200 @@ -59,7 +59,8 @@ val (_, subps) = strip_comb pat val eqs = map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) val c_eq_pat = - simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum + simplify (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps (map Thm.assume eqs)) c_assum in (subps @ pats, fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat)) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Aug 07 21:40:03 2025 +0200 @@ -322,7 +322,7 @@ fun decomp_scnp_tac orders ctxt = let val extra_simps = Named_Theorems.get ctxt \<^named_theorems>\termination_simp\ - val autom_tac = auto_tac (ctxt addsimps extra_simps) + val autom_tac = auto_tac (ctxt |> Simplifier.add_simps extra_simps) in gen_sizechange_tac orders autom_tac ctxt end diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Function/sum_tree.ML --- a/src/HOL/Tools/Function/sum_tree.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Function/sum_tree.ML Thu Aug 07 21:40:03 2025 +0200 @@ -22,7 +22,7 @@ (* Theory dependencies *) val sumcase_split_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps (@{thm Product_Type.split} :: @{thms sum.case})) + |> Simplifier.add_simps (@{thm Product_Type.split} :: @{thms sum.case})) (* top-down access in balanced tree *) fun access_top_down {left, right, init} len i = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Thu Aug 07 21:40:03 2025 +0200 @@ -543,7 +543,7 @@ "Let_def [abs_def]". *) fun nnf_ss simp_options = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps (nnf_extra_simps simp_options) + |> Simplifier.add_simps (nnf_extra_simps simp_options) |> fold Simplifier.add_proc [\<^simproc>\defined_All\, \<^simproc>\defined_Ex\, \<^simproc>\neq\, \<^simproc>\let_simp\]) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Aug 07 21:40:03 2025 +0200 @@ -295,7 +295,7 @@ else Conv.all_conv | _ => Conv.all_conv) -fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths +fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) |> Simplifier.add_simps ths val cheat_choice = \<^prop>\\x. \y. Q x y \ \f. \x. Q x (f x)\ diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Aug 07 21:40:03 2025 +0200 @@ -167,8 +167,8 @@ let val distinct_tac = if i < length newTs then - full_simp_tac (put_simpset HOL_ss ctxt addsimps (nth dist_rewrites i)) 1 - else full_simp_tac (put_simpset HOL_ss ctxt addsimps (flat other_dist_rewrites)) 1; + full_simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps (nth dist_rewrites i)) 1 + else full_simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps (flat other_dist_rewrites)) 1; val inject = map (fn r => r RS iffD1) @@ -392,7 +392,7 @@ val tac = EVERY [resolve_tac ctxt [exhaustion'] 1, ALLGOALS (asm_simp_tac - (put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))]; + (put_simpset HOL_ss ctxt |> Simplifier.add_simps (dist_rewrites' @ inject @ case_thms')))]; in (Goal.prove_sorry_global thy [] [] t1 (K tac), Goal.prove_sorry_global thy [] [] t2 (K tac)) @@ -465,10 +465,11 @@ let val nchotomy'' = infer_instantiate ctxt [(v, Thm.cterm_of ctxt Ma)] nchotomy'; - val simplify = asm_simp_tac (put_simpset HOL_ss ctxt addsimps (prems @ case_rewrites)) + val simplify = + asm_simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps (prems @ case_rewrites)) in EVERY [ - simp_tac (put_simpset HOL_ss ctxt addsimps [hd prems]) 1, + simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simp (hd prems)) 1, cut_tac nchotomy'' 1, REPEAT (eresolve_tac ctxt [disjE] 1 THEN REPEAT (eresolve_tac ctxt [exE] 1) THEN simplify 1), diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 07 21:40:03 2025 +0200 @@ -876,7 +876,7 @@ val intro'''' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt - addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]) + |> Simplifier.add_simps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}]) intro''' (* splitting conjunctions introduced by prod.inject*) val intro''''' = split_conjuncts_in_assms ctxt intro'''' diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 07 21:40:03 2025 +0200 @@ -1088,7 +1088,7 @@ [defthm, @{thm pred.sel}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}] val unfolddef_tac = - Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1 + Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps simprules) 1 val introthm = Goal.prove ctxt (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac) val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); @@ -1104,8 +1104,8 @@ (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit)) val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI) val tac = - Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps - (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1 + Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1 THEN resolve_tac ctxt @{thms Predicate.singleI} 1 in SOME (Goal.prove ctxt (argnames @ hoarg_names') [] neg_introtrm (fn _ => tac)) @@ -1346,8 +1346,10 @@ val eq_term = HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) val def = Core_Data.predfun_definition_of ctxt predname full_mode - val tac = fn _ => Simplifier.simp_tac - (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm pred.sel}]) 1 + val tac = fn _ => + Simplifier.simp_tac + (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps [def, @{thm holds_eq}, @{thm pred.sel}]) 1 val eq = Goal.prove ctxt arg_names [] eq_term tac in (pred, result_thms @ [eq]) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 07 21:40:03 2025 +0200 @@ -157,7 +157,9 @@ let val ctxt = Proof_Context.init_global thy val inline_defs = Named_Theorems.get ctxt \<^named_theorems>\code_pred_inline\ - val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th + val th' = + Simplifier.full_simplify + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps inline_defs) th (*val _ = print_step options ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th)) ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs)) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 07 21:40:03 2025 +0200 @@ -162,7 +162,8 @@ Logic.dest_implies o Thm.prop_of) @{thm exI} fun prove_introrule (index, (ps, introrule)) = let - val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 + val tac = + Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simp th) 1 THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1 THEN (EVERY (map (fn y => resolve_tac ctxt' @@ -178,16 +179,17 @@ in maps introrulify' ths' |> Variable.export ctxt' ctxt end fun rewrite ctxt = - Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm Ball_def}, @{thm Bex_def}]) - #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) + Simplifier.simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm Ball_def}, @{thm Bex_def}]) + #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm all_not_ex}) #> Conv.fconv_rule (nnf_conv ctxt) - #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}]) + #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm ex_disj_distrib}) fun rewrite_intros ctxt = - Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm all_not_ex}) #> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt - addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) + |> Simplifier.add_simps (tl @{thms bool_simps}) + |> Simplifier.add_simps @{thms nnf_simps}) #> split_conjuncts_in_assms ctxt fun print_specs options thy msg ths = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Aug 07 21:40:03 2025 +0200 @@ -35,7 +35,7 @@ val HOL_basic_ss' = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms prod.inject} + |> Simplifier.add_simps @{thms simp_thms prod.inject} |> Simplifier.set_unsafe_solver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) |> Simplifier.set_unsafe_solver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI}))) @@ -60,7 +60,7 @@ val ho_args = ho_args_of mode args val f_tac = (case f of - Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps + Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode, @{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1 @@ -140,7 +140,7 @@ (* replace TRY by determining if it necessary - are there equations when calling compile match? *) in (* make this simpset better! *) - asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 + asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt |> Simplifier.add_simps simprules) 1 THEN trace_tac ctxt options "after prove_match:" THEN (DETERM (TRY (resolve_tac ctxt [eval_if_P] 1 @@ -180,7 +180,7 @@ preds in simp_tac (put_simpset HOL_basic_ss ctxt - addsimps (@{thms HOL.simp_thms pred.sel} @ defs)) 1 + |> Simplifier.add_simps (@{thms HOL.simp_thms pred.sel} @ defs)) 1 (* need better control here! *) end @@ -233,7 +233,7 @@ val params = ho_args_of mode args in trace_tac ctxt options "before prove_neg_expr:" - THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps + THEN full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then @@ -249,9 +249,9 @@ (* test: *) THEN dresolve_tac ctxt @{thms sym} 1 THEN asm_full_simp_tac - (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1) + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm not_False_eq_True}) 1) THEN simp_tac - (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm not_False_eq_True}) 1 THEN rec_tac end | Sidecond t => @@ -338,7 +338,7 @@ val ho_args = ho_args_of mode args val f_tac = (case f of - Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps + Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode, @{thm Product_Type.split_conv}]) 1 | Free _ => all_tac @@ -383,7 +383,8 @@ preds in (* only simplify the one assumption *) - full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm pred.sel} :: defs) 1 + full_simp_tac (put_simpset HOL_basic_ss' ctxt + |> Simplifier.add_simps (@{thm pred.sel} :: defs)) 1 (* need better control here! *) THEN trace_tac ctxt options "after sidecond2 simplification" end @@ -394,7 +395,7 @@ val (in_ts, _) = split_mode mode ts; val split_simpset = put_simpset HOL_basic_ss' ctxt - addsimps [@{thm case_prod_eta}, @{thm case_prod_beta}, + |> Simplifier.add_simps [@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] fun prove_prems2 out_ts [] = trace_tac ctxt options "before prove_match2 - last call:" @@ -441,10 +442,11 @@ trace_tac ctxt options "before neg prem 2" THEN eresolve_tac ctxt @{thms bindE} 1 THEN (if is_some name then - full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps - [Core_Data.predfun_definition_of ctxt (the name) mode]) 1 + full_simp_tac (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps [Core_Data.predfun_definition_of ctxt (the name) mode]) 1 THEN eresolve_tac ctxt @{thms not_predE} 1 - THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms not_False_eq_True}) 1 + THEN simp_tac (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps @{thms not_False_eq_True}) 1 THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) else eresolve_tac ctxt @{thms not_predE'} 1) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Aug 07 21:40:03 2025 +0200 @@ -56,24 +56,24 @@ fun add ts = Thm.declaration_attribute (fn th => fn context => context |> Data.map (fn (ss, ts') => - (simpset_map (Context.proof_of context) (fn ctxt => ctxt addsimps [th]) ss, + (simpset_map (Context.proof_of context) (Simplifier.add_simp th) ss, merge (op aconv) (ts', ts)))) fun del ts = Thm.declaration_attribute (fn th => fn context => context |> Data.map (fn (ss, ts') => - (simpset_map (Context.proof_of context) (fn ctxt => ctxt delsimps [th]) ss, + (simpset_map (Context.proof_of context) (Simplifier.del_simp th) ss, subtract (op aconv) ts' ts))) fun simp_thms_conv ctxt = - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms}); + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms simp_thms}); val FWD = Drule.implies_elim_list; val true_tm = \<^cterm>\True\; val false_tm = \<^cterm>\False\; -val presburger_ss = simpset_of (\<^context> addsimps @{thms zdvd1_eq}); +val presburger_ss = simpset_of (\<^context> |> Simplifier.add_simps @{thms zdvd1_eq}); val lin_ss = simpset_of (put_simpset presburger_ss \<^context> - addsimps (@{thms dvd_eq_mod_eq_0 add.assoc [where 'a = int] add.commute [where 'a = int] add.left_commute [where 'a = int] + |> Simplifier.add_simps (@{thms dvd_eq_mod_eq_0 add.assoc [where 'a = int] add.commute [where 'a = int] add.left_commute [where 'a = int] mult.assoc [where 'a = int] mult.commute [where 'a = int] mult.left_commute [where 'a = int] })); @@ -109,7 +109,8 @@ val eval_ss = simpset_of (put_simpset presburger_ss \<^context> - addsimps @{thms simp_from_to} delsimps @{thms insert_iff bex_triv}); + |> Simplifier.add_simps @{thms simp_from_to} + |> Simplifier.del_simps @{thms insert_iff bex_triv}); fun eval_conv ctxt = Simplifier.rewrite (put_simpset eval_ss ctxt); (* recognising cterm without moving to terms *) @@ -567,7 +568,7 @@ val conv_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps (@{thms simp_thms} @ take 4 @{thms ex_simps} @ + |> Simplifier.add_simps (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, @{thm all_not_ex}, @{thm ex_disj_distrib}])); fun conv ctxt p = @@ -701,7 +702,7 @@ (t, procedure t)))); val comp_ss = - simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm}); + simpset_of (put_simpset HOL_ss \<^context> |> Simplifier.add_simps @{thms semiring_norm}); fun strip_objimp ct = (case Thm.term_of ct of @@ -721,7 +722,7 @@ local val all_maxscope_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps map (fn th => th RS sym) @{thms "all_simps"}) + |> Simplifier.add_simps (map (fn th => th RS sym) @{thms "all_simps"})) in fun thin_prems_tac ctxt P = simp_tac (put_simpset all_maxscope_ss ctxt) THEN' @@ -810,20 +811,20 @@ local val ss1 = simpset_of (put_simpset comp_ss \<^context> - addsimps @{thms simp_thms} @ + |> Simplifier.add_simps (@{thms simp_thms} @ [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] - @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}] + @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]) |> Splitter.add_split @{thm "zdiff_int_split"}) val ss2 = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"}, + |> Simplifier.add_simps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, @{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}] |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]) val div_mod_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms + |> Simplifier.add_simps @{thms simp_thms mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq mod_add_eq div_add1_eq [symmetric] div_add1_eq [symmetric] mod_self mod_by_0 div_by_0 @@ -834,7 +835,7 @@ |> 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]}] + |> Simplifier.add_simps [@{thm minus_div_mult_eq_mod [symmetric]}] |> fold Splitter.add_split [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) @@ -867,7 +868,9 @@ fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => let val simpset_ctxt = - put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths + put_simpset (fst (get ctxt)) ctxt + |> Simplifier.del_simps del_ths + |> Simplifier.add_simps add_ths in Method.insert_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\arith\)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Thu Aug 07 21:40:03 2025 +0200 @@ -58,7 +58,7 @@ val ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}); + |> Simplifier.add_simps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}); fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Aug 07 21:40:03 2025 +0200 @@ -81,7 +81,7 @@ val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one}, @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; val rew_ts = map (Logic.dest_equals o Thm.prop_of) rew_thms; -val rew_ss = simpset_of (put_simpset HOL_ss \<^context> addsimps rew_thms); +val rew_ss = simpset_of (put_simpset HOL_ss \<^context> |> Simplifier.add_simps rew_thms); in @@ -146,9 +146,9 @@ let val proj_simps = map (snd o snd) proj_defs; fun tac { context = ctxt, prems = _ } = - ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps proj_simps)) + ALLGOALS (simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps proj_simps)) THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) - THEN ALLGOALS (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms fst_conv snd_conv})); + THEN ALLGOALS (simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps @{thms fst_conv snd_conv})); in (map (fn prop => Goal.prove_sorry lthy [v] [] prop tac) eqs, lthy) end; in lthy diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Aug 07 21:40:03 2025 +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} - |> Simplifier.add_proc regularize_simproc) + mk_minimal_simpset ctxt + |> Simplifier.add_simps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + |> Simplifier.add_proc regularize_simproc |> Simplifier.add_unsafe_solver equiv_solver |> Simplifier.add_unsafe_solver quotient_solver val eq_eqvs = eq_imp_rel_get ctxt @@ -511,7 +511,8 @@ @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs val simpset = - (mk_minimal_simpset ctxt) addsimps thms + mk_minimal_simpset ctxt + |> Simplifier.add_simps thms |> Simplifier.add_unsafe_solver quotient_solver in EVERY' [ @@ -607,7 +608,7 @@ fun descend_procedure_tac ctxt simps = let - val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) + val simpset = mk_minimal_simpset ctxt |> Simplifier.add_simps (simps @ default_unfolds) in full_simp_tac simpset THEN' Object_Logic.full_atomize_tac ctxt @@ -658,7 +659,7 @@ fun partiality_descend_procedure_tac ctxt simps = let - val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) + val simpset = mk_minimal_simpset ctxt |> Simplifier.add_simps (simps @ default_unfolds) in full_simp_tac simpset THEN' Object_Logic.full_atomize_tac ctxt @@ -693,7 +694,7 @@ (* the tactic leaves three subgoals to be proved *) fun lift_procedure_tac ctxt simps rthm = let - val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds) + val simpset = mk_minimal_simpset ctxt |> Simplifier.add_simps (simps @ default_unfolds) in full_simp_tac simpset THEN' Object_Logic.full_atomize_tac ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/cvc5_replay.ML --- a/src/HOL/Tools/SMT/cvc5_replay.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/cvc5_replay.ML Thu Aug 07 21:40:03 2025 +0200 @@ -69,7 +69,7 @@ (Symtab.map (K rewrite) insts) decls (concl, ctxt) - |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules) + |> Simplifier.simplify (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules) end fun add_used_asserts_in_step (Lethe_Proof.Lethe_Replay_Node {prems, @@ -300,7 +300,7 @@ proof_ctxt = [], concl = Thm.prop_of th' |> Simplifier.rewrite_term (Proof_Context.theory_of - (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [], + (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules)) rewrite_rules [], bounds = [], insts = Symtab.empty, declarations = [], diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/cvc_proof_parse.ML --- a/src/HOL/Tools/SMT/cvc_proof_parse.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/cvc_proof_parse.ML Thu Aug 07 21:40:03 2025 +0200 @@ -39,7 +39,7 @@ #> Thm.prop_of #> snd o Logic.dest_equals #> Simplifier.rewrite_term (Proof_Context.theory_of - (empty_simpset ctxt addsimps rewrite_rules (*@ @{thms eq_True} still useful?*))) rewrite_rules [] + (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules (*@ @{thms eq_True} still useful?*))) rewrite_rules [] val normalize = @@ -48,7 +48,7 @@ #> Thm.prop_of #> snd o Logic.dest_equals #> Simplifier.rewrite_term (Proof_Context.theory_of - (empty_simpset ctxt addsimps rewrite_rules @ @{thms eq_True})) rewrite_rules [] + (empty_simpset ctxt |> Simplifier.add_simps (rewrite_rules @ @{thms eq_True}))) rewrite_rules [] in (expand th) aconv (normalize th') end fun parse_proof_unsatcore ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/lethe_replay_methods.ML --- a/src/HOL/Tools/SMT/lethe_replay_methods.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML Thu Aug 07 21:40:03 2025 +0200 @@ -385,7 +385,8 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) + |> Simplifier.add_simps @{thms simp_thms} + |> Simplifier.add_simps thms |> Simplifier.asm_full_simp_tac (* sko_forall requires the assumptions to be able to prove the equivalence in case of double @@ -401,7 +402,8 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) + |> Simplifier.add_simps @{thms simp_thms} + |> Simplifier.add_simps thms |> Simplifier.full_simp_tac val try_provers = SMT_Replay_Methods.try_provers @@ -990,7 +992,7 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel}) + |> Simplifier.add_simps (thms @ @{thms if_True if_False refl simp_thms if_cancel}) |> Simplifier.add_eqcong @{thm verit_ite_if_cong} |> Simplifier.full_simp_tac in @@ -1017,7 +1019,7 @@ fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => 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} + |> Simplifier.add_simps @{thms HOL.simp_thms HOL.all_simps} |> Simplifier.add_proc @{simproc HOL.defined_All} |> Simplifier.add_proc @{simproc HOL.defined_Ex}) THEN' TRY' (Blast.blast_tac ctxt) @@ -1118,7 +1120,7 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms) + |> Simplifier.add_simps thms |> Simplifier.full_simp_tac fun rewrite_only_thms_tmp ctxt thms = rewrite_only_thms ctxt thms @@ -1129,7 +1131,8 @@ |> empty_simpset |> put_simpset HOL_basic_ss |> Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]} - |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms}) + |> Simplifier.add_simps thms + |> Simplifier.add_simps @{thms simp_thms} |> Simplifier.full_simp_tac fun chain_rewrite_thms ctxt thms = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Aug 07 21:40:03 2025 +0200 @@ -429,7 +429,8 @@ fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t val proper_num_ss = - simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms Num.numeral_One minus_zero}) + simpset_of (put_simpset HOL_ss \<^context> + |> Simplifier.add_simps @{thms Num.numeral_One minus_zero}) fun norm_num_conv ctxt = SMT_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/smt_replay.ML --- a/src/HOL/Tools/SMT/smt_replay.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/smt_replay.ML Thu Aug 07 21:40:03 2025 +0200 @@ -152,7 +152,7 @@ val basic_simpset = simpset_of (put_simpset HOL_ss \<^context> - addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special + |> Simplifier.add_simps @{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} |> fold Simplifier.add_proc [\<^simproc>\numeral_divmod\, fast_int_arith_simproc, antisym_le_simproc, antisym_less_simproc]) @@ -169,7 +169,7 @@ 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) + simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt |> Simplifier.add_simps rules) end @@ -178,7 +178,8 @@ val remove_fun_app = mk_meta_eq @{thm fun_app_def} fun rewrite_conv _ [] = Conv.all_conv - | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) + | rewrite_conv ctxt eqs = + Simplifier.full_rewrite (empty_simpset ctxt |> Simplifier.add_simps eqs) val rewrite_true_rule = @{lemma "True \ \ False" by simp} val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule] diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/smt_replay_arith.ML --- a/src/HOL/Tools/SMT/smt_replay_arith.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_arith.ML Thu Aug 07 21:40:03 2025 +0200 @@ -81,13 +81,13 @@ fun arith_full_simps ctxt thms = ctxt |> empty_simpset - |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms - addsimps arith_thms - |> 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}]) + |> put_simpset HOL_basic_ss + |> Simplifier.add_simps thms + |> Simplifier.add_simps arith_thms + |> 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 val final_False = combined |> arith_full_simps ctxt (Named_Theorems.get ctxt @{named_theorems ac_simps}) @@ -106,7 +106,7 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps thms) + |> Simplifier.add_simps thms |> Simplifier.full_simp_tac fun la_farkas args ctxt = diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/smt_replay_methods.ML --- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 07 21:40:03 2025 +0200 @@ -475,7 +475,7 @@ ctxt |> empty_simpset |> put_simpset HOL_basic_ss - |> (fn ctxt => ctxt addsimps @{thms not_not eq_commute}) + |> Simplifier.add_simps @{thms not_not eq_commute} in prove ctxt t (fn _ => EVERY' (map (fn thm => K (unfold_tac ctxt [thm])) ((map_filter reorder_for_simp thms))) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/SMT/verit_replay.ML --- a/src/HOL/Tools/SMT/verit_replay.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/SMT/verit_replay.ML Thu Aug 07 21:40:03 2025 +0200 @@ -74,7 +74,7 @@ (Symtab.map (K rewrite) insts) decls (concl, ctxt) - |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules) + |> Simplifier.simplify (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules) end fun add_used_asserts_in_step (Lethe_Proof.Lethe_Replay_Node {prems, @@ -244,7 +244,7 @@ proof_ctxt = [], concl = Thm.prop_of th |> Simplifier.rewrite_term (Proof_Context.theory_of - (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [], + (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules)) rewrite_rules [], bounds = [], insts = Symtab.empty, declarations = [], diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 07 21:40:03 2025 +0200 @@ -186,7 +186,7 @@ Method.insert_tac ctxt local_facts THEN' (case meth of Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts - | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) + | Simp_Method => Simplifier.asm_full_simp_tac (ctxt |> Simplifier.add_simps global_facts) | _ => Method.insert_tac ctxt global_facts THEN' (case meth of diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/arith_data.ML Thu Aug 07 21:40:03 2025 +0200 @@ -89,10 +89,11 @@ (K (EVERY [expand_tac, norm_tac ctxt])))); fun simp_all_tac rules ctxt = - ALLGOALS (safe_simp_tac (put_simpset HOL_ss ctxt addsimps rules)); + ALLGOALS (safe_simp_tac (put_simpset HOL_ss ctxt |> Simplifier.add_simps rules)); fun simplify_meta_eq rules ctxt = - simplify (put_simpset HOL_basic_ss ctxt addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}) - o mk_meta_eq; + simplify (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps rules + |> Simplifier.add_eqcong @{thm eq_cong2}) o mk_meta_eq; end; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Thu Aug 07 21:40:03 2025 +0200 @@ -195,7 +195,7 @@ EVERY [ resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1, ALLGOALS (EVERY' - [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), + [asm_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps case_rewrites), resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) |> Drule.export_without_context; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/functor.ML --- a/src/HOL/Tools/functor.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/functor.ML Thu Aug 07 21:40:03 2025 +0200 @@ -81,7 +81,8 @@ (* mapper properties *) val compositionality_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [Simpdata.mk_eq @{thm comp_def}]); + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def})); fun make_comp_prop ctxt variances (tyco, mapper) = let @@ -131,7 +132,8 @@ in (comp_prop, prove_compositionality) end; val identity_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps [Simpdata.mk_eq @{thm id_def}]); + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simp (Simpdata.mk_eq @{thm id_def})); fun make_id_prop ctxt variances (tyco, mapper) = let diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/groebner.ML Thu Aug 07 21:40:03 2025 +0200 @@ -397,13 +397,13 @@ val nnf_simps = @{thms nnf_simps}; fun weak_dnf_conv ctxt = - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms weak_dnf_simps}); + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms weak_dnf_simps}); val initial_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps nnf_simps - addsimps [not_all, not_ex] - addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps})); + |> Simplifier.add_simps nnf_simps + |> Simplifier.add_simps [not_all, not_ex] + |> Simplifier.add_simps (map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}))); fun initial_conv ctxt = Simplifier.rewrite (put_simpset initial_ss ctxt); @@ -520,7 +520,8 @@ fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v)) (Thm.abstract_rule (getname v) v th) fun simp_ex_conv ctxt = - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)}) + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps @{thms simp_thms(39)}) fun free_in v t = Cterms.defined (Cterms.build (Drule.add_frees_cterm t)) v; @@ -655,7 +656,7 @@ in holify_polynomial end ; -fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]); +fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp idom_thm); fun prove_nz n = eqF_elim (ring_eq_conv (Thm.mk_binop eq_tm (mk_const n) (mk_const @0))); val neq_01 = prove_nz @1; fun neq_rule n th = [prove_nz n, th] MRS neq_thm; @@ -745,7 +746,7 @@ val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse) val th3 = Thm.equal_elim - (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym]) + (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp (not_ex RS sym)) (th2 |> Thm.cprop_of)) th2 in specl (Cterms.list_set_rev avs) ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS @{thm notnotD}) @@ -784,7 +785,7 @@ val poly_eq_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms} + |> Simplifier.add_simps @{thms simp_thms} |> Simplifier.add_proc poly_eq_simproc) local @@ -920,8 +921,9 @@ fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt - addsimps (Named_Theorems.get ctxt \<^named_theorems>\algebra\) - delsimps del_thms addsimps add_thms); + |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\algebra\) + |> Simplifier.del_simps del_thms + |> Simplifier.add_simps add_thms); fun ring_tac add_ths del_ths ctxt = Object_Logic.full_atomize_tac ctxt diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/inductive.ML Thu Aug 07 21:40:03 2025 +0200 @@ -993,7 +993,7 @@ fold_rev lambda params (fp_const $ fp_fun))) ||> Proof_Context.restore_naming lthy; val fp_def' = - Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) + Simplifier.rewrite (put_simpset HOL_basic_ss lthy' |> Simplifier.add_simp fp_def) (Thm.cterm_of lthy' (list_comb (rec_const, params))); val specs = if is_auxiliary then diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/inductive_set.ML Thu Aug 07 21:40:03 2025 +0200 @@ -62,7 +62,8 @@ | decomp _ = NONE; val simp = full_simp_tac - (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}) 1; + (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps @{thms mem_Collect_eq case_prod_conv}) 1; fun mk_rew t = (case strip_abs_vars t of [] => NONE | xs => (case decomp (strip_abs_body t) of @@ -235,7 +236,7 @@ end) in Simplifier.simplify - (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv} + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms mem_Collect_eq case_prod_conv} |> Simplifier.add_proc \<^simproc>\Collect_mem\) thm'' |> zero_var_indexes |> eta_contract_thm ctxt (equal p) end; @@ -384,7 +385,7 @@ thm |> Thm.instantiate (TVars.empty, Vars.make insts) |> Simplifier.full_simplify - (put_simpset HOL_basic_ss ctxt addsimps to_set_simps + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps to_set_simps |> Simplifier.add_proc (strong_ind_simproc pred_arities) |> Simplifier.add_proc \<^simproc>\Collect_mem\) |> Rule_Cases.save thm @@ -489,8 +490,8 @@ (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)), list_comb (c, params)))))) (K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN - simp_tac (put_simpset HOL_basic_ss lthy addsimps - [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1)) + simp_tac (put_simpset HOL_basic_ss lthy + |> Simplifier.add_simps [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1)) in lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"), [Attrib.internal \<^here> (K pred_set_conv_att)]), diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/lin_arith.ML Thu Aug 07 21:40:03 2025 +0200 @@ -105,10 +105,10 @@ val trace = Attrib.setup_config_bool \<^binding>\linarith_trace\ (K false); fun nnf_simpset ctxt = - (empty_simpset ctxt - |> Simplifier.set_mkeqTrue mk_eq_True - |> Simplifier.set_mksimps (mksimps mksimps_pairs)) - addsimps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj + empty_simpset ctxt + |> Simplifier.set_mkeqTrue mk_eq_True + |> Simplifier.set_mksimps (mksimps mksimps_pairs) + |> Simplifier.add_simps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj de_Morgan_conj not_all not_ex not_not} fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt) diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Aug 07 21:40:03 2025 +0200 @@ -28,7 +28,7 @@ (*Maps n to #n for n = 1, 2*) val numeral_syms = [@{thm numeral_One} RS sym, @{thm numeral_2_eq_2} RS sym]; val numeral_sym_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps numeral_syms); + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps numeral_syms); (*Utilities*) @@ -158,18 +158,18 @@ val norm_ss1 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps numeral_syms @ add_0s @ mult_1s @ - [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps}) + |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @ + [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})) val norm_ss2 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps}) + |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps})) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps add_0s @ bin_simps); + |> Simplifier.add_simps (add_0s @ bin_simps)); fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)); val simplify_meta_eq = simplify_meta_eq @@ -231,17 +231,17 @@ val norm_ss1 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps}) + |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps})) val norm_ss2 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps}) + |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps})) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps add_0s @ bin_simps); + |> Simplifier.add_simps (add_0s @ bin_simps)); fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = simplify_meta_eq @@ -262,16 +262,17 @@ val norm_ss1 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps}) + |> Simplifier.add_simps + (numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})) val norm_ss2 = simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> - addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps}) + |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps})) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps bin_simps) + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps bin_simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = simplify_meta_eq @@ -357,7 +358,7 @@ val trans_tac = Numeral_Simprocs.trans_tac val norm_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps mult_1s @ @{thms ac_simps}) + |> Simplifier.add_simps (mult_1s @ @{thms ac_simps})) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) val simplify_meta_eq = cancel_simplify_meta_eq diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Thu Aug 07 21:40:03 2025 +0200 @@ -220,16 +220,16 @@ val norm_ss1 = simpset_of (put_simpset num_ss \<^context> - addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ @{thms minus_zero ac_simps}) + |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @ + diff_simps @ @{thms minus_zero ac_simps})) val norm_ss2 = simpset_of (put_simpset num_ss \<^context> - addsimps non_add_simps @ mult_minus_simps) + |> Simplifier.add_simps (non_add_simps @ mult_minus_simps)) val norm_ss3 = simpset_of (put_simpset num_ss \<^context> - addsimps minus_from_mult_simps @ @{thms ac_simps minus_mult_commute}) + |> Simplifier.add_simps (minus_from_mult_simps @ @{thms ac_simps minus_mult_commute})) structure CancelNumeralsCommon = struct @@ -246,7 +246,7 @@ THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps @@ -300,7 +300,7 @@ THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps @@ -323,7 +323,7 @@ val trans_tac = trans_tac val norm_ss1a = - simpset_of (put_simpset norm_ss1 \<^context> addsimps (inverse_1s @ divide_simps)) + simpset_of (put_simpset norm_ss1 \<^context> |> Simplifier.add_simps (inverse_1s @ divide_simps)) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) @@ -331,7 +331,7 @@ val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps (simps @ @{thms add_frac_eq not_False_eq_True})) + |> Simplifier.add_simps (simps @ @{thms add_frac_eq not_False_eq_True})) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps @@ -350,7 +350,9 @@ structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = struct - val assoc_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute}) + val assoc_ss = + simpset_of + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps @{thms ac_simps minus_mult_commute}) val eq_reflection = eq_reflection val is_numeral = can HOLogic.dest_number end; @@ -366,11 +368,14 @@ val trans_tac = trans_tac val norm_ss1 = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps minus_from_mult_simps @ mult_1s) + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps (minus_from_mult_simps @ mult_1s)) val norm_ss2 = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ mult_minus_simps) + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps (simps @ mult_minus_simps)) val norm_ss3 = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap}) + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps @{thms ac_simps minus_mult_commute numeral_times_minus_swap}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) @@ -379,7 +384,8 @@ (* simp_thms are necessary because some of the cancellation rules below (e.g. mult_less_cancel_left) introduce various logical connectives *) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ @{thms simp_thms}) + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps (simps @ @{thms simp_thms})) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq @@ -500,7 +506,8 @@ val find_first = find_first_t [] val trans_tac = trans_tac val norm_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps mult_1s @ @{thms ac_simps minus_mult_commute}) + simpset_of (put_simpset HOL_basic_ss \<^context> + |> Simplifier.add_simps (mult_1s @ @{thms ac_simps minus_mult_commute})) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) val simplify_meta_eq = cancel_simplify_meta_eq @@ -592,7 +599,7 @@ val z = Thm.instantiate_cterm (TVars.make1 (zero_tvar, T), Vars.empty) zero val eq = Thm.instantiate_cterm (TVars.make1 (type_tvar, T), Vars.empty) geq val th = - Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) + Simplifier.rewrite (ctxt |> Simplifier.add_simps @{thms simp_thms}) (HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply eq t) z))) in Thm.equal_elim (Thm.symmetric th) TrueI end @@ -701,7 +708,7 @@ val field_comp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms semiring_norm + |> Simplifier.add_simps @{thms semiring_norm mult_numeral_1 mult_numeral_1_right divide_numeral_1 @@ -728,7 +735,7 @@ fun field_comp_conv ctxt = Simplifier.rewrite (put_simpset field_comp_ss ctxt) then_conv - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}) + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms numeral_One}) end diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/record.ML Thu Aug 07 21:40:03 2025 +0200 @@ -477,8 +477,8 @@ make_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, - simpset = simpset_map ctxt0 (fn ctxt => ctxt addsimps simps) simpset, - defset = simpset_map ctxt0 (fn ctxt => ctxt addsimps defs) defset} + simpset = simpset_map ctxt0 (Simplifier.add_simps simps) simpset, + defset = simpset_map ctxt0 (Simplifier.add_simps defs) defset} equalities extinjects extsplit splits extfields fieldext; in Data.put data thy end; @@ -963,7 +963,8 @@ (fn {context = ctxt', ...} => simp_tac (put_simpset defset ctxt') 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN - TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply id_o o_id}) 1)); + TRY (simp_tac (put_simpset HOL_ss ctxt' + |> Simplifier.add_simps @{thms id_apply id_o o_id}) 1)); val dest = if is_sel_upd_pair thy acc upd then @{thm o_eq_dest} @@ -987,7 +988,7 @@ (fn {context = ctxt', ...} => simp_tac (put_simpset defset ctxt') 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN - TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply}) 1)); + TRY (simp_tac (put_simpset HOL_ss ctxt' |> Simplifier.add_simps @{thms id_apply}) 1)); val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest}; in Drule.export_without_context (othm RS dest) end; @@ -1386,7 +1387,7 @@ SOME (Goal.prove_sorry_global thy [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset (get_simpset thy) ctxt' - addsimps @{thms simp_thms} + |> Simplifier.add_simps @{thms simp_thms} |> Simplifier.add_proc (split_simproc (K ~1))) 1)) end handle TERM _ => NONE) | _ => NONE) @@ -1423,9 +1424,9 @@ val _ $ (_ $ Var (r, _)) = Thm.concl_of induct_thm; val thm = infer_instantiate ctxt [(r, Thm.cterm_of ctxt free)] induct_thm; in - simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN + simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms induct_atomize}) i THEN resolve_tac ctxt [thm] i THEN - simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_rulify}) i + simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms induct_rulify}) i end; val split_frees_tacs = @@ -1448,7 +1449,7 @@ val thms' = @{thms o_apply K_record_comp} @ thms; in EVERY split_frees_tacs THEN - full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' |> add_simproc) i + full_simp_tac (put_simpset (get_simpset thy) ctxt |> Simplifier.add_simps thms' |> add_simproc) i end); @@ -1632,7 +1633,7 @@ simplify (put_simpset HOL_ss defs_ctxt) (Goal.prove_sorry_global defs_thy [] [] inject_prop (fn {context = ctxt', ...} => - simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [ext_def]) 1 THEN + simp_tac (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simp ext_def) 1 THEN REPEAT_DETERM (resolve_tac ctxt' @{thms refl_conj_eq} 1 ORELSE Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE @@ -1651,7 +1652,7 @@ val start = infer_instantiate defs_ctxt [(("y", 0), Thm.cterm_of defs_ctxt ext)] surject_assist_idE; val tactic1 = - simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN + simp_tac (put_simpset HOL_basic_ss defs_ctxt |> Simplifier.add_simp ext_def) 1 THEN REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1; val tactic2 = REPEAT (resolve_tac defs_ctxt [surject_assistI] 1 THEN resolve_tac defs_ctxt [refl] 1); @@ -1996,7 +1997,7 @@ val terminal = resolve_tac ext_ctxt [updacc_eq_idI] 1 THEN resolve_tac ext_ctxt [refl] 1; val tactic = - simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN + simp_tac (put_simpset HOL_basic_ss ext_ctxt |> Simplifier.add_simps ext_defs) 1 THEN REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal); val updaccs = Seq.list_of (tactic init_thm); in @@ -2138,7 +2139,7 @@ val sel_upd_ss = simpset_of (put_simpset record_ss defs_ctxt - addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms)); + |> Simplifier.add_simps (sel_defs @ accessor_thms @ upd_defs @ updator_thms)); val (sel_convs, upd_convs) = timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () => @@ -2152,7 +2153,7 @@ val (fold_congs, unfold_congs) = timeit_msg defs_ctxt "record upd fold/unfold congs:" (fn () => let val symdefs = map Thm.symmetric (sel_defs @ upd_defs); - val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs; + val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt |> Simplifier.add_simps symdefs; val ua_congs = map (Drule.export_without_context o simplify fold_ctxt) upd_acc_cong_assists; in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end); @@ -2178,12 +2179,12 @@ (fn {context = ctxt', ...} => EVERY [resolve_tac ctxt' [surject_assist_idE] 1, - simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ext_defs) 1, + simp_tac (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simps ext_defs) 1, REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE (resolve_tac ctxt' [surject_assistI] 1 THEN simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt' - addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))])); + |> Simplifier.add_simps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))])); val cases_scheme = timeit_msg defs_ctxt "record cases_scheme proof:" (fn () => Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop) @@ -2196,7 +2197,7 @@ (fn {context = ctxt', ...} => try_param_tac ctxt' rN cases_scheme 1 THEN ALLGOALS (asm_full_simp_tac - (put_simpset HOL_basic_ss ctxt' addsimps @{thms unit_all_eq1})))); + (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simps @{thms unit_all_eq1})))); val split_meta = timeit_msg defs_ctxt "record split_meta proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_meta_prop @@ -2218,7 +2219,7 @@ Goal.prove_sorry_global defs_thy [] [] split_ex_prop (fn {context = ctxt', ...} => simp_tac - (put_simpset HOL_basic_ss ctxt' addsimps + (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simps (@{lemma "\x. P x \ \ (\x. \ P x)" by simp} :: @{thms not_not Not_eq_iff})) 1 THEN resolve_tac ctxt' [split_object] 1)); @@ -2226,7 +2227,8 @@ val equality = timeit_msg defs_ctxt "record equality proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] equality_prop (fn {context = ctxt', ...} => - asm_full_simp_tac (put_simpset record_ss ctxt' addsimps (split_meta :: sel_convs)) 1)); + asm_full_simp_tac (put_simpset record_ss ctxt' + |> Simplifier.add_simps (split_meta :: sel_convs)) 1)); val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'), (_, fold_congs'), (_, unfold_congs'), diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/reification.ML Thu Aug 07 21:40:03 2025 +0200 @@ -19,7 +19,8 @@ val FWD = curry (op OF); -fun rewrite_with ctxt eqs = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps eqs); +fun rewrite_with ctxt eqs = + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps eqs); val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp} diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Thu Aug 07 21:40:03 2025 +0200 @@ -107,7 +107,7 @@ (* extra-logical functions *) val semiring_norm_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms semiring_norm}); + simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps @{thms semiring_norm}); val semiring_funs = {is_const = can HOLogic.dest_number o Thm.term_of, @@ -119,7 +119,8 @@ (case Rat.dest x of (i, 1) => i | _ => error "int_of_rat: bad int")), conv = (fn ctxt => Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) - then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))}; + then_conv Simplifier.rewrite + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms numeral_One}))}; val divide_const = Thm.cterm_of \<^context> (Logic.varify_global \<^term>\(/)\); val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) []; @@ -256,19 +257,19 @@ val is_number = can dest_number; fun numeral01_conv ctxt = - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}]); + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm numeral_One}); fun zero1_numeral_conv ctxt = - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One} RS sym]); + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp (@{thm numeral_One} RS sym)); fun zerone_conv ctxt cv = zero1_numeral_conv ctxt then_conv cv then_conv numeral01_conv ctxt; val nat_add_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms arith_simps} @ @{thms diff_nat_numeral} @ @{thms rel_simps} + |> Simplifier.add_simps (@{thms arith_simps} @ @{thms diff_nat_numeral} @ @{thms rel_simps} @ @{thms if_False if_True Nat.add_0 add_Suc add_numeral_left Suc_eq_plus1} - @ map (fn th => th RS sym) @{thms numerals}); + @ map (fn th => th RS sym) @{thms numerals})); fun nat_add_conv ctxt = zerone_conv ctxt (Simplifier.rewrite (put_simpset nat_add_ss ctxt)); @@ -849,8 +850,8 @@ val nat_exp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps}) - addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]); + |> Simplifier.add_simps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps}) + |> Simplifier.add_simps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]); (* various normalizing conversions *) @@ -861,7 +862,8 @@ val pow_conv = Conv.arg_conv (Simplifier.rewrite (put_simpset nat_exp_ss ctxt)) then_conv Simplifier.rewrite - (put_simpset HOL_basic_ss ctxt addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) + (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps [nth (snd semiring) 31, nth (snd semiring) 34]) then_conv conv ctxt val dat = (is_const, conv ctxt, conv ctxt, pow_conv) in semiring_normalizers_conv vars semiring ring field dat term_ord end; diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Aug 07 21:40:03 2025 +0200 @@ -302,7 +302,8 @@ fun elim_image_tac ctxt = eresolve_tac ctxt @{thms imageE} THEN' REPEAT_DETERM o CHANGED o - (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case}) + (TRY o full_simp_tac + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms split_paired_all prod.case}) THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt) @@ -320,9 +321,9 @@ REPEAT_DETERM1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms SigmaI} ORELSE' ((resolve_tac ctxt @{thms CollectI} ORELSE' resolve_tac ctxt [collectI']) THEN' - TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])) + TRY o simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm prod.case})) ORELSE' ((resolve_tac ctxt @{thms vimageI2} ORELSE' resolve_tac ctxt [vimageI2']) THEN' - TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])) + TRY o simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm prod.case})) ORELSE' (resolve_tac ctxt @{thms image_eqI} THEN' (REPEAT_DETERM o (resolve_tac ctxt @{thms refl} @@ -347,17 +348,18 @@ ORELSE' dresolve_tac ctxt @{thms iffD1[OF mem_Sigma_iff]} ORELSE' eresolve_tac ctxt @{thms conjE} ORELSE' ((eresolve_tac ctxt @{thms CollectE} ORELSE' eresolve_tac ctxt [collectE']) THEN' - TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN' + TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm prod.case}) THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac ctxt @{thms refl}) ORELSE' (eresolve_tac ctxt @{thms imageE} THEN' (REPEAT_DETERM o CHANGED o - (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case}) + (TRY o full_simp_tac + (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms split_paired_all prod.case}) THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac ctxt @{thms refl}))) ORELSE' eresolve_tac ctxt @{thms ComplE} ORELSE' ((eresolve_tac ctxt @{thms vimageE} ORELSE' eresolve_tac ctxt [vimageE']) - THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) + THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm prod.case}) THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac ctxt @{thms refl})) fun tac ctxt fm = @@ -403,7 +405,7 @@ val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case} fun tac ctxt = resolve_tac ctxt @{thms set_eqI} - THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms) + THEN' simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps unfold_thms) THEN' resolve_tac ctxt @{thms iffI} THEN' REPEAT_DETERM o resolve_tac ctxt @{thms exI} THEN' resolve_tac ctxt @{thms conjI} THEN' resolve_tac ctxt @{thms refl} THEN' assume_tac ctxt @@ -411,7 +413,7 @@ THEN' eresolve_tac ctxt @{thms conjE} THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject} THEN' Subgoal.FOCUS (fn {prems, context = ctxt', ...} => - simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (filter is_eq prems)) 1) ctxt + simp_tac (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simps (filter is_eq prems)) 1) ctxt THEN' TRY o assume_tac ctxt in case try mk_term (Thm.term_of ct) of @@ -439,7 +441,7 @@ val ct = Thm.cterm_of ctxt' t' fun unfold_conv thms = Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) - (empty_simpset ctxt' addsimps thms) + (empty_simpset ctxt' |> Simplifier.add_simps thms) val prep_eq = (comprehension_conv ctxt' then_conv unfold_conv prep_thms) ct val t'' = Thm.term_of (Thm.rhs_of prep_eq) fun mk_thm (fm, t''') = Goal.prove ctxt' [] [] @@ -477,7 +479,7 @@ let fun unfold_conv thms = Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) - (empty_simpset ctxt addsimps thms) + (empty_simpset ctxt |> Simplifier.add_simps thms) val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex in case base_proc ctxt (Thm.rhs_of prep_thm) of diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/HOL/Tools/simpdata.ML Thu Aug 07 21:40:03 2025 +0200 @@ -195,10 +195,11 @@ |> simpset_of; fun hol_simplify ctxt rews = - Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews); + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps rews); fun unfold_tac ctxt ths = - ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths)); + ALLGOALS (full_simp_tac + (clear_simpset (put_simpset HOL_basic_ss ctxt) |> Simplifier.add_simps ths)); end; diff -r 55a71dd13ca0 -r 73af47bc277c src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/Tools/induct.ML Thu Aug 07 21:40:03 2025 +0200 @@ -230,7 +230,7 @@ (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)), simpset_of ((empty_simpset \<^context> - |> Simplifier.add_proc rearrange_eqs_simproc) addsimps [Drule.norm_hhf_eq])); + |> Simplifier.add_proc rearrange_eqs_simproc) |> Simplifier.add_simp Drule.norm_hhf_eq)); fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1), ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) = ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)), @@ -345,10 +345,10 @@ context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f; fun induct_simp f = - Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm]))); + Thm.declaration_attribute (fn thm => map_simpset (f thm)); -val induct_simp_add = induct_simp (op addsimps); -val induct_simp_del = induct_simp (op delsimps); +val induct_simp_add = induct_simp Simplifier.add_simp; +val induct_simp_del = induct_simp Simplifier.del_simp; end; diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/Datatype.thy --- a/src/ZF/Datatype.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/Datatype.thy Thu Aug 07 21:40:03 2025 +0200 @@ -104,8 +104,8 @@ val goal = Logic.mk_equals (old, new); val thm = Goal.prove ctxt [] [] goal (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN - simp_tac (put_simpset datatype_ss ctxt addsimps - (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) + simp_tac (put_simpset datatype_ss ctxt + |> Simplifier.add_simps (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) handle ERROR msg => (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); raise Match) diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/Tools/datatype_package.ML Thu Aug 07 21:40:03 2025 +0200 @@ -334,8 +334,8 @@ (*Proves a single recursor equation.*) (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt [recursor_trans] 1, - simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1, - IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]); + simp_tac (put_simpset rank_ss ctxt |> Simplifier.add_simps case_eqns) 1, + IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt |> Simplifier.add_simps (tl con_defs)) 1)]); in thy2 |> Sign.add_path big_rec_base_name diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu Aug 07 21:40:03 2025 +0200 @@ -356,7 +356,7 @@ resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1, DETERM (eresolve_tac ctxt [raw_induct] 1), (*Push Part inside Collect*) - full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1, + full_simp_tac (min_ss |> Simplifier.add_simp @{thm Part_Collect}) 1, (*This CollectE and disjE separates out the introduction rules*) REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm disjE}])), (*Now break down the individual cases. No disjE here in case @@ -450,7 +450,7 @@ (*Simplification largely reduces the mutual induction rule to the standard rule*) val mut_ss = - min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; + min_ss |> Simplifier.add_simps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; val all_defs = con_defs @ part_rec_defs; @@ -473,13 +473,13 @@ using freeness of the Sum constructors; proves all but one conjunct by contradiction*) rewrite_goals_tac ctxt all_defs THEN - simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1 THEN + simp_tac (mut_ss |> Simplifier.add_simp @{thm Part_iff}) 1 THEN IF_UNSOLVED (*simp_tac may have finished it off!*) ((*simplify assumptions*) (*some risk of excessive simplification here -- might have to identify the bare minimum set of rewrites*) full_simp_tac - (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1 + (mut_ss |> Simplifier.add_simps (@{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps})) 1 THEN (*unpackage and use "prem" in the corresponding place*) REPEAT (resolve_tac ctxt @{thms impI} 1) THEN diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/UNITY/Constrains.thy Thu Aug 07 21:40:03 2025 +0200 @@ -480,7 +480,7 @@ (* Three subgoals *) rewrite_goal_tac ctxt [@{thm st_set_def}] 3, REPEAT (force_tac ctxt 2), - full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\program\)) 1, + full_simp_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\program\)) 1, ALLGOALS (clarify_tac ctxt), REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})), ALLGOALS (clarify_tac ctxt), diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Thu Aug 07 21:40:03 2025 +0200 @@ -354,11 +354,11 @@ REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co \ transient*) - simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\program\)) 2, + simp_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\program\)) 2, Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] [] @{thm transientI} 2, (*simplify the command's domain*) - simp_tac (ctxt addsimps [@{thm domain_def}]) 3, + simp_tac (ctxt |> Simplifier.add_simp @{thm domain_def}) 3, (* proving the domain part *) clarify_tac ctxt 3, dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4, @@ -367,7 +367,7 @@ REPEAT (resolve_tac ctxt @{thms state_update_type} 3), constrains_tac ctxt 1, ALLGOALS (clarify_tac ctxt), - ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])), + ALLGOALS (asm_full_simp_tac (ctxt |> Simplifier.add_simp @{thm st_set_def})), ALLGOALS (clarify_tac ctxt), ALLGOALS (asm_lr_simp_tac ctxt)]); \ diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/Univ.thy --- a/src/ZF/Univ.thy Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/Univ.thy Thu Aug 07 21:40:03 2025 +0200 @@ -790,8 +790,8 @@ ML \ val rank_ss = - simpset_of (\<^context> addsimps [@{thm VsetI}] - addsimps @{thms rank_rls} @ (@{thms rank_rls} RLN (2, [@{thm lt_trans}]))); + simpset_of (\<^context> |> Simplifier.add_simp @{thm VsetI} + |> Simplifier.add_simps (@{thms rank_rls} @ (@{thms rank_rls} RLN (2, [@{thm lt_trans}])))); \ end diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/arith_data.ML Thu Aug 07 21:40:03 2025 +0200 @@ -114,8 +114,8 @@ fun simplify_meta_eq rules ctxt = let val ctxt' = put_simpset FOL_ss ctxt - delsimps @{thms iff_simps} (*these could erase the whole rule!*) - addsimps rules + |> Simplifier.del_simps @{thms iff_simps} (*these could erase the whole rule!*) + |> Simplifier.add_simps rules |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] in mk_meta_eq o simplify ctxt' end; @@ -130,15 +130,15 @@ val find_first_coeff = find_first_coeff [] val norm_ss1 = - simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac}) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (add_0s @ add_succs @ mult_1s @ @{thms add_ac})) val norm_ss2 = - simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ @{thms add_ac} @ - @{thms mult_ac} @ tc_rules @ natifys) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (add_0s @ mult_1s @ @{thms add_ac} @ + @{thms mult_ac} @ tc_rules @ natifys)) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ tc_rules @ natifys) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (add_0s @ tc_rules @ natifys)) fun numeral_simp_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = simplify_meta_eq final_rules diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Thu Aug 07 20:33:28 2025 +0200 +++ b/src/ZF/int_arith.ML Thu Aug 07 21:40:03 2025 +0200 @@ -157,13 +157,13 @@ val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> - addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}) + |> Simplifier.add_simps (add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac})) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> - addsimps bin_simps @ int_mult_minus_simps @ intifys) + |> Simplifier.add_simps (bin_simps @ int_mult_minus_simps @ intifys)) val norm_ss3 = simpset_of (put_simpset ZF_ss \<^context> - addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys) + |> Simplifier.add_simps (int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) @@ -171,7 +171,7 @@ val numeral_simp_ss = simpset_of (put_simpset ZF_ss \<^context> - addsimps add_0s @ bin_simps @ tc_rules @ intifys) + |> Simplifier.add_simps (add_0s @ bin_simps @ tc_rules @ intifys)) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) THEN ALLGOALS (asm_simp_tac ctxt) @@ -229,20 +229,20 @@ val norm_ss1 = simpset_of (put_simpset ZF_ss \<^context> - addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys) + |> Simplifier.add_simps (add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys)) val norm_ss2 = simpset_of (put_simpset ZF_ss \<^context> - addsimps bin_simps @ int_mult_minus_simps @ intifys) + |> Simplifier.add_simps (bin_simps @ int_mult_minus_simps @ intifys)) val norm_ss3 = simpset_of (put_simpset ZF_ss \<^context> - addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys) + |> Simplifier.add_simps (int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (add_0s @ bin_simps @ tc_rules @ intifys)) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) @@ -275,16 +275,16 @@ fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans} val norm_ss1 = - simpset_of (put_simpset ZF_ss \<^context> addsimps mult_1s @ diff_simps @ zminus_simps) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (mult_1s @ diff_simps @ zminus_simps)) val norm_ss2 = - simpset_of (put_simpset ZF_ss \<^context> addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ - bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps ([@{thm zmult_zminus_right} RS @{thm sym}] @ + bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)) fun norm_tac ctxt = ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ tc_rules @ intifys) + simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (bin_simps @ tc_rules @ intifys)) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);