\chapter{Generic tools and packages}\label{ch:gen-tools}

\section{Theory specification commands}

\subsection{Axiomatic type classes}\label{sec:axclass}

\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}

\begin{matharray}{rcl}

  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\

  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

  intro_classes & : & \isarmeth \\

\end{matharray}

Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}

interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic

may make use of this light-weight mechanism of abstract theories

\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type

classes in Isabelle \cite{isabelle-axclass} that is part of the standard

Isabelle documentation.

\begin{rail}

  'axclass' classdecl (axmdecl prop +)

  ;

  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)

  ;

\end{rail}

\begin{descr}

\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as

  the intersection of existing classes, with additional axioms holding.  Class

  axioms may not contain more than one type variable.  The class axioms (with

  implicit sort constraints added) are bound to the given names.  Furthermore

  a class introduction rule is generated (being bound as

  $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to

  support instantiation proofs of this class.

  The ``axioms'' are stored as theorems according to the given name

  specifications, adding the class name $c$ as name space prefix; the same

  facts are also stored collectively as $c_class{\dtt}axioms$.

\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a

  goal stating a class relation or type arity.  The proof would usually

  proceed by $intro_classes$, and then establish the characteristic theorems

  of the type classes involved.  After finishing the proof, the theory will be

  augmented by a type signature declaration corresponding to the resulting

  theorem.

\item [$intro_classes$] repeatedly expands all class introduction rules of

  this theory.  Note that this method usually needs not be named explicitly,

  as it is already included in the default proof step (of $\PROOFNAME$ etc.).

  In particular, instantiation of trivial (syntactic) classes may be performed

  by a single ``$\DDOT$'' proof step.

\end{descr}

\subsection{Locales and local contexts}\label{sec:locale}

Locales are named local contexts, consisting of a list of declaration elements

that are modeled after the Isar proof context commands (cf.\

\S\ref{sec:proof-context}).

\subsubsection{Localized commands}

Existing locales may be augmented later on by adding new facts.  Note that the

actual context definition may not be changed!  Several theory commands that

produce facts in some way are available in ``localized'' versions, referring

to a named locale instead of the global theory context.

\indexouternonterm{locale}

\begin{rail}

  locale: '(' 'in' name ')'

  ;

\end{rail}

Emerging facts of localized commands are stored in two versions, both in the

target locale and the theory (after export).  The latter view produces a

qualified binding, using the locale name as a name space prefix.

For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from

the locale context of $loc$ and augments its body by an appropriate

``$\isarkeyword{notes}$'' element (see below).  The exported view of $a$,

after discharging the locale context, is stored as $loc{.}a$ within the global

theory.  A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly,

only that the fact emerges through the subsequent proof, which may refer to

the full infrastructure of the locale context (covering local parameters with

typing and concrete syntax, assumptions, definitions etc.).  Most notably,

fact declarations of the locale are active during the proof as well (e.g.\ 

local $simp$ rules).

As a general principle, results exported from a locale context acquire

additional premises according to the specification.  Usually this is only a

single predicate according to the standard ``closed'' view of locale

specifications.

\subsubsection{Locale specifications}

\indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}

\begin{matharray}{rcl}

  \isarcmd{locale} & : & \isarkeep{theory} \\

  \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\

  \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\

\end{matharray}

\indexouternonterm{contextexpr}\indexouternonterm{contextelem}

\railalias{printlocale}{print\_locale}

\railterm{printlocale}

\begin{rail}

  'locale' ('(open)')? name ('=' localeexpr)?

  ;

  printlocale '!'? localeexpr

  ;

  localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))

  ;

  contextexpr: nameref | '(' contextexpr ')' |

  (contextexpr (name mixfix? +)) | (contextexpr + '+')

  ;

  contextelem: fixes | constrains | assumes | defines | notes | includes

  ;

  fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')

  ;

  constrains: 'constrains' (name '::' type + 'and')

  ;

  assumes: 'assumes' (thmdecl? props + 'and')

  ;

  defines: 'defines' (thmdecl? prop proppat? + 'and')

  ;

  notes: 'notes' (thmdef? thmrefs + 'and')

  ;

  includes: 'includes' contextexpr

  ;

\end{rail}

\begin{descr}

\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context

  consisting of a certain view of existing locales ($import$) plus some

  additional elements ($body$).  Both $import$ and $body$ are optional; the

  degenerate form $\LOCALE~loc$ defines an empty locale, which may still be

  useful to collect declarations of facts later on.  Type-inference on locale

  expressions automatically takes care of the most general typing that the

  combined context elements may acquire.

  The $import$ consists of a structured context expression, consisting of

  references to existing locales, renamed contexts, or merged contexts.

  Renaming uses positional notation: $c~\vec x$ means that (a prefix of) the

  fixed parameters of context $c$ are named according to $\vec x$; a

  ``\texttt{_}'' (underscore) \indexisarthm{_@\texttt{_}} means to skip that

  position.  Renaming by default deletes existing syntax.  Optionally,

  new syntax may by specified with a mixfix annotation.  Note that the

  special syntax declared with ``$(structure)$'' (see below) is

  neither deleted nor can it be changed.

  Merging proceeds from left-to-right, suppressing any duplicates stemming

  from different paths through the import hierarchy.

  The $body$ consists of basic context elements, further context expressions

  may be included as well.

  \begin{descr}

  \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$

    and mixfix annotation $mx$ (both are optional).  The special syntax

    declaration ``$(structure)$'' means that $x$ may be referenced

    implicitly in this context.

  \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$

    on the local parameter $x$.

  \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to

    $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).

  \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter.

    This is close to $\DEFNAME$ within a proof (cf.\

    \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational

    proposition instead of variable-term pair.  The left-hand side of the

    equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x

      \equiv t}$''.

  \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context.  Most

    notably, this may include arbitrary declarations in any attribute

    specifications included here, e.g.\ a local $simp$ rule.

  \item [$\INCLUDES{c}$] copies the specified context in a statically scoped

    manner.  Only available in the long goal format of \S\ref{sec:goals}.

    In contrast, the initial $import$ specification of a locale expression

    maintains a dynamic relation to the locales being referenced (benefiting

    from any later fact declarations in the obvious manner).

  \end{descr}

  Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and

  $\DEFINESNAME$ above are illegal in locale definitions.  In the long goal

  format of \S\ref{sec:goals}, term bindings may be included as expected,

  though.

  \medskip By default, locale specifications are ``closed up'' by turning the

  given text into a predicate definition $loc_axioms$ and deriving the

  original assumptions as local lemmas (modulo local definitions).  The

  predicate statement covers only the newly specified assumptions, omitting

  the content of included locale expressions.  The full cumulative view is

  only provided on export, involving another predicate $loc$ that refers to

  the complete specification text.

  In any case, the predicate arguments are those locale parameters that

  actually occur in the respective piece of text.  Also note that these

  predicates operate at the meta-level in theory, but the locale packages

  attempts to internalize statements according to the object-logic setup

  (e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see

  also \S\ref{sec:object-logic}).  Separate introduction rules

  $loc_axioms.intro$ and $loc.intro$ are declared as well.

  The $(open)$ option of a locale specification prevents both the current

  $loc_axioms$ and cumulative $loc$ predicate constructions.  Predicates are

  also omitted for empty specification texts.

\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale

  expression in a flattened form.  The notable special case

  $\isarkeyword{print_locale}~loc$ just prints the contents of the named

  locale, but keep in mind that type-inference will normalize type variables

  according to the usual alphabetical order.  The command omits

  $\isarkeyword{notes}$ elements by default.  Use

  $\isarkeyword{print_locale}!$ to get them included.

\item [$\isarkeyword{print_locales}$] prints the names of all locales of the

  current theory.

\end{descr}

\subsubsection{Interpretation of locales}

Locale expressions (more precisely, \emph{context expressions}) may be

instantiated, and the instantiated facts added to the current context.

This requires a proof of the instantiated specification and is called

\emph{locale interpretation}.  Interpretation is possible in theories

and locales

(command $\isarcmd{interpretation}$) and also in proof contexts

($\isarcmd{interpret}$).

\indexisarcmd{interpretation}\indexisarcmd{interpret}

\indexisarcmd{print-interps}

\begin{matharray}{rcl}

  \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\

  \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\

  \isarcmd{print_interps}^* & : &  \isarkeep{theory~|~proof} \\

\end{matharray}

\indexouternonterm{interp}

\railalias{printinterps}{print\_interps}

\railterm{printinterps}

\begin{rail}

  'interpretation' (interp | name ('<' | subseteq) contextexp)

  ;

  'interpret' interp

  ;

  printinterps '!'? name

  ;

  interp: thmdecl? contextexpr ('[' (inst+) ']')?

  ;

\end{rail}

\begin{descr}

\item [$\isarcmd{interpretation}~expr~insts$]

  The first form of $\isarcmd{interpretation}$ interprets $expr$

  in the theory.  The instantiation is given as a list of

  terms $insts$ and is positional.

  All parameters must receive an instantiation term --- with the

  exception of defined parameters.  These are, if omitted, derived

  from the defining equation and other instantiations.  Use ``\_'' to

  omit an instantiation term.  Free variables are automatically

  generalized.

  The command generates proof obligations for the instantiated

  specifications (assumes and defines elements).  Once these are

  discharged by the user, instantiated facts are added to the theory in

  a post-processing phase.

  The command is aware of interpretations already active in the

  theory.  No proof obligations are generated for those, neither is

  post-processing applied to their facts.  This avoids duplication of

  interpreted facts, in particular.  Note that, in the case of a

  locale with import, parts of the interpretation may already be

  active.  The command will only generate proof obligations and add

  facts for new parts.

  The context expression may be preceded by a name and/or attributes.

  These take effect in the post-processing of facts.  The name is used

  to prefix fact names, for example to avoid accidental hiding of

  other facts.  Attributes are applied after attributes of the

  interpreted facts.

  Adding facts to locales has the

  effect of adding interpreted facts to the theory for all active

  interpretations also.  That is, interpretations dynamically

  participate in any facts added to locales.

\item [$\isarcmd{interpretation}~name~\subseteq~expr$]

  This form of the command interprets $expr$ in the locale $name$.  It

  requires a proof that the specification of $name$ implies the

  specification of $expr$.  As in the localized version of the theorem

  command, the proof is in the context of $name$.  After the proof

  obligation has been dischared, the facts of $expr$

  become part of locale $name$ as \emph{derived} context elements and

  are available when the context $name$ is subsequently entered.

  Note that, like import, this is dynamic: facts added to a locale

  part of $expr$ after interpretation become also available in

  $name$.  Like facts

  of renamed context elements, facts obtained by interpretation may be

  accessed by prefixing with the parameter renaming (where the parameters

  are separated by `\_').

  Unlike interpretation in theories, instantiation is confined to the

  renaming of parameters, which may be specified as part of the context

  expression $expr$.  Using defined parameters in $name$ one may

  achieve an effect similar to instantiation, though.

  Only specification fragments of $expr$ that are not already part of

  $name$ (be it imported, derived or a derived fragment of the import)

  are considered by interpretation.  This enables circular

  interpretations.

  If interpretations of $name$ exist in the current theory, the

  command adds interpretations for $expr$ as well, with the same

  prefix and attributes, although only for fragments of $expr$ that

  are not interpreted in the theory already.

\item [$\isarcmd{interpret}~expr~insts$]

  interprets $expr$ in the proof context and is otherwise similar to

  interpretation in theories.  Free variables in instantiations are not

  generalized, however.

\item [$\isarcmd{print_interps}~loc$]

  prints the interpretations of a particular locale $loc$ that are

  active in the current context, either theory or proof context.  The

  exclamation point argument causes triggers printing of

  \emph{witness} theorems justifying interpretations.  These are

  normally omitted from the output.

\end{descr}

\begin{warn}

  Since attributes are applied to interpreted theorems, interpretation

  may modify the current simpset and claset.  Take this into

  account when choosing attributes for local theorems.

\end{warn}

\begin{warn}

  An interpretation in a theory may subsume previous interpretations.

  This happens if the same specification fragment is interpreted twice

  and the instantiation of the second interpretation is more general

  than the interpretation of the first.  A warning

  is issued, since it is likely that these could have been generalized

  in the first place.  The locale package does not attempt to remove

  subsumed interpretations.  This situation is normally harmless, but

  note that $blast$ gets confused by the presence of multiple axclass

  instances of a rule.

\end{warn}

\section{Derived proof schemes}

\subsection{Generalized elimination}\label{sec:obtain}

\indexisarcmd{obtain}\indexisarcmd{guess}

\begin{matharray}{rcl}

  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\

  \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\

\end{matharray}

Generalized elimination means that additional elements with certain properties

may be introduced in the current context, by virtue of a locally proven

``soundness statement''.  Technically speaking, the $\OBTAINNAME$ language

element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see

\S\ref{sec:proof-context}), together with a soundness proof of its additional

claim.  According to the nature of existential reasoning, assumptions get

eliminated from any result exported from the context later, provided that the

corresponding parameters do \emph{not} occur in the conclusion.

\begin{rail}

  'obtain' (vars + 'and') 'where' (props + 'and')

  ;

  'guess' (vars + 'and')

  ;

\end{rail}

$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$

shall refer to (optional) facts indicated for forward chaining.

\begin{matharray}{l}

  \langle facts~\vec b\rangle \\

  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]

  \quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\

  \quad \PROOF{succeed} \\

  \qquad \FIX{thesis} \\

  \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\

  \qquad \THUS{}{thesis} \\

  \quad\qquad \APPLY{-} \\

  \quad\qquad \USING{\vec b}~~\langle proof\rangle \\

  \quad \QED{} \\

  \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\

\end{matharray}

Typically, the soundness proof is relatively straight-forward, often just by

canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.

Accordingly, the ``$that$'' reduction above is declared as simplification and

introduction rule.

In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be

meta-logical existential quantifiers and conjunctions.  This concept has a

broad range of useful applications, ranging from plain elimination (or

introduction) of object-level existential and conjunctions, to elimination

over results of symbolic evaluation of recursive definitions, for example.

Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,

where the result is treated as a genuine assumption.

\medskip

The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but

derives the obtained statement from the course of reasoning!  The proof starts

with a fixed goal $thesis$.  The subsequent proof may refine this to anything

of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce

new subgoals.  The final goal state is then used as reduction rule for the

obtain scheme described above.  Obtained parameters $\vec x$ are marked as

internal by default, which prevents the proof context from being polluted by

ad-hoc variables.  The variable names and type constraints given as arguments

for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly

in the text.

It is important to note that the facts introduced by $\OBTAINNAME$ and

$\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring

here are fixed in the present context!

\subsection{Calculational reasoning}\label{sec:calculation}

\indexisarcmd{also}\indexisarcmd{finally}

\indexisarcmd{moreover}\indexisarcmd{ultimately}

\indexisarcmd{print-trans-rules}

\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric}

\begin{matharray}{rcl}

  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\

  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\

  \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\

  \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\

  \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\

  trans & : & \isaratt \\

  sym & : & \isaratt \\

  symmetric & : & \isaratt \\

\end{matharray}

Calculational proof is forward reasoning with implicit application of

transitivity rules (such those of $=$, $\leq$, $<$).  Isabelle/Isar maintains

an auxiliary register $calculation$\indexisarthm{calculation} for accumulating

results obtained by transitivity composed with the current result.  Command

$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the

final $calculation$ by forward chaining towards the next goal statement.  Both

commands require valid current facts, i.e.\ may occur only after commands that

produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of

$\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are

similar to $\ALSO$ and $\FINALLY$, but only collect further results in

$calculation$ without applying any rules yet.

Also note that the implicit term abbreviation ``$\dots$'' has its canonical

application with calculational proofs.  It refers to the argument of the

preceding statement. (The argument of a curried infix expression happens to be

its right-hand side.)

Isabelle/Isar calculations are implicitly subject to block structure in the

sense that new threads of calculational reasoning are commenced for any new

block (as opened by a local goal, for example).  This means that, apart from

being able to nest calculations, there is no separate \emph{begin-calculation}

command required.

\medskip

The Isar calculation proof commands may be defined as follows:\footnote{We

  suppress internal bookkeeping such as proper handling of block-structure.}

\begin{matharray}{rcl}

  \ALSO@0 & \equiv & \NOTE{calculation}{this} \\

  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]

  \FINALLY & \equiv & \ALSO~\FROM{calculation} \\

  \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\

  \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\

\end{matharray}

\begin{rail}

  ('also' | 'finally') ('(' thmrefs ')')?

  ;

  'trans' (() | 'add' | 'del')

  ;

\end{rail}

\begin{descr}

\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as

  follows.  The first occurrence of $\ALSO$ in some calculational thread

  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same

  level of block-structure updates $calculation$ by some transitivity rule

  applied to $calculation$ and $this$ (in that order).  Transitivity rules are

  picked from the current context, unless alternative rules are given as

  explicit arguments.

\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as

  $\ALSO$, and concludes the current calculational thread.  The final result

  is exhibited as fact for forward chaining towards the next goal. Basically,

  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that

  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and

  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding

  calculational proofs.

\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,

  but collect results only, without applying rules.

\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity

  rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules

  (for the $symmetric$ operation and single step elimination patters) of the

  current context.

\item [$trans$] declares theorems as transitivity rules.

\item [$sym$] declares symmetry rules.

\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the

  current context.  For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a

  swapped fact derived from that assumption.

  In structured proof texts it is often more appropriate to use an explicit

  single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =

    x}~\DDOT$''.  The very same rules known to $symmetric$ are declared as

  $elim?$ as well.

\end{descr}

\section{Proof tools}

\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}

\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}

\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}

\indexisarmeth{fail}\indexisarmeth{succeed}

\begin{matharray}{rcl}

  unfold & : & \isarmeth \\

  fold & : & \isarmeth \\

  insert & : & \isarmeth \\[0.5ex]

  erule^* & : & \isarmeth \\

  drule^* & : & \isarmeth \\

  frule^* & : & \isarmeth \\

  succeed & : & \isarmeth \\

  fail & : & \isarmeth \\

\end{matharray}

\begin{rail}

  ('fold' | 'unfold' | 'insert') thmrefs

  ;

  ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs

  ;

\end{rail}

\begin{descr}

\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the

  given meta-level definitions throughout all goals; any chained facts

  provided are inserted into the goal and subject to rewriting as well.

\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof

  state.  Note that current facts indicated for forward chaining are ignored.

\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the

  basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by

  elim-resolution, destruct-resolution, and forward-resolution, respectively

  \cite{isabelle-ref}.  The optional natural number argument (default $0$)

  specifies additional assumption steps to be performed here.

  Note that these methods are improper ones, mainly serving for

  experimentation and tactic script emulation.  Different modes of basic rule

  application are usually expressed in Isar at the proof language level,

  rather than via implicit proof state manipulations.  For example, a proper

  single-step elimination would be done using the plain $rule$ method, with

  forward chaining of current facts.

\item [$succeed$] yields a single (unchanged) result; it is the identity of

  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

\item [$fail$] yields an empty result sequence; it is the identity of the

  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

\end{descr}

\indexisaratt{tagged}\indexisaratt{untagged}

\indexisaratt{THEN}\indexisaratt{COMP}

\indexisaratt{unfolded}\indexisaratt{folded}

\indexisaratt{standard}\indexisarattof{Pure}{elim-format}

\indexisaratt{no-vars}

\begin{matharray}{rcl}

  tagged & : & \isaratt \\

  untagged & : & \isaratt \\[0.5ex]

  THEN & : & \isaratt \\

  COMP & : & \isaratt \\[0.5ex]

  unfolded & : & \isaratt \\

  folded & : & \isaratt \\[0.5ex]

  elim_format & : & \isaratt \\

  standard^* & : & \isaratt \\

  no_vars^* & : & \isaratt \\

\end{matharray}

\begin{rail}

  'tagged' (nameref+)

  ;

  'untagged' name

  ;

  ('THEN' | 'COMP') ('[' nat ']')? thmref

  ;

  ('unfolded' | 'folded') thmrefs

  ;

\end{rail}

\begin{descr}

\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some

  theorem.  Tags may be any list of strings that serve as comment for some

  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the

  result).  The first string is considered the tag name, the rest its

  arguments.  Note that untag removes any tags of the same name.

\item [$THEN~a$ and $COMP~a$] compose rules by resolution.  $THEN$ resolves

  with the first premise of $a$ (an alternative position may be also

  specified); the $COMP$ version skips the automatic lifting process that is

  normally intended (cf.\ \texttt{RS} and \texttt{COMP} in

  \cite[\S5]{isabelle-ref}).

\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the

  given meta-level definitions throughout a rule.

\item [$elim_format$] turns a destruction rule into elimination rule format,

  by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP

  B$.

  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own

  version of this operation.

\item [$standard$] puts a theorem into the standard form of object-rules at

  the outermost theory level.  Note that this operation violates the local

  proof context (including active locales).

\item [$no_vars$] replaces schematic variables by free ones; this is mainly

  for tuning output of pretty printed theorems.

\end{descr}

\subsection{Further tactic emulations}\label{sec:tactics}

The following improper proof methods emulate traditional tactics.  These admit

direct access to the goal state, which is normally considered harmful!  In

particular, this may involve both numbered goal addressing (default 1), and

dynamic instantiation within the scope of some subgoal.

\begin{warn}

  Dynamic instantiations refer to universally quantified parameters of

  a subgoal (the dynamic context) rather than fixed variables and term

  abbreviations of a (static) Isar context.

\end{warn}

Tactic emulation methods, unlike their ML counterparts, admit

simultaneous instantiation from both dynamic and static contexts.  If

names occur in both contexts goal parameters hide locally fixed

variables.  Likewise, schematic variables refer to term abbreviations,

if present in the static context.  Otherwise the schematic variable is

interpreted as a schematic variable and left to be solved by unification

with certain parts of the subgoal.

Note that the tactic emulation proof methods in Isabelle/Isar are consistently

named $foo_tac$.  Note also that variable names occurring on left hand sides

of instantiations must be preceded by a question mark if they coincide with

a keyword or contain dots.

This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).

\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}

\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}

\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}

\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}

\indexisarmeth{rotate-tac}\indexisarmeth{tactic}

\begin{matharray}{rcl}

  rule_tac^* & : & \isarmeth \\

  erule_tac^* & : & \isarmeth \\

  drule_tac^* & : & \isarmeth \\

  frule_tac^* & : & \isarmeth \\

  cut_tac^* & : & \isarmeth \\

  thin_tac^* & : & \isarmeth \\

  subgoal_tac^* & : & \isarmeth \\

  rename_tac^* & : & \isarmeth \\

  rotate_tac^* & : & \isarmeth \\

  tactic^* & : & \isarmeth \\

\end{matharray}

\railalias{ruletac}{rule\_tac}

\railterm{ruletac}

\railalias{eruletac}{erule\_tac}

\railterm{eruletac}

\railalias{druletac}{drule\_tac}

\railterm{druletac}

\railalias{fruletac}{frule\_tac}

\railterm{fruletac}

\railalias{cuttac}{cut\_tac}

\railterm{cuttac}

\railalias{thintac}{thin\_tac}

\railterm{thintac}

\railalias{subgoaltac}{subgoal\_tac}

\railterm{subgoaltac}

\railalias{renametac}{rename\_tac}

\railterm{renametac}

\railalias{rotatetac}{rotate\_tac}

\railterm{rotatetac}

\begin{rail}

  ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?

  ( insts thmref | thmrefs )

  ;

  subgoaltac goalspec? (prop +)

  ;

  renametac goalspec? (name +)

  ;

  rotatetac goalspec? int?

  ;

  'tactic' text

  ;

  insts: ((name '=' term) + 'and') 'in'

  ;

\end{rail}

\begin{descr}

\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.

  This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see

  \cite[\S3]{isabelle-ref}).

  Multiple rules may be only given if there is no instantiation; then

  $rule_tac$ is the same as \texttt{resolve_tac} in ML (see

  \cite[\S3]{isabelle-ref}).

\item [$cut_tac$] inserts facts into the proof state as assumption of a

  subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note

  that the scope of schematic variables is spread over the main goal

  statement.  Instantiations may be given as well, see also ML tactic

  \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.

\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note

  that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in

  \cite[\S3]{isabelle-ref}.

\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See

  also \texttt{subgoal_tac} and \texttt{subgoals_tac} in

  \cite[\S3]{isabelle-ref}.

\item [$rename_tac~\vec x$] renames parameters of a goal according to the list

  $\vec x$, which refers to the \emph{suffix} of variables.

\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:

  from right to left if $n$ is positive, and from left to right if $n$ is

  negative; the default value is $1$.  See also \texttt{rotate_tac} in

  \cite[\S3]{isabelle-ref}.

\item [$tactic~text$] produces a proof method from any ML text of type

  \texttt{tactic}.  Apart from the usual ML environment and the current

  implicit theory context, the ML code may refer to the following locally

  bound values:

{\footnotesize\begin{verbatim}

val ctxt  : Proof.context

val facts : thm list

val thm   : string -> thm

val thms  : string -> thm list

\end{verbatim}}

  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}

  indicates any current facts for forward-chaining, and

  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global

  theorems) from the context.

\end{descr}

\subsection{The Simplifier}\label{sec:simplifier}

\subsubsection{Simplification methods}

\indexisarmeth{simp}\indexisarmeth{simp-all}

\begin{matharray}{rcl}

  simp & : & \isarmeth \\

  simp_all & : & \isarmeth \\

\end{matharray}

\railalias{simpall}{simp\_all}

\railterm{simpall}

\railalias{noasm}{no\_asm}

\railterm{noasm}

\railalias{noasmsimp}{no\_asm\_simp}

\railterm{noasmsimp}

\railalias{noasmuse}{no\_asm\_use}

\railterm{noasmuse}

\railalias{asmlr}{asm\_lr}

\railterm{asmlr}

\indexouternonterm{simpmod}

\begin{rail}

  ('simp' | simpall) ('!' ?) opt? (simpmod *)

  ;

  opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'

  ;

  simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |

    'split' (() | 'add' | 'del')) ':' thmrefs

  ;

\end{rail}

\begin{descr}

\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules

  according to the arguments given.  Note that the \railtterm{only} modifier

  first removes all other rewrite rules, congruences, and looper tactics

  (including splits), and then behaves like \railtterm{add}.

  \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence

  rules (see also \cite{isabelle-ref}), the default is to add.

  \medskip The \railtterm{split} modifiers add or delete rules for the

  Splitter (see also \cite{isabelle-ref}), the default is to add.  This works

  only if the Simplifier method has been properly setup to include the

  Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).

\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from

  the last to the first one).

\end{descr}

By default the Simplifier methods take local assumptions fully into account,

using equational assumptions in the subsequent normalization process, or

simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in

\cite[\S10]{isabelle-ref}).  In structured proofs this is usually quite well

behaved in practice: just the local premises of the actual goal are involved,

additional facts may be inserted via explicit forward-chaining (using $\THEN$,

$\FROMNAME$ etc.).  The full context of assumptions is only included if the

``$!$'' (bang) argument is given, which should be used with some care, though.

Additional Simplifier options may be specified to tune the behavior further

(mostly for unstructured scripts with many accidental local facts):

``$(no_asm)$'' means assumptions are ignored completely (cf.\

\texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the

simplification of the conclusion but are not themselves simplified (cf.\

\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are

simplified but are not used in the simplification of each other or the

conclusion (cf.\ \texttt{full_simp_tac}).

For compatibility reasons, there is also an option ``$(asm_lr)$'',

which means that an assumption is only used for simplifying assumptions

which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}).

\medskip

The Splitter package is usually configured to work as part of the Simplifier.

The effect of repeatedly applying \texttt{split_tac} can be simulated by

``$(simp~only\colon~split\colon~\vec a)$''.  There is also a separate $split$

method available for single-step case splitting.

\subsubsection{Declaring rules}

\indexisarcmd{print-simpset}

\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}

\begin{matharray}{rcl}

  \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\

  simp & : & \isaratt \\

  cong & : & \isaratt \\

  split & : & \isaratt \\

\end{matharray}

\begin{rail}

  ('simp' | 'cong' | 'split') (() | 'add' | 'del')

  ;

\end{rail}

\begin{descr}

\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to

  the Simplifier, which is also known as ``simpset'' internally

  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.

\item [$simp$] declares simplification rules.

\item [$cong$] declares congruence rules.

\item [$split$] declares case split rules.

\end{descr}

\subsubsection{Forward simplification}

\indexisaratt{simplified}

\begin{matharray}{rcl}

  simplified & : & \isaratt \\

\end{matharray}

\begin{rail}

  'simplified' opt? thmrefs?

  ;

  opt: '(' (noasm | noasmsimp | noasmuse) ')'

  ;

\end{rail}

\begin{descr}

\item [$simplified~\vec a$] causes a theorem to be simplified, either by

  exactly the specified rules $\vec a$, or the implicit Simplifier context if

  no arguments are given.  The result is fully simplified by default,

  including assumptions and conclusion; the options $no_asm$ etc.\ tune the

  Simplifier in the same way as the for the $simp$ method.

  Note that forward simplification restricts the simplifier to its most basic

  operation of term rewriting; solver and looper tactics \cite{isabelle-ref}

  are \emph{not} involved here.  The $simplified$ attribute should be only

  rarely required under normal circumstances.

\end{descr}

\subsubsection{Low-level equational reasoning}

\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}

\begin{matharray}{rcl}

  subst^* & : & \isarmeth \\

  hypsubst^* & : & \isarmeth \\

  split^* & : & \isarmeth \\

\end{matharray}

\begin{rail}

  'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref

  ;

  'split' ('(' 'asm' ')')? thmrefs

  ;

\end{rail}

These methods provide low-level facilities for equational reasoning that are

intended for specialized applications only.  Normally, single step

calculations would be performed in a structured text (see also

\S\ref{sec:calculation}), while the Simplifier methods provide the canonical

way for automated normalization (see \S\ref{sec:simplifier}).

\begin{descr}

\item [$subst~eq$] performs a single substitution step using rule $eq$, which

  may be either a meta or object equality.

\item [$subst~(asm)~eq$] substitutes in an assumption.

\item [$subst~(i \dots j)~eq$] performs several substitutions in the

conclusion. The numbers $i$ to $j$ indicate the positions to substitute at.

Positions are ordered from the top of the term tree moving down from left to

right. For example, in $(a+b)+(c+d)$ there are three positions where

commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$

and 3 to $c+d$. If the positions in the list $(i \dots j)$ are

non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all

substitutions are performed simultaneously. Otherwise the behaviour of

$subst$ is not specified.

\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the

assumptions. Positions $1 \dots i@1$ refer

to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on.