# HG changeset patch # User wenzelm # Date 1754944206 -7200 # Node ID 2f6ce3ce27be45945197d65feb8af5b38e3c49ac # Parent 3602e2da6da1454365adcefee322c3065d418892 avoid legacy operations; diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/approximation.ML --- 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>\approximation_preproc\)) + (put_simpset HOL_basic_ss ctxt + |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\approximation_preproc\)) fun reify_form_conv ctxt ct = let diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/approximation_generator.ML --- 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 = diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/cooper_tac.ML --- 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>\cancel_div_mod_nat\ |> Simplifier.add_proc \<^simproc>\cancel_div_mod_int\ 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 *) diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/ferrack_tac.ML --- 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 diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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); diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/langford.ML --- 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 => diff -r 3602e2da6da1 -r 2f6ce3ce27be src/HOL/Decision_Procs/mir_tac.ML --- 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>\cancel_div_mod_nat\ |> Simplifier.add_proc \<^simproc>\cancel_div_mod_int\ 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)