--- 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;
\<close>
@@ -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
--- 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>\<open>defined_All\<close>
|> Simplifier.add_proc \<^simproc>\<open>defined_Ex\<close>
|> 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;
\<close>
--- 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 \<open>
-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);
\<close>
--- 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 ***)
--- 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 =
--- 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
--- 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 \<open>
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>\<open>MACHIN_TAG\<close>, _) $ _ $
@@ -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
\<close>
--- 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>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y and s = fset_ct in
lemma \<open>finite s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> dist x y \<equiv> SUP a\<in>s. \<bar>dist x a - dist a y\<bar>\<close>
@@ -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>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y and s = fset_ct in
lemma \<open>x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<equiv> \<forall>a\<in>s. dist x a = dist y a\<close>
--- 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
--- 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
\<close>
--- 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 =
--- 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
\<close>
--- 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}]))])))\<close>
--- 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}]))])))\<close>
--- 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
\<close>
--- 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 \<open>
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"]
\<close>
--- 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 \<open>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})\<close>
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
--- 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
--- 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;
--- 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>\<open>cancelation_simproc_pre\<close>
+ |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close>)
|> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (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>\<open>cancelation_simproc_post\<close>
+ |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close>)
|> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.rhs_of thm)
in @{thm Pure.transitive} OF [thm, post_simplified_ct] end
in
--- 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));
--- 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
--- 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
--- 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)
--- 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,
--- 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
--- 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;
--- 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
--- 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>\<open>unit_eq\<close>);
in
fun split_all_tac ctxt = SUBGOAL (fn (t, i) =>
@@ -538,7 +538,7 @@
ML \<open>
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>\<open>Pair\<close>, _) $ 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;
\<close>
@@ -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>\<open>Pure.eq \<^Type>\<open>set A\<close> for S S'\<close>
(K (EVERY
--- 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 []
\<close>
--- 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')
--- 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>\<open>Main\<close>))
- |> 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>\<open>Main\<close>))
+ |> 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'
--- 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
--- 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>\<open>:\<close>;
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]};
--- 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
--- 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
--- 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
--- 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) =
--- 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>\<open>termination_simp\<close>)))
+ (auto_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>termination_simp\<close>)))
val _ =
Theory.setup
--- 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
--- 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 *)
--- 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))
--- 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>\<open>termination_simp\<close>
- 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
--- 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 =
--- 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>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>, \<^simproc>\<open>neq\<close>, \<^simproc>\<open>let_simp\<close>])
--- 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>\<open>\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)\<close>
--- 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),
--- 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''''
--- 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])
--- 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>\<open>code_pred_inline\<close>
- 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))
--- 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 =
--- 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)
--- 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>\<open>True\<close>;
val false_tm = \<^cterm>\<open>False\<close>;
-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>\<open>cancel_div_mod_int\<close>)
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>\<open>arith\<close>))
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
--- 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)
--- 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
--- 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
--- 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 = [],
--- 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 =
--- 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 =
--- 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))
--- 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>\<open>numeral_divmod\<close>, 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 \<equiv> \<not> False" by simp}
val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule]
--- 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 =
--- 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)))
--- 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 = [],
--- 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
--- 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;
--- 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;
--- 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
--- 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>\<open>algebra\<close>)
- delsimps del_thms addsimps add_thms);
+ |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>algebra\<close>)
+ |> Simplifier.del_simps del_thms
+ |> Simplifier.add_simps add_thms);
fun ring_tac add_ths del_ths ctxt =
Object_Logic.full_atomize_tac ctxt
--- 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
--- 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>\<open>Collect_mem\<close>) 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>\<open>Collect_mem\<close>) |>
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)]),
--- 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>\<open>linarith_trace\<close> (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)
--- 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
--- 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>\<open>Not\<close>
(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
--- 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 "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> 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'),
--- 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}
--- 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>\<open>(/)\<close>);
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;
--- 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
--- 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;
--- 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;
--- 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)
--- 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
--- 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
--- 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>\<open>program\<close>)) 1,
+ full_simp_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 1,
ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
ALLGOALS (clarify_tac ctxt),
--- 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 \<and> transient*)
- simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 2,
+ simp_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 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)]);
\<close>
--- 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
\<open>
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}]))));
\<close>
end
--- 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
--- 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);