--- a/src/HOL/Decision_Procs/langford.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Sat Oct 21 11:24:34 2023 +0200
@@ -127,7 +127,7 @@
local
-fun proc ctxt ct =
+fun reduce_ex_proc ctxt ct =
(case Thm.term_of ct of
\<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
let
@@ -168,9 +168,7 @@
in
-val reduce_ex_simproc =
- Simplifier.make_simproc \<^context> "reduce_ex_simproc"
- {lhss = [\<^term>\<open>\<exists>x. P x\<close>], proc = K proc};
+val reduce_ex_simproc = \<^simproc_setup>\<open>passive reduce_ex ("\<exists>x. P x") = \<open>K reduce_ex_proc\<close>\<close>;
end;
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Oct 21 11:24:34 2023 +0200
@@ -148,9 +148,9 @@
map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
val regularize_simproc =
- Simplifier.make_simproc \<^context> "regularize"
- {lhss = [\<^term>\<open>Ball (Respects (R1 ===> R2)) P\<close>, \<^term>\<open>Bex (Respects (R1 ===> R2)) P\<close>],
- proc = K ball_bex_range_simproc};
+ \<^simproc_setup>\<open>passive regularize
+ ("Ball (Respects (R1 ===> R2)) P" | "Bex (Respects (R1 ===> R2)) P") =
+ \<open>K ball_bex_range_simproc\<close>\<close>
fun regularize_tac ctxt =
let
--- a/src/HOL/Tools/SMT/smt_real.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Sat Oct 21 11:24:34 2023 +0200
@@ -116,10 +116,9 @@
(* Z3 proof replay *)
-val real_linarith_proc =
- Simplifier.make_simproc \<^context> "fast_real_arith"
- {lhss = [\<^term>\<open>(m::real) < n\<close>, \<^term>\<open>(m::real) \<le> n\<close>, \<^term>\<open>(m::real) = n\<close>],
- proc = K Lin_Arith.simproc}
+val real_linarith_simproc =
+ \<^simproc_setup>\<open>passive fast_real_arith ("(m::real) < n" | "(m::real) \<le> n" | "(m::real) = n") =
+ \<open>K Lin_Arith.simproc\<close>\<close>;
(* setup *)
@@ -128,6 +127,6 @@
SMTLIB_Interface.add_logic (10, smtlib_logic) #>
setup_builtins #>
Z3_Interface.add_mk_builtins smt_mk_builtins #>
- SMT_Replay.add_simproc real_linarith_proc))
+ SMT_Replay.add_simproc real_linarith_simproc))
end;
--- a/src/HOL/Tools/SMT/smt_replay.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML Sat Oct 21 11:24:34 2023 +0200
@@ -140,20 +140,22 @@
end
handle THM _ => NONE
+ val fast_int_arith_simproc =
+ \<^simproc_setup>\<open>passive fast_int_arith ("(m::int) < n" | "(m::int) \<le> n" | "(m::int) = n") =
+ \<open>K Lin_Arith.simproc\<close>\<close>
+
+ val antisym_le_simproc =
+ \<^simproc_setup>\<open>passive antisym_le ("(x::'a::order) \<le> y") = \<open>K prove_antisym_le\<close>\<close>
+
+ val antisym_less_simproc =
+ \<^simproc_setup>\<open>passive antisym_less ("\<not> (x::'a::linorder) < y") = \<open>K prove_antisym_less\<close>\<close>
+
val basic_simpset =
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>,
- Simplifier.make_simproc \<^context> "fast_int_arith"
- {lhss = [\<^term>\<open>(m::int) < n\<close>, \<^term>\<open>(m::int) \<le> n\<close>, \<^term>\<open>(m::int) = n\<close>],
- proc = K Lin_Arith.simproc},
- Simplifier.make_simproc \<^context> "antisym_le"
- {lhss = [\<^term>\<open>(x::'a::order) \<le> y\<close>],
- proc = K prove_antisym_le},
- Simplifier.make_simproc \<^context> "antisym_less"
- {lhss = [\<^term>\<open>\<not> (x::'a::linorder) < y\<close>],
- proc = K prove_antisym_less}])
+ addsimprocs [\<^simproc>\<open>numeral_divmod\<close>, fast_int_arith_simproc,
+ antisym_le_simproc, antisym_less_simproc])
structure Simpset = Generic_Data
(
--- a/src/HOL/Tools/int_arith.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/int_arith.ML Sat Oct 21 11:24:34 2023 +0200
@@ -23,24 +23,22 @@
val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});
val zero_to_of_int_zero_simproc =
- Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
- {lhss = [\<^term>\<open>0::'a::ring\<close>],
- proc = fn _ => fn _ => fn ct =>
+ \<^simproc_setup>\<open>passive zero_to_of_int_zero ("0::'a::ring") =
+ \<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
else SOME (Thm.instantiate' [SOME T] [] zeroth)
- end};
+ end\<close>\<close>;
val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
val one_to_of_int_one_simproc =
- Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
- {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
- proc = fn _ => fn _ => fn ct =>
+ \<^simproc_setup>\<open>passive one_to_of_int_one ("1::'a::ring_1") =
+ \<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
else SOME (Thm.instantiate' [SOME T] [] oneth)
- end};
+ end\<close>\<close>;
fun check (Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>int\<close>)) = false
| check (Const (\<^const_name>\<open>Groups.one\<close>, _)) = true
@@ -63,14 +61,11 @@
|> simpset_of;
val zero_one_idom_simproc =
- Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
- {lhss =
- [\<^term>\<open>(x::'a::ring_char_0) = y\<close>,
- \<^term>\<open>(x::'a::linordered_idom) < y\<close>,
- \<^term>\<open>(x::'a::linordered_idom) \<le> y\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive zero_one_idom
+ ("(x::'a::ring_char_0) = y" | "(u::'b::linordered_idom) < v" | "(u::'b::linordered_idom) \<le> v") =
+ \<open>fn _ => fn ctxt => fn ct =>
if check (Thm.term_of ct)
then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
- else NONE};
+ else NONE\<close>\<close>
end;
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Oct 21 11:24:34 2023 +0200
@@ -437,23 +437,21 @@
val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc
val field_divide_cancel_numeral_factor =
- Simplifier.make_simproc \<^context> "field_divide_cancel_numeral_factor"
- {lhss =
- [\<^term>\<open>((l::'a::field) * m) / n\<close>,
- \<^term>\<open>(l::'a::field) / (m * n)\<close>,
- \<^term>\<open>((numeral v)::'a::field) / (numeral w)\<close>,
- \<^term>\<open>((numeral v)::'a::field) / (- numeral w)\<close>,
- \<^term>\<open>((- numeral v)::'a::field) / (numeral w)\<close>,
- \<^term>\<open>((- numeral v)::'a::field) / (- numeral w)\<close>],
- proc = K DivideCancelNumeralFactor.proc}
+ \<^simproc_setup>\<open>passive field_divide_cancel_numeral_factor
+ ("((l::'a::field) * m) / n" | "(l::'a::field) / (m * n)" |
+ "((numeral v)::'a::field) / (numeral w)" |
+ "((numeral v)::'a::field) / (- numeral w)" |
+ "((- numeral v)::'a::field) / (numeral w)" |
+ "((- numeral v)::'a::field) / (- numeral w)") =
+ \<open>K DivideCancelNumeralFactor.proc\<close>\<close>;
+
+val field_eq_cancel_numeral_factor =
+ \<^simproc_setup>\<open>passive field_eq_cancel_numeral_factor
+ ("(l::'a::field) * m = n" | "(l::'a::field) = m * n") =
+ \<open>K EqCancelNumeralFactor.proc\<close>\<close>;
val field_cancel_numeral_factors =
- [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor"
- {lhss =
- [\<^term>\<open>(l::'a::field) * m = n\<close>,
- \<^term>\<open>(l::'a::field) = m * n\<close>],
- proc = K EqCancelNumeralFactor.proc},
- field_divide_cancel_numeral_factor]
+ [field_divide_cancel_numeral_factor, field_eq_cancel_numeral_factor]
(** Declarations for ExtractCommonTerm **)
@@ -599,7 +597,7 @@
(Thm.apply (Thm.apply eq t) z)))
in Thm.equal_elim (Thm.symmetric th) TrueI end
-fun proc ctxt ct =
+fun add_frac_frac_proc ctxt ct =
let
val ((x,y),(w,z)) =
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
@@ -610,7 +608,7 @@
in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
-fun proc2 ctxt ct =
+fun add_frac_num_proc ctxt ct =
let
val (l,r) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm l
@@ -636,7 +634,7 @@
val is_number = is_number o Thm.term_of
-fun proc3 ctxt ct =
+fun ord_frac_proc ct =
(case Thm.term_of ct of
Const(\<^const_name>\<open>Orderings.less\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ =>
let
@@ -683,25 +681,22 @@
| _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
val add_frac_frac_simproc =
- Simplifier.make_simproc \<^context> "add_frac_frac_simproc"
- {lhss = [\<^term>\<open>(x::'a::field) / y + (w::'a::field) / z\<close>],
- proc = K proc}
+ \<^simproc_setup>\<open>passive add_frac_frac ("(x::'a::field) / y + (w::'a::field) / z") =
+ \<open>K add_frac_frac_proc\<close>\<close>
val add_frac_num_simproc =
- Simplifier.make_simproc \<^context> "add_frac_num_simproc"
- {lhss = [\<^term>\<open>(x::'a::field) / y + z\<close>, \<^term>\<open>z + (x::'a::field) / y\<close>],
- proc = K proc2}
+ \<^simproc_setup>\<open>passive add_frac_num ("(x::'a::field) / y + z" | "z + (x::'a::field) / y") =
+ \<open>K add_frac_num_proc\<close>\<close>
val ord_frac_simproc =
- Simplifier.make_simproc \<^context> "ord_frac_simproc"
- {lhss =
- [\<^term>\<open>(a::'a::{field,ord}) / b < c\<close>,
- \<^term>\<open>(a::'a::{field,ord}) / b \<le> c\<close>,
- \<^term>\<open>c < (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>c \<le> (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>c = (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>(a::'a::{field, ord}) / b = c\<close>],
- proc = K proc3}
+ \<^simproc_setup>\<open>passive ord_frac
+ ("(a::'a::{field,ord}) / b < c" |
+ "(a::'a::{field,ord}) / b \<le> c" |
+ "c < (a::'a::{field,ord}) / b" |
+ "c \<le> (a::'a::{field,ord}) / b" |
+ "c = (a::'a::{field,ord}) / b" |
+ "(a::'a::{field, ord}) / b = c") =
+ \<open>K (K ord_frac_proc)\<close>\<close>
val field_comp_ss =
simpset_of
--- a/src/Tools/induct.ML Sat Oct 21 00:25:40 2023 +0200
+++ b/src/Tools/induct.ML Sat Oct 21 11:24:34 2023 +0200
@@ -171,9 +171,7 @@
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
val rearrange_eqs_simproc =
- Simplifier.make_simproc \<^context> "rearrange_eqs"
- {lhss = [\<^term>\<open>Pure.all (t :: 'a::{} \<Rightarrow> prop)\<close>],
- proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
+ \<^simproc_setup>\<open>passive rearrange_eqs ("Pure.all (t :: 'a::{} \<Rightarrow> prop)") = \<open>K mk_swap_rrule\<close>\<close>;
(* rotate k premises to the left by j, skipping over first j premises *)