# HG changeset patch # User wenzelm # Date 941379635 -3600 # Node ID d9aef93c0e324029896c2e353f7b35c86ccd5661 # Parent 9d319a76dbeb1e042f95002d235362b40b2758cb tuned; diff -r 9d319a76dbeb -r d9aef93c0e32 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/generic.tex Sun Oct 31 15:20:35 1999 +0100 @@ -37,9 +37,9 @@ becomes a (generalized) \emph{elimination}. Note that the classical reasoner introduces another version of $rule$ that - is able to pick appropriate rules automatically, whenever explicit $thms$ - are omitted (see \S\ref{sec:classical-basic}); that method is the default - for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates + is able to pick appropriate rules automatically, whenever $thms$ are omitted + (see \S\ref{sec:classical-basic}); that method is the default for + $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates $\BY{default}$. \item [$erule~thms$] is similar to $rule$, but applies rules by elim-resolution. This is an improper method, mainly for experimentation and @@ -47,11 +47,11 @@ $rule$ (single step, involving facts) or $elim$ (repeated steps, see \S\ref{sec:classical-basic}). \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given - meta-level definitions throughout all goals; any facts provided are - \emph{ignored}. -\item [$succeed$] yields a single (unchanged) result; it is the identify of + meta-level definitions throughout all goals; any facts provided are inserted + into the goal and subject to rewriting as well. +\item [$succeed$] yields a single (unchanged) result; it is the identity of the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). -\item [$fail$] yields an empty result sequence; it is the identify of the +\item [$fail$] yields an empty result sequence; it is the identity of the ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). \end{descr} @@ -98,12 +98,12 @@ result). \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note - the reversed order). Note that premises may be skipped by including $\_$ - (underscore) as argument. + the reversed order). Note that premises may be skipped by including + ``$\_$'' (underscore) as argument. $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$ - that does not include the automatic lifting process that is normally - intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). + that skips the automatic lifting process that is normally intended (cf.\ + \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named instantiation, respectively. The terms given in $of$ are substituted for @@ -180,9 +180,10 @@ \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}$. Typical proof - idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and - ``$\FINALLY~\HAVE{}{\phi}~\DOT$''. + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that + ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and + ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding + calculational proofs. \item [$trans$] maintains the set of transitivity rules of the theory or proof context, by adding or deleting theorems (the default is to add). @@ -204,12 +205,12 @@ intro_classes & : & \isarmeth \\ \end{matharray} -Axiomatic type classes are provided by Isabelle/Pure as a purely -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus -any object logic may make use of this light-weight mechanism for abstract -theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of -the standard Isabelle documentation. +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} +interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic +may make use of this light-weight mechanism of abstract theories. See +\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard +Isabelle documentation. %FIXME cite \begin{rail} @@ -225,21 +226,22 @@ holding. Class axioms may not contain more than one type variable. The class axioms (with implicit sort constraints added) are bound to the given names. Furthermore a class introduction rule is generated, which is - employed by method $intro_classes$ in support instantiation proofs of this + employed by method $intro_classes$ to support instantiation proofs of this class. \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: (\vec s)c$] setup up a goal stating the class relation or type arity. The - proof would usually proceed by the $intro_classes$ method, and then - establish the characteristic theorems of the type classes involved. After - finishing the proof the theory will be augmented by a type signature - declaration corresponding to the resulting theorem. -\item [$intro_classes$] repeatedly expands the class introduction rules of + proof would usually proceed by $intro_classes$, and then establish the + characteristic theorems of the type classes involved. After finishing the + proof, the theory will be augmented by a type signature declaration + corresponding to the resulting theorem. +\item [$intro_classes$] repeatedly expands all class introduction rules of this theory. \end{descr} -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using -axiomatic type classes, including instantiation proofs. +%FIXME +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using +%axiomatic type classes, including instantiation proofs. \section{The Simplifier} @@ -345,7 +347,7 @@ given ones may be applied. The latter form admits better control of what actually happens, thus it is very appropriate as an initial method for $\PROOFNAME$ that splits up certain connectives of the goal, before entering - the actual proof. + the actual sub-proof. \item [$contradiction$] solves some goal by contradiction, deriving any result from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may @@ -388,7 +390,10 @@ Any of above methods support additional modifiers of the context of classical rules. There semantics is analogous to the attributes given in -\S\ref{sec:classical-mod}. +\S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted +into the goal before doing the search. The ``!''~argument causes the full +context of assumptions to be included as well.\footnote{This is slightly less + hazardous than for the Simplifier (see \S\ref{sec:simp}).} \subsection{Combined automated methods} @@ -403,7 +408,7 @@ ('force' | 'auto') ('!' ?) (clasimpmod * ) ; - clasimpmod: ('simp' ('add' | 'del' | 'only') | other | + clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' | (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs \end{rail} @@ -414,8 +419,13 @@ modifier arguments correspond to those given in \S\ref{sec:simp} and \S\ref{sec:classical-auto}. Just note that the ones related to the Simplifier are prefixed by \railtoken{simp} here. + + Facts provided by forward chaining are inserted into the goal before doing + the search. The ``!''~argument causes the full context of assumptions to be + included as well. \end{descr} + \subsection{Modifying the context}\label{sec:classical-mod} \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} diff -r 9d319a76dbeb -r d9aef93c0e32 doc-src/IsarRef/hol.tex --- a/doc-src/IsarRef/hol.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/hol.tex Sun Oct 31 15:20:35 1999 +0100 @@ -146,8 +146,8 @@ \end{descr} See \cite{isabelle-HOL} for more information. Note that -$\isarkeyword{inductive_cases}$ corresponds to the ML function -\texttt{mk_cases}. +$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML +function. \section{Proof by induction} diff -r 9d319a76dbeb -r d9aef93c0e32 doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/intro.tex Sun Oct 31 15:20:35 1999 +0100 @@ -149,7 +149,7 @@ \end{tabular} \end{center} -See \texttt{HOL/Isar_examples} for a collection of introductory examples. +See \texttt{HOL/Isar_examples} for a collection of introductory examples, and \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from browsable HTML sources, both sessions provide actual documents (in PDF). diff -r 9d319a76dbeb -r d9aef93c0e32 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/pure.tex Sun Oct 31 15:20:35 1999 +0100 @@ -370,10 +370,9 @@ afterwards. Thus $text$ may actually change the theory as a side effect. \item [$\isarkeyword{setup}~text$] changes the current theory context by - applying setup functions from $text$, which refers to an ML expression of - type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the - canonical way to initialize object-logic specific tools and packages written - in ML. + applying $text$, which refers to an ML expression of type $(theory \to + theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to + initialize object-logic specific tools and packages written in ML. \end{descr} @@ -424,7 +423,7 @@ \section{Proof commands} -Proof commands provide transitions of Isar/VM machine configurations, which +Proof commands perform transitions of Isar/VM machine configurations, which are block-structured, consisting of a stack of nodes with three main components: logical proof context, current facts, and open goals. Isar/VM transitions are \emph{typed} according to the following three three different @@ -434,16 +433,18 @@ to be \emph{proven}; the next command may refine it by some proof method (read: tactic), and enter a sub-proof to establish the actual result. \item [$proof(state)$] is like an internal theory mode: the context may be - augmented by \emph{stating} additional assumptions, intermediate result etc. + augmented by \emph{stating} additional assumptions, intermediate results + etc. \item [$proof(chain)$] is intermediate between $proof(state)$ and - $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just - picked up in order to be used when refining the goal claimed next. + $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' + register) have been just picked up in order to be used when refining the + goal claimed next. \end{descr} \subsection{Proof markup commands}\label{sec:markup-prf} -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect} +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} \indexisarcmd{txt}\indexisarcmd{txt-raw} \begin{matharray}{rcl} \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\ @@ -480,10 +481,10 @@ 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 object that may be used in the subsequent proof as any other variable +a local value that may be used in the subsequent proof as any other variable or constant. Furthermore, any result $\edrv \phi[x]$ exported from the -current context will be universally closed wrt.\ $x$ at the outermost level: -$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables. +context will be universally closed wrt.\ $x$ at the outermost level: $\edrv +\All x \phi$ (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 @@ -497,9 +498,9 @@ user. Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by -combining $\FIX x$ with another kind of assumption that causes any -hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus, -exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. +combining $\FIX x$ with another version of assumption that causes any +hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. +Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. \begin{rail} 'fix' (vars + 'and') comment? @@ -530,7 +531,7 @@ these concatenated. \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}$, with the + $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the resulting hypothetical equation solved by reflexivity. The default name for the definitional equation is $x_def$. @@ -554,7 +555,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 -$this$.\indexisarthm{this} refers to the most recently established facts. +$this$\indexisarthm{this} refers to the most recently established facts. \begin{rail} 'note' thmdef? thmrefs comment? ; @@ -596,8 +597,8 @@ \begin{matharray}{rcl} \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ - \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\ - \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\ + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ \end{matharray} @@ -605,7 +606,7 @@ Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ and $\LEMMANAME$. New local goals may be claimed within proof mode as well. Four variants are available, indicating whether the result is meant to solve -some pending goal and whether forward chaining is employed. +some pending goal or whether forward chaining is employed. \begin{rail} ('theorem' | 'lemma') goal @@ -620,7 +621,7 @@ \begin{descr} \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, eventually resulting in some theorem $\turn \phi$ put back into the theory. -\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as +\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as ``lemma''. \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a theorem with the current assumption context as hypotheses. @@ -655,8 +656,8 @@ goal to a number of sub-goals that are to be solved later. Facts are passed to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. -\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals - completely. No facts are passed to $m@2$. +\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve + remaining goals. No facts are passed to $m@2$. \end{enumerate} The only other proper way to affect pending goals is by $\SHOWNAME$ (or @@ -668,17 +669,19 @@ or constitute some well-understood reduction to new sub-goals. Arbitrary automatic proof tools that are prone leave a large number of badly structured sub-goals are no help in continuing the proof document in any intelligible -way. A much better technique would be to $\SHOWNAME$ some non-trivial -reduction as an explicit rule, which is solved completely by some automated -method, and then applied to some pending goal. +way. +%FIXME +%A more appropriate technique would be to $\SHOWNAME$ some non-trivial +%reduction as an explicit rule, which is solved completely by some automated +%method, and then applied to some pending goal. \medskip 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. There is no -separate default terminal method; in any case the final step is to solve all -remaining goals by assumption, though. +separate default terminal method. In any case, any goals left after that are +solved by assumption as the very last step. \begin{rail} 'proof' interest? meth? comment? @@ -708,8 +711,8 @@ $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it - abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both - methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done + abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, + though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by expanding its definition; in many cases $\PROOF{m@1}$ is already sufficient to see what is going wrong. \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it @@ -717,12 +720,12 @@ \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it abbreviates $\BY{assumption}$. \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake}; - 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, involving some oracle in its internal derivation object - (this is indicated as ``$[!]$'' in the printed result). The main - application of $\isarkeyword{sorry}$ is to support experimentation and - top-down proof development. + provided that the \texttt{quick_and_dirty} flag is enabled, + $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of + course, the result is a fake theorem only, involving some oracle in its + internal derivation object (this is indicated as ``$[!]$'' in the printed + result). The main application of $\isarkeyword{sorry}$ is to support + experimentation and top-down proof development. \end{descr} @@ -772,13 +775,13 @@ \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 $\ISS{p@1 \dots}{p@n}$. In both cases, -higher-order matching is invoked to bind extra-logical term variables, which -may be either named schematic variables of the form $\Var{x}$, or nameless -dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in -the $\LETNAME$ form the patterns occur on the left-hand side, while the -$\ISNAME$ patterns are in postfix position. +or by annotating assumptions or goal statements with a list of patterns +$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to +bind extra-logical term variables, which may be either named schematic +variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' +(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the +patterns occur on the left-hand side, while the $\ISNAME$ patterns are in +postfix position. Term abbreviations are quite different from actual local definitions as introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are @@ -807,7 +810,7 @@ (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its object-logical statement. The latter two abstract over any meta-level -parameters bound by $\Forall$. +parameters. Fact statements resulting from assumptions or finished goals are bound as $\Var{this_prop}$\indexisarvar{this-prop}, @@ -816,7 +819,7 @@ $\Var{this}$ refers to an object-logic statement that is an application $f(t)$, then $t$ is bound to the special text variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of -this feature are calculational proofs (see \S\ref{sec:calculation}). +the latter are calculational proofs (see \S\ref{sec:calculation}). \subsection{Block structure} @@ -834,8 +837,8 @@ again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of different context within a sub-proof may be switched via $\isarkeyword{next}$, which is just a single block-close followed by block-open again. Thus the -effect of $\isarkeyword{next}$ is a local reset the proof -context.\footnote{There is no goal focus involved here!} +effect of $\isarkeyword{next}$ to reset the local proof context. There is no +goal focus involved here! For slightly more advanced applications, there are explicit block parentheses as well. These typically achieve a stronger forward style of reasoning. @@ -887,8 +890,8 @@ specifications are applied to a temporary context derived from the current theory or proof; the result is discarded, i.e.\ attributes involved in $thms$ do not have any permanent effect. -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks - and print terms or propositions according to the current theory or proof +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and + print terms or propositions according to the current theory or proof context; the inferred type of $t$ is output as well. Note that these commands are also useful in inspecting the current environment of term abbreviations. @@ -915,17 +918,16 @@ process. \item [$\isarkeyword{pwd}~$] prints the current working directory. \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, - $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some + $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some theory given as $name$ argument. These commands are basically the same as - the corresponding ML functions\footnote{For historic reasons, the original - ML versions also change the theory context to that of the theory loaded.} - (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar - versions may load new- and old-style theories alike. + the corresponding ML functions\footnote{The ML versions also change the + implicit theory context to that of the theory loaded.} (see also + \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may + load new- and old-style theories alike. \end{descr} -Note that these system commands are scarcely used when working with the -Proof~General interface, since loading of theories is done fully -transparently. +These system commands are scarcely used when working with the Proof~General +interface, since loading of theories is done fully transparently. %%% Local Variables: %%% mode: latex diff -r 9d319a76dbeb -r d9aef93c0e32 doc-src/IsarRef/refcard.tex --- a/doc-src/IsarRef/refcard.tex Sat Oct 30 20:41:30 1999 +0200 +++ b/doc-src/IsarRef/refcard.tex Sun Oct 31 15:20:35 1999 +0100 @@ -14,13 +14,13 @@ $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\ $\BG~\dots~\EN$ & declare explicit blocks \\ $\isarcmd{next}$ & switch implicit blocks \\ - $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\ - $\LET{p = t}$ & \text{abbreviate terms by matching} \\ + $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\ + $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\ \end{tabular} \begin{matharray}{rcl} - theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\ - & \Or & \LEMMA{name}{form}~proof \\ + theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\ + & \Or & \LEMMA{name}{prop}~proof \\ & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex] proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex] stmt & = & \BG~stmt^*~\EN \\ @@ -28,11 +28,11 @@ & \Or & \NOTE{name}{name^+} \\ & \Or & \LET{term = term} \\[0.5ex] & \Or & \FIX{var^+} \\ - & \Or & \ASSUME{name}{form^+}\\ + & \Or & \ASSUME{name}{prop^+}\\ & \Or & \THEN~goal{\dsh}stmt \\ & \Or & goal{\dsh}stmt \\ - goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\ - & \Or & \SHOW{name}{form}~proof \\ + goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\ + & \Or & \SHOW{name}{prop}~proof \\ \end{matharray} @@ -44,8 +44,8 @@ \DOT & \equiv & \BY{assumption} \\ \HENCENAME & \equiv & \THEN~\HAVENAME \\ \THUSNAME & \equiv & \THEN~\SHOWNAME \\ - \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\ - \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex] + \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\ + \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex] \FROM{this} & \equiv & \THEN \\ \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ @@ -67,7 +67,7 @@ \subsection{Diagnostic commands} \begin{matharray}{ll} - \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\ + \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\ \isarcmd{term}~t & \text{print term} \\ \isarcmd{prop}~\phi & \text{print meta-level proposition} \\ \isarcmd{typ}~\tau & \text{print meta-level type} \\ @@ -78,22 +78,22 @@ \begin{tabular}{ll} \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex] - $assumption$ & apply assumption \\ - $rule~a@1~\dots~a@n$ & apply some rule \\ + $assumption$ & apply some assumption \\ + $rule~a@1\;\dots\;a@n$ & apply some rule \\ $rule$ & apply standard rule (default for $\PROOFNAME$) \\ $induct~x$ & apply induction rule \\ - $contradiction$ & apply $\neg{}$ elimination rule \\[2ex] + $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex] \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex] $-$ & \text{no rules} \\ - $intro~a@1~\dots~a@n$ & \text{introduction rules} \\ - $elim~a@1~\dots~a@n$ & \text{elimination rules} \\ - $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex] + $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\ + $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\ + $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex] \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] $simp$ & Simplifier \\ - $blast$, $fast$ & Classical reasoner \\ - $force$, $auto$ & Simplifier + Classical reasoner \\ + $blast$, $fast$ & Classical Reasoner \\ + $force$, $auto$ & Simplifier + Classical Reasoner \\ $arith$ & Arithmetic procedure \\ \end{tabular} @@ -102,8 +102,8 @@ \begin{tabular}{ll} \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex] - $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\ - $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\ + $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\ + $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\ $RS~b$ & resolve fact with rule \\ $standard$ & put into standard result form \\ $rulify$ & put into object-rule form \\ @@ -111,12 +111,11 @@ \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex] $simp$ & declare Simplifier rules \\ - $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\ - $iff$ & declare Simplifier + Classical reasoner rules \\ - $trans$ & calculational rules (general transitivity) \\ + $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\ + $iff$ & declare Simplifier + Classical Reasoner rules \\ + $trans$ & declare calculational rules (general transitivity) \\ \end{tabular} - %%% Local Variables: %%% mode: latex %%% TeX-master: "isar-ref"