wenzelm@7046: wenzelm@7167: \chapter{Basic Isar elements} wenzelm@7167: wenzelm@7167: Subsequently, we introduce most of the basic Isar theory and proof commands as wenzelm@7167: provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes further Isar wenzelm@7167: elements as provided by generic tools and packages that are either part of wenzelm@7175: Pure Isabelle, or preloaded by most object logics (such as the Simplifier). wenzelm@7167: See chapter~\ref{ch:hol-tools} for actual object-logic specific elements (for wenzelm@7167: 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@7175: specify chapter and section headings. wenzelm@7134: \item [$\TEXT~text$] specifies an actual body of prose text, including wenzelm@7175: references to formal entities (the latter feature is not yet exploited in wenzelm@7175: any way). 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' | '<=') 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@7175: Isabelle organizes any kind of names (of types, constants, theorems etc.) by wenzelm@7175: hierarchically structured name spaces. Normally the user never has to control wenzelm@7175: the behavior 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@7175: way to initialize 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@7175: function $text$, which has to be of type $Sign\mathord.sg \times object \to wenzelm@7175: term)$. wenzelm@7167: \end{descr} wenzelm@7134: wenzelm@7134: wenzelm@7134: \section{Proof commands} wenzelm@7134: wenzelm@7167: Proof commands provide transitions of Isar/VM machine configurations. There wenzelm@7175: are 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@7175: $proof(prove)$: some existing facts have been just picked up in order to use wenzelm@7175: them 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@7134: \subsection{Proof context} wenzelm@7134: wenzelm@7134: \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let} 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: \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ wenzelm@7134: \end{matharray} wenzelm@7134: wenzelm@7175: FIXME wenzelm@7175: wenzelm@7134: \begin{rail} wenzelm@7134: 'fix' (var +) comment? wenzelm@7134: ; wenzelm@7175: ('assume' | 'presume') thmdecl? \\ (prop proppat? +) comment? wenzelm@7134: ; wenzelm@7175: 'def' thmdecl? \\ var '==' term termpat? comment? wenzelm@7134: ; wenzelm@7134: 'let' ((term + 'as') '=' term comment? + 'and') wenzelm@7134: ; wenzelm@7134: wenzelm@7134: var: name ('::' type)? wenzelm@7134: ; wenzelm@7134: \end{rail} wenzelm@7134: wenzelm@7167: \begin{descr} wenzelm@7167: \item [$\FIX{x}$] FIXME wenzelm@7167: \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME wenzelm@7167: \item [$\DEF{a}{x \equiv t}$] FIXME wenzelm@7167: \item [$\LET{\vec p = \vec t}$] FIXME wenzelm@7167: \end{descr} wenzelm@7167: 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@7175: FIXME 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@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@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@7167: the enclosing context. Thus fixed variables are generalized, assumptions wenzelm@7167: discharged, and local definitions eliminated. wenzelm@7167: \end{descr} wenzelm@7134: wenzelm@7134: \subsection{Calculational proof} wenzelm@7134: wenzelm@7134: \indexisarcmd{also}\indexisarcmd{finally} wenzelm@7134: \begin{matharray}{rcl} wenzelm@7134: \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ wenzelm@7134: \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ wenzelm@7134: \end{matharray} wenzelm@7134: wenzelm@7175: FIXME wenzelm@7175: wenzelm@7134: \begin{rail} wenzelm@7134: ('also' | 'finally') transrules? comment? wenzelm@7134: ; wenzelm@7134: wenzelm@7134: transrules: '(' thmrefs ')' interest? wenzelm@7134: ; wenzelm@7134: \end{rail} wenzelm@7134: wenzelm@7167: \begin{descr} wenzelm@7175: \item [$\ALSO~(thms)$] FIXME wenzelm@7175: \item [$\FINALLY~(thms)$] FIXME wenzelm@7167: \end{descr} wenzelm@7134: wenzelm@7134: wenzelm@7134: wenzelm@7134: \subsection{Improper proof steps} wenzelm@7134: wenzelm@7175: The following commands emulate unstructured tactic scripts to some extent. wenzelm@7175: While these are anathema for writing proper Isar proof documents, they might wenzelm@7175: come in handy for exploring and debugging. wenzelm@7167: wenzelm@7167: \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back} wenzelm@7134: \begin{matharray}{rcl} wenzelm@7134: \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\ wenzelm@7134: \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\ wenzelm@7134: \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ wenzelm@7134: \end{matharray} wenzelm@7134: wenzelm@7134: \railalias{thenapply}{then\_apply} wenzelm@7134: \railterm{thenapply} wenzelm@7134: wenzelm@7134: \begin{rail} wenzelm@7134: 'apply' method wenzelm@7134: ; wenzelm@7134: thenapply method wenzelm@7134: ; wenzelm@7134: 'back' wenzelm@7134: ; wenzelm@7134: \end{rail} wenzelm@7134: wenzelm@7167: \begin{descr} wenzelm@7134: \item [$ $] FIXME wenzelm@7167: \end{descr} wenzelm@7134: wenzelm@7134: wenzelm@7134: \section{Other commands} wenzelm@7134: 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: