--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 11 22:30:06 2025 +0200
@@ -534,7 +534,7 @@
| _ => Ferrante_Rackoff_Data.Nox
in h end
fun ss phi ctxt =
- simpset_of (put_simpset HOL_ss ctxt addsimps (simps phi))
+ simpset_of (put_simpset HOL_ss ctxt |> Simplifier.add_simps (simps phi))
in
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"}
{isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
@@ -869,7 +869,7 @@
in h end;
fun class_field_ss phi ctxt =
simpset_of (put_simpset HOL_basic_ss ctxt
- addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
+ |> Simplifier.add_simps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
|> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}])
in
--- a/src/HOL/Decision_Procs/approximation.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Mon Aug 11 22:30:06 2025 +0200
@@ -187,8 +187,8 @@
fun preproc_form_conv ctxt =
Simplifier.rewrite
- (put_simpset HOL_basic_ss ctxt addsimps
- (Named_Theorems.get ctxt \<^named_theorems>\<open>approximation_preproc\<close>))
+ (put_simpset HOL_basic_ss ctxt
+ |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>approximation_preproc\<close>))
fun reify_form_conv ctxt ct =
let
--- a/src/HOL/Decision_Procs/approximation_generator.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Mon Aug 11 22:30:06 2025 +0200
@@ -120,7 +120,9 @@
by auto
}
-fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
+fun rewrite_with ctxt thms =
+ Simplifier.rewrite (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps thms)
+
fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
fun approx_random ctxt prec eps frees e xs genuine_only size seed =
--- a/src/HOL/Decision_Procs/cooper_tac.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Mon Aug 11 22:30:06 2025 +0200
@@ -45,31 +45,31 @@
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms refl mod_add_eq mod_add_left_eq
+ |> Simplifier.add_simps @{thms refl mod_add_eq mod_add_left_eq
mod_add_right_eq
div_add1_eq [symmetric] div_add1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0
div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
Suc_eq_plus1}
- addsimps @{thms ac_simps}
+ |> Simplifier.add_simps @{thms ac_simps}
|> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
|> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
+ |> Simplifier.add_simps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
|> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
(* Simp rules for changing (n::int) to int n *)
val simpset1 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
- map (fn r => r RS sym) @{thms of_nat_numeral [where ?'a = int] int_int_eq zle_int of_nat_less_iff [where ?'a = int]}
+ |> Simplifier.add_simps (@{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
+ map (fn r => r RS sym) @{thms of_nat_numeral [where ?'a = int] int_int_eq zle_int of_nat_less_iff [where ?'a = int]})
|> Splitter.add_split @{thm zdiff_int_split}
(*simp rules for elimination of int n*)
val simpset2 =
put_simpset HOL_basic_ss ctxt
- addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *),
+ |> Simplifier.add_simps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *),
@{thm of_nat_0 [where ?'a = int]}, @{thm of_nat_1 [where ?'a = int]}]
|> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong}
(* simp rules for elimination of abs *)
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Mon Aug 11 22:30:06 2025 +0200
@@ -10,10 +10,10 @@
structure Ferrack_Tac: FERRACK_TAC =
struct
-val ferrack_ss = let val ths = [@{thm of_int_eq_iff}, @{thm of_int_less_iff},
- @{thm of_int_le_iff}]
- in \<^context> delsimps ths addsimps (map (fn th => th RS sym) ths)
- end |> simpset_of;
+val ferrack_ss =
+ let val ths = [@{thm of_int_eq_iff}, @{thm of_int_less_iff}, @{thm of_int_le_iff}]
+ in \<^context> |> Simplifier.del_simps ths |> Simplifier.add_simps (map (fn th => th RS sym) ths)
+ end |> simpset_of;
val binarith = @{thms arith_simps}
val comp_arith = binarith @ @{thms simp_thms}
@@ -53,7 +53,7 @@
(* Transform the term*)
val (t,np,nh) = prepare_for_linr q g
(* Some simpsets for dealing with mod div abs and nat*)
- val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
+ val simpset0 = put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps comp_arith
val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 11 22:30:06 2025 +0200
@@ -164,7 +164,8 @@
(mk_meta_eq qe)))
[fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
val bex_conv =
- Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})
+ Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms simp_thms bex_simps(1-5)})
val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
in result_th
end
@@ -199,7 +200,7 @@
let
val ss' =
merge_ss (simpset_of
- (put_simpset HOL_basic_ss ctxt addsimps
+ (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps
@{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss);
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
--- a/src/HOL/Decision_Procs/langford.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Mon Aug 11 22:30:06 2025 +0200
@@ -30,7 +30,8 @@
fun simp_rule ctxt =
Conv.fconv_rule
(Conv.arg_conv
- (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
+ (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
+ |> Simplifier.add_simps @{thms ball_simps simp_thms})));
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
(case Thm.term_of ep of
@@ -38,7 +39,7 @@
let
val p = Thm.dest_arg ep
val ths =
- simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
+ simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps gather)
(Thm.instantiate' [] [SOME p] stupid)
val (L, U) =
let val (_, q) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of ths))
@@ -151,7 +152,7 @@
|> Conv.fconv_rule
(Conv.arg_conv
(Simplifier.rewrite
- (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms simp_thms ex_simps})))
|> SOME
end
| _ =>
@@ -161,7 +162,7 @@
|> Conv.fconv_rule
(Conv.arg_conv
(Simplifier.rewrite
- (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms simp_thms ex_simps})))
|> SOME)
end
| _ => NONE);
@@ -176,12 +177,13 @@
let
val ctxt' =
Context_Position.set_visible false (put_simpset dlo_ss ctxt)
- addsimps @{thms dnf_simps} |> Simplifier.add_proc reduce_ex_simproc
+ |> Simplifier.add_simps @{thms dnf_simps}
+ |> Simplifier.add_proc reduce_ex_simproc
val dnfex_conv = Simplifier.rewrite ctxt'
val pcv =
Simplifier.rewrite
(put_simpset dlo_ss ctxt
- 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})
val mk_env = Cterms.list_set_rev o Cterms.build o Drule.add_frees_cterm
in
fn p =>
--- a/src/HOL/Decision_Procs/mir_tac.ML Mon Aug 11 21:55:09 2025 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Mon Aug 11 22:30:06 2025 +0200
@@ -11,8 +11,9 @@
struct
val mir_ss =
- simpset_of (\<^context> delsimps [@{thm "of_int_eq_iff"}, @{thm "of_int_less_iff"}, @{thm "of_int_le_iff"}]
- addsimps @{thms "iff_real_of_int"});
+ simpset_of (\<^context>
+ |> Simplifier.del_simps [@{thm "of_int_eq_iff"}, @{thm "of_int_less_iff"}, @{thm "of_int_le_iff"}]
+ |> Simplifier.add_simps @{thms "iff_real_of_int"});
val nT = HOLogic.natT;
val nat_arith = [@{thm diff_nat_numeral}];
@@ -61,7 +62,8 @@
fun mir_tac ctxt q =
Object_Logic.atomize_prems_tac ctxt
THEN' simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
+ |> Simplifier.add_simps [@{thm "abs_ge_zero"}]
+ |> Simplifier.add_simps @{thms simp_thms})
THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
THEN' SUBGOAL (fn (g, i) =>
let
@@ -70,30 +72,31 @@
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset =
put_simpset HOL_basic_ss ctxt
- addsimps [refl, @{thm mod_add_eq},
+ |> Simplifier.add_simps [refl, @{thm mod_add_eq},
@{thm mod_self},
@{thm div_0}, @{thm mod_0},
@{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
@{thm "Suc_eq_plus1"}]
- addsimps @{thms add.assoc add.commute add.left_commute}
+ |> Simplifier.add_simps @{thms add.assoc add.commute add.left_commute}
|> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
|> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 = put_simpset HOL_basic_ss ctxt
- addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
- addsimps comp_ths
+ |> Simplifier.add_simps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
+ |> Simplifier.add_simps comp_ths
|> fold Splitter.add_split
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = put_simpset HOL_basic_ss ctxt
- addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
- map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
+ |> Simplifier.add_simps (@{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
+ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}])
|> Splitter.add_split @{thm "zdiff_int_split"}
(*simp rules for elimination of int n*)
val simpset2 = put_simpset HOL_basic_ss ctxt
- addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral},
- @{thm "of_nat_0"}, @{thm "of_nat_1"}]
+ |> Simplifier.add_simps
+ [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm zero_le_numeral},
+ @{thm "of_nat_0"}, @{thm "of_nat_1"}]
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
(* simp rules for elimination of abs *)
val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)