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