--- a/NEWS Wed Oct 02 20:49:44 2024 +0200
+++ b/NEWS Wed Oct 02 22:08:52 2024 +0200
@@ -9,6 +9,10 @@
*** General ***
+* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
+so its declarations are applied immediately, but also named for later
+re-use.
+
* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
--- a/src/Doc/Isar_Ref/Spec.thy Wed Oct 02 20:49:44 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Oct 02 22:08:52 2024 +0200
@@ -231,7 +231,7 @@
(\secref{sec:locale}).
\<^rail>\<open>
- @@{command bundle} @{syntax name}
+ (@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline>
( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
;
@@{command print_bundles} ('!'?)
@@ -258,6 +258,9 @@
b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
bindings are not recorded in the bundle.
+ \<^descr> \<^theory_text>\<open>open_bundle b\<close> is like \<^theory_text>\<open>bundle b\<close> followed by \<^theory_text>\<open>unbundle b\<close>, so its
+ declarations are applied immediately, but also named for later re-use.
+
\<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
current context; the ``\<open>!\<close>'' option indicates extra verbosity.
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Oct 02 22:08:52 2024 +0200
@@ -20,7 +20,7 @@
declare vec_lambda_inject [simplified, simp]
-bundle vec_syntax
+open_bundle vec_syntax
begin
notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
@@ -30,8 +30,6 @@
no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
-unbundle vec_syntax
-
text \<open>
Concrete syntax for \<open>('a, 'b) vec\<close>:
\<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
--- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 22:08:52 2024 +0200
@@ -12,17 +12,16 @@
definition\<^marker>\<open>tag important\<close> lipschitz_on
where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
-bundle lipschitz_syntax
+open_bundle lipschitz_syntax
begin
notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
+
bundle no_lipschitz_syntax
begin
no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
-unbundle lipschitz_syntax
-
lemma lipschitz_onI: "L-lipschitz_on X f"
if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L"
using that by (auto simp: lipschitz_on_def)
--- a/src/HOL/Combinatorics/Perm.thy Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy Wed Oct 02 22:08:52 2024 +0200
@@ -792,7 +792,7 @@
subsection \<open>Syntax\<close>
-bundle no_permutation_syntax
+open_bundle no_permutation_syntax
begin
no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
@@ -806,6 +806,4 @@
notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
end
-unbundle no_permutation_syntax
-
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Oct 02 22:08:52 2024 +0200
@@ -245,7 +245,7 @@
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
- |> Bundle.bundle ((binding, [restore_lifting_att])) []
+ |> Bundle.bundle {open_bundle = false} ((binding, [restore_lifting_att])) []
|> pair binding
end
--- a/src/Pure/Isar/bundle.ML Wed Oct 02 20:49:44 2024 +0200
+++ b/src/Pure/Isar/bundle.ML Wed Oct 02 22:08:52 2024 +0200
@@ -21,11 +21,11 @@
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: name list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
- val bundle: binding * Attrib.thms ->
+ val bundle: {open_bundle: bool} -> binding * Attrib.thms ->
(binding * typ option * mixfix) list -> local_theory -> local_theory
- val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
+ val bundle_cmd: {open_bundle: bool} -> binding * (Facts.ref * Token.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
- val init: binding -> theory -> local_theory
+ val init: {open_bundle: bool} -> binding -> theory -> local_theory
end;
structure Bundle: BUNDLE =
@@ -53,6 +53,7 @@
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
+val get_global = Name_Space.get o get_all_generic o Context.Theory;
val get = Name_Space.get o get_all_generic o Context.Proof;
fun read ctxt = get ctxt o check ctxt;
@@ -164,7 +165,7 @@
local
-fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes {open_bundle} (binding, raw_bundle) raw_fixes lthy =
let
val (_, ctxt') = add_fixes raw_fixes lthy;
val bundle0 = raw_bundle
@@ -179,6 +180,7 @@
(fn phi => fn context =>
let val psi = Morphism.set_trim_context'' context phi
in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
+ |> open_bundle ? apply_bundle true bundle
end;
in
@@ -195,22 +197,29 @@
fun bad_operation _ = error "Not possible in bundle target";
-fun conclude invisible binding =
+fun conclude {open_bundle, invisible} binding =
Local_Theory.background_theory_result (fn thy =>
- thy
- |> invisible ? Context_Position.set_visible_global false
- |> Context.Theory
- |> define_bundle (binding, the_target thy)
- ||> (Context.the_theory
- #> invisible ? Context_Position.restore_visible_global thy
- #> reset_target));
+ let
+ val (name, thy') = thy
+ |> invisible ? Context_Position.set_visible_global false
+ |> Context.Theory
+ |> define_bundle (binding, the_target thy)
+ ||> Context.the_theory;
+ val bundle = get_global thy' name;
+ val thy'' = thy'
+ |> open_bundle ?
+ (Context_Position.set_visible_global false #>
+ Attrib.global_notes "" [(Binding.empty_atts, bundle)] #> snd)
+ |> Context_Position.restore_visible_global thy
+ |> reset_target;
+ in (name, thy'') end);
fun pretty binding lthy =
let
val bundle = the_target (Proof_Context.theory_of lthy);
val (name, lthy') = lthy
|> Local_Theory.raw_theory (Context_Position.set_visible_global false)
- |> conclude true binding;
+ |> conclude {open_bundle = false, invisible = true} binding;
val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
val markup_name =
Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name;
@@ -235,12 +244,12 @@
in
-fun init binding thy =
+fun init {open_bundle} binding thy =
thy
|> Local_Theory.init
{background_naming = Sign.naming_of thy,
setup = set_target [] #> Proof_Context.init_global,
- conclude = conclude false binding #> #2}
+ conclude = conclude {open_bundle = open_bundle, invisible = false} binding #> #2}
{define = bad_operation,
notes = bundle_notes,
abbrev = bad_operation,
--- a/src/Pure/Pure.thy Wed Oct 02 20:49:44 2024 +0200
+++ b/src/Pure/Pure.thy Wed Oct 02 22:08:52 2024 +0200
@@ -37,7 +37,7 @@
"declaration" "syntax_declaration"
"parse_ast_translation" "parse_translation" "print_translation"
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
- and "bundle" :: thy_decl_block
+ and "bundle" "open_bundle" :: thy_decl_block
and "unbundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
@@ -637,26 +637,34 @@
ML \<open>
local
+fun bundle_cmd open_bundle =
+ (Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
+ >> (uncurry (Bundle.bundle_cmd {open_bundle = open_bundle}));
+
+fun bundle_begin open_bundle =
+ Parse.binding --| Parse.begin >> Bundle.init {open_bundle = open_bundle};
+
val _ =
Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
- "define bundle of declarations"
- ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
- >> (uncurry Bundle.bundle_cmd))
- (Parse.binding --| Parse.begin >> Bundle.init);
+ "define bundle of declarations" (bundle_cmd false) (bundle_begin false);
+
+val _ =
+ Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>open_bundle\<close>
+ "define and open bundle of declarations" (bundle_cmd true) (bundle_begin true);
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
- "activate declarations from bundle in local theory"
+ "open bundle in local theory"
(Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>include\<close>
- "activate declarations from bundle in proof body"
+ "open bundle in proof body"
(Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>including\<close>
- "activate declarations from bundle in goal refinement"
+ "open bundle in goal refinement"
(Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
val _ =