doc-src/IsarRef/Thy/document/Generic.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 35613 9d3ff36ad4e1
child 40291 012ed4426fda
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Generic}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Generic\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Configuration options%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \begin{isamarkuptext}%
    30 Isabelle/Pure maintains a record of named configuration options
    31   within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|.  Tools may declare
    32   options in ML, and then refer to these values (relative to the
    33   context).  Thus global reference variables are easily avoided.  The
    34   user may change the value of a configuration option by means of an
    35   associated attribute of the same name.  This form of context
    36   declaration works particularly well with commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
    37 
    38   For historical reasons, some tools cannot take the full proof
    39   context into account and merely refer to the background theory.
    40   This is accommodated by configuration options being declared as
    41   ``global'', which may not be changed within a local context.
    42 
    43   \begin{matharray}{rcll}
    44     \indexdef{}{command}{print\_configs}\hypertarget{command.print-configs}{\hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    45   \end{matharray}
    46 
    47   \begin{rail}
    48     name ('=' ('true' | 'false' | int | name))?
    49   \end{rail}
    50 
    51   \begin{description}
    52   
    53   \item \hyperlink{command.print-configs}{\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}} prints the available configuration
    54   options, with names, types, and current values.
    55   
    56   \item \isa{{\isachardoublequote}name\ {\isacharequal}\ value{\isachardoublequote}} as an attribute expression modifies the
    57   named option, with the syntax of the value depending on the option's
    58   type.  For \verb|bool| the default value is \isa{true}.  Any
    59   attempt to change a global option in a local context is ignored.
    60 
    61   \end{description}%
    62 \end{isamarkuptext}%
    63 \isamarkuptrue%
    64 %
    65 \isamarkupsection{Basic proof tools%
    66 }
    67 \isamarkuptrue%
    68 %
    69 \isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
    70 }
    71 \isamarkuptrue%
    72 %
    73 \begin{isamarkuptext}%
    74 \begin{matharray}{rcl}
    75     \indexdef{}{method}{unfold}\hypertarget{method.unfold}{\hyperlink{method.unfold}{\mbox{\isa{unfold}}}} & : & \isa{method} \\
    76     \indexdef{}{method}{fold}\hypertarget{method.fold}{\hyperlink{method.fold}{\mbox{\isa{fold}}}} & : & \isa{method} \\
    77     \indexdef{}{method}{insert}\hypertarget{method.insert}{\hyperlink{method.insert}{\mbox{\isa{insert}}}} & : & \isa{method} \\[0.5ex]
    78     \indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
    79     \indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
    80     \indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
    81     \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
    82     \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
    83   \end{matharray}
    84 
    85   \begin{rail}
    86     ('fold' | 'unfold' | 'insert') thmrefs
    87     ;
    88     ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
    89     ;
    90   \end{rail}
    91 
    92   \begin{description}
    93   
    94   \item \hyperlink{method.unfold}{\mbox{\isa{unfold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{method.fold}{\mbox{\isa{fold}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand (or fold back) the given definitions throughout
    95   all goals; any chained facts provided are inserted into the goal and
    96   subject to rewriting as well.
    97 
    98   \item \hyperlink{method.insert}{\mbox{\isa{insert}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} inserts theorems as facts
    99   into all goals of the proof state.  Note that current facts
   100   indicated for forward chaining are ignored.
   101 
   102   \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}}
   103   method (see \secref{sec:pure-meth-att}), but apply rules by
   104   elim-resolution, destruct-resolution, and forward-resolution,
   105   respectively \cite{isabelle-implementation}.  The optional natural
   106   number argument (default 0) specifies additional assumption steps to
   107   be performed here.
   108 
   109   Note that these methods are improper ones, mainly serving for
   110   experimentation and tactic script emulation.  Different modes of
   111   basic rule application are usually expressed in Isar at the proof
   112   language level, rather than via implicit proof state manipulations.
   113   For example, a proper single-step elimination would be done using
   114   the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
   115   facts.
   116 
   117   \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
   118   the identity of the ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' method combinator (cf.\
   119   \secref{sec:proof-meth}).
   120 
   121   \item \hyperlink{method.fail}{\mbox{\isa{fail}}} yields an empty result sequence; it is the
   122   identity of the ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' method combinator (cf.\
   123   \secref{sec:proof-meth}).
   124 
   125   \end{description}
   126 
   127   \begin{matharray}{rcl}
   128     \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
   129     \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
   130     \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
   131     \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
   132     \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
   133     \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\[0.5ex]
   134     \indexdef{}{attribute}{rotated}\hypertarget{attribute.rotated}{\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}} & : & \isa{attribute} \\
   135     \indexdef{Pure}{attribute}{elim\_format}\hypertarget{attribute.Pure.elim-format}{\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}}} & : & \isa{attribute} \\
   136     \indexdef{}{attribute}{standard}\hypertarget{attribute.standard}{\hyperlink{attribute.standard}{\mbox{\isa{standard}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
   137     \indexdef{}{attribute}{no\_vars}\hypertarget{attribute.no-vars}{\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
   138   \end{matharray}
   139 
   140   \begin{rail}
   141     'tagged' name name
   142     ;
   143     'untagged' name
   144     ;
   145     ('THEN' | 'COMP') ('[' nat ']')? thmref
   146     ;
   147     ('unfolded' | 'folded') thmrefs
   148     ;
   149     'rotated' ( int )?
   150   \end{rail}
   151 
   152   \begin{description}
   153 
   154   \item \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}~\isa{{\isachardoublequote}name\ value{\isachardoublequote}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}~\isa{name} add and remove \emph{tags} of some theorem.
   155   Tags may be any list of string pairs that serve as formal comment.
   156   The first string is considered the tag name, the second its value.
   157   Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
   158 
   159   \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
   160   compose rules by resolution.  \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
   161   first premise of \isa{a} (an alternative position may be also
   162   specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
   163   lifting process that is normally intended (cf.\ \verb|op RS| and
   164   \verb|op COMP| in \cite{isabelle-implementation}).
   165   
   166   \item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand and fold back again the given
   167   definitions throughout a rule.
   168 
   169   \item \hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n} rotate the premises of a
   170   theorem by \isa{n} (default 1).
   171 
   172   \item \hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}} turns a destruction rule into
   173   elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
   174   
   175   Note that the Classical Reasoner (\secref{sec:classical}) provides
   176   its own version of this operation.
   177 
   178   \item \hyperlink{attribute.standard}{\mbox{\isa{standard}}} puts a theorem into the standard form of
   179   object-rules at the outermost theory level.  Note that this
   180   operation violates the local proof context (including active
   181   locales).
   182 
   183   \item \hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} replaces schematic variables by free
   184   ones; this is mainly for tuning output of pretty printed theorems.
   185 
   186   \end{description}%
   187 \end{isamarkuptext}%
   188 \isamarkuptrue%
   189 %
   190 \isamarkupsubsection{Low-level equational reasoning%
   191 }
   192 \isamarkuptrue%
   193 %
   194 \begin{isamarkuptext}%
   195 \begin{matharray}{rcl}
   196     \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isa{method} \\
   197     \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isa{method} \\
   198     \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isa{method} \\
   199   \end{matharray}
   200 
   201   \begin{rail}
   202     'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
   203     ;
   204     'split' ('(' 'asm' ')')? thmrefs
   205     ;
   206   \end{rail}
   207 
   208   These methods provide low-level facilities for equational reasoning
   209   that are intended for specialized applications only.  Normally,
   210   single step calculations would be performed in a structured text
   211   (see also \secref{sec:calculation}), while the Simplifier methods
   212   provide the canonical way for automated normalization (see
   213   \secref{sec:simplifier}).
   214 
   215   \begin{description}
   216 
   217   \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq} performs a single substitution step
   218   using rule \isa{eq}, which may be either a meta or object
   219   equality.
   220 
   221   \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}} substitutes in an
   222   assumption.
   223 
   224   \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}} performs several
   225   substitutions in the conclusion. The numbers \isa{i} to \isa{j}
   226   indicate the positions to substitute at.  Positions are ordered from
   227   the top of the term tree moving down from left to right. For
   228   example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
   229   where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}}, 2 to the whole term, and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
   230 
   231   If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
   232   (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
   233   assume all substitutions are performed simultaneously.  Otherwise
   234   the behaviour of \isa{subst} is not specified.
   235 
   236   \item \hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}} performs the
   237   substitutions in the assumptions. The positions refer to the
   238   assumptions in order from left to right.  For example, given in a
   239   goal of the form \isa{{\isachardoublequote}P\ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}, position 1 of
   240   commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is the subterm \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and
   241   position 2 is the subterm \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
   242 
   243   \item \hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}} performs substitution using some
   244   assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
   245 
   246   \item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} performs single-step case
   247   splitting using the given rules.  By default, splitting is performed
   248   in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to
   249   operate on assumptions instead.
   250   
   251   Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
   252   application of split rules as declared in the current context.
   253 
   254   \end{description}%
   255 \end{isamarkuptext}%
   256 \isamarkuptrue%
   257 %
   258 \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
   259 }
   260 \isamarkuptrue%
   261 %
   262 \begin{isamarkuptext}%
   263 The following improper proof methods emulate traditional tactics.
   264   These admit direct access to the goal state, which is normally
   265   considered harmful!  In particular, this may involve both numbered
   266   goal addressing (default 1), and dynamic instantiation within the
   267   scope of some subgoal.
   268 
   269   \begin{warn}
   270     Dynamic instantiations refer to universally quantified parameters
   271     of a subgoal (the dynamic context) rather than fixed variables and
   272     term abbreviations of a (static) Isar context.
   273   \end{warn}
   274 
   275   Tactic emulation methods, unlike their ML counterparts, admit
   276   simultaneous instantiation from both dynamic and static contexts.
   277   If names occur in both contexts goal parameters hide locally fixed
   278   variables.  Likewise, schematic variables refer to term
   279   abbreviations, if present in the static context.  Otherwise the
   280   schematic variable is interpreted as a schematic variable and left
   281   to be solved by unification with certain parts of the subgoal.
   282 
   283   Note that the tactic emulation proof methods in Isabelle/Isar are
   284   consistently named \isa{foo{\isacharunderscore}tac}.  Note also that variable names
   285   occurring on left hand sides of instantiations must be preceded by a
   286   question mark if they coincide with a keyword or contain dots.  This
   287   is consistent with the attribute \hyperlink{attribute.where}{\mbox{\isa{where}}} (see
   288   \secref{sec:pure-meth-att}).
   289 
   290   \begin{matharray}{rcl}
   291     \indexdef{}{method}{rule\_tac}\hypertarget{method.rule-tac}{\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   292     \indexdef{}{method}{erule\_tac}\hypertarget{method.erule-tac}{\hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   293     \indexdef{}{method}{drule\_tac}\hypertarget{method.drule-tac}{\hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   294     \indexdef{}{method}{frule\_tac}\hypertarget{method.frule-tac}{\hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   295     \indexdef{}{method}{cut\_tac}\hypertarget{method.cut-tac}{\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   296     \indexdef{}{method}{thin\_tac}\hypertarget{method.thin-tac}{\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   297     \indexdef{}{method}{subgoal\_tac}\hypertarget{method.subgoal-tac}{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   298     \indexdef{}{method}{rename\_tac}\hypertarget{method.rename-tac}{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   299     \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate-tac}{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   300     \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   301     \indexdef{}{method}{raw\_tactic}\hypertarget{method.raw-tactic}{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
   302   \end{matharray}
   303 
   304   \begin{rail}
   305     ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
   306     ( insts thmref | thmrefs )
   307     ;
   308     'subgoal_tac' goalspec? (prop +)
   309     ;
   310     'rename_tac' goalspec? (name +)
   311     ;
   312     'rotate_tac' goalspec? int?
   313     ;
   314     ('tactic' | 'raw_tactic') text
   315     ;
   316 
   317     insts: ((name '=' term) + 'and') 'in'
   318     ;
   319   \end{rail}
   320 
   321 \begin{description}
   322 
   323   \item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc. do resolution of rules with explicit
   324   instantiation.  This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
   325 
   326   Multiple rules may be only given if there is no instantiation; then
   327   \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
   328   \cite{isabelle-implementation}).
   329 
   330   \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}} inserts facts into the proof state as
   331   assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
   332   \cite{isabelle-implementation}.  Note that the scope of schematic
   333   variables is spread over the main goal statement.  Instantiations
   334   may be given as well, see also ML tactic \verb|cut_inst_tac| in
   335   \cite{isabelle-implementation}.
   336 
   337   \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} deletes the specified assumption
   338   from a subgoal; note that \isa{{\isasymphi}} may contain schematic variables.
   339   See also \verb|thin_tac| in \cite{isabelle-implementation}.
   340 
   341   \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} adds \isa{{\isasymphi}} as an
   342   assumption to a subgoal.  See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
   343 
   344   \item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} renames parameters of a
   345   goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the
   346   \emph{suffix} of variables.
   347 
   348   \item \hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n} rotates the assumptions of a
   349   goal by \isa{n} positions: from right to left if \isa{n} is
   350   positive, and from left to right if \isa{n} is negative; the
   351   default value is 1.  See also \verb|rotate_tac| in
   352   \cite{isabelle-implementation}.
   353 
   354   \item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} produces a proof method from
   355   any ML text of type \verb|tactic|.  Apart from the usual ML
   356   environment and the current proof context, the ML code may refer to
   357   the locally bound values \verb|facts|, which indicates any
   358   current facts used for forward-chaining.
   359 
   360   \item \hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}} is similar to \hyperlink{method.tactic}{\mbox{\isa{tactic}}}, but
   361   presents the goal state in its raw internal form, where simultaneous
   362   subgoals appear as conjunction of the logical framework instead of
   363   the usual split into several subgoals.  While feature this is useful
   364   for debugging of complex method definitions, it should not never
   365   appear in production theories.
   366 
   367   \end{description}%
   368 \end{isamarkuptext}%
   369 \isamarkuptrue%
   370 %
   371 \isamarkupsection{The Simplifier \label{sec:simplifier}%
   372 }
   373 \isamarkuptrue%
   374 %
   375 \isamarkupsubsection{Simplification methods%
   376 }
   377 \isamarkuptrue%
   378 %
   379 \begin{isamarkuptext}%
   380 \begin{matharray}{rcl}
   381     \indexdef{}{method}{simp}\hypertarget{method.simp}{\hyperlink{method.simp}{\mbox{\isa{simp}}}} & : & \isa{method} \\
   382     \indexdef{}{method}{simp\_all}\hypertarget{method.simp-all}{\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}} & : & \isa{method} \\
   383   \end{matharray}
   384 
   385   \indexouternonterm{simpmod}
   386   \begin{rail}
   387     ('simp' | 'simp_all') opt? (simpmod *)
   388     ;
   389 
   390     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
   391     ;
   392     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
   393       'split' (() | 'add' | 'del')) ':' thmrefs
   394     ;
   395   \end{rail}
   396 
   397   \begin{description}
   398 
   399   \item \hyperlink{method.simp}{\mbox{\isa{simp}}} invokes the Simplifier, after declaring
   400   additional rules according to the arguments given.  Note that the
   401   \railtterm{only} modifier first removes all other rewrite rules,
   402   congruences, and looper tactics (including splits), and then behaves
   403   like \railtterm{add}.
   404 
   405   \medskip The \railtterm{cong} modifiers add or delete Simplifier
   406   congruence rules (see also \cite{isabelle-ref}), the default is to
   407   add.
   408 
   409   \medskip The \railtterm{split} modifiers add or delete rules for the
   410   Splitter (see also \cite{isabelle-ref}), the default is to add.
   411   This works only if the Simplifier method has been properly setup to
   412   include the Splitter (all major object logics such HOL, HOLCF, FOL,
   413   ZF do this already).
   414 
   415   \item \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} is similar to \hyperlink{method.simp}{\mbox{\isa{simp}}}, but acts on
   416   all goals (backwards from the last to the first one).
   417 
   418   \end{description}
   419 
   420   By default the Simplifier methods take local assumptions fully into
   421   account, using equational assumptions in the subsequent
   422   normalization process, or simplifying assumptions themselves (cf.\
   423   \verb|asm_full_simp_tac| in \cite{isabelle-ref}).  In structured
   424   proofs this is usually quite well behaved in practice: just the
   425   local premises of the actual goal are involved, additional facts may
   426   be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
   427   \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
   428 
   429   Additional Simplifier options may be specified to tune the behavior
   430   further (mostly for unstructured scripts with many accidental local
   431   facts): ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}}'' means assumptions are ignored
   432   completely (cf.\ \verb|simp_tac|), ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}}'' means
   433   assumptions are used in the simplification of the conclusion but are
   434   not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}}'' means assumptions are simplified but are not used
   435   in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|).  For compatibility reasons, there is also an option
   436   ``\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}}'', which means that an assumption is only used
   437   for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
   438 
   439   The configuration option \isa{{\isachardoublequote}depth{\isacharunderscore}limit{\isachardoublequote}} limits the number of
   440   recursive invocations of the simplifier during conditional
   441   rewriting.
   442 
   443   \medskip The Splitter package is usually configured to work as part
   444   of the Simplifier.  The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isachardoublequote}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}''.  There is also a separate \isa{split}
   445   method available for single-step case splitting.%
   446 \end{isamarkuptext}%
   447 \isamarkuptrue%
   448 %
   449 \isamarkupsubsection{Declaring rules%
   450 }
   451 \isamarkuptrue%
   452 %
   453 \begin{isamarkuptext}%
   454 \begin{matharray}{rcl}
   455     \indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   456     \indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
   457     \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
   458     \indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
   459   \end{matharray}
   460 
   461   \begin{rail}
   462     ('simp' | 'cong' | 'split') (() | 'add' | 'del')
   463     ;
   464   \end{rail}
   465 
   466   \begin{description}
   467 
   468   \item \hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}} prints the collection of rules
   469   declared to the Simplifier, which is also known as ``simpset''
   470   internally \cite{isabelle-ref}.
   471 
   472   \item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
   473 
   474   \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
   475 
   476   \item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
   477 
   478   \end{description}%
   479 \end{isamarkuptext}%
   480 \isamarkuptrue%
   481 %
   482 \isamarkupsubsection{Simplification procedures%
   483 }
   484 \isamarkuptrue%
   485 %
   486 \begin{isamarkuptext}%
   487 \begin{matharray}{rcl}
   488     \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc-setup}{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   489     simproc & : & \isa{attribute} \\
   490   \end{matharray}
   491 
   492   \begin{rail}
   493     'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
   494     ;
   495 
   496     'simproc' (('add' ':')? | 'del' ':') (name+)
   497     ;
   498   \end{rail}
   499 
   500   \begin{description}
   501 
   502   \item \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}} defines a named simplification
   503   procedure that is invoked by the Simplifier whenever any of the
   504   given term patterns match the current redex.  The implementation,
   505   which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
   506   supposed to be some proven rewrite rule \isa{{\isachardoublequote}r\ {\isasymequiv}\ r{\isacharprime}{\isachardoublequote}} (or a
   507   generalized version), or \verb|NONE| to indicate failure.  The
   508   \verb|simpset| argument holds the full context of the current
   509   Simplifier invocation, including the actual Isar proof context.  The
   510   \verb|morphism| informs about the difference of the original
   511   compilation context wrt.\ the one of the actual application later
   512   on.  The optional \hyperlink{keyword.identifier}{\mbox{\isa{\isakeyword{identifier}}}} specifies theorems that
   513   represent the logical content of the abstract theory of this
   514   simproc.
   515 
   516   Morphisms and identifiers are only relevant for simprocs that are
   517   defined within a local target context, e.g.\ in a locale.
   518 
   519   \item \isa{{\isachardoublequote}simproc\ add{\isacharcolon}\ name{\isachardoublequote}} and \isa{{\isachardoublequote}simproc\ del{\isacharcolon}\ name{\isachardoublequote}}
   520   add or delete named simprocs to the current Simplifier context.  The
   521   default is to add a simproc.  Note that \hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}}
   522   already adds the new simproc to the subsequent context.
   523 
   524   \end{description}%
   525 \end{isamarkuptext}%
   526 \isamarkuptrue%
   527 %
   528 \isamarkupsubsection{Forward simplification%
   529 }
   530 \isamarkuptrue%
   531 %
   532 \begin{isamarkuptext}%
   533 \begin{matharray}{rcl}
   534     \indexdef{}{attribute}{simplified}\hypertarget{attribute.simplified}{\hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}} & : & \isa{attribute} \\
   535   \end{matharray}
   536 
   537   \begin{rail}
   538     'simplified' opt? thmrefs?
   539     ;
   540 
   541     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   542     ;
   543   \end{rail}
   544 
   545   \begin{description}
   546   
   547   \item \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} causes a theorem to
   548   be simplified, either by exactly the specified rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}, or the implicit Simplifier context if no arguments are given.
   549   The result is fully simplified by default, including assumptions and
   550   conclusion; the options \isa{no{\isacharunderscore}asm} etc.\ tune the Simplifier in
   551   the same way as the for the \isa{simp} method.
   552 
   553   Note that forward simplification restricts the simplifier to its
   554   most basic operation of term rewriting; solver and looper tactics
   555   \cite{isabelle-ref} are \emph{not} involved here.  The \isa{simplified} attribute should be only rarely required under normal
   556   circumstances.
   557 
   558   \end{description}%
   559 \end{isamarkuptext}%
   560 \isamarkuptrue%
   561 %
   562 \isamarkupsection{The Classical Reasoner \label{sec:classical}%
   563 }
   564 \isamarkuptrue%
   565 %
   566 \isamarkupsubsection{Basic methods%
   567 }
   568 \isamarkuptrue%
   569 %
   570 \begin{isamarkuptext}%
   571 \begin{matharray}{rcl}
   572     \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
   573     \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
   574     \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
   575     \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
   576   \end{matharray}
   577 
   578   \begin{rail}
   579     ('rule' | 'intro' | 'elim') thmrefs?
   580     ;
   581   \end{rail}
   582 
   583   \begin{description}
   584 
   585   \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
   586   refinement over the primitive one (see \secref{sec:pure-meth-att}).
   587   Both versions essentially work the same, but the classical version
   588   observes the classical rule context in addition to that of
   589   Isabelle/Pure.
   590 
   591   Common object logics (HOL, ZF, etc.) declare a rich collection of
   592   classical rules (even if these would qualify as intuitionistic
   593   ones), but only few declarations to the rule context of
   594   Isabelle/Pure (\secref{sec:pure-meth-att}).
   595 
   596   \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
   597   deriving any result from both \isa{{\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}} and \isa{A}.  Chained
   598   facts, which are guaranteed to participate, may appear in either
   599   order.
   600 
   601   \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
   602   by intro- or elim-resolution, after having inserted any chained
   603   facts.  Exactly the rules given as arguments are taken into account;
   604   this allows fine-tuned decomposition of a proof problem, in contrast
   605   to common automated tools.
   606 
   607   \end{description}%
   608 \end{isamarkuptext}%
   609 \isamarkuptrue%
   610 %
   611 \isamarkupsubsection{Automated methods%
   612 }
   613 \isamarkuptrue%
   614 %
   615 \begin{isamarkuptext}%
   616 \begin{matharray}{rcl}
   617     \indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isa{method} \\
   618     \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
   619     \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
   620     \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
   621     \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
   622     \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
   623   \end{matharray}
   624 
   625   \indexouternonterm{clamod}
   626   \begin{rail}
   627     'blast' nat? (clamod *)
   628     ;
   629     ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
   630     ;
   631 
   632     clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   633     ;
   634   \end{rail}
   635 
   636   \begin{description}
   637 
   638   \item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
   639   \verb|blast_tac| in \cite{isabelle-ref}).  The optional argument
   640   specifies a user-supplied search bound (default 20).
   641 
   642   \item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.safe}{\mbox{\isa{safe}}}, and \hyperlink{method.clarify}{\mbox{\isa{clarify}}} refer to the generic classical
   643   reasoner.  See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
   644   information.
   645 
   646   \end{description}
   647 
   648   Any of the above methods support additional modifiers of the context
   649   of classical rules.  Their semantics is analogous to the attributes
   650   given before.  Facts provided by forward chaining are inserted into
   651   the goal before commencing proof search.%
   652 \end{isamarkuptext}%
   653 \isamarkuptrue%
   654 %
   655 \isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
   656 }
   657 \isamarkuptrue%
   658 %
   659 \begin{isamarkuptext}%
   660 \begin{matharray}{rcl}
   661     \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
   662     \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
   663     \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
   664     \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
   665     \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
   666     \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
   667   \end{matharray}
   668 
   669   \indexouternonterm{clasimpmod}
   670   \begin{rail}
   671     'auto' (nat nat)? (clasimpmod *)
   672     ;
   673     ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
   674     ;
   675 
   676     clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
   677       ('cong' | 'split') (() | 'add' | 'del') |
   678       'iff' (((() | 'add') '?'?) | 'del') |
   679       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
   680   \end{rail}
   681 
   682   \begin{description}
   683 
   684   \item \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} provide access
   685   to Isabelle's combined simplification and classical reasoning
   686   tactics.  These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
   687   added as wrapper, see \cite{isabelle-ref} for more information.  The
   688   modifier arguments correspond to those given in
   689   \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
   690   the ones related to the Simplifier are prefixed by \railtterm{simp}
   691   here.
   692 
   693   Facts provided by forward chaining are inserted into the goal before
   694   doing the search.
   695 
   696   \end{description}%
   697 \end{isamarkuptext}%
   698 \isamarkuptrue%
   699 %
   700 \isamarkupsubsection{Declaring rules%
   701 }
   702 \isamarkuptrue%
   703 %
   704 \begin{isamarkuptext}%
   705 \begin{matharray}{rcl}
   706     \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   707     \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
   708     \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
   709     \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
   710     \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
   711     \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
   712   \end{matharray}
   713 
   714   \begin{rail}
   715     ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
   716     ;
   717     'rule' 'del'
   718     ;
   719     'iff' (((() | 'add') '?'?) | 'del')
   720     ;
   721   \end{rail}
   722 
   723   \begin{description}
   724 
   725   \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}} prints the collection of rules
   726   declared to the Classical Reasoner, which is also known as
   727   ``claset'' internally \cite{isabelle-ref}.
   728   
   729   \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
   730   declare introduction, elimination, and destruction rules,
   731   respectively.  By default, rules are considered as \emph{unsafe}
   732   (i.e.\ not applied blindly without backtracking), while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' classifies as \emph{safe}.  Rule declarations marked by
   733   ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' coincide with those of Isabelle/Pure, cf.\
   734   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
   735   of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method).  The optional natural number
   736   specifies an explicit weight argument, which is ignored by automated
   737   tools, but determines the search order of single rule steps.
   738 
   739   \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes introduction,
   740   elimination, or destruction rules from the context.
   741 
   742   \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
   743   Simplifier and the Classical reasoner at the same time.
   744   Non-conditional rules result in a ``safe'' introduction and
   745   elimination pair; conditional ones are considered ``unsafe''.  Rules
   746   with negative conclusion are automatically inverted (using \isa{{\isachardoublequote}{\isasymnot}{\isachardoublequote}}-elimination internally).
   747 
   748   The ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
   749   the Isabelle/Pure context only, and omits the Simplifier
   750   declaration.
   751 
   752   \end{description}%
   753 \end{isamarkuptext}%
   754 \isamarkuptrue%
   755 %
   756 \isamarkupsubsection{Classical operations%
   757 }
   758 \isamarkuptrue%
   759 %
   760 \begin{isamarkuptext}%
   761 \begin{matharray}{rcl}
   762     \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
   763   \end{matharray}
   764 
   765   \begin{description}
   766 
   767   \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
   768   elimination, by resolving with the classical swap principle \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ B{\isacharparenright}{\isachardoublequote}}.
   769 
   770   \end{description}%
   771 \end{isamarkuptext}%
   772 \isamarkuptrue%
   773 %
   774 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
   775 }
   776 \isamarkuptrue%
   777 %
   778 \begin{isamarkuptext}%
   779 \begin{matharray}{rcl}
   780     \indexdef{}{command}{judgment}\hypertarget{command.judgment}{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   781     \indexdef{}{method}{atomize}\hypertarget{method.atomize}{\hyperlink{method.atomize}{\mbox{\isa{atomize}}}} & : & \isa{method} \\
   782     \indexdef{}{attribute}{atomize}\hypertarget{attribute.atomize}{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}} & : & \isa{attribute} \\
   783     \indexdef{}{attribute}{rule\_format}\hypertarget{attribute.rule-format}{\hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}}} & : & \isa{attribute} \\
   784     \indexdef{}{attribute}{rulify}\hypertarget{attribute.rulify}{\hyperlink{attribute.rulify}{\mbox{\isa{rulify}}}} & : & \isa{attribute} \\
   785   \end{matharray}
   786 
   787   The very starting point for any Isabelle object-logic is a ``truth
   788   judgment'' that links object-level statements to the meta-logic
   789   (with its minimal language of \isa{prop} that covers universal
   790   quantification \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and implication \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}).
   791 
   792   Common object-logics are sufficiently expressive to internalize rule
   793   statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} within their own
   794   language.  This is useful in certain situations where a rule needs
   795   to be viewed as an atomic statement from the meta-level perspective,
   796   e.g.\ \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}} versus \isa{{\isachardoublequote}{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x{\isachardoublequote}}.
   797 
   798   From the following language elements, only the \hyperlink{method.atomize}{\mbox{\isa{atomize}}}
   799   method and \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} attribute are occasionally
   800   required by end-users, the rest is for those who need to setup their
   801   own object-logic.  In the latter case existing formulations of
   802   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
   803 
   804   Generic tools may refer to the information provided by object-logic
   805   declarations internally.
   806 
   807   \begin{rail}
   808     'judgment' constdecl
   809     ;
   810     'atomize' ('(' 'full' ')')?
   811     ;
   812     'rule_format' ('(' 'noasm' ')')?
   813     ;
   814   \end{rail}
   815 
   816   \begin{description}
   817   
   818   \item \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares constant
   819   \isa{c} as the truth judgment of the current object-logic.  Its
   820   type \isa{{\isasymsigma}} should specify a coercion of the category of
   821   object-level propositions to \isa{prop} of the Pure meta-logic;
   822   the mixfix annotation \isa{{\isachardoublequote}{\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} would typically just link the
   823   object language (internally of syntactic category \isa{logic})
   824   with that of \isa{prop}.  Only one \hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}
   825   declaration may be given in any theory development.
   826   
   827   \item \hyperlink{method.atomize}{\mbox{\isa{atomize}}} (as a method) rewrites any non-atomic
   828   premises of a sub-goal, using the meta-level equations declared via
   829   \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand.  As a result,
   830   heavily nested goals become amenable to fundamental operations such
   831   as resolution (cf.\ the \hyperlink{method.rule}{\mbox{\isa{rule}}} method).  Giving the ``\isa{{\isachardoublequote}{\isacharparenleft}full{\isacharparenright}{\isachardoublequote}}'' option here means to turn the whole subgoal into an
   832   object-statement (if possible), including the outermost parameters
   833   and assumptions as well.
   834 
   835   A typical collection of \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} rules for a particular
   836   object-logic would provide an internalization for each of the
   837   connectives of \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}}.
   838   Meta-level conjunction should be covered as well (this is
   839   particularly important for locales, see \secref{sec:locale}).
   840 
   841   \item \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} rewrites a theorem by the equalities
   842   declared as \hyperlink{attribute.rulify}{\mbox{\isa{rulify}}} rules in the current object-logic.
   843   By default, the result is fully normalized, including assumptions
   844   and conclusions at any depth.  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} option
   845   restricts the transformation to the conclusion of a rule.
   846 
   847   In common object-logics (HOL, FOL, ZF), the effect of \hyperlink{attribute.rule-format}{\mbox{\isa{rule{\isacharunderscore}format}}} is to replace (bounded) universal quantification
   848   (\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}) and implication (\isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}}) by the corresponding
   849   rule statements over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}.
   850 
   851   \end{description}%
   852 \end{isamarkuptext}%
   853 \isamarkuptrue%
   854 %
   855 \isadelimtheory
   856 %
   857 \endisadelimtheory
   858 %
   859 \isatagtheory
   860 \isacommand{end}\isamarkupfalse%
   861 %
   862 \endisatagtheory
   863 {\isafoldtheory}%
   864 %
   865 \isadelimtheory
   866 %
   867 \endisadelimtheory
   868 \isanewline
   869 \end{isabellebody}%
   870 %%% Local Variables:
   871 %%% mode: latex
   872 %%% TeX-master: "root"
   873 %%% End: