
diff -r e7418f8d49fe -r d468d72a458f doc-src/IsarImplementation/Thy/document/Isar.tex
--- 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:




