
wenzelm@7046: 
wenzelm@7315: \chapter{Basic Isar elements}\label{ch:pure-syntax}
wenzelm@7167: 
wenzelm@7315: Subsequently, we introduce the main part of the basic Isar theory and proof
wenzelm@7315: commands as provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes
wenzelm@7315: further Isar elements as provided by generic tools and packages that are
wenzelm@7315: either part of Pure Isabelle, or pre-loaded by most object logics (such as the
wenzelm@7315: Simplifier).  See chapter~\ref{ch:hol-tools} for actual object-logic specific
wenzelm@7315: elements (for Isabelle/HOL).
wenzelm@7046: 
wenzelm@7167: \medskip
wenzelm@7167: 
wenzelm@7167: Isar commands may be either \emph{proper} document constructors, or
wenzelm@7175: \emph{improper commands} (indicated by $^*$).  Some proof methods and
wenzelm@7175: attributes introduced later may be classified as improper as well.  Improper
wenzelm@7175: Isar language elements might be helpful when developing proof documents, while
wenzelm@7175: their use is strongly discouraged for the final version.  Typical examples are
wenzelm@7175: diagnostic commands that print terms or theorems according to the current
wenzelm@7175: context; other commands even emulate old-style tactical theorem proving, which
wenzelm@7175: facilitates porting of legacy proof scripts.
wenzelm@7167: 
wenzelm@7134: 
wenzelm@7134: \section{Theory commands}
wenzelm@7134: 
wenzelm@7167: \subsection{Defining theories}\label{sec:begin-thy}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
wenzelm@7134:   \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
wenzelm@7134:   \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: Isabelle/Isar ``new-style'' theories are either defined via theory files or
wenzelm@7167: interactively.  Both actual theory specifications and proofs are handled
wenzelm@7175: uniformly --- occasionally definitional mechanisms even require some manual
wenzelm@7175: proof.  In contrast, ``old-style'' Isabelle theories support batch processing
wenzelm@7175: only, with the proof scripts collected in separate ML files.
wenzelm@7134: 
wenzelm@7134: The first command of any theory has to be $\THEORY$, starting a new theory
wenzelm@7175: based on the merge of existing ones.  The theory context may be also changed
wenzelm@7175: by $\CONTEXT$ without creating a new theory.  In both cases, $\END$ concludes
wenzelm@7175: the theory development; it has to be the very last command of any proper
wenzelm@7175: theory file.
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'theory' name '=' (name + '+') filespecs? ':'
wenzelm@7134:   ;
wenzelm@7134:   'context' name
wenzelm@7134:   ;
wenzelm@7134:   'end'
wenzelm@7134:   ;;
wenzelm@7134: 
wenzelm@7167:   filespecs: 'files' ((name | parname) +);
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
wenzelm@7175:   existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader system ensures
wenzelm@7175:   that any of the base theories are properly loaded (and fully up-to-date when
wenzelm@7175:   $\THEORY$ is executed interactively).  The optional $\isarkeyword{files}$
wenzelm@7175:   specification declares additional dependencies on ML files.  Unless put in
wenzelm@7175:   parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see
wenzelm@7175:   also \S\ref{sec:ML}).
wenzelm@7134:   
wenzelm@7167: \item [$\CONTEXT~B$] enters an existing theory context $B$, basically in
wenzelm@7134:   read-only mode, so only a limited set of commands may be performed.  Just as
wenzelm@7134:   for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
wenzelm@7175:   
wenzelm@7167: \item [$\END$] concludes the current theory definition or context switch.
wenzelm@7175:   Note that this command cannot be undone, instead the theory definition
wenzelm@7175:   itself has to be retracted.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Formal comments}\label{sec:formal-cmt-thy}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
wenzelm@7167: \indexisarcmd{subsubsection}\indexisarcmd{text}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{title} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
wenzelm@7167:   \isarcmd{section} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{text} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7167: There are several commands to include \emph{formal comments} in theory
wenzelm@7167: specification (a few more are available for proofs, see
wenzelm@7167: \S\ref{sec:formal-cmt-prf}).  In contrast to source-level comments
wenzelm@7134: \verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
wenzelm@7134: given as formal comment is meant to be part of the actual document.
wenzelm@7134: Consequently, it would be included in the final printed version.
wenzelm@7134: 
wenzelm@7134: Apart from plain prose, formal comments may also refer to logical entities of
wenzelm@7175: the theory context (types, terms, theorems etc.).  Proper processing of the
wenzelm@7175: text would then include some further consistency checks with the items
wenzelm@7175: declared in the current theory, e.g.\ type-checking of included
wenzelm@7175: terms.\footnote{The current version of Isabelle/Isar does not process formal
wenzelm@7134:   comments in any such way.  This will be available as part of the automatic
wenzelm@7175:   theory and proof document preparation system (using (PDF){\LaTeX}) that is
wenzelm@7134:   planned for the near future.}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'title' text text? text?
wenzelm@7134:   ;
wenzelm@7167:   ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\isarkeyword{title}~title~author~date$] specifies the document title
wenzelm@7175:   just as in typical {\LaTeX} documents.
wenzelm@7167: \item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,
wenzelm@7175:   $\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$]
wenzelm@7315:   mark chapter and section headings.
wenzelm@7134: \item [$\TEXT~text$] specifies an actual body of prose text, including
wenzelm@7315:   references to formal entities.\footnote{The latter feature is not yet
wenzelm@7315:     exploited.  Nevertheless, any text of the form \texttt{\at\{\dots\}}
wenzelm@7315:     should be considered as reserved for future use.}
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7135: \subsection{Type classes and sorts}\label{sec:classes}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{classes} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7167:   'classes' (classdecl comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'classrel' nameref '<' nameref comment?
wenzelm@7134:   ;
wenzelm@7134:   'defaultsort' sort comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{classes}~c<\vec c ~\dots$] declares class $c$ to be a
wenzelm@7175:   subclass of existing classes $\vec c$.  Cyclic class structures are ruled
wenzelm@7175:   out.
wenzelm@7134: \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
wenzelm@7134:   existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
wenzelm@7175:   $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way
wenzelm@7175:   introduce proven class relations.
wenzelm@7134: \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
wenzelm@7175:   any type variables input without sort constraints.  Usually, the default
wenzelm@7134:   sort would be only changed when defining new logics.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7315: \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{types} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{arities} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'types' (typespec '=' type infix? comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'typedecl' typespec infix? comment?
wenzelm@7134:   ;
wenzelm@7134:   'nonterminals' (name +) comment?
wenzelm@7134:   ;
wenzelm@7134:   'arities' (nameref '::' arity comment? +)
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym}
wenzelm@7134:   $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
wenzelm@7134:   as are available in Isabelle/HOL for example, type synonyms are just purely
wenzelm@7134:   syntactic abbreviations, without any logical significance.  Internally, type
wenzelm@7134:   synonyms are fully expanded, as may be observed when printing terms or
wenzelm@7134:   theorems.
wenzelm@7134: \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
wenzelm@7134:   $t$, intended as an actual logical type.  Note that some logics such as
wenzelm@7134:   Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
wenzelm@7175: \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm@7175:   $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm@7175:   Isabelle's inner syntax of terms or types.
wenzelm@7134: \item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's
wenzelm@7134:   order-sorted signature of types by new type constructor arities.  This is
wenzelm@7175:   done axiomatically!  The $\isarkeyword{instance}$ command (see
wenzelm@7175:   \S\ref{sec:axclass}) provides a way introduce proven type arities.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{Constants and simple definitions}
wenzelm@7134: 
wenzelm@7175: \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{defs} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'consts' (constdecl +)
wenzelm@7134:   ;
wenzelm@7134:   'defs' (thmdecl? prop comment? +)
wenzelm@7134:   ;
wenzelm@7134:   'constdefs' (constdecl prop comment? +)
wenzelm@7134:   ;
wenzelm@7134: 
wenzelm@7134:   constdecl: name '::' type mixfix? comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\CONSTS~c::\sigma~\dots$] declares constant $c$ to have any instance
wenzelm@7175:   of type scheme $\sigma$.  The optional mixfix annotations may attach
wenzelm@7175:   concrete syntax constants.
wenzelm@7134: \item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for
wenzelm@7134:   some existing constant.  See \cite[\S6]{isabelle-ref} for more details on
wenzelm@7134:   the form of equations admitted as constant definitions.
wenzelm@7175: \item [$\isarkeyword{constdefs}~c::\sigma~eqn~\dots$] combines constant
wenzelm@7134:   declarations and definitions, using canonical name $c_def$ for the
wenzelm@7134:   definitional axiom.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Syntax and translations}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{syntax}\indexisarcmd{translations}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{translations} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'syntax' ('(' name 'output'? ')')? (constdecl +)
wenzelm@7134:   ;
wenzelm@7134:   'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
wenzelm@7134:   ;
wenzelm@7134:   transpat: ('(' nameref ')')? string
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm@7175:   except that the actual logical signature extension is omitted.  Thus the
wenzelm@7175:   context free grammar of Isabelle's inner syntax may be augmented in
wenzelm@7175:   arbitrary ways.  The $mode$ argument refers to the print mode that the
wenzelm@7175:   grammar rules belong; unless there is the \texttt{output} flag given, all
wenzelm@7175:   productions are added both to the input and output grammar.
wenzelm@7175: \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
wenzelm@7175:   rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse
wenzelm@7175:   rules (\texttt{=>}), print rules (\texttt{<=}).  Translation patterns may be
wenzelm@7134:   prefixed by the syntactic category to be used for parsing; the default is
wenzelm@7134:   \texttt{logic}.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{Axioms and theorems}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7135:   'axioms' (axmdecl prop comment? +)
wenzelm@7134:   ;
wenzelm@7134:   ('theorems' | 'lemmas') thmdef? thmrefs
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary
wenzelm@7134:   statements as logical axioms.  In fact, axioms are ``axiomatic theorems'',
wenzelm@7175:   and may be referred just as any other theorem later.
wenzelm@7134:   
wenzelm@7134:   Axioms are usually only introduced when declaring new logical systems.
wenzelm@7175:   Everyday work is typically done the hard way, with proper definitions and
wenzelm@7134:   actual theorems.
wenzelm@7134: \item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems
wenzelm@7175:   as $name$.  Typical applications would also involve attributes (to augment
wenzelm@7175:   the default simpset, for example).
wenzelm@7134: \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
wenzelm@7134:   tags the results as ``lemma''.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Name spaces}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{global}\indexisarcmd{local}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{global} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{local} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7315: Isabelle organises any kind of names (of types, constants, theorems etc.)  by
wenzelm@7175: hierarchically structured name spaces.  Normally the user never has to control
wenzelm@7315: the behaviour of name space entry by hand, yet the following commands provide
wenzelm@7175: some way to do so.
wenzelm@7175: 
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm@7167:   name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm@7167:   mode, causing all names to be automatically qualified by the theory name.
wenzelm@7167:   Changing this to $\isarkeyword{global}$ causes all names to be declared as
wenzelm@7175:   base names only, until $\isarkeyword{local}$ is declared again.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Incorporating ML code}\label{sec:ML}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134:   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7175:   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'use' name
wenzelm@7134:   ;
wenzelm@7134:   'ML' text
wenzelm@7134:   ;
wenzelm@7134:   'setup' text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
wenzelm@7175:   The current theory context (if present) is passed down to the ML session.
wenzelm@7175:   Furthermore, the file name is checked with the $\isarkeyword{files}$
wenzelm@7175:   dependency declaration given in the theory header (see also
wenzelm@7175:   \S\ref{sec:begin-thy}).
wenzelm@7175: \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
wenzelm@7175:   The theory context is passed just as for $\isarkeyword{use}$.
wenzelm@7167: \item [$\isarkeyword{setup}~text$] changes the current theory context by
wenzelm@7175:   applying setup functions $text$, which has to be an ML expression of type
wenzelm@7175:   $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the usual
wenzelm@7315:   way to initialise object-logic specific tools and packages written in ML.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7167: \subsection{Syntax translation functions}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
wenzelm@7167: \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
wenzelm@7167: \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134:   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: Syntax translation functions written in ML admit almost arbitrary
wenzelm@7134: manipulations of Isabelle's inner syntax.  Any of the above commands have a
wenzelm@7134: single \railqtoken{text} argument that refers to an ML expression of
wenzelm@7134: appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
wenzelm@7134: transformations.
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{Oracles}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{oracle}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7175: Oracles provide an interface to external reasoning systems, without giving up
wenzelm@7175: control completely --- each theorem carries a derivation object recording any
wenzelm@7175: oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'oracle' name '=' text comment?
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
wenzelm@7315:   function $text$, which has to be of type $Sign\mathord.sg \times
wenzelm@7315:   Object\mathord.T \to term)$.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \section{Proof commands}
wenzelm@7134: 
wenzelm@7315: Proof commands provide transitions of Isar/VM machine configurations, which
wenzelm@7315: are block-structured, consisting of a stack of nodes with three main
wenzelm@7315: components: logical \emph{proof context}, local \emph{facts}, and open
wenzelm@7315: \emph{goals}.  Isar/VM transitions are \emph{typed} according to the following
wenzelm@7315: three three different modes of operation:
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$proof(prove)$] means that a new goal has just been stated that is now
wenzelm@7167:   to be \emph{proven}; the next command may refine it by some proof method
wenzelm@7175:   ($\approx$ tactic), and enter a sub-proof to establish the final result.
wenzelm@7167: \item [$proof(state)$] is like an internal theory mode: the context may be
wenzelm@7175:   augmented by \emph{stating} additional assumptions, intermediate result etc.
wenzelm@7175: \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
wenzelm@7315:   $proof(prove)$: existing facts have been just picked up in order to use them
wenzelm@7315:   when refining the goal to be claimed next.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7167: 
wenzelm@7167: \subsection{Formal comments}\label{sec:formal-cmt-prf}
wenzelm@7167: 
wenzelm@7167: \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7167:   \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167:   \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167:   \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167:   \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7175: These formal comments in proof mode closely correspond to the ones of theory
wenzelm@7175: mode (see \S\ref{sec:formal-cmt-thy}).
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7167:   ('sect' | 'subsect' | 'subsubsect' | 'txt') text
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7315: \subsection{Proof context}\label{sec:proof-context}
wenzelm@7134: 
wenzelm@7315: \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7315: The logical proof context consists of fixed variables and assumptions.  The
wenzelm@7315: former closely correspond to Skolem constants, or meta-level universal
wenzelm@7315: quantification as provided by the Isabelle/Pure logical framework.
wenzelm@7315: Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
wenzelm@7315: a local entity that may be used in the subsequent proof as any other variable
wenzelm@7315: or constant.  Furthermore, any result $\phi[x]$ exported from the current
wenzelm@7315: context will be universally closed wrt.\ $x$ at the outermost level (this is
wenzelm@7315: expressed using Isabelle's meta-variables).
wenzelm@7315: 
wenzelm@7315: Similarly, introducing some assumption $\chi$ has two effects.  On the one
wenzelm@7315: hand, a local theorem is created that may be used as a fact in subsequent
wenzelm@7315: proof steps.  On the other hand, any result $\phi$ exported from the context
wenzelm@7315: becomes conditional wrt.\ the assumption.  Thus, solving an enclosing goal
wenzelm@7315: using this result would basically introduce a new subgoal stemming from the
wenzelm@7315: assumption.  How this situation is handled depends on the actual version of
wenzelm@7315: assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying
wenzelm@7315: with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to
wenzelm@7315: be proved later by the user.
wenzelm@7315: 
wenzelm@7315: Local definitions, introduced by $\DEF{a}{x \equiv t}$, are achieved by
wenzelm@7315: combining $\FIX x$ with another version of assumption that causes any
wenzelm@7315: hypothetical equation $x = t$ to be eliminated by reflexivity.  Thus,
wenzelm@7315: exporting some result $\phi[x]$ simply yields $\phi[t]$.
wenzelm@7175: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'fix' (var +) comment?
wenzelm@7134:   ;
wenzelm@7315:   ('assume' | 'presume') (assm comment? + 'and')
wenzelm@7134:   ;
wenzelm@7175:   'def' thmdecl? \\ var '==' term termpat? comment?
wenzelm@7134:   ;
wenzelm@7134: 
wenzelm@7134:   var: name ('::' type)?
wenzelm@7134:   ;
wenzelm@7315:   assm: thmdecl? (prop proppat? +)
wenzelm@7315:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7315: \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
wenzelm@7315: \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
wenzelm@7315:   $\Phi$.  Subsequent results used to solve some enclosing goal (e.g.\ via
wenzelm@7315:   $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be able to
wenzelm@7315:   unify with existing premises in the goal, while $\PRESUMENAME$ leaves $\Phi$
wenzelm@7315:   as new subgoals.  Note that several lists of assumptions may be given
wenzelm@7315:   (separated by \railterm{and}); the resulting list of current facts consists
wenzelm@7315:   of all of these.
wenzelm@7315: \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
wenzelm@7315:   In results exported from the context, $x$ is replaced by $t$.  Basically,
wenzelm@7315:   $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$ (the
wenzelm@7315:   resulting hypothetical equation is solved by reflexivity, though).
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7315: The internal register $prems$\indexisarreg{prems} refers to all current
wenzelm@7315: assumptions as a list of theorems.
wenzelm@7315: 
wenzelm@7167: 
wenzelm@7167: \subsection{Facts and forward chaining}
wenzelm@7167: 
wenzelm@7167: \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm@7167: \begin{matharray}{rcl}
wenzelm@7167:   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167:   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167:   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167:   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167: \end{matharray}
wenzelm@7167: 
wenzelm@7315: New facts are established either by assumption or proof of local statements
wenzelm@7315: (via $\HAVENAME$ or $\SHOWNAME$).  Any facts will usually be involved in
wenzelm@7315: proofs of further results: either as explicit arguments of proof methods or
wenzelm@7315: when forward chaining towards the next goal via $\THEN$ (and variants).
wenzelm@7175: 
wenzelm@7167: \begin{rail}
wenzelm@7167:   'note' thmdef? thmrefs comment?
wenzelm@7167:   ;
wenzelm@7167:   'then' comment?
wenzelm@7167:   ;
wenzelm@7167:   ('from' | 'with') thmrefs comment?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm@7175:   as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm@7175:   right hand sides.
wenzelm@7167: \item [$\THEN$] indicates forward chaining by the current facts in order to
wenzelm@7175:   establish the goal to be claimed next.  The initial proof method invoked to
wenzelm@7175:   solve that will be offered these facts to do ``anything appropriate'' (see
wenzelm@7175:   also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
wenzelm@7167:   \S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
wenzelm@7175: \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; also note that
wenzelm@7167:   $\THEN$ is equivalent to $\FROM{facts}$.
wenzelm@7175: \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
wenzelm@7175:   chaining is from earlier facts together with the current ones.
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7315: Note that the internal register of \emph{current facts} may be referred as
wenzelm@7315: theorem list $facts$.\indexisarreg{facts}
wenzelm@7315: 
wenzelm@7167: 
wenzelm@7167: \subsection{Goal statements}
wenzelm@7167: 
wenzelm@7167: \indexisarcmd{theorem}\indexisarcmd{lemma}
wenzelm@7167: \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm@7167: \begin{matharray}{rcl}
wenzelm@7167:   \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167:   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167:   \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167:   \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167:   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167:   \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167: \end{matharray}
wenzelm@7167: 
wenzelm@7175: Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
wenzelm@7175: and $\LEMMANAME$.  New local goals may be claimed within proof mode: four
wenzelm@7175: variants are available, indicating whether the result is meant to solve some
wenzelm@7175: pending goal and whether forward chaining is employed.
wenzelm@7175: 
wenzelm@7167: \begin{rail}
wenzelm@7167:   ('theorem' | 'lemma') goal
wenzelm@7167:   ;
wenzelm@7167:   ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@7167:   ;
wenzelm@7167: 
wenzelm@7167:   goal: thmdecl? proppat comment?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
wenzelm@7175:   eventually resulting in some theorem $\turn \phi$, which will be stored in
wenzelm@7175:   the theory.
wenzelm@7167: \item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
wenzelm@7167:   ``lemma''.
wenzelm@7167: \item [$\HAVE{name}{\phi}$] claims a local goal, eventually resulting in a
wenzelm@7167:   theorem with the current assumption context as hypotheses.
wenzelm@7175: \item [$\SHOW{name}{\phi}$] is similar to $\HAVE{name}{\phi}$, but solves some
wenzelm@7175:   pending goal with the result \emph{exported} into the corresponding context.
wenzelm@7167: \item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\ 
wenzelm@7167:   claims a local goal to be proven by forward chaining the current facts.
wenzelm@7167: \item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$.
wenzelm@7167: \end{descr}
wenzelm@7167: 
wenzelm@7167: 
wenzelm@7167: \subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm@7167: 
wenzelm@7175: \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm@7175: \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm@7175: \begin{matharray}{rcl}
wenzelm@7175:   \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@7175:   \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175:   \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175: \end{matharray}
wenzelm@7175: 
wenzelm@7167: Arbitrary goal refinements via tactics is considered harmful.  Consequently
wenzelm@7167: the Isar framework admits proof methods to be invoked in two places only.
wenzelm@7167: \begin{enumerate}
wenzelm@7175: \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
wenzelm@7175:   intermediate goal to a number of sub-goals that are to be solved later.
wenzelm@7175:   Facts are passed to $m@1$ for forward chaining if so indicated by
wenzelm@7175:   $proof(chain)$ mode.
wenzelm@7167:   
wenzelm@7175: \item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining
wenzelm@7167:   pending goals completely.  No facts are passed to $m@2$.
wenzelm@7167: \end{enumerate}
wenzelm@7167: 
wenzelm@7167: The only other proper way to affect pending goals is by $\SHOWNAME$, which
wenzelm@7167: involves an explicit statement of what is solved.
wenzelm@7167: 
wenzelm@7175: \medskip
wenzelm@7175: 
wenzelm@7167: Also note that initial proof methods should either solve the goal completely,
wenzelm@7167: or constitute some well-understood deterministic reduction to new sub-goals.
wenzelm@7167: Arbitrary automatic proof tools that are prone leave a large number of badly
wenzelm@7167: structured sub-goals are no help in continuing the proof document in any
wenzelm@7175: intelligible way.  A much better technique would be to $\SHOWNAME$ some
wenzelm@7175: non-trivial reduction as an explicit rule, which is solved completely by some
wenzelm@7175: automated method, and then applied to some pending goal.
wenzelm@7167: 
wenzelm@7175: \medskip
wenzelm@7175: 
wenzelm@7175: Unless given explicitly by the user, the default initial method is
wenzelm@7175: ``$default$'', which is usually set up to apply a single standard elimination
wenzelm@7175: or introduction rule according to the topmost symbol involved.  The default
wenzelm@7175: terminal method is ``$finish$''; it solves all goals by assumption.
wenzelm@7167: 
wenzelm@7167: \begin{rail}
wenzelm@7167:   'proof' interest? meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   'qed' meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   'by' meth meth? comment?
wenzelm@7167:   ;
wenzelm@7167:   ('.' | '..' | 'sorry') comment?
wenzelm@7167:   ;
wenzelm@7167: 
wenzelm@7167:   meth: method interest?
wenzelm@7167:   ;
wenzelm@7167: \end{rail}
wenzelm@7167: 
wenzelm@7167: \begin{descr}
wenzelm@7175: \item [$\PROOF{m@1}$] refines the pending goal by proof method $m@1$; facts
wenzelm@7175:   for forward chaining are passed if so indicated by $proof(chain)$.
wenzelm@7175: \item [$\QED{m@2}$] refines any remaining goals by proof method $m@1$ and
wenzelm@7167:   concludes the sub-proof.  If the goal had been $\SHOWNAME$, some pending
wenzelm@7167:   sub-goal is solved as well by the rule resulting from the result exported to
wenzelm@7175:   the enclosing goal context.  Thus $\QEDNAME$ may fail for two reasons:
wenzelm@7175:   either $m@2$ fails to solve all remaining goals completely, or the resulting
wenzelm@7175:   rule does not resolve with any enclosing goal.  Debugging such a situation
wenzelm@7175:   might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$, or
wenzelm@7175:   weakening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$.
wenzelm@7175: \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates
wenzelm@7175:   $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods.
wenzelm@7175:   Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
wenzelm@7175:   expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
wenzelm@7175:   sufficient to see what is going wrong.
wenzelm@7175: \item [$\DDOT$] is a \emph{default proof}; it abbreviates $\BY{default}$.
wenzelm@7175: \item [$\DOT$] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
wenzelm@7175:   method ``$-$'' does nothing except inserting any facts into the proof state.
wenzelm@7167: \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
wenzelm@7167:   \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
wenzelm@7167:   the goal without much ado.  Of course, the result is a fake theorem only,
wenzelm@7175:   involving some oracle in its internal derivation object (this is indicated
wenzelm@7175:   as $[!]$ in the printed result.  The main application of
wenzelm@7167:   $\isarkeyword{sorry}$ is to support top-down proof development.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7315: \subsection{Improper proof steps}
wenzelm@7315: 
wenzelm@7315: The following commands emulate unstructured tactic scripts to some extent.
wenzelm@7315: While these are anathema for writing proper Isar proof documents, they might
wenzelm@7315: come in handy for exploring and debugging.
wenzelm@7315: 
wenzelm@7315: \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
wenzelm@7315: \begin{matharray}{rcl}
wenzelm@7315:   \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315:   \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315:   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315: \end{matharray}
wenzelm@7315: 
wenzelm@7315: \railalias{thenapply}{then\_apply}
wenzelm@7315: \railterm{thenapply}
wenzelm@7315: 
wenzelm@7315: \begin{rail}
wenzelm@7315:   'apply' method
wenzelm@7315:   ;
wenzelm@7315:   thenapply method
wenzelm@7315:   ;
wenzelm@7315:   'back'
wenzelm@7315:   ;
wenzelm@7315: \end{rail}
wenzelm@7315: 
wenzelm@7315: \begin{descr}
wenzelm@7315: \item [$\isarkeyword{apply}~m$] applies proof method $m$ in the
wenzelm@7315:   plain-old-tactic sense.  Facts for forward chaining are ignored.
wenzelm@7315: \item [$\isarkeyword{then_apply}~m$] is similar to $\isarkeyword{apply}$, but
wenzelm@7315:   observes the goal's facts.
wenzelm@7315: \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
wenzelm@7315:   the last proof command.  Basically, any proof command may return multiple
wenzelm@7315:   results.
wenzelm@7315: \end{descr}
wenzelm@7315: 
wenzelm@7315: 
wenzelm@7315: \subsection{Term abbreviations}\label{sec:term-abbrev}
wenzelm@7315: 
wenzelm@7315: \indexisarcmd{let}
wenzelm@7315: \begin{matharray}{rcl}
wenzelm@7315:   \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315:   \isarkeyword{is} & : & syntax \\
wenzelm@7315: \end{matharray}
wenzelm@7315: 
wenzelm@7315: Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
wenzelm@7315: or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
wenzelm@7315: etc.) with a list of patterns $\IS{p@1 \dots p@n}$.  In both cases,
wenzelm@7315: higher-order matching is applied to bind extra-logical text
wenzelm@7315: variables\index{text variables}, which may be either of the form $\VVar{x}$
wenzelm@7315: (token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless
wenzelm@7315: dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the
wenzelm@7315: $\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$
wenzelm@7315: patterns are in postfix position.
wenzelm@7315: 
wenzelm@7315: Note that term abbreviations are quite different from actual local definitions
wenzelm@7315: as introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
wenzelm@7315: visible within the logic as actual equations, while abbreviations disappear
wenzelm@7315: during the input process just after type checking.
wenzelm@7315: 
wenzelm@7315: \begin{rail}
wenzelm@7315:   'let' ((term + 'as') '=' term comment? + 'and')
wenzelm@7315:   ;  
wenzelm@7315: \end{rail}
wenzelm@7315: 
wenzelm@7315: The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
wenzelm@7315: \railnonterm{proppat} (see \S\ref{sec:term-pats}).
wenzelm@7315: 
wenzelm@7315: \begin{descr}
wenzelm@7315: \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
wenzelm@7315:   by simultaneous higher-order matching against terms $\vec t$.
wenzelm@7315: \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
wenzelm@7315:   preceding statement.  Also note that $\ISNAME$ is not a separate command,
wenzelm@7315:   but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
wenzelm@7315: \end{descr}
wenzelm@7315: 
wenzelm@7315: Furthermore, a few automatic term abbreviations\index{automatic abbreviation}
wenzelm@7315: for goals and facts are available.  For any open goal, $\VVar{thesis}$ refers
wenzelm@7315: to its object-logic statement, $\VVar{thesis_prop}$ to the full proposition
wenzelm@7315: (which may be a rule), and $\VVar{thesis_concl}$ to its (atomic) conclusion.
wenzelm@7315: 
wenzelm@7315: Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$
wenzelm@7315: as object-logic statement get $x$ bound to the special text variable
wenzelm@7315: ``$\dots$'' (three dots).  The canonical application of this feature are
wenzelm@7315: calculational proofs, see \S\ref{sec:calculation}.
wenzelm@7315: 
wenzelm@7315: 
wenzelm@7134: \subsection{Block structure}
wenzelm@7134: 
wenzelm@7167: While Isar is inherently block-structured, opening and closing blocks is
wenzelm@7167: mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm@7167: local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm@7167: again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
wenzelm@7167: different context within a sub-proof are typically switched via
wenzelm@7167: $\isarkeyword{next}$, which is just a single block-close followed by
wenzelm@7167: block-open again.  Thus the effect of $\isarkeyword{next}$ is to reset the
wenzelm@7167: proof context to that of the head of the sub-proof.  Note that there is no
wenzelm@7175: goal focus involved here!
wenzelm@7167: 
wenzelm@7175: For slightly more advanced applications, there are explicit block parentheses
wenzelm@7175: as well.  These typically achieve a strong forward style of reasoning.
wenzelm@7167: 
wenzelm@7134: \indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134:   \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7167: \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
wenzelm@7167:   resetting the context to the initial one.
wenzelm@7167: \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
wenzelm@7167:   close blocks.  Any current facts pass through $\isarkeyword{\{\{}$
wenzelm@7167:   unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into
wenzelm@7315:   the enclosing context.  Thus fixed variables are generalised, assumptions
wenzelm@7167:   discharged, and local definitions eliminated.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \section{Other commands}
wenzelm@7134: 
wenzelm@7315: The following commands are not part of the actual proper or improper
wenzelm@7315: Isabelle/Isar syntax, but assist interactive development, for example.  Also
wenzelm@7315: note that $undo$ does not apply here, since the theory or proof configuration
wenzelm@7315: is not changed.
wenzelm@7315: 
wenzelm@7134: \subsection{Diagnostics}
wenzelm@7134: 
wenzelm@7134: \indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134:   \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134:   \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134:   \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7134: \begin{rail}
wenzelm@7134:   'typ' type
wenzelm@7134:   ;
wenzelm@7134:   'term' term
wenzelm@7134:   ;
wenzelm@7134:   'prop' prop
wenzelm@7134:   ;
wenzelm@7134:   'thm' thmrefs
wenzelm@7134:   ;
wenzelm@7134: \end{rail}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
wenzelm@7134:   $\isarkeyword{prop}~\phi$] read and print types / terms / propositions
wenzelm@7134:   according to the current theory or proof context.
wenzelm@7134: \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
wenzelm@7134:   theory or proof context.  Note that any attributes included in the theorem
wenzelm@7175:   specifications are applied to a temporary context derived from the current
wenzelm@7175:   theory or proof; the result is discarded.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7134: \subsection{System operations}
wenzelm@7134: 
wenzelm@7167: \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
wenzelm@7167: \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
wenzelm@7134: \begin{matharray}{rcl}
wenzelm@7134:   \isarcmd{cd} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{pwd} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134:   \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134: \end{matharray}
wenzelm@7134: 
wenzelm@7167: \begin{descr}
wenzelm@7134: \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
wenzelm@7134:   process.
wenzelm@7134: \item [$\isarkeyword{pwd}~$] prints the current working directory.
wenzelm@7175: \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
wenzelm@7175:   $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
wenzelm@7175:   theory given as $name$ argument.  These commands are exactly the same as the
wenzelm@7175:   corresponding ML functions (see also \cite[\S1 and \S6]{isabelle-ref}).
wenzelm@7175:   Note that both the ML and Isar versions of these commands may load new- and
wenzelm@7175:   old-style theories alike.
wenzelm@7167: \end{descr}
wenzelm@7134: 
wenzelm@7134: 
wenzelm@7046: %%% Local Variables: 
wenzelm@7046: %%% mode: latex
wenzelm@7046: %%% TeX-master: "isar-ref"
wenzelm@7046: %%% End: 




