--- a/src/HOL/Analysis/Measurable.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Analysis/Measurable.thy Thu Oct 19 21:38:09 2023 +0200
@@ -67,7 +67,8 @@
method_setup\<^marker>\<open>tag important\<close> measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
"measurability prover"
-simproc_setup\<^marker>\<open>tag important\<close> measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
+simproc_setup\<^marker>\<open>tag important\<close> measurable ("A \<in> sets M" | "f \<in> measurable M N") =
+ \<open>K Measurable.proc\<close>
setup \<open>
Global_Theory.add_thms_dynamic (\<^binding>\<open>measurable\<close>, Measurable.get_all)
--- a/src/HOL/Analysis/measurable.ML Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML Thu Oct 19 21:38:09 2023 +0200
@@ -22,14 +22,14 @@
val measurable_tac : Proof.context -> thm list -> tactic
- val simproc : Simplifier.proc
+ val proc : Simplifier.proc
val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
val del_preprocessor : string -> Context.generic -> Context.generic
val add_local_cong : thm -> Proof.context -> Proof.context
val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context)
-end ;
+end
structure Measurable : MEASURABLE =
struct
@@ -256,7 +256,7 @@
in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end;
-fun simproc ctxt redex =
+fun proc ctxt redex =
let
val t = HOLogic.mk_Trueprop (Thm.term_of redex);
fun tac {context = ctxt, prems = _ } =
--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Oct 19 21:38:09 2023 +0200
@@ -199,6 +199,6 @@
ML_file \<open>Tools/datatype_simprocs.ML\<close>
simproc_setup datatype_no_proper_subterm
- ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_simproc\<close>
+ ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_proc\<close>
end
--- a/src/HOL/Finite_Set.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Finite_Set.thy Thu Oct 19 21:38:09 2023 +0200
@@ -24,7 +24,7 @@
end
-simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
+simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.proc\<close>
declare [[simproc del: finite_Collect]]
--- a/src/HOL/List.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/List.thy Thu Oct 19 21:38:09 2023 +0200
@@ -557,7 +557,7 @@
signature LIST_TO_SET_COMPREHENSION =
sig
- val simproc : Simplifier.proc
+ val proc: Simplifier.proc
end
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
@@ -717,7 +717,7 @@
in
-fun simproc ctxt redex =
+fun proc ctxt redex =
let
fun make_inner_eqs bound_vs Tis eqs t =
(case dest_case ctxt t of
@@ -774,7 +774,7 @@
\<close>
simproc_setup list_to_set_comprehension ("set xs") =
- \<open>K List_to_Set_Comprehension.simproc\<close>
+ \<open>K List_to_Set_Comprehension.proc\<close>
code_datatype set coset
hide_const (open) coset
--- a/src/HOL/Product_Type.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Product_Type.thy Thu Oct 19 21:38:09 2023 +0200
@@ -1304,7 +1304,7 @@
ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
simproc_setup passive set_comprehension ("Collect P") =
- \<open>K Set_Comprehension_Pointfree.code_simproc\<close>
+ \<open>K Set_Comprehension_Pointfree.code_proc\<close>
setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>set_comprehension\<close>])\<close>
--- a/src/HOL/Tools/datatype_simprocs.ML Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML Thu Oct 19 21:38:09 2023 +0200
@@ -6,7 +6,7 @@
*)
signature DATATYPE_SIMPROCS = sig
- val no_proper_subterm_simproc : Simplifier.proc
+ val no_proper_subterm_proc : Simplifier.proc
end
structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct
@@ -86,7 +86,7 @@
- support for nested datatypes
- replace size-based proof with proper subexpression relation
*)
-fun no_proper_subterm_simproc ctxt ct =
+fun no_proper_subterm_proc ctxt ct =
let
val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd)
val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 19 21:38:09 2023 +0200
@@ -7,9 +7,9 @@
signature SET_COMPREHENSION_POINTFREE =
sig
- val base_simproc : Simplifier.proc
- val code_simproc : Simplifier.proc
- val simproc : Simplifier.proc
+ val base_proc : Simplifier.proc
+ val code_proc : Simplifier.proc
+ val proc : Simplifier.proc
end
structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
@@ -484,7 +484,7 @@
Option.map (export o post o unfold o mk_thm) (rewrite_term t'')
end;
-fun base_simproc ctxt redex =
+fun base_proc ctxt redex =
let
val set_compr = Thm.term_of redex
in
@@ -500,7 +500,7 @@
infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
end;
-fun simproc ctxt redex =
+fun proc ctxt redex =
let
val pred $ set_compr = Thm.term_of redex
val arg_cong' = instantiate_arg_cong ctxt pred
@@ -509,14 +509,14 @@
|> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
end;
-fun code_simproc ctxt redex =
+fun code_proc ctxt redex =
let
fun unfold_conv thms =
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(empty_simpset ctxt addsimps thms)
val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
in
- case base_simproc ctxt (Thm.rhs_of prep_thm) of
+ case base_proc ctxt (Thm.rhs_of prep_thm) of
SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
unfold_conv @{thms eq_equal} (Thm.rhs_of rewr_thm)])
| NONE => NONE
--- a/src/HOL/Transcendental.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Transcendental.thy Thu Oct 19 21:38:09 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 : Simplifier.proc
-val root_simproc : int * int -> Simplifier.proc
-val powr_simproc : int * int -> Simplifier.proc
+val sqrt_proc : Simplifier.proc
+val root_proc : int * int -> Simplifier.proc
+val powr_proc : int * int -> Simplifier.proc
end
@@ -7428,7 +7428,7 @@
NONE => NONE
| SOME y => if y * y = x then SOME y else NONE
-fun sqrt_simproc ctxt ct =
+fun sqrt_proc ctxt ct =
let
val n = ct |> Thm.term_of |> dest_comb |> snd |> dest_comb |> snd |> HOLogic.dest_numeral
in
@@ -7440,7 +7440,7 @@
end
handle TERM _ => NONE
-fun root_simproc (threshold1, threshold2) ctxt ct =
+fun root_proc (threshold1, threshold2) ctxt ct =
let
val [n, x] =
ct |> Thm.term_of |> strip_comb |> snd |> map (dest_comb #> snd #> HOLogic.dest_numeral)
@@ -7455,7 +7455,7 @@
handle TERM _ => NONE
| Match => NONE
-fun powr_simproc (threshold1, threshold2) ctxt ct =
+fun powr_proc (threshold1, threshold2) ctxt ct =
let
val eq_thm = Conv.try_conv (Conv.rewr_conv @{thm numeral_powr_inverse_eq}) ct
val ct = Thm.dest_equals_rhs (Thm.cprop_of eq_thm)
@@ -7484,14 +7484,14 @@
end
simproc_setup sqrt_numeral ("sqrt (numeral n)") =
- \<open>K Root_Numeral_Simproc.sqrt_simproc\<close>
+ \<open>K Root_Numeral_Simproc.sqrt_proc\<close>
simproc_setup root_numeral ("root (numeral n) (numeral x)") =
- \<open>K (Root_Numeral_Simproc.root_simproc (200, Integer.pow 200 2))\<close>
+ \<open>K (Root_Numeral_Simproc.root_proc (200, Integer.pow 200 2))\<close>
simproc_setup powr_divide_numeral
("numeral x powr (m / numeral n :: real)" | "numeral x powr (inverse (numeral n) :: real)") =
- \<open>K (Root_Numeral_Simproc.powr_simproc (200, Integer.pow 200 2))\<close>
+ \<open>K (Root_Numeral_Simproc.powr_proc (200, Integer.pow 200 2))\<close>
lemma "root 100 1267650600228229401496703205376 = 2"