# HG changeset patch # User wenzelm # Date 935349200 -7200 # Node ID 76a39a3784b5f63a651aa3c6345e32c4e81e1cc4 # Parent d3968533692ce058fa3b78de9a8c5f5ff315ce72 checkpoint; diff -r d3968533692c -r 76a39a3784b5 doc-src/IsarRef/basics.tex --- a/doc-src/IsarRef/basics.tex Sun Aug 22 18:21:36 1999 +0200 +++ b/doc-src/IsarRef/basics.tex Sun Aug 22 21:13:20 1999 +0200 @@ -4,23 +4,36 @@ Isabelle/Isar offers two main improvements over classic Isabelle: \begin{enumerate} \item A new \emph{theory format}, often referred to as ``new-style theories'', - supporting interactive development with unlimited undo operation. -\item A formal \emph{proof language} language designed to support - \emph{intelligible} semi-automated reasoning. Rather than putting together - tactic scripts, the author is enabled to express the reasoning in way that - is close to mathematical practice. + supporting interactive development and unlimited undo operation. +\item A \emph{formal proof language} designed to support intelligible + semi-automated reasoning. Rather than putting together tactic scripts, the + author is enabled to express the reasoning in way that is close to + mathematical practice. \end{enumerate} The Isar proof language is embedded into the new theory format as a proper sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or -$\LEMMANAME$ at the theory levels, and left with the final end of proof. Some -theory extension mechanisms require proof as well, such as the HOL -$\isarkeyword{typedef}$. +$\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\ +via $\QEDNAME$). Some theory extension mechanisms require proof as well, such +as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty +representing sets. New-style theory files may still be associated with an ML file consisting of -plain old tactic scripts. Generally, migration between the two formats is -made relatively easy, and users may start to benefit from interactive theory -development even before they have any idea of the Isar proof language. +plain old tactic scripts. There is no longer any ML binding generated for the +theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and +\texttt{thms} may be used to retrieve this information from ML (see also +\cite{isabelle-ref}). Nevertheless, migration between classic Isabelle and +Isabelle/Isar is relatively easy. Thus users may start to benefit from +interactive theory development even before they have any idea of the Isar +proof language. + +\begin{warn} + Proof~General does \emph{not} support mixed interactive development of + classic Isabelle theory files and tactic scripts together with Isar + documents at the same time. The \texttt{isa} and \texttt{isar} versions of + Proof~General appear as two different theorem proving systems; only one + prover may be active at any time. +\end{warn} \section{The Isar proof language} diff -r d3968533692c -r 76a39a3784b5 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Sun Aug 22 18:21:36 1999 +0200 +++ b/doc-src/IsarRef/generic.tex Sun Aug 22 21:13:20 1999 +0200 @@ -1,7 +1,7 @@ \chapter{Generic Tools and Packages}\label{ch:gen-tools} -\section{Basic proof methods and attributes}\label{sec:pure-meth} +\section{Basic proof methods}\label{sec:pure-meth} \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption} \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold} @@ -33,6 +33,9 @@ %FIXME thmref (single) %FIXME var vs. term + +\section{Miscellaneous attributes} + \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS} \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard} \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export} @@ -78,6 +81,73 @@ FIXME + +\section{Calculational proof}\label{sec:calculation} + +\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans} +\begin{matharray}{rcl} + \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ + trans & : & \isaratt \\ +\end{matharray} + +Calculational proof is forward reasoning with implicit application of +transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains +an auxiliary register $calculation$\indexisarreg{calculation} for accumulating +results obtained by transitivity obtained together with the current facts. +Command $\ALSO$ updates $calculation$ from the most recent result, while +$\FINALLY$ exhibits the final result by forward chaining towards the next goal +statement. Both commands require valid current facts, i.e.\ may occur only +after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or +some finished $\HAVENAME$ or $\SHOWNAME$. + +Also note that the automatic term abbreviation ``$\dots$'' has its canonical +application with calculational proofs. It automatically refers to the +argument\footnote{The argument of a curried infix expression is its right-hand + side.} of the preceding statement. + +Isabelle/Isar calculations are implicitly subject to block structure in the +sense that new threads of calculational reasoning are commenced for any new +block (as opened by a local goal, for example). This means that, apart from +being able to nest calculations, there is no separate \emph{begin-calculation} +command required. + +\begin{rail} + ('also' | 'finally') transrules? comment? + ; + 'trans' (() | 'add' ':' | 'del' ':') thmrefs + ; + + transrules: '(' thmrefs ')' interest? + ; +\end{rail} + +\begin{descr} +\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as + follows. The first occurrence of $\ALSO$ in some calculational thread + initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the + \emph{same} level of block-structure updates $calculation$ by some + transitivity rule applied to $calculation$ and $facts$ (in that order). + Transitivity rules are picked from the current context plus those given as + $thms$ (the latter have precedence). + +\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as + $\ALSO$, and concludes the current calculational thread. The final result + is exhibited as fact for forward chaining towards the next goal. Basically, + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof + idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$. + +\item [Attribute $trans$] maintains the set of transitivity rules of the + theory or proof context, by adding or deleting the theorems provided as + arguments. The default is adding of rules. +\end{descr} + +See theory \texttt{HOL/Isar_examples/Group} for a simple applications of +calculations for basic equational reasoning. +\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced +calculational steps in combination with natural deduction. + + \section{Axiomatic Type Classes}\label{sec:axclass} \indexisarcmd{axclass}\indexisarcmd{instance} @@ -114,8 +184,48 @@ \section{The Simplifier} +\subsection{Simplification methods} + +\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp} +\begin{matharray}{rcl} + simp & : & \isarmeth \\ + asm_simp & : & \isarmeth \\ + simp & : & \isaratt \\ +\end{matharray} + +\begin{rail} + 'simp' (simpmod+)? + ; + + simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs + ; +\end{rail} + + +\subsection{Forward simplification} + +\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify} +\begin{matharray}{rcl} + simplify & : & \isaratt \\ + asm_simplify & : & \isaratt \\ + full_simplify & : & \isaratt \\ + asm_full_simplify & : & \isaratt \\ +\end{matharray} + +FIXME + + \section{The Classical Reasoner} +\subsection{Single step methods} + +\subsection{Automatic methods} + +\subsection{Combined automatic methods} + +\subsection{Modifying the context} + + %\indexisarcmd{} %\begin{matharray}{rcl} diff -r d3968533692c -r 76a39a3784b5 doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Sun Aug 22 18:21:36 1999 +0200 +++ b/doc-src/IsarRef/intro.tex Sun Aug 22 21:13:20 1999 +0200 @@ -15,7 +15,7 @@ lemma "0 < foo" by (simp add: foo_def); end \end{ttbox} -Note that \emph{any} Isabelle/Isar command may be retracted by \texttt{undo}. +Note that any Isabelle/Isar command may be retracted by \texttt{undo}. Plain TTY-based interaction like this used to be quite feasible with traditional tactic based theorem proving, but developing Isar documents @@ -30,7 +30,7 @@ \medskip -The easiest way to use ProofGeneral is to make it the default Isabelle user +The easiest way to use Proof~General is to make it the default Isabelle user interface. Just say something like this in your Isabelle settings file (cf.\ \cite{isabelle-sys}): \begin{ttbox} @@ -39,8 +39,8 @@ \end{ttbox} You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the actual installation directory of Proof~General. Now the capital -\texttt{Isabelle} binary refers to the \texttt{ProofGeneral/isar} interface. -It's usage is as follows: +\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar} +interface. It's usage is as follows: \begin{ttbox} Usage: interface [OPTIONS] [FILES ...] @@ -53,12 +53,12 @@ Starts Proof General for Isabelle/Isar with proof documents FILES (default Scratch.thy). \end{ttbox} -The defaults for these options may be changed via the -\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU Emacs\footnote{GNU - Emacs version 20.x required.} with loading of the startup file enabled may -be configured as follows:\footnote{The interface disables \texttt{.emacs} by - default to ensure successful startup despite any strange commands that tend - to occur there.} +Note that the defaults for these options may be overridden via the +\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU +Emacs\footnote{Version 20.x required.} with loading of the startup file +enabled may be configured as follows:\footnote{The interface disables + \texttt{.emacs} by default to ensure successful startup despite any strange + commands that tend to occur there.} \begin{ttbox} PROOFGENERAL_OPTIONS="-p emacs -u true" \end{ttbox} @@ -68,7 +68,7 @@ \begin{ttbox} Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy \end{ttbox} -Users of XEmacs may note the toolbar for navigating forward and backward +Users of XEmacs may note the tool bar for navigating forward and backward through the text. Consult the Proof~General documentation \cite{proofgeneral} for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}. diff -r d3968533692c -r 76a39a3784b5 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Sun Aug 22 18:21:36 1999 +0200 +++ b/doc-src/IsarRef/pure.tex Sun Aug 22 21:13:20 1999 +0200 @@ -1,12 +1,12 @@ -\chapter{Basic Isar elements} +\chapter{Basic Isar elements}\label{ch:pure-syntax} -Subsequently, we introduce most of the basic Isar theory and proof commands as -provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes further Isar -elements as provided by generic tools and packages that are either part of -Pure Isabelle, or preloaded by most object logics (such as the Simplifier). -See chapter~\ref{ch:hol-tools} for actual object-logic specific elements (for -Isabelle/HOL). +Subsequently, we introduce the main part of the basic Isar theory and proof +commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes +further Isar elements as provided by generic tools and packages that are +either part of Pure Isabelle, or pre-loaded by most object logics (such as the +Simplifier). See chapter~\ref{ch:hol-tools} for actual object-logic specific +elements (for Isabelle/HOL). \medskip @@ -114,10 +114,11 @@ just as in typical {\LaTeX} documents. \item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$, $\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$] - specify chapter and section headings. + mark chapter and section headings. \item [$\TEXT~text$] specifies an actual body of prose text, including - references to formal entities (the latter feature is not yet exploited in - any way). + references to formal entities.\footnote{The latter feature is not yet + exploited. Nevertheless, any text of the form \texttt{\at\{\dots\}} + should be considered as reserved for future use.} \end{descr} @@ -153,7 +154,7 @@ \end{descr} -\subsection{Types}\label{sec:types-pure} +\subsection{Primitive types and type abbreviations}\label{sec:types-pure} \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} \begin{matharray}{rcl} @@ -300,9 +301,9 @@ \isarcmd{local} & : & \isartrans{theory}{theory} \\ \end{matharray} -Isabelle organizes any kind of names (of types, constants, theorems etc.) by +Isabelle organises any kind of names (of types, constants, theorems etc.) by hierarchically structured name spaces. Normally the user never has to control -the behavior of name space entry by hand, yet the following commands provide +the behaviour of name space entry by hand, yet the following commands provide some way to do so. \begin{descr} @@ -343,7 +344,7 @@ \item [$\isarkeyword{setup}~text$] changes the current theory context by applying setup functions $text$, which has to be an ML expression of type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual - way to initialize object-logic specific tools and packages written in ML. + way to initialise object-logic specific tools and packages written in ML. \end{descr} @@ -386,15 +387,18 @@ \begin{descr} \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML - function $text$, which has to be of type $Sign\mathord.sg \times object \to - term)$. + function $text$, which has to be of type $Sign\mathord.sg \times + Object\mathord.T \to term)$. \end{descr} \section{Proof commands} -Proof commands provide transitions of Isar/VM machine configurations. There -are three different modes of operation. +Proof commands provide transitions of Isar/VM machine configurations, which +are block-structured, consisting of a stack of nodes with three main +components: logical \emph{proof context}, local \emph{facts}, and open +\emph{goals}. Isar/VM transitions are \emph{typed} according to the following +three three different modes of operation: \begin{descr} \item [$proof(prove)$] means that a new goal has just been stated that is now to be \emph{proven}; the next command may refine it by some proof method @@ -402,8 +406,8 @@ \item [$proof(state)$] is like an internal theory mode: the context may be augmented by \emph{stating} additional assumptions, intermediate result etc. \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and - $proof(prove)$: some existing facts have been just picked up in order to use - them when refining the goal to be claimed next. + $proof(prove)$: existing facts have been just picked up in order to use them + when refining the goal to be claimed next. \end{descr} @@ -426,40 +430,72 @@ \end{rail} -\subsection{Proof context} +\subsection{Proof context}\label{sec:proof-context} -\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let} +\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} \begin{matharray}{rcl} \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ \end{matharray} -FIXME +The logical proof context consists of fixed variables and assumptions. The +former closely correspond to Skolem constants, or meta-level universal +quantification as provided by the Isabelle/Pure logical framework. +Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in +a local entity that may be used in the subsequent proof as any other variable +or constant. Furthermore, any result $\phi[x]$ exported from the current +context will be universally closed wrt.\ $x$ at the outermost level (this is +expressed using Isabelle's meta-variables). + +Similarly, introducing some assumption $\chi$ has two effects. On the one +hand, a local theorem is created that may be used as a fact in subsequent +proof steps. On the other hand, any result $\phi$ exported from the context +becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal +using this result would basically introduce a new subgoal stemming from the +assumption. How this situation is handled depends on the actual version of +assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying +with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to +be proved later by the user. + +Local definitions, introduced by $\DEF{a}{x \equiv t}$, are achieved by +combining $\FIX x$ with another version of assumption that causes any +hypothetical equation $x = t$ to be eliminated by reflexivity. Thus, +exporting some result $\phi[x]$ simply yields $\phi[t]$. \begin{rail} 'fix' (var +) comment? ; - ('assume' | 'presume') thmdecl? \\ (prop proppat? +) comment? + ('assume' | 'presume') (assm comment? + 'and') ; 'def' thmdecl? \\ var '==' term termpat? comment? ; - 'let' ((term + 'as') '=' term comment? + 'and') - ; var: name ('::' type)? ; + assm: thmdecl? (prop proppat? +) + ; \end{rail} \begin{descr} -\item [$\FIX{x}$] FIXME -\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME -\item [$\DEF{a}{x \equiv t}$] FIXME -\item [$\LET{\vec p = \vec t}$] FIXME +\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$. +\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems + $\Phi$. Subsequent results used to solve some enclosing goal (e.g.\ via + $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be able to + unify with existing premises in the goal, while $\PRESUMENAME$ leaves $\Phi$ + as new subgoals. Note that several lists of assumptions may be given + (separated by \railterm{and}); the resulting list of current facts consists + of all of these. +\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. + In results exported from the context, $x$ is replaced by $t$. Basically, + $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$ (the + resulting hypothetical equation is solved by reflexivity, though). \end{descr} +The internal register $prems$\indexisarreg{prems} refers to all current +assumptions as a list of theorems. + \subsection{Facts and forward chaining} @@ -471,7 +507,10 @@ \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ \end{matharray} -FIXME +New facts are established either by assumption or proof of local statements +(via $\HAVENAME$ or $\SHOWNAME$). Any facts will usually be involved in +proofs of further results: either as explicit arguments of proof methods or +when forward chaining towards the next goal via $\THEN$ (and variants). \begin{rail} 'note' thmdef? thmrefs comment? @@ -497,6 +536,9 @@ chaining is from earlier facts together with the current ones. \end{descr} +Note that the internal register of \emph{current facts} may be referred as +theorem list $facts$.\indexisarreg{facts} + \subsection{Goal statements} @@ -629,6 +671,92 @@ \end{descr} +\subsection{Improper proof steps} + +The following commands emulate unstructured tactic scripts to some extent. +While these are anathema for writing proper Isar proof documents, they might +come in handy for exploring and debugging. + +\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back} +\begin{matharray}{rcl} + \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\ + \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\ + \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ +\end{matharray} + +\railalias{thenapply}{then\_apply} +\railterm{thenapply} + +\begin{rail} + 'apply' method + ; + thenapply method + ; + 'back' + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{apply}~m$] applies proof method $m$ in the + plain-old-tactic sense. Facts for forward chaining are ignored. +\item [$\isarkeyword{then_apply}~m$] is similar to $\isarkeyword{apply}$, but + observes the goal's facts. +\item [$\isarkeyword{back}$] does back-tracking over the result sequence of + the last proof command. Basically, any proof command may return multiple + results. +\end{descr} + + +\subsection{Term abbreviations}\label{sec:term-abbrev} + +\indexisarcmd{let} +\begin{matharray}{rcl} + \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarkeyword{is} & : & syntax \\ +\end{matharray} + +Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements, +or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$ +etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases, +higher-order matching is applied to bind extra-logical text +variables\index{text variables}, which may be either of the form $\VVar{x}$ +(token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless +dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the +$\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$ +patterns are in postfix position. + +Note that term abbreviations are quite different from actual local definitions +as introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are +visible within the logic as actual equations, while abbreviations disappear +during the input process just after type checking. + +\begin{rail} + 'let' ((term + 'as') '=' term comment? + 'and') + ; +\end{rail} + +The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or +\railnonterm{proppat} (see \S\ref{sec:term-pats}). + +\begin{descr} +\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$ + by simultaneous higher-order matching against terms $\vec t$. +\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the + preceding statement. Also note that $\ISNAME$ is not a separate command, + but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). +\end{descr} + +Furthermore, a few automatic term abbreviations\index{automatic abbreviation} +for goals and facts are available. For any open goal, $\VVar{thesis}$ refers +to its object-logic statement, $\VVar{thesis_prop}$ to the full proposition +(which may be a rule), and $\VVar{thesis_concl}$ to its (atomic) conclusion. + +Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$ +as object-logic statement get $x$ bound to the special text variable +``$\dots$'' (three dots). The canonical application of this feature are +calculational proofs, see \S\ref{sec:calculation}. + + \subsection{Block structure} While Isar is inherently block-structured, opening and closing blocks is @@ -657,67 +785,18 @@ \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and close blocks. Any current facts pass through $\isarkeyword{\{\{}$ unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into - the enclosing context. Thus fixed variables are generalized, assumptions + the enclosing context. Thus fixed variables are generalised, assumptions discharged, and local definitions eliminated. \end{descr} -\subsection{Calculational proof} - -\indexisarcmd{also}\indexisarcmd{finally} -\begin{matharray}{rcl} - \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ -\end{matharray} - -FIXME - -\begin{rail} - ('also' | 'finally') transrules? comment? - ; - - transrules: '(' thmrefs ')' interest? - ; -\end{rail} - -\begin{descr} -\item [$\ALSO~(thms)$] FIXME -\item [$\FINALLY~(thms)$] FIXME -\end{descr} - - - -\subsection{Improper proof steps} - -The following commands emulate unstructured tactic scripts to some extent. -While these are anathema for writing proper Isar proof documents, they might -come in handy for exploring and debugging. - -\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back} -\begin{matharray}{rcl} - \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\ - \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\ - \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ -\end{matharray} - -\railalias{thenapply}{then\_apply} -\railterm{thenapply} - -\begin{rail} - 'apply' method - ; - thenapply method - ; - 'back' - ; -\end{rail} - -\begin{descr} -\item [$ $] FIXME -\end{descr} - \section{Other commands} +The following commands are not part of the actual proper or improper +Isabelle/Isar syntax, but assist interactive development, for example. Also +note that $undo$ does not apply here, since the theory or proof configuration +is not changed. + \subsection{Diagnostics} \indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm} diff -r d3968533692c -r 76a39a3784b5 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Sun Aug 22 18:21:36 1999 +0200 +++ b/doc-src/IsarRef/syntax.tex Sun Aug 22 21:13:20 1999 +0200 @@ -1,15 +1,69 @@ - -%FIXME -% - examples (!?) - \chapter{Isar document syntax} -FIXME shortcut +We give a complete reference of all basic syntactic entities underlying the +the Isabelle/Isar document syntax. This chapter will not introduce any actual +theory and proof commands, though (cf.\ chapter~\ref{ch:pure-syntax} and +later). + +\medskip + +In order to get started with writing well-formed Isabelle/Isar documents, the +most important aspect to be noted is the difference of \emph{inner} versus +\emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the +logic, while outer syntax is that of Isabelle/Isar theories (and proofs). As +a general rule, inner syntax entities may occur only as \emph{atomic entities} +within outer syntax. For example, quoted string \texttt{"x + y"} and +identifier \texttt{z} are legal term specifications, while \texttt{x + y} is +not. + +\begin{warn} + Note that old-style Isabelle theories used to fake parts of the inner type + syntax, with complicated rules when quotes may be omitted. Despite the + minor drawback of requiring quotes more often, Isabelle/Isar is simpler and + more robust in that respect. +\end{warn} + + +\section{Lexical matters}\label{sec:lex-syntax} + +The Isabelle/Isar outer syntax provides token classes as presented below. +Note that some of these coincide (by full intention) with inner lexical syntax +as given in \cite{isabelle-ref}. These different levels of syntax should not +be confused, though. -FIXME important note: inner versus outer syntax +\begin{matharray}{rcl} + ident & = & letter~quasiletter^* \\ + longident & = & ident\verb,.,ident~\dots~ident \\ + symident & = & sym^+ \\ + nat & = & digit^+ \\ + var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ + textvar & = & \verb,??,ident \\ + typefree & = & \verb,',ident \\ + typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ + string & = & \verb,", ~\dots~ \verb,", \\ + verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[2ex] -\section{Lexical matters} + letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$ + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \verb,<, ~|~ + \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \verb,^, ~|~ \verb,_, ~|~ + \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ +\end{matharray} + +The syntax of \texttt{string} admits any characters, including newlines; +\verb|"| and \verb|\| have to be escaped by a backslash, though. Note that +ML-style control character notation is not supported. The body of +\texttt{verbatim} may consist of any text not containing \verb|*}|. + +Comments take the form \texttt{(*~\dots~*)} and may be nested, just as in ML. +Note that these are \emph{source} comments only, which are stripped after +lexical analysis of the input. The Isar document syntax also provides several +elements of \emph{formal comments} that are actually part of the text (see +\S\ref{sec:comments}, \S\ref{sec:formal-cmt-thy}, \S\ref{sec:formal-cmt-prf}). + \section{Common syntax entities} @@ -46,7 +100,7 @@ \end{rail} -\subsection{Comments} +\subsection{Comments}\label{sec:comments} Large chunks of plain \railqtoken{text} are usually given \railtoken{verbatim}, i.e.\ enclosed in \verb|{*|\dots\verb|*}|. For @@ -58,8 +112,8 @@ level. A few commands such as $\PROOFNAME$ admit additional markup with a ``level of interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$) indicates that the respective part of the document becomes $n$ levels -more boring or obscure; \texttt{\%\%} means that the interest drops by -$\infty$ --- abandon every hope, who enter here. +more obscure; \texttt{\%\%} means that interest drops by $\infty$ --- +\emph{abandon every hope, who enter here}. \indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest} \begin{rail} @@ -94,7 +148,7 @@ \subsection{Types and terms}\label{sec:types-terms} The actual inner Isabelle syntax, that of types and terms of the logic, is far -too flexible in order to be modeled explicitly at the outer theory level. +too flexible in order to be modelled explicitly at the outer theory level. Basically, any such entity has to be quoted at the outer level to turn it into a single token (the parsing and type-checking is performed later). For convenience, a slightly more liberal convention is adopted: quotes may be @@ -123,7 +177,7 @@ \end{rail} -\subsection{Term patterns} +\subsection{Term patterns}\label{sec:term-pats} Assumptions and goal statements usually admit automatic binding of schematic text variables by giving (optional) patterns of the form $\IS{p@1 \dots p@n}$. @@ -161,8 +215,8 @@ \subsection{Attributes and theorems}\label{sec:syn-att} Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own -``semi-inner'' syntax, which does not have to be atomic at the outer level -unlike that of types and terms. Instead, the attribute argument +``semi-inner'' syntax, in the sense that input conforming \railnonterm{args} +below are parsed by the attribute a second time. The attribute argument specifications may be any sequence of atomic entities (identifiers, strings etc.), or properly bracketed argument lists. Below \railqtoken{atom} refers to any atomic entity, including \railtoken{keyword}s conforming to @@ -180,7 +234,7 @@ ; \end{rail} -Theorem specifications come in several flavors: \railnonterm{axmdecl} and +Theorem specifications come in several flavours: \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal statements, \railnonterm{thmdef} collects lists of existing theorems. Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}