--- a/src/HOL/Analysis/measurable.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML Thu Oct 19 17:06:39 2023 +0200
@@ -22,7 +22,7 @@
val measurable_tac : Proof.context -> thm list -> tactic
- val simproc : Proof.context -> cterm -> thm option
+ val simproc : Simplifier.proc
val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
val del_preprocessor : string -> Context.generic -> Context.generic
--- a/src/HOL/HOL.thy Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/HOL.thy Thu Oct 19 17:06:39 2023 +0200
@@ -1648,7 +1648,7 @@
signature REORIENT_PROC =
sig
val add : (term -> bool) -> theory -> theory
- val proc : Proof.context -> cterm -> thm option
+ val proc : Simplifier.proc
end;
structure Reorient_Proc : REORIENT_PROC =
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Thu Oct 19 17:06:39 2023 +0200
@@ -8,7 +8,7 @@
val cont_thms: term -> thm list
val all_cont_thms: term -> thm list
val cont_tac: Proof.context -> int -> tactic
- val cont_proc: Proof.context -> cterm -> thm option
+ val cont_proc: Simplifier.proc
end
structure ContProc : CONT_PROC =
--- a/src/HOL/Library/Cancellation/cancel.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML Thu Oct 19 17:06:39 2023 +0200
@@ -35,7 +35,7 @@
signature CANCEL =
sig
- val proc: Proof.context -> cterm -> thm option
+ val proc: Simplifier.proc
end;
functor Cancel_Fun(Data: CANCEL_NUMERALS_DATA): CANCEL =
--- a/src/HOL/Library/Cancellation/cancel_simprocs.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
@@ -7,10 +7,10 @@
signature CANCEL_SIMPROCS =
sig
- val eq_cancel: Proof.context -> cterm -> thm option
- val less_cancel: Proof.context -> cterm -> thm option
- val less_eq_cancel: Proof.context -> cterm -> thm option
- val diff_cancel: Proof.context -> cterm -> thm option
+ val eq_cancel: Simplifier.proc
+ val less_cancel: Simplifier.proc
+ val less_eq_cancel: Simplifier.proc
+ val diff_cancel: Simplifier.proc
end;
structure Cancel_Simprocs : CANCEL_SIMPROCS =
--- a/src/HOL/Library/multiset_simprocs.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Library/multiset_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
@@ -7,8 +7,8 @@
signature MULTISET_SIMPROCS =
sig
- val subset_cancel_msets: Proof.context -> cterm -> thm option
- val subseteq_cancel_msets: Proof.context -> cterm -> thm option
+ val subset_cancel_msets: Simplifier.proc
+ val subseteq_cancel_msets: Simplifier.proc
end;
structure Multiset_Simprocs : MULTISET_SIMPROCS =
--- a/src/HOL/List.thy Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/List.thy Thu Oct 19 17:06:39 2023 +0200
@@ -557,7 +557,7 @@
signature LIST_TO_SET_COMPREHENSION =
sig
- val simproc : Proof.context -> cterm -> thm option
+ val simproc : Simplifier.proc
end
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML Thu Oct 19 17:06:39 2023 +0200
@@ -6,7 +6,7 @@
signature Z3_REPLAY_RULES =
sig
- val apply: Proof.context -> cterm -> thm option
+ val apply: Simplifier.proc
end;
structure Z3_Replay_Rules: Z3_REPLAY_RULES =
--- a/src/HOL/Tools/datatype_simprocs.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
@@ -6,7 +6,7 @@
*)
signature DATATYPE_SIMPROCS = sig
- val no_proper_subterm_simproc : Proof.context -> cterm -> thm option
+ val no_proper_subterm_simproc : Simplifier.proc
end
structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct
--- a/src/HOL/Tools/lin_arith.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Oct 19 17:06:39 2023 +0200
@@ -9,7 +9,7 @@
val pre_tac: Proof.context -> int -> tactic
val simple_tac: Proof.context -> int -> tactic
val tac: Proof.context -> int -> tactic
- val simproc: Proof.context -> cterm -> thm option
+ val simproc: Simplifier.proc
val add_inj_thms: thm list -> Context.generic -> Context.generic
val add_lessD: thm -> Context.generic -> Context.generic
val add_simps: thm list -> Context.generic -> Context.generic
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
@@ -5,21 +5,21 @@
signature NAT_NUMERAL_SIMPROCS =
sig
- val combine_numerals: Proof.context -> cterm -> thm option
- val eq_cancel_numerals: Proof.context -> cterm -> thm option
- val less_cancel_numerals: Proof.context -> cterm -> thm option
- val le_cancel_numerals: Proof.context -> cterm -> thm option
- val diff_cancel_numerals: Proof.context -> cterm -> thm option
- val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val dvd_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val eq_cancel_factor: Proof.context -> cterm -> thm option
- val less_cancel_factor: Proof.context -> cterm -> thm option
- val le_cancel_factor: Proof.context -> cterm -> thm option
- val div_cancel_factor: Proof.context -> cterm -> thm option
- val dvd_cancel_factor: Proof.context -> cterm -> thm option
+ val combine_numerals: Simplifier.proc
+ val eq_cancel_numerals: Simplifier.proc
+ val less_cancel_numerals: Simplifier.proc
+ val le_cancel_numerals: Simplifier.proc
+ val diff_cancel_numerals: Simplifier.proc
+ val eq_cancel_numeral_factor: Simplifier.proc
+ val less_cancel_numeral_factor: Simplifier.proc
+ val le_cancel_numeral_factor: Simplifier.proc
+ val div_cancel_numeral_factor: Simplifier.proc
+ val dvd_cancel_numeral_factor: Simplifier.proc
+ val eq_cancel_factor: Simplifier.proc
+ val less_cancel_factor: Simplifier.proc
+ val le_cancel_factor: Simplifier.proc
+ val div_cancel_factor: Simplifier.proc
+ val dvd_cancel_factor: Simplifier.proc
end;
structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
@@ -17,24 +17,24 @@
signature NUMERAL_SIMPROCS =
sig
val trans_tac: Proof.context -> thm option -> tactic
- val assoc_fold: Proof.context -> cterm -> thm option
- val combine_numerals: Proof.context -> cterm -> thm option
- val eq_cancel_numerals: Proof.context -> cterm -> thm option
- val less_cancel_numerals: Proof.context -> cterm -> thm option
- val le_cancel_numerals: Proof.context -> cterm -> thm option
- val eq_cancel_factor: Proof.context -> cterm -> thm option
- val le_cancel_factor: Proof.context -> cterm -> thm option
- val less_cancel_factor: Proof.context -> cterm -> thm option
- val div_cancel_factor: Proof.context -> cterm -> thm option
- val mod_cancel_factor: Proof.context -> cterm -> thm option
- val dvd_cancel_factor: Proof.context -> cterm -> thm option
- val divide_cancel_factor: Proof.context -> cterm -> thm option
- val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
- val field_combine_numerals: Proof.context -> cterm -> thm option
+ val assoc_fold: Simplifier.proc
+ val combine_numerals: Simplifier.proc
+ val eq_cancel_numerals: Simplifier.proc
+ val less_cancel_numerals: Simplifier.proc
+ val le_cancel_numerals: Simplifier.proc
+ val eq_cancel_factor: Simplifier.proc
+ val le_cancel_factor: Simplifier.proc
+ val less_cancel_factor: Simplifier.proc
+ val div_cancel_factor: Simplifier.proc
+ val mod_cancel_factor: Simplifier.proc
+ val dvd_cancel_factor: Simplifier.proc
+ val divide_cancel_factor: Simplifier.proc
+ val eq_cancel_numeral_factor: Simplifier.proc
+ val less_cancel_numeral_factor: Simplifier.proc
+ val le_cancel_numeral_factor: Simplifier.proc
+ val div_cancel_numeral_factor: Simplifier.proc
+ val divide_cancel_numeral_factor: Simplifier.proc
+ val field_combine_numerals: Simplifier.proc
val field_divide_cancel_numeral_factor: simproc
val num_ss: simpset
val field_comp_conv: Proof.context -> conv
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 19 17:06:39 2023 +0200
@@ -7,9 +7,9 @@
signature SET_COMPREHENSION_POINTFREE =
sig
- val base_simproc : Proof.context -> cterm -> thm option
- val code_simproc : Proof.context -> cterm -> thm option
- val simproc : Proof.context -> cterm -> thm option
+ val base_simproc : Simplifier.proc
+ val code_simproc : Simplifier.proc
+ val simproc : Simplifier.proc
end
structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
--- a/src/HOL/Transcendental.thy Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/Transcendental.thy Thu Oct 19 17:06:39 2023 +0200
@@ -7352,9 +7352,9 @@
val sqrt' : int option -> int -> int option
val nth_root : int option -> int -> int -> int option
val nth_root' : int option -> int -> int -> int option
-val sqrt_simproc : Proof.context -> cterm -> thm option
-val root_simproc : int * int -> Proof.context -> cterm -> thm option
-val powr_simproc : int * int -> Proof.context -> cterm -> thm option
+val sqrt_simproc : Simplifier.proc
+val root_simproc : int * int -> Simplifier.proc
+val powr_simproc : int * int -> Simplifier.proc
end
--- a/src/Provers/Arith/cancel_div_mod.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Thu Oct 19 17:06:39 2023 +0200
@@ -27,7 +27,7 @@
signature CANCEL_DIV_MOD =
sig
- val proc: Proof.context -> cterm -> thm option
+ val proc: Simplifier.proc
end;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Thu Oct 19 17:06:39 2023 +0200
@@ -37,7 +37,7 @@
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
- sig val proc: Proof.context -> cterm -> thm option end =
+ sig val proc: Simplifier.proc end =
struct
(*the simplification procedure*)
--- a/src/Provers/Arith/cancel_numerals.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Thu Oct 19 17:06:39 2023 +0200
@@ -44,7 +44,7 @@
signature CANCEL_NUMERALS =
sig
- val proc: Proof.context -> cterm -> thm option
+ val proc: Simplifier.proc
end;
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
--- a/src/Provers/Arith/combine_numerals.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Oct 19 17:06:39 2023 +0200
@@ -38,7 +38,7 @@
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
- val proc: Proof.context -> cterm -> thm option
+ val proc: Simplifier.proc
end
=
struct
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Oct 19 17:06:39 2023 +0200
@@ -93,7 +93,7 @@
sig
val prems_lin_arith_tac: Proof.context -> int -> tactic
val lin_arith_tac: Proof.context -> int -> tactic
- val lin_arith_simproc: Proof.context -> cterm -> thm option
+ val lin_arith_simproc: Simplifier.proc
val map_data:
({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: simpset,
--- a/src/Provers/quantifier1.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Provers/quantifier1.ML Thu Oct 19 17:06:39 2023 +0200
@@ -65,12 +65,12 @@
signature QUANTIFIER1 =
sig
- val rearrange_all: Proof.context -> cterm -> thm option
- val rearrange_All: Proof.context -> cterm -> thm option
- val rearrange_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
- val rearrange_Ex: Proof.context -> cterm -> thm option
- val rearrange_Bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
- val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+ val rearrange_all: Simplifier.proc
+ val rearrange_All: Simplifier.proc
+ val rearrange_Ball: (Proof.context -> tactic) -> Simplifier.proc
+ val rearrange_Ex: Simplifier.proc
+ val rearrange_Bex: (Proof.context -> tactic) -> Simplifier.proc
+ val rearrange_Collect: (Proof.context -> tactic) -> Simplifier.proc
end;
functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
--- a/src/Pure/raw_simplifier.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Oct 19 17:06:39 2023 +0200
@@ -19,7 +19,8 @@
type rrule
val mk_rrules: Proof.context -> thm list -> rrule list
val eq_rrule: rrule * rrule -> bool
- type proc
+ type proc = Proof.context -> cterm -> thm option
+ type simproc0
type solver
val mk_solver: string -> (Proof.context -> int -> tactic) -> solver
type simpset
@@ -36,8 +37,7 @@
val dest_simps: simpset -> thm list
type simproc
val eq_simproc: simproc * simproc -> bool
- val cert_simproc: theory -> string ->
- {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
+ val cert_simproc: theory -> string -> {lhss: term list, proc: proc Morphism.entity} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val trim_context_simproc: simproc -> simproc
val simpset_of: Proof.context -> simpset
@@ -208,14 +208,17 @@
(* simplification procedures *)
-datatype proc =
- Proc of
+type proc = Proof.context -> cterm -> thm option;
+
+datatype simproc0 =
+ Simproc0 of
{name: string,
lhs: term,
- proc: (Proof.context -> cterm -> thm option) Morphism.entity,
+ proc: proc Morphism.entity,
stamp: stamp};
-fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
+fun eq_simproc0 (Simproc0 {stamp = stamp1, ...}, Simproc0 {stamp = stamp2, ...}) =
+ stamp1 = stamp2;
(* solvers *)
@@ -257,7 +260,7 @@
prems: thm list,
depth: int * bool Unsynchronized.ref} *
{congs: thm Congtab.table * cong_name list,
- procs: proc Net.net,
+ procs: simproc0 Net.net,
mk_rews:
{mk: Proof.context -> thm -> thm list,
mk_cong: Proof.context -> thm -> thm,
@@ -288,7 +291,7 @@
{simps = Net.entries rules
|> map (fn {name, thm, ...} => (name, thm)),
procs = Net.entries procs
- |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
+ |> map (fn Simproc0 {name, lhs, stamp, ...} => ((name, lhs), stamp))
|> partition_eq (eq_snd op =)
|> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
congs = congs |> fst |> Congtab.dest,
@@ -336,7 +339,7 @@
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
val congs' = Congtab.merge (K true) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
- val procs' = Net.merge eq_proc (procs1, procs2);
+ val procs' = Net.merge eq_simproc0 (procs1, procs2);
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
val solvers' = merge eq_solver (solvers1, solvers2);
@@ -715,7 +718,7 @@
Simproc of
{name: string,
lhss: term list,
- proc: (Proof.context -> cterm -> thm option) Morphism.entity,
+ proc: proc Morphism.entity,
stamp: stamp};
fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
@@ -739,28 +742,28 @@
local
-fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
+fun add_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
(cond_tracing ctxt (fn () =>
print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
- (congs, Net.insert_term eq_proc (lhs, proc) procs,
+ (congs, Net.insert_term eq_simproc0 (lhs, proc) procs,
mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
handle Net.INSERT =>
(cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
ctxt));
-fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
+fun del_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
- (congs, Net.delete_term eq_proc (lhs, proc) procs,
+ (congs, Net.delete_term eq_simproc0 (lhs, proc) procs,
mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
handle Net.DELETE =>
(cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
ctxt);
fun prep_procs (Simproc {name, lhss, proc, stamp}) =
- lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, stamp = stamp});
+ lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, stamp = stamp});
in
@@ -1049,7 +1052,7 @@
in sort rrs ([], []) end;
fun proc_rews [] = NONE
- | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
+ | proc_rews (Simproc0 {name, proc, lhs, ...} :: ps) =
if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
(cond_tracing' ctxt simp_debug (fn () =>
print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
--- a/src/Pure/simplifier.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/Pure/simplifier.ML Thu Oct 19 17:06:39 2023 +0200
@@ -38,14 +38,13 @@
val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
val the_simproc: Proof.context -> string -> simproc
val make_simproc: Proof.context -> string ->
- {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
- type 'a simproc_spec =
- {passive: bool, lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
+ {lhss: term list, proc: morphism -> proc} -> simproc
+ type 'a simproc_spec = {passive: bool, lhss: 'a list, proc: morphism -> proc}
val define_simproc: binding -> term simproc_spec -> local_theory -> simproc * local_theory
val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> simproc * local_theory
type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a}
type simproc_setup_input = Input.source simproc_setup
- type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup
+ type simproc_setup_internal = (morphism -> proc) simproc_setup
val simproc_setup_parser: Input.source simproc_setup parser
val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list
val simproc_setup: simproc_setup_internal -> simproc
@@ -140,7 +139,7 @@
type 'a simproc_spec =
{passive: bool,
lhss: 'a list,
- proc: morphism -> Proof.context -> cterm -> thm option};
+ proc: morphism -> proc};
local
@@ -174,7 +173,7 @@
type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a};
type simproc_setup_input = Input.source simproc_setup;
-type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup;
+type simproc_setup_internal = (morphism -> proc) simproc_setup;
val simproc_setup_parser : simproc_setup_input parser =
Scan.optional (Parse.$$$ "passive" >> K true) false --
--- a/src/ZF/Datatype.thy Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/Datatype.thy Thu Oct 19 17:06:39 2023 +0200
@@ -63,7 +63,7 @@
structure Data_Free:
sig
val trace: bool Config.T
- val proc: Proof.context -> cterm -> thm option
+ val proc: Simplifier.proc
end =
struct
--- a/src/ZF/arith_data.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/arith_data.ML Thu Oct 19 17:06:39 2023 +0200
@@ -7,9 +7,9 @@
signature ARITH_DATA =
sig
(*the main outcome*)
- val nateq_cancel_numerals_proc: Proof.context -> cterm -> thm option
- val natless_cancel_numerals_proc: Proof.context -> cterm -> thm option
- val natdiff_cancel_numerals_proc: Proof.context -> cterm -> thm option
+ val nateq_cancel_numerals_proc: Simplifier.proc
+ val natless_cancel_numerals_proc: Simplifier.proc
+ val natdiff_cancel_numerals_proc: Simplifier.proc
(*tools for use in similar applications*)
val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
--- a/src/ZF/int_arith.ML Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/int_arith.ML Thu Oct 19 17:06:39 2023 +0200
@@ -6,11 +6,11 @@
signature INT_NUMERAL_SIMPROCS =
sig
- val inteq_cancel_numerals_proc: Proof.context -> cterm -> thm option
- val intless_cancel_numerals_proc: Proof.context -> cterm -> thm option
- val intle_cancel_numerals_proc: Proof.context -> cterm -> thm option
- val int_combine_numerals_proc: Proof.context -> cterm -> thm option
- val int_combine_numerals_prod_proc: Proof.context -> cterm -> thm option
+ val inteq_cancel_numerals_proc: Simplifier.proc
+ val intless_cancel_numerals_proc: Simplifier.proc
+ val intle_cancel_numerals_proc: Simplifier.proc
+ val int_combine_numerals_proc: Simplifier.proc
+ val int_combine_numerals_prod_proc: Simplifier.proc
end
structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =