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