# HG changeset patch
# User haftmann
# Date 1606459715 0
# Node ID e7c2848b78e80d20c98caa6d80698dd48a336d13
# Parent  a4d7da18ac5cd8172f7fb62f392d6ee604fcdaa5
refined syntax for bundle mixins for locale and class specifications

diff -r a4d7da18ac5c -r e7c2848b78e8 NEWS
--- a/NEWS	Thu Nov 26 23:23:19 2020 +0100
+++ b/NEWS	Fri Nov 27 06:48:35 2020 +0000
@@ -57,6 +57,12 @@
 * Session Pure-Examples contains notable examples for Isabelle/Pure
 (former entries of HOL-Isar_Examples).
 
+* Named contexts (locale and class specifications, locale and class
+context blocks) allow bundle mixins for the surface context.  This
+allows syntax notations to be organized within bundles conveniently.
+See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples
+and the Isar reference manual for syntx descriptions.
+
 * Definitions in locales produce rule which can be added as congruence
 rule to protect foundational terms during simplification.
 
diff -r a4d7da18ac5c -r e7c2848b78e8 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Nov 27 06:48:35 2020 +0000
@@ -139,17 +139,19 @@
   \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.
 
   \<^rail>\<open>
-    @@{command context} @{syntax name} @'begin'
+    @@{command context} @{syntax name} @{syntax_ref "opening"}? @'begin'
     ;
     @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
     ;
     @{syntax_def target}: '(' @'in' @{syntax name} ')'
   \<close>
 
-  \<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing
+  \<^descr> \<^theory_text>\<open>context c bundles begin\<close> opens a named context, by recommencing an existing
   locale or class \<open>c\<close>. Note that locale and class definitions allow to include
   the \<^theory_text>\<open>begin\<close> keyword as well, in order to continue the local theory
-  immediately after the initial specification.
+  immediately after the initial specification.  Optionally given
+  \<open>bundles\<close> only take effect in the surface context within the \<^theory_text>\<open>begin\<close> /
+  \<^theory_text>\<open>end\<close> block.
 
   \<^descr> \<^theory_text>\<open>context bundles elements begin\<close> opens an unnamed context, by extending
   the enclosing global or local theory target by the given declaration bundles
@@ -237,6 +239,10 @@
     (@@{command include} | @@{command including}) (@{syntax name}+)
     ;
     @{syntax_def "includes"}: @'includes' (@{syntax name}+)
+    ;
+    @{syntax_def "opening"}: @'opening' (@{syntax name}+)
+    ;
+    @@{command unbundle} (@{syntax name}+)
   \<close>
 
   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -255,22 +261,27 @@
   \<^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>
+  (\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>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>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works 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\<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 works in situations
-  where a specification context is constructed, notably for \<^theory_text>\<open>context\<close> and
-  long statements of \<^theory_text>\<open>theorem\<close> etc.
-
 
   Here is an artificial example of bundling various configuration options:
 \<close>
@@ -524,7 +535,8 @@
     @@{command print_locales} ('!'?)
     ;
     @{syntax_def locale}: @{syntax context_elem}+ |
-      @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
+      @{syntax_ref "opening"} ('+' (@{syntax context_elem}+))? |
+      @{syntax locale_expr} @{syntax_ref "opening"}? ('+' (@{syntax context_elem}+))?
     ;
     @{syntax_def context_elem}:
       @'fixes' @{syntax vars} |
@@ -534,9 +546,11 @@
       @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
   \<close>
 
-  \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
+  \<^descr> \<^theory_text>\<open>locale loc = import bundles + body\<close> defines a new locale \<open>loc\<close> as a context
   consisting of a certain view of existing locales (\<open>import\<close>) plus some
-  additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional; the
+  additional elements (\<open>body\<close>);  given \<open>bundles\<close> take effect in the surface
+  context within both \<open>import\<close> and \<open>body\<close> and the potentially following
+  \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.  Each part is optional; the
   degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be
   useful to collect declarations of facts later on. Type-inference on locale
   expressions automatically takes care of the most general typing that the
@@ -816,8 +830,9 @@
     @@{command class} class_spec @'begin'?
     ;
     class_spec: @{syntax name} '='
-      ((@{syntax name} '+' (@{syntax context_elem}+)) |
-        @{syntax name} | (@{syntax context_elem}+))
+      ((@{syntax name} @{syntax_ref "opening"}? '+' (@{syntax context_elem}+)) |
+        @{syntax name} @{syntax_ref "opening"}? |
+        @{syntax_ref "opening"}? '+' (@{syntax context_elem}+))
     ;
     @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
     ;
@@ -831,7 +846,7 @@
     class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
   \<close>
 
-  \<^descr> \<^theory_text>\<open>class c = superclasses + body\<close> defines a new class \<open>c\<close>, inheriting from
+  \<^descr> \<^theory_text>\<open>class c = superclasses bundles + body\<close> defines a new class \<open>c\<close>, inheriting from
   \<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales
   \<open>superclasses\<close>.
 
@@ -846,6 +861,9 @@
   @{method intro_classes} method takes care of the details of class membership
   proofs.
 
+  Optionally given \<open>bundles\<close> take effect in the surface context within the
+  \<open>body\<close> and the potentially following \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.
+
   \<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> opens a target (cf.\
   \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close>
   corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
diff -r a4d7da18ac5c -r e7c2848b78e8 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/HOL/Product_Type.thy	Fri Nov 27 06:48:35 2020 +0000
@@ -814,9 +814,6 @@
 code_printing
   constant scomp \<rightharpoonup> (Eval) infixl 3 "#->"
 
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
 text \<open>
   \<^term>\<open>map_prod\<close> --- action of the product functor upon functions.
 \<close>
diff -r a4d7da18ac5c -r e7c2848b78e8 src/HOL/ex/Specifications_with_bundle_mixins.thy
--- a/src/HOL/ex/Specifications_with_bundle_mixins.thy	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy	Fri Nov 27 06:48:35 2020 +0000
@@ -2,8 +2,7 @@
   imports "HOL-Library.Perm"
 begin
 
-locale involutory =
-  includes permutation_syntax
+locale involutory = opening permutation_syntax +
   fixes f :: \<open>'a perm\<close>
   assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close>
 begin
@@ -23,8 +22,7 @@
 end
 
 
-class at_most_two_elems =
-  includes permutation_syntax
+class at_most_two_elems = opening permutation_syntax +
   assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close>
 begin
 
diff -r a4d7da18ac5c -r e7c2848b78e8 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Fri Nov 27 06:48:35 2020 +0000
@@ -18,6 +18,7 @@
     ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
   val constdecl: (binding * string option * mixfix) parser
   val includes: (xstring * Position.T) list parser
+  val opening: (xstring * Position.T) list parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expression: string list parser
@@ -84,6 +85,8 @@
 
 val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
 
+val opening = Parse.$$$ "opening" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
     >> (single o Scan.triple1) ||
diff -r a4d7da18ac5c -r e7c2848b78e8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Nov 26 23:23:19 2020 +0100
+++ b/src/Pure/Pure.thy	Fri Nov 27 06:48:35 2020 +0000
@@ -46,6 +46,7 @@
   and "instantiation" :: thy_decl_block
   and "instance" :: thy_goal
   and "overloading" :: thy_decl_block
+  and "opening" :: quasi_command
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt
   and "schematic_goal" :: thy_goal_stmt
@@ -626,8 +627,8 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
-    ((Parse.name_position
-        >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd [] name)) ||
+    (((Parse.name_position -- Scan.optional Parse_Spec.opening [])
+        >> (fn (name, incls) => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd incls name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
       --| Parse.begin);
@@ -647,18 +648,19 @@
 local
 
 val locale_context_elements =
-  Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+  Scan.repeat1 Parse_Spec.context_element;
 
 val locale_val =
-  Parse_Spec.locale_expression --
-    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! locale_context_elements) ([], []) ||
-  locale_context_elements >> pair ([], []);
+  ((Parse_Spec.locale_expression -- Scan.optional Parse_Spec.opening [])
+    || Parse_Spec.opening >> pair ([], []))
+  -- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! locale_context_elements) []
+  || locale_context_elements >> pair (([], []), []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
     (Parse.binding --
-      Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), ([], [])) -- Parse.opt_begin
-      >> (fn ((name, (expr, (includes, elems))), begin) =>
+      Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) ((([], []), []), []) -- Parse.opt_begin
+      >> (fn ((name, ((expr, includes), elems)), begin) =>
           Toplevel.begin_main_target begin
             (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd)));
 
@@ -710,17 +712,18 @@
 local
 
 val class_context_elements =
-  Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+  Scan.repeat1 Parse_Spec.context_element;
 
 val class_val =
-  Parse_Spec.class_expression --
-    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! class_context_elements) ([], []) ||
-  class_context_elements >> pair [];
+  ((Parse_Spec.class_expression -- Scan.optional Parse_Spec.opening [])
+    || Parse_Spec.opening >> pair [])
+  -- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! class_context_elements) [] ||
+  class_context_elements >> pair ([], []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
-   (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], ([], [])) -- Parse.opt_begin
-    >> (fn ((name, (supclasses, (includes, elems))), begin) =>
+   (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) (([], []), []) -- Parse.opt_begin
+    >> (fn ((name, ((supclasses, includes), elems)), begin) =>
         Toplevel.begin_main_target begin
           (Class_Declaration.class_cmd name includes supclasses elems #> snd)));