--- 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.
--- 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>,
--- 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>
--- 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
--- 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) ||
--- 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)));