
wenzelm@7046: 
wenzelm@7895: \chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
wenzelm@7167: 
wenzelm@7315: Subsequently, we introduce the main part of the basic Isar theory and proof
wenzelm@7315: commands as provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes
wenzelm@7895: further Isar elements provided by generic tools and packages (such as the
wenzelm@7895: Simplifier) that are either part of Pure Isabelle or pre-loaded by most object
wenzelm@7895: logics.  Chapter~\ref{ch:hol-tools} refers to actual object-logic specific
wenzelm@7895: elements of Isabelle/HOL.
wenzelm@7046: 
wenzelm@7167: \medskip
wenzelm@7167: 
wenzelm@7167: Isar commands may be either \emph{proper} document constructors, or
wenzelm@7466: \emph{improper commands}.  Some proof methods and attributes introduced later
wenzelm@7466: are classified as improper as well.  Improper Isar language elements, which
wenzelm@7466: are subsequently marked by $^*$, are often helpful when developing proof
wenzelm@7981: documents, while their use is discouraged for the final outcome.  Typical
wenzelm@7981: examples are diagnostic commands that print terms or theorems according to the
wenzelm@7981: current context; other commands even emulate old-style tactical theorem
wenzelm@7981: proving, which facilitates porting of legacy proof scripts.
wenzelm@7167: 
wenzelm@7134: 
wenzelm@7134: \section{Theory commands}
wenzelm@7134: 
wenzelm@7167: \subsection{Defining theories}\label{sec:begin-thy}
wenzelm@7134: 
wenzelm@7895: \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7895:   \isarcmd{header} & : & \isarkeep{toplevel} \\
wenzelm@7134:   \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
wenzelm@7134:   \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
wenzelm@7134:   \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: Isabelle/Isar ``new-style'' theories are either defined via theory files or
wenzelm@7981: interactively.  Both theory-level specifications and proofs are handled
wenzelm@7335: uniformly --- occasionally definitional mechanisms even require some explicit
wenzelm@7335: proof as well.  In contrast, ``old-style'' Isabelle theories support batch
wenzelm@7335: processing only, with the proof scripts collected in separate ML files.
wenzelm@7134: 
wenzelm@7895: The first actual command of any theory has to be $\THEORY$, starting a new
wenzelm@7895: theory based on the merge of existing ones.  Just preceding $\THEORY$, there
wenzelm@7895: may be an optional $\isarkeyword{header}$ declaration, which is relevant to
wenzelm@7895: document preparation only; it acts very much like a special pre-theory markup
wenzelm@7895: command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The theory
wenzelm@7895: context may be also changed by $\CONTEXT$ without creating a new theory.  In
wenzelm@7895: both cases, $\END$ concludes the theory development; it has to be the very
wenzelm@7895: last command in a theory file.
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7895:   'header' text
wenzelm@7895:   ;
wenzelm@7134:   'theory' name '=' (name + '+') filespecs? ':'
wenzelm@7134:   ;
wenzelm@7134:   'context' name
wenzelm@7134:   ;
wenzelm@7134:   'end'
wenzelm@7134:   ;;
wenzelm@7134: 
wenzelm@7167:   filespecs: 'files' ((name | parname) +);
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7895: \item [$\isarkeyword{header}~text$] provides plain text markup just preceding
wenzelm@7895:   the formal begin of a theory.  In actual document preparation the
wenzelm@7895:   corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
wenzelm@7895:   produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
wenzelm@7895:   \S\ref{sec:markup-prf} for further markup commands.
wenzelm@7895:   
wenzelm@7981: \item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
wenzelm@7981:   based on existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader
wenzelm@7981:   system ensures that any of the base theories are properly loaded (and fully
wenzelm@7981:   up-to-date when $\THEORY$ is executed interactively).  The optional
wenzelm@7981:   $\isarkeyword{files}$ specification declares additional dependencies on ML
wenzelm@7981:   files.  Unless put in parentheses, any file will be loaded immediately via
wenzelm@7981:   $\isarcmd{use}$ (see also \S\ref{sec:ML}).  The optional ML file
wenzelm@7981:   \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
wenzelm@7981:   included in $\isarkeyword{files}$, though.
wenzelm@7134:   
wenzelm@7895: \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
wenzelm@7981:   mode, so only a limited set of commands may be performed without destroying
wenzelm@7981:   the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
wenzelm@7981:   loaded and up-to-date.
wenzelm@7175:   
wenzelm@7167: \item [$\END$] concludes the current theory definition or context switch.
wenzelm@7981: Note that this command cannot be undone, but the whole theory definition has
wenzelm@7981: to be retracted.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7895: \subsection{Theory markup commands}\label{sec:markup-thy}
wenzelm@7134: 
wenzelm@7895: \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
wenzelm@7895: \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
wenzelm@7167:   \isarcmd{section} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{text} & : & \isartrans{theory}{theory} \\
wenzelm@7895:   \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7895: Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
wenzelm@7981: a structured way to insert text into the document generated from a theory (see
wenzelm@7895: \cite{isabelle-sys} for more information on Isabelle's document preparation
wenzelm@7895: tools).
wenzelm@7134: 
wenzelm@7895: \railalias{textraw}{text\_raw}
wenzelm@7895: \railterm{textraw}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7895:   ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
wenzelm@7335:   $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
wenzelm@7335:   and section headings.
wenzelm@7895: \item [$\TEXT$] specifies paragraphs of plain text, including references to
wenzelm@7895:   formal entities.\footnote{The latter feature is not yet supported.
wenzelm@7895:     Nevertheless, any source text of the form
wenzelm@7895:     ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved
wenzelm@7895:     for future use.}
wenzelm@7895: \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
wenzelm@7895:   without additional markup.  Thus the full range of document manipulations
wenzelm@7895:   becomes available.  A typical application would be to emit
wenzelm@7895:   \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
wenzelm@7895:   parts from the final document.\footnote{This requires the \texttt{comment}
wenzelm@7981:     package to be included in {\LaTeX}.}
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7895: Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
wenzelm@7981: macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
wenzelm@7895: \verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
wenzelm@7981: argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
wenzelm@7981: may be included here as well.
wenzelm@7895: 
wenzelm@8485: \medskip
wenzelm@8485: 
wenzelm@8485: Additional markup commands are available for proofs (see
wenzelm@7895: \S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
wenzelm@7895: declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
wenzelm@7895: elements just preceding the actual theory definition.
wenzelm@7895: 
wenzelm@7134: 
wenzelm@7135: \subsection{Type classes and sorts}\label{sec:classes}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{classes} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7167:   'classes' (classdecl comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'classrel' nameref '<' nameref comment?
wenzelm@7134:   ;
wenzelm@7134:   'defaultsort' sort comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass
wenzelm@7335:   of existing classes $\vec c$.  Cyclic class structures are ruled out.
wenzelm@7134: \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
wenzelm@7134:   existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
wenzelm@7895:   $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
wenzelm@7175:   introduce proven class relations.
wenzelm@7134: \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
wenzelm@7895:   any type variables given without sort constraints.  Usually, the default
wenzelm@7134:   sort would be only changed when defining new logics.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7315: \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{types} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{arities} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'types' (typespec '=' type infix? comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'typedecl' typespec infix? comment?
wenzelm@7134:   ;
wenzelm@7134:   'nonterminals' (name +) comment?
wenzelm@7134:   ;
wenzelm@7134:   'arities' (nameref '::' arity comment? +)
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
wenzelm@7134:   $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
wenzelm@7134:   as are available in Isabelle/HOL for example, type synonyms are just purely
wenzelm@7895:   syntactic abbreviations without any logical significance.  Internally, type
wenzelm@7981:   synonyms are fully expanded.
wenzelm@7134: \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
wenzelm@7895:   $t$, intended as an actual logical type.  Note that object-logics such as
wenzelm@7895:   Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
wenzelm@7175: \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm@7175:   $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm@7175:   Isabelle's inner syntax of terms or types.
wenzelm@7335: \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
wenzelm@7335:   signature of types by new type constructor arities.  This is done
wenzelm@7335:   axiomatically!  The $\isarkeyword{instance}$ command (see
wenzelm@7895:   \S\ref{sec:axclass}) provides a way to introduce proven type arities.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7981: \subsection{Constants and simple definitions}\label{sec:consts}
wenzelm@7134: 
wenzelm@7175: \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{defs} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'consts' (constdecl +)
wenzelm@7134:   ;
wenzelm@7608:   'defs' (axmdecl prop comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'constdefs' (constdecl prop comment? +)
wenzelm@7134:   ;
wenzelm@7134: 
wenzelm@7134:   constdecl: name '::' type mixfix? comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
wenzelm@7335:   scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
wenzelm@7895:   to the constants declared.
wenzelm@7335: \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
wenzelm@7335:   existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
wenzelm@7335:   form of equations admitted as constant definitions.
wenzelm@7335: \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
wenzelm@7335:   definitions of constants, using canonical name $c_def$ for the definitional
wenzelm@7335:   axiom.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7981: \subsection{Syntax and translations}\label{sec:syn-trans}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{syntax}\indexisarcmd{translations}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{translations} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'syntax' ('(' name 'output'? ')')? (constdecl +)
wenzelm@7134:   ;
wenzelm@7134:   'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
wenzelm@7134:   ;
wenzelm@7134:   transpat: ('(' nameref ')')? string
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm@7175:   except that the actual logical signature extension is omitted.  Thus the
wenzelm@7175:   context free grammar of Isabelle's inner syntax may be augmented in
wenzelm@7335:   arbitrary ways, independently of the logic.  The $mode$ argument refers to
wenzelm@7335:   the print mode that the grammar rules belong; unless there is the
wenzelm@7335:   \texttt{output} flag given, all productions are added both to the input and
wenzelm@7335:   output grammar.
wenzelm@7175: \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
wenzelm@7981:   rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
wenzelm@7895:   (\texttt{=>}), or print rules (\texttt{<=}).  Translation patterns may be
wenzelm@7895:   prefixed by the syntactic category to be used for parsing; the default is
wenzelm@7134:   \texttt{logic}.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{Axioms and theorems}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7135:   'axioms' (axmdecl prop comment? +)
wenzelm@7134:   ;
wenzelm@7134:   ('theorems' | 'lemmas') thmdef? thmrefs
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
wenzelm@7895:   axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
wenzelm@7895:   may be referred later just as any other theorem.
wenzelm@7134:   
wenzelm@7134:   Axioms are usually only introduced when declaring new logical systems.
wenzelm@7175:   Everyday work is typically done the hard way, with proper definitions and
wenzelm@7134:   actual theorems.
wenzelm@7335: \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
wenzelm@7981:   Typical applications would also involve attributes, to augment the
wenzelm@7335:   Simplifier context, for example.
wenzelm@7134: \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
wenzelm@7134:   tags the results as ``lemma''.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Name spaces}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{global}\indexisarcmd{local}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{global} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{local} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7895: Isabelle organizes any kind of name declarations (of types, constants,
wenzelm@7895: theorems etc.)  by hierarchically structured name spaces.  Normally the user
wenzelm@7895: never has to control the behavior of name space entry by hand, yet the
wenzelm@7895: following commands provide some way to do so.
wenzelm@7175: 
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm@7167:   name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm@7167:   mode, causing all names to be automatically qualified by the theory name.
wenzelm@7895:   Changing this to $\isarkeyword{global}$ causes all names to be declared
wenzelm@7895:   without the theory prefix, until $\isarkeyword{local}$ is declared again.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Incorporating ML code}\label{sec:ML}
wenzelm@7134: 
wenzelm@7895: \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134:   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7895:   \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
wenzelm@7175:   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7895: \railalias{MLsetup}{ML\_setup}
wenzelm@7895: \railterm{MLsetup}
wenzelm@7895: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'use' name
wenzelm@7134:   ;
wenzelm@7895:   ('ML' | MLsetup | 'setup') text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
wenzelm@7466:   The current theory context (if present) is passed down to the ML session,
wenzelm@7981:   but may not be modified.  Furthermore, the file name is checked with the
wenzelm@7466:   $\isarkeyword{files}$ dependency declaration given in the theory header (see
wenzelm@7466:   also \S\ref{sec:begin-thy}).
wenzelm@7466:   
wenzelm@7895: \item [$\isarkeyword{ML}~text$] executes ML commands from $text$.  The theory
wenzelm@7895:   context is passed in the same way as for $\isarkeyword{use}$.
wenzelm@7895:   
wenzelm@7895: \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
wenzelm@7895:   theory context is passed down to the ML session, and fetched back
wenzelm@7895:   afterwards.  Thus $text$ may actually change the theory as a side effect.
wenzelm@7895:   
wenzelm@7167: \item [$\isarkeyword{setup}~text$] changes the current theory context by
wenzelm@8379:   applying $text$, which refers to an ML expression of type
wenzelm@8379:   \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
wenzelm@8379:   canonical way to initialize object-logic specific tools and packages written
wenzelm@8379:   in ML.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@8250: \subsection{Syntax translation functions}
wenzelm@7134: 
wenzelm@8250: \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
wenzelm@8250: \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
wenzelm@8250: \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
wenzelm@8250: \begin{matharray}{rcl}
wenzelm@8250:   \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250:   \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250:   \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250:   \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250:   \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250:   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
wenzelm@8250: \end{matharray}
wenzelm@7134: 
wenzelm@8250: Syntax translation functions written in ML admit almost arbitrary
wenzelm@8250: manipulations of Isabelle's inner syntax.  Any of the above commands have a
wenzelm@8250: single \railqtoken{text} argument that refers to an ML expression of
wenzelm@8379: appropriate type.
wenzelm@8379: 
wenzelm@8379: \begin{ttbox}
wenzelm@8379: val parse_ast_translation   : (string * (ast list -> ast)) list
wenzelm@8379: val parse_translation       : (string * (term list -> term)) list
wenzelm@8379: val print_translation       : (string * (term list -> term)) list
wenzelm@8379: val typed_print_translation :
wenzelm@8379:   (string * (bool -> typ -> term list -> term)) list
wenzelm@8379: val print_ast_translation   : (string * (ast list -> ast)) list
wenzelm@8379: val token_translation       :
wenzelm@8379:   (string * string * (string -> string * real)) list
wenzelm@8379: \end{ttbox}
wenzelm@8379: See \cite[\S8]{isabelle-ref} for more information on syntax transformations.
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{Oracles}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{oracle}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7175: Oracles provide an interface to external reasoning systems, without giving up
wenzelm@7175: control completely --- each theorem carries a derivation object recording any
wenzelm@7175: oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'oracle' name '=' text comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
wenzelm@8379:   function $text$, which has to be of type
wenzelm@8379:   \texttt{Sign.sg~*~Object.T~->~term}.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \section{Proof commands}
wenzelm@7134: 
wenzelm@7987: Proof commands perform transitions of Isar/VM machine configurations, which
wenzelm@7315: are block-structured, consisting of a stack of nodes with three main
wenzelm@7335: components: logical proof context, current facts, and open goals.  Isar/VM
wenzelm@7335: transitions are \emph{typed} according to the following three three different
wenzelm@7335: modes of operation:
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$proof(prove)$] means that a new goal has just been stated that is now
wenzelm@7167:   to be \emph{proven}; the next command may refine it by some proof method
wenzelm@7895:   (read: tactic), and enter a sub-proof to establish the actual result.
wenzelm@7167: \item [$proof(state)$] is like an internal theory mode: the context may be
wenzelm@7987:   augmented by \emph{stating} additional assumptions, intermediate results
wenzelm@7987:   etc.
wenzelm@7895: \item [$proof(chain)$] is intermediate between $proof(state)$ and
wenzelm@7987:   $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
wenzelm@7987:   register) have been just picked up in order to be used when refining the
wenzelm@7987:   goal claimed next.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7167: 
wenzelm@7895: \subsection{Proof markup commands}\label{sec:markup-prf}
wenzelm@7167: 
wenzelm@7987: \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
wenzelm@7895: \indexisarcmd{txt}\indexisarcmd{txt-raw}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@8101:   \isarcmd{sect} & : & \isartrans{proof}{proof} \\
wenzelm@8101:   \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
wenzelm@8101:   \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
wenzelm@8101:   \isarcmd{txt} & : & \isartrans{proof}{proof} \\
wenzelm@8101:   \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7895: These markup commands for proof mode closely correspond to the ones of theory
wenzelm@7895: mode (see \S\ref{sec:markup-thy}).  Note that $\isarkeyword{txt_raw}$ is
wenzelm@7895: special in the same way as $\isarkeyword{text_raw}$.
wenzelm@7895: 
wenzelm@7895: \railalias{txtraw}{txt\_raw}
wenzelm@7895: \railterm{txtraw}
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7895:   ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7315: \subsection{Proof context}\label{sec:proof-context}
wenzelm@7134: 
wenzelm@7315: \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7315: The logical proof context consists of fixed variables and assumptions.  The
wenzelm@7315: former closely correspond to Skolem constants, or meta-level universal
wenzelm@7315: quantification as provided by the Isabelle/Pure logical framework.
wenzelm@7315: Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
wenzelm@7987: a local value that may be used in the subsequent proof as any other variable
wenzelm@7895: or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
wenzelm@7987: context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
wenzelm@7987: \All x \phi$ (this is expressed using Isabelle's meta-variables).
wenzelm@7315: 
wenzelm@7315: Similarly, introducing some assumption $\chi$ has two effects.  On the one
wenzelm@7315: hand, a local theorem is created that may be used as a fact in subsequent
wenzelm@7895: proof steps.  On the other hand, any result $\chi \drv \phi$ exported from the
wenzelm@7895: context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
wenzelm@7895: Thus, solving an enclosing goal using such a result would basically introduce
wenzelm@7895: a new subgoal stemming from the assumption.  How this situation is handled
wenzelm@7895: depends on the actual version of assumption command used: while $\ASSUMENAME$
wenzelm@7895: insists on solving the subgoal by unification with some premise of the goal,
wenzelm@7895: $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
wenzelm@7895: user.
wenzelm@7315: 
wenzelm@7319: Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
wenzelm@7987: combining $\FIX x$ with another version of assumption that causes any
wenzelm@7987: hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
wenzelm@7987: Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7431:   'fix' (vars + 'and') comment?
wenzelm@7134:   ;
wenzelm@7315:   ('assume' | 'presume') (assm comment? + 'and')
wenzelm@7134:   ;
wenzelm@7175:   'def' thmdecl? \\ var '==' term termpat? comment?
wenzelm@7134:   ;
wenzelm@7134: 
wenzelm@7134:   var: name ('::' type)?
wenzelm@7134:   ;
wenzelm@7458:   vars: (name+) ('::' type)?
wenzelm@7431:   ;
wenzelm@7315:   assm: thmdecl? (prop proppat? +)
wenzelm@7315:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7315: \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
wenzelm@7315: \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
wenzelm@7335:   $\Phi$ by assumption.  Subsequent results applied to an enclosing goal
wenzelm@7895:   (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
wenzelm@7335:   able to unify with existing premises in the goal, while $\PRESUMENAME$
wenzelm@7335:   leaves $\Phi$ as new subgoals.
wenzelm@7335:   
wenzelm@7335:   Several lists of assumptions may be given (separated by
wenzelm@7895:   $\isarkeyword{and}$); the resulting list of current facts consists of all of
wenzelm@7895:   these concatenated.
wenzelm@7315: \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
wenzelm@7315:   In results exported from the context, $x$ is replaced by $t$.  Basically,
wenzelm@7987:   $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
wenzelm@7335:   resulting hypothetical equation solved by reflexivity.
wenzelm@7431:   
wenzelm@7431:   The default name for the definitional equation is $x_def$.
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7895: The special name $prems$\indexisarthm{prems} refers to all assumptions of the
wenzelm@7895: current context as a list of theorems.
wenzelm@7315: 
wenzelm@7167: 
wenzelm@7167: \subsection{Facts and forward chaining}
wenzelm@7167: 
wenzelm@7167: \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm@7167: \begin{matharray}{rcl}
wenzelm@7167:   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167:   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167:   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167:   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167: \end{matharray}
wenzelm@7167: 
wenzelm@7319: New facts are established either by assumption or proof of local statements.
wenzelm@7335: Any fact will usually be involved in further proofs, either as explicit
wenzelm@7335: arguments of proof methods or when forward chaining towards the next goal via
wenzelm@7335: $\THEN$ (and variants).  Note that the special theorem name
wenzelm@7987: $this$\indexisarthm{this} refers to the most recently established facts.
wenzelm@7167: \begin{rail}
wenzelm@7167:   'note' thmdef? thmrefs comment?
wenzelm@7167:   ;
wenzelm@7167:   'then' comment?
wenzelm@7167:   ;
wenzelm@7167:   ('from' | 'with') thmrefs comment?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm@7175:   as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm@7175:   right hand sides.
wenzelm@7167: \item [$\THEN$] indicates forward chaining by the current facts in order to
wenzelm@7895:   establish the goal to be claimed next.  The initial proof method invoked to
wenzelm@7895:   refine that will be offered the facts to do ``anything appropriate'' (cf.\ 
wenzelm@7895:   also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
wenzelm@7895:   \S\ref{sec:pure-meth}) would typically do an elimination rather than an
wenzelm@7895:   introduction.  Automatic methods usually insert the facts into the goal
wenzelm@7895:   state before operation.
wenzelm@7335: \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
wenzelm@7458:   equivalent to $\FROM{this}$.
wenzelm@7175: \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
wenzelm@7175:   chaining is from earlier facts together with the current ones.
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7389: Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
wenzelm@7895: multiple facts to be given in their proper order, corresponding to a prefix of
wenzelm@7895: the premises of the rule involved.  Note that positions may be easily skipped
wenzelm@7458: using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example.  This involves
wenzelm@7895: the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure
wenzelm@7895: as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
wenzelm@7389: 
wenzelm@7167: 
wenzelm@7167: \subsection{Goal statements}
wenzelm@7167: 
wenzelm@7167: \indexisarcmd{theorem}\indexisarcmd{lemma}
wenzelm@7167: \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm@7167: \begin{matharray}{rcl}
wenzelm@7167:   \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167:   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7987:   \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
wenzelm@7987:   \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
wenzelm@7167:   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167:   \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167: \end{matharray}
wenzelm@7167: 
wenzelm@7175: Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
wenzelm@7895: and $\LEMMANAME$.  New local goals may be claimed within proof mode as well.
wenzelm@7895: Four variants are available, indicating whether the result is meant to solve
wenzelm@7987: some pending goal or whether forward chaining is employed.
wenzelm@7175: 
wenzelm@7167: \begin{rail}
wenzelm@7167:   ('theorem' | 'lemma') goal
wenzelm@7167:   ;
wenzelm@7167:   ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@7167:   ;
wenzelm@7167: 
wenzelm@7167:   goal: thmdecl? proppat comment?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
wenzelm@7895:   eventually resulting in some theorem $\turn \phi$ put back into the theory.
wenzelm@7987: \item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
wenzelm@7167:   ``lemma''.
wenzelm@7335: \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
wenzelm@7167:   theorem with the current assumption context as hypotheses.
wenzelm@7335: \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
wenzelm@7895:   pending goal with the result \emph{exported} into the corresponding context
wenzelm@7895:   (cf.\ \S\ref{sec:proof-context}).
wenzelm@7895: \item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
wenzelm@7895:   to be proven by forward chaining the current facts.  Note that $\HENCENAME$
wenzelm@7895:   is also equivalent to $\FROM{this}~\HAVENAME$.
wenzelm@7895: \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$.  Note that $\THUSNAME$ is
wenzelm@7895:   also equivalent to $\FROM{this}~\SHOWNAME$.
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7167: 
wenzelm@7167: \subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm@7167: 
wenzelm@7175: \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm@7175: \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm@7175: \begin{matharray}{rcl}
wenzelm@7175:   \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@7175:   \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175: \end{matharray}
wenzelm@7175: 
wenzelm@7335: Arbitrary goal refinement via tactics is considered harmful.  Consequently the
wenzelm@7335: Isar framework admits proof methods to be invoked in two places only.
wenzelm@7167: \begin{enumerate}
wenzelm@7175: \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
wenzelm@7335:   goal to a number of sub-goals that are to be solved later.  Facts are passed
wenzelm@7895:   to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
wenzelm@7167:   
wenzelm@7987: \item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
wenzelm@7987:   remaining goals.  No facts are passed to $m@2$.
wenzelm@7167: \end{enumerate}
wenzelm@7167: 
wenzelm@7335: The only other proper way to affect pending goals is by $\SHOWNAME$ (or
wenzelm@7335: $\THUSNAME$), which involves an explicit statement of what is to be solved.
wenzelm@7167: 
wenzelm@7175: \medskip
wenzelm@7175: 
wenzelm@7167: Also note that initial proof methods should either solve the goal completely,
wenzelm@7895: or constitute some well-understood reduction to new sub-goals.  Arbitrary
wenzelm@7895: automatic proof tools that are prone leave a large number of badly structured
wenzelm@7895: sub-goals are no help in continuing the proof document in any intelligible
wenzelm@7987: way.
wenzelm@7987: %FIXME
wenzelm@7987: %A more appropriate technique would be to $\SHOWNAME$ some non-trivial
wenzelm@7987: %reduction as an explicit rule, which is solved completely by some automated
wenzelm@7987: %method, and then applied to some pending goal.
wenzelm@7167: 
wenzelm@7175: \medskip
wenzelm@7175: 
wenzelm@7175: Unless given explicitly by the user, the default initial method is
wenzelm@7175: ``$default$'', which is usually set up to apply a single standard elimination
wenzelm@7458: or introduction rule according to the topmost symbol involved.  There is no
wenzelm@7987: separate default terminal method.  In any case, any goals left after that are
wenzelm@7987: solved by assumption as the very last step.
wenzelm@7167: 
wenzelm@7167: \begin{rail}
wenzelm@7167:   'proof' interest? meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   'qed' meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   'by' meth meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   ('.' | '..' | 'sorry') comment?
wenzelm@7167:   ;
wenzelm@7167: 
wenzelm@7167:   meth: method interest?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7335: \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
wenzelm@7335:   forward chaining are passed if so indicated by $proof(chain)$ mode.
wenzelm@7335: \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
wenzelm@7895:   concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
wenzelm@7895:   $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
wenzelm@7895:   from the result \emph{exported} into the enclosing goal context.  Thus
wenzelm@7895:   $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
wenzelm@7895:   rule does not fit to any pending goal\footnote{This includes any additional
wenzelm@7895:     ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
wenzelm@7895:   context.  Debugging such a situation might involve temporarily changing
wenzelm@7895:   $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
wenzelm@7895:   some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
wenzelm@7895: \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
wenzelm@7987:   abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
wenzelm@7987:   though.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
wenzelm@7895:   by expanding its definition; in many cases $\PROOF{m@1}$ is already
wenzelm@7175:   sufficient to see what is going wrong.
wenzelm@7895: \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
wenzelm@7895:   abbreviates $\BY{default}$.
wenzelm@7895: \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
wenzelm@8195:   abbreviates $\BY{this}$.
wenzelm@8379: \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the
wenzelm@8379:   \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the
wenzelm@8379:   goal without further ado.  Of course, the result is a fake theorem only,
wenzelm@8379:   involving some oracle in its internal derivation object (this is indicated
wenzelm@8379:   as ``$[!]$'' in the printed result).  The main application of $\SORRY$ is to
wenzelm@8379:   support experimentation and top-down proof development.
wenzelm@7315: \end{descr}
wenzelm@7315: 
wenzelm@7315: 
wenzelm@7315: \subsection{Term abbreviations}\label{sec:term-abbrev}
wenzelm@7315: 
wenzelm@7315: \indexisarcmd{let}
wenzelm@7315: \begin{matharray}{rcl}
wenzelm@7315:   \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315:   \isarkeyword{is} & : & syntax \\
wenzelm@7315: \end{matharray}
wenzelm@7315: 
wenzelm@7315: Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
wenzelm@7987: or by annotating assumptions or goal statements with a list of patterns
wenzelm@7987: $\ISS{p@1\;\dots}{p@n}$.  In both cases, higher-order matching is invoked to
wenzelm@7987: bind extra-logical term variables, which may be either named schematic
wenzelm@7987: variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
wenzelm@7987: (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
wenzelm@7987: patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
wenzelm@7987: postfix position.
wenzelm@7315: 
wenzelm@7319: Term abbreviations are quite different from actual local definitions as
wenzelm@7319: introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
wenzelm@7315: visible within the logic as actual equations, while abbreviations disappear
wenzelm@7315: during the input process just after type checking.
wenzelm@7315: 
wenzelm@7315: \begin{rail}
wenzelm@7315:   'let' ((term + 'as') '=' term comment? + 'and')
wenzelm@7315:   ;  
wenzelm@7315: \end{rail}
wenzelm@7315: 
wenzelm@7315: The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
wenzelm@7315: \railnonterm{proppat} (see \S\ref{sec:term-pats}).
wenzelm@7315: 
wenzelm@7315: \begin{descr}
wenzelm@7315: \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
wenzelm@7315:   by simultaneous higher-order matching against terms $\vec t$.
wenzelm@7315: \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
wenzelm@7315:   preceding statement.  Also note that $\ISNAME$ is not a separate command,
wenzelm@7315:   but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
wenzelm@7315: \end{descr}
wenzelm@7315: 
wenzelm@7988: A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
wenzelm@7988: and facts are available as well.  For any open goal,
wenzelm@7466: $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
wenzelm@7466: (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
wenzelm@7466: (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
wenzelm@7335: object-logical statement.  The latter two abstract over any meta-level
wenzelm@7987: parameters.
wenzelm@7315: 
wenzelm@7466: Fact statements resulting from assumptions or finished goals are bound as
wenzelm@7466: $\Var{this_prop}$\indexisarvar{this-prop},
wenzelm@7466: $\Var{this_concl}$\indexisarvar{this-concl}, and
wenzelm@7466: $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above.  In case
wenzelm@7466: $\Var{this}$ refers to an object-logic statement that is an application
wenzelm@7895: $f(t)$, then $t$ is bound to the special text variable
wenzelm@7466: ``$\dots$''\indexisarvar{\dots} (three dots).  The canonical application of
wenzelm@7987: the latter are calculational proofs (see \S\ref{sec:calculation}).
wenzelm@7315: 
wenzelm@7315: 
wenzelm@7134: \subsection{Block structure}
wenzelm@7134: 
wenzelm@7397: \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm@7397: \begin{matharray}{rcl}
wenzelm@8448:   \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7974:   \BG & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7974:   \EN & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7397: \end{matharray}
wenzelm@7397: 
wenzelm@7167: While Isar is inherently block-structured, opening and closing blocks is
wenzelm@7167: mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm@7167: local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm@7167: again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
wenzelm@8448: different context within a sub-proof may be switched via $\NEXT$, which is
wenzelm@8448: just a single block-close followed by block-open again.  Thus the effect of
wenzelm@8448: $\NEXT$ to reset the local proof context. There is no goal focus involved
wenzelm@8448: here!
wenzelm@7167: 
wenzelm@7175: For slightly more advanced applications, there are explicit block parentheses
wenzelm@7895: as well.  These typically achieve a stronger forward style of reasoning.
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@8448: \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
wenzelm@8448:   local context to the initial one.
wenzelm@7167: \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
wenzelm@7895:   close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
wenzelm@7895:   unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
wenzelm@7895:   \emph{exported} into the enclosing context.  Thus fixed variables are
wenzelm@7895:   generalized, assumptions discharged, and local definitions unfolded (cf.\ 
wenzelm@7895:   \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
wenzelm@7895:   $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
wenzelm@7895:   backward reasoning with the result exported at $\SHOWNAME$ time.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \section{Other commands}
wenzelm@7134: 
wenzelm@8448: \subsection{Diagnostics}\label{sec:diag}
wenzelm@7134: 
wenzelm@8485: \indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
wenzelm@8485: \indexisarcmd{print-facts}\indexisarcmd{print-binds}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@8485:   \isarcmd{pr} & : & \isarkeep{\cdot} \\
wenzelm@7974:   \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134:   \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134:   \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
wenzelm@7974:   \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
wenzelm@8379:   \isarcmd{print_facts} & : & \isarkeep{proof} \\
wenzelm@8379:   \isarcmd{print_binds} & : & \isarkeep{proof} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7335: These commands are not part of the actual Isabelle/Isar syntax, but assist
wenzelm@7335: interactive development.  Also note that $undo$ does not apply here, since the
wenzelm@7335: theory or proof configuration is not changed.
wenzelm@7335: 
wenzelm@7134: \begin{rail}
wenzelm@8485:   'pr' modes? nat?
wenzelm@7134:   ;
wenzelm@8485:   'thm' modes? thmrefs
wenzelm@8485:   ;
wenzelm@8485:   'term' modes? term
wenzelm@7134:   ;
wenzelm@8485:   'prop' modes? prop
wenzelm@7134:   ;
wenzelm@8485:   'typ' modes? type
wenzelm@8485:   ;
wenzelm@8485: 
wenzelm@8485:   modes: '(' (name + ) ')'
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@8485: \item [$\isarkeyword{pr}~n$] prints the current top-level state, i.e.\ the
wenzelm@8485:   theory identifier or proof state.  The latter includes the proof context,
wenzelm@8485:   current facts and goals.  The optional argument $n$ affects the implicit
wenzelm@8485:   limit of goals to be displayed, which is initially 10.  Omitting the limit
wenzelm@8485:   leaves the value unchanged.
wenzelm@7974: \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
wenzelm@7974:   theory or proof context.  Note that any attributes included in the theorem
wenzelm@7974:   specifications are applied to a temporary context derived from the current
wenzelm@7974:   theory or proof; the result is discarded, i.e.\ attributes involved in
wenzelm@7974:   $thms$ do not have any permanent effect.
wenzelm@7987: \item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
wenzelm@7987:   print terms or propositions according to the current theory or proof
wenzelm@7895:   context; the inferred type of $t$ is output as well.  Note that these
wenzelm@7895:   commands are also useful in inspecting the current environment of term
wenzelm@7895:   abbreviations.
wenzelm@7974: \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
wenzelm@7974:   according to the current theory or proof context.
wenzelm@8379: \item [$\isarkeyword{print_facts}$] prints any named facts of the current
wenzelm@8379:   context, including assumptions and local results.
wenzelm@8379: \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
wenzelm@8379:   the context.
wenzelm@8485: \end{descr}
wenzelm@8485: 
wenzelm@8485: The basic diagnostic commands above admit a list of $modes$ to be specified,
wenzelm@8485: which is appended to the current print mode (see also \cite{isabelle-ref}).
wenzelm@8485: Thus the output behavior may be modified according particular print mode
wenzelm@8485: features.
wenzelm@8485: 
wenzelm@8485: \medskip
wenzelm@8485: 
wenzelm@8485: For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would print the
wenzelm@8485: current proof state with mathematical symbols and special characters
wenzelm@8485: represented in {\LaTeX} source, according to the Isabelle style
wenzelm@8485: \cite{isabelle-sys}.  The resulting text can be directly pasted into and
wenzelm@8485: \verb,\begin{isabelle},\dots\verb,\end{isabelle}, environment.
wenzelm@8485: 
wenzelm@8485: Note that $\isarkeyword{pr}~(latex)$ is sufficient to achieve the same output,
wenzelm@8485: if the current Isabelle session has the other modes already activated, say due
wenzelm@8485: to some particular user interface configuration such as Proof~General
wenzelm@8485: \cite{proofgeneral} with X-Symbol mode \cite{FIXME}.
wenzelm@8485: 
wenzelm@8485: 
wenzelm@8485: \subsection{History commands}\label{sec:history}
wenzelm@8485: 
wenzelm@8485: \indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill}
wenzelm@8485: \begin{matharray}{rcl}
wenzelm@8485:   \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\
wenzelm@8485:   \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\
wenzelm@8485:   \isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\
wenzelm@8485: \end{matharray}
wenzelm@8485: 
wenzelm@8485: The Isabelle/Isar top-level maintains a two-stage history, for theory and
wenzelm@8485: proof state transformation.  Basically, any command can be undone using
wenzelm@8485: $\isarkeyword{undo}$, excluding mere diagnostic elements.  Its effect may be
wenzelm@8485: revoked via $\isarkeyword{redo}$, unless the corresponding the
wenzelm@8485: $\isarkeyword{undo}$ step has crossed the beginning of a proof or theory.  The
wenzelm@8485: $\isarkeyword{kill}$ command aborts the current history node altogether,
wenzelm@8485: discontinuing a proof or even the whole theory.  This operation is \emph{not}
wenzelm@8485: undoable.
wenzelm@8485: 
wenzelm@8485: \begin{warn}
wenzelm@8485:   History commands may not be used with user interfaces such as Proof~General
wenzelm@8485:   \cite{proofgeneral}, which takes care of stepping forth and back itself.
wenzelm@8485:   Interfering with manual $\isarkeyword{undo}$, $\isarkeyword{redo}$, or even
wenzelm@8485:   $\isarkeyword{kill}$ commands would quickly result in utter confusion.
wenzelm@8485: \end{warn}
wenzelm@8485: 
wenzelm@8485: \begin{descr}
wenzelm@8485: \item [$\isarkeyword{undo}$] revokes the latest state-transforming command.
wenzelm@8485: \item [$\isarkeyword{redo}$] undos the latest $\isarkeyword{undo}$.
wenzelm@8485: \item [$\isarkeyword{kill}$] aborts the current history level.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@8379: \subsection{Meta-linguistic features}
wenzelm@8379: 
wenzelm@8379: \indexisarcmd{oops}
wenzelm@8379: \begin{matharray}{rcl}
wenzelm@8379:   \isarcmd{oops}^* & : & \isartrans{proof}{theory} \\
wenzelm@8379: \end{matharray}
wenzelm@8379: 
wenzelm@8379: The $\OOPS$ command discontinues the current proof attempt, while considering
wenzelm@8379: the partial proof text as properly processed.  This is conceptually quite
wenzelm@8379: different from ``faking'' actual proofs via $\SORRY$ (see
wenzelm@8379: \S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
wenzelm@8379: but goes back right to the theory level.  Furthermore, $\OOPS$ does not
wenzelm@8379: produce any result theorem --- there is no claim to be able to complete the
wenzelm@8379: proof anyhow.
wenzelm@8379: 
wenzelm@8379: A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
wenzelm@8379: system itself, in conjunction with the document preparation tools of Isabelle
wenzelm@8379: described in \cite{isabelle-sys}.  Thus partial or even wrong proof attempts
wenzelm@8379: can be discussed in a logically sound manner.  Note that the Isabelle {\LaTeX}
wenzelm@8379: macros can be easily adapted to print something like ``$\dots$'' instead of an
wenzelm@8379: ``$\OOPS$'' keyword.
wenzelm@8379: 
wenzelm@8485: \medskip The $\OOPS$ command is undoable, in contrast to $\isarkeyword{kill}$
wenzelm@8485: (see \S\ref{sec:history}).  The effect is to get back to the theory
wenzelm@8485: \emph{before} the opening of the proof.
wenzelm@8485: 
wenzelm@8485: \begin{descr}
wenzelm@8485: \item [$\isarkeyword{oops}$] dismisses the current proof, leaving the text in
wenzelm@8485:   as properly processed.
wenzelm@8485: \end{descr}
wenzelm@8485: 
wenzelm@8379: 
wenzelm@7134: \subsection{System operations}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
wenzelm@7167: \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{cd} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{pwd} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
wenzelm@7134:   process.
wenzelm@7134: \item [$\isarkeyword{pwd}~$] prints the current working directory.
wenzelm@7175: \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
wenzelm@7987:   $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
wenzelm@7895:   theory given as $name$ argument.  These commands are basically the same as
wenzelm@7987:   the corresponding ML functions\footnote{The ML versions also change the
wenzelm@7987:     implicit theory context to that of the theory loaded.}  (see also
wenzelm@7987:   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
wenzelm@7987:   load new- and old-style theories alike.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7987: These system commands are scarcely used when working with the Proof~General
wenzelm@7987: interface, since loading of theories is done fully transparently.
wenzelm@7134: 
wenzelm@8379: 
wenzelm@8379: \subsection{Emulating tactic scripts}
wenzelm@8379: 
wenzelm@8379: The following elements emulate unstructured tactic scripts to some extent.
wenzelm@8379: While these are anathema for writing proper Isar proof documents, they might
wenzelm@8379: come in handy for interactive exploration and debugging.
wenzelm@8379: 
wenzelm@8379: \indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{back}\indexisarmeth{tactic}
wenzelm@8379: \begin{matharray}{rcl}
wenzelm@8379:   \isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\
wenzelm@8485:   \isarcmd{apply_end} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@8485:   \isarcmd{back} & : & \isartrans{proof}{proof} \\
wenzelm@8379:   tactic & : & \isarmeth \\
wenzelm@8379: \end{matharray}
wenzelm@8379: 
wenzelm@8379: \railalias{applyend}{apply\_end}
wenzelm@8379: \railterm{applyend}
wenzelm@8379: 
wenzelm@8379: \begin{rail}
wenzelm@8379:   'apply' method
wenzelm@8379:   ;
wenzelm@8379:   applyend method
wenzelm@8379:   ;
wenzelm@8379:   'tactic' text
wenzelm@8379:   ;
wenzelm@8379: \end{rail}
wenzelm@8379: 
wenzelm@8379: \begin{descr}
wenzelm@8379: \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial
wenzelm@8379:   position, but retains ``$prove$'' mode (unlike $\PROOFNAME$).  Thus
wenzelm@8379:   consecutive method applications may be given just as in tactic scripts.  In
wenzelm@8379:   order to complete the proof properly, any of the actual structured proof
wenzelm@8379:   commands (e.g.\ ``$\DOT$'') has to be given eventually.
wenzelm@8379:   
wenzelm@8379:   Facts are passed to $m$ as indicated by the goal's forward-chain mode.
wenzelm@8379:   Common use of $\isarkeyword{apply}$ would be in a purely backward manner,
wenzelm@8379:   though.
wenzelm@8379: \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
wenzelm@8379:   terminal position.  Basically, this simulates a multi-step tactic script for
wenzelm@8379:   $\QEDNAME$, but may be given anywhere within the proof body.
wenzelm@8379:   
wenzelm@8379:   No facts are passed to $m$.  Furthermore, the static context is that of the
wenzelm@8379:   enclosing goal (as for actual $\QEDNAME$).  Thus the proof method may not
wenzelm@8379:   refer to any assumptions introduced in the current body, for example.
wenzelm@8485: \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
wenzelm@8485:   the latest proof command.\footnote{Unlike the ML function \texttt{back}
wenzelm@8485:     \cite{isabelle-ref}, the Isar command does not search upwards for further
wenzelm@8485:     branch points.} Basically, any proof command may return multiple results.
wenzelm@8379: \item [$tactic~text$] produces a proof method from any ML text of type
wenzelm@8379:   \texttt{tactic}.  Apart from the usual ML environment, and the current
wenzelm@8379:   implicit theory context, the ML code may refer to the following locally
wenzelm@8379:   bound values:
wenzelm@8485: %%FIXME ttbox produces too much trailing space
wenzelm@8485: {\footnotesize\begin{verbatim}
wenzelm@8379: val ctxt  : Proof.context
wenzelm@8379: val facts : thm list
wenzelm@8379: val thm   : string -> thm
wenzelm@8379: val thms  : string -> thm list
wenzelm@8485: \end{verbatim}}
wenzelm@8379:   Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
wenzelm@8379:   indicates any current facts for forward-chaining, and
wenzelm@8379:   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
wenzelm@8379:   theorems) from the context.
wenzelm@8379: \end{descr}
wenzelm@8379: 
wenzelm@8379: 
wenzelm@7046: %%% Local Variables: 
wenzelm@7046: %%% mode: latex
wenzelm@7046: %%% TeX-master: "isar-ref"
wenzelm@7046: %%% End: 




