# HG changeset patch # User wenzelm # Date 1697634832 -7200 # Node ID f7e972d567f3a5fd857ec605a2260bc80fb07929 # Parent c74fd21af246438eb21ce293b9486ffdff17cbfd clarified signature: more concise variations on implicit theory setup; diff -r c74fd21af246 -r f7e972d567f3 src/Doc/Codegen/Computations.thy --- a/src/Doc/Codegen/Computations.thy Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Doc/Codegen/Computations.thy Wed Oct 18 15:13:52 2023 +0200 @@ -276,8 +276,7 @@ \<^instantiate>\x = ct and y = \if b then \<^cterm>\True\ else \<^cterm>\False\\ in cterm \x \ y\ for x y :: bool\; - val (_, dvd_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\dvd\, raw_dvd))); + val (_, dvd_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\dvd\, raw_dvd)); in diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Oct 18 15:13:52 2023 +0200 @@ -663,8 +663,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: pol\; -val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\pnsubstl\, pol))); +val (_, raw_pol_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\pnsubstl\, pol)); fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Decision_Procs/Reflective_Field.thy --- a/src/HOL/Decision_Procs/Reflective_Field.thy Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Decision_Procs/Reflective_Field.thy Wed Oct 18 15:13:52 2023 +0200 @@ -643,8 +643,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: \pexpr \ pexpr \ pexpr list\\; -val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\fnorm\, fnorm))); +val (_, raw_fnorm_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\fnorm\, fnorm)); fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Wed Oct 18 15:13:52 2023 +0200 @@ -339,8 +339,8 @@ fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) -val (_, export_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => +val (_, export_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => let val shyptab = add_shyps shyps Sorttab.empty fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab @@ -355,7 +355,7 @@ else () in Thm.global_cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) - end))); + end)); fun export_thm thy hyps shyps prop = let diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Wed Oct 18 15:13:52 2023 +0200 @@ -194,8 +194,8 @@ set_inducts = []}} end; -val _ = Theory.setup (Named_Target.theory_map (fn lthy => +val _ = Named_Target.global_setup (fn lthy => fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy)) - [fp_sugar_of_sum, fp_sugar_of_prod] lthy)); + [fp_sugar_of_sum, fp_sugar_of_prod] lthy); end; diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 18 15:13:52 2023 +0200 @@ -697,11 +697,11 @@ end; -val (_, oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\cooper\, +val (_, oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\cooper\, (fn (ctxt, t) => (Thm.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop) - (t, procedure t))))); + (t, procedure t)))); val comp_ss = simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm}); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Tools/record.ML Wed Oct 18 15:13:52 2023 +0200 @@ -1060,7 +1060,7 @@ - If X is a more-selector we have to make sure that S is not in the updated subrecord. *) -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\select_update\ +val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\select_update\ {lhss = [\<^term>\x::'a::{}\], passive = false, proc = fn _ => fn ctxt => fn ct => @@ -1115,7 +1115,7 @@ end else NONE | _ => NONE) - end})); + end}); val simproc = #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none)); @@ -1165,7 +1165,7 @@ 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 _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\update\ +val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\update\ {lhss = [\<^term>\x::'a::{}\], passive = false, proc = fn _ => fn ctxt => fn ct => @@ -1283,7 +1283,7 @@ (prove_unfold_defs thy upd_funs noops' [simproc] (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE - end})); + end}); val upd_simproc = #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none)); @@ -1306,7 +1306,7 @@ Complexity: #components * #updates #updates *) -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\eq\ +val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\eq\ {lhss = [\<^term>\r = s\], passive = false, proc = fn _ => fn ctxt => fn ct => @@ -1318,7 +1318,7 @@ (case get_equalities (Proof_Context.theory_of ctxt) name of NONE => NONE | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) - | _ => NONE)})); + | _ => NONE)}); val eq_simproc = #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none)); @@ -1360,7 +1360,7 @@ else NONE | _ => NONE)}; -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\ex_sel_eq\ +val _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\ex_sel_eq\ {lhss = [\<^term>\Ex t\], passive = false, proc = fn _ => fn ctxt => fn ct => @@ -1399,7 +1399,7 @@ addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) end handle TERM _ => NONE) | _ => NONE) - end})); + end}); val ex_sel_eq_simproc = #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none)); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Types_To_Sets/local_typedef.ML --- a/src/HOL/Types_To_Sets/local_typedef.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Types_To_Sets/local_typedef.ML Wed Oct 18 15:13:52 2023 +0200 @@ -70,8 +70,9 @@ (** END OF THE CRITICAL CODE **) -val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\cancel_type_definition\, cancel_type_definition_cterm))); +val (_, cancel_type_definition_oracle) = + Theory.setup_result + (Thm.add_oracle (\<^binding>\cancel_type_definition\, cancel_type_definition_cterm)); fun cancel_type_definition thm = Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm)); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/Types_To_Sets/unoverloading.ML --- a/src/HOL/Types_To_Sets/unoverloading.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/Types_To_Sets/unoverloading.ML Wed Oct 18 15:13:52 2023 +0200 @@ -119,9 +119,9 @@ (** END OF THE CRITICAL CODE **) -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\unoverload\, - fn (const, thm) => unoverload_impl const thm))); +val (_, unoverload_oracle) = + Theory.setup_result + (Thm.add_oracle (\<^binding>\unoverload\, fn (const, thm) => unoverload_impl const thm)); fun unoverload const thm = unoverload_oracle (const, thm); diff -r c74fd21af246 -r f7e972d567f3 src/HOL/ex/Sorting_Algorithms_Examples.thy --- a/src/HOL/ex/Sorting_Algorithms_Examples.thy Tue Oct 17 22:29:12 2023 +0200 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Wed Oct 18 15:13:52 2023 +0200 @@ -27,8 +27,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt (term_of_int_list ks)\ in cterm \x \ y\ for x y :: \int list\\; - val (_, sort_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\sort\, raw_sort))); + val (_, sort_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\sort\, raw_sort)); in diff -r c74fd21af246 -r f7e972d567f3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Wed Oct 18 15:13:52 2023 +0200 @@ -117,10 +117,9 @@ (ML_Lex.read "val " @ ML_Lex.read_range range name @ ML_Lex.read - (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^ + (" = snd (Theory.setup_result (Thm.add_oracle (" ^ ML_Syntax.make_binding (name, #1 range) ^ ", ") @ - ML_Lex.read_source source @ - ML_Lex.read "))))") + ML_Lex.read_source source @ ML_Lex.read ")))") |> Context.theory_map; diff -r c74fd21af246 -r f7e972d567f3 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/Isar/named_target.ML Wed Oct 18 15:13:52 2023 +0200 @@ -16,6 +16,9 @@ val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory + val global_setup: (local_theory -> local_theory) -> unit + val global_setup_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 'b + val global_setup_result0: (local_theory -> 'a * local_theory) -> 'a val revoke_reinitializability: local_theory -> local_theory val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory end; @@ -139,8 +142,11 @@ val theory_init = init [] ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; +fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; -fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; +val global_setup = Theory.setup o theory_map; +fun global_setup_result f g = Theory.setup_result (theory_map_result f g); +fun global_setup_result0 g = global_setup_result (K I) g; val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); diff -r c74fd21af246 -r f7e972d567f3 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/ML/ml_thms.ML Wed Oct 18 15:13:52 2023 +0200 @@ -122,8 +122,7 @@ fun ml_store get (name, ths) = let val (_, ths') = - Context.>>> (Context.map_theory_result - (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); + Theory.setup_result (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])); val _ = Theory.setup (Data.put ths'); val _ = if name = "" then () diff -r c74fd21af246 -r f7e972d567f3 src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/Tools/plugin.ML Wed Oct 18 15:13:52 2023 +0200 @@ -57,13 +57,13 @@ val thy' = Data.put data' thy; in (name, thy') end; -fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs)); +fun define_setup binding rhs = Theory.setup_result (define binding rhs); (* immediate entries *) fun declare binding thy = define binding [] thy; -fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding)); +fun declare_setup binding = Theory.setup_result (declare binding); (* filter *) diff -r c74fd21af246 -r f7e972d567f3 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/drule.ML Wed Oct 18 15:13:52 2023 +0200 @@ -337,10 +337,10 @@ val read_prop = certify o Simple_Syntax.read_prop; fun store_thm name th = - Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); + Theory.setup_result (Global_Theory.store_thm (name, th)); fun store_thm_open name th = - Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); + Theory.setup_result (Global_Theory.store_thm_open (name, th)); fun store_standard_thm name th = store_thm name (export_without_context th); fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th); diff -r c74fd21af246 -r f7e972d567f3 src/Pure/ex/Def.thy --- a/src/Pure/ex/Def.thy Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/ex/Def.thy Wed Oct 18 15:13:52 2023 +0200 @@ -66,7 +66,7 @@ (* simproc setup *) val _ = - (Theory.setup o Named_Target.theory_map) + Named_Target.global_setup (Simplifier.define_simproc \<^binding>\expand_def\ {lhss = [Free ("x", TFree ("'a", []))], passive = false, proc = K get_def}); diff -r c74fd21af246 -r f7e972d567f3 src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/skip_proof.ML Wed Oct 18 15:13:52 2023 +0200 @@ -26,8 +26,7 @@ (* oracle setup *) val (_, make_thm_cterm) = - Context.>>> - (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I))); + Theory.setup_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)); fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop); diff -r c74fd21af246 -r f7e972d567f3 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Pure/theory.ML Wed Oct 18 15:13:52 2023 +0200 @@ -10,7 +10,9 @@ val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit + val setup_result: (theory -> 'a * theory) -> 'a val local_setup: (Proof.context -> Proof.context) -> unit + val local_setup_result: (Proof.context -> 'a * Proof.context) -> 'a val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory @@ -49,7 +51,10 @@ fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); +fun setup_result f = Context.>>> (Context.map_theory_result f); + fun local_setup f = Context.>> (Context.map_proof f); +fun local_setup_result f = Context.>>> (Context.map_proof_result f); (* implicit theory Pure *) diff -r c74fd21af246 -r f7e972d567f3 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Tools/Code/code_runtime.ML Wed Oct 18 15:13:52 2023 +0200 @@ -152,9 +152,9 @@ Thm.mk_binop iff ct (if result then \<^cprop>\PROP Code_Generator.holds\ else ct) end; -val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\holds_by_evaluation\, - fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); +val (_, raw_check_holds_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\holds_by_evaluation\, + fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)); fun check_holds_oracle ctxt evaluator vs_ty_t ct = raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); @@ -417,8 +417,7 @@ fun holds ct = Thm.mk_binop \<^cterm>\Pure.eq :: prop \ prop \ prop\ ct \<^cprop>\PROP Code_Generator.holds\; -val (_, holds_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\holds\, holds))); +val (_, holds_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\holds\, holds)); in diff -r c74fd21af246 -r f7e972d567f3 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Oct 17 22:29:12 2023 +0200 +++ b/src/Tools/nbe.ML Wed Oct 18 15:13:52 2023 +0200 @@ -78,9 +78,9 @@ val get_triv_classes = map fst o Triv_Class_Data.get; -val (_, triv_of_class) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\triv_of_class\, fn (thy, T, class) => - Thm.global_cterm_of thy (Logic.mk_of_class (T, class))))); +val (_, triv_of_class) = + Theory.setup_result (Thm.add_oracle (\<^binding>\triv_of_class\, + fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class)))); in @@ -592,10 +592,10 @@ val rhs = Thm.cterm_of ctxt raw_rhs; in Thm.mk_binop eq lhs rhs end; -val (_, raw_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, +val (_, raw_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => - mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)))); + mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))); fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);