%
\begin{isabellebody}%
\def\isabellecontext{Isar}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Isar\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Isar language elements%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isar proof language (see also
\cite[\S2]{isabelle-isar-ref}) consists of three main categories of
language elements as follows.
\begin{enumerate}
\item Proof \emph{commands} define the primary language of
transactions of the underlying Isar/VM interpreter. Typical
examples are \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}, and \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}.
Composing proof commands according to the rules of the Isar/VM leads
to expressions of structured proof text, such that both the machine
and the human reader can give it a meaning as formal reasoning.
\item Proof \emph{methods} define a secondary language of mixed
forward-backward refinement steps involving facts and goals.
Typical examples are \hyperlink{method.rule}{\mbox{\isa{rule}}}, \hyperlink{method.unfold}{\mbox{\isa{unfold}}}, and \hyperlink{method.simp}{\mbox{\isa{simp}}}.
Methods can occur in certain well-defined parts of the Isar proof
language, say as arguments to \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}, \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}},
or \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}.
\item \emph{Attributes} define a tertiary language of small
annotations to theorems being defined or referenced. Attributes can
modify both the context and the theorem.
Typical examples are \hyperlink{attribute.intro}{\mbox{\isa{intro}}} (which affects the context),
and \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} (which affects the theorem).
\end{enumerate}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof commands%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \emph{proof command} is state transition of the Isar/VM
proof interpreter.
In principle, Isar proof commands could be defined in user-space as
well. The system is built like that in the first place: one part of
the commands are primitive, the other part is defined as derived
elements. Adding to the genuine structured proof language requires
profound understanding of the Isar/VM machinery, though, so this is
beyond the scope of this manual.
What can be done realistically is to define some diagnostic commands
that inspect the general state of the Isar/VM, and report some
feedback to the user. Typically this involves checking of the
linguistic \emph{mode} of a proof state, or peeking at the pending
goals (if available).
Another common application is to define a toplevel command that
poses a problem to the user as Isar proof state and processes the
final result relatively to the context. Thus a proof can be
incorporated into the context of some user-space tool, without
modifying the Isar proof language itself.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Proof.state}\verb|type Proof.state| \\
\indexdef{}{ML}{Proof.assert\_forward}\verb|Proof.assert_forward: Proof.state -> Proof.state| \\
\indexdef{}{ML}{Proof.assert\_chain}\verb|Proof.assert_chain: Proof.state -> Proof.state| \\
\indexdef{}{ML}{Proof.assert\_backward}\verb|Proof.assert_backward: Proof.state -> Proof.state| \\
\indexdef{}{ML}{Proof.simple\_goal}\verb|Proof.simple_goal: Proof.state -> {context: Proof.context, goal: thm}| \\
\indexdef{}{ML}{Proof.goal}\verb|Proof.goal: Proof.state ->|\isasep\isanewline%
\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
\indexdef{}{ML}{Proof.raw\_goal}\verb|Proof.raw_goal: Proof.state ->|\isasep\isanewline%
\verb| {context: Proof.context, facts: thm list, goal: thm}| \\
\indexdef{}{ML}{Proof.theorem}\verb|Proof.theorem: Method.text option ->|\isasep\isanewline%
\verb| (thm list list -> Proof.context -> Proof.context) ->|\isasep\isanewline%
\verb| (term * term list) list list -> Proof.context -> Proof.state| \\
\end{mldecls}
\begin{description}
\item Type \verb|Proof.state| represents Isar proof states.
This is a block-structured configuration with proof context,
linguistic mode, and optional goal. The latter consists of goal
context, goal facts (``\isa{using}''), and tactical goal state
(see \secref{sec:tactical-goals}).
The general idea is that the facts shall contribute to the
refinement of some parts of the tactical goal --- how exactly is
defined by the proof method that is applied in that situation.
\item \verb|Proof.assert_forward|, \verb|Proof.assert_chain|, \verb|Proof.assert_backward| are partial identity functions that fail
unless a certain linguistic mode is active, namely ``\isa{proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}}'', ``\isa{proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}}'', ``\isa{proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}}'', respectively (using the terminology of
\cite{isabelle-isar-ref}).
It is advisable study the implementations of existing proof commands
for suitable modes to be asserted.
\item \verb|Proof.simple_goal|~\isa{state} returns the structured
Isar goal (if available) in the form seen by ``simple'' methods
(like \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.blast}{\mbox{\isa{blast}}}). The Isar goal facts are
already inserted as premises into the subgoals, which are presented
individually as in \verb|Proof.goal|.
\item \verb|Proof.goal|~\isa{state} returns the structured Isar
goal (if available) in the form seen by regular methods (like
\hyperlink{method.rule}{\mbox{\isa{rule}}}). The auxiliary internal encoding of Pure
conjunctions is split into individual subgoals as usual.
\item \verb|Proof.raw_goal|~\isa{state} returns the structured
Isar goal (if available) in the raw internal form seen by ``raw''
methods (like \hyperlink{method.induct}{\mbox{\isa{induct}}}). This form is rarely appropriate
for dignostic tools; \verb|Proof.simple_goal| or \verb|Proof.goal|
should be used in most situations.
\item \verb|Proof.theorem|~\isa{before{\isaliteral{5F}{\isacharunderscore}}qed\ after{\isaliteral{5F}{\isacharunderscore}}qed\ statement\ ctxt}
initializes a toplevel Isar proof state within a given context.
The optional \isa{before{\isaliteral{5F}{\isacharunderscore}}qed} method is applied at the end of
the proof, just before extracting the result (this feature is rarely
used).
The \isa{after{\isaliteral{5F}{\isacharunderscore}}qed} continuation receives the extracted result
in order to apply it to the final context in a suitable way (e.g.\
storing named facts). Note that at this generic level the target
context is specified as \verb|Proof.context|, but the usual
wrapping of toplevel proofs into command transactions will provide a
\verb|local_theory| here (\chref{ch:local-theory}). This
affects the way how results are stored.
The \isa{statement} is given as a nested list of terms, each
associated with optional \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns as usual in the
Isar source language. The original nested list structure over terms
is turned into one over theorems when \isa{after{\isaliteral{5F}{\isacharunderscore}}qed} is
invoked.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{Isar.goal}\hypertarget{ML antiquotation.Isar.goal}{\hyperlink{ML antiquotation.Isar.goal}{\mbox{\isa{Isar{\isaliteral{2E}{\isachardot}}goal}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\end{matharray}
\begin{description}
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}Isar{\isaliteral{2E}{\isachardot}}goal{\isaliteral{7D}{\isacharbraceright}}} refers to the regular goal state (if
available) of the current proof state managed by the Isar toplevel
--- as abstract value.
This only works for diagnostic ML commands, such as \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
The following example peeks at a certain goal configuration.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
\isacommand{notepad}\isamarkupfalse%
\isanewline
\isakeyword{begin}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{have}\isamarkupfalse%
\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimML
\ \ \ \ %
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ \ \ \ \ val\ n\ {\isaliteral{3D}{\isacharequal}}\ Thm{\isaliteral{2E}{\isachardot}}nprems{\isaliteral{5F}{\isacharunderscore}}of\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}goal\ %
\isaantiq
Isar{\isaliteral{2E}{\isachardot}}goal{}%
\endisaantiq
{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ \ \ \ \ %
\isaantiq
assert{}%
\endisaantiq
\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isadelimproof
\ \ \ \ %
\endisadelimproof
%
\isatagproof
\isacommand{oops}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Here we see 3 individual subgoals in the same way as regular
proof methods would do.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof methods%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \isa{method} is a function \isa{context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ goal\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ goal{\isaliteral{29}{\isacharparenright}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} that operates on the full Isar goal
configuration with context, goal facts, and tactical goal state and
enumerates possible follow-up goal states, with the potential
addition of named extensions of the proof context (\emph{cases}).
The latter feature is rarely used.
This means a proof method is like a structurally enhanced tactic
(cf.\ \secref{sec:tactics}). The well-formedness conditions for
tactics need to hold for methods accordingly, with the following
additions.
\begin{itemize}
\item Goal addressing is further limited either to operate either
uniformly on \emph{all} subgoals, or specifically on the
\emph{first} subgoal.
Exception: old-style tactic emulations that are embedded into the
method space, e.g.\ \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}.
\item A non-trivial method always needs to make progress: an
identical follow-up goal state has to be avoided.\footnote{This
enables the user to write method expressions like \isa{meth\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2B}{\isacharplus}}}
without looping, while the trivial do-nothing case can be recovered
via \isa{meth\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}}.}
Exception: trivial stuttering steps, such as ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' or
\hyperlink{method.succeed}{\mbox{\isa{succeed}}}.
\item Goal facts passed to the method must not be ignored. If there
is no sensible use of facts outside the goal state, facts should be
inserted into the subgoals that are addressed by the method.
\end{itemize}
\medskip Syntactically, the language of proof methods appears as
arguments to Isar commands like \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} or \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}.
User-space additions are reasonably easy by plugging suitable
method-valued parser functions into the framework, using the
\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}} command, for example.
To get a better idea about the range of possibilities, consider the
following Isar proof schemes. This is the general form of
structured proof text:
\medskip
\begin{tabular}{l}
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{props}~\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} \\
\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{28}{\isacharparenleft}}initial{\isaliteral{5F}{\isacharunderscore}}method{\isaliteral{29}{\isacharparenright}}} \\
\quad\isa{body} \\
\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{28}{\isacharparenleft}}terminal{\isaliteral{5F}{\isacharunderscore}}method{\isaliteral{29}{\isacharparenright}}} \\
\end{tabular}
\medskip
The goal configuration consists of \isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and
\isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} appended in that order, and various \isa{props} being claimed. The \isa{initial{\isaliteral{5F}{\isacharunderscore}}method} is invoked
with facts and goals together and refines the problem to something
that is handled recursively in the proof \isa{body}. The \isa{terminal{\isaliteral{5F}{\isacharunderscore}}method} has another chance to finish any remaining
subgoals, but it does not see the facts of the initial step.
\medskip This pattern illustrates unstructured proof scripts:
\medskip
\begin{tabular}{l}
\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{props} \\
\quad\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} \\
\quad\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} \\
\quad\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}}~\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}} \\
\quad\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\
\end{tabular}
\medskip
The \isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} operates on the original claim while
using \isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}. Since the \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command
structurally resets the facts, the \isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} will
operate on the remaining goal state without facts. The \isa{method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}} will see again a collection of \isa{facts\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}} that has been inserted into the script explicitly.
\medskip Empirically, any Isar proof method can be categorized as
follows.
\begin{enumerate}
\item \emph{Special method with cases} with named context additions
associated with the follow-up goal state.
Example: \hyperlink{method.induct}{\mbox{\isa{induct}}}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
Pure conjunction (\secref{sec:logic-aux}), instead of separate
subgoals (\secref{sec:tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
Example: \hyperlink{method.rule}{\mbox{\isa{rule}}}, which captures the key ideas behind
structured reasoning in Isar in purest form.
\item \emph{Simple method} with weaker emphasis on facts, which are
inserted into subgoals to emulate old-style tactical as
``premises''.
Examples: \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}}.
\item \emph{Old-style tactic emulation} with detailed numeric goal
addressing and explicit references to entities of the internal goal
state (which are otherwise invisible from proper Isar proof text).
The naming convention \isa{foo{\isaliteral{5F}{\isacharunderscore}}tac} makes this special
non-standard status clear.
Example: \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}}.
\end{enumerate}
When implementing proof methods, it is advisable to study existing
implementations carefully and imitate the typical ``boiler plate''
for context-sensitive parsing and further combinators to wrap-up
tactic expressions as methods.\footnote{Aliases or abbreviations of
the standard method combinators should be avoided. Note that from
Isabelle99 until Isabelle2009 the system did provide various odd
combinations of method wrappers that made user applications more
complicated than necessary.}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Proof.method}\verb|type Proof.method| \\
\indexdef{}{ML}{METHOD\_CASES}\verb|METHOD_CASES: (thm list -> cases_tactic) -> Proof.method| \\
\indexdef{}{ML}{METHOD}\verb|METHOD: (thm list -> tactic) -> Proof.method| \\
\indexdef{}{ML}{SIMPLE\_METHOD}\verb|SIMPLE_METHOD: tactic -> Proof.method| \\
\indexdef{}{ML}{SIMPLE\_METHOD'}\verb|SIMPLE_METHOD': (int -> tactic) -> Proof.method| \\
\indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{Method.insert\_tac}\verb|Method.insert_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{Method.setup}\verb|Method.setup: binding -> (Proof.context -> Proof.method) context_parser ->|\isasep\isanewline%
\verb| string -> theory -> theory| \\
\end{mldecls}
\begin{description}
\item Type \verb|Proof.method| represents proof methods as
abstract type.
\item \verb|METHOD_CASES|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ facts\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ cases{\isaliteral{5F}{\isacharunderscore}}tactic{\isaliteral{29}{\isacharparenright}}} wraps
\isa{cases{\isaliteral{5F}{\isacharunderscore}}tactic} depending on goal facts as proof method with
cases; the goal context is passed via method syntax.
\item \verb|METHOD|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ facts\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ tactic{\isaliteral{29}{\isacharparenright}}} wraps \isa{tactic} depending on goal facts as regular proof method; the goal
context is passed via method syntax.
\item \verb|SIMPLE_METHOD|~\isa{tactic} wraps a tactic that
addresses all subgoals uniformly as simple proof method. Goal facts
are already inserted into all subgoals before \isa{tactic} is
applied.
\item \verb|SIMPLE_METHOD'|~\isa{tactic} wraps a tactic that
addresses a specific subgoal as simple proof method. Goal facts are
already inserted into the first subgoal before \isa{tactic} is
applied to the same.
\item \verb|HEADGOAL|~\isa{tactic} applies \isa{tactic} to
the first subgoal. This is convenient to reproduce part the \verb|SIMPLE_METHOD'| wrapping within regular \verb|METHOD|, for example.
\item \verb|Method.insert_tac|~\isa{facts\ i} inserts \isa{facts} into subgoal \isa{i}. This is convenient to reproduce
part of the \verb|SIMPLE_METHOD| or \verb|SIMPLE_METHOD'| wrapping
within regular \verb|METHOD|, for example.
\item \verb|Method.setup|~\isa{name\ parser\ description} provides
the functionality of the Isar command \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}} as ML
function.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
See also \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}} in
\cite{isabelle-isar-ref} which includes some abstract examples.
\medskip The following toy examples illustrate how the goal facts
and state are passed to proof methods. The pre-defined proof method
called ``\hyperlink{method.tactic}{\mbox{\isa{tactic}}}'' wraps ML source of type \verb|tactic| (abstracted over \verb|facts|). This allows immediate
experimentation without parsing of concrete syntax.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
\isacommand{notepad}\isamarkupfalse%
\isanewline
\isakeyword{begin}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{assume}\isamarkupfalse%
\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}tactic\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ rtac\ %
\isaantiq
thm\ conjI{}%
\endisaantiq
\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ a\ \isacommand{apply}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}tactic\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ resolve{\isaliteral{5F}{\isacharunderscore}}tac\ facts\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ b\ \isacommand{apply}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}tactic\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ resolve{\isaliteral{5F}{\isacharunderscore}}tac\ facts\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ a\ \isakeyword{and}\ b%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimML
\ \ \ \ %
\endisadelimML
%
\isatagML
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}Isar{\isaliteral{2E}{\isachardot}}goal{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isadelimproof
\ \ \ \ %
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}tactic\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Method{\isaliteral{2E}{\isachardot}}insert{\isaliteral{5F}{\isacharunderscore}}tac\ facts\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}tactic\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}rtac\ %
\isaantiq
thm\ conjI{}%
\endisaantiq
\ THEN{\isaliteral{5F}{\isacharunderscore}}ALL{\isaliteral{5F}{\isacharunderscore}}NEW\ atac{\isaliteral{29}{\isacharparenright}}\ {\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\medskip The next example implements a method that simplifies
the first subgoal by rewrite rules given as arguments.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
\ my{\isaliteral{5F}{\isacharunderscore}}simp\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ \ \ CHANGED\ {\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}full{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}tac\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}HOL{\isaliteral{5F}{\isacharunderscore}}basic{\isaliteral{5F}{\isacharunderscore}}ss\ addsimps\ thms{\isaliteral{29}{\isacharparenright}}\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}rewrite\ subgoal\ by\ given\ rules{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
The concrete syntax wrapping of \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}} always
passes-through the proof context at the end of parsing, but it is
not used in this example.
The \verb|Attrib.thms| parser produces a list of theorems from the
usual Isar syntax involving attribute expressions etc.\ (syntax
category \hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}) \cite{isabelle-isar-ref}. The resulting
\verb|thms| are added to \verb|HOL_basic_ss| which already
contains the basic Simplifier setup for HOL.
The tactic \verb|asm_full_simp_tac| is the one that is also used in
method \hyperlink{method.simp}{\mbox{\isa{simp}}} by default. The extra wrapping by the \verb|CHANGED| tactical ensures progress of simplification: identical goal
states are filtered out explicitly to make the raw tactic conform to
standard Isar method behaviour.
\medskip Method \hyperlink{method.my-simp}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}simp}}} can be used in Isar proofs like
this:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{notepad}\isamarkupfalse%
\isanewline
\isakeyword{begin}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{fix}\isamarkupfalse%
\ a\ b\ c\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp\ a\ b{\isaliteral{29}{\isacharparenright}}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
Here is a similar method that operates on all subgoals,
instead of just the first one.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
\ my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}all\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD\isanewline
\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}CHANGED\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}ALLGOALS\ {\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}full{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}tac\isanewline
\ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}HOL{\isaliteral{5F}{\isacharunderscore}}basic{\isaliteral{5F}{\isacharunderscore}}ss\ addsimps\ thms{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}rewrite\ all\ subgoals\ by\ given\ rules{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
\isanewline
\isanewline
\isacommand{notepad}\isamarkupfalse%
\isanewline
\isakeyword{begin}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{fix}\isamarkupfalse%
\ a\ b\ c\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}all\ a\ b{\isaliteral{29}{\isacharparenright}}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\medskip Apart from explicit arguments, common proof methods
typically work with a default configuration provided by the context.
As a shortcut to rule management we use a cheap solution via functor
\verb|Named_Thms| (see also \verb|~~/src/Pure/Tools/named_thms.ML|).%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ structure\ My{\isaliteral{5F}{\isacharunderscore}}Simps\ {\isaliteral{3D}{\isacharequal}}\isanewline
\ \ \ \ Named{\isaliteral{5F}{\isacharunderscore}}Thms\isanewline
\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}val\ name\ {\isaliteral{3D}{\isacharequal}}\ %
\isaantiq
binding\ my{\isaliteral{5F}{\isacharunderscore}}simp{}%
\endisaantiq
\ val\ description\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}simp\ rule{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
\isacommand{setup}\isamarkupfalse%
\ My{\isaliteral{5F}{\isacharunderscore}}Simps{\isaliteral{2E}{\isachardot}}setup%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
This provides ML access to a list of theorems in canonical
declaration order via \verb|My_Simps.get|. The user can add or
delete rules via the attribute \hyperlink{attribute.my-simp}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}simp}}}. The actual
proof method is now defined as before, but we append the explicit
arguments and the rules from the context.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
\ my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ thms\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ctxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ SIMPLE{\isaliteral{5F}{\isacharunderscore}}METHOD{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}fn\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
\ \ \ \ \ \ CHANGED\ {\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{5F}{\isacharunderscore}}full{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5F}{\isacharunderscore}}tac\isanewline
\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}HOL{\isaliteral{5F}{\isacharunderscore}}basic{\isaliteral{5F}{\isacharunderscore}}ss\ addsimps\ {\isaliteral{28}{\isacharparenleft}}thms\ {\isaliteral{40}{\isacharat}}\ My{\isaliteral{5F}{\isacharunderscore}}Simps{\isaliteral{2E}{\isachardot}}get\ ctxt{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}rewrite\ subgoal\ by\ given\ rules\ and\ my{\isaliteral{5F}{\isacharunderscore}}simp\ rules\ from\ the\ context{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
\medskip Method \hyperlink{method.my-simp'}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{27}{\isacharprime}}}}} can be used in Isar proofs
like this:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{notepad}\isamarkupfalse%
\isanewline
\isakeyword{begin}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{fix}\isamarkupfalse%
\ a\ b\ c\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isaliteral{5B}{\isacharbrackleft}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{27}{\isacharprime}}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
\medskip The \hyperlink{method.my-simp}{\mbox{\isa{my{\isaliteral{5F}{\isacharunderscore}}simp}}} variants defined above are
``simple'' methods, i.e.\ the goal facts are merely inserted as goal
premises by the \verb|SIMPLE_METHOD'| or \verb|SIMPLE_METHOD| wrapper.
For proof methods that are similar to the standard collection of
\hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}}
there is little more that can be done.
Note that using the primary goal facts in the same manner as the
method arguments obtained via concrete syntax or the context does
not meet the requirement of ``strong emphasis on facts'' of regular
proof methods, because rewrite rules as used above can be easily
ignored. A proof text ``\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{foo}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{my{\isaliteral{5F}{\isacharunderscore}}simp}'' where \isa{foo} is not used would
deceive the reader.
\medskip The technical treatment of rules from the context requires
further attention. Above we rebuild a fresh \verb|simpset| from
the arguments and \emph{all} rules retrieved from the context on
every invocation of the method. This does not scale to really large
collections of rules, which easily emerges in the context of a big
theory library, for example.
This is an inherent limitation of the simplistic rule management via
functor \verb|Named_Thms|, because it lacks tool-specific
storage and retrieval. More realistic applications require
efficient index-structures that organize theorems in a customized
manner, such as a discrimination net that is indexed by the
left-hand sides of rewrite rules. For variations on the Simplifier,
re-use of the existing type \verb|simpset| is adequate, but
scalability would require it be maintained statically within the
context data, not dynamically on each tool invocation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Attributes \label{sec:attributes}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
An \emph{attribute} is a function \isa{context\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ thm}, which means both a (generic) context and a theorem
can be modified simultaneously. In practice this mixed form is very
rare, instead attributes are presented either as \emph{declaration
attribute:} \isa{thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} or \emph{rule
attribute:} \isa{context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm}.
Attributes can have additional arguments via concrete syntax. There
is a collection of context-sensitive parsers for various logical
entities (types, terms, theorems). These already take care of
applying morphisms to the arguments when attribute expressions are
moved into a different context (see also \secref{sec:morphisms}).
When implementing declaration attributes, it is important to operate
exactly on the variant of the generic context that is provided by
the system, which is either global theory context or local proof
context. In particular, the background theory of a local context
must not be modified in this situation!%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{attribute}\verb|type attribute| \\
\indexdef{}{ML}{Thm.rule\_attribute}\verb|Thm.rule_attribute: (Context.generic -> thm -> thm) -> attribute| \\
\indexdef{}{ML}{Thm.declaration\_attribute}\verb|Thm.declaration_attribute: |\isasep\isanewline%
\verb| (thm -> Context.generic -> Context.generic) -> attribute| \\
\indexdef{}{ML}{Attrib.setup}\verb|Attrib.setup: binding -> attribute context_parser ->|\isasep\isanewline%
\verb| string -> theory -> theory| \\
\end{mldecls}
\begin{description}
\item Type \verb|attribute| represents attributes as concrete
type alias.
\item \verb|Thm.rule_attribute|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ context\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ rule{\isaliteral{29}{\isacharparenright}}} wraps
a context-dependent rule (mapping on \verb|thm|) as attribute.
\item \verb|Thm.declaration_attribute|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ decl{\isaliteral{29}{\isacharparenright}}}
wraps a theorem-dependent declaration (mapping on \verb|Context.generic|) as attribute.
\item \verb|Attrib.setup|~\isa{name\ parser\ description} provides
the functionality of the Isar command \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}} as
ML function.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{attributes}\hypertarget{ML antiquotation.attributes}{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
\end{matharray}
\begin{railoutput}
\rail@begin{1}{}
\rail@term{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}}[]
\rail@nont{\isa{attributes}}[]
\rail@end
\end{railoutput}
\begin{description}
\item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}attributes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}} embeds attribute source
representation into the ML text, which is particularly useful with
declarations like \verb|Local_Theory.note|. Attribute names are
internalized at compile time, but the source is unevaluated. This
means attributes with formal arguments (types, terms, theorems) may
be subject to odd effects of dynamic scoping!
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isadelimmlex
%
\endisadelimmlex
%
\isatagmlex
%
\begin{isamarkuptext}%
See also \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}} in
\cite{isabelle-isar-ref} which includes some abstract examples.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
\isadelimmlex
%
\endisadelimmlex
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: