--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Aug 27 16:48:41 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,974 +0,0 @@
-%
-\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}{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 that operates on
- subgoal 1. Goal facts are inserted into the subgoal then the \isa{tactic} is applied.
-
- \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: