# HG changeset patch
# User wenzelm
# Date 1727899732 -7200
# Node ID 849efff7de153cc3d8fd483d047b179367ecdad7
# Parent  f14fcf94e0e90829f5a0b447615766039cb51193
provide 'open_bundle' command;

diff -r f14fcf94e0e9 -r 849efff7de15 NEWS
--- 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
diff -r f14fcf94e0e9 -r 849efff7de15 src/Doc/Isar_Ref/Spec.thy
--- 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.
 
diff -r f14fcf94e0e9 -r 849efff7de15 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- 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>
diff -r f14fcf94e0e9 -r 849efff7de15 src/HOL/Analysis/Lipschitz.thy
--- 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)
diff -r f14fcf94e0e9 -r 849efff7de15 src/HOL/Combinatorics/Perm.thy
--- 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
diff -r f14fcf94e0e9 -r 849efff7de15 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
 
diff -r f14fcf94e0e9 -r 849efff7de15 src/Pure/Isar/bundle.ML
--- 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,
diff -r f14fcf94e0e9 -r 849efff7de15 src/Pure/Pure.thy
--- 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 _ =