represent both algebraic and local-theory views on locale interpretation in interfaces
--- a/NEWS Sat Nov 14 08:45:52 2015 +0100
+++ b/NEWS Sat Nov 14 17:37:44 2015 +0100
@@ -315,7 +315,9 @@
commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
* Command 'permanent_interpretation' is available in Pure, without
-need to load a separate theory.
+need to load a separate theory. Keyword 'defines' identifies
+mixin definitions, keyword 'rewrites' identifies rewrite morphisms.
+INCOMPATIBILITY.
* Command 'print_definitions' prints dependencies of definitional
specifications. This functionality used to be part of 'print_theory'.
--- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 14 17:37:44 2015 +0100
@@ -605,74 +605,108 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
@{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "interpretation"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
@{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "permanent_interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
@{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
- @{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
+ @{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
Locales may be instantiated, and the resulting instantiated declarations
added to the current context. This requires proof (of the instantiated
- specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is
- possible in locales (\<^theory_text>\<open>sublocale\<close>), global and local theories
- (\<^theory_text>\<open>interpretation\<close>) and also within proof bodies (\<^theory_text>\<open>interpret\<close>).
+ specification) and is called \<^emph>\<open>locale interpretation\<close>.
+ Interpretation is possible within
+ arbitrary local theories (\<^theory_text>\<open>interpretation\<close>),
+ within proof bodies (\<^theory_text>\<open>interpret\<close>), into global theories
+ (another variant of \<^theory_text>\<open>interpretation\<close>)
+ and into locales (\<^theory_text>\<open>sublocale\<close>).
+ As a generalization, interpretation into
+ arbitrary local theories is possible, although this is
+ only implemented by certain targets
+ (\<^theory_text>\<open>permanent_interpretation\<close>).
+
@{rail \<open>
@@{command interpretation} @{syntax locale_expr} equations?
;
@@{command interpret} @{syntax locale_expr} equations?
;
+ @@{command interpretation} @{syntax locale_expr} equations?
+ ;
@@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
- equations?
+ definitions? equations?
+ ;
+ @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
+ definitions? equations?
;
@@{command print_dependencies} '!'? @{syntax locale_expr}
;
@@{command print_interps} @{syntax nameref}
;
+ definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
+ @{syntax mixfix}? @'=' @{syntax term} + @'and');
+
equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> in a global or
- local theory. The command generates proof obligations for the instantiated
- specifications. Once these are discharged by the user, instantiated
- declarations (in particular, facts) are added to the theory in a
- post-processing phase.
+ The core of each interpretation command is a locale expression
+ \<open>expr\<close>; the command generates proof obligations for the instantiated
+ specifications. Once these are discharged by the user, instantiated
+ declarations (in particular, facts) are added to the context in
+ a post-processing phase, in a manner specific to each command.
- The command is aware of interpretations that are already active.
- Post-processing is achieved through a variant of roundup that takes the
+ Interpretation commands are aware of interpretations that are already active:
+ post-processing is achieved through a variant of roundup that takes
interpretations of the current global or local theory into account. In order
to simplify the proof obligations according to existing interpretations use
methods @{method intro_locales} or @{method unfold_locales}.
+ Given equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is
+ interpreted, adding rewrite rules. This is particularly useful
+ for interpreting concepts introduced through definitions. The
+ equations must be proved the user.
+
+ Given definitions \<open>defs\<close> produce corresponding definitions in
+ the local theory's underlying target \<^emph>\<open>and\<close> amend the morphism
+ with the equations stemming from the symmetric of the
+ definitions. Hence they need not be proved explicitly the user.
+ Such rewrite definitions are a even more useful device for
+ interpreting concepts introduced through definitions, but they
+ are only supported for interpretation commands operating in
+ a local theory whose implementing target actually supports this.
+
+ \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close>
+ interprets \<open>expr\<close> into a local theory such that its lifetime is
+ limited to the current context block (e.g. a locale or unnamed context).
+ At the closing @{command end}
+ of the block the interpretation and its declarations disappear.
+ Hence facts based on interpretation can be established without
+ creating permanent links to the interpreted locale instances, as
+ would be the case with @{command sublocale}.
+
+ \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets
+ \<open>expr\<close> into a proof context: the interpretation and its declarations
+ disappear when closing the current proof block.
+ Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be
+ explicitly universally quantified.
+
+ \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close>
+ interprets \<open>expr\<close> into a global theory.
+
When adding declarations to locales, interpreted versions of these
declarations are added to the global theory for all interpretations in the
global theory as well. That is, interpretations in global theories
dynamically participate in any declarations added to locales.
- In contrast, the lifetime of an interpretation in a local theory is limited
- to the current context block. At the closing \<^theory_text>\<open>end\<close> of the block the
- interpretation and its declarations disappear. This enables establishing
- facts based on interpretations without creating permanent links to the
- interpreted locale instances, as would be the case with \<^theory_text>\<open>sublocale\<close>. While
- \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is technically possible, it is not useful since
- its result is discarded immediately.
-
Free variables in the interpreted expression are allowed. They are turned
into schematic variables in the generated declarations. In order to use a
free variable whose name is already bound in the context --- for example,
because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
- The equations \<open>eqns\<close> yield \<^emph>\<open>rewrite morphisms\<close>, which are unfolded during
- post-processing and are useful for interpreting concepts introduced through
- definitions. The equations must be proved.
-
- \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> in the proof context and
- is otherwise similar to interpretation in local theories. Note that for
- \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly universally quantified.
-
- \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr rewrites eqns\<close> interprets \<open>expr\<close> in the locale
+ \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> defines "defs" expr rewrites eqns\<close> interprets \<open>expr\<close> into the locale
\<open>name\<close>. A proof that the specification of \<open>name\<close> implies the specification
of \<open>expr\<close> is required. As in the localized version of the theorem command,
the proof is in the context of \<open>name\<close>. After the proof obligation has been
@@ -689,15 +723,30 @@
adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
- The equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is interpreted.
- This enables mapping definitions from the interpreted locales to entities of
- \<open>name\<close> and can help break infinite chains induced by circular \<^theory_text>\<open>sublocale\<close>
+ Using equations \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can
+ help break infinite chains induced by circular \<^theory_text>\<open>sublocale\<close>
declarations.
In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
locale argument must be omitted. The command then refers to the locale (or
class) target of the context block.
+ \<^descr> \<^theory_text>\<open>permanent_interpretation defines "defs" rewrites eqns\<close>
+ interprets \<open>expr\<close> into the target of the current local theory.
+ When adding declarations to locales, interpreted versions of these
+ declarations are added to any target for all interpretations
+ in that target as well. That is, permanent interpretations
+ dynamically participate in any declarations added to
+ locales.
+
+ The local theory's underlying target must explicitly support
+ permanent interpretations. Prominent examples are global theories
+ (where \<^theory_text>\<open>permanent_interpretation\<close> technically
+ corresponds to \<^theory_text>\<open>interpretation\<close>) and locales
+ (where \<^theory_text>\<open>permanent_interpretation\<close> technically
+ corresponds to \<^theory_text>\<open>sublocale\<close>). Unnamed contexts
+ (see \secref{sec:target}) are not admissible.
+
\<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
interpretation of \<open>expr\<close> in the current context. It lists all locale
instances for which interpretations would be added to the current context.
@@ -711,7 +760,6 @@
\<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
declarations.
-
\begin{warn}
If a global theory inherits declarations (body elements) for a locale from
one parent and an interpretation of that locale from another parent, the
@@ -733,71 +781,11 @@
more general than the interpretation of the first. The locale package does
not attempt to remove subsumed interpretations.
\end{warn}
-\<close>
-
-subsubsection \<open>Permanent locale interpretation\<close>
-
-text \<open>
- Permanent locale interpretation is an extension on top
- of \<^theory_text>\<open>interpretation\<close> and \<^theory_text>\<open>sublocale\<close>
- and provides
-
- \<^enum> a unified view on arbitrary suitable local theories as interpretation
- target;
-
- \<^enum> rewrite morphisms by means of \<^emph>\<open>rewrite definitions\<close>.
-
- \begin{matharray}{rcl}
- @{command_def "permanent_interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>
- \end{matharray}
-
- @{rail \<open>
- @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
- definitions? equations?
- ;
- definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
- @{syntax mixfix}? @'=' @{syntax term} + @'and');
- equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
- \<close>}
-
- \<^descr> \<^theory_text>\<open>permanent_interpretation expr defines "defs" rewrites eqns\<close> interprets
- \<open>expr\<close> in the current local theory. The command generates proof obligations
- for the instantiated specifications. Instantiated declarations (in
- particular, facts) are added to the local theory's underlying target in a
- post-processing phase. When adding declarations to locales, interpreted
- versions of these declarations are added to any target for all
- interpretations in that target as well. That is, permanent interpretations
- dynamically participate in any declarations added to locales.
-
- The local theory's underlying target must explicitly support permanent
- interpretations. Prominent examples are global theories (where
- \<^theory_text>\<open>permanent_interpretation\<close> is technically corresponding to
- \<^theory_text>\<open>interpretation\<close>) and locales (where \<^theory_text>\<open>permanent_interpretation\<close> is
- technically corresponding to \<^theory_text>\<open>sublocale\<close>). Unnamed contexts (see
- \secref{sec:target}) are not admissible since they are non-permanent due to
- their very nature.
-
- In additions to \<^emph>\<open>rewrite morphisms\<close> specified by \<open>eqns\<close>, also \<^emph>\<open>rewrite
- definitions\<close> may be specified. Semantically, a rewrite definition
-
- \<^item> produces a corresponding definition in the local theory's underlying
- target \<^emph>\<open>and\<close>
-
- \<^item> augments the rewrite morphism with the equation stemming from the
- symmetric of the corresponding definition.
-
- This is technically different to to a naive combination of a conventional
- definition and an explicit rewrite equation:
-
- \<^item> Definitions are parsed in the syntactic interpretation context, just
- like equations.
-
- \<^item> The proof needs not consider the equations stemming from definitions --
- they are proved implicitly by construction.
-
- Rewrite definitions yield a pattern for introducing new explicit operations
- for existing terms after interpretation.
+ \begin{warn}
+ While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
+ its result is discarded immediately.
+ \end{warn}
\<close>
--- a/src/HOL/Statespace/state_space.ML Sat Nov 14 08:45:52 2015 +0100
+++ b/src/HOL/Statespace/state_space.ML Sat Nov 14 17:37:44 2015 +0100
@@ -127,7 +127,7 @@
fun prove_interpretation_in ctxt_tac (name, expr) thy =
thy
- |> Interpretation.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
+ |> Interpretation.global_sublocale_cmd (name, Position.none) (expression_no_pos expr) [] []
|> Proof.global_terminal_proof
((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
|> Proof_Context.theory_of
--- a/src/Pure/Isar/interpretation.ML Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Sat Nov 14 17:37:44 2015 +0100
@@ -7,33 +7,48 @@
signature INTERPRETATION =
sig
- val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
- val interpret_cmd: Expression.expression -> (Attrib.binding * string) list ->
- bool -> Proof.state -> Proof.state
- val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list ->
- local_theory -> Proof.state
+ type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
+ type 'a rewrites = (Attrib.binding * 'a) list
+
+ (*interpretation in proofs*)
+ val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
+ val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
+
+ (*algebraic-view*)
+ val global_interpretation: Expression.expression_i ->
+ term defines -> term rewrites -> theory -> Proof.state
+ val global_sublocale: string -> Expression.expression_i ->
+ term defines -> term rewrites ->theory -> Proof.state
+ val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
+ string defines -> string rewrites -> theory -> Proof.state
+ val sublocale: Expression.expression_i ->
+ term defines -> term rewrites -> local_theory -> Proof.state
+ val sublocale_cmd: Expression.expression ->
+ string defines -> string rewrites -> local_theory -> Proof.state
+
+ (*local-theory-based view*)
+ val ephemeral_interpretation: Expression.expression_i ->
+ term rewrites -> local_theory -> Proof.state
val permanent_interpretation: Expression.expression_i ->
- (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
- local_theory -> Proof.state
+ term defines -> term rewrites -> local_theory -> Proof.state
val permanent_interpretation_cmd: Expression.expression ->
- (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
+ string defines -> string rewrites -> local_theory -> Proof.state
+
+ (*mixed Isar interface*)
+ val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
+ val interpretation_cmd: Expression.expression -> string rewrites ->
local_theory -> Proof.state
-
- val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
- val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list ->
- local_theory -> Proof.state
- val sublocale: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
- val sublocale_cmd: Expression.expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
- val sublocale_global: string -> Expression.expression_i ->
- (Attrib.binding * term) list -> theory -> Proof.state
- val sublocale_global_cmd: xstring * Position.T -> Expression.expression ->
- (Attrib.binding * string) list -> theory -> Proof.state
end;
structure Interpretation : INTERPRETATION =
struct
-(** reading **)
+(** common interpretation machinery **)
+
+type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
+type 'a rewrites = (Attrib.binding * 'a) list
+
+(* reading of locale expressions with rewrite morphisms *)
local
@@ -72,7 +87,7 @@
end;
-(** common interpretation machinery **)
+(* interpretation machinery *)
local
@@ -112,12 +127,12 @@
end;
-(** first dimension: proof vs. local theory **)
+(** interfaces **)
+
+(* interpretation in proofs *)
local
-(* proof *)
-
fun gen_interpret prep_interpretation expression raw_eqns int state =
let
val _ = Proof.assert_forward_or_chain state;
@@ -132,25 +147,43 @@
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
end;
-
-(* local theory *)
+in
-fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy =
- generic_interpretation prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy;
+fun interpret expression = gen_interpret cert_interpretation expression;
+fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
-fun gen_interpretation prep_interpretation expression raw_defs raw_eqns =
- Local_Theory.assert_bottom true
- #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+end;
-(** second dimension: relation to underlying target **)
+(* algebraic-view *)
+
+local
-fun subscribe_or_activate lthy =
- if Named_Target.is_theory lthy
- then Local_Theory.subscription
- else Locale.activate_fragment;
+fun gen_global_interpretation prep_interpretation expression
+ raw_defs raw_eqns thy =
+ let
+ val lthy = Named_Target.theory_init thy;
+ fun setup_proof after_qed =
+ Element.witness_proof_eqs
+ (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
+ in
+ lthy |>
+ generic_interpretation_with_defs prep_interpretation setup_proof
+ Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+ end;
+
+fun gen_global_sublocale prep_loc prep_interpretation
+ raw_locale expression raw_defs raw_eqns thy =
+ let
+ val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
+ fun setup_proof after_qed =
+ Element.witness_proof_eqs
+ (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
+ in
+ lthy |>
+ generic_interpretation_with_defs prep_interpretation setup_proof
+ Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+ end;
fun subscribe_locale_only lthy =
let
@@ -160,48 +193,68 @@
else ();
in Local_Theory.subscription end;
+fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
+ generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
-(** special case: global sublocale command **)
+in
-fun gen_sublocale_global prep_loc prep_interpretation
- raw_locale expression raw_eqns thy =
- let
- val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
- fun setup_proof after_qed =
- Element.witness_proof_eqs
- (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
- in
- lthy |>
- generic_interpretation prep_interpretation setup_proof
- Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
- end;
+fun global_interpretation expression =
+ gen_global_interpretation cert_interpretation expression;
+fun global_sublocale expression =
+ gen_global_sublocale (K I) cert_interpretation expression;
+fun global_sublocale_cmd raw_expression =
+ gen_global_sublocale Locale.check read_interpretation raw_expression;
+fun sublocale expression =
+ gen_sublocale cert_interpretation expression;
+fun sublocale_cmd raw_expression =
+ gen_sublocale read_interpretation raw_expression;
+
+end;
+
+
+(* local-theory-based view *)
+
+local
+
+fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
+ Local_Theory.assert_bottom true
+ #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
in
-
-(** interfaces **)
-
-fun interpret x = gen_interpret cert_interpretation x;
-fun interpret_cmd x = gen_interpret read_interpretation x;
+fun ephemeral_interpretation expression =
+ generic_interpretation cert_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Locale.activate_fragment expression;
-fun ephemeral_interpretation x =
- gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
+fun permanent_interpretation expression =
+ gen_permanent_interpretation cert_interpretation expression;
+fun permanent_interpretation_cmd raw_expression =
+ gen_permanent_interpretation read_interpretation raw_expression;
-fun permanent_interpretation x = gen_interpretation cert_interpretation x;
-fun permanent_interpretation_cmd x = gen_interpretation read_interpretation x;
+end;
+
+
+(* mixed Isar interface *)
+
+local
-fun interpretation x =
- gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;
-fun interpretation_cmd x =
- gen_local_theory_interpretation read_interpretation subscribe_or_activate x;
+fun subscribe_or_activate lthy =
+ if Named_Target.is_theory lthy
+ then Local_Theory.subscription
+ else Locale.activate_fragment;
-fun sublocale x =
- gen_local_theory_interpretation cert_interpretation subscribe_locale_only x;
-fun sublocale_cmd x =
- gen_local_theory_interpretation read_interpretation subscribe_locale_only x;
+fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
+ generic_interpretation prep_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
-fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x;
-fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x;
+in
+
+fun interpretation expression =
+ gen_local_theory_interpretation cert_interpretation expression;
+fun interpretation_cmd raw_expression =
+ gen_local_theory_interpretation read_interpretation raw_expression;
end;
--- a/src/Pure/Isar/isar_syn.ML Sat Nov 14 08:45:52 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Nov 14 17:37:44 2015 +0100
@@ -407,23 +407,27 @@
Scan.optional
(@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+val interpretation_args_with_defs =
+ Parse.!!! Parse_Spec.locale_expression --
+ (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+ Scan.optional
+ (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
+
val _ =
Outer_Syntax.command @{command_keyword sublocale}
"prove sublocale relation between a locale and a locale expression"
((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
- interpretation_args >> (fn (loc, (expr, equations)) =>
- Toplevel.theory_to_proof (Interpretation.sublocale_global_cmd loc expr equations)))
- || interpretation_args >> (fn (expr, equations) =>
- Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
+ interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
+ Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
+ || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
+ Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
"prove interpretation of locale expression into named theory"
- (Parse.!!! Parse_Spec.locale_expression --
- Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
- -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
- Scan.optional (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
- >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
+ (interpretation_args_with_defs
+ >> (fn (expr, (defs, equations)) => Interpretation.permanent_interpretation_cmd expr defs equations));
val _ =
Outer_Syntax.command @{command_keyword interpretation}