--- a/NEWS Fri Oct 04 13:22:35 2024 +0200
+++ b/NEWS Fri Oct 04 13:29:33 2024 +0200
@@ -13,6 +13,9 @@
so its declarations are applied immediately, but also named for later
re-use.
+* The syntax of opnening bundles has changed slightly: multiple bundles
+need to be separated by the keyword 'and'. Minor INCOMPATIBILITY.
+
* 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 Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Oct 04 13:29:33 2024 +0200
@@ -211,10 +211,12 @@
\begin{matharray}{rcl}
@{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
+ @{command_def "unbundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@{keyword_def "includes"} & : & syntax \\
+ @{keyword_def "opening"} & : & syntax \\
\end{matharray}
The outer syntax of fact expressions (\secref{sec:syn-att}) involves
@@ -234,15 +236,17 @@
(@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline>
( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
;
+ @@{command unbundle} @{syntax bundles}
+ ;
@@{command print_bundles} ('!'?)
;
- (@@{command include} | @@{command including}) (@{syntax name}+)
+ (@@{command include} | @@{command including}) @{syntax bundles}
;
- @{syntax_def "includes"}: @'includes' (@{syntax name}+)
+ @{syntax_def "includes"}: @'includes' @{syntax bundles}
;
- @{syntax_def "opening"}: @'opening' (@{syntax name}+)
+ @{syntax_def "opening"}: @'opening' @{syntax bundles}
;
- @@{command unbundle} (@{syntax name}+)
+ @{syntax bundles}: @{syntax name} + @'and'
\<close>
\<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -259,32 +263,31 @@
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.
+ declarations are activated immediately, but also named for later re-use.
+
+ \<^descr> \<^theory_text>\<open>unbundle \<^vec>b\<close> activates the declarations from the given bundles in
+ the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
+ (\secref{sec:theorems}) with the expanded bundles.
\<^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.
- \<^descr> \<^theory_text>\<open>include b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles
- in a proof body (forward mode). This is analogous to \<^theory_text>\<open>note\<close>
+ \<^descr> \<^theory_text>\<open>include \<^vec>b\<close> activates the declarations from the given bundles in a
+ proof body (forward mode). This is analogous to \<^theory_text>\<open>note\<close>
+ (\secref{sec:proof-facts}) with the expanded bundles.
+
+ \<^descr> \<^theory_text>\<open>including \<^vec>b\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof
+ refinement (backward mode). This is analogous to \<^theory_text>\<open>using\<close>
(\secref{sec:proof-facts}) with the expanded bundles.
- \<^descr> \<^theory_text>\<open>including b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement
- (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})
- with the expanded bundles.
-
- \<^descr> \<^theory_text>\<open>includes b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but applies to a
- confined specification context: unnamed \<^theory_text>\<open>context\<close>s and
- long statements of \<^theory_text>\<open>theorem\<close>.
+ \<^descr> \<^theory_text>\<open>includes \<^vec>b\<close> is similar to \<^theory_text>\<open>include\<close>, but applies to a confined
+ specification context: unnamed \<^theory_text>\<open>context\<close>s and long statements of
+ \<^theory_text>\<open>theorem\<close>.
- \<^descr> \<^theory_text>\<open>opening b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>includes\<close>, but applies to
- a named specification context: \<^theory_text>\<open>locale\<close>s, \<^theory_text>\<open>class\<close>es and
- named \<^theory_text>\<open>context\<close>s. The effect is confined to the surface context within the
- specification block itself and the corresponding \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.
-
- \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in
- the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
- (\secref{sec:theorems}) with the expanded bundles.
-
+ \<^descr> \<^theory_text>\<open>opening \<^vec>b\<close> is similar to \<^theory_text>\<open>includes\<close>, but applies to a named
+ specification context: \<^theory_text>\<open>locale\<close>s, \<^theory_text>\<open>class\<close>es and named \<^theory_text>\<open>context\<close>s. The
+ effect is confined to the surface context within the specification block
+ itself and the corresponding \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.
Here is an artificial example of bundling various configuration options:
\<close>
--- a/src/HOL/Library/Code_Target_Int.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy Fri Oct 04 13:29:33 2024 +0200
@@ -160,7 +160,7 @@
by transfer (simp add: fun_eq_iff)
context
- includes integer.lifting bit_operations_syntax
+ includes integer.lifting and bit_operations_syntax
begin
declare [[code drop: \<open>bit :: int \<Rightarrow> _\<close> \<open>not :: int \<Rightarrow> _\<close>
--- a/src/HOL/Library/Code_Target_Nat.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Fri Oct 04 13:29:33 2024 +0200
@@ -11,7 +11,7 @@
subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close>
context
-includes natural.lifting integer.lifting
+includes natural.lifting and integer.lifting
begin
lift_definition Nat :: "integer \<Rightarrow> nat"
--- a/src/HOL/Library/DAList.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/DAList.thy Fri Oct 04 13:29:33 2024 +0200
@@ -129,7 +129,7 @@
subsection \<open>Quickcheck generators\<close>
context
- includes state_combinator_syntax term_syntax
+ includes state_combinator_syntax and term_syntax
begin
definition
--- a/src/HOL/Library/Disjoint_FSets.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Disjoint_FSets.thy Fri Oct 04 13:29:33 2024 +0200
@@ -62,7 +62,7 @@
(* FIXME should be provable without lifting *)
lemma fmadd_disjnt: "fdisjnt (fmdom m) (fmdom n) \<Longrightarrow> m ++\<^sub>f n = n ++\<^sub>f m"
unfolding fdisjnt_alt_def
-including fset.lifting fmap.lifting
+including fset.lifting and fmap.lifting
apply transfer
apply (rule ext)
apply (auto simp: map_add_def split: option.splits)
--- a/src/HOL/Library/Finite_Map.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Finite_Map.thy Fri Oct 04 13:29:33 2024 +0200
@@ -1188,7 +1188,7 @@
lemma fmap_exhaust[cases type: fmap]:
obtains (fmempty) "m = fmempty"
| (fmupd) x y m' where "m = fmupd x y m'" "x |\<notin>| fmdom m'"
-using that including fmap.lifting fset.lifting
+using that including fmap.lifting and fset.lifting
proof transfer
fix m P
assume "finite (dom m)"
--- a/src/HOL/Probability/PMF_Impl.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy Fri Oct 04 13:29:33 2024 +0200
@@ -534,7 +534,7 @@
begin
context
- includes state_combinator_syntax term_syntax
+ includes state_combinator_syntax and term_syntax
begin
definition
--- a/src/HOL/String.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/String.thy Fri Oct 04 13:29:33 2024 +0200
@@ -180,7 +180,7 @@
by (auto simp add: UNIV_char_of_nat card_image)
context
- includes lifting_syntax integer.lifting natural.lifting
+ includes lifting_syntax and integer.lifting and natural.lifting
begin
lemma [transfer_rule]:
--- a/src/Pure/Isar/parse_spec.ML Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Isar/parse_spec.ML Fri Oct 04 13:29:33 2024 +0200
@@ -17,6 +17,7 @@
val specification:
((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
val constdecl: (binding * string option * mixfix) parser
+ val bundles: (xstring * Position.T) list parser
val includes: (xstring * Position.T) list parser
val opening: (xstring * Position.T) list parser
val locale_fixes: (binding * string option * mixfix) list parser
@@ -81,11 +82,16 @@
>> Scan.triple2;
-(* locale and context elements *)
+(* bundles *)
+
+val bundles = Parse.and_list1 Parse.name_position;
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val includes = Parse.$$$ "includes" |-- Parse.!!! bundles;
-val opening = Parse.$$$ "opening" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val opening = Parse.$$$ "opening" |-- Parse.!!! bundles;
+
+
+(* locale and context elements *)
val locale_fixes =
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
--- a/src/Pure/Pure.thy Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Pure.thy Fri Oct 04 13:29:33 2024 +0200
@@ -654,18 +654,15 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
- "open bundle in local theory"
- (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
+ "open bundle in local theory" (Parse_Spec.bundles >> Bundle.unbundle_cmd);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>include\<close>
- "open bundle in proof body"
- (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
+ "open bundle in proof body" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>including\<close>
- "open bundle in goal refinement"
- (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
+ "open bundle in goal refinement" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.including_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>