--- a/doc-src/IsarRef/IsaMakefile Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile Fri May 02 16:36:05 2008 +0200
@@ -22,7 +22,7 @@
Thy: $(LOG)/HOL-Thy.gz
$(LOG)/HOL-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
- Thy/syntax.thy
+ Thy/pure.thy Thy/syntax.thy
@$(USEDIR) HOL Thy
--- a/doc-src/IsarRef/Makefile Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Makefile Fri May 02 16:36:05 2008 +0200
@@ -13,8 +13,8 @@
NAME = isar-ref
-FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex pure.tex \
- generic.tex logics.tex refcard.tex conversion.tex \
+FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex \
+ Thy/document/pure.tex generic.tex logics.tex refcard.tex conversion.tex \
../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
--- a/doc-src/IsarRef/Thy/ROOT.ML Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Fri May 02 16:36:05 2008 +0200
@@ -4,3 +4,4 @@
use "../../antiquote_setup.ML";
use_thy "intro";
use_thy "syntax";
+use_thy "pure";
--- a/doc-src/IsarRef/Thy/document/intro.tex Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex Fri May 02 16:36:05 2008 +0200
@@ -4,6 +4,7 @@
%
\isadelimtheory
\isanewline
+\isanewline
%
\endisadelimtheory
%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/pure.tex Fri May 02 16:36:05 2008 +0200
@@ -0,0 +1,1806 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{pure}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ pure\isanewline
+\isakeyword{imports}\ CPure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Basic language elements \label{ch:pure-syntax}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Subsequently, we introduce the main part of Pure theory and proof
+ commands, together with fundamental proof methods and attributes.
+ \Chref{ch:gen-tools} describes further Isar elements provided by
+ generic tools and packages (such as the Simplifier) that are either
+ part of Pure Isabelle or pre-installed in most object logics.
+ \Chref{ch:logics} refers to object-logic specific elements (mainly
+ for HOL and ZF).
+
+ \medskip Isar commands may be either \emph{proper} document
+ constructors, or \emph{improper commands}. Some proof methods and
+ attributes introduced later are classified as improper as well.
+ Improper Isar language elements, which are subsequently marked by
+ ``\isa{\isactrlsup {\isacharasterisk}}'', are often helpful when developing proof
+ documents, while their use is discouraged for the final
+ human-readable outcome. Typical examples are diagnostic commands
+ that print terms or theorems according to the current context; other
+ commands emulate old-style tactical theorem proving.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Theory commands%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Defining theories \label{sec:begin-thy}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{header}\isa{\isacommand{header}} & : & \isarkeep{toplevel} \\
+ \indexdef{}{command}{theory}\isa{\isacommand{theory}} & : & \isartrans{toplevel}{theory} \\
+ \indexdef{}{command}{end}\isa{\isacommand{end}} & : & \isartrans{theory}{toplevel} \\
+ \end{matharray}
+
+ Isabelle/Isar theories are defined via theory, which contain both
+ specifications and proofs; occasionally definitional mechanisms also
+ require some explicit proof.
+
+ The first ``real'' command of any theory has to be \isa{\isacommand{theory}}, which starts a new theory based on the merge of existing
+ ones. Just preceding the \isa{\isacommand{theory}} keyword, there may be
+ an optional \isa{\isacommand{header}} declaration, which is relevant to
+ document preparation only; it acts very much like a special
+ pre-theory markup command (cf.\ \secref{sec:markup-thy} and
+ \secref{sec:markup-thy}). The \isa{\isacommand{end}} command concludes a
+ theory development; it has to be the very last command of any theory
+ file loaded in batch-mode.
+
+ \begin{rail}
+ 'header' text
+ ;
+ 'theory' name 'imports' (name +) uses? 'begin'
+ ;
+
+ uses: 'uses' ((name | parname) +);
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{header}}~\isa{text}] provides plain text
+ markup just preceding the formal beginning of a theory. In actual
+ document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
+ headings. See also \secref{sec:markup-thy} and
+ \secref{sec:markup-prf} for further markup commands.
+
+ \item [\isa{\isacommand{theory}}~\isa{A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}}] starts a new theory \isa{A} based on the
+ merge of existing theories \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}.
+
+ Due to inclusion of several ancestors, the overall theory structure
+ emerging in an Isabelle session forms a directed acyclic graph
+ (DAG). Isabelle's theory loader ensures that the sources
+ contributing to the development graph are always up-to-date.
+ Changed files are automatically reloaded when processing theory
+ headers.
+
+ The optional \indexdef{}{keyword}{uses}\isa{\isakeyword{uses}} specification declares additional
+ dependencies on extra files (usually ML sources). Files will be
+ loaded immediately (as ML), unless the name is put in parentheses,
+ which merely documents the dependency to be resolved later in the
+ text (typically via explicit \indexref{}{command}{use}\isa{\isacommand{use}} in the body text,
+ see \secref{sec:ML}).
+
+ \item [\isa{\isacommand{end}}] concludes the current theory definition or
+ context switch.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Markup commands \label{sec:markup-thy}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{chapter}\isa{\isacommand{chapter}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{section}\isa{\isacommand{section}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{subsection}\isa{\isacommand{subsection}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{subsubsection}\isa{\isacommand{subsubsection}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{text}\isa{\isacommand{text}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{text-raw}\isa{\isacommand{text{\isacharunderscore}raw}} & : & \isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ Apart from formal comments (see \secref{sec:comments}), markup
+ commands provide a structured way to insert text into the document
+ generated from a theory (see \cite{isabelle-sys} for more
+ information on Isabelle's document preparation tools).
+
+ \begin{rail}
+ ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
+ ;
+ 'text\_raw' text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{chapter}}, \isa{\isacommand{section}}, \isa{\isacommand{subsection}}, and \isa{\isacommand{subsubsection}}] mark chapter and
+ section headings.
+
+ \item [\isa{\isacommand{text}}] specifies paragraphs of plain text.
+
+ \item [\isa{\isacommand{text{\isacharunderscore}raw}}] inserts {\LaTeX} source into the
+ output, without additional markup. Thus the full range of document
+ manipulations becomes available.
+
+ \end{descr}
+
+ The \isa{text} argument of these markup commands (except for
+ \isa{\isacommand{text{\isacharunderscore}raw}}) may contain references to formal entities
+ (``antiquotations'', see also \secref{sec:antiq}). These are
+ interpreted in the present theory context, or the named \isa{target}.
+
+ Any of these markup elements corresponds to a {\LaTeX} command with
+ the name prefixed by \verb|\isamarkup|. For the sectioning
+ commands this is a plain macro with a single argument, e.g.\
+ \verb|\isamarkupchapter{|\isa{{\isasymdots}}\verb|}| for
+ \isa{\isacommand{chapter}}. The \isa{\isacommand{text}} markup results in a
+ {\LaTeX} environment \verb|\begin{isamarkuptext}|~\isa{{\isasymdots}}~\verb|\end{isamarkuptext}|, while \isa{\isacommand{text{\isacharunderscore}raw}}
+ causes the text to be inserted directly into the {\LaTeX} source.
+
+ \medskip Additional markup commands are available for proofs (see
+ \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\isa{\isacommand{header}} declaration (see \secref{sec:begin-thy}) admits to insert
+ section markup just preceding the actual theory definition.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{classes}\isa{\isacommand{classes}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{classrel}\isa{\isacommand{classrel}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \indexdef{}{command}{defaultsort}\isa{\isacommand{defaultsort}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{class-deps}\isa{\isacommand{class{\isacharunderscore}deps}} & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'classes' (classdecl +)
+ ;
+ 'classrel' (nameref ('<' | subseteq) nameref + 'and')
+ ;
+ 'defaultsort' sort
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{classes}}~\isa{c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}]
+ declares class \isa{c} to be a subclass of existing classes \isa{c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}. Cyclic class structures are not permitted.
+
+ \item [\isa{\isacommand{classrel}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}] states
+ subclass relations between existing classes \isa{c\isactrlsub {\isadigit{1}}} and
+ \isa{c\isactrlsub {\isadigit{2}}}. This is done axiomatically! The \indexref{}{command}{instance}\isa{\isacommand{instance}} command (see \secref{sec:axclass}) provides a way to
+ introduce proven class relations.
+
+ \item [\isa{\isacommand{defaultsort}}~\isa{s}] makes sort \isa{s} the
+ new default sort for any type variables given without sort
+ constraints. Usually, the default sort would be only changed when
+ defining a new object-logic.
+
+ \item [\isa{\isacommand{class{\isacharunderscore}deps}}] visualizes the subclass relation,
+ using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{types}\isa{\isacommand{types}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{typedecl}\isa{\isacommand{typedecl}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{nonterminals}\isa{\isacommand{nonterminals}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{arities}\isa{\isacommand{arities}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \end{matharray}
+
+ \begin{rail}
+ 'types' (typespec '=' type infix? +)
+ ;
+ 'typedecl' typespec infix?
+ ;
+ 'nonterminals' (name +)
+ ;
+ 'arities' (nameref '::' arity +)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{types}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}}]
+ introduces \emph{type synonym} \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t}
+ for existing type \isa{{\isasymtau}}. 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.
+
+ \item [\isa{\isacommand{typedecl}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t}]
+ declares a new type constructor \isa{t}, intended as an actual
+ logical type (of the object-logic, if available).
+
+ \item [\isa{\isacommand{nonterminals}}~\isa{c}] declares type
+ constructors \isa{c} (without arguments) to act as purely
+ syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
+ syntax of terms or types.
+
+ \item [\isa{\isacommand{arities}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s}] augments Isabelle's order-sorted signature of types by new type
+ constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\isa{\isacommand{instance}} command (see \S\ref{sec:axclass}) provides a way to
+ introduce proven type arities.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Primitive constants and definitions \label{sec:consts}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Definitions essentially express abbreviations within the logic. The
+ simplest form of a definition is \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
+ where the arguments of \isa{c} appear on the left, abbreviating a
+ prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t} may be
+ written more conveniently as \isa{c\ x\ y\ {\isasymequiv}\ t}. Moreover,
+ definitions may be weakened by adding arbitrary pre-conditions:
+ \isa{A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t}.
+
+ \medskip The built-in well-formedness conditions for definitional
+ specifications are:
+
+ \begin{itemize}
+
+ \item Arguments (on the left-hand side) must be distinct variables.
+
+ \item All variables on the right-hand side must also appear on the
+ left-hand side.
+
+ \item All type variables on the right-hand side must also appear on
+ the left-hand side; this prohibits \isa{{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}} for example.
+
+ \item The definition must not be recursive. Most object-logics
+ provide definitional principles that can be used to express
+ recursion safely.
+
+ \end{itemize}
+
+ Overloading means that a constant being declared as \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl} may be defined separately on type instances \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
+ recursively at type instances corresponding to the immediate
+ argument types \isa{{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n}. Incomplete
+ specification patterns impose global constraints on all occurrences,
+ e.g.\ \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}} on the left-hand side means that all
+ corresponding occurrences on some right-hand side need to be an
+ instance of this, general \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}} will be disallowed.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{consts}\isa{\isacommand{consts}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{defs}\isa{\isacommand{defs}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{constdefs}\isa{\isacommand{constdefs}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'consts' ((name '::' type mixfix?) +)
+ ;
+ 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
+ ;
+ \end{rail}
+
+ \begin{rail}
+ 'constdefs' structs? (constdecl? constdef +)
+ ;
+
+ structs: '(' 'structure' (vars + 'and') ')'
+ ;
+ constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
+ ;
+ constdef: thmdecl? prop
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{consts}}~\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}] declares constant
+ \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
+ optional mixfix annotations may attach concrete syntax to the
+ constants declared.
+
+ \item [\isa{\isacommand{defs}}~\isa{name{\isacharcolon}\ eqn}] introduces \isa{eqn}
+ as a definitional axiom for some existing constant.
+
+ The \isa{{\isacharparenleft}unchecked{\isacharparenright}} option disables global dependency checks
+ for this definition, which is occasionally useful for exotic
+ overloading. It is at the discretion of the user to avoid malformed
+ theory specifications!
+
+ The \isa{{\isacharparenleft}overloaded{\isacharparenright}} option declares definitions to be
+ potentially overloaded. Unless this option is given, a warning
+ message would be issued for any definitional equation with a more
+ special type than that of the corresponding constant declaration.
+
+ \item [\isa{\isacommand{constdefs}}] provides a streamlined combination of
+ constants declarations and definitions: type-inference takes care of
+ the most general typing of the given specification (the optional
+ type constraint may refer to type-inference dummies ``\verb|_|'' as usual). The resulting type declaration needs to agree with
+ that of the specification; overloading is \emph{not} supported here!
+
+ The constant name may be omitted altogether, if neither type nor
+ syntax declarations are given. The canonical name of the
+ definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
+ unless specified otherwise. Also note that the given list of
+ specifications is processed in a strictly sequential manner, with
+ type-checking being performed independently.
+
+ An optional initial context of \isa{{\isacharparenleft}structure{\isacharparenright}} declarations
+ admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isasymindex}}''). The latter concept is
+ particularly useful with locales (see also \S\ref{sec:locale}).
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax and translations \label{sec:syn-trans}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{syntax}\isa{\isacommand{syntax}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no-syntax}\isa{\isacommand{no{\isacharunderscore}syntax}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{translations}\isa{\isacommand{translations}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no-translations}\isa{\isacommand{no{\isacharunderscore}translations}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \railalias{rightleftharpoons}{\isasymrightleftharpoons}
+ \railterm{rightleftharpoons}
+
+ \railalias{rightharpoonup}{\isasymrightharpoonup}
+ \railterm{rightharpoonup}
+
+ \railalias{leftharpoondown}{\isasymleftharpoondown}
+ \railterm{leftharpoondown}
+
+ \begin{rail}
+ ('syntax' | 'no\_syntax') mode? (constdecl +)
+ ;
+ ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+ ;
+
+ mode: ('(' ( name | 'output' | name 'output' ) ')')
+ ;
+ transpat: ('(' nameref ')')? string
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{syntax}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] is similar to
+ \isa{\isacommand{consts}}~\isa{decls}, except that the actual logical
+ signature extension is omitted. Thus the context free grammar of
+ Isabelle's inner syntax may be augmented in arbitrary ways,
+ independently of the logic. The \isa{mode} argument refers to the
+ print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\isa{\isakeyword{output}} indicator is given, all productions are added both to the
+ input and output grammar.
+
+ \item [\isa{\isacommand{no{\isacharunderscore}syntax}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] removes
+ grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \isa{\isacommand{syntax}} above.
+
+ \item [\isa{\isacommand{translations}}~\isa{rules}] specifies syntactic
+ translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isasymrightleftharpoons}}),
+ parse rules (\isa{{\isasymrightharpoonup}}), or print rules (\isa{{\isasymleftharpoondown}}).
+ Translation patterns may be prefixed by the syntactic category to be
+ used for parsing; the default is \isa{logic}.
+
+ \item [\isa{\isacommand{no{\isacharunderscore}translations}}~\isa{rules}] removes syntactic
+ translation rules, which are interpreted in the same manner as for
+ \isa{\isacommand{translations}} above.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcll}
+ \indexdef{}{command}{axioms}\isa{\isacommand{axioms}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \indexdef{}{command}{lemmas}\isa{\isacommand{lemmas}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{theorems}\isa{\isacommand{theorems}} & : & isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'axioms' (axmdecl prop +)
+ ;
+ ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{axioms}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduces arbitrary
+ statements as axioms of the meta-logic. In fact, axioms are
+ ``axiomatic theorems'', and may be referred later just as any other
+ theorem.
+
+ Axioms are usually only introduced when declaring new logical
+ systems. Everyday work is typically done the hard way, with proper
+ definitions and proven theorems.
+
+ \item [\isa{\isacommand{lemmas}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
+ retrieves and stores existing facts in the theory context, or the
+ specified target context (see also \secref{sec:target}). Typical
+ applications would also involve attributes, to declare Simplifier
+ rules, for example.
+
+ \item [\isa{\isacommand{theorems}}] is essentially the same as \isa{\isacommand{lemmas}}, but marks the result as a different kind of facts.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Name spaces%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{global}\isa{\isacommand{global}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{local}\isa{\isacommand{local}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{hide}\isa{\isacommand{hide}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'hide' ('(open)')? name (nameref + )
+ ;
+ \end{rail}
+
+ Isabelle organizes any kind of name declarations (of types,
+ constants, theorems etc.) by separate hierarchically structured name
+ spaces. Normally the user does not have to control the behavior of
+ name spaces by hand, yet the following commands provide some way to
+ do so.
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{global}} and \isa{\isacommand{local}}] change the
+ current name declaration mode. Initially, theories start in
+ \isa{\isacommand{local}} mode, causing all names to be automatically
+ qualified by the theory name. Changing this to \isa{\isacommand{global}}
+ causes all names to be declared without the theory prefix, until
+ \isa{\isacommand{local}} is declared again.
+
+ Note that global names are prone to get hidden accidently later,
+ when qualified names of the same base name are introduced.
+
+ \item [\isa{\isacommand{hide}}~\isa{space\ names}] fully removes
+ declarations from a given name space (which may be \isa{class},
+ \isa{type}, \isa{const}, or \isa{fact}); with the \isa{{\isacharparenleft}open{\isacharparenright}} option, only the base name is hidden. Global
+ (unqualified) names may never be hidden.
+
+ Note that hiding name space accesses has no impact on logical
+ declarations -- they remain valid internally. Entities that are no
+ longer accessible to the user are printed with the special qualifier
+ ``\isa{{\isacharquery}{\isacharquery}}'' prefixed to the full internal name.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Incorporating ML code \label{sec:ML}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{use}\isa{\isacommand{use}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ \indexdef{}{command}{ML}\isa{\isacommand{ML}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ \indexdef{}{command}{ML-val}\isa{\isacommand{ML{\isacharunderscore}val}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{ML-command}\isa{\isacommand{ML{\isacharunderscore}command}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{setup}\isa{\isacommand{setup}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{method-setup}\isa{\isacommand{method{\isacharunderscore}setup}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'use' name
+ ;
+ ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
+ ;
+ 'method\_setup' name '=' text text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{use}}~\isa{file}] reads and executes ML
+ commands from \isa{file}. The current theory context is passed
+ down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with
+ the \indexref{}{keyword}{uses}\isa{\isakeyword{uses}} dependency declaration given in the theory
+ header (see also \secref{sec:begin-thy}).
+
+ \item [\isa{\isacommand{ML}}~\isa{text}] is similar to \isa{\isacommand{use}}, but executes ML commands directly from the given \isa{text}.
+
+ \item [\isa{\isacommand{ML{\isacharunderscore}val}} and \isa{\isacommand{ML{\isacharunderscore}command}}] are
+ diagnostic versions of \isa{\isacommand{ML}}, which means that the context
+ may not be updated. \isa{\isacommand{ML{\isacharunderscore}val}} echos the bindings produced
+ at the ML toplevel, but \isa{\isacommand{ML{\isacharunderscore}command}} is silent.
+
+ \item [\isa{\isacommand{setup}}~\isa{text}] changes the current theory
+ context by applying \isa{text}, which refers to an ML expression
+ of type \verb|theory -> theory|. This enables to initialize
+ any object-logic specific tools and packages written in ML, for
+ example.
+
+ \item [\isa{\isacommand{method{\isacharunderscore}setup}}~\isa{name\ {\isacharequal}\ text\ description}]
+ defines a proof method in the current theory. The given \isa{text} has to be an ML expression of type \verb|Args.src ->|\isasep\isanewline%
+\verb| Proof.context -> Proof.method|. Parsing concrete method syntax
+ from \verb|Args.src| input can be quite tedious in general. The
+ following simple examples are for methods without any explicit
+ arguments, or a list of theorems, respectively.
+
+%FIXME proper antiquotations
+{\footnotesize
+\begin{verbatim}
+ Method.no_args (Method.METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt =>
+ Method.METHOD (fn facts => foobar_tac))
+\end{verbatim}
+}
+
+ Note that mere tactic emulations may ignore the \isa{facts}
+ parameter above. Proper proof methods would do something
+ appropriate with the list of current facts, though. Single-rule
+ methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
+ using \verb|Method.insert_tac| before applying the main tactic.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax translation functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{parse-ast-translation}\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{parse-translation}\isa{\isacommand{parse{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print-translation}\isa{\isacommand{print{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{typed-print-translation}\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print-ast-translation}\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{token-translation}\isa{\isacommand{token{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
+ 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+ ;
+
+ 'token\_translation' text
+ ;
+ \end{rail}
+
+ Syntax translation functions written in ML admit almost arbitrary
+ manipulations of Isabelle's inner syntax. Any of the above commands
+ have a single \railqtok{text} argument that refers to an ML
+ expression of appropriate type, which are as follows by default:
+
+%FIXME proper antiquotations
+\begin{ttbox}
+val parse_ast_translation : (string * (ast list -> ast)) list
+val parse_translation : (string * (term list -> term)) list
+val print_translation : (string * (term list -> term)) list
+val typed_print_translation :
+ (string * (bool -> typ -> term list -> term)) list
+val print_ast_translation : (string * (ast list -> ast)) list
+val token_translation :
+ (string * string * (string -> string * real)) list
+\end{ttbox}
+
+ If the \isa{{\isacharparenleft}advanced{\isacharparenright}} option is given, the corresponding
+ translation functions may depend on the current theory or proof
+ context. This allows to implement advanced syntax mechanisms, as
+ translations functions may refer to specific theory declarations or
+ auxiliary proof data.
+
+ See also \cite[\S8]{isabelle-ref} for more information on the
+ general concept of syntax transformations in Isabelle.
+
+%FIXME proper antiquotations
+\begin{ttbox}
+val parse_ast_translation:
+ (string * (Context.generic -> ast list -> ast)) list
+val parse_translation:
+ (string * (Context.generic -> term list -> term)) list
+val print_translation:
+ (string * (Context.generic -> term list -> term)) list
+val typed_print_translation:
+ (string * (Context.generic -> bool -> typ -> term list -> term)) list
+val print_ast_translation:
+ (string * (Context.generic -> ast list -> ast)) list
+\end{ttbox}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Oracles%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{oracle}\isa{\isacommand{oracle}} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some type
+ \verb|T| given by the user. This acts like an infinitary
+ specification of axioms -- there is no internal check of the
+ correctness of the results! The inference kernel records oracle
+ invocations within the internal derivation object of theorems, and
+ the pretty printer attaches ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' to indicate results
+ that are not fully checked by Isabelle inferences.
+
+ \begin{rail}
+ 'oracle' name '(' type ')' '=' text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{oracle}}~\isa{name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text}] turns the
+ given ML expression \isa{text} of type \verb|{theory|\isasep\isanewline%
+\verb| ->|~\isa{type}~\verb|-> term| into an ML function
+ \verb|name| of type \verb|{theory ->|~\isa{type}~\verb|-> thm|.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof commands%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Proof commands perform transitions of Isar/VM machine
+ configurations, which are block-structured, consisting of a stack of
+ nodes with three main components: logical proof context, current
+ facts, and open goals. Isar/VM transitions are \emph{typed}
+ according to the following three different modes of operation:
+
+ \begin{descr}
+
+ \item [\isa{proof{\isacharparenleft}prove{\isacharparenright}}] 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, and enter a sub-proof to establish the
+ actual result.
+
+ \item [\isa{proof{\isacharparenleft}state{\isacharparenright}}] is like a nested theory mode: the
+ context may be augmented by \emph{stating} additional assumptions,
+ intermediate results etc.
+
+ \item [\isa{proof{\isacharparenleft}chain{\isacharparenright}}] is intermediate between \isa{proof{\isacharparenleft}state{\isacharparenright}} and \isa{proof{\isacharparenleft}prove{\isacharparenright}}: existing facts (i.e.\
+ the contents of the special ``\indexref{}{fact}{this}\isa{this}'' register) have been
+ just picked up in order to be used when refining the goal claimed
+ next.
+
+ \end{descr}
+
+ The proof mode indicator may be read as a verb telling the writer
+ what kind of operation may be performed next. The corresponding
+ typings of proof commands restricts the shape of well-formed proof
+ texts to particular command sequences. So dynamic arrangements of
+ commands eventually turn out as static texts of a certain structure.
+ \Appref{ap:refcard} gives a simplified grammar of the overall
+ (extensible) language emerging that way.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Markup commands \label{sec:markup-prf}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{sect}\isa{\isacommand{sect}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{subsect}\isa{\isacommand{subsect}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{subsubsect}\isa{\isacommand{subsubsect}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{txt}\isa{\isacommand{txt}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{txt-raw}\isa{\isacommand{txt{\isacharunderscore}raw}} & : & \isartrans{proof}{proof} \\
+ \end{matharray}
+
+ These markup commands for proof mode closely correspond to the ones
+ of theory mode (see \S\ref{sec:markup-thy}).
+
+ \begin{rail}
+ ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+ ;
+ \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Context elements \label{sec:proof-context}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{fix}\isa{\isacommand{fix}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{assume}\isa{\isacommand{assume}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{presume}\isa{\isacommand{presume}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{def}\isa{\isacommand{def}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \end{matharray}
+
+ The logical proof context consists of fixed variables and
+ assumptions. The former closely correspond to Skolem constants, or
+ meta-level universal quantification as provided by the Isabelle/Pure
+ logical framework. Introducing some \emph{arbitrary, but fixed}
+ variable via ``\isa{\isacommand{fix}}~\isa{x} results in a local value
+ that may be used in the subsequent proof as any other variable or
+ constant. Furthermore, any result \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} exported from
+ the context will be universally closed wrt.\ \isa{x} at the
+ outermost level: \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} (this is expressed in normal
+ form using Isabelle's meta-variables).
+
+ Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
+ On the one hand, a local theorem is created that may be used as a
+ fact in subsequent proof steps. On the other hand, any result
+ \isa{{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}} exported from the context becomes conditional wrt.\
+ the assumption: \isa{{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}}. Thus, solving an enclosing goal
+ using such a result would basically introduce a new subgoal stemming
+ from the assumption. How this situation is handled depends on the
+ version of assumption command used: while \isa{\isacommand{assume}}
+ insists on solving the subgoal by unification with some premise of
+ the goal, \isa{\isacommand{presume}} leaves the subgoal unchanged in order
+ to be proved later by the user.
+
+ Local definitions, introduced by ``\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}'', are achieved by combining ``\isa{\isacommand{fix}}~\isa{x}'' with
+ another version of assumption that causes any hypothetical equation
+ \isa{x\ {\isasymequiv}\ t} to be eliminated by the reflexivity rule. Thus,
+ exporting some result \isa{x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} yields \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}}.
+
+ \railalias{equiv}{\isasymequiv}
+ \railterm{equiv}
+
+ \begin{rail}
+ 'fix' (vars + 'and')
+ ;
+ ('assume' | 'presume') (props + 'and')
+ ;
+ 'def' (def + 'and')
+ ;
+ def: thmdecl? \\ name ('==' | equiv) term termpat?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{fix}}~\isa{x}] introduces a local variable
+ \isa{x} that is \emph{arbitrary, but fixed.}
+
+ \item [\isa{\isacommand{assume}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \isa{\isacommand{presume}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduce a local fact \isa{{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}} by
+ assumption. Subsequent results applied to an enclosing goal (e.g.\
+ by \indexref{}{command}{show}\isa{\isacommand{show}}) are handled as follows: \isa{\isacommand{assume}} expects to be able to unify with existing premises in the
+ goal, while \isa{\isacommand{presume}} leaves \isa{{\isasymphi}} as new subgoals.
+
+ Several lists of assumptions may be given (separated by
+ \indexref{}{keyword}{and}\isa{\isakeyword{and}}; the resulting list of current facts consists
+ of all of these concatenated.
+
+ \item [\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}] introduces a local
+ (non-polymorphic) definition. In results exported from the context,
+ \isa{x} is replaced by \isa{t}. Basically, ``\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}'' abbreviates ``\isa{\isacommand{fix}}~\isa{x}~\isa{\isacommand{assume}}~\isa{x\ {\isasymequiv}\ t}'', with the resulting
+ hypothetical equation solved by reflexivity.
+
+ The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
+ Several simultaneous definitions may be given at the same time.
+
+ \end{descr}
+
+ The special name \indexref{}{fact}{prems}\isa{prems} refers to all assumptions of the
+ current context as a list of theorems. This feature should be used
+ with great care! It is better avoided in final proof texts.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Facts and forward chaining%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{note}\isa{\isacommand{note}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{then}\isa{\isacommand{then}} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \indexdef{}{command}{from}\isa{\isacommand{from}} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \indexdef{}{command}{with}\isa{\isacommand{with}} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \indexdef{}{command}{using}\isa{\isacommand{using}} & : & \isartrans{proof(prove)}{proof(prove)} \\
+ \indexdef{}{command}{unfolding}\isa{\isacommand{unfolding}} & : & \isartrans{proof(prove)}{proof(prove)} \\
+ \end{matharray}
+
+ New facts are established either by assumption or proof of local
+ statements. Any fact will usually be involved in further proofs,
+ either as explicit arguments of proof methods, or when forward
+ chaining towards the next goal via \isa{\isacommand{then}} (and variants);
+ \isa{\isacommand{from}} and \isa{\isacommand{with}} are composite forms
+ involving \isa{\isacommand{note}}. The \isa{\isacommand{using}} elements
+ augments the collection of used facts \emph{after} a goal has been
+ stated. Note that the special theorem name \indexref{}{fact}{this}\isa{this} refers
+ to the most recently established facts, but only \emph{before}
+ issuing a follow-up claim.
+
+ \begin{rail}
+ 'note' (thmdef? thmrefs + 'and')
+ ;
+ ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{note}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
+ recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n}, binding
+ the result as \isa{a}. Note that attributes may be involved as
+ well, both on the left and right hand sides.
+
+ \item [\isa{\isacommand{then}}] indicates forward chaining by the current
+ facts in order to establish the goal to be claimed next. The
+ initial proof method invoked to refine that will be offered the
+ facts to do ``anything appropriate'' (see also
+ \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\isa{rule}
+ (see \secref{sec:pure-meth-att}) would typically do an elimination
+ rather than an introduction. Automatic methods usually insert the
+ facts into the goal state before operation. This provides a simple
+ scheme to control relevance of facts in automated proof search.
+
+ \item [\isa{\isacommand{from}}~\isa{b}] abbreviates ``\isa{\isacommand{note}}~\isa{b}~\isa{\isacommand{then}}''; thus \isa{\isacommand{then}} is
+ equivalent to ``\isa{\isacommand{from}}~\isa{this}''.
+
+ \item [\isa{\isacommand{with}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
+ abbreviates ``\isa{\isacommand{from}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this}''; thus the forward chaining is from earlier facts together
+ with the current ones.
+
+ \item [\isa{\isacommand{using}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] augments
+ the facts being currently indicated for use by a subsequent
+ refinement step (such as \indexref{}{command}{apply}\isa{\isacommand{apply}} or \indexref{}{command}{proof}\isa{\isacommand{proof}}).
+
+ \item [\isa{\isacommand{unfolding}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] is
+ structurally similar to \isa{\isacommand{using}}, but unfolds definitional
+ equations \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n} throughout the goal state
+ and facts.
+
+ \end{descr}
+
+ Forward chaining with an empty list of theorems is the same as not
+ chaining at all. Thus ``\isa{\isacommand{from}}~\isa{nothing}'' has no
+ effect apart from entering \isa{prove{\isacharparenleft}chain{\isacharparenright}} mode, since
+ \indexref{}{fact}{nothing}\isa{nothing} is bound to the empty list of theorems.
+
+ Basic proof methods (such as \indexref{}{method}{rule}\isa{rule}) expect multiple
+ facts to be given in their proper order, corresponding to a prefix
+ of the premises of the rule involved. Note that positions may be
+ easily skipped using something like \isa{\isacommand{from}}~\isa{{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b}, for example. This involves the trivial rule
+ \isa{PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}}, which is bound in Isabelle/Pure as
+ ``\indexref{}{fact}{-}\isa{{\isacharunderscore}}'' (underscore).
+
+ Automated methods (such as \isa{simp} or \isa{auto}) just
+ insert any given facts before their usual operation. Depending on
+ the kind of procedure involved, the order of facts is less
+ significant here.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Goal statements \label{sec:goals}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ From a theory context, proof mode is entered by an initial goal
+ command such as \isa{\isacommand{lemma}}, \isa{\isacommand{theorem}}, or
+ \isa{\isacommand{corollary}}. Within a proof, new claims may be
+ introduced locally as well; four variants are available here to
+ indicate whether forward chaining of facts should be performed
+ initially (via \indexref{}{command}{then}\isa{\isacommand{then}}), and whether the final result
+ is meant to solve some pending goal.
+
+ Goals may consist of multiple statements, resulting in a list of
+ facts eventually. A pending multi-goal is internally represented as
+ a meta-level conjunction (printed as \isa{{\isacharampersand}{\isacharampersand}}), which is usually
+ split into the corresponding number of sub-goals prior to an initial
+ method application, via \indexref{}{command}{proof}\isa{\isacommand{proof}}
+ (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\isa{\isacommand{apply}}
+ (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\isa{induct} method
+ covered in \secref{sec:cases-induct} acts on multiple claims
+ simultaneously.
+
+ Claims at the theory level may be either in short or long form. A
+ short goal merely consists of several simultaneous propositions
+ (often just one). A long goal includes an explicit context
+ specification for the subsequent conclusion, involving local
+ parameters and assumptions. Here the role of each part of the
+ statement is explicitly marked by separate keywords (see also
+ \secref{sec:locale}); the local assumptions being introduced here
+ are available as \indexref{}{fact}{assms}\isa{assms} in the proof. Moreover, there
+ are two kinds of conclusions: \indexdef{}{element}{shows}\isa{shows} states several
+ simultaneous propositions (essentially a big conjunction), while
+ \indexdef{}{element}{obtains}\isa{obtains} claims several simultaneous simultaneous
+ contexts of (essentially a big disjunction of eliminated parameters
+ and assumptions, cf.\ \secref{sec:obtain}).
+
+ \begin{rail}
+ ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
+ ;
+ ('have' | 'show' | 'hence' | 'thus') goal
+ ;
+ 'print\_statement' modes? thmrefs
+ ;
+
+ goal: (props + 'and')
+ ;
+ longgoal: thmdecl? (contextelem *) conclusion
+ ;
+ conclusion: 'shows' goal | 'obtains' (parname? case + '|')
+ ;
+ case: (vars + 'and') 'where' (props + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{lemma}}~\isa{a{\isacharcolon}\ {\isasymphi}}] enters proof mode with
+ \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isasymturnstile}\ {\isasymphi}} to be put back into the target context. An additional
+ \railnonterm{context} specification may build up an initial proof
+ context for the subsequent claim; this includes local definitions
+ and syntax as well, see the definition of \isa{contextelem} in
+ \secref{sec:locale}.
+
+ \item [\isa{\isacommand{theorem}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \isa{\isacommand{corollary}}~\isa{a{\isacharcolon}\ {\isasymphi}}] are essentially the same as \isa{\isacommand{lemma}}~\isa{a{\isacharcolon}\ {\isasymphi}}, but the facts are internally marked as
+ being of a different kind. This discrimination acts like a formal
+ comment.
+
+ \item [\isa{\isacommand{have}}~\isa{a{\isacharcolon}\ {\isasymphi}}] claims a local goal,
+ eventually resulting in a fact within the current logical context.
+ This operation is completely independent of any pending sub-goals of
+ an enclosing goal statements, so \isa{\isacommand{have}} may be freely
+ used for experimental exploration of potential results within a
+ proof body.
+
+ \item [\isa{\isacommand{show}}~\isa{a{\isacharcolon}\ {\isasymphi}}] is like \isa{\isacommand{have}}~\isa{a{\isacharcolon}\ {\isasymphi}} plus a second stage to refine some pending
+ sub-goal for each one of the finished result, after having been
+ exported into the corresponding context (at the head of the
+ sub-proof of this \isa{\isacommand{show}} command).
+
+ To accommodate interactive debugging, resulting rules are printed
+ before being applied internally. Even more, interactive execution
+ of \isa{\isacommand{show}} predicts potential failure and displays the
+ resulting error as a warning beforehand. Watch out for the
+ following message:
+
+ %FIXME proper antiquitation
+ \begin{ttbox}
+ Problem! Local statement will fail to solve any pending goal
+ \end{ttbox}
+
+ \item [\isa{\isacommand{hence}}] abbreviates ``\isa{\isacommand{then}}~\isa{\isacommand{have}}'', i.e.\ claims a local goal to be proven by forward
+ chaining the current facts. Note that \isa{\isacommand{hence}} is also
+ equivalent to ``\isa{\isacommand{from}}~\isa{this}~\isa{\isacommand{have}}''.
+
+ \item [\isa{\isacommand{thus}}] abbreviates ``\isa{\isacommand{then}}~\isa{\isacommand{show}}''. Note that \isa{\isacommand{thus}} is also equivalent to
+ ``\isa{\isacommand{from}}~\isa{this}~\isa{\isacommand{show}}''.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}statement}}~\isa{a}] prints facts from the
+ current theory or proof context in long statement form, according to
+ the syntax for \isa{\isacommand{lemma}} given above.
+
+ \end{descr}
+
+ Any goal statement causes some term abbreviations (such as
+ \indexref{}{variable}{?thesis}\isa{{\isacharquery}thesis}) to be bound automatically, see also
+ \secref{sec:term-abbrev}. Furthermore, the local context of a
+ (non-atomic) goal is provided via the \indexref{}{case}{rule-context}\isa{rule{\isacharunderscore}context} case.
+
+ The optional case names of \indexref{}{element}{obtains}\isa{obtains} have a twofold
+ meaning: (1) during the of this claim they refer to the the local
+ context introductions, (2) the resulting rule is annotated
+ accordingly to support symbolic case splits when used with the
+ \indexref{}{method}{cases}\isa{cases} method (cf. \secref{sec:cases-induct}).
+
+ \medskip
+
+ \begin{warn}
+ Isabelle/Isar suffers theory-level goal statements to contain
+ \emph{unbound schematic variables}, although this does not conform
+ to the aim of human-readable proof documents! The main problem
+ with schematic goals is that the actual outcome is usually hard to
+ predict, depending on the behavior of the proof methods applied
+ during the course of reasoning. Note that most semi-automated
+ methods heavily depend on several kinds of implicit rule
+ declarations within the current theory context. As this would
+ also result in non-compositional checking of sub-proofs,
+ \emph{local goals} are not allowed to be schematic at all.
+ Nevertheless, schematic goals do have their use in Prolog-style
+ interactive synthesis of proven results, usually by stepwise
+ refinement via emulation of traditional Isabelle tactic scripts
+ (see also \secref{sec:tactic-commands}). In any case, users
+ should know what they are doing.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{proof}\isa{\isacommand{proof}} & : & \isartrans{proof(prove)}{proof(state)} \\
+ \indexdef{}{command}{qed}\isa{\isacommand{qed}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
+ \indexdef{}{command}{by}\isa{\isacommand{by}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \indexdef{}{command}{..}\isa{\isacommand{{\isachardot}{\isachardot}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \indexdef{}{command}{.}\isa{\isacommand{{\isachardot}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \indexdef{}{command}{sorry}\isa{\isacommand{sorry}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \end{matharray}
+
+ Arbitrary goal refinement via tactics is considered harmful.
+ Structured proof composition in Isar admits proof methods to be
+ invoked in two places only.
+
+ \begin{enumerate}
+
+ \item An \emph{initial} refinement step \indexref{}{command}{proof}\isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}} reduces a newly stated goal to a number
+ of sub-goals that are to be solved later. Facts are passed to
+ \isa{m\isactrlsub {\isadigit{1}}} for forward chaining, if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode.
+
+ \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\isa{\isacommand{qed}}~\isa{m\isactrlsub {\isadigit{2}}} is intended to solve remaining goals. No facts are
+ passed to \isa{m\isactrlsub {\isadigit{2}}}.
+
+ \end{enumerate}
+
+ The only other (proper) way to affect pending goals in a proof body
+ is by \indexref{}{command}{show}\isa{\isacommand{show}}, which involves an explicit statement of
+ what is to be solved eventually. Thus we avoid the fundamental
+ problem of unstructured tactic scripts that consist of numerous
+ consecutive goal transformations, with invisible effects.
+
+ \medskip As a general rule of thumb for good proof style, initial
+ proof methods should either solve the goal completely, or constitute
+ some well-understood 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
+ an intelligible manner.
+
+ Unless given explicitly by the user, the default initial method is
+ ``\indexref{}{method}{rule}\isa{rule}'', which applies a single standard elimination
+ or introduction rule according to the topmost symbol involved.
+ There is no separate default terminal method. Any remaining goals
+ are always solved by assumption in the very last step.
+
+ \begin{rail}
+ 'proof' method?
+ ;
+ 'qed' method?
+ ;
+ 'by' method method?
+ ;
+ ('.' | '..' | 'sorry')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}}] refines the goal by
+ proof method \isa{m\isactrlsub {\isadigit{1}}}; facts for forward chaining are
+ passed if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode.
+
+ \item [\isa{\isacommand{qed}}~\isa{m\isactrlsub {\isadigit{2}}}] refines any remaining
+ goals by proof method \isa{m\isactrlsub {\isadigit{2}}} and concludes the
+ sub-proof by assumption. If the goal had been \isa{show} (or
+ \isa{thus}), some pending sub-goal is solved as well by the rule
+ resulting from the result \emph{exported} into the enclosing goal
+ context. Thus \isa{qed} may fail for two reasons: either \isa{m\isactrlsub {\isadigit{2}}} fails, or the resulting rule does not fit to any
+ pending goal\footnote{This includes any additional ``strong''
+ assumptions as introduced by \isa{assume}.} of the enclosing
+ context. Debugging such a situation might involve temporarily
+ changing \isa{\isacommand{show}} into \isa{\isacommand{have}}, or weakening the
+ local context by replacing occurrences of \isa{\isacommand{assume}} by
+ \isa{\isacommand{presume}}.
+
+ \item [\isa{\isacommand{by}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}}] is a
+ \emph{terminal proof}\index{proof!terminal}; it abbreviates
+ \isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}}~\isa{qed}~\isa{m\isactrlsub {\isadigit{2}}}, but with backtracking across both methods. Debugging
+ an unsuccessful \isa{\isacommand{by}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}}
+ command can be done by expanding its definition; in many cases
+ \isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}} (or even \isa{apply}~\isa{m\isactrlsub {\isadigit{1}}}) is already sufficient to see the
+ problem.
+
+ \item [``\isa{\isacommand{{\isachardot}{\isachardot}}}''] is a \emph{default
+ proof}\index{proof!default}; it abbreviates \isa{\isacommand{by}}~\isa{rule}.
+
+ \item [``\isa{\isacommand{{\isachardot}}}''] is a \emph{trivial
+ proof}\index{proof!trivial}; it abbreviates \isa{\isacommand{by}}~\isa{this}.
+
+ \item [\isa{\isacommand{sorry}}] is a \emph{fake proof}\index{proof!fake}
+ pretending to solve the pending claim without further ado. This
+ only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
+ proofs are not the real thing. Internally, each theorem container
+ is tainted by an oracle invocation, which is indicated as ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' in the printed result.
+
+ The most important application of \isa{\isacommand{sorry}} is to support
+ experimentation and top-down proof development.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The following proof methods and attributes refer to basic logical
+ operations of Isar. Further methods and attributes are provided by
+ several generic and object-logic specific tools and packages (see
+ \chref{ch:gen-tools} and \chref{ch:logics}).
+
+ \begin{matharray}{rcl}
+ \indexdef{}{method}{-}\isa{{\isacharminus}} & : & \isarmeth \\
+ \indexdef{}{method}{fact}\isa{fact} & : & \isarmeth \\
+ \indexdef{}{method}{assumption}\isa{assumption} & : & \isarmeth \\
+ \indexdef{}{method}{this}\isa{this} & : & \isarmeth \\
+ \indexdef{}{method}{rule}\isa{rule} & : & \isarmeth \\
+ \indexdef{}{method}{iprover}\isa{iprover} & : & \isarmeth \\[0.5ex]
+ \indexdef{}{attribute}{intro}\isa{intro} & : & \isaratt \\
+ \indexdef{}{attribute}{elim}\isa{elim} & : & \isaratt \\
+ \indexdef{}{attribute}{dest}\isa{dest} & : & \isaratt \\
+ \indexdef{}{attribute}{rule}\isa{rule} & : & \isaratt \\[0.5ex]
+ \indexdef{}{attribute}{OF}\isa{OF} & : & \isaratt \\
+ \indexdef{}{attribute}{of}\isa{of} & : & \isaratt \\
+ \indexdef{}{attribute}{where}\isa{where} & : & \isaratt \\
+ \end{matharray}
+
+ \begin{rail}
+ 'fact' thmrefs?
+ ;
+ 'rule' thmrefs?
+ ;
+ 'iprover' ('!' ?) (rulemod *)
+ ;
+ rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
+ ;
+ ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
+ ;
+ 'rule' 'del'
+ ;
+ 'OF' thmrefs
+ ;
+ 'of' insts ('concl' ':' insts)?
+ ;
+ 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [``\isa{{\isacharminus}}''] does nothing but insert the forward
+ chaining facts as premises into the goal. Note that command
+ \indexref{}{command}{proof}\isa{\isacommand{proof}} without any method actually performs a single
+ reduction step using the \indexref{}{method}{rule}\isa{rule} method; thus a plain
+ \emph{do-nothing} proof step would be ``\isa{\isacommand{proof}}~\isa{{\isacharminus}}'' rather than \isa{\isacommand{proof}} alone.
+
+ \item [\isa{fact}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] composes
+ some fact from \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} (or implicitly from
+ the current proof context) modulo unification of schematic type and
+ term variables. The rule structure is not taken into account, i.e.\
+ meta-level implication is considered atomic. This is the same
+ principle underlying literal facts (cf.\ \secref{sec:syn-att}):
+ ``\isa{\isacommand{have}}~\isa{{\isasymphi}}~\isa{\isacommand{by}}~\isa{fact}'' is
+ equivalent to ``\isa{\isacommand{note}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isasymturnstile}\ {\isasymphi}} is an instance of some known
+ \isa{{\isasymturnstile}\ {\isasymphi}} in the proof context.
+
+ \item [\isa{assumption}] solves some goal by a single assumption
+ step. All given facts are guaranteed to participate in the
+ refinement; this means there may be only 0 or 1 in the first place.
+ Recall that \isa{\isacommand{qed}} (\secref{sec:proof-steps}) already
+ concludes any remaining sub-goals by assumption, so structured
+ proofs usually need not quote the \isa{assumption} method at
+ all.
+
+ \item [\isa{this}] applies all of the current facts directly as
+ rules. Recall that ``\isa{\isacommand{{\isachardot}}}'' (dot) abbreviates ``\isa{\isacommand{by}}~\isa{this}''.
+
+ \item [\isa{rule}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some
+ rule given as argument in backward manner; facts are used to reduce
+ the rule before applying it to the goal. Thus \isa{rule}
+ without facts is plain introduction, while with facts it becomes
+ elimination.
+
+ When no arguments are given, the \isa{rule} method tries to pick
+ appropriate rules automatically, as declared in the current context
+ using the \isa{intro}, \isa{elim}, \isa{dest}
+ attributes (see below). This is the default behavior of \isa{\isacommand{proof}} and ``\isa{\isacommand{{\isachardot}{\isachardot}}}'' (double-dot) steps (see
+ \secref{sec:proof-steps}).
+
+ \item [\isa{iprover}] performs intuitionistic proof search,
+ depending on specifically declared rules from the context, or given
+ as explicit arguments. Chained facts are inserted into the goal
+ before commencing proof search; ``\isa{iprover}\isa{{\isacharbang}}''
+ means to include the current \isa{prems} as well.
+
+ Rules need to be classified as \isa{intro}, \isa{elim}, or \isa{dest}; here the ``\isa{{\isacharbang}} indicator refers
+ to ``safe'' rules, which may be applied aggressively (without
+ considering back-tracking later). Rules declared with ``\isa{{\isacharquery}}'' are ignored in proof search (the single-step \isa{rule}
+ method still observes these). An explicit weight annotation may be
+ given as well; otherwise the number of rule premises will be taken
+ into account here.
+
+ \item [\isa{intro}, \isa{elim}, and \isa{dest}]
+ declare introduction, elimination, and destruct rules, to be used
+ with the \isa{rule} and \isa{iprover} methods. Note that
+ the latter will ignore rules declared with ``\isa{{\isacharquery}}'', while
+ ``\isa{{\isacharbang}}'' are used most aggressively.
+
+ The classical reasoner (see \secref{sec:classical}) introduces its
+ own variants of these attributes; use qualified names to access the
+ present versions of Isabelle/Pure, i.e.\ \isa{Pure{\isachardot}intro}.
+
+ \item [\isa{rule}~\isa{del}] undeclares introduction,
+ elimination, or destruct rules.
+
+ \item [\isa{OF}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some
+ theorem to all of the given rules \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n}
+ (in parallel). This corresponds to the \verb|op MRS| operation in
+ ML, but note the reversed order. Positions may be effectively
+ skipped by including ``\verb|_|'' (underscore) as argument.
+
+ \item [\isa{of}~\isa{t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}] performs
+ positional instantiation of term variables. The terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n} are substituted for any schematic
+ variables occurring in a theorem from left to right; ``\verb|_|'' (underscore) indicates to skip a position. Arguments following
+ a ``\isa{\isakeyword{concl}}\isa{{\isacharcolon}}'' specification refer to positions
+ of the conclusion of a rule.
+
+ \item [\isa{where}~\isa{x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] performs named instantiation of
+ schematic type and term variables occurring in a theorem. Schematic
+ variables have to be specified on the left-hand side (e.g.\ \isa{{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}}). The question mark may be omitted if the variable name is
+ a plain identifier without index. As type instantiations are
+ inferred from term instantiations, explicit type instantiations are
+ seldom necessary.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{let}\isa{\isacommand{let}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{keyword}{is}\isa{\isakeyword{is}} & : & syntax \\
+ \end{matharray}
+
+ Abbreviations may be either bound by explicit \isa{\isacommand{let}}\isa{p\ {\isasymequiv}\ t} statements, or by annotating assumptions or goal statements
+ with a list of patterns ``\isa{{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n}''.
+ In both cases, higher-order matching is invoked to bind
+ extra-logical term variables, which may be either named schematic
+ variables of the form \isa{{\isacharquery}x}, or nameless dummies ``\isa{{\isacharunderscore}}'' (underscore). Note that in the \isa{\isacommand{let}} form the
+ patterns occur on the left-hand side, while the \isa{\isakeyword{is}}
+ patterns are in postfix position.
+
+ Polymorphism of term bindings is handled in Hindley-Milner style,
+ similar to ML. Type variables referring to local assumptions or
+ open goal statements are \emph{fixed}, while those of finished
+ results or bound by \isa{\isacommand{let}} may occur in \emph{arbitrary}
+ instances later. Even though actual polymorphism should be rarely
+ used in practice, this mechanism is essential to achieve proper
+ incremental type-inference, as the user proceeds to build up the
+ Isar proof text from left to right.
+
+ \medskip Term abbreviations are quite different from local
+ definitions as introduced via \isa{\isacommand{def}} (see
+ \secref{sec:proof-context}). The latter are visible within the
+ logic as actual equations, while abbreviations disappear during the
+ input process just after type checking. Also note that \isa{\isacommand{def}} does not support polymorphism.
+
+ \begin{rail}
+ 'let' ((term + 'and') '=' term + 'and')
+ ;
+ \end{rail}
+
+ The syntax of \isa{\isakeyword{is}} patterns follows \railnonterm{termpat}
+ or \railnonterm{proppat} (see \secref{sec:term-decls}).
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{let}}~\isa{p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] binds any text variables in patterns
+ \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} by simultaneous higher-order
+ matching against terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n}.
+
+ \item [\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}] resembles \isa{\isacommand{let}}, but matches \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} against the
+ preceding statement. Also note that \isa{\isakeyword{is}} is not a
+ separate command, but part of others (such as \isa{\isacommand{assume}},
+ \isa{\isacommand{have}} etc.).
+
+ \end{descr}
+
+ Some \emph{implicit} term abbreviations\index{term abbreviations}
+ for goals and facts are available as well. For any open goal,
+ \indexref{}{variable}{thesis}\isa{thesis} refers to its object-level statement,
+ abstracted over any meta-level parameters (if present). Likewise,
+ \indexref{}{variable}{this}\isa{this} is bound for fact statements resulting from
+ assumptions or finished goals. In case \isa{this} refers to
+ an object-logic statement that is an application \isa{f\ t}, then
+ \isa{t} is bound to the special text variable ``\isa{{\isasymdots}}''
+ (three dots). The canonical application of this convenience are
+ calculational proofs (see \secref{sec:calculation}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Block structure%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{next}\isa{\isacommand{next}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{\{}\isa{\isacommand{{\isacharbraceleft}}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{\}}\isa{\isacommand{{\isacharbraceright}}} & : & \isartrans{proof(state)}{proof(state)} \\
+ \end{matharray}
+
+ 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} internal blocks, which are closed again when concluding
+ the sub-proof (by \isa{\isacommand{qed}} etc.). Sections of different
+ context within a sub-proof may be switched via \isa{\isacommand{next}},
+ which is just a single block-close followed by block-open again.
+ The effect of \isa{\isacommand{next}} is to reset the local proof context;
+ there is no goal focus involved here!
+
+ For slightly more advanced applications, there are explicit block
+ parentheses as well. These typically achieve a stronger forward
+ style of reasoning.
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{next}}] switches to a fresh block within a
+ sub-proof, resetting the local context to the initial one.
+
+ \item [\isa{\isacommand{{\isacharbraceleft}}} and \isa{\isacommand{{\isacharbraceright}}}] explicitly open and close
+ blocks. Any current facts pass through ``\isa{\isacommand{{\isacharbraceleft}}}''
+ unchanged, while ``\isa{\isacommand{{\isacharbraceright}}}'' causes any result to be
+ \emph{exported} into the enclosing context. Thus fixed variables
+ are generalized, assumptions discharged, and local definitions
+ unfolded (cf.\ \secref{sec:proof-context}). There is no difference
+ of \isa{\isacommand{assume}} and \isa{\isacommand{presume}} in this mode of
+ forward reasoning --- in contrast to plain backward reasoning with
+ the result exported at \isa{\isacommand{show}} time.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isar provides separate commands to accommodate tactic-style
+ proof scripts within the same system. While being outside the
+ orthodox Isar proof language, these might come in handy for
+ interactive exploration and debugging, or even actual tactical proof
+ within new-style theories (to benefit from document preparation, for
+ example). See also \secref{sec:tactics} for actual tactics, that
+ have been encapsulated as proof methods. Proper proof methods may
+ be used in scripts, too.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{apply}\isa{\isacommand{apply}}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
+ \indexdef{}{command}{apply-end}\isa{\isacommand{apply{\isacharunderscore}end}}^* & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{done}\isa{\isacommand{done}}^* & : & \isartrans{proof(prove)}{proof(state)} \\
+ \indexdef{}{command}{defer}\isa{\isacommand{defer}}^* & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{prefer}\isa{\isacommand{prefer}}^* & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{back}\isa{\isacommand{back}}^* & : & \isartrans{proof}{proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ ( 'apply' | 'apply\_end' ) method
+ ;
+ 'defer' nat?
+ ;
+ 'prefer' nat
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{apply}}~\isa{m}] applies proof method \isa{m}
+ in initial position, but unlike \isa{\isacommand{proof}} it retains
+ ``\isa{proof{\isacharparenleft}prove{\isacharparenright}}'' mode. Thus consecutive method
+ applications may be given just as in tactic scripts.
+
+ Facts are passed to \isa{m} as indicated by the goal's
+ forward-chain mode, and are \emph{consumed} afterwards. Thus any
+ further \isa{\isacommand{apply}} command would always work in a purely
+ backward manner.
+
+ \item [\isa{\isacommand{apply{\isacharunderscore}end}}~\isa{m}] applies proof method
+ \isa{m} as if in terminal position. Basically, this simulates a
+ multi-step tactic script for \isa{\isacommand{qed}}, but may be given
+ anywhere within the proof body.
+
+ No facts are passed to \isa{m} here. Furthermore, the static
+ context is that of the enclosing goal (as for actual \isa{\isacommand{qed}}). Thus the proof method may not refer to any assumptions
+ introduced in the current body, for example.
+
+ \item [\isa{\isacommand{done}}] completes a proof script, provided that
+ the current goal state is solved completely. Note that actual
+ structured proof commands (e.g.\ ``\isa{\isacommand{{\isachardot}}}'' or \isa{\isacommand{sorry}}) may be used to conclude proof scripts as well.
+
+ \item [\isa{\isacommand{defer}}~\isa{n} and \isa{\isacommand{prefer}}~\isa{n}] shuffle the list of pending goals: \isa{\isacommand{defer}} puts off
+ sub-goal \isa{n} to the end of the list (\isa{n\ {\isacharequal}\ {\isadigit{1}}} by
+ default), while \isa{\isacommand{prefer}} brings sub-goal \isa{n} to the
+ front.
+
+ \item [\isa{\isacommand{back}}] does back-tracking over the result
+ sequence of the latest proof command. Basically, any proof command
+ may return multiple results.
+
+ \end{descr}
+
+ Any proper Isar proof method may be used with tactic script commands
+ such as \isa{\isacommand{apply}}. A few additional emulations of actual
+ tactics are provided as well; these would be never used in actual
+ structured proofs, of course.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Meta-linguistic features%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{oops}\isa{\isacommand{oops}} & : & \isartrans{proof}{theory} \\
+ \end{matharray}
+
+ The \isa{\isacommand{oops}} command discontinues the current proof
+ attempt, while considering the partial proof text as properly
+ processed. This is conceptually quite different from ``faking''
+ actual proofs via \indexref{}{command}{sorry}\isa{\isacommand{sorry}} (see
+ \secref{sec:proof-steps}): \isa{\isacommand{oops}} does not observe the
+ proof structure at all, but goes back right to the theory level.
+ Furthermore, \isa{\isacommand{oops}} does not produce any result theorem
+ --- there is no intended claim to be able to complete the proof
+ anyhow.
+
+ A typical application of \isa{\isacommand{oops}} is to explain Isar proofs
+ \emph{within} the system itself, in conjunction with the document
+ preparation tools of Isabelle described in \cite{isabelle-sys}.
+ Thus partial or even wrong proof attempts can be discussed in a
+ logically sound manner. Note that the Isabelle {\LaTeX} macros can
+ be easily adapted to print something like ``\isa{{\isasymdots}}'' instead of
+ the keyword ``\isa{\isacommand{oops}}''.
+
+ \medskip The \isa{\isacommand{oops}} command is undo-able, unlike
+ \indexref{}{command}{kill}\isa{\isacommand{kill}} (see \secref{sec:history}). The effect is to
+ get back to the theory just before the opening of the proof.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Other commands%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Diagnostics%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
+ \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ These diagnostic commands assist interactive development. Note that
+ \isa{\isacommand{undo}} does not apply here, the theory or proof
+ configuration is not changed.
+
+ \begin{rail}
+ 'pr' modes? nat? (',' nat)?
+ ;
+ 'thm' modes? thmrefs
+ ;
+ 'term' modes? term
+ ;
+ 'prop' modes? prop
+ ;
+ 'typ' modes? type
+ ;
+ 'prf' modes? thmrefs?
+ ;
+ 'full\_prf' modes? thmrefs?
+ ;
+
+ modes: '(' (name + ) ')'
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{pr}}~\isa{goals{\isacharcomma}\ prems}] prints the current
+ proof state (if present), including the proof context, current facts
+ and goals. The optional limit arguments affect the number of goals
+ and premises to be displayed, which is initially 10 for both.
+ Omitting limit values leaves the current setting unchanged.
+
+ \item [\isa{\isacommand{thm}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] retrieves
+ theorems from the current theory or proof context. Note that any
+ attributes included in the theorem specifications are applied to a
+ temporary context derived from the current theory or proof; the
+ result is discarded, i.e.\ attributes involved in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} do not have any permanent effect.
+
+ \item [\isa{\isacommand{term}}~\isa{t} and \isa{\isacommand{prop}}~\isa{{\isasymphi}}]
+ read, type-check and print terms or propositions according to the
+ current theory or proof context; the inferred type of \isa{t} is
+ output as well. Note that these commands are also useful in
+ inspecting the current environment of term abbreviations.
+
+ \item [\isa{\isacommand{typ}}~\isa{{\isasymtau}}] reads and prints types of the
+ meta-logic according to the current theory or proof context.
+
+ \item [\isa{\isacommand{prf}}] displays the (compact) proof term of the
+ current proof state (if present), or of the given theorems. Note
+ that this requires proof terms to be switched on for the current
+ object logic (see the ``Proof terms'' section of the Isabelle
+ reference manual for information on how to do this).
+
+ \item [\isa{\isacommand{full{\isacharunderscore}prf}}] is like \isa{\isacommand{prf}}, but displays
+ the full proof term, i.e.\ also displays information omitted in the
+ compact proof term, which is denoted by ``\verb|_|''
+ placeholders there.
+
+ \end{descr}
+
+ All of the diagnostic commands above admit a list of \isa{modes}
+ to be specified, which is appended to the current print mode (see
+ also \cite{isabelle-ref}). Thus the output behavior may be modified
+ according particular print mode features. For example, \isa{\isacommand{pr}}~\isa{{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}} would print the current
+ proof state with mathematical symbols and special characters
+ represented in {\LaTeX} source, according to the Isabelle style
+ \cite{isabelle-sys}.
+
+ Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
+ systematic way to include formal items into the printed text
+ document.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Inspecting the context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{print-commands}\isa{\isacommand{print{\isacharunderscore}commands}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{print-theory}\isa{\isacommand{print{\isacharunderscore}theory}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print-syntax}\isa{\isacommand{print{\isacharunderscore}syntax}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print-methods}\isa{\isacommand{print{\isacharunderscore}methods}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print-attributes}\isa{\isacommand{print{\isacharunderscore}attributes}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print-theorems}\isa{\isacommand{print{\isacharunderscore}theorems}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{find-theorems}\isa{\isacommand{find{\isacharunderscore}theorems}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{thms-deps}\isa{\isacommand{thms{\isacharunderscore}deps}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print-facts}\isa{\isacommand{print{\isacharunderscore}facts}}^* & : & \isarkeep{proof} \\
+ \indexdef{}{command}{print-binds}\isa{\isacommand{print{\isacharunderscore}binds}}^* & : & \isarkeep{proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'print\_theory' ( '!'?)
+ ;
+
+ 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+ ;
+ criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+ 'simp' ':' term | term)
+ ;
+ 'thm\_deps' thmrefs
+ ;
+ \end{rail}
+
+ These commands print certain parts of the theory and proof context.
+ Note that there are some further ones available, such as for the set
+ of rules declared for simplifications.
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{print{\isacharunderscore}commands}}] prints Isabelle's outer theory
+ syntax, including keywords and command.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}theory}}] prints the main logical content of
+ the theory context; the ``\isa{{\isacharbang}}'' option indicates extra
+ verbosity.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}syntax}}] prints the inner syntax of types
+ and terms, depending on the current context. The output can be very
+ verbose, including grammar tables and syntax translation rules. See
+ \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
+ inner syntax.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}methods}}] prints all proof methods
+ available in the current theory context.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}attributes}}] prints all attributes
+ available in the current theory context.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}theorems}}] prints theorems resulting from
+ the last command.
+
+ \item [\isa{\isacommand{find{\isacharunderscore}theorems}}~\isa{criteria}] retrieves facts
+ from the theory or proof context matching all of given search
+ criteria. The criterion \isa{name{\isacharcolon}\ p} selects all theorems
+ whose fully qualified name matches pattern \isa{p}, which may
+ contain ``\isa{{\isacharasterisk}}'' wildcards. The criteria \isa{intro},
+ \isa{elim}, and \isa{dest} select theorems that match the
+ current goal as introduction, elimination or destruction rules,
+ respectively. The criterion \isa{simp{\isacharcolon}\ t} selects all rewrite
+ rules whose left-hand side matches the given term. The criterion
+ term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
+ ``\verb|_|'', schematic variables, and type constraints.
+
+ Criteria can be preceded by ``\isa{{\isacharminus}}'' to select theorems that
+ do \emph{not} match. Note that giving the empty list of criteria
+ yields \emph{all} currently known facts. An optional limit for the
+ number of printed facts may be given; the default is 40. By
+ default, duplicates are removed from the search result. Use
+ \isa{\isakeyword{with{\isacharunderscore}dups}} to display duplicates.
+
+ \item [\isa{\isacommand{thm{\isacharunderscore}deps}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}]
+ visualizes dependencies of facts, using Isabelle's graph browser
+ tool (see also \cite{isabelle-sys}).
+
+ \item [\isa{\isacommand{print{\isacharunderscore}facts}}] prints all local facts of the
+ current context, both named and unnamed ones.
+
+ \item [\isa{\isacommand{print{\isacharunderscore}binds}}] prints all term abbreviations
+ present in the context.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{History commands \label{sec:history}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{undo}\isa{\isacommand{undo}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{redo}\isa{\isacommand{redo}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{kill}\isa{\isacommand{kill}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ The Isabelle/Isar top-level maintains a two-stage history, for
+ theory and proof state transformation. Basically, any command can
+ be undone using \isa{\isacommand{undo}}, excluding mere diagnostic
+ elements. Its effect may be revoked via \isa{\isacommand{redo}}, unless
+ the corresponding \isa{\isacommand{undo}} step has crossed the beginning
+ of a proof or theory. The \isa{\isacommand{kill}} command aborts the
+ current history node altogether, discontinuing a proof or even the
+ whole theory. This operation is \emph{not} undo-able.
+
+ \begin{warn}
+ History commands should never be used with user interfaces such as
+ Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
+ care of stepping forth and back itself. Interfering by manual
+ \isa{\isacommand{undo}}, \isa{\isacommand{redo}}, or even \isa{\isacommand{kill}}
+ commands would quickly result in utter confusion.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{System operations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{cd}\isa{\isacommand{cd}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{pwd}\isa{\isacommand{pwd}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{use-thy}\isa{\isacommand{use{\isacharunderscore}thy}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{display-drafts}\isa{\isacommand{display{\isacharunderscore}drafts}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{print-drafts}\isa{\isacommand{print{\isacharunderscore}drafts}}^* & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('cd' | 'use\_thy' | 'update\_thy') name
+ ;
+ ('display\_drafts' | 'print\_drafts') (name +)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\isa{\isacommand{cd}}~\isa{path}] changes the current directory
+ of the Isabelle process.
+
+ \item [\isa{\isacommand{pwd}}] prints the current working directory.
+
+ \item [\isa{\isacommand{use{\isacharunderscore}thy}}~\isa{A}] preload theory \isa{A}.
+ These system commands are scarcely used when working interactively,
+ since loading of theories is done automatically as required.
+
+ \item [\isa{\isacommand{display{\isacharunderscore}drafts}}~\isa{paths} and \isa{\isacommand{print{\isacharunderscore}drafts}}~\isa{paths}] perform simple output of a given list
+ of raw source files. Only those symbols that do not require
+ additional {\LaTeX} packages are displayed properly, everything else
+ is left verbatim.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/Thy/document/session.tex Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/session.tex Fri May 02 16:36:05 2008 +0200
@@ -2,6 +2,8 @@
\input{syntax.tex}
+\input{pure.tex}
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 16:36:05 2008 +0200
@@ -4,6 +4,7 @@
%
\isadelimtheory
\isanewline
+\isanewline
%
\endisadelimtheory
%
--- a/doc-src/IsarRef/Thy/intro.thy Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/intro.thy Fri May 02 16:36:05 2008 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
theory intro
imports CPure
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/pure.thy Fri May 02 16:36:05 2008 +0200
@@ -0,0 +1,1792 @@
+(* $Id$ *)
+
+theory pure
+imports CPure
+begin
+
+chapter {* Basic language elements \label{ch:pure-syntax} *}
+
+text {*
+ Subsequently, we introduce the main part of Pure theory and proof
+ commands, together with fundamental proof methods and attributes.
+ \Chref{ch:gen-tools} describes further Isar elements provided by
+ generic tools and packages (such as the Simplifier) that are either
+ part of Pure Isabelle or pre-installed in most object logics.
+ \Chref{ch:logics} refers to object-logic specific elements (mainly
+ for HOL and ZF).
+
+ \medskip Isar commands may be either \emph{proper} document
+ constructors, or \emph{improper commands}. Some proof methods and
+ attributes introduced later are classified as improper as well.
+ Improper Isar language elements, which are subsequently marked by
+ ``@{text "\<^sup>*"}'', are often helpful when developing proof
+ documents, while their use is discouraged for the final
+ human-readable outcome. Typical examples are diagnostic commands
+ that print terms or theorems according to the current context; other
+ commands emulate old-style tactical theorem proving.
+*}
+
+
+section {* Theory commands *}
+
+subsection {* Defining theories \label{sec:begin-thy} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "header"} & : & \isarkeep{toplevel} \\
+ @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
+ @{command_def "end"} & : & \isartrans{theory}{toplevel} \\
+ \end{matharray}
+
+ Isabelle/Isar theories are defined via theory, which contain both
+ specifications and proofs; occasionally definitional mechanisms also
+ require some explicit proof.
+
+ The first ``real'' command of any theory has to be @{command
+ "theory"}, which starts a new theory based on the merge of existing
+ ones. Just preceding the @{command "theory"} keyword, there may be
+ an optional @{command "header"} declaration, which is relevant to
+ document preparation only; it acts very much like a special
+ pre-theory markup command (cf.\ \secref{sec:markup-thy} and
+ \secref{sec:markup-thy}). The @{command "end"} command concludes a
+ theory development; it has to be the very last command of any theory
+ file loaded in batch-mode.
+
+ \begin{rail}
+ 'header' text
+ ;
+ 'theory' name 'imports' (name +) uses? 'begin'
+ ;
+
+ uses: 'uses' ((name | parname) +);
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "header"}~@{text "text"}] provides plain text
+ markup just preceding the formal beginning of a theory. In actual
+ document preparation the corresponding {\LaTeX} macro @{verbatim
+ "\\isamarkupheader"} may be redefined to produce chapter or section
+ headings. See also \secref{sec:markup-thy} and
+ \secref{sec:markup-prf} for further markup commands.
+
+ \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
+ B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
+ merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
+
+ Due to inclusion of several ancestors, the overall theory structure
+ emerging in an Isabelle session forms a directed acyclic graph
+ (DAG). Isabelle's theory loader ensures that the sources
+ contributing to the development graph are always up-to-date.
+ Changed files are automatically reloaded when processing theory
+ headers.
+
+ The optional @{keyword_def "uses"} specification declares additional
+ dependencies on extra files (usually ML sources). Files will be
+ loaded immediately (as ML), unless the name is put in parentheses,
+ which merely documents the dependency to be resolved later in the
+ text (typically via explicit @{command_ref "use"} in the body text,
+ see \secref{sec:ML}).
+
+ \item [@{command "end"}] concludes the current theory definition or
+ context switch.
+
+ \end{descr}
+*}
+
+
+subsection {* Markup commands \label{sec:markup-thy} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ Apart from formal comments (see \secref{sec:comments}), markup
+ commands provide a structured way to insert text into the document
+ generated from a theory (see \cite{isabelle-sys} for more
+ information on Isabelle's document preparation tools).
+
+ \begin{rail}
+ ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
+ ;
+ 'text\_raw' text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "chapter"}, @{command "section"}, @{command
+ "subsection"}, and @{command "subsubsection"}] mark chapter and
+ section headings.
+
+ \item [@{command "text"}] specifies paragraphs of plain text.
+
+ \item [@{command "text_raw"}] inserts {\LaTeX} source into the
+ output, without additional markup. Thus the full range of document
+ manipulations becomes available.
+
+ \end{descr}
+
+ The @{text "text"} argument of these markup commands (except for
+ @{command "text_raw"}) may contain references to formal entities
+ (``antiquotations'', see also \secref{sec:antiq}). These are
+ interpreted in the present theory context, or the named @{text
+ "target"}.
+
+ Any of these markup elements corresponds to a {\LaTeX} command with
+ the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning
+ commands this is a plain macro with a single argument, e.g.\
+ @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
+ @{command "chapter"}. The @{command "text"} markup results in a
+ {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text
+ "\<dots>"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
+ causes the text to be inserted directly into the {\LaTeX} source.
+
+ \medskip Additional markup commands are available for proofs (see
+ \secref{sec:markup-prf}). Also note that the @{command_ref
+ "header"} declaration (see \secref{sec:begin-thy}) admits to insert
+ section markup just preceding the actual theory definition.
+*}
+
+
+subsection {* Type classes and sorts \label{sec:classes} *}
+
+text {*
+ \begin{matharray}{rcll}
+ @{command_def "classes"} & : & \isartrans{theory}{theory} \\
+ @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
+ @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'classes' (classdecl +)
+ ;
+ 'classrel' (nameref ('<' | subseteq) nameref + 'and')
+ ;
+ 'defaultsort' sort
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
+ declares class @{text c} to be a subclass of existing classes @{text
+ "c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
+
+ \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
+ subclass relations between existing classes @{text "c\<^sub>1"} and
+ @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
+ "instance"} command (see \secref{sec:axclass}) provides a way to
+ introduce proven class relations.
+
+ \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
+ new default sort for any type variables given without sort
+ constraints. Usually, the default sort would be only changed when
+ defining a new object-logic.
+
+ \item [@{command "class_deps"}] visualizes the subclass relation,
+ using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
+
+ \end{descr}
+*}
+
+
+subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}
+
+text {*
+ \begin{matharray}{rcll}
+ @{command_def "types"} & : & \isartrans{theory}{theory} \\
+ @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
+ @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
+ @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ \end{matharray}
+
+ \begin{rail}
+ 'types' (typespec '=' type infix? +)
+ ;
+ 'typedecl' typespec infix?
+ ;
+ 'nonterminals' (name +)
+ ;
+ 'arities' (nameref '::' arity +)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
+ introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
+ for existing type @{text "\<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.
+
+ \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
+ declares a new type constructor @{text t}, intended as an actual
+ logical type (of the object-logic, if available).
+
+ \item [@{command "nonterminals"}~@{text c}] declares type
+ constructors @{text c} (without arguments) to act as purely
+ syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
+ syntax of terms or types.
+
+ \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
+ s"}] augments Isabelle's order-sorted signature of types by new type
+ constructor arities. This is done axiomatically! The @{command_ref
+ "instance"} command (see \S\ref{sec:axclass}) provides a way to
+ introduce proven type arities.
+
+ \end{descr}
+*}
+
+
+subsection {* Primitive constants and definitions \label{sec:consts} *}
+
+text {*
+ Definitions essentially express abbreviations within the logic. The
+ simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
+ c} is a newly declared constant. Isabelle also allows derived forms
+ where the arguments of @{text c} appear on the left, abbreviating a
+ prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
+ written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
+ definitions may be weakened by adding arbitrary pre-conditions:
+ @{text "A \<Longrightarrow> c x y \<equiv> t"}.
+
+ \medskip The built-in well-formedness conditions for definitional
+ specifications are:
+
+ \begin{itemize}
+
+ \item Arguments (on the left-hand side) must be distinct variables.
+
+ \item All variables on the right-hand side must also appear on the
+ left-hand side.
+
+ \item All type variables on the right-hand side must also appear on
+ the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
+ \<alpha> list)"} for example.
+
+ \item The definition must not be recursive. Most object-logics
+ provide definitional principles that can be used to express
+ recursion safely.
+
+ \end{itemize}
+
+ Overloading means that a constant being declared as @{text "c :: \<alpha>
+ decl"} may be defined separately on type instances @{text "c ::
+ (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
+ t}. The right-hand side may mention overloaded constants
+ recursively at type instances corresponding to the immediate
+ argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
+ specification patterns impose global constraints on all occurrences,
+ e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
+ corresponding occurrences on some right-hand side need to be an
+ instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
+
+ \begin{matharray}{rcl}
+ @{command_def "consts"} & : & \isartrans{theory}{theory} \\
+ @{command_def "defs"} & : & \isartrans{theory}{theory} \\
+ @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'consts' ((name '::' type mixfix?) +)
+ ;
+ 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
+ ;
+ \end{rail}
+
+ \begin{rail}
+ 'constdefs' structs? (constdecl? constdef +)
+ ;
+
+ structs: '(' 'structure' (vars + 'and') ')'
+ ;
+ constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
+ ;
+ constdef: thmdecl? prop
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
+ @{text c} to have any instance of type scheme @{text \<sigma>}. The
+ optional mixfix annotations may attach concrete syntax to the
+ constants declared.
+
+ \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
+ as a definitional axiom for some existing constant.
+
+ The @{text "(unchecked)"} option disables global dependency checks
+ for this definition, which is occasionally useful for exotic
+ overloading. It is at the discretion of the user to avoid malformed
+ theory specifications!
+
+ The @{text "(overloaded)"} option declares definitions to be
+ potentially overloaded. Unless this option is given, a warning
+ message would be issued for any definitional equation with a more
+ special type than that of the corresponding constant declaration.
+
+ \item [@{command "constdefs"}] provides a streamlined combination of
+ constants declarations and definitions: type-inference takes care of
+ the most general typing of the given specification (the optional
+ type constraint may refer to type-inference dummies ``@{verbatim
+ _}'' as usual). The resulting type declaration needs to agree with
+ that of the specification; overloading is \emph{not} supported here!
+
+ The constant name may be omitted altogether, if neither type nor
+ syntax declarations are given. The canonical name of the
+ definitional axiom for constant @{text c} will be @{text c_def},
+ unless specified otherwise. Also note that the given list of
+ specifications is processed in a strictly sequential manner, with
+ type-checking being performed independently.
+
+ An optional initial context of @{text "(structure)"} declarations
+ admits use of indexed syntax, using the special symbol @{verbatim
+ "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
+ particularly useful with locales (see also \S\ref{sec:locale}).
+
+ \end{descr}
+*}
+
+
+subsection {* Syntax and translations \label{sec:syn-trans} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
+ @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
+ @{command_def "translations"} & : & \isartrans{theory}{theory} \\
+ @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \railalias{rightleftharpoons}{\isasymrightleftharpoons}
+ \railterm{rightleftharpoons}
+
+ \railalias{rightharpoonup}{\isasymrightharpoonup}
+ \railterm{rightharpoonup}
+
+ \railalias{leftharpoondown}{\isasymleftharpoondown}
+ \railterm{leftharpoondown}
+
+ \begin{rail}
+ ('syntax' | 'no\_syntax') mode? (constdecl +)
+ ;
+ ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+ ;
+
+ mode: ('(' ( name | 'output' | name 'output' ) ')')
+ ;
+ transpat: ('(' nameref ')')? string
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
+ @{command "consts"}~@{text decls}, except that the actual logical
+ signature extension is omitted. Thus the context free grammar of
+ Isabelle's inner syntax may be augmented in arbitrary ways,
+ independently of the logic. The @{text mode} argument refers to the
+ print mode that the grammar rules belong; unless the @{keyword_ref
+ "output"} indicator is given, all productions are added both to the
+ input and output grammar.
+
+ \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
+ grammar declarations (and translations) resulting from @{text
+ decls}, which are interpreted in the same manner as for @{command
+ "syntax"} above.
+
+ \item [@{command "translations"}~@{text rules}] specifies syntactic
+ translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
+ parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
+ Translation patterns may be prefixed by the syntactic category to be
+ used for parsing; the default is @{text logic}.
+
+ \item [@{command "no_translations"}~@{text rules}] removes syntactic
+ translation rules, which are interpreted in the same manner as for
+ @{command "translations"} above.
+
+ \end{descr}
+*}
+
+
+subsection {* Axioms and theorems \label{sec:axms-thms} *}
+
+text {*
+ \begin{matharray}{rcll}
+ @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
+ @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
+ @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'axioms' (axmdecl prop +)
+ ;
+ ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
+ statements as axioms of the meta-logic. In fact, axioms are
+ ``axiomatic theorems'', and may be referred later just as any other
+ theorem.
+
+ Axioms are usually only introduced when declaring new logical
+ systems. Everyday work is typically done the hard way, with proper
+ definitions and proven theorems.
+
+ \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
+ retrieves and stores existing facts in the theory context, or the
+ specified target context (see also \secref{sec:target}). Typical
+ applications would also involve attributes, to declare Simplifier
+ rules, for example.
+
+ \item [@{command "theorems"}] is essentially the same as @{command
+ "lemmas"}, but marks the result as a different kind of facts.
+
+ \end{descr}
+*}
+
+
+subsection {* Name spaces *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "global"} & : & \isartrans{theory}{theory} \\
+ @{command_def "local"} & : & \isartrans{theory}{theory} \\
+ @{command_def "hide"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'hide' ('(open)')? name (nameref + )
+ ;
+ \end{rail}
+
+ Isabelle organizes any kind of name declarations (of types,
+ constants, theorems etc.) by separate hierarchically structured name
+ spaces. Normally the user does not have to control the behavior of
+ name spaces by hand, yet the following commands provide some way to
+ do so.
+
+ \begin{descr}
+
+ \item [@{command "global"} and @{command "local"}] change the
+ current name declaration mode. Initially, theories start in
+ @{command "local"} mode, causing all names to be automatically
+ qualified by the theory name. Changing this to @{command "global"}
+ causes all names to be declared without the theory prefix, until
+ @{command "local"} is declared again.
+
+ Note that global names are prone to get hidden accidently later,
+ when qualified names of the same base name are introduced.
+
+ \item [@{command "hide"}~@{text "space names"}] fully removes
+ declarations from a given name space (which may be @{text "class"},
+ @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
+ "(open)"} option, only the base name is hidden. Global
+ (unqualified) names may never be hidden.
+
+ Note that hiding name space accesses has no impact on logical
+ declarations -- they remain valid internally. Entities that are no
+ longer accessible to the user are printed with the special qualifier
+ ``@{text "??"}'' prefixed to the full internal name.
+
+ \end{descr}
+*}
+
+
+subsection {* Incorporating ML code \label{sec:ML} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+ @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
+ @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
+ @{command_def "setup"} & : & \isartrans{theory}{theory} \\
+ @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'use' name
+ ;
+ ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
+ ;
+ 'method\_setup' name '=' text text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "use"}~@{text "file"}] reads and executes ML
+ commands from @{text "file"}. The current theory context is passed
+ down to the ML toplevel and may be modified, using @{ML
+ "Context.>>"} or derived ML commands. The file name is checked with
+ the @{keyword_ref "uses"} dependency declaration given in the theory
+ header (see also \secref{sec:begin-thy}).
+
+ \item [@{command "ML"}~@{text "text"}] is similar to @{command
+ "use"}, but executes ML commands directly from the given @{text
+ "text"}.
+
+ \item [@{command "ML_val"} and @{command "ML_command"}] are
+ diagnostic versions of @{command "ML"}, which means that the context
+ may not be updated. @{command "ML_val"} echos the bindings produced
+ at the ML toplevel, but @{command "ML_command"} is silent.
+
+ \item [@{command "setup"}~@{text "text"}] changes the current theory
+ context by applying @{text "text"}, which refers to an ML expression
+ of type @{ML_type "theory -> theory"}. This enables to initialize
+ any object-logic specific tools and packages written in ML, for
+ example.
+
+ \item [@{command "method_setup"}~@{text "name = text description"}]
+ defines a proof method in the current theory. The given @{text
+ "text"} has to be an ML expression of type @{ML_type "Args.src ->
+ Proof.context -> Proof.method"}. Parsing concrete method syntax
+ from @{ML_type Args.src} input can be quite tedious in general. The
+ following simple examples are for methods without any explicit
+ arguments, or a list of theorems, respectively.
+
+%FIXME proper antiquotations
+{\footnotesize
+\begin{verbatim}
+ Method.no_args (Method.METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt =>
+ Method.METHOD (fn facts => foobar_tac))
+\end{verbatim}
+}
+
+ Note that mere tactic emulations may ignore the @{text facts}
+ parameter above. Proper proof methods would do something
+ appropriate with the list of current facts, though. Single-rule
+ methods usually do strict forward-chaining (e.g.\ by using @{ML
+ Drule.multi_resolves}), while automatic ones just insert the facts
+ using @{ML Method.insert_tac} before applying the main tactic.
+
+ \end{descr}
+*}
+
+
+subsection {* Syntax translation functions *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
+ @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ \begin{rail}
+ ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
+ 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+ ;
+
+ 'token\_translation' text
+ ;
+ \end{rail}
+
+ Syntax translation functions written in ML admit almost arbitrary
+ manipulations of Isabelle's inner syntax. Any of the above commands
+ have a single \railqtok{text} argument that refers to an ML
+ expression of appropriate type, which are as follows by default:
+
+%FIXME proper antiquotations
+\begin{ttbox}
+val parse_ast_translation : (string * (ast list -> ast)) list
+val parse_translation : (string * (term list -> term)) list
+val print_translation : (string * (term list -> term)) list
+val typed_print_translation :
+ (string * (bool -> typ -> term list -> term)) list
+val print_ast_translation : (string * (ast list -> ast)) list
+val token_translation :
+ (string * string * (string -> string * real)) list
+\end{ttbox}
+
+ If the @{text "(advanced)"} option is given, the corresponding
+ translation functions may depend on the current theory or proof
+ context. This allows to implement advanced syntax mechanisms, as
+ translations functions may refer to specific theory declarations or
+ auxiliary proof data.
+
+ See also \cite[\S8]{isabelle-ref} for more information on the
+ general concept of syntax transformations in Isabelle.
+
+%FIXME proper antiquotations
+\begin{ttbox}
+val parse_ast_translation:
+ (string * (Context.generic -> ast list -> ast)) list
+val parse_translation:
+ (string * (Context.generic -> term list -> term)) list
+val print_translation:
+ (string * (Context.generic -> term list -> term)) list
+val typed_print_translation:
+ (string * (Context.generic -> bool -> typ -> term list -> term)) list
+val print_ast_translation:
+ (string * (Context.generic -> ast list -> ast)) list
+\end{ttbox}
+*}
+
+
+subsection {* Oracles *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
+ \end{matharray}
+
+ The oracle interface promotes a given ML function @{ML_text
+ "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type
+ @{ML_text T} given by the user. This acts like an infinitary
+ specification of axioms -- there is no internal check of the
+ correctness of the results! The inference kernel records oracle
+ invocations within the internal derivation object of theorems, and
+ the pretty printer attaches ``@{text "[!]"}'' to indicate results
+ that are not fully checked by Isabelle inferences.
+
+ \begin{rail}
+ 'oracle' name '(' type ')' '=' text
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
+ given ML expression @{text "text"} of type @{ML_text "{theory
+ ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function
+ @{ML_text name} of type @{ML_text "{theory ->"}~@{text
+ "type"}~@{ML_text "-> thm"}.
+
+ \end{descr}
+*}
+
+
+section {* Proof commands *}
+
+text {*
+ Proof commands perform transitions of Isar/VM machine
+ configurations, which are block-structured, consisting of a stack of
+ nodes with three main components: logical proof context, current
+ facts, and open goals. Isar/VM transitions are \emph{typed}
+ according to the following three different modes of operation:
+
+ \begin{descr}
+
+ \item [@{text "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, and enter a sub-proof to establish the
+ actual result.
+
+ \item [@{text "proof(state)"}] is like a nested theory mode: the
+ context may be augmented by \emph{stating} additional assumptions,
+ intermediate results etc.
+
+ \item [@{text "proof(chain)"}] is intermediate between @{text
+ "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
+ the contents of the special ``@{fact_ref this}'' register) have been
+ just picked up in order to be used when refining the goal claimed
+ next.
+
+ \end{descr}
+
+ The proof mode indicator may be read as a verb telling the writer
+ what kind of operation may be performed next. The corresponding
+ typings of proof commands restricts the shape of well-formed proof
+ texts to particular command sequences. So dynamic arrangements of
+ commands eventually turn out as static texts of a certain structure.
+ \Appref{ap:refcard} gives a simplified grammar of the overall
+ (extensible) language emerging that way.
+*}
+
+
+subsection {* Markup commands \label{sec:markup-prf} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "sect"} & : & \isartrans{proof}{proof} \\
+ @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
+ @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
+ @{command_def "txt"} & : & \isartrans{proof}{proof} \\
+ @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
+ \end{matharray}
+
+ These markup commands for proof mode closely correspond to the ones
+ of theory mode (see \S\ref{sec:markup-thy}).
+
+ \begin{rail}
+ ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+ ;
+ \end{rail}
+*}
+
+
+subsection {* Context elements \label{sec:proof-context} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
+ \end{matharray}
+
+ The logical proof context consists of fixed variables and
+ assumptions. The former closely correspond to Skolem constants, or
+ meta-level universal quantification as provided by the Isabelle/Pure
+ logical framework. Introducing some \emph{arbitrary, but fixed}
+ variable via ``@{command "fix"}~@{text x} results in a local value
+ that may be used in the subsequent proof as any other variable or
+ constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
+ the context will be universally closed wrt.\ @{text x} at the
+ outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
+ form using Isabelle's meta-variables).
+
+ Similarly, introducing some assumption @{text \<chi>} has two effects.
+ On the one hand, a local theorem is created that may be used as a
+ fact in subsequent proof steps. On the other hand, any result
+ @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
+ the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
+ using such a result would basically introduce a new subgoal stemming
+ from the assumption. How this situation is handled depends on the
+ version of assumption command used: while @{command "assume"}
+ insists on solving the subgoal by unification with some premise of
+ the goal, @{command "presume"} leaves the subgoal unchanged in order
+ to be proved later by the user.
+
+ Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
+ t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
+ another version of assumption that causes any hypothetical equation
+ @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
+ exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
+ \<phi>[t]"}.
+
+ \railalias{equiv}{\isasymequiv}
+ \railterm{equiv}
+
+ \begin{rail}
+ 'fix' (vars + 'and')
+ ;
+ ('assume' | 'presume') (props + 'and')
+ ;
+ 'def' (def + 'and')
+ ;
+ def: thmdecl? \\ name ('==' | equiv) term termpat?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "fix"}~@{text x}] introduces a local variable
+ @{text x} that is \emph{arbitrary, but fixed.}
+
+ \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
+ "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
+ assumption. Subsequent results applied to an enclosing goal (e.g.\
+ by @{command_ref "show"}) are handled as follows: @{command
+ "assume"} expects to be able to unify with existing premises in the
+ goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
+
+ Several lists of assumptions may be given (separated by
+ @{keyword_ref "and"}; the resulting list of current facts consists
+ of all of these concatenated.
+
+ \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
+ (non-polymorphic) definition. In results exported from the context,
+ @{text x} is replaced by @{text t}. Basically, ``@{command
+ "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
+ x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
+ hypothetical equation solved by reflexivity.
+
+ The default name for the definitional equation is @{text x_def}.
+ Several simultaneous definitions may be given at the same time.
+
+ \end{descr}
+
+ The special name @{fact_ref prems} refers to all assumptions of the
+ current context as a list of theorems. This feature should be used
+ with great care! It is better avoided in final proof texts.
+*}
+
+
+subsection {* Facts and forward chaining *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
+ @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
+ @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
+ @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
+ @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
+ \end{matharray}
+
+ New facts are established either by assumption or proof of local
+ statements. Any fact will usually be involved in further proofs,
+ either as explicit arguments of proof methods, or when forward
+ chaining towards the next goal via @{command "then"} (and variants);
+ @{command "from"} and @{command "with"} are composite forms
+ involving @{command "note"}. The @{command "using"} elements
+ augments the collection of used facts \emph{after} a goal has been
+ stated. Note that the special theorem name @{fact_ref this} refers
+ to the most recently established facts, but only \emph{before}
+ issuing a follow-up claim.
+
+ \begin{rail}
+ 'note' (thmdef? thmrefs + 'and')
+ ;
+ ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
+ recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
+ the result as @{text a}. Note that attributes may be involved as
+ well, both on the left and right hand sides.
+
+ \item [@{command "then"}] indicates forward chaining by the current
+ facts in order to establish the goal to be claimed next. The
+ initial proof method invoked to refine that will be offered the
+ facts to do ``anything appropriate'' (see also
+ \secref{sec:proof-steps}). For example, method @{method_ref rule}
+ (see \secref{sec:pure-meth-att}) would typically do an elimination
+ rather than an introduction. Automatic methods usually insert the
+ facts into the goal state before operation. This provides a simple
+ scheme to control relevance of facts in automated proof search.
+
+ \item [@{command "from"}~@{text b}] abbreviates ``@{command
+ "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
+ equivalent to ``@{command "from"}~@{text this}''.
+
+ \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
+ abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
+ this"}''; thus the forward chaining is from earlier facts together
+ with the current ones.
+
+ \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
+ the facts being currently indicated for use by a subsequent
+ refinement step (such as @{command_ref "apply"} or @{command_ref
+ "proof"}).
+
+ \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
+ structurally similar to @{command "using"}, but unfolds definitional
+ equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
+ and facts.
+
+ \end{descr}
+
+ Forward chaining with an empty list of theorems is the same as not
+ chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
+ effect apart from entering @{text "prove(chain)"} mode, since
+ @{fact_ref nothing} is bound to the empty list of theorems.
+
+ Basic proof methods (such as @{method_ref rule}) expect multiple
+ facts to be given in their proper order, corresponding to a prefix
+ of the premises of the rule involved. Note that positions may be
+ easily skipped using something like @{command "from"}~@{text "_
+ \<AND> a \<AND> b"}, for example. This involves the trivial rule
+ @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
+ ``@{fact_ref "_"}'' (underscore).
+
+ Automated methods (such as @{method simp} or @{method auto}) just
+ insert any given facts before their usual operation. Depending on
+ the kind of procedure involved, the order of facts is less
+ significant here.
+*}
+
+
+subsection {* Goal statements \label{sec:goals} *}
+
+text {*
+ \begin{matharray}{rcl}
+ \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+ \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
+ \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ From a theory context, proof mode is entered by an initial goal
+ command such as @{command "lemma"}, @{command "theorem"}, or
+ @{command "corollary"}. Within a proof, new claims may be
+ introduced locally as well; four variants are available here to
+ indicate whether forward chaining of facts should be performed
+ initially (via @{command_ref "then"}), and whether the final result
+ is meant to solve some pending goal.
+
+ Goals may consist of multiple statements, resulting in a list of
+ facts eventually. A pending multi-goal is internally represented as
+ a meta-level conjunction (printed as @{text "&&"}), which is usually
+ split into the corresponding number of sub-goals prior to an initial
+ method application, via @{command_ref "proof"}
+ (\secref{sec:proof-steps}) or @{command_ref "apply"}
+ (\secref{sec:tactic-commands}). The @{method_ref induct} method
+ covered in \secref{sec:cases-induct} acts on multiple claims
+ simultaneously.
+
+ Claims at the theory level may be either in short or long form. A
+ short goal merely consists of several simultaneous propositions
+ (often just one). A long goal includes an explicit context
+ specification for the subsequent conclusion, involving local
+ parameters and assumptions. Here the role of each part of the
+ statement is explicitly marked by separate keywords (see also
+ \secref{sec:locale}); the local assumptions being introduced here
+ are available as @{fact_ref assms} in the proof. Moreover, there
+ are two kinds of conclusions: @{element_def "shows"} states several
+ simultaneous propositions (essentially a big conjunction), while
+ @{element_def "obtains"} claims several simultaneous simultaneous
+ contexts of (essentially a big disjunction of eliminated parameters
+ and assumptions, cf.\ \secref{sec:obtain}).
+
+ \begin{rail}
+ ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
+ ;
+ ('have' | 'show' | 'hence' | 'thus') goal
+ ;
+ 'print\_statement' modes? thmrefs
+ ;
+
+ goal: (props + 'and')
+ ;
+ longgoal: thmdecl? (contextelem *) conclusion
+ ;
+ conclusion: 'shows' goal | 'obtains' (parname? case + '|')
+ ;
+ case: (vars + 'and') 'where' (props + 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
+ @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
+ \<phi>"} to be put back into the target context. An additional
+ \railnonterm{context} specification may build up an initial proof
+ context for the subsequent claim; this includes local definitions
+ and syntax as well, see the definition of @{syntax contextelem} in
+ \secref{sec:locale}.
+
+ \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
+ "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
+ "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
+ being of a different kind. This discrimination acts like a formal
+ comment.
+
+ \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
+ eventually resulting in a fact within the current logical context.
+ This operation is completely independent of any pending sub-goals of
+ an enclosing goal statements, so @{command "have"} may be freely
+ used for experimental exploration of potential results within a
+ proof body.
+
+ \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
+ "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
+ sub-goal for each one of the finished result, after having been
+ exported into the corresponding context (at the head of the
+ sub-proof of this @{command "show"} command).
+
+ To accommodate interactive debugging, resulting rules are printed
+ before being applied internally. Even more, interactive execution
+ of @{command "show"} predicts potential failure and displays the
+ resulting error as a warning beforehand. Watch out for the
+ following message:
+
+ %FIXME proper antiquitation
+ \begin{ttbox}
+ Problem! Local statement will fail to solve any pending goal
+ \end{ttbox}
+
+ \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
+ "have"}'', i.e.\ claims a local goal to be proven by forward
+ chaining the current facts. Note that @{command "hence"} is also
+ equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
+
+ \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
+ "show"}''. Note that @{command "thus"} is also equivalent to
+ ``@{command "from"}~@{text this}~@{command "show"}''.
+
+ \item [@{command "print_statement"}~@{text a}] prints facts from the
+ current theory or proof context in long statement form, according to
+ the syntax for @{command "lemma"} given above.
+
+ \end{descr}
+
+ Any goal statement causes some term abbreviations (such as
+ @{variable_ref "?thesis"}) to be bound automatically, see also
+ \secref{sec:term-abbrev}. Furthermore, the local context of a
+ (non-atomic) goal is provided via the @{case_ref rule_context} case.
+
+ The optional case names of @{element_ref "obtains"} have a twofold
+ meaning: (1) during the of this claim they refer to the the local
+ context introductions, (2) the resulting rule is annotated
+ accordingly to support symbolic case splits when used with the
+ @{method_ref cases} method (cf. \secref{sec:cases-induct}).
+
+ \medskip
+
+ \begin{warn}
+ Isabelle/Isar suffers theory-level goal statements to contain
+ \emph{unbound schematic variables}, although this does not conform
+ to the aim of human-readable proof documents! The main problem
+ with schematic goals is that the actual outcome is usually hard to
+ predict, depending on the behavior of the proof methods applied
+ during the course of reasoning. Note that most semi-automated
+ methods heavily depend on several kinds of implicit rule
+ declarations within the current theory context. As this would
+ also result in non-compositional checking of sub-proofs,
+ \emph{local goals} are not allowed to be schematic at all.
+ Nevertheless, schematic goals do have their use in Prolog-style
+ interactive synthesis of proven results, usually by stepwise
+ refinement via emulation of traditional Isabelle tactic scripts
+ (see also \secref{sec:tactic-commands}). In any case, users
+ should know what they are doing.
+ \end{warn}
+*}
+
+
+subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
+ @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
+ @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \end{matharray}
+
+ Arbitrary goal refinement via tactics is considered harmful.
+ Structured proof composition in Isar admits proof methods to be
+ invoked in two places only.
+
+ \begin{enumerate}
+
+ \item An \emph{initial} refinement step @{command_ref
+ "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
+ of sub-goals that are to be solved later. Facts are passed to
+ @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
+ "proof(chain)"} mode.
+
+ \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
+ "m\<^sub>2"} is intended to solve remaining goals. No facts are
+ passed to @{text "m\<^sub>2"}.
+
+ \end{enumerate}
+
+ The only other (proper) way to affect pending goals in a proof body
+ is by @{command_ref "show"}, which involves an explicit statement of
+ what is to be solved eventually. Thus we avoid the fundamental
+ problem of unstructured tactic scripts that consist of numerous
+ consecutive goal transformations, with invisible effects.
+
+ \medskip As a general rule of thumb for good proof style, initial
+ proof methods should either solve the goal completely, or constitute
+ some well-understood 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
+ an intelligible manner.
+
+ Unless given explicitly by the user, the default initial method is
+ ``@{method_ref rule}'', which applies a single standard elimination
+ or introduction rule according to the topmost symbol involved.
+ There is no separate default terminal method. Any remaining goals
+ are always solved by assumption in the very last step.
+
+ \begin{rail}
+ 'proof' method?
+ ;
+ 'qed' method?
+ ;
+ 'by' method method?
+ ;
+ ('.' | '..' | 'sorry')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
+ proof method @{text "m\<^sub>1"}; facts for forward chaining are
+ passed if so indicated by @{text "proof(chain)"} mode.
+
+ \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
+ goals by proof method @{text "m\<^sub>2"} and concludes the
+ sub-proof by assumption. If the goal had been @{text "show"} (or
+ @{text "thus"}), some pending sub-goal is solved as well by the rule
+ resulting from the result \emph{exported} into the enclosing goal
+ context. Thus @{text "qed"} may fail for two reasons: either @{text
+ "m\<^sub>2"} fails, or the resulting rule does not fit to any
+ pending goal\footnote{This includes any additional ``strong''
+ assumptions as introduced by @{text "assume"}.} of the enclosing
+ context. Debugging such a situation might involve temporarily
+ changing @{command "show"} into @{command "have"}, or weakening the
+ local context by replacing occurrences of @{command "assume"} by
+ @{command "presume"}.
+
+ \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
+ \emph{terminal proof}\index{proof!terminal}; it abbreviates
+ @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
+ "m\<^sub>2"}, but with backtracking across both methods. Debugging
+ an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
+ command can be done by expanding its definition; in many cases
+ @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
+ "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
+ problem.
+
+ \item [``@{command ".."}''] is a \emph{default
+ proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
+ "rule"}.
+
+ \item [``@{command "."}''] is a \emph{trivial
+ proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
+ "this"}.
+
+ \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
+ pretending to solve the pending claim without further ado. This
+ only works in interactive development, or if the @{ML
+ quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
+ proofs are not the real thing. Internally, each theorem container
+ is tainted by an oracle invocation, which is indicated as ``@{text
+ "[!]"}'' in the printed result.
+
+ The most important application of @{command "sorry"} is to support
+ experimentation and top-down proof development.
+
+ \end{descr}
+*}
+
+
+subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
+
+text {*
+ The following proof methods and attributes refer to basic logical
+ operations of Isar. Further methods and attributes are provided by
+ several generic and object-logic specific tools and packages (see
+ \chref{ch:gen-tools} and \chref{ch:logics}).
+
+ \begin{matharray}{rcl}
+ @{method_def "-"} & : & \isarmeth \\
+ @{method_def "fact"} & : & \isarmeth \\
+ @{method_def "assumption"} & : & \isarmeth \\
+ @{method_def "this"} & : & \isarmeth \\
+ @{method_def "rule"} & : & \isarmeth \\
+ @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
+ @{attribute_def "intro"} & : & \isaratt \\
+ @{attribute_def "elim"} & : & \isaratt \\
+ @{attribute_def "dest"} & : & \isaratt \\
+ @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
+ @{attribute_def "OF"} & : & \isaratt \\
+ @{attribute_def "of"} & : & \isaratt \\
+ @{attribute_def "where"} & : & \isaratt \\
+ \end{matharray}
+
+ \begin{rail}
+ 'fact' thmrefs?
+ ;
+ 'rule' thmrefs?
+ ;
+ 'iprover' ('!' ?) (rulemod *)
+ ;
+ rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
+ ;
+ ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
+ ;
+ 'rule' 'del'
+ ;
+ 'OF' thmrefs
+ ;
+ 'of' insts ('concl' ':' insts)?
+ ;
+ 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [``@{method "-"}''] does nothing but insert the forward
+ chaining facts as premises into the goal. Note that command
+ @{command_ref "proof"} without any method actually performs a single
+ reduction step using the @{method_ref rule} method; thus a plain
+ \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
+ "-"}'' rather than @{command "proof"} alone.
+
+ \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
+ some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
+ the current proof context) modulo unification of schematic type and
+ term variables. The rule structure is not taken into account, i.e.\
+ meta-level implication is considered atomic. This is the same
+ principle underlying literal facts (cf.\ \secref{sec:syn-att}):
+ ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
+ equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
+ "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
+ @{text "\<turnstile> \<phi>"} in the proof context.
+
+ \item [@{method assumption}] solves some goal by a single assumption
+ step. All given facts are guaranteed to participate in the
+ refinement; this means there may be only 0 or 1 in the first place.
+ Recall that @{command "qed"} (\secref{sec:proof-steps}) already
+ concludes any remaining sub-goals by assumption, so structured
+ proofs usually need not quote the @{method assumption} method at
+ all.
+
+ \item [@{method this}] applies all of the current facts directly as
+ rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
+ "by"}~@{text this}''.
+
+ \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
+ rule given as argument in backward manner; facts are used to reduce
+ the rule before applying it to the goal. Thus @{method rule}
+ without facts is plain introduction, while with facts it becomes
+ elimination.
+
+ When no arguments are given, the @{method rule} method tries to pick
+ appropriate rules automatically, as declared in the current context
+ using the @{attribute intro}, @{attribute elim}, @{attribute dest}
+ attributes (see below). This is the default behavior of @{command
+ "proof"} and ``@{command ".."}'' (double-dot) steps (see
+ \secref{sec:proof-steps}).
+
+ \item [@{method iprover}] performs intuitionistic proof search,
+ depending on specifically declared rules from the context, or given
+ as explicit arguments. Chained facts are inserted into the goal
+ before commencing proof search; ``@{method iprover}@{text "!"}''
+ means to include the current @{fact prems} as well.
+
+ Rules need to be classified as @{attribute intro}, @{attribute
+ elim}, or @{attribute dest}; here the ``@{text "!"} indicator refers
+ to ``safe'' rules, which may be applied aggressively (without
+ considering back-tracking later). Rules declared with ``@{text
+ "?"}'' are ignored in proof search (the single-step @{method rule}
+ method still observes these). An explicit weight annotation may be
+ given as well; otherwise the number of rule premises will be taken
+ into account here.
+
+ \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
+ declare introduction, elimination, and destruct rules, to be used
+ with the @{method rule} and @{method iprover} methods. Note that
+ the latter will ignore rules declared with ``@{text "?"}'', while
+ ``@{text "!"}'' are used most aggressively.
+
+ The classical reasoner (see \secref{sec:classical}) introduces its
+ own variants of these attributes; use qualified names to access the
+ present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
+
+ \item [@{attribute rule}~@{text del}] undeclares introduction,
+ elimination, or destruct rules.
+
+ \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
+ theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
+ (in parallel). This corresponds to the @{ML "op MRS"} operation in
+ ML, but note the reversed order. Positions may be effectively
+ skipped by including ``@{verbatim _}'' (underscore) as argument.
+
+ \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
+ positional instantiation of term variables. The terms @{text
+ "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
+ variables occurring in a theorem from left to right; ``@{verbatim
+ _}'' (underscore) indicates to skip a position. Arguments following
+ a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
+ of the conclusion of a rule.
+
+ \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
+ \<AND> x\<^sub>n = t\<^sub>n"}] performs named instantiation of
+ schematic type and term variables occurring in a theorem. Schematic
+ variables have to be specified on the left-hand side (e.g.\ @{text
+ "?x1.3"}). The question mark may be omitted if the variable name is
+ a plain identifier without index. As type instantiations are
+ inferred from term instantiations, explicit type instantiations are
+ seldom necessary.
+
+ \end{descr}
+*}
+
+
+subsection {* Term abbreviations \label{sec:term-abbrev} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{keyword_def "is"} & : & syntax \\
+ \end{matharray}
+
+ Abbreviations may be either bound by explicit @{command "let"}@{text
+ "p \<equiv> t"} statements, or by annotating assumptions or goal statements
+ with a list of patterns ``@{text "\<IS> p\<^sub>1 \<dots> p\<^sub>n"}''.
+ In both cases, higher-order matching is invoked to bind
+ extra-logical term variables, which may be either named schematic
+ variables of the form @{text ?x}, or nameless dummies ``@{variable
+ _}'' (underscore). Note that in the @{command "let"} form the
+ patterns occur on the left-hand side, while the @{keyword "is"}
+ patterns are in postfix position.
+
+ Polymorphism of term bindings is handled in Hindley-Milner style,
+ similar to ML. Type variables referring to local assumptions or
+ open goal statements are \emph{fixed}, while those of finished
+ results or bound by @{command "let"} may occur in \emph{arbitrary}
+ instances later. Even though actual polymorphism should be rarely
+ used in practice, this mechanism is essential to achieve proper
+ incremental type-inference, as the user proceeds to build up the
+ Isar proof text from left to right.
+
+ \medskip Term abbreviations are quite different from local
+ definitions as introduced via @{command "def"} (see
+ \secref{sec:proof-context}). The latter are visible within the
+ logic as actual equations, while abbreviations disappear during the
+ input process just after type checking. Also note that @{command
+ "def"} does not support polymorphism.
+
+ \begin{rail}
+ 'let' ((term + 'and') '=' term + 'and')
+ ;
+ \end{rail}
+
+ The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
+ or \railnonterm{proppat} (see \secref{sec:term-decls}).
+
+ \begin{descr}
+
+ \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND>
+ \<dots>p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns
+ @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order
+ matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
+
+ \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
+ "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
+ preceding statement. Also note that @{keyword "is"} is not a
+ separate command, but part of others (such as @{command "assume"},
+ @{command "have"} etc.).
+
+ \end{descr}
+
+ Some \emph{implicit} term abbreviations\index{term abbreviations}
+ for goals and facts are available as well. For any open goal,
+ @{variable_ref thesis} refers to its object-level statement,
+ abstracted over any meta-level parameters (if present). Likewise,
+ @{variable_ref this} is bound for fact statements resulting from
+ assumptions or finished goals. In case @{variable this} refers to
+ an object-logic statement that is an application @{text "f t"}, then
+ @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
+ (three dots). The canonical application of this convenience are
+ calculational proofs (see \secref{sec:calculation}).
+*}
+
+
+subsection {* Block structure *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
+ \end{matharray}
+
+ 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} internal blocks, which are closed again when concluding
+ the sub-proof (by @{command "qed"} etc.). Sections of different
+ context within a sub-proof may be switched via @{command "next"},
+ which is just a single block-close followed by block-open again.
+ The effect of @{command "next"} is to reset the local proof context;
+ there is no goal focus involved here!
+
+ For slightly more advanced applications, there are explicit block
+ parentheses as well. These typically achieve a stronger forward
+ style of reasoning.
+
+ \begin{descr}
+
+ \item [@{command "next"}] switches to a fresh block within a
+ sub-proof, resetting the local context to the initial one.
+
+ \item [@{command "{"} and @{command "}"}] explicitly open and close
+ blocks. Any current facts pass through ``@{command "{"}''
+ unchanged, while ``@{command "}"}'' causes any result to be
+ \emph{exported} into the enclosing context. Thus fixed variables
+ are generalized, assumptions discharged, and local definitions
+ unfolded (cf.\ \secref{sec:proof-context}). There is no difference
+ of @{command "assume"} and @{command "presume"} in this mode of
+ forward reasoning --- in contrast to plain backward reasoning with
+ the result exported at @{command "show"} time.
+
+ \end{descr}
+*}
+
+
+subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
+
+text {*
+ The Isar provides separate commands to accommodate tactic-style
+ proof scripts within the same system. While being outside the
+ orthodox Isar proof language, these might come in handy for
+ interactive exploration and debugging, or even actual tactical proof
+ within new-style theories (to benefit from document preparation, for
+ example). See also \secref{sec:tactics} for actual tactics, that
+ have been encapsulated as proof methods. Proper proof methods may
+ be used in scripts, too.
+
+ \begin{matharray}{rcl}
+ @{command_def "apply"}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
+ @{command_def "apply_end"}^* & : & \isartrans{proof(state)}{proof(state)} \\
+ @{command_def "done"}^* & : & \isartrans{proof(prove)}{proof(state)} \\
+ @{command_def "defer"}^* & : & \isartrans{proof}{proof} \\
+ @{command_def "prefer"}^* & : & \isartrans{proof}{proof} \\
+ @{command_def "back"}^* & : & \isartrans{proof}{proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ ( 'apply' | 'apply\_end' ) method
+ ;
+ 'defer' nat?
+ ;
+ 'prefer' nat
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "apply"}~@{text m}] applies proof method @{text m}
+ in initial position, but unlike @{command "proof"} it retains
+ ``@{text "proof(prove)"}'' mode. Thus consecutive method
+ applications may be given just as in tactic scripts.
+
+ Facts are passed to @{text m} as indicated by the goal's
+ forward-chain mode, and are \emph{consumed} afterwards. Thus any
+ further @{command "apply"} command would always work in a purely
+ backward manner.
+
+ \item [@{command "apply_end"}~@{text "m"}] applies proof method
+ @{text m} as if in terminal position. Basically, this simulates a
+ multi-step tactic script for @{command "qed"}, but may be given
+ anywhere within the proof body.
+
+ No facts are passed to @{method m} here. Furthermore, the static
+ context is that of the enclosing goal (as for actual @{command
+ "qed"}). Thus the proof method may not refer to any assumptions
+ introduced in the current body, for example.
+
+ \item [@{command "done"}] completes a proof script, provided that
+ the current goal state is solved completely. Note that actual
+ structured proof commands (e.g.\ ``@{command "."}'' or @{command
+ "sorry"}) may be used to conclude proof scripts as well.
+
+ \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
+ n}] shuffle the list of pending goals: @{command "defer"} puts off
+ sub-goal @{text n} to the end of the list (@{text "n = 1"} by
+ default), while @{command "prefer"} brings sub-goal @{text n} to the
+ front.
+
+ \item [@{command "back"}] does back-tracking over the result
+ sequence of the latest proof command. Basically, any proof command
+ may return multiple results.
+
+ \end{descr}
+
+ Any proper Isar proof method may be used with tactic script commands
+ such as @{command "apply"}. A few additional emulations of actual
+ tactics are provided as well; these would be never used in actual
+ structured proofs, of course.
+*}
+
+
+subsection {* Meta-linguistic features *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "oops"} & : & \isartrans{proof}{theory} \\
+ \end{matharray}
+
+ The @{command "oops"} command discontinues the current proof
+ attempt, while considering the partial proof text as properly
+ processed. This is conceptually quite different from ``faking''
+ actual proofs via @{command_ref "sorry"} (see
+ \secref{sec:proof-steps}): @{command "oops"} does not observe the
+ proof structure at all, but goes back right to the theory level.
+ Furthermore, @{command "oops"} does not produce any result theorem
+ --- there is no intended claim to be able to complete the proof
+ anyhow.
+
+ A typical application of @{command "oops"} is to explain Isar proofs
+ \emph{within} the system itself, in conjunction with the document
+ preparation tools of Isabelle described in \cite{isabelle-sys}.
+ Thus partial or even wrong proof attempts can be discussed in a
+ logically sound manner. Note that the Isabelle {\LaTeX} macros can
+ be easily adapted to print something like ``@{text "\<dots>"}'' instead of
+ the keyword ``@{command "oops"}''.
+
+ \medskip The @{command "oops"} command is undo-able, unlike
+ @{command_ref "kill"} (see \secref{sec:history}). The effect is to
+ get back to the theory just before the opening of the proof.
+*}
+
+
+section {* Other commands *}
+
+subsection {* Diagnostics *}
+
+text {*
+ \begin{matharray}{rcl}
+ \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
+ \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ These diagnostic commands assist interactive development. Note that
+ @{command undo} does not apply here, the theory or proof
+ configuration is not changed.
+
+ \begin{rail}
+ 'pr' modes? nat? (',' nat)?
+ ;
+ 'thm' modes? thmrefs
+ ;
+ 'term' modes? term
+ ;
+ 'prop' modes? prop
+ ;
+ 'typ' modes? type
+ ;
+ 'prf' modes? thmrefs?
+ ;
+ 'full\_prf' modes? thmrefs?
+ ;
+
+ modes: '(' (name + ) ')'
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "pr"}~@{text "goals, prems"}] prints the current
+ proof state (if present), including the proof context, current facts
+ and goals. The optional limit arguments affect the number of goals
+ and premises to be displayed, which is initially 10 for both.
+ Omitting limit values leaves the current setting unchanged.
+
+ \item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves
+ theorems from the current theory or proof context. Note that any
+ attributes included in the theorem specifications are applied to a
+ temporary context derived from the current theory or proof; the
+ result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
+ \<dots>, a\<^sub>n"} do not have any permanent effect.
+
+ \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
+ read, type-check and print terms or propositions according to the
+ current theory or proof context; the inferred type of @{text t} is
+ output as well. Note that these commands are also useful in
+ inspecting the current environment of term abbreviations.
+
+ \item [@{command "typ"}~@{text \<tau>}] reads and prints types of the
+ meta-logic according to the current theory or proof context.
+
+ \item [@{command "prf"}] displays the (compact) proof term of the
+ current proof state (if present), or of the given theorems. Note
+ that this requires proof terms to be switched on for the current
+ object logic (see the ``Proof terms'' section of the Isabelle
+ reference manual for information on how to do this).
+
+ \item [@{command "full_prf"}] is like @{command "prf"}, but displays
+ the full proof term, i.e.\ also displays information omitted in the
+ compact proof term, which is denoted by ``@{verbatim _}''
+ placeholders there.
+
+ \end{descr}
+
+ All of the diagnostic commands above admit a list of @{text modes}
+ to be specified, which is appended to the current print mode (see
+ also \cite{isabelle-ref}). Thus the output behavior may be modified
+ according particular print mode features. For example, @{command
+ "pr"}~@{text "(latex xsymbols symbols)"} would print the current
+ proof state with mathematical symbols and special characters
+ represented in {\LaTeX} source, according to the Isabelle style
+ \cite{isabelle-sys}.
+
+ Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
+ systematic way to include formal items into the printed text
+ document.
+*}
+
+
+subsection {* Inspecting the context *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "print_commands"}^* & : & \isarkeep{\cdot} \\
+ @{command_def "print_theory"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_syntax"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_methods"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_attributes"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_theorems"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "find_theorems"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "thms_deps"}^* & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_facts"}^* & : & \isarkeep{proof} \\
+ @{command_def "print_binds"}^* & : & \isarkeep{proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'print\_theory' ( '!'?)
+ ;
+
+ 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+ ;
+ criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+ 'simp' ':' term | term)
+ ;
+ 'thm\_deps' thmrefs
+ ;
+ \end{rail}
+
+ These commands print certain parts of the theory and proof context.
+ Note that there are some further ones available, such as for the set
+ of rules declared for simplifications.
+
+ \begin{descr}
+
+ \item [@{command "print_commands"}] prints Isabelle's outer theory
+ syntax, including keywords and command.
+
+ \item [@{command "print_theory"}] prints the main logical content of
+ the theory context; the ``@{text "!"}'' option indicates extra
+ verbosity.
+
+ \item [@{command "print_syntax"}] prints the inner syntax of types
+ and terms, depending on the current context. The output can be very
+ verbose, including grammar tables and syntax translation rules. See
+ \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
+ inner syntax.
+
+ \item [@{command "print_methods"}] prints all proof methods
+ available in the current theory context.
+
+ \item [@{command "print_attributes"}] prints all attributes
+ available in the current theory context.
+
+ \item [@{command "print_theorems"}] prints theorems resulting from
+ the last command.
+
+ \item [@{command "find_theorems"}~@{text criteria}] retrieves facts
+ from the theory or proof context matching all of given search
+ criteria. The criterion @{text "name: p"} selects all theorems
+ whose fully qualified name matches pattern @{text p}, which may
+ contain ``@{text "*"}'' wildcards. The criteria @{text intro},
+ @{text elim}, and @{text dest} select theorems that match the
+ current goal as introduction, elimination or destruction rules,
+ respectively. The criterion @{text "simp: t"} selects all rewrite
+ rules whose left-hand side matches the given term. The criterion
+ term @{text t} selects all theorems that contain the pattern @{text
+ t} -- as usual, patterns may contain occurrences of the dummy
+ ``@{verbatim _}'', schematic variables, and type constraints.
+
+ Criteria can be preceded by ``@{text "-"}'' to select theorems that
+ do \emph{not} match. Note that giving the empty list of criteria
+ yields \emph{all} currently known facts. An optional limit for the
+ number of printed facts may be given; the default is 40. By
+ default, duplicates are removed from the search result. Use
+ @{keyword "with_dups"} to display duplicates.
+
+ \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
+ visualizes dependencies of facts, using Isabelle's graph browser
+ tool (see also \cite{isabelle-sys}).
+
+ \item [@{command "print_facts"}] prints all local facts of the
+ current context, both named and unnamed ones.
+
+ \item [@{command "print_binds"}] prints all term abbreviations
+ present in the context.
+
+ \end{descr}
+*}
+
+
+subsection {* History commands \label{sec:history} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ The Isabelle/Isar top-level maintains a two-stage history, for
+ theory and proof state transformation. Basically, any command can
+ be undone using @{command "undo"}, excluding mere diagnostic
+ elements. Its effect may be revoked via @{command "redo"}, unless
+ the corresponding @{command "undo"} step has crossed the beginning
+ of a proof or theory. The @{command "kill"} command aborts the
+ current history node altogether, discontinuing a proof or even the
+ whole theory. This operation is \emph{not} undo-able.
+
+ \begin{warn}
+ History commands should never be used with user interfaces such as
+ Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
+ care of stepping forth and back itself. Interfering by manual
+ @{command "undo"}, @{command "redo"}, or even @{command "kill"}
+ commands would quickly result in utter confusion.
+ \end{warn}
+*}
+
+
+subsection {* System operations *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "cd"}^* & : & \isarkeep{\cdot} \\
+ @{command_def "pwd"}^* & : & \isarkeep{\cdot} \\
+ @{command_def "use_thy"}^* & : & \isarkeep{\cdot} \\
+ @{command_def "display_drafts"}^* & : & \isarkeep{\cdot} \\
+ @{command_def "print_drafts"}^* & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('cd' | 'use\_thy' | 'update\_thy') name
+ ;
+ ('display\_drafts' | 'print\_drafts') (name +)
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "cd"}~@{text path}] changes the current directory
+ of the Isabelle process.
+
+ \item [@{command "pwd"}] prints the current working directory.
+
+ \item [@{command "use_thy"}~@{text A}] preload theory @{text A}.
+ These system commands are scarcely used when working interactively,
+ since loading of theories is done automatically as required.
+
+ \item [@{command "display_drafts"}~@{text paths} and @{command
+ "print_drafts"}~@{text paths}] perform simple output of a given list
+ of raw source files. Only those symbols that do not require
+ additional {\LaTeX} packages are displayed properly, everything else
+ is left verbatim.
+
+ \end{descr}
+*}
+
+end
--- a/doc-src/IsarRef/Thy/syntax.thy Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/syntax.thy Fri May 02 16:36:05 2008 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
theory "syntax"
imports CPure
--- a/doc-src/IsarRef/isar-ref.tex Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Fri May 02 16:36:05 2008 +0200
@@ -71,7 +71,7 @@
\input{Thy/document/intro.tex}
\input{basics.tex}
\input{Thy/document/syntax.tex}
-\input{pure.tex}
+\input{Thy/document/pure.tex}
\input{generic.tex}
\input{logics.tex}
--- a/doc-src/IsarRef/pure.tex Fri May 02 16:32:51 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1636 +0,0 @@
-
-\chapter{Basic language elements}\label{ch:pure-syntax}
-
-Subsequently, we introduce the main part of Pure theory and proof commands,
-together with fundamental proof methods and attributes.
-Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
-tools and packages (such as the Simplifier) that are either part of Pure
-Isabelle or pre-installed in most object logics. Chapter~\ref{ch:logics}
-refers to object-logic specific elements (mainly for HOL and ZF).
-
-\medskip
-
-Isar commands may be either \emph{proper} document constructors, or
-\emph{improper commands}. Some proof methods and attributes introduced later
-are classified as improper as well. Improper Isar language elements, which
-are subsequently marked by ``$^*$'', are often helpful when developing proof
-documents, while their use is discouraged for the final human-readable
-outcome. Typical examples are diagnostic commands that print terms or
-theorems according to the current context; other commands emulate old-style
-tactical theorem proving.
-
-
-\section{Theory commands}
-
-\subsection{Defining theories}\label{sec:begin-thy}
-
-\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}
-\begin{matharray}{rcl}
- \isarcmd{header} & : & \isarkeep{toplevel} \\
- \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
- \isarcmd{end} & : & \isartrans{theory}{toplevel} \\
-\end{matharray}
-
-Isabelle/Isar ``new-style'' theories are either defined via theory files or
-interactively. Both theory-level specifications and proofs are handled
-uniformly --- occasionally definitional mechanisms even require some explicit
-proof as well. In contrast, ``old-style'' Isabelle theories support batch
-processing only, with the proof scripts collected in separate ML files.
-
-The first ``real'' command of any theory has to be $\THEORY$, which
-starts a new theory based on the merge of existing ones. Just
-preceding $\THEORY$, there may be an optional $\isarkeyword{header}$
-declaration, which is relevant to document preparation only; it acts
-very much like a special pre-theory markup command (cf.\
-\S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The $\END$
-command concludes a theory development; it has to be the very last
-command of any theory file loaded in batch-mode.
-
-\begin{rail}
- 'header' text
- ;
- 'theory' name 'imports' (name +) uses? 'begin'
- ;
-
- uses: 'uses' ((name | parname) +);
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{header}~text$] provides plain text markup just preceding
- the formal beginning of a theory. In actual document preparation the
- corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
- produce chapter or section headings. See also \S\ref{sec:markup-thy} and
- \S\ref{sec:markup-prf} for further markup commands.
-
-\item [$\THEORY~A~\isarkeyword{imports}~B@1~\ldots~B@n~\isarkeyword{begin}$]
- starts a new theory $A$ based on the merge of existing theories $B@1, \dots,
- B@n$.
-
- Due to inclusion of several ancestors, the overall theory structure emerging
- in an Isabelle session forms a directed acyclic graph (DAG). Isabelle's
- theory loader ensures that the sources contributing to the development graph
- are always up-to-date. Changed files are automatically reloaded when
- processing theory headers interactively; batch-mode explicitly distinguishes
- \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
-
- The optional $\isarkeyword{uses}$ specification declares additional
- dependencies on ML files. Files will be loaded immediately, unless the name
- is put in parentheses, which merely documents the dependency to be resolved
- later in the text (typically via explicit $\isarcmd{use}$ in the body text,
- see \S\ref{sec:ML}). In reminiscence of the old-style theory system of
- Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
- \texttt{$A$.ML} consisting of ML code that is executed in the context of the
- \emph{finished} theory $A$. That file should not be included in the
- $\isarkeyword{uses}$ dependency declaration, though.
-
-\item [$\END$] concludes the current theory definition or context switch.
- Note that this command cannot be undone, but the whole theory definition has
- to be retracted.
-
-\end{descr}
-
-
-\subsection{Markup commands}\label{sec:markup-thy}
-
-\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
-\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
-\begin{matharray}{rcl}
- \isarcmd{chapter} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{section} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{subsection} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{subsubsection} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{text} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{text_raw} & : & \isarkeep{local{\dsh}theory} \\
-\end{matharray}
-
-Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
-a structured way to insert text into the document generated from a theory (see
-\cite{isabelle-sys} for more information on Isabelle's document preparation
-tools).
-
-\begin{rail}
- ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
- ;
- 'text\_raw' text
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
- $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
- and section headings.
-\item [$\TEXT$] specifies paragraphs of plain text.
-\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
- without additional markup. Thus the full range of document manipulations
- becomes available.
-\end{descr}
-
-The $text$ argument of these markup commands (except for
-$\isarkeyword{text_raw}$) may contain references to formal entities
-(``antiquotations'', see also \S\ref{sec:antiq}). These are
-interpreted in the present theory context, or the specified $target$.
-
-Any of these markup elements corresponds to a {\LaTeX} command with the name
-prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain
-macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for
-$\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a
-{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots}
- \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text
-to be inserted directly into the {\LaTeX} source.
-
-\medskip
-
-Additional markup commands are available for proofs (see
-\S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$
-declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just
-preceding the actual theory definition.
-
-
-\subsection{Type classes and sorts}\label{sec:classes}
-
-\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
-\indexisarcmd{class-deps}
-\begin{matharray}{rcll}
- \isarcmd{classes} & : & \isartrans{theory}{theory} \\
- \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
- \isarcmd{class_deps} & : & \isarkeep{theory~|~proof} \\
-\end{matharray}
-
-\begin{rail}
- 'classes' (classdecl +)
- ;
- 'classrel' (nameref ('<' | subseteq) nameref + 'and')
- ;
- 'defaultsort' sort
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
- subclass of existing classes $\vec c$. Cyclic class structures are ruled
- out.
-\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations
- between existing classes $c@1$ and $c@2$. This is done axiomatically! The
- $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
- proven class relations.
-\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
- any type variables given without sort constraints. Usually, the default
- sort would be only changed when defining a new object-logic.
-\item [$\isarkeyword{class_deps}$] visualizes the subclass relation,
- using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
-\end{descr}
-
-
-\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
-
-\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
-\begin{matharray}{rcll}
- \isarcmd{types} & : & \isartrans{theory}{theory} \\
- \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
- \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
- \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
-\end{matharray}
-
-\begin{rail}
- 'types' (typespec '=' type infix? +)
- ;
- 'typedecl' typespec infix?
- ;
- 'nonterminals' (name +)
- ;
- 'arities' (nameref '::' arity +)
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\TYPES~(\vec\alpha)t = \tau$] 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.
-
-\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
- $t$, intended as an actual logical type. Note that the Isabelle/HOL
- object-logic overrides $\isarkeyword{typedecl}$ by its own version
- (\S\ref{sec:hol-typedef}).
-
-\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
- $\vec 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$] augments Isabelle's order-sorted
- signature of types by new type constructor arities. This is done
- axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
- way to introduce proven type arities.
-
-\end{descr}
-
-
-\subsection{Primitive constants and definitions}\label{sec:consts}
-
-Definitions essentially express abbreviations within the logic. The
-simplest form of a definition is $f :: \sigma \equiv t$, where $f$ is
-a newly declared constant. Isabelle also allows derived forms where
-the arguments of~$f$ appear on the left, abbreviating a string of
-$\lambda$-abstractions, e.g.\ $f \equiv \lambda x\, y. t$ may be
-written more conveniently as $f \, x \, y \equiv t$. Moreover,
-definitions may be weakened by adding arbitrary pre-conditions: $A
-\Imp f \, x\, y \equiv t$.
-
-\medskip The built-in well-formedness conditions for definitional
-specifications are:
-\begin{itemize}
-\item Arguments (on the left-hand side) must be distinct variables.
-\item All variables on the right-hand side must also appear on the
- left-hand side.
-\item All type variables on the right-hand side must also appear on
- the left-hand side; this prohibits $0::nat \equiv length
- ([]::\alpha\, list)$ for example.
-\item The definition must not be recursive. Most object-logics
- provide definitional principles that can be used to express
- recursion safely.
-\end{itemize}
-
-Overloading means that a constant being declared as $c :: \alpha\,
-decl$ may be defined separately on type instances $c ::
-(\vec\beta)\,t\,decl$ for each type constructor $t$. The RHS may
-mention overloaded constants recursively at type instances
-corresponding to the immediate argument types $\vec\beta$. Incomplete
-specification patterns impose global constraints on all occurrences,
-e.g. $d :: \alpha \times \alpha$ on the LHS means that all
-corresponding occurrences on some RHS need to be an instance of this,
-general $d :: \alpha \times \beta$ will be disallowed.
-
-\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
-\begin{matharray}{rcl}
- \isarcmd{consts} & : & \isartrans{theory}{theory} \\
- \isarcmd{defs} & : & \isartrans{theory}{theory} \\
- \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'consts' ((name '::' type mixfix?) +)
- ;
- 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
- ;
-\end{rail}
-
-\begin{rail}
- 'constdefs' structs? (constdecl? constdef +)
- ;
-
- structs: '(' 'structure' (vars + 'and') ')'
- ;
- constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
- ;
- constdef: thmdecl? prop
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
- scheme $\sigma$. The optional mixfix annotations may attach concrete syntax
- to the constants declared.
-
-\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for
- some existing constant.
-
- The $(unchecked)$ option disables global dependency checks for this
- definition, which is occasionally useful for exotic overloading. It
- is at the discretion of the user to avoid malformed theory
- specifications!
-
- The $(overloaded)$ option declares definitions to be potentially
- overloaded. Unless this option is given, a warning message would be
- issued for any definitional equation with a more special type than
- that of the corresponding constant declaration.
-
-\item [$\CONSTDEFS$] provides a streamlined combination of constants
- declarations and definitions: type-inference takes care of the most general
- typing of the given specification (the optional type constraint may refer to
- type-inference dummies ``$_$'' as usual). The resulting type declaration
- needs to agree with that of the specification; overloading is \emph{not}
- supported here!
-
- The constant name may be omitted altogether, if neither type nor syntax
- declarations are given. The canonical name of the definitional axiom for
- constant $c$ will be $c_def$, unless specified otherwise. Also note that
- the given list of specifications is processed in a strictly sequential
- manner, with type-checking being performed independently.
-
- An optional initial context of $(structure)$ declarations admits use of
- indexed syntax, using the special symbol \verb,\<index>, (printed as
- ``\i''). The latter concept is particularly useful with locales (see also
- \S\ref{sec:locale}).
-\end{descr}
-
-
-\subsection{Syntax and translations}\label{sec:syn-trans}
-
-\indexisarcmd{syntax}\indexisarcmd{no-syntax}
-\indexisarcmd{translations}\indexisarcmd{no-translations}
-\begin{matharray}{rcl}
- \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
- \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\
- \isarcmd{translations} & : & \isartrans{theory}{theory} \\
- \isarcmd{no_translations} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\railalias{rightleftharpoons}{\isasymrightleftharpoons}
-\railterm{rightleftharpoons}
-
-\railalias{rightharpoonup}{\isasymrightharpoonup}
-\railterm{rightharpoonup}
-
-\railalias{leftharpoondown}{\isasymleftharpoondown}
-\railterm{leftharpoondown}
-
-\begin{rail}
- ('syntax' | 'no\_syntax') mode? (constdecl +)
- ;
- ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
- ;
-
- mode: ('(' ( name | 'output' | name 'output' ) ')')
- ;
- transpat: ('(' nameref ')')? string
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
- except that the actual logical signature extension is omitted. Thus the
- context free grammar of Isabelle's inner syntax may be augmented in
- arbitrary ways, independently of the logic. The $mode$ argument refers to
- the print mode that the grammar rules belong; unless the
- $\isarkeyword{output}$ indicator is given, all productions are added both to
- the input and output grammar.
-
-\item [$\isarkeyword{no_syntax}~(mode)~decls$] removes grammar declarations
- (and translations) resulting from $decls$, which are interpreted in the same
- manner as for $\isarkeyword{syntax}$ above.
-
-\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
- rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
- rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
- Translation patterns may be prefixed by the syntactic category to be used
- for parsing; the default is $logic$.
-
-\item [$\isarkeyword{no_translations}~rules$] removes syntactic
- translation rules, which are interpreted in the same manner as for
- $\isarkeyword{translations}$ above.
-
-\end{descr}
-
-
-\subsection{Axioms and theorems}\label{sec:axms-thms}
-
-\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
-\begin{matharray}{rcll}
- \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \isarcmd{lemmas} & : & \isarkeep{local{\dsh}theory} \\
- \isarcmd{theorems} & : & isarkeep{local{\dsh}theory} \\
-\end{matharray}
-
-\begin{rail}
- 'axioms' (axmdecl prop +)
- ;
- ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
- axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and
- may be referred later just as any other theorem.
-
- Axioms are usually only introduced when declaring new logical systems.
- Everyday work is typically done the hard way, with proper definitions and
- proven theorems.
-
-\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores
- existing facts in the theory context, or the specified target
- context (see also \S\ref{sec:target}). Typical applications would
- also involve attributes, to declare Simplifier rules, for example.
-
-\item [$\isarkeyword{theorems}$] is essentially the same as
- $\isarkeyword{lemmas}$, but marks the result as a different kind of facts.
-
-\end{descr}
-
-
-\subsection{Name spaces}
-
-\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide}
-\begin{matharray}{rcl}
- \isarcmd{global} & : & \isartrans{theory}{theory} \\
- \isarcmd{local} & : & \isartrans{theory}{theory} \\
- \isarcmd{hide} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'hide' ('(open)')? name (nameref + )
- ;
-\end{rail}
-
-Isabelle organizes any kind of name declarations (of types, constants,
-theorems etc.) by separate hierarchically structured name spaces. Normally
-the user does not have to control the behavior of name spaces by hand, yet the
-following commands provide some way to do so.
-
-\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
- without the theory prefix, until $\isarkeyword{local}$ is declared again.
-
- Note that global names are prone to get hidden accidently later, when
- qualified names of the same base name are introduced.
-
-\item [$\isarkeyword{hide}~space~names$] fully removes declarations
- from a given name space (which may be $class$, $type$, $const$, or
- $fact$); with the $(open)$ option, only the base name is hidden.
- Global (unqualified) names may never be hidden.
-
- Note that hiding name space accesses has no impact on logical declarations
- -- they remain valid internally. Entities that are no longer accessible to
- the user are printed with the special qualifier ``$\mathord?\mathord?$''
- prefixed to the full internal name.
-\end{descr}
-
-
-\subsection{Incorporating ML code}\label{sec:ML}
-
-\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-val}\indexisarcmd{ML-command}
-\indexisarcmd{setup}\indexisarcmd{method-setup}
-\begin{matharray}{rcl}
- \isarcmd{use} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \isarcmd{ML} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \isarcmd{ML_val} & : & \isartrans{\cdot}{\cdot} \\
- \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
- \isarcmd{setup} & : & \isartrans{theory}{theory} \\
- \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'use' name
- ;
- ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
- ;
- 'method\_setup' name '=' text text
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{use}~file$] reads and executes ML commands from
- $file$. The current theory context is passed down to the ML
- toplevel and may be modified, using \verb,Context.>>, or any other
- ML commands derived from it. The file name is checked with the
- $\isarkeyword{uses}$ dependency declaration given in the theory
- header (see also \S\ref{sec:begin-thy}).
-
-\item [$\isarkeyword{ML}~text$] is similar to $\isarkeyword{use}$, but
- executes ML commands from the given $text$.
-
-\item [$\isarkeyword{ML_val}$ and $\isarkeyword{ML_command}$] are
- diagnostic versions of $\isarkeyword{ML}$, which means that the
- context may not be updated. $\isarkeyword{ML_val}$ echos the
- bindings produced at the ML toplevel, but $\isarkeyword{ML_command}$
- is silent.
-
-\item [$\isarkeyword{setup}~text$] changes the current theory context
- by applying $text$, which refers to an ML expression of type
- \texttt{theory~->~theory)}. The $\isarkeyword{setup}$ command is
- the canonical way to initialize any object-logic specific tools and
- packages written in ML.
-
-\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
- method in the current theory. The given $text$ has to be an ML expression
- of type \texttt{Args.src -> Proof.context -> Proof.method}. Parsing
- concrete method syntax from \texttt{Args.src} input can be quite tedious in
- general. The following simple examples are for methods without any explicit
- arguments, or a list of theorems, respectively.
-
-{\footnotesize
-\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
- Method.METHOD (fn facts => foobar_tac))
-\end{verbatim}
-}
-
-Note that mere tactic emulations may ignore the \texttt{facts} parameter
-above. Proper proof methods would do something appropriate with the list of
-current facts, though. Single-rule methods usually do strict forward-chaining
-(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just
-insert the facts using \texttt{Method.insert_tac} before applying the main
-tactic.
-\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}
-
-\railalias{parseasttranslation}{parse\_ast\_translation}
-\railterm{parseasttranslation}
-
-\railalias{parsetranslation}{parse\_translation}
-\railterm{parsetranslation}
-
-\railalias{printtranslation}{print\_translation}
-\railterm{printtranslation}
-
-\railalias{typedprinttranslation}{typed\_print\_translation}
-\railterm{typedprinttranslation}
-
-\railalias{printasttranslation}{print\_ast\_translation}
-\railterm{printasttranslation}
-
-\railalias{tokentranslation}{token\_translation}
-\railterm{tokentranslation}
-
-\begin{rail}
- ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
- printasttranslation ) ('(advanced)')? text;
-
- tokentranslation text
-\end{rail}
-
-Syntax translation functions written in ML admit almost arbitrary
-manipulations of Isabelle's inner syntax. Any of the above commands have a
-single \railqtok{text} argument that refers to an ML expression of appropriate
-type, which are as follows by default:
-
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-val token_translation :
- (string * string * (string -> string * real)) list
-\end{ttbox}
-
-In case that the $(advanced)$ option is given, the corresponding
-translation functions may depend on the current theory or proof
-context. This allows to implement advanced syntax mechanisms, as
-translations functions may refer to specific theory declarations or
-auxiliary proof data.
-
-See also \cite[\S8]{isabelle-ref} for more information on the general concept
-of syntax transformations in Isabelle.
-
-\begin{ttbox}
-val parse_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-val parse_translation:
- (string * (Context.generic -> term list -> term)) list
-val print_translation:
- (string * (Context.generic -> term list -> term)) list
-val typed_print_translation:
- (string * (Context.generic -> bool -> typ -> term list -> term)) list
-val print_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-\end{ttbox}
-
-
-\subsection{Oracles}
-
-\indexisarcmd{oracle}
-\begin{matharray}{rcl}
- \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-The oracle interface promotes a given ML function \texttt{theory -> T -> term}
-to \texttt{theory -> T -> thm}, for some type \texttt{T} given by the user.
-This acts like an infinitary specification of axioms -- there is no internal
-check of the correctness of the results! The inference kernel records oracle
-invocations within the internal derivation object of theorems, and the pretty
-printer attaches ``\texttt{[!]}'' to indicate results that are not fully
-checked by Isabelle inferences.
-
-\begin{rail}
- 'oracle' name '(' type ')' '=' text
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{oracle}~name~(type)=~text$] turns the given ML expression
- $text$ of type \texttt{theory~->~$type$~->~term} into an ML function $name$
- of type \texttt{theory~->~$type$~->~thm}.
-\end{descr}
-
-
-\section{Proof commands}
-
-Proof commands perform transitions of Isar/VM machine configurations, which
-are block-structured, consisting of a stack of nodes with three main
-components: logical proof context, current facts, and open goals. Isar/VM
-transitions are \emph{typed} according to the following three different modes
-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,
- and enter a sub-proof to establish the actual result.
-\item [$proof(state)$] is like a nested theory mode: the context may be
- augmented by \emph{stating} additional assumptions, intermediate results
- etc.
-\item [$proof(chain)$] is intermediate between $proof(state)$ and
- $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
- register) have been just picked up in order to be used when refining the
- goal claimed next.
-\end{descr}
-
-The proof mode indicator may be read as a verb telling the writer what kind of
-operation may be performed next. The corresponding typings of proof commands
-restricts the shape of well-formed proof texts to particular command
-sequences. So dynamic arrangements of commands eventually turn out as static
-texts of a certain structure. Appendix~\ref{ap:refcard} gives a simplified
-grammar of the overall (extensible) language emerging that way.
-
-
-\subsection{Markup commands}\label{sec:markup-prf}
-
-\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
-\indexisarcmd{txt}\indexisarcmd{txt-raw}
-\begin{matharray}{rcl}
- \isarcmd{sect} & : & \isartrans{proof}{proof} \\
- \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
- \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
- \isarcmd{txt} & : & \isartrans{proof}{proof} \\
- \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
-\end{matharray}
-
-These markup commands for proof mode closely correspond to the ones of theory
-mode (see \S\ref{sec:markup-thy}).
-
-\railalias{txtraw}{txt\_raw}
-\railterm{txtraw}
-
-\begin{rail}
- ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
- ;
-\end{rail}
-
-
-\subsection{Context elements}\label{sec:proof-context}
-
-\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
-\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)} \\
-\end{matharray}
-
-The logical proof context consists of fixed variables and assumptions. The
-former closely correspond to Skolem constants, or meta-level universal
-quantification as provided by the Isabelle/Pure logical framework.
-Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results
-in a local value that may be used in the subsequent proof as any other
-variable or constant. Furthermore, any result $\edrv \phi[x]$ exported from
-the context will be universally closed wrt.\ $x$ at the outermost level:
-$\edrv \All x \phi$ (this is expressed using Isabelle's meta-variables).
-
-Similarly, introducing some assumption $\chi$ has two effects. On the one
-hand, a local theorem is created that may be used as a fact in subsequent
-proof steps. On the other hand, any result $\chi \drv \phi$ exported from the
-context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
-Thus, solving an enclosing goal using such a result would basically introduce
-a new subgoal stemming from the assumption. How this situation is handled
-depends on the actual version of assumption command used: while $\ASSUMENAME$
-insists on solving the subgoal by unification with some premise of the goal,
-$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
-user.
-
-Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by
-combining ``$\FIX x$'' with another version of assumption that causes any
-hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
-Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
-
-\railalias{equiv}{\isasymequiv}
-\railterm{equiv}
-
-\begin{rail}
- 'fix' (vars + 'and')
- ;
- ('assume' | 'presume') (props + 'and')
- ;
- 'def' (def + 'and')
- ;
- def: thmdecl? \\ name ('==' | equiv) term termpat?
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
- $\vec x$.
-
-\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
- theorems $\vec\phi$ by assumption. Subsequent results applied to an
- enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
- expects to be able to unify with existing premises in the goal, while
- $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals.
-
- Several lists of assumptions may be given (separated by
- $\isarkeyword{and}$); the resulting list of current facts consists of all of
- these concatenated.
-
-\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
- In results exported from the context, $x$ is replaced by $t$. Basically,
- ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
- with the resulting hypothetical equation solved by reflexivity.
-
- The default name for the definitional equation is $x_def$. Several
- simultaneous definitions may be given at the same time.
-
-\end{descr}
-
-The special name $prems$\indexisarthm{prems} refers to all assumptions of the
-current context as a list of theorems.
-
-
-\subsection{Facts and forward chaining}
-
-\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
-\indexisarcmd{using}\indexisarcmd{unfolding}
-\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)} \\
- \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
- \isarcmd{unfolding} & : & \isartrans{proof(prove)}{proof(prove)} \\
-\end{matharray}
-
-New facts are established either by assumption or proof of local statements.
-Any fact will usually be involved in further proofs, either as explicit
-arguments of proof methods, or when forward chaining towards the next goal via
-$\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms
-involving $\NOTENAME$. The $\USINGNAME$ elements augments the collection of
-used facts \emph{after} a goal has been stated. Note that the special theorem
-name $this$\indexisarthm{this} refers to the most recently established facts,
-but only \emph{before} issuing a follow-up claim.
-
-\begin{rail}
- 'note' (thmdef? thmrefs + 'and')
- ;
- ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
- as $a$. Note that attributes may be involved as well, both on the left and
- right hand sides.
-
-\item [$\THEN$] indicates forward chaining by the current facts in order to
- establish the goal to be claimed next. The initial proof method invoked to
- refine that will be offered the facts to do ``anything appropriate'' (see
- also \S\ref{sec:proof-steps}). For example, method $rule$ (see
- \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
- introduction. Automatic methods usually insert the facts into the goal
- state before operation. This provides a simple scheme to control relevance
- of facts in automated proof search.
-
-\item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$
- is equivalent to ``$\FROM{this}$''.
-
-\item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
- forward chaining is from earlier facts together with the current ones.
-
-\item [$\USING{\vec b}$] augments the facts being currently indicated
- for use by a subsequent refinement step (such as $\APPLYNAME$ or
- $\PROOFNAME$).
-
-\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$,
- but unfolds definitional equations $\vec b$ throughout the goal
- state and facts.
-
-\end{descr}
-
-Forward chaining with an empty list of theorems is the same as not chaining at
-all. Thus ``$\FROM{nothing}$'' has no effect apart from entering
-$prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the
-empty list of theorems.
-
-Basic proof methods (such as $rule$) expect multiple facts to be given in
-their proper order, corresponding to a prefix of the premises of the rule
-involved. Note that positions may be easily skipped using something like
-$\FROM{\Text{\texttt{_}}~a~b}$, for example. This involves the trivial rule
-$\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as
-``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
-
-Automated methods (such as $simp$ or $auto$) just insert any given facts
-before their usual operation. Depending on the kind of procedure involved,
-the order of facts is less significant here.
-
-
-\subsection{Goal statements}\label{sec:goals}
-
-\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
-\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
-\indexisarcmd{print-statement}
-\begin{matharray}{rcl}
- \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
- \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
- \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
- \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
- \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
- \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\
-\end{matharray}
-
-From a theory context, proof mode is entered by an initial goal command such
-as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$. Within a proof, new
-claims may be introduced locally as well; four variants are available here to
-indicate whether forward chaining of facts should be performed initially (via
-$\THEN$), and whether the final result is meant to solve some pending goal.
-
-Goals may consist of multiple statements, resulting in a list of facts
-eventually. A pending multi-goal is internally represented as a meta-level
-conjunction (printed as \verb,&&,), which is usually split into the
-corresponding number of sub-goals prior to an initial method application, via
-$\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
-(\S\ref{sec:tactic-commands}). The $induct$ method covered in
-\S\ref{sec:cases-induct} acts on multiple claims simultaneously.
-
-Claims at the theory level may be either in short or long form. A
-short goal merely consists of several simultaneous propositions (often
-just one). A long goal includes an explicit context specification for
-the subsequent conclusion, involving local parameters and assumptions.
-Here the role of each part of the statement is explicitly marked by
-separate keywords (see also \S\ref{sec:locale}); the local assumptions
-being introduced here are available as $assms$\indexisarthm{assms} in
-the proof. \indexisarelem{shows}\indexisarelem{obtains}Moreover,
-there are two kinds of conclusions: $\isarkeyword{shows}$ states
-several simultaneous propositions (essentially a big conjunction),
-while $\isarkeyword{obtains}$ claims several simultaneous simultaneous
-contexts of (essentially a big disjunction of eliminated parameters
-and assumptions, cf.\ \S\ref{sec:obtain}).
-
-\begin{rail}
- ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
- ;
- ('have' | 'show' | 'hence' | 'thus') goal
- ;
- 'print\_statement' modes? thmrefs
- ;
-
- goal: (props + 'and')
- ;
- longgoal: thmdecl? (contextelem *) conclusion
- ;
- conclusion: 'shows' goal | 'obtains' (parname? case + '|')
- ;
- case: (vars + 'and') 'where' (props + 'and')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
- eventually resulting in some fact $\turn \vec\phi$ to be put back into the
- theory context, or into the specified locale (cf.\ \S\ref{sec:locale}). An
- additional \railnonterm{context} specification may build up an initial proof
- context for the subsequent claim; this includes local definitions and syntax
- as well, see the definition of $contextelem$ in \S\ref{sec:locale}.
-
-\item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
- the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
- being of a different kind. This discrimination acts like a formal comment.
-
-\item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a
- fact within the current logical context. This operation is completely
- independent of any pending sub-goals of an enclosing goal statements, so
- $\HAVENAME$ may be freely used for experimental exploration of potential
- results within a proof body.
-
-\item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage
- to refine some pending sub-goal for each one of the finished result, after
- having been exported into the corresponding context (at the head of the
- sub-proof of this $\SHOWNAME$ command).
-
- To accommodate interactive debugging, resulting rules are printed before
- being applied internally. Even more, interactive execution of $\SHOWNAME$
- predicts potential failure and displays the resulting error as a warning
- beforehand. Watch out for the following message:
-
- \begin{ttbox}
- Problem! Local statement will fail to solve any pending goal
- \end{ttbox}
-
-\item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local
- goal to be proven by forward chaining the current facts. Note that
- $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''.
-
-\item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''. Note that $\THUSNAME$
- is also equivalent to ``$\FROM{this}~\SHOWNAME$''.
-
-\item [$\isarkeyword{print_statement}~\vec a$] prints theorems from
- the current theory or proof context in long statement form,
- according to the syntax for $\isarkeyword{lemma}$ given above.
-
-\end{descr}
-
-Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
-be bound automatically, see also \S\ref{sec:term-abbrev}. Furthermore, the
-local context of a (non-atomic) goal is provided via the
-$rule_context$\indexisarcase{rule-context} case.
-
-The optional case names of $\isarkeyword{obtains}$ have a twofold
-meaning: (1) during the of this claim they refer to the the local
-context introductions, (2) the resulting rule is annotated accordingly
-to support symbolic case splits when used with the $cases$ method (cf.
-\S\ref{sec:cases-induct}).
-
-\medskip
-
-\begin{warn}
- Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound
- schematic variables}, although this does not conform to the aim of
- human-readable proof documents! The main problem with schematic goals is
- that the actual outcome is usually hard to predict, depending on the
- behavior of the proof methods applied during the course of reasoning. Note
- that most semi-automated methods heavily depend on several kinds of implicit
- rule declarations within the current theory context. As this would also
- result in non-compositional checking of sub-proofs, \emph{local goals} are
- not allowed to be schematic at all. Nevertheless, schematic goals do have
- their use in Prolog-style interactive synthesis of proven results, usually
- by stepwise refinement via emulation of traditional Isabelle tactic scripts
- (see also \S\ref{sec:tactic-commands}). In any case, users should know what
- they are doing.
-\end{warn}
-
-
-\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
-
-\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}
-
-Arbitrary goal refinement via tactics is considered harmful. Properly, the
-Isar framework admits proof methods to be invoked in two places only.
-\begin{enumerate}
-\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
- goal to a number of sub-goals that are to be solved later. Facts are passed
- to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
-
-\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
- remaining goals. No facts are passed to $m@2$.
-\end{enumerate}
-
-The only other (proper) way to affect pending goals in a proof body is by
-$\SHOWNAME$, which involves an explicit statement of what is to be solved
-eventually. Thus we avoid the fundamental problem of unstructured tactic
-scripts that consist of numerous consecutive goal transformations, with
-invisible effects.
-
-\medskip
-
-As a general rule of thumb for good proof style, initial proof methods should
-either solve the goal completely, or constitute some well-understood 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 an intelligible manner.
-
-Unless given explicitly by the user, the default initial method is ``$rule$'',
-which applies a single standard elimination or introduction rule according to
-the topmost symbol involved. There is no separate default terminal method.
-Any remaining goals are always solved by assumption in the very last step.
-
-\begin{rail}
- 'proof' method?
- ;
- 'qed' method?
- ;
- 'by' method method?
- ;
- ('.' | '..' | 'sorry')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
- forward chaining are passed if so indicated by $proof(chain)$ mode.
-
-\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
- concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or
- $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
- from the result \emph{exported} into the enclosing goal context. Thus
- $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
- rule does not fit to any pending goal\footnote{This includes any additional
- ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
- context. Debugging such a situation might involve temporarily changing
- $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
- occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
-
-\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
- abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both
- methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
- by expanding its definition; in many cases $\PROOF{m@1}$ (or even
- $\APPLY{m@1}$) is already sufficient to see the problem.
-
-\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
- abbreviates $\BY{rule}$.
-
-\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
- abbreviates $\BY{this}$.
-
-\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve
- the pending claim without further ado. This only works in interactive
- development, or if the \texttt{quick_and_dirty} flag is enabled. Facts
- emerging from fake proofs are not the real thing. Internally, each theorem
- container is tainted by an oracle invocation, which is indicated as
- ``$[!]$'' in the printed result.
-
- The most important application of $\SORRY$ is to support experimentation and
- top-down proof development.
-\end{descr}
-
-
-\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
-
-The following proof methods and attributes refer to basic logical operations
-of Isar. Further methods and attributes are provided by several generic and
-object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
-\ref{ch:logics}).
-
-\indexisarmeth{$-$}\indexisarmeth{fact}\indexisarmeth{assumption}
-\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{iprover}
-\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
-\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
-\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
-\begin{matharray}{rcl}
- - & : & \isarmeth \\
- fact & : & \isarmeth \\
- assumption & : & \isarmeth \\
- this & : & \isarmeth \\
- rule & : & \isarmeth \\
- iprover & : & \isarmeth \\[0.5ex]
- intro & : & \isaratt \\
- elim & : & \isaratt \\
- dest & : & \isaratt \\
- rule & : & \isaratt \\[0.5ex]
- OF & : & \isaratt \\
- of & : & \isaratt \\
- where & : & \isaratt \\
-\end{matharray}
-
-\begin{rail}
- 'fact' thmrefs?
- ;
- 'rule' thmrefs?
- ;
- 'iprover' ('!' ?) (rulemod *)
- ;
- rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
- ;
- ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
- ;
- 'rule' 'del'
- ;
- 'OF' thmrefs
- ;
- 'of' insts ('concl' ':' insts)?
- ;
- 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [``$-$''] does nothing but insert the forward chaining facts as premises
- into the goal. Note that command $\PROOFNAME$ without any method actually
- performs a single reduction step using the $rule$ method; thus a plain
- \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
- $\PROOFNAME$ alone.
-
-\item [$fact~\vec a$] composes any previous fact from $\vec a$ (or implicitly
- from the current proof context) modulo matching of schematic type and term
- variables. The rule structure is not taken into account, i.e.\ meta-level
- implication is considered atomic. This is the same principle underlying
- literal facts (cf.\ \S\ref{sec:syn-att}): ``$\HAVE{}{\phi}~\BY{fact}$'' is
- equivalent to ``$\NOTE{}{\backquote\phi\backquote}$'' provided that $\edrv
- \phi$ is an instance of some known $\edrv \phi$ in the proof context.
-
-\item [$assumption$] solves some goal by a single assumption step. All given
- facts are guaranteed to participate in the refinement; this means there may
- be only $0$ or $1$ in the first place. Recall that $\QEDNAME$ (see
- \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by
- assumption, so structured proofs usually need not quote the $assumption$
- method at all.
-
-\item [$this$] applies all of the current facts directly as rules. Recall
- that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''.
-
-\item [$rule~\vec a$] applies some rule given as argument in backward manner;
- facts are used to reduce the rule before applying it to the goal. Thus
- $rule$ without facts is plain introduction, while with facts it becomes
- elimination.
-
- When no arguments are given, the $rule$ method tries to pick appropriate
- rules automatically, as declared in the current context using the $intro$,
- $elim$, $dest$ attributes (see below). This is the default behavior of
- $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
- \S\ref{sec:proof-steps}).
-
-\item [$iprover$] performs intuitionistic proof search, depending on
- specifically declared rules from the context, or given as explicit
- arguments. Chained facts are inserted into the goal before commencing proof
- search; ``$iprover!$'' means to include the current $prems$ as well.
-
- Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
- indicator refers to ``safe'' rules, which may be applied aggressively
- (without considering back-tracking later). Rules declared with ``$?$'' are
- ignored in proof search (the single-step $rule$ method still observes
- these). An explicit weight annotation may be given as well; otherwise the
- number of rule premises will be taken into account here.
-
-\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
- destruct rules, to be used with the $rule$ and $iprover$ methods. Note that
- the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
- most aggressively.
-
- The classical reasoner (see \S\ref{sec:classical}) introduces its own
- variants of these attributes; use qualified names to access the present
- versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
-
-\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
-
-\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
- parallel). This corresponds to the \texttt{MRS} operator in ML
- \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
- effectively skipped by including ``$\_$'' (underscore) as argument.
-
-\item [$of~\vec t$] performs positional instantiation of term variables. The
- terms $\vec t$ are substituted for any schematic variables occurring in a
- theorem from left to right; ``\texttt{_}'' (underscore) indicates to skip a
- position. Arguments following a ``$concl\colon$'' specification refer to
- positions of the conclusion of a rule.
-
-\item [$where~\vec x = \vec t$] performs named instantiation of schematic type
- and term variables occurring in a theorem. Schematic variables have to be
- specified on the left-hand side (e.g.\ $?x1\!.\!3$). The question mark may
- be omitted if the variable name is a plain identifier without index. As
- type instantiations are inferred from term instantiations, explicit type
- instantiations are seldom necessary.
-
-\end{descr}
-
-
-\subsection{Term abbreviations}\label{sec:term-abbrev}
-
-\indexisarcmd{let}
-\begin{matharray}{rcl}
- \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
- \isarkeyword{is} & : & syntax \\
-\end{matharray}
-
-Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
-or by annotating assumptions or goal statements with a list of patterns
-``$\ISS{p@1\;\dots}{p@n}$''. In both cases, higher-order matching is invoked
-to bind extra-logical term variables, which may be either named schematic
-variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
-(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
-patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
-postfix position.
-
-Polymorphism of term bindings is handled in Hindley-Milner style, similar to
-ML. Type variables referring to local assumptions or open goal statements are
-\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
-in \emph{arbitrary} instances later. Even though actual polymorphism should
-be rarely used in practice, this mechanism is essential to achieve proper
-incremental type-inference, as the user proceeds to build up the Isar proof
-text from left to right.
-
-\medskip
-
-Term abbreviations are quite different from local definitions as introduced
-via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are visible within
-the logic as actual equations, while abbreviations disappear during the input
-process just after type checking. Also note that $\DEFNAME$ does not support
-polymorphism.
-
-\begin{rail}
- 'let' ((term + 'and') '=' term + 'and')
- ;
-\end{rail}
-
-The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
-\railnonterm{proppat} (see \S\ref{sec:term-decls}).
-
-\begin{descr}
-\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
- by simultaneous higher-order matching against terms $\vec t$.
-\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
- preceding statement. Also note that $\ISNAME$ is not a separate command,
- but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
-\end{descr}
-
-Some \emph{automatic} term abbreviations\index{term abbreviations} for goals
-and facts are available as well. For any open goal,
-$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement,
-abstracted over any meta-level parameters (if present). Likewise,
-$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from
-assumptions or finished goals. In case $\Var{this}$ refers to an object-logic
-statement that is an application $f(t)$, then $t$ is bound to the special text
-variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical
-application of the latter are calculational proofs (see
-\S\ref{sec:calculation}).
-
-
-\subsection{Block structure}
-
-\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
-\begin{matharray}{rcl}
- \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
- \BG & : & \isartrans{proof(state)}{proof(state)} \\
- \EN & : & \isartrans{proof(state)}{proof(state)} \\
-\end{matharray}
-
-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 may be switched via $\NEXT$, which is
-just a single block-close followed by block-open again. The effect of $\NEXT$
-is to reset the local proof context; there is no goal focus involved here!
-
-For slightly more advanced applications, there are explicit block parentheses
-as well. These typically achieve a stronger forward style of reasoning.
-
-\begin{descr}
-\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
- local context to the initial one.
-\item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts
- pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
- \emph{exported} into the enclosing context. Thus fixed variables are
- generalized, assumptions discharged, and local definitions unfolded (cf.\
- \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and
- $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
- backward reasoning with the result exported at $\SHOWNAME$ time.
-\end{descr}
-
-
-\subsection{Emulating tactic scripts}\label{sec:tactic-commands}
-
-The Isar provides separate commands to accommodate tactic-style proof scripts
-within the same system. While being outside the orthodox Isar proof language,
-these might come in handy for interactive exploration and debugging, or even
-actual tactical proof within new-style theories (to benefit from document
-preparation, for example). See also \S\ref{sec:tactics} for actual tactics,
-that have been encapsulated as proof methods. Proper proof methods may be
-used in scripts, too.
-
-\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done}
-\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
-\begin{matharray}{rcl}
- \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
- \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
- \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
- \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
- \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
- \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
-\end{matharray}
-
-\begin{rail}
- ( 'apply' | 'apply\_end' ) method
- ;
- 'defer' nat?
- ;
- 'prefer' nat
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
- $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method
- applications may be given just as in tactic scripts.
-
- Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
- are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would
- always work in a purely backward manner.
-
-\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
- terminal position. Basically, this simulates a multi-step tactic script for
- $\QEDNAME$, but may be given anywhere within the proof body.
-
- No facts are passed to $m$. Furthermore, the static context is that of the
- enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not
- refer to any assumptions introduced in the current body, for example.
-
-\item [$\isarkeyword{done}$] completes a proof script, provided that the
- current goal state is solved completely. Note that actual structured proof
- commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof
- scripts as well.
-
-\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list
- of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$
- by default), while $prefer$ brings goal $n$ to the top.
-
-\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
- the latest proof command. Basically, any proof command may return multiple
- results.
-
-\end{descr}
-
-Any proper Isar proof method may be used with tactic script commands such as
-$\APPLYNAME$. A few additional emulations of actual tactics are provided as
-well; these would be never used in actual structured proofs, of course.
-
-
-\subsection{Meta-linguistic features}
-
-\indexisarcmd{oops}
-\begin{matharray}{rcl}
- \isarcmd{oops} & : & \isartrans{proof}{theory} \\
-\end{matharray}
-
-The $\OOPS$ command discontinues the current proof attempt, while considering
-the partial proof text as properly processed. This is conceptually quite
-different from ``faking'' actual proofs via $\SORRY$ (see
-\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
-but goes back right to the theory level. Furthermore, $\OOPS$ does not
-produce any result theorem --- there is no intended claim to be able to
-complete the proof anyhow.
-
-A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
-system itself, in conjunction with the document preparation tools of Isabelle
-described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts
-can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX}
-macros can be easily adapted to print something like ``$\dots$'' instead of an
-``$\OOPS$'' keyword.
-
-\medskip The $\OOPS$ command is undo-able, unlike $\isarkeyword{kill}$ (see
-\S\ref{sec:history}). The effect is to get back to the theory just before the
-opening of the proof.
-
-
-\section{Other commands}
-
-\subsection{Diagnostics}
-
-\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}
-\indexisarcmd{prop}\indexisarcmd{typ}
-\begin{matharray}{rcl}
- \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
- \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
-\end{matharray}
-
-These diagnostic commands assist interactive development. Note that $undo$
-does not apply here, the theory or proof configuration is not changed.
-
-\begin{rail}
- 'pr' modes? nat? (',' nat)?
- ;
- 'thm' modes? thmrefs
- ;
- 'term' modes? term
- ;
- 'prop' modes? prop
- ;
- 'typ' modes? type
- ;
- 'prf' modes? thmrefs?
- ;
- 'full\_prf' modes? thmrefs?
- ;
-
- modes: '(' (name + ) ')'
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if
- present), including the proof context, current facts and goals. The
- optional limit arguments affect the number of goals and premises to be
- displayed, which is initially 10 for both. Omitting limit values leaves the
- current setting unchanged.
-\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
- or proof context. Note that any attributes included in the theorem
- specifications are applied to a temporary context derived from the current
- theory or proof; the result is discarded, i.e.\ attributes involved in $\vec
- a$ do not have any permanent effect.
-\item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check
- and print terms or propositions according to the current theory or proof
- context; the inferred type of $t$ is output as well. Note that these
- commands are also useful in inspecting the current environment of term
- abbreviations.
-\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
- according to the current theory or proof context.
-\item [$\isarkeyword{prf}$] displays the (compact) proof term of the current
- proof state (if present), or of the given theorems. Note that this
- requires proof terms to be switched on for the current object logic
- (see the ``Proof terms'' section of the Isabelle reference manual
- for information on how to do this).
-\item [$\isarkeyword{full_prf}$] is like $\isarkeyword{prf}$, but displays
- the full proof term, i.e.\ also displays information omitted in
- the compact proof term, which is denoted by ``$_$'' placeholders there.
-\end{descr}
-
-All of the diagnostic commands above admit a list of $modes$ to be specified,
-which is appended to the current print mode (see also \cite{isabelle-ref}).
-Thus the output behavior may be modified according particular print mode
-features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would
-print the current proof state with mathematical symbols and special characters
-represented in {\LaTeX} source, according to the Isabelle style
-\cite{isabelle-sys}.
-
-Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic
-way to include formal items into the printed text document.
-
-
-\subsection{Inspecting the context}
-
-\indexisarcmd{print-facts}\indexisarcmd{print-binds}
-\indexisarcmd{print-commands}\indexisarcmd{print-syntax}
-\indexisarcmd{print-methods}\indexisarcmd{print-attributes}
-\indexisarcmd{find-theorems}\indexisarcmd{thm-deps}
-\indexisarcmd{print-theorems}\indexisarcmd{print-theory}
-\begin{matharray}{rcl}
- \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
- \isarcmd{print_theory}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{find_theorems}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
- \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
- \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
-\end{matharray}
-
-\begin{rail}
- 'print\_theory' ( '!'?)
- ;
-
- 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
- ;
- criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
- 'simp' ':' term | term)
- ;
- 'thm\_deps' thmrefs
- ;
-\end{rail}
-
-These commands print certain parts of the theory and proof context. Note that
-there are some further ones available, such as for the set of rules declared
-for simplifications.
-
-\begin{descr}
-
-\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
- including keywords and command.
-
-\item [$\isarkeyword{print_theory}$] prints the main logical content
- of the theory context; the ``$!$'' option indicates extra verbosity.
-
-\item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
- terms, depending on the current context. The output can be very verbose,
- including grammar tables and syntax translation rules. See \cite[\S7,
- \S8]{isabelle-ref} for further information on Isabelle's inner syntax.
-
-\item [$\isarkeyword{print_methods}$] prints all proof methods available in
- the current theory context.
-
-\item [$\isarkeyword{print_attributes}$] prints all attributes available in
- the current theory context.
-
-\item [$\isarkeyword{print_theorems}$] prints theorems available in the
- current theory context.
-
- In interactive mode this actually refers to the theorems left by the last
- transaction; this allows to inspect the result of advanced definitional
- packages, such as $\isarkeyword{datatype}$.
-
-\item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory
- or proof context matching all of the search criteria $\vec c$. The
- criterion $name: p$ selects all theorems whose fully qualified name matches
- pattern $p$, which may contain ``$*$'' wildcards. The criteria $intro$,
- $elim$, and $dest$ select theorems that match the current goal as
- introduction, elimination or destruction rules, respectively. The criterion
- $simp: t$ selects all rewrite rules whose left-hand side matches the given
- term. The criterion term $t$ selects all theorems that contain the pattern
- $t$ -- as usual, patterns may contain occurrences of the dummy ``$\_$'',
- schematic variables, and type constraints.
-
- Criteria can be preceded by ``$-$'' to select theorems that do \emph{not}
- match. Note that giving the empty list of criteria yields \emph{all}
- currently known facts. An optional limit for the number of printed facts
- may be given; the default is 40. Per default, duplicates are removed from
- the search result. Use $\isarkeyword{with_dups}$ to display duplicates.
-
-\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
- using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
-
-\item [$\isarkeyword{print_facts}$] prints all local facts of the
- current context, both named and unnamed ones.
-
-\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
- the context.
-
-\end{descr}
-
-
-\subsection{History commands}\label{sec:history}
-
-\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill}
-\begin{matharray}{rcl}
- \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\
- \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\
- \isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\
-\end{matharray}
-
-The Isabelle/Isar top-level maintains a two-stage history, for theory and
-proof state transformation. Basically, any command can be undone using
-$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be
-revoked via $\isarkeyword{redo}$, unless the corresponding
-$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The
-$\isarkeyword{kill}$ command aborts the current history node altogether,
-discontinuing a proof or even the whole theory. This operation is \emph{not}
-undo-able.
-
-\begin{warn}
- History commands should never be used with user interfaces such as
- Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of
- stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$,
- $\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly
- result in utter confusion.
-\end{warn}
-
-
-\subsection{System operations}
-
-\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{update-thy}
-\indexisarcmd{display-drafts}\indexisarcmd{print-drafts}
-\begin{matharray}{rcl}
- \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
- \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
- \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\
- \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
- \isarcmd{display_drafts}^* & : & \isarkeep{\cdot} \\
- \isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\
-\end{matharray}
-
-\begin{rail}
- ('cd' | 'use\_thy' | 'update\_thy') name
- ;
- ('display\_drafts' | 'print\_drafts') (name +)
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\isarkeyword{cd}~path$] changes the current directory of the Isabelle
- process.
-\item [$\isarkeyword{pwd}~$] prints the current working directory.
-\item [$\isarkeyword{use_thy}$ and $\isarkeyword{update_thy}$] preload
- some theory given as $name$ argument. These system commands are
- scarcely used when working interactively, since loading of theories
- is done transparently.
-\item [$\isarkeyword{display_drafts}~paths$ and
- $\isarkeyword{print_drafts}~paths$] perform simple output of a given list of
- raw source files. Only those symbols that do not require additional
- {\LaTeX} packages are displayed properly, everything else is left verbatim.
-\end{descr}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End:
--- a/doc-src/IsarRef/style.sty Fri May 02 16:32:51 2008 +0200
+++ b/doc-src/IsarRef/style.sty Fri May 02 16:36:05 2008 +0200
@@ -36,9 +36,7 @@
\newcommand{\isasymGUESS}{\isakeyword{guess}}
\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymBEGIN}{\isakeyword{begin}}
\newcommand{\isasymEND}{\isakeyword{end}}
\newcommand{\isasymCONSTS}{\isakeyword{consts}}
\newcommand{\isasymDEFS}{\isakeyword{defs}}