# HG changeset patch # User wenzelm # Date 1697639364 -7200 # Node ID f34926a91fea0e4c8962747a529a354e7e3d3400 # Parent f7e972d567f3a5fd857ec605a2260bc80fb07929 clarified signature: more concise simproc setup in ML; diff -r f7e972d567f3 -r f34926a91fea src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Oct 18 15:13:52 2023 +0200 +++ b/src/HOL/Tools/record.ML Wed Oct 18 16:29:24 2023 +0200 @@ -1060,65 +1060,65 @@ - If X is a more-selector we have to make sure that S is not in the updated subrecord. *) -val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\select_update\ - {lhss = [\<^term>\x::'a::{}\], - passive = false, - proc = fn _ => fn ctxt => fn ct => - let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - in - (case t of - (sel as Const (s, Type (_, [_, rangeS]))) $ - ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => - if is_selector thy s andalso is_some (get_updates thy u) then - let - val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy; - - fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = - (case Symtab.lookup updates u of - NONE => NONE - | SOME u_name => - if u_name = s then - (case mk_eq_terms r of - NONE => - let - val rv = ("r", rT); - val rb = Bound 0; - val (kv, kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end - | SOME (trm, trm', vars) => - let - val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k; - in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end) - else if has_field extfields u_name rangeS orelse - has_field extfields s (domain_type kT) then NONE - else - (case mk_eq_terms r of - SOME (trm, trm', vars) => - let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k - in SOME (upd $ kb $ trm, trm', kv :: vars) end - | NONE => - let - val rv = ("r", rT); - val rb = Bound 0; - val (kv, kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end)) - | mk_eq_terms _ = NONE; - in - (case mk_eq_terms (upd $ k $ r) of - SOME (trm, trm', vars) => - SOME - (prove_unfold_defs thy [] [] [] - (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm')))) - | NONE => NONE) - end - else NONE - | _ => NONE) - end}); + +fun select_update_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + in + (case t of + (sel as Const (s, Type (_, [_, rangeS]))) $ + ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => + if is_selector thy s andalso is_some (get_updates thy u) then + let + val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy; + + fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = + (case Symtab.lookup updates u of + NONE => NONE + | SOME u_name => + if u_name = s then + (case mk_eq_terms r of + NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end + | SOME (trm, trm', vars) => + let + val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k; + in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end) + else if has_field extfields u_name rangeS orelse + has_field extfields s (domain_type kT) then NONE + else + (case mk_eq_terms r of + SOME (trm, trm', vars) => + let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k + in SOME (upd $ kb $ trm, trm', kv :: vars) end + | NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end)) + | mk_eq_terms _ = NONE; + in + (case mk_eq_terms (upd $ k $ r) of + SOME (trm, trm', vars) => + SOME + (prove_unfold_defs thy [] [] [] + (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm')))) + | NONE => NONE) + end + else NONE + | _ => NONE) + end; val simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none)); + Simplifier.simproc_setup_global + {name = \<^binding>\select_update\, lhss = ["x::'a::{}"], proc = K select_update_proc, + passive = false}; fun get_upd_acc_cong_thm upd acc thy ss = let @@ -1165,128 +1165,127 @@ In both cases "more" updates complicate matters: for this reason we omit considering further updates if doing so would introduce both a more update and an update to a field within it.*) -val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\update\ - {lhss = [\<^term>\x::'a::{}\], - passive = false, - proc = fn _ => fn ctxt => fn ct => + +fun upd_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + (*We can use more-updators with other updators as long + as none of the other updators go deeper than any more + updator. min here is the depth of the deepest other + updator, max the depth of the shallowest more updator.*) + fun include_depth (dep, true) (min, max) = + if min <= dep + then SOME (min, if dep <= max orelse max = ~1 then dep else max) + else NONE + | include_depth (dep, false) (min, max) = + if dep <= max orelse max = ~1 + then SOME (if min <= dep then dep else min, max) + else NONE; + + fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max = + (case get_update_details u thy of + SOME (s, dep, ismore) => + (case include_depth (dep, ismore) (min, max) of + SOME (min', max') => + let val (us, bs, _) = getupdseq tm min' max' + in ((upd, s, f) :: us, bs, fastype_of term) end + | NONE => ([], term, HOLogic.unitT)) + | NONE => ([], term, HOLogic.unitT)) + | getupdseq term _ _ = ([], term, HOLogic.unitT); + + val (upds, base, baseT) = getupdseq t 0 ~1; + val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds + val upd_ord = rev_order o fast_string_ord o apply2 #2 + val (upds, commuted) = + if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then + (sort upd_ord orig_upds, true) + else + (orig_upds, false) + + fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm = + if s = s' andalso null (loose_bnos tm') + andalso subst_bound (HOLogic.unit, tm') = tm + then (true, Abs (n, T, Const (s', T') $ Bound 1)) + else (false, HOLogic.unit) + | is_upd_noop _ _ _ = (false, HOLogic.unit); + + fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - (*We can use more-updators with other updators as long - as none of the other updators go deeper than any more - updator. min here is the depth of the deepest other - updator, max the depth of the shallowest more updator.*) - fun include_depth (dep, true) (min, max) = - if min <= dep - then SOME (min, if dep <= max orelse max = ~1 then dep else max) - else NONE - | include_depth (dep, false) (min, max) = - if dep <= max orelse max = ~1 - then SOME (if min <= dep then dep else min, max) - else NONE; - - fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max = - (case get_update_details u thy of - SOME (s, dep, ismore) => - (case include_depth (dep, ismore) (min, max) of - SOME (min', max') => - let val (us, bs, _) = getupdseq tm min' max' - in ((upd, s, f) :: us, bs, fastype_of term) end - | NONE => ([], term, HOLogic.unitT)) - | NONE => ([], term, HOLogic.unitT)) - | getupdseq term _ _ = ([], term, HOLogic.unitT); - - val (upds, base, baseT) = getupdseq t 0 ~1; - val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds - val upd_ord = rev_order o fast_string_ord o apply2 #2 - val (upds, commuted) = - if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then - (sort upd_ord orig_upds, true) - else - (orig_upds, false) - - fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm = - if s = s' andalso null (loose_bnos tm') - andalso subst_bound (HOLogic.unit, tm') = tm - then (true, Abs (n, T, Const (s', T') $ Bound 1)) - else (false, HOLogic.unit) - | is_upd_noop _ _ _ = (false, HOLogic.unit); - - fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = + val ss = get_sel_upd_defs thy; + val uathm = get_upd_acc_cong_thm upd acc thy ss; + in + [Drule.export_without_context (uathm RS updacc_noopE), + Drule.export_without_context (uathm RS updacc_noop_compE)] + end; + + (*If f is constant then (f o g) = f. We know that K_skeleton + only returns constant abstractions thus when we see an + abstraction we can discard inner updates.*) + fun add_upd (f as Abs _) _ = [f] + | add_upd f fs = (f :: fs); + + (*mk_updterm returns + (orig-term-skeleton-update list , simplified-skeleton, + variables, duplicate-updates, simp-flag, noop-simps) + + where duplicate-updates is a table used to pass upward + the list of update functions which can be composed + into an update above them, simp-flag indicates whether + any simplification was achieved, and noop-simps are + used for eliminating case (2) defined above*) + fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term = let - val ss = get_sel_upd_defs thy; - val uathm = get_upd_acc_cong_thm upd acc thy ss; + val (lhs_upds, rhs, vars, dups, simp, noops) = + mk_updterm upds (Symtab.update (u, ()) above) term; + val (fvar, skelf) = + K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; + val (isnoop, skelf') = is_upd_noop s f term; + val funT = domain_type T; + fun mk_comp_local (f, f') = + Const (\<^const_name>\Fun.comp\, funT --> funT --> funT) $ f $ f'; in - [Drule.export_without_context (uathm RS updacc_noopE), - Drule.export_without_context (uathm RS updacc_noop_compE)] - end; - - (*If f is constant then (f o g) = f. We know that K_skeleton - only returns constant abstractions thus when we see an - abstraction we can discard inner updates.*) - fun add_upd (f as Abs _) _ = [f] - | add_upd f fs = (f :: fs); - - (*mk_updterm returns - (orig-term-skeleton-update list , simplified-skeleton, - variables, duplicate-updates, simp-flag, noop-simps) - - where duplicate-updates is a table used to pass upward - the list of update functions which can be composed - into an update above them, simp-flag indicates whether - any simplification was achieved, and noop-simps are - used for eliminating case (2) defined above*) - fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term = - let - val (lhs_upds, rhs, vars, dups, simp, noops) = - mk_updterm upds (Symtab.update (u, ()) above) term; - val (fvar, skelf) = - K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; - val (isnoop, skelf') = is_upd_noop s f term; - val funT = domain_type T; - fun mk_comp_local (f, f') = - Const (\<^const_name>\Fun.comp\, funT --> funT --> funT) $ f $ f'; - in - if isnoop then - ((upd $ skelf', i)::lhs_upds, rhs, vars, - Symtab.update (u, []) dups, true, - if Symtab.defined noops u then noops - else Symtab.update (u, get_noop_simps upd skelf') noops) - else if Symtab.defined above u then - ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars, - Symtab.map_default (u, []) (add_upd skelf) dups, - true, noops) - else - (case Symtab.lookup dups u of - SOME fs => - ((upd $ skelf, i)::lhs_upds, - upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, - fvar :: vars, dups, true, noops) - | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) - end - | mk_updterm [] _ _ = - ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) - | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us); - - val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base; - val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd) - val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds - (* Note that the simplifier works bottom up. So all nested updates are already - normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be - inserted at its place inside the sorted nested updates. The necessary swaps can be - expressed via 'upd_funs' by replicating the outer update at the designated position: *) - val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1 - val noops' = maps snd (Symtab.dest noops); - in - if simp orelse commuted then - SOME - (prove_unfold_defs thy upd_funs noops' [simproc] - (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) - else NONE - end}); + if isnoop then + ((upd $ skelf', i)::lhs_upds, rhs, vars, + Symtab.update (u, []) dups, true, + if Symtab.defined noops u then noops + else Symtab.update (u, get_noop_simps upd skelf') noops) + else if Symtab.defined above u then + ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars, + Symtab.map_default (u, []) (add_upd skelf) dups, + true, noops) + else + (case Symtab.lookup dups u of + SOME fs => + ((upd $ skelf, i)::lhs_upds, + upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, + fvar :: vars, dups, true, noops) + | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) + end + | mk_updterm [] _ _ = + ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) + | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us); + + val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base; + val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd) + val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds + (* Note that the simplifier works bottom up. So all nested updates are already + normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be + inserted at its place inside the sorted nested updates. The necessary swaps can be + expressed via 'upd_funs' by replicating the outer update at the designated position: *) + val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1 + val noops' = maps snd (Symtab.dest noops); + in + if simp orelse commuted then + SOME + (prove_unfold_defs thy upd_funs noops' [simproc] + (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) + else NONE + end; val upd_simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none)); + Simplifier.simproc_setup_global + {name = \<^binding>\update\, lhss = ["x::'a::{}"], proc = K upd_proc, passive = false}; end; @@ -1306,22 +1305,20 @@ Complexity: #components * #updates #updates *) -val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\eq\ - {lhss = [\<^term>\r = s\], - passive = false, - proc = fn _ => fn ctxt => fn ct => - (case Thm.term_of ct of - \<^Const_>\HOL.eq T for _ _\ => - (case rec_id ~1 T of - "" => NONE - | name => - (case get_equalities (Proof_Context.theory_of ctxt) name of - NONE => NONE - | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) - | _ => NONE)}); +fun eq_proc ctxt ct = + (case Thm.term_of ct of + \<^Const_>\HOL.eq T for _ _\ => + (case rec_id ~1 T of + "" => NONE + | name => + (case get_equalities (Proof_Context.theory_of ctxt) name of + NONE => NONE + | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) + | _ => NONE); val eq_simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none)); + Simplifier.simproc_setup_global + {name = \<^binding>\eq\, lhss = ["r = s"], proc = K eq_proc, passive = false}; (* split_simproc *) @@ -1360,51 +1357,47 @@ else NONE | _ => NONE)}; -val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\ex_sel_eq\ - {lhss = [\<^term>\Ex t\], - passive = false, - proc = fn _ => fn ctxt => fn ct => - let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - fun mkeq (lr, T, (sel, Tsel), x) i = - if is_selector thy sel then - let - val x' = - if not (Term.is_dependent x) - then Free ("x" ^ string_of_int i, range_type Tsel) - else raise TERM ("", [x]); - val sel' = Const (sel, Tsel) $ Bound 0; - val (l, r) = if lr then (sel', x') else (x', sel'); - in \<^Const>\HOL.eq T for l r\ end - else raise TERM ("", [Const (sel, Tsel)]); - - fun dest_sel_eq (\<^Const_>\HOL.eq T\ $ (Const (sel, Tsel) $ Bound 0) $ X) = - (true, T, (sel, Tsel), X) - | dest_sel_eq (\<^Const_>\HOL.eq T\ $ X $ (Const (sel, Tsel) $ Bound 0)) = - (false, T, (sel, Tsel), X) - | dest_sel_eq _ = raise TERM ("", []); - in - (case t of - \<^Const_>\Ex T for \Abs (s, _, t)\\ => - (let - val eq = mkeq (dest_sel_eq t) 0; - val prop = - Logic.list_all ([("r", T)], - Logic.mk_equals (\<^Const>\Ex T for \Abs (s, T, eq)\\, \<^Const>\True\)); - in - SOME (Goal.prove_sorry_global thy [] [] prop - (fn {context = ctxt', ...} => - simp_tac (put_simpset (get_simpset thy) ctxt' - addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) - end handle TERM _ => NONE) - | _ => NONE) - end}); +fun ex_sel_eq_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + fun mkeq (lr, T, (sel, Tsel), x) i = + if is_selector thy sel then + let + val x' = + if not (Term.is_dependent x) + then Free ("x" ^ string_of_int i, range_type Tsel) + else raise TERM ("", [x]); + val sel' = Const (sel, Tsel) $ Bound 0; + val (l, r) = if lr then (sel', x') else (x', sel'); + in \<^Const>\HOL.eq T for l r\ end + else raise TERM ("", [Const (sel, Tsel)]); + + fun dest_sel_eq (\<^Const_>\HOL.eq T\ $ (Const (sel, Tsel) $ Bound 0) $ X) = + (true, T, (sel, Tsel), X) + | dest_sel_eq (\<^Const_>\HOL.eq T\ $ X $ (Const (sel, Tsel) $ Bound 0)) = + (false, T, (sel, Tsel), X) + | dest_sel_eq _ = raise TERM ("", []); + in + (case t of + \<^Const_>\Ex T for \Abs (s, _, t)\\ => + (let + val eq = mkeq (dest_sel_eq t) 0; + val prop = + Logic.list_all ([("r", T)], + Logic.mk_equals (\<^Const>\Ex T for \Abs (s, T, eq)\\, \<^Const>\True\)); + in + SOME (Goal.prove_sorry_global thy [] [] prop + (fn {context = ctxt', ...} => + simp_tac (put_simpset (get_simpset thy) ctxt' + addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) + end handle TERM _ => NONE) + | _ => NONE) + end; 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])); + Simplifier.simproc_setup_global + {name = \<^binding>\ex_sel_eq\, lhss = ["Ex t"], proc = K ex_sel_eq_proc, passive = true}; (* split_simp_tac *) diff -r f7e972d567f3 -r f34926a91fea src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Oct 18 15:13:52 2023 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Wed Oct 18 16:29:24 2023 +0200 @@ -17,8 +17,7 @@ val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory val oracle: bstring * Position.range -> Input.source -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory - val simproc_setup: string * Position.T -> string list -> Input.source -> bool -> - local_theory -> local_theory + val simproc_setup: Input.source Simplifier.simproc_setup -> local_theory -> local_theory val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition val terminal_proof: Method.text_range * Method.text_range option -> Toplevel.transition -> Toplevel.transition @@ -137,14 +136,10 @@ (* simprocs *) -fun simproc_setup name lhss source passive = - ML_Context.expression (Input.pos_of source) - (ML_Lex.read - ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^ - ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^ - ", passive = " ^ Bool.toString passive ^ - ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})") - |> Context.proof_map; +fun simproc_setup arg = + Context.proof_map + (ML_Context.expression (Input.pos_of (#proc arg)) + (ML_Lex.read "Simplifier.simproc_setup_local " @ Simplifier.simproc_setup_ml arg)); (* local endings *) diff -r f7e972d567f3 -r f34926a91fea src/Pure/Pure.thy --- a/src/Pure/Pure.thy Wed Oct 18 15:13:52 2023 +0200 +++ b/src/Pure/Pure.thy Wed Oct 18 16:29:24 2023 +0200 @@ -333,11 +333,12 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" - (Parse.name_position -- + (Parse.binding -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\) -- (\<^keyword>\=\ |-- Parse.ML_source) -- Parse.opt_keyword "passive" - >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d)); + >> (fn (((name, lhss), proc), passive) => + Isar_Cmd.simproc_setup {name = name, lhss = lhss, passive = passive, proc = proc})); in end\ diff -r f7e972d567f3 -r f34926a91fea src/Pure/ex/Def.thy --- a/src/Pure/ex/Def.thy Wed Oct 18 15:13:52 2023 +0200 +++ b/src/Pure/ex/Def.thy Wed Oct 18 16:29:24 2023 +0200 @@ -66,9 +66,8 @@ (* simproc setup *) val _ = - Named_Target.global_setup - (Simplifier.define_simproc \<^binding>\expand_def\ - {lhss = [Free ("x", TFree ("'a", []))], passive = false, proc = K get_def}); + Simplifier.simproc_setup_global + {name = \<^binding>\expand_def\, lhss = ["x::'a"], passive = false, proc = K get_def}; (* Isar command *) diff -r f7e972d567f3 -r f34926a91fea src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Oct 18 15:13:52 2023 +0200 +++ b/src/Pure/simplifier.ML Wed Oct 18 16:29:24 2023 +0200 @@ -41,8 +41,14 @@ {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc type 'a simproc_spec = {lhss: 'a list, passive: bool, proc: morphism -> Proof.context -> cterm -> thm option} - val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory - val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory + 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 = {name: binding, lhss: string list, passive: bool, proc: 'a} + val simproc_setup_local: + (morphism -> Proof.context -> cterm -> thm option) simproc_setup -> simproc + val simproc_setup_global: + (morphism -> Proof.context -> cterm -> thm option) simproc_setup -> simproc + val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list val pretty_simpset: bool -> Proof.context -> Pretty.T val default_mk_sym: Proof.context -> thm -> thm option val prems_of: Proof.context -> thm list @@ -153,6 +159,7 @@ |> Simprocs.map (#2 o Name_Space.define context true (b', simproc')) |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc']) end) + |> pair simproc0 end; in @@ -163,6 +170,27 @@ end; +(* implicit simproc_setup *) + +type 'a simproc_setup = {name: binding, lhss: string list, passive: bool, proc: 'a}; + +fun simproc_setup_local {name, lhss, passive, proc} = + Theory.local_setup_result + (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc}); + +fun simproc_setup_global {name, lhss, passive, proc} = + Named_Target.global_setup_result Raw_Simplifier.transform_simproc + (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc}); + +fun simproc_setup_ml {name, lhss, passive, proc} = + ML_Lex.read + ("{name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^ + ", lhss = " ^ ML_Syntax.print_strings lhss ^ + ", passive = " ^ Bool.toString passive ^ + ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}"; + + + (** congruence rule to protect foundational terms of local definitions **) local