--- a/NEWS Sun Apr 15 13:21:13 2012 +0200
+++ b/NEWS Sun Apr 15 14:50:09 2012 +0200
@@ -74,6 +74,14 @@
Any other local theory specification element works within the "context
... begin ... end" block as well.
+* Bundled declarations associate attributed fact expressions with a
+given name in the context. These may be later included in other
+contexts. This allows to manage context extensions casually, without
+the logical dependencies of locales and locale interpretation.
+
+See commands 'bundle', 'include', 'including' etc. in the isar-ref
+manual.
+
* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
tolerant against multiple unifiers, as long as the final result is
unique. (As before, rules are composed in canonical right-to-left
--- a/doc-src/IsarRef/Thy/Proof.thy Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Sun Apr 15 14:50:09 2012 +0200
@@ -294,7 +294,7 @@
*}
-subsection {* Facts and forward chaining *}
+subsection {* Facts and forward chaining \label{sec:proof-facts} *}
text {*
\begin{matharray}{rcl}
@@ -440,7 +440,7 @@
goal: (@{syntax props} + @'and')
;
- longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
+ longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion
;
conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
;
@@ -454,8 +454,8 @@
\<phi>"} to be put back into the target context. An additional @{syntax
context} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of @{syntax context_elem} in
- \secref{sec:locale}.
+ well, see also @{syntax "includes"} in \secref{sec:bundle} and
+ @{syntax context_elem} in \secref{sec:locale}.
\item @{command "theorem"}~@{text "a: \<phi>"} and @{command
"corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
--- a/doc-src/IsarRef/Thy/Spec.thy Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Apr 15 14:50:09 2012 +0200
@@ -126,9 +126,10 @@
"instantiation"}, @{command "overloading"}.
@{rail "
- @@{command context} (@{syntax nameref} | (@{syntax context_elem}+)) @'begin'
+ @@{command context} @{syntax nameref} @'begin'
;
-
+ @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin'
+ ;
@{syntax_def target}: '(' @'in' @{syntax nameref} ')'
"}
@@ -140,12 +141,13 @@
@{keyword "begin"} keyword as well, in order to continue the local
theory immediately after the initial specification.
- \item @{command "context"}~@{text "elements \<BEGIN>"} opens an
- unnamed context, by extending the enclosing global or local theory
- target by the given context elements (@{text "\<FIXES>"}, @{text
- "\<ASSUMES>"} etc.). This means any results stemming from
- definitions and proofs in the extended context will be exported into
- the enclosing target by lifting over extra parameters and premises.
+ \item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens
+ an unnamed context, by extending the enclosing global or local
+ theory target by the given declaration bundles (\secref{sec:bundle})
+ and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"}
+ etc.). This means any results stemming from definitions and proofs
+ in the extended context will be exported into the enclosing target
+ by lifting over extra parameters and premises.
\item @{command (local) "end"} concludes the current local theory,
according to the nesting of contexts. Note that a global @{command
@@ -187,6 +189,78 @@
"~~/src/HOL/Isar_Examples/Group_Context.thy"}. *}
+section {* Bundled declarations \label{sec:bundle} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
+ @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{keyword_def "includes"} & : & syntax \\
+ \end{matharray}
+
+ The outer syntax of fact expressions (\secref{sec:syn-att}) involves
+ theorems and attributes, which are evaluated in the context and
+ applied to it. Attributes may declare theorems to the context, as
+ in @{text "this_rule [intro] that_rule [elim]"} for example.
+ Configuration options (\secref{sec:config}) are special declaration
+ attributes that operate on the context without a theorem, as in
+ @{text "[[show_types = false]]"} for example.
+
+ Expressions of this form may be defined as \emph{bundled
+ declarations} in the context, and included in other situations later
+ on. Including declaration bundles augments a local context casually
+ without logical dependencies, which is in contrast to locales and
+ locale interpretation (\secref{sec:locale}).
+
+ @{rail "
+ @@{command bundle} @{syntax target}? \\
+ @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
+ ;
+ (@@{command include} | @@{command including}) (@{syntax nameref}+)
+ ;
+ @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+)
+ "}
+
+ \begin{description}
+
+ \item @{command bundle}~@{text "b = decls"} defines a bundle of
+ declarations in the current context. The RHS is similar to the one
+ of the @{command declare} command. Bundles defined in local theory
+ targets are subject to transformations via morphisms, when moved
+ into different application contexts; this works analogously to any
+ other local theory specification.
+
+ \item @{command print_bundles} prints the named bundles that are
+ available in the current context.
+
+ \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
+ from the given bundles into the current proof body context. This is
+ analogous to @{command "note"} (\secref{sec:proof-facts}) with the
+ expanded bundles.
+
+ \item @{command including} is similar to @{command include}, but
+ works in proof refinement (backward mode). This is analogous to
+ @{command "using"} (\secref{sec:proof-facts}) with the expanded
+ bundles.
+
+ \item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to
+ @{command include}, but works in situations where a specification
+ context is constructed, notably for @{command context} and long
+ statements of @{command theorem} etc.
+
+ \end{description}
+
+ Here is an artificial example of bundling various configuration
+ options: *}
+
+bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
+
+lemma "x = x"
+ including trace by metis
+
+
section {* Basic specification elements *}
text {*
--- a/doc-src/IsarRef/Thy/document/Proof.tex Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Sun Apr 15 14:50:09 2012 +0200
@@ -373,7 +373,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Facts and forward chaining%
+\isamarkupsubsection{Facts and forward chaining \label{sec:proof-facts}%
}
\isamarkuptrue%
%
@@ -590,6 +590,10 @@
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\indexref{}{syntax}{includes}\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}[]
+\rail@endbar
\rail@plus
\rail@nextplus{1}
\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
@@ -634,8 +638,8 @@
\item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context. An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
- \secref{sec:locale}.
+ well, see also \hyperlink{syntax.includes}{\mbox{\isa{includes}}} in \secref{sec:bundle} and
+ \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in \secref{sec:locale}.
\item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as
being of a different kind. This discrimination acts like a formal
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Apr 15 13:21:13 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Apr 15 14:50:09 2012 +0200
@@ -187,16 +187,21 @@
targets, like \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}, \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}, \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}, \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}.
\begin{railoutput}
-\rail@begin{3}{}
+\rail@begin{1}{}
+\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@term{\isa{\isakeyword{begin}}}[]
+\rail@end
+\rail@begin{2}{}
\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
\rail@bar
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@nextbar{1}
+\rail@nont{\indexref{}{syntax}{includes}\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}[]
+\rail@endbar
\rail@plus
-\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
-\rail@nextplus{2}
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@endplus
-\rail@endbar
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
\rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
@@ -216,11 +221,13 @@
\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as well, in order to continue the local
theory immediately after the initial specification.
- \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}elements\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens an
- unnamed context, by extending the enclosing global or local theory
- target by the given context elements (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C46495845533E}{\isasymFIXES}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}{\isaliteral{22}{\isachardoublequote}}} etc.). This means any results stemming from
- definitions and proofs in the extended context will be exported into
- the enclosing target by lifting over extra parameters and premises.
+ \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}bundles\ elements\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens
+ an unnamed context, by extending the enclosing global or local
+ theory target by the given declaration bundles (\secref{sec:bundle})
+ and context elements (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C46495845533E}{\isasymFIXES}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}{\isaliteral{22}{\isachardoublequote}}}
+ etc.). This means any results stemming from definitions and proofs
+ in the extended context will be exported into the enclosing target
+ by lifting over extra parameters and premises.
\item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory,
according to the nesting of contexts. Note that a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory
@@ -259,6 +266,129 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Bundled declarations \label{sec:bundle}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{bundle}\hypertarget{command.bundle}{\hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{print\_bundles}\hypertarget{command.print-bundles}{\hyperlink{command.print-bundles}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}bundles}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{include}\hypertarget{command.include}{\hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{including}\hypertarget{command.including}{\hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{keyword}{includes}\hypertarget{keyword.includes}{\hyperlink{keyword.includes}{\mbox{\isa{\isakeyword{includes}}}}} & : & syntax \\
+ \end{matharray}
+
+ The outer syntax of fact expressions (\secref{sec:syn-att}) involves
+ theorems and attributes, which are evaluated in the context and
+ applied to it. Attributes may declare theorems to the context, as
+ in \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}\ that{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} for example.
+ Configuration options (\secref{sec:config}) are special declaration
+ attributes that operate on the context without a theorem, as in
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}types\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} for example.
+
+ Expressions of this form may be defined as \emph{bundled
+ declarations} in the context, and included in other situations later
+ on. Including declaration bundles augments a local context casually
+ without logical dependencies, which is in contrast to locales and
+ locale interpretation (\secref{sec:locale}).
+
+ \begin{railoutput}
+\rail@begin{6}{}
+\rail@term{\hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
+\rail@endbar
+\rail@cr{3}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@bar
+\rail@nextbar{4}
+\rail@term{\isa{\isakeyword{for}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
+\rail@nextplus{5}
+\rail@cterm{\isa{\isakeyword{and}}}[]
+\rail@endplus
+\rail@endbar
+\rail@end
+\rail@begin{2}{}
+\rail@bar
+\rail@term{\hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{\indexdef{}{syntax}{includes}\hypertarget{syntax.includes}{\hyperlink{syntax.includes}{\mbox{\isa{includes}}}}}
+\rail@term{\isa{\isakeyword{includes}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{command.bundle}{\mbox{\isa{\isacommand{bundle}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3D}{\isacharequal}}\ decls{\isaliteral{22}{\isachardoublequote}}} defines a bundle of
+ declarations in the current context. The RHS is similar to the one
+ of the \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} command. Bundles defined in local theory
+ targets are subject to transformations via morphisms, when moved
+ into different application contexts; this works analogously to any
+ other local theory specification.
+
+ \item \hyperlink{command.print-bundles}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}bundles}}}} prints the named bundles that are
+ available in the current context.
+
+ \item \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} includes the declarations
+ from the given bundles into the current proof body context. This is
+ analogous to \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} (\secref{sec:proof-facts}) with the
+ expanded bundles.
+
+ \item \hyperlink{command.including}{\mbox{\isa{\isacommand{including}}}} is similar to \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}, but
+ works in proof refinement (backward mode). This is analogous to
+ \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} (\secref{sec:proof-facts}) with the expanded
+ bundles.
+
+ \item \hyperlink{keyword.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is similar to
+ \hyperlink{command.include}{\mbox{\isa{\isacommand{include}}}}, but works in situations where a specification
+ context is constructed, notably for \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}} and long
+ statements of \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} etc.
+
+ \end{description}
+
+ Here is an artificial example of bundling various configuration
+ options:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{bundle}\isamarkupfalse%
+\ trace\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ linarith{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ metis{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{2C}{\isacharcomma}}\ smt{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isacommand{including}\isamarkupfalse%
+\ trace%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ metis%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
\isamarkupsection{Basic specification elements%
}
\isamarkuptrue%