simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
--- a/NEWS Sat Oct 21 14:36:47 2023 +0200
+++ b/NEWS Sat Oct 21 21:19:02 2023 +0200
@@ -40,6 +40,22 @@
val eq_simproc = \<^simproc_setup>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
+* Simplification procedures may be distinguished via characteristic
+theorems that are specified as 'identifier' in ML antiquotation
+"simproc_setup" (but not in the corresponding Isar command). This allows
+to work with several versions of the simproc, e.g. due to locale
+interpretations. For example:
+
+ locale test = fixes x y :: 'a assumes eq: "x = y"
+ begin
+
+ ML \<open>
+ \<^simproc_setup>\<open>foo (x) = \<open>fn _ => fn _ => fn _ => SOME @{thm eq}\<close>
+ identifier test_axioms\<close>
+ \<close>
+
+ end
+
* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 21 21:19:02 2023 +0200
@@ -40,14 +40,16 @@
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
fun mk_perm_bool_simproc names =
- Simplifier.make_simproc \<^context> "perm_bool"
- {lhss = [\<^term>\<open>perm pi x\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "perm_bool",
+ lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
- | _ => NONE)};
+ | _ => NONE),
+ identifier = []};
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Oct 21 21:19:02 2023 +0200
@@ -44,14 +44,16 @@
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
fun mk_perm_bool_simproc names =
- Simplifier.make_simproc \<^context> "perm_bool"
- {lhss = [\<^term>\<open>perm pi x\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "perm_bool",
+ lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
- | _ => NONE)};
+ | _ => NONE),
+ identifier = []};
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);
--- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Oct 21 21:19:02 2023 +0200
@@ -364,14 +364,16 @@
mk_solver "distinctFieldSolver" (distinctTree_tac names);
fun distinct_simproc names =
- Simplifier.make_simproc \<^context> "DistinctTreeProver.distinct_simproc"
- {lhss = [\<^term>\<open>x = y\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "DistinctTreeProver.distinct_simproc",
+ lhss = [\<^term>\<open>x = y\<close>],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ x $ y =>
Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
- | _ => NONE)};
+ | _ => NONE),
+ identifier = []};
end;
--- a/src/HOL/Tools/groebner.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/groebner.ML Sat Oct 21 21:19:02 2023 +0200
@@ -779,9 +779,11 @@
let val th = poly_eq_conv ct
in if Thm.is_reflexive th then NONE else SOME th end
in
- Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
- {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
- proc = Morphism.entity (fn _ => fn _ => proc)}
+ Simplifier.cert_simproc (Thm.theory_of_thm idl_sub)
+ {name = "poly_eq_simproc",
+ lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
+ proc = Morphism.entity (fn _ => fn _ => proc),
+ identifier = []}
end;
val poly_eq_ss =
--- a/src/HOL/Tools/inductive_set.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sat Oct 21 21:19:02 2023 +0200
@@ -38,8 +38,9 @@
val anyt = Free ("t", TFree ("'t", []));
fun strong_ind_simproc tab =
- Simplifier.make_simproc \<^context> "strong_ind"
- {lhss = [\<^term>\<open>x::'a::{}\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "strong_ind",
+ lhss = [\<^term>\<open>x::'a::{}\<close>],
proc = fn _ => fn ctxt => fn ct =>
let
fun close p t f =
@@ -102,7 +103,8 @@
end
else NONE
| _ => NONE)
- end};
+ end,
+ identifier = []};
(* only eta contract terms occurring as arguments of functions satisfying p *)
fun eta_contract p =
@@ -318,11 +320,13 @@
fun to_pred_simproc rules =
let val rules' = map mk_meta_eq rules
in
- Simplifier.make_simproc \<^context> "to_pred"
- {lhss = [anyt],
+ Simplifier.make_simproc \<^context>
+ {name = "to_pred",
+ lhss = [anyt],
proc = fn _ => fn ctxt => fn ct =>
lookup_rule (Proof_Context.theory_of ctxt)
- (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)}
+ (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
+ identifier = []}
end;
fun to_pred_proc thy rules t =
--- a/src/HOL/Tools/record.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/record.ML Sat Oct 21 21:19:02 2023 +0200
@@ -1322,8 +1322,9 @@
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
fun split_simproc P =
- Simplifier.make_simproc \<^context> "record_split"
- {lhss = [\<^term>\<open>x::'a::{}\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "record_split",
+ lhss = [\<^term>\<open>x::'a::{}\<close>],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1348,7 +1349,8 @@
else NONE
end)
else NONE
- | _ => NONE)};
+ | _ => NONE),
+ identifier = []};
fun ex_sel_eq_proc ctxt ct =
let
--- a/src/Pure/ML/ml_thms.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/ML/ml_thms.ML Sat Oct 21 21:19:02 2023 +0200
@@ -8,6 +8,8 @@
sig
val the_attributes: Proof.context -> int -> Token.src list
val the_thmss: Proof.context -> thm list list
+ val thm_binding: string -> bool -> thm list -> Proof.context ->
+ (Proof.context -> string * string) * Proof.context
val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser
val get_stored_thms: unit -> thm list
val get_stored_thm: unit -> thm
--- a/src/Pure/Pure.thy Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/Pure.thy Sat Oct 21 21:19:02 2023 +0200
@@ -7,7 +7,7 @@
theory Pure
keywords
"!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<subseteq>" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output"
+ "\<subseteq>" "]" "binder" "by" "identifier" "in" "infix" "infixl" "infixr" "is" "open" "output"
"overloaded" "passive" "pervasive" "premises" "structure" "unchecked"
and "private" "qualified" :: before_command
and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
--- a/src/Pure/ROOT.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/ROOT.ML Sat Oct 21 21:19:02 2023 +0200
@@ -277,6 +277,7 @@
ML_file "Isar/class_declaration.ML";
ML_file "Isar/target_context.ML";
ML_file "Isar/experiment.ML";
+ML_file "ML/ml_thms.ML";
ML_file "simplifier.ML";
ML_file "Tools/plugin.ML";
@@ -327,7 +328,6 @@
(*ML add-ons*)
ML_file "ML/ml_pp.ML";
-ML_file "ML/ml_thms.ML";
ML_file "ML/ml_instantiate.ML";
ML_file "ML/ml_file.ML";
ML_file "ML/ml_pid.ML";
--- a/src/Pure/raw_simplifier.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Sat Oct 21 21:19:02 2023 +0200
@@ -36,8 +36,8 @@
safe_solvers: string list}
val dest_simps: simpset -> thm list
type simproc
- val eq_simproc: simproc * simproc -> bool
- val cert_simproc: theory -> string -> {lhss: term list, proc: proc Morphism.entity} -> simproc
+ val cert_simproc: theory ->
+ {name: string, lhss: term list, proc: proc Morphism.entity, identifier: thm list} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val trim_context_simproc: simproc -> simproc
val simpset_of: Proof.context -> simpset
@@ -215,10 +215,12 @@
{name: string,
lhs: term,
proc: proc Morphism.entity,
- stamp: stamp};
+ id: stamp * thm list};
-fun eq_simproc0 (Simproc0 {stamp = stamp1, ...}, Simproc0 {stamp = stamp2, ...}) =
- stamp1 = stamp2;
+fun eq_simproc_id ((s1: stamp, ths1: thm list), (s2, ths2)) =
+ s1 = s2 andalso eq_list Thm.eq_thm_prop (ths1, ths2);
+
+fun eq_simproc0 (Simproc0 a, Simproc0 b) = eq_simproc_id (#id a, #id b);
(* solvers *)
@@ -291,8 +293,8 @@
{simps = Net.entries rules
|> map (fn {name, thm, ...} => (name, thm)),
procs = Net.entries procs
- |> map (fn Simproc0 {name, lhs, stamp, ...} => ((name, lhs), stamp))
- |> partition_eq (eq_snd op =)
+ |> map (fn Simproc0 {name, lhs, id, ...} => ((name, lhs), id))
+ |> partition_eq (eq_snd eq_simproc_id)
|> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
congs = congs |> fst |> Congtab.dest,
weak_congs = congs |> snd,
@@ -719,26 +721,28 @@
{name: string,
lhss: term list,
proc: proc Morphism.entity,
- stamp: stamp};
-
-fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
+ id: stamp * thm list};
-fun cert_simproc thy name {lhss, proc} =
- Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
+fun cert_simproc thy {name, lhss, proc, identifier} =
+ Simproc
+ {name = name,
+ lhss = map (Sign.cert_term thy) lhss,
+ proc = proc,
+ id = (stamp (), map (Thm.transfer thy) identifier)};
-fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
+fun transform_simproc phi (Simproc {name, lhss, proc, id = (stamp, identifier)}) =
Simproc
{name = name,
lhss = map (Morphism.term phi) lhss,
proc = Morphism.transform phi proc,
- stamp = stamp};
+ id = (stamp, Morphism.fact phi identifier)};
-fun trim_context_simproc (Simproc {name, lhss, proc, stamp}) =
+fun trim_context_simproc (Simproc {name, lhss, proc, id = (stamp, identifier)}) =
Simproc
{name = name,
lhss = lhss,
proc = Morphism.entity_reset_context proc,
- stamp = stamp};
+ id = (stamp, map Thm.trim_context identifier)};
local
@@ -762,8 +766,8 @@
(cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
ctxt);
-fun prep_procs (Simproc {name, lhss, proc, stamp}) =
- lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, stamp = stamp});
+fun prep_procs (Simproc {name, lhss, proc, id}) =
+ lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, id = id});
in
--- a/src/Pure/simplifier.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/Pure/simplifier.ML Sat Oct 21 21:19:02 2023 +0200
@@ -37,14 +37,16 @@
val cong_del: attribute
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 -> proc} -> simproc
- type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b}
- val read_simproc_spec: Proof.context -> (string, 'a) simproc_spec -> (term, 'a) simproc_spec
- val define_simproc: (term, morphism -> proc) simproc_spec -> local_theory ->
+ val make_simproc: Proof.context ->
+ {name: string, lhss: term list, proc: morphism -> proc, identifier: thm list} -> simproc
+ type ('a, 'b, 'c) simproc_spec =
+ {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c}
+ val read_simproc_spec: Proof.context ->
+ (string, 'b, 'c) simproc_spec -> (term, 'b, 'c) simproc_spec
+ val define_simproc: (term, morphism -> proc, thm list) simproc_spec -> local_theory ->
simproc * local_theory
- val simproc_setup: (term, morphism -> proc) simproc_spec -> simproc
- val simproc_setup_cmd: (string, morphism -> proc) simproc_spec -> simproc
+ val simproc_setup: (term, morphism -> proc, thm list) simproc_spec -> simproc
+ val simproc_setup_cmd: (string, morphism -> proc, thm list) simproc_spec -> simproc
val simproc_setup_command: (local_theory -> local_theory) parser
val pretty_simpset: bool -> Proof.context -> Pretty.T
val default_mk_sym: Proof.context -> thm -> thm option
@@ -125,28 +127,30 @@
(* define simprocs *)
-fun make_simproc ctxt name {lhss, proc} =
+fun make_simproc ctxt {name, lhss, proc, identifier} =
let
val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
- cert_simproc (Proof_Context.theory_of ctxt) name
- {lhss = lhss', proc = Morphism.entity proc}
+ cert_simproc (Proof_Context.theory_of ctxt)
+ {name = name, lhss = lhss', proc = Morphism.entity proc, identifier = identifier}
end;
-type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b};
+type ('a, 'b, 'c) simproc_spec =
+ {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c};
-fun read_simproc_spec ctxt {passive, name, lhss, proc} : (term, 'a) simproc_spec =
+fun read_simproc_spec ctxt {passive, name, lhss, proc, identifier} =
let
val lhss' =
Syntax.read_terms ctxt lhss handle ERROR msg =>
error (msg ^ Position.here_list (map Syntax.read_input_pos lhss));
- in {passive = passive, name = name, lhss = lhss', proc = proc} end;
+ in {passive = passive, name = name, lhss = lhss', proc = proc, identifier = identifier} end;
-fun define_simproc {passive, name, lhss, proc} lthy =
+fun define_simproc {passive, name, lhss, proc, identifier} lthy =
let
val simproc0 =
- make_simproc lthy (Local_Theory.full_name lthy name) {lhss = lhss, proc = proc};
+ make_simproc lthy
+ {name = Local_Theory.full_name lthy name, lhss = lhss, proc = proc, identifier = identifier};
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name}
(fn phi => fn context =>
@@ -171,12 +175,14 @@
Named_Target.setup_result Raw_Simplifier.transform_simproc
(fn lthy => lthy |> define_simproc (read_simproc_spec lthy args));
-val simproc_setup_parser =
+
+val parse_simproc_spec =
Scan.optional (Parse.$$$ "passive" >> K true) false --
Parse.binding --
(Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
- (Parse.$$$ "=" |-- Parse.ML_source)
- >> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d});
+ (Parse.$$$ "=" |-- Parse.ML_source) --
+ Scan.option ((Parse.position (Parse.$$$ "identifier") >> #2) -- Parse.thms1)
+ >> (fn ((((a, b), c), d), e) => {passive = a, name = b, lhss = c, proc = d, identifier = e});
val _ = Theory.setup
(ML_Context.add_antiquotation_embedded \<^binding>\<open>simproc_setup\<close>
@@ -184,31 +190,44 @@
let
val ml = ML_Lex.tokenize_no_range;
- val {passive, name, lhss, proc} = input
- |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) simproc_setup_parser
+ val {passive, name, lhss, proc, identifier} = input
+ |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) parse_simproc_spec
|> read_simproc_spec ctxt;
- val (decl, ctxt') = ML_Context.read_antiquotes proc ctxt;
- fun decl' ctxt'' =
+ val (decl1, ctxt1) = ML_Context.read_antiquotes proc ctxt;
+ val (decl2, ctxt2) =
+ (case identifier of
+ NONE => (K ("", "[]"), ctxt1)
+ | SOME (_, thms) => ML_Thms.thm_binding "thms" false (Attrib.eval_thms ctxt1 thms) ctxt1);
+
+ fun decl' ctxt' =
let
- val (ml_env, ml_body) = decl ctxt'';
+ val (ml_env1, ml_body1) = decl1 ctxt';
+ val (ml_env2, ml_body2) = decl2 ctxt' |> apply2 ml;
val ml_body' =
ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @
ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @
ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss) @
- ml ", proc = (" @ ml_body @ ml ")}";
- in (ml_env, ml_body') end;
- in (decl', ctxt') end));
+ ml ", proc = (" @ ml_body1 @ ml ")" @
+ ml ", identifier = (" @ ml_body2 @ ml ")}";
+ in (ml_env1 @ ml_env2, ml_body') end;
+ in (decl', ctxt2) end));
val simproc_setup_command =
- simproc_setup_parser >> (fn {passive, name, lhss, proc} =>
- Context.proof_map
- (ML_Context.expression (Input.pos_of proc)
- (ML_Lex.read
- ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^
- ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
- ", lhss = " ^ ML_Syntax.print_strings lhss ^
- ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}")));
+ parse_simproc_spec >> (fn {passive, name, lhss, proc, identifier} =>
+ (case identifier of
+ NONE =>
+ Context.proof_map
+ (ML_Context.expression (Input.pos_of proc)
+ (ML_Lex.read
+ ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^
+ ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
+ ", lhss = " ^ ML_Syntax.print_strings lhss ^
+ ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read "), identifier = []}"))
+ | SOME (pos, _) =>
+ error ("Bad command " ^ Markup.markup Markup.keyword1 "simproc_setup" ^
+ " with " ^ Markup.markup Markup.keyword2 "identifier" ^
+ ": this is only supported in\nML antiquotation \<^simproc_setup>\<open>...\<close>" ^ Position.here pos)));