# HG changeset patch # User wenzelm # Date 936367913 -7200 # Node ID bb282845ca778b487403f073f39d0b9e3ab91dfc # Parent e67eed4cd2241f91375d974e7948373db8f0a028 updated; diff -r e67eed4cd224 -r bb282845ca77 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Fri Sep 03 16:11:03 1999 +0200 +++ b/doc-src/IsarRef/generic.tex Fri Sep 03 16:11:53 1999 +0200 @@ -4,12 +4,11 @@ \section{Basic proof methods}\label{sec:pure-meth} \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption} -\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold} +\indexisarmeth{fold}\indexisarmeth{unfold} \indexisarmeth{rule}\indexisarmeth{erule} \begin{matharray}{rcl} - & : & \isarmeth \\ assumption & : & \isarmeth \\ - finish & : & \isarmeth \\[0.5ex] rule & : & \isarmeth \\ erule^* & : & \isarmeth \\[0.5ex] fold & : & \isarmeth \\ @@ -29,11 +28,8 @@ performs a single reduction step using the $rule$ method (see below); thus a plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$ alone. -\item [$assumption$] solves some goal by assumption, after inserting the - goal's facts. -\item [$finish$] solves all remaining goals by assumption; this is the default - terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be - spelled out explicitly. +\item [$assumption$] solves some goal by assumption. The facts (if any) are + guaranteed to participate. \item [$rule~thms$] applies some rule given as argument in backward manner; facts are used to reduce the rule before applying it to the goal. Thus $rule$ without facts is plain \emph{introduction}, while with facts it @@ -142,7 +138,7 @@ Calculational proof is forward reasoning with implicit application of transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains an auxiliary register $calculation$\indexisarthm{calculation} for accumulating -results obtained by transitivity obtained together with the current facts. +results obtained by transitivity obtained together with the current result. 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 @@ -173,11 +169,11 @@ \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 same + initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the 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). + applied to $calculation$ and $this$ (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 @@ -343,9 +339,10 @@ actually happens, thus it is very appropriate as an initial method for $\PROOFNAME$ that splits up certain connectives of the goal, before entering the sub-proof. - -\item [Method $contradiction$] solves some goal by contradiction: both $A$ and - $\neg A$ have to be present in the assumptions. + +\item [Method $contradiction$] solves some goal by contradiction, deriving any + result from both $\neg A$ and $A$. Facts, which are guaranteed to + participate, may appear in either order. \end{descr} diff -r e67eed4cd224 -r bb282845ca77 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Fri Sep 03 16:11:03 1999 +0200 +++ b/doc-src/IsarRef/pure.tex Fri Sep 03 16:11:53 1999 +0200 @@ -410,8 +410,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)$: existing facts have been just picked up in order to use them - when refining the goal claimed next. + $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just + picked up in order to use them when refining the goal claimed next. \end{descr} @@ -478,7 +478,7 @@ var: name ('::' type)? ; - vars: name+ ('::' type)? + vars: (name+) ('::' type)? ; assm: thmdecl? (prop proppat? +) ; @@ -521,7 +521,7 @@ Any fact will usually be involved in further proofs, either as explicit arguments of proof methods or when forward chaining towards the next goal via $\THEN$ (and variants). Note that the special theorem name -$facts$.\indexisarthm{facts} refers to the most recently established facts. +$this$.\indexisarthm{this} refers to the most recently established facts. \begin{rail} 'note' thmdef? thmrefs comment? ; @@ -541,7 +541,7 @@ \S\ref{sec:proof-steps}). For example, method $rule$ (see \S\ref{sec:pure-meth}) would do an elimination rather than an introduction. \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is - equivalent to $\FROM{facts}$. + equivalent to $\FROM{this}$. \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward chaining is from earlier facts together with the current ones. \end{descr} @@ -549,9 +549,9 @@ Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect multiple facts to be given in proper order, corresponding to a prefix of the premises of the rule involved. Note that positions may be easily skipped -using a form like $\FROM{_~a~b}$, for example. This involves the rule -$PROP~\psi \Imp PROP~\psi$, which is bound in Isabelle/Pure as ``_'' -(underscore).\indexisarthm{_@\texttt{_}} +using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves +the rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure as +``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} \subsection{Goal statements} @@ -593,8 +593,10 @@ \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some pending goal with the result \emph{exported} into the corresponding context. \item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a - local goal to be proven by forward chaining the current facts. -\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. + local goal to be proven by forward chaining the current facts. Note that + $\HENCENAME$ is equivalent to $\FROM{this}~\HAVENAME$. +\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. Note that + $\THUSNAME$ is equivalent to $\FROM{this}~\SHOWNAME$. \end{descr} @@ -639,8 +641,9 @@ Unless given explicitly by the user, the default initial method is ``$default$'', which is usually set up to apply a single standard elimination -or introduction rule according to the topmost symbol involved. The default -terminal method is ``$finish$''; it solves all goals by assumption. +or introduction rule according to the topmost symbol involved. There is no +default terminal method; in any case the final step is to solve all remaining +goals by assumption. \begin{rail} 'proof' interest? meth? comment? @@ -673,7 +676,8 @@ expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually sufficient to see what is going wrong. \item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$. -\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates $\BY{-}$. +\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates + $\BY{assumption}$. \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of course, the result is a fake theorem only, @@ -734,7 +738,7 @@ 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 +dummies ``\texttt{_}'' (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.