\chapter{Basic Isar elements}

Subsequently, we introduce most of the basic Isar theory and proof commands as

provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes further Isar

elements as provided by generic tools and packages that are either part of

Pure Isabelle, or preloaded by most object logics (such as the simplifier).

See chapter~\ref{ch:hol-tools} for actual object-logic specific elements (for

Isabelle/HOL).

\medskip

Isar commands may be either \emph{proper} document constructors, or

\emph{improper commands} (indicated by $^*$).  Improper commands might be

helpful when developing proof documents, while their use is strongly

discouraged for the final outcome.  Typical examples are diagnostic commands

that print terms or theorems according to the current context; other commands

even emulate old-style tactical theorem proving, which facilitates porting of

legacy proof scripts.

\section{Theory commands}

\subsection{Defining theories}\label{sec:begin-thy}

\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}

\begin{matharray}{rcl}

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

  \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\

  \isarcmd{end} & : & \isartrans{theory}{\cdot} \\

\end{matharray}

Isabelle/Isar ``new-style'' theories are either defined via theory files or

interactively.  Both actual theory specifications and proofs are handled

uniformly --- occasionally definitional mechanisms even require some proof.

In contrast, ``old-style'' Isabelle theories support batch processing only,

with the proof scripts collected in separate ML files.

The first command of any theory has to be $\THEORY$, starting a new theory

based on the merge of existing ones.  The theory context may be changed by

$\CONTEXT$ without creating a new theory.  In both cases $\END$ concludes the

theory development; it has to be the very last command of any proper theory

file.

\begin{rail}

  'theory' name '=' (name + '+') filespecs? ':'

  ;

  'context' name

  ;

  'end'

  ;;

  filespecs: 'files' ((name | parname) +);

\end{rail}

\begin{descr}

\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on

  existing ones $B@1 + \cdots + B@n$.  Note that Isabelle's theory loader

  system ensures that any of the base theories are properly loaded (and fully

  up-to-date when $\THEORY$ is executed interactively).  The optional

  $\isarkeyword{files}$ specification declares additional dependencies on ML

  files.  Unless put in in parentheses, any file will be loaded immediately

  via $\isarcmd{use}$ (see also \S\ref{sec:ML}).

\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in

  read-only mode, so only a limited set of commands may be performed.  Just as

  for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.

\item [$\END$] concludes the current theory definition or context switch.

\end{descr}

\subsection{Formal comments}\label{sec:formal-cmt-thy}

\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}

\indexisarcmd{subsubsection}\indexisarcmd{text}

\begin{matharray}{rcl}

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

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

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

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

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

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

\end{matharray}

There are several commands to include \emph{formal comments} in theory

specification (a few more are available for proofs, see

\S\ref{sec:formal-cmt-prf}).  In contrast to source-level comments

\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text

given as formal comment is meant to be part of the actual document.

Consequently, it would be included in the final printed version.

Apart from plain prose, formal comments may also refer to logical entities of

the current theory context (types, terms, theorems etc.).  Proper processing

of the text would then include some further consistency checks with the items

declared in the current theory, e.g.\ type-checking of included terms.

\footnote{The current version of Isabelle/Isar does not process formal

  comments in any such way.  This will be available as part of the automatic

  theory and proof document preparation system (via (PDF)LaTeX) that is

  planned for the near future.}

\begin{rail}

  'title' text text? text?

  ;

  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{title}~title~author~date$] specifies the document title

  just as in typical LaTeX documents.

\item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,

  $\isarkeyword{subsection}~text$, $\isarkeyword{subsubsection}~text$] specify

  chapter and subsection headings.

\item [$\TEXT~text$] specifies an actual body of prose text, including

  references to formal entities.\footnote{The latter feature is not yet

    exploited in any way.}

\end{descr}

\subsection{Type classes and sorts}\label{sec:classes}

\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}

\begin{matharray}{rcl}

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

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

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

\end{matharray}

\begin{rail}

  'classes' (classdecl comment? +)

  ;

  'classrel' nameref '<' nameref comment?

  ;

  'defaultsort' sort comment?

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{classes}~c<cs ~\dots$] declares class $c$ to be a

  subclass of existing classes $cs$.  Cyclic class structures are ruled out.

\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between

  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The

  $\isarkeyword{instance}$ command provides a way introduce proven class

  relations (see \S\ref{sec:axclass}).

\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for

  any type variables input without sort constraints.  Typically, the default

  sort would be only changed when defining new logics.

\end{descr}

\subsection{Types}\label{sec:types-pure}

\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}

\begin{matharray}{rcl}

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

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

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

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

\end{matharray}

\begin{rail}

  'types' (typespec '=' type infix? comment? +)

  ;

  'typedecl' typespec infix? comment?

  ;

  'nonterminals' (name +) comment?

  ;

  'arities' (nameref '::' arity comment? +)

  ;

\end{rail}

\begin{descr}

\item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym}

  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,

  as are available in Isabelle/HOL for example, type synonyms are just purely

  syntactic abbreviations, without any logical significance.  Internally, type

  synonyms are fully expanded, as may be observed when printing terms or

  theorems.

\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor

  $t$, intended as an actual logical type.  Note that some logics such as

  Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.

\item [$\isarkeyword{nonterminals}~c~\dots$] declares $0$-ary type

  constructors $c$ to act as purely syntactic types, i.e.\ nonterminal symbols

  of Isabelle's inner syntax of terms or types.

\item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's

  order-sorted signature of types by new type constructor arities.  This is

  done axiomatically!  The $\isarkeyword{instance}$ command provides a way

  introduce proven type arities (see \S\ref{sec:axclass}).

\end{descr}

\subsection{Constants and simple definitions}

\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}

\begin{matharray}{rcl}

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

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

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

\end{matharray}

\begin{rail}

  'consts' (constdecl +)

  ;

  'defs' (thmdecl? prop comment? +)

  ;

  'constdefs' (constdecl prop comment? +)

  ;

  constdecl: name '::' type mixfix? comment?

  ;

\end{rail}

\begin{descr}

\item [$\CONSTS~c::\tau~\dots$] declares constant $c$ to have any instance of

  type scheme $\tau$.  The optional mixfix annotations may attach concrete

  syntax to the constant.

\item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for

  some existing constant.  See \cite[\S6]{isabelle-ref} for more details on

  the form of equations admitted as constant definitions.

\item [$\isarkeyword{constdefs}~c::\tau~eqn~\dots$] combines constant

  declarations and definitions, using canonical name $c_def$ for the

  definitional axiom.

\end{descr}

\subsection{Syntax and translations}

\indexisarcmd{syntax}\indexisarcmd{translations}

\begin{matharray}{rcl}

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

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

\end{matharray}

\begin{rail}

  'syntax' ('(' name 'output'? ')')? (constdecl +)

  ;

  'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)

  ;

  transpat: ('(' nameref ')')? string

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{syntax}~mode~decls$] is similar to $\CONSTS~decls$,

  except the actual logical signature extension.  Thus the context free

  grammar of Isabelle's inner syntax may be augmented in arbitrary ways.  The

  $mode$ argument refers to the print mode that the grammar rules belong;

  unless there is the \texttt{output} flag given, all productions are added

  both to the input and output grammar.

\item [$\isarkeyword{translations}~rule~\dots$] specifies syntactic

  translation rules (macros): parse/print rules (\texttt{==}), parse rules

  (\texttt{=>}), print rules (\texttt{<=}).  Translation patterns may be

  prefixed by the syntactic category to be used for parsing; the default is

  \texttt{logic}.

\end{descr}

\subsection{Axioms and theorems}

\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}

\begin{matharray}{rcl}

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

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

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

\end{matharray}

\begin{rail}

  'axioms' (axmdecl prop comment? +)

  ;

  ('theorems' | 'lemmas') thmdef? thmrefs

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary

  statements as logical axioms.  In fact, axioms are ``axiomatic theorems'',

  and may be referred as any other theorems later.

  Axioms are usually only introduced when declaring new logical systems.

  Everyday work is normally done the hard way, with proper definitions and

  actual theorems.

\item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems

  as $name$.  Typical applications would also involve attributes to augment

  the default simpset, for example.

\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but

  tags the results as ``lemma''.

\end{descr}

\subsection{Name spaces}

Isabelle organizes any kind of names (of types, constants, theorems etc.)  by

hierarchically structured name spaces.  Normally the user never has to control

the behavior of name space entry by hand, yet the following commands provide

some way to do so.

\indexisarcmd{global}\indexisarcmd{local}

\begin{matharray}{rcl}

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

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

\end{matharray}

\begin{descr}

\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current

  name declaration mode.  Initially, theories start in $\isarkeyword{local}$

  mode, causing all names to be automatically qualified by the theory name.

  Changing this to $\isarkeyword{global}$ causes all names to be declared as

  base names only.

\end{descr}

\subsection{Incorporating ML code}\label{sec:ML}

\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}

\begin{matharray}{rcl}

  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\

  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\

  \isarcmd{setup} & : & \isartrans{\cdot}{\cdot} \\

\end{matharray}

\begin{rail}

  'use' name

  ;

  'ML' text

  ;

  'setup' text

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{use}~file$] reads and execute ML commands from $file$.

  The current theory context as passed down to the ML session.  Furthermore,

  the file name is checked with the dependency declarations given in the

  theory header (see also \S\ref{sec:begin-thy}).

  \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.

  The theory context is passed just as in $\isarkeyword{use}$.

\item [$\isarkeyword{setup}~text$] changes the current theory context by

  applying setup functions $text$ (which has to be an ML expression of type

  $(theory -> theory)~list$.  The $\isarkeyword{setup}$ is the usual way to

  initialize object-logic specific tools and packages written in ML.

\end{descr}

\subsection{Syntax translation functions}

\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}

\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}

\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}

\begin{matharray}{rcl}

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

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

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

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

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

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

\end{matharray}

Syntax translation functions written in ML admit almost arbitrary

manipulations of Isabelle's inner syntax.  Any of the above commands have a

single \railqtoken{text} argument that refers to an ML expression of

appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax

transformations.

\subsection{Oracles}

\indexisarcmd{oracle}

\begin{matharray}{rcl}

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

\end{matharray}

\begin{rail}

  'oracle' name '=' text comment?

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{oracle}~name=text$] FIXME

\end{descr}

\section{Proof commands}

Proof commands provide transitions of Isar/VM machine configurations.  There

are three different kinds of operation:

\begin{descr}

\item [$proof(prove)$] means that a new goal has just been stated that is now

  to be \emph{proven}; the next command may refine it by some proof method

  ($\approx$ tactic) and enter a sub-proof to establish the final result.

\item [$proof(state)$] is like an internal theory mode: the context may be

  augmented by \emph{stating} additional assumptions, intermediate result;

\item [$proof(chain)$] indicates an intermediate mode between $proof(state)$

  and $proof(state)$: some already established facts have been just picked up

  in order to use them when refining the subsequent goal.

\end{descr}

\subsection{Formal comments}\label{sec:formal-cmt-prf}

The following formal comments in proof mode closely correspond to the ones of

theory mode (see \S\ref{sec:formal-cmt-thy} for more information).

\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}

\begin{matharray}{rcl}

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

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

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

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

\end{matharray}

\begin{rail}

  ('sect' | 'subsect' | 'subsubsect' | 'txt') text

  ;

\end{rail}

\subsection{Proof context}

FIXME

\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}

\begin{matharray}{rcl}

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

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

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

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

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

\end{matharray}

\begin{rail}

  'fix' (var +) comment?

  ;

  ('assume' | 'presume') thmdecl? (proppat +) comment?

  ;

  'def' thmdecl? var '==' termpat comment?

  ;

  'let' ((term + 'as') '=' term comment? + 'and')

  ;

  var: name ('::' type)?

  ;

\end{rail}

\begin{descr}

\item [$\FIX{x}$] FIXME

\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME

\item [$\DEF{a}{x \equiv t}$] FIXME

\item [$\LET{\vec p = \vec t}$] FIXME

\end{descr}

\subsection{Facts and forward chaining}

FIXME

\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}

\begin{matharray}{rcl}

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

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

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

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

\end{matharray}

\begin{rail}

  'note' thmdef? thmrefs comment?

  ;

  'then' comment?

  ;

  ('from' | 'with') thmrefs comment?

  ;

\end{rail}

\begin{descr}

\item [$\NOTE{a}{bs}$] recalls existing facts $bs$, binding the result as $a$

  (and $facts$).  Note that attributes may be involved as well, both on the

  left and right hand side.

\item [$\THEN$] indicates forward chaining by the current facts in order to

  establish the subsequent goal.  The initial proof method invoked to solve

  that will be offered these facts to do anything ``appropriate'' (see also

  \S\ref{sec:proof-steps}).  For example, method $rule$ (see

  \S\ref{sec:pure-meth}) would do an elimination rather than an introduction.

\item [$\FROM{bs}$] abbreviates $\NOTE{facts}{bs}~\THEN$; also note that

  $\THEN$ is equivalent to $\FROM{facts}$.

\item [$\WITH{bs}$] abbreviates $\FROM{bs~facts}$; thus the forward chaining

  is from earlier facts together with the current ones.

\end{descr}

\subsection{Goal statements}

Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$

and $\LEMMANAME$.  New local goals may be claimed within proof mode: four

variants indicate whether the result is meant to solve some pending goal and

whether forward chaining is employed.

\indexisarcmd{theorem}\indexisarcmd{lemma}

\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}

\begin{matharray}{rcl}

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

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

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

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

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

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

\end{matharray}

\begin{rail}

  ('theorem' | 'lemma') goal

  ;

  ('have' | 'show' | 'hence' | 'thus') goal

  ;

  goal: thmdecl? proppat comment?

  ;

\end{rail}

\begin{descr}

\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,

  eventually resulting in some theorem $\turn \phi$, which stored in the

  theory.

\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as

  ``lemma''.

\item [$\HAVE{name}{\phi}$] claims a local goal, eventually resulting in a

  theorem with the current assumption context as hypotheses.

\item [$\SHOW{name}{\phi}$] same as $\HAVE{name}{\phi}$, but solves some

  pending goal with the result exported to the enclosing assumption context.

\item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\ 

  claims a local goal to be proven by forward chaining the current facts.

\item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$.

\end{descr}

\subsection{Initial and terminal proof steps}\label{sec:proof-steps}

Arbitrary goal refinements via tactics is considered harmful.  Consequently

the Isar framework admits proof methods to be invoked in two places only.

\begin{enumerate}

\item An \emph{initial} refinement step (via $\PROOF{m@1}$) reduces a newly

  stated intermediate goal to a number of sub-goals that are to be solved

  subsequently.  Facts are passed to $m@1$ for forward chaining if so

  indicated by $proof(chain)$ mode.

\item A \emph{terminal} conclusion step (via $\QED{m@2}$)) solves any remaining

  pending goals completely.  No facts are passed to $m@2$.

\end{enumerate}

The only other proper way to affect pending goals is by $\SHOWNAME$, which

involves an explicit statement of what is solved.

Also note that initial proof methods should either solve the goal completely,

or constitute some well-understood deterministic reduction to new sub-goals.

Arbitrary automatic proof tools that are prone leave a large number of badly

structured sub-goals are no help in continuing the proof document in any

intelligible way.  A much better technique is to $\SHOWNAME$ some non-trivial

reduction as an explicit rule, which is solved completely by some automated

method, and then applied to some pending goal.

\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}

\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}

\begin{matharray}{rcl}

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

  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\

  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

  \isarcmd{..} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\

\end{matharray}

\begin{rail}

  'proof' interest? meth? comment?

  ;

  'qed' meth? comment?

  ;

  'by' meth meth? comment?

  ;

  ('.' | '..' | 'sorry') comment?

  ;

  meth: method interest?

  ;

\end{rail}

\begin{descr}

\item [$\PROOF{m}$] refines the pending goal by proof method $m$ (facts for

  forward chaining are passed if indicated by $proof(chain)$).

\item [$\QED{m}$] refines any remaining goals by proof method $m$ and

  concludes the sub-proof.  If the goal had been $\SHOWNAME$, some pending

  sub-goal is solved as well by the rule resulting from the result exported to

  the enclosing goal context.

  Thus $\QEDNAME$ may fail for two reasons: either $m$ fails to solve all

  remaining goals completely, or the resulting rule does not resolve with any

  enclosing goal.  Debugging such a situation might involve temporarily

  changing $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by

  replacing $\ASSUMENAME$ by $\PRESUMENAME$.

\item [$\BY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates

  $\PROOF{m@1}~\QED{m@2}$, automatically backtracking across both methods.

  Debugging an unsuccessful $\BY{m@1}{m@2}$ commands might be done by simply

  expanding the abbreviation by hand; usually $\PROOF{m@1}$ is already

  sufficient to see what goes wrong.

\item [$\isarkeyword{..}$] is a \emph{default proof}; it abbreviates

  $\BY{default}{finish}$, where method $default$ usually applies a single

  elimination or introduction rule according to the topmost symbol, and

  $finish$ solves all goals by assumption.

\item [$\isarkeyword{.}$] is a \emph{trivial proof}, it abbreviates

  $\BY{-}{finish}$, where method $-$ does nothing except inserting any facts

  into the proof state.

\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that

  \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve

  the goal without much ado.  Of course, the result is a fake theorem only,

  involving some oracle in its internal derivation object.  Note that this is

  indicated as \texttt{[!]} in the printed result.  The main application of

  $\isarkeyword{sorry}$ is to support top-down proof development.

\end{descr}

\subsection{Block structure}

While Isar is inherently block-structured, opening and closing blocks is

mostly handled rather casually, with little explicit user-intervention.  Any

local goal statement automatically opens \emph{two} blocks, which are closed

again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of

different context within a sub-proof are typically switched via

$\isarkeyword{next}$, which is just a single block-close followed by

block-open again.  Thus the effect of $\isarkeyword{next}$ is to reset the

proof context to that of the head of the sub-proof.  Note that there is no

goal focus involved!

There are explicit block parentheses as well.  These typically achieve a

strong forward style of reasoning.

\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}

\begin{matharray}{rcl}

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

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

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

\end{matharray}

\begin{descr}

\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,

  resetting the context to the initial one.

\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and

  close blocks.  Any current facts pass through $\isarkeyword{\{\{}$

  unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into

  the enclosing context.  Thus fixed variables are generalized, assumptions

  discharged, and local definitions eliminated.

\end{descr}

\subsection{Calculational proof}

\indexisarcmd{also}\indexisarcmd{finally}

\begin{matharray}{rcl}

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

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

\end{matharray}

\begin{rail}

  ('also' | 'finally') transrules? comment?

  ;

  transrules: '(' thmrefs ')' interest?

  ;

\end{rail}

\begin{descr}

\item [$ $] FIXME

\end{descr}

\subsection{Improper proof steps}

The following commands emulate tactic scripts to some extent.  While these are

anathema for writing proper Isar proof documents, they might come in handy for

exploring and debugging.

\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}

\begin{matharray}{rcl}

  \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\

  \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\

  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\

\end{matharray}

\railalias{thenapply}{then\_apply}

\railterm{thenapply}

\begin{rail}

  'apply' method

  ;

  thenapply method

  ;

  'back'

  ;

\end{rail}

\begin{descr}

\item [$ $] FIXME

\end{descr}

\section{Other commands}

\subsection{Diagnostics}

\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}

\begin{matharray}{rcl}

  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\

  \isarcmd{term} & : & \isarkeep{theory~|~proof} \\

  \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\

  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\

\end{matharray}

\begin{rail}

  'typ' type

  ;

  'term' term

  ;

  'prop' prop

  ;

  'thm' thmrefs

  ;

\end{rail}

\begin{descr}

\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,

  $\isarkeyword{prop}~\phi$] read and print types / terms / propositions

  according to the current theory or proof context.

\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current

  theory or proof context.  Note that any attributes included in the theorem

  specifications are applied to a temporary proof context derived from the

  current theory or proof; the resulting context is discarded.

\end{descr}

\subsection{System operations}

\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}

\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}

\begin{matharray}{rcl}

  \isarcmd{cd} & : & \isarkeep{\cdot} \\

  \isarcmd{pwd} & : & \isarkeep{\cdot} \\

  \isarcmd{use_thy} & : & \isarkeep{\cdot} \\

  \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\

  \isarcmd{update_thy} & : & \isarkeep{\cdot} \\

  \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\

\end{matharray}

\begin{descr}

\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle

  process.

\item [$\isarkeyword{pwd}~$] prints the current working directory.

\item [$\isarkeyword{use_thy}~name$, $\isarkeyword{use_thy_only}~name$,

  $\isarkeyword{update_thy}~name$, $\isarkeyword{update_thy_only}~name$] load

  theory files.  These commands are exactly the same as the corresponding ML

  functions (see also \cite[\S1 and \S6]{isabelle-ref}).

\end{descr}

%%% Local Variables: 

%%% mode: latex

%%% TeX-master: "isar-ref"

%%% End: