--- a/src/HOL/Tools/record.ML Sat May 27 23:34:07 2023 +0200
+++ b/src/HOL/Tools/record.ML Sat May 27 23:34:42 2023 +0200
@@ -1116,9 +1116,8 @@
| _ => NONE)
end}));
-val simproc_name =
- Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none);
-val simproc = Simplifier.the_simproc (Context.the_local_context ()) simproc_name;
+val simproc =
+ #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
fun get_upd_acc_cong_thm upd acc thy ss =
let
@@ -1284,9 +1283,8 @@
else NONE
end}));
-val upd_simproc_name =
- Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none);
-val upd_simproc = Simplifier.the_simproc (Context.the_local_context ()) upd_simproc_name;
+val upd_simproc =
+ #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none));
end;
@@ -1319,8 +1317,9 @@
| SOME thm => SOME (thm RS @{thm Eq_TrueI})))
| _ => NONE)}));
-val eq_simproc_name = Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none);
-val eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) eq_simproc_name;
+val eq_simproc =
+ #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none));
+
(* split_simproc *)
@@ -1398,9 +1397,9 @@
| _ => NONE)
end}));
-val ex_sel_eq_simproc_name =
- Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none);
-val ex_sel_eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) ex_sel_eq_simproc_name;
+val ex_sel_eq_simproc =
+ #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none));
+
val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc]));
--- a/src/Pure/ex/Def.thy Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/ex/Def.thy Sat May 27 23:34:42 2023 +0200
@@ -32,6 +32,9 @@
fun transform_def phi ({lhs, eq}: def) =
{lhs = Morphism.term phi lhs, eq = Morphism.thm phi eq};
+fun trim_context_def ({lhs, eq}: def) =
+ {lhs = lhs, eq = Thm.trim_context eq};
+
structure Data = Generic_Data
(
type T = def Item_Net.T;
@@ -43,8 +46,8 @@
let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => fn context =>
- let val psi = Morphism.set_trim_context'' context phi
- in (Data.map o Item_Net.update) (transform_def psi def0) context end)
+ let val def' = def0 |> transform_def phi |> trim_context_def
+ in (Data.map o Item_Net.update) def' context end)
end;
fun get_def ctxt ct =
--- a/src/Pure/morphism.ML Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/morphism.ML Sat May 27 23:34:42 2023 +0200
@@ -49,6 +49,9 @@
val transform_reset_context: morphism -> 'a entity -> 'a entity
val form: 'a entity -> 'a
val form_entity: (morphism -> 'a) -> 'a
+ val form_context: theory -> (theory -> 'a) entity -> 'a
+ val form_context': Proof.context -> (Proof.context -> 'a) entity -> 'a
+ val form_context'': Context.generic -> (Context.generic -> 'a) entity -> 'a
type declaration = morphism -> Context.generic -> Context.generic
type declaration_entity = (Context.generic -> Context.generic) entity
val binding_morphism: string -> (binding -> binding) -> morphism
@@ -193,6 +196,10 @@
fun form (Entity (f, phi)) = f phi;
fun form_entity f = f identity;
+fun form_context thy x = form (entity_set_context thy x) thy;
+fun form_context' ctxt x = form (entity_set_context' ctxt x) ctxt;
+fun form_context'' context x = form (entity_set_context'' context x) context;
+
type declaration = morphism -> Context.generic -> Context.generic;
type declaration_entity = (Context.generic -> Context.generic) entity;
--- a/src/Pure/raw_simplifier.ML Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Sat May 27 23:34:42 2023 +0200
@@ -38,6 +38,7 @@
val cert_simproc: theory -> string ->
{lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
val transform_simproc: morphism -> simproc -> simproc
+ val trim_context_simproc: simproc -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
@@ -208,7 +209,7 @@
Proc of
{name: string,
lhs: term,
- proc: Proof.context -> cterm -> thm option,
+ proc: (Proof.context -> cterm -> thm option) Morphism.entity,
stamp: stamp};
fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
@@ -721,7 +722,14 @@
Simproc
{name = name,
lhss = map (Morphism.term phi) lhss,
- proc = Morphism.transform_reset_context phi proc,
+ proc = Morphism.transform phi proc,
+ stamp = stamp};
+
+fun trim_context_simproc (Simproc {name, lhss, proc, stamp}) =
+ Simproc
+ {name = name,
+ lhss = lhss,
+ proc = Morphism.entity_reset_context proc,
stamp = stamp};
local
@@ -747,7 +755,7 @@
ctxt);
fun prep_procs (Simproc {name, lhss, proc, stamp}) =
- lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
+ lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, stamp = stamp});
in
@@ -1041,7 +1049,7 @@
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);
- (case proc ctxt eta_t' of
+ (case Morphism.form_context' ctxt proc eta_t' of
NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
| SOME raw_thm =>
(cond_tracing ctxt (fn () =>
--- a/src/Pure/simplifier.ML Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/simplifier.ML Sat May 27 23:34:42 2023 +0200
@@ -35,7 +35,7 @@
val simp_flip: attribute
val cong_add: attribute
val cong_del: attribute
- val check_simproc: Proof.context -> xstring * Position.T -> string
+ val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
val the_simproc: Proof.context -> string -> simproc
type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
@@ -109,14 +109,13 @@
val get_simprocs = Simprocs.get o Context.Proof;
-fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
val the_simproc = Name_Space.get o get_simprocs;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt);
val _ = Theory.setup
(ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
- (Args.context -- Scan.lift Parse.embedded_position
- >> (fn (ctxt, name) =>
- "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, name) =>
+ "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (#1 (check_simproc ctxt name)))));
(* define simprocs *)
@@ -136,14 +135,14 @@
fun def_simproc prep b {lhss, proc} lthy =
let
- val simproc =
+ val simproc0 =
make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b}
(fn phi => fn context =>
let
val b' = Morphism.binding phi b;
- val simproc' = transform_simproc phi simproc;
+ val simproc' = simproc0 |> transform_simproc phi |> trim_context_simproc;
in
context
|> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
@@ -319,7 +318,7 @@
val simproc_att =
(Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
- Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
+ Scan.repeat1 (Scan.lift (Args.named_attribute (decl o #2 o check_simproc ctxt))))
>> (fn atts => Thm.declaration_attribute (fn th =>
fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));