1.1 --- a/doc-src/IsarRef/generic.tex Sat Oct 30 20:41:30 1999 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex Sun Oct 31 15:20:35 1999 +0100
1.3 @@ -37,9 +37,9 @@
1.4 becomes a (generalized) \emph{elimination}.
1.5
1.6 Note that the classical reasoner introduces another version of $rule$ that
1.7 - is able to pick appropriate rules automatically, whenever explicit $thms$
1.8 - are omitted (see \S\ref{sec:classical-basic}); that method is the default
1.9 - for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
1.10 + is able to pick appropriate rules automatically, whenever $thms$ are omitted
1.11 + (see \S\ref{sec:classical-basic}); that method is the default for
1.12 + $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates
1.13 $\BY{default}$.
1.14 \item [$erule~thms$] is similar to $rule$, but applies rules by
1.15 elim-resolution. This is an improper method, mainly for experimentation and
1.16 @@ -47,11 +47,11 @@
1.17 $rule$ (single step, involving facts) or $elim$ (repeated steps, see
1.18 \S\ref{sec:classical-basic}).
1.19 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
1.20 - meta-level definitions throughout all goals; any facts provided are
1.21 - \emph{ignored}.
1.22 -\item [$succeed$] yields a single (unchanged) result; it is the identify of
1.23 + meta-level definitions throughout all goals; any facts provided are inserted
1.24 + into the goal and subject to rewriting as well.
1.25 +\item [$succeed$] yields a single (unchanged) result; it is the identity of
1.26 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
1.27 -\item [$fail$] yields an empty result sequence; it is the identify of the
1.28 +\item [$fail$] yields an empty result sequence; it is the identity of the
1.29 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
1.30 \end{descr}
1.31
1.32 @@ -98,12 +98,12 @@
1.33 result).
1.34 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies
1.35 $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
1.36 - the reversed order). Note that premises may be skipped by including $\_$
1.37 - (underscore) as argument.
1.38 + the reversed order). Note that premises may be skipped by including
1.39 + ``$\_$'' (underscore) as argument.
1.40
1.41 $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
1.42 - that does not include the automatic lifting process that is normally
1.43 - intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
1.44 + that skips the automatic lifting process that is normally intended (cf.\
1.45 + \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
1.46
1.47 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
1.48 instantiation, respectively. The terms given in $of$ are substituted for
1.49 @@ -180,9 +180,10 @@
1.50 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
1.51 $\ALSO$, and concludes the current calculational thread. The final result
1.52 is exhibited as fact for forward chaining towards the next goal. Basically,
1.53 - $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof
1.54 - idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
1.55 - ``$\FINALLY~\HAVE{}{\phi}~\DOT$''.
1.56 + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
1.57 + ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
1.58 + ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
1.59 + calculational proofs.
1.60
1.61 \item [$trans$] maintains the set of transitivity rules of the theory or proof
1.62 context, by adding or deleting theorems (the default is to add).
1.63 @@ -204,12 +205,12 @@
1.64 intro_classes & : & \isarmeth \\
1.65 \end{matharray}
1.66
1.67 -Axiomatic type classes are provided by Isabelle/Pure as a purely
1.68 -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
1.69 -any object logic may make use of this light-weight mechanism for abstract
1.70 -theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
1.71 -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
1.72 -the standard Isabelle documentation.
1.73 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
1.74 +interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
1.75 +may make use of this light-weight mechanism of abstract theories. See
1.76 +\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on
1.77 +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
1.78 +Isabelle documentation.
1.79 %FIXME cite
1.80
1.81 \begin{rail}
1.82 @@ -225,21 +226,22 @@
1.83 holding. Class axioms may not contain more than one type variable. The
1.84 class axioms (with implicit sort constraints added) are bound to the given
1.85 names. Furthermore a class introduction rule is generated, which is
1.86 - employed by method $intro_classes$ in support instantiation proofs of this
1.87 + employed by method $intro_classes$ to support instantiation proofs of this
1.88 class.
1.89
1.90 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
1.91 (\vec s)c$] setup up a goal stating the class relation or type arity. The
1.92 - proof would usually proceed by the $intro_classes$ method, and then
1.93 - establish the characteristic theorems of the type classes involved. After
1.94 - finishing the proof the theory will be augmented by a type signature
1.95 - declaration corresponding to the resulting theorem.
1.96 -\item [$intro_classes$] repeatedly expands the class introduction rules of
1.97 + proof would usually proceed by $intro_classes$, and then establish the
1.98 + characteristic theorems of the type classes involved. After finishing the
1.99 + proof, the theory will be augmented by a type signature declaration
1.100 + corresponding to the resulting theorem.
1.101 +\item [$intro_classes$] repeatedly expands all class introduction rules of
1.102 this theory.
1.103 \end{descr}
1.104
1.105 -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
1.106 -axiomatic type classes, including instantiation proofs.
1.107 +%FIXME
1.108 +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
1.109 +%axiomatic type classes, including instantiation proofs.
1.110
1.111
1.112 \section{The Simplifier}
1.113 @@ -345,7 +347,7 @@
1.114 given ones may be applied. The latter form admits better control of what
1.115 actually happens, thus it is very appropriate as an initial method for
1.116 $\PROOFNAME$ that splits up certain connectives of the goal, before entering
1.117 - the actual proof.
1.118 + the actual sub-proof.
1.119
1.120 \item [$contradiction$] solves some goal by contradiction, deriving any result
1.121 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
1.122 @@ -388,7 +390,10 @@
1.123
1.124 Any of above methods support additional modifiers of the context of classical
1.125 rules. There semantics is analogous to the attributes given in
1.126 -\S\ref{sec:classical-mod}.
1.127 +\S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted
1.128 +into the goal before doing the search. The ``!''~argument causes the full
1.129 +context of assumptions to be included as well.\footnote{This is slightly less
1.130 + hazardous than for the Simplifier (see \S\ref{sec:simp}).}
1.131
1.132
1.133 \subsection{Combined automated methods}
1.134 @@ -403,7 +408,7 @@
1.135 ('force' | 'auto') ('!' ?) (clasimpmod * )
1.136 ;
1.137
1.138 - clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
1.139 + clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
1.140 (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
1.141 \end{rail}
1.142
1.143 @@ -414,8 +419,13 @@
1.144 modifier arguments correspond to those given in \S\ref{sec:simp} and
1.145 \S\ref{sec:classical-auto}. Just note that the ones related to the
1.146 Simplifier are prefixed by \railtoken{simp} here.
1.147 +
1.148 + Facts provided by forward chaining are inserted into the goal before doing
1.149 + the search. The ``!''~argument causes the full context of assumptions to be
1.150 + included as well.
1.151 \end{descr}
1.152
1.153 +
1.154 \subsection{Modifying the context}\label{sec:classical-mod}
1.155
1.156 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
2.1 --- a/doc-src/IsarRef/hol.tex Sat Oct 30 20:41:30 1999 +0200
2.2 +++ b/doc-src/IsarRef/hol.tex Sun Oct 31 15:20:35 1999 +0100
2.3 @@ -146,8 +146,8 @@
2.4 \end{descr}
2.5
2.6 See \cite{isabelle-HOL} for more information. Note that
2.7 -$\isarkeyword{inductive_cases}$ corresponds to the ML function
2.8 -\texttt{mk_cases}.
2.9 +$\isarkeyword{inductive_cases}$ corresponds to the \texttt{mk_cases} ML
2.10 +function.
2.11
2.12
2.13 \section{Proof by induction}
3.1 --- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:41:30 1999 +0200
3.2 +++ b/doc-src/IsarRef/intro.tex Sun Oct 31 15:20:35 1999 +0100
3.3 @@ -149,7 +149,7 @@
3.4 \end{tabular}
3.5 \end{center}
3.6
3.7 -See \texttt{HOL/Isar_examples} for a collection of introductory examples.
3.8 +See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
3.9 \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
3.10 browsable HTML sources, both sessions provide actual documents (in PDF).
3.11
4.1 --- a/doc-src/IsarRef/pure.tex Sat Oct 30 20:41:30 1999 +0200
4.2 +++ b/doc-src/IsarRef/pure.tex Sun Oct 31 15:20:35 1999 +0100
4.3 @@ -370,10 +370,9 @@
4.4 afterwards. Thus $text$ may actually change the theory as a side effect.
4.5
4.6 \item [$\isarkeyword{setup}~text$] changes the current theory context by
4.7 - applying setup functions from $text$, which refers to an ML expression of
4.8 - type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the
4.9 - canonical way to initialize object-logic specific tools and packages written
4.10 - in ML.
4.11 + applying $text$, which refers to an ML expression of type $(theory \to
4.12 + theory)~list$. The $\isarkeyword{setup}$ command is the canonical way to
4.13 + initialize object-logic specific tools and packages written in ML.
4.14 \end{descr}
4.15
4.16
4.17 @@ -424,7 +423,7 @@
4.18
4.19 \section{Proof commands}
4.20
4.21 -Proof commands provide transitions of Isar/VM machine configurations, which
4.22 +Proof commands perform transitions of Isar/VM machine configurations, which
4.23 are block-structured, consisting of a stack of nodes with three main
4.24 components: logical proof context, current facts, and open goals. Isar/VM
4.25 transitions are \emph{typed} according to the following three three different
4.26 @@ -434,16 +433,18 @@
4.27 to be \emph{proven}; the next command may refine it by some proof method
4.28 (read: tactic), and enter a sub-proof to establish the actual result.
4.29 \item [$proof(state)$] is like an internal theory mode: the context may be
4.30 - augmented by \emph{stating} additional assumptions, intermediate result etc.
4.31 + augmented by \emph{stating} additional assumptions, intermediate results
4.32 + etc.
4.33 \item [$proof(chain)$] is intermediate between $proof(state)$ and
4.34 - $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
4.35 - picked up in order to be used when refining the goal claimed next.
4.36 + $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
4.37 + register) have been just picked up in order to be used when refining the
4.38 + goal claimed next.
4.39 \end{descr}
4.40
4.41
4.42 \subsection{Proof markup commands}\label{sec:markup-prf}
4.43
4.44 -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
4.45 +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
4.46 \indexisarcmd{txt}\indexisarcmd{txt-raw}
4.47 \begin{matharray}{rcl}
4.48 \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
4.49 @@ -480,10 +481,10 @@
4.50 former closely correspond to Skolem constants, or meta-level universal
4.51 quantification as provided by the Isabelle/Pure logical framework.
4.52 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
4.53 -a local object that may be used in the subsequent proof as any other variable
4.54 +a local value that may be used in the subsequent proof as any other variable
4.55 or constant. Furthermore, any result $\edrv \phi[x]$ exported from the
4.56 -current context will be universally closed wrt.\ $x$ at the outermost level:
4.57 -$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
4.58 +context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
4.59 +\All x \phi$ (this is expressed using Isabelle's meta-variables).
4.60
4.61 Similarly, introducing some assumption $\chi$ has two effects. On the one
4.62 hand, a local theorem is created that may be used as a fact in subsequent
4.63 @@ -497,9 +498,9 @@
4.64 user.
4.65
4.66 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
4.67 -combining $\FIX x$ with another kind of assumption that causes any
4.68 -hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus,
4.69 -exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
4.70 +combining $\FIX x$ with another version of assumption that causes any
4.71 +hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
4.72 +Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
4.73
4.74 \begin{rail}
4.75 'fix' (vars + 'and') comment?
4.76 @@ -530,7 +531,7 @@
4.77 these concatenated.
4.78 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
4.79 In results exported from the context, $x$ is replaced by $t$. Basically,
4.80 - $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
4.81 + $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
4.82 resulting hypothetical equation solved by reflexivity.
4.83
4.84 The default name for the definitional equation is $x_def$.
4.85 @@ -554,7 +555,7 @@
4.86 Any fact will usually be involved in further proofs, either as explicit
4.87 arguments of proof methods or when forward chaining towards the next goal via
4.88 $\THEN$ (and variants). Note that the special theorem name
4.89 -$this$.\indexisarthm{this} refers to the most recently established facts.
4.90 +$this$\indexisarthm{this} refers to the most recently established facts.
4.91 \begin{rail}
4.92 'note' thmdef? thmrefs comment?
4.93 ;
4.94 @@ -596,8 +597,8 @@
4.95 \begin{matharray}{rcl}
4.96 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
4.97 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
4.98 - \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
4.99 - \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
4.100 + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
4.101 + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
4.102 \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
4.103 \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
4.104 \end{matharray}
4.105 @@ -605,7 +606,7 @@
4.106 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
4.107 and $\LEMMANAME$. New local goals may be claimed within proof mode as well.
4.108 Four variants are available, indicating whether the result is meant to solve
4.109 -some pending goal and whether forward chaining is employed.
4.110 +some pending goal or whether forward chaining is employed.
4.111
4.112 \begin{rail}
4.113 ('theorem' | 'lemma') goal
4.114 @@ -620,7 +621,7 @@
4.115 \begin{descr}
4.116 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
4.117 eventually resulting in some theorem $\turn \phi$ put back into the theory.
4.118 -\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
4.119 +\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
4.120 ``lemma''.
4.121 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
4.122 theorem with the current assumption context as hypotheses.
4.123 @@ -655,8 +656,8 @@
4.124 goal to a number of sub-goals that are to be solved later. Facts are passed
4.125 to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
4.126
4.127 -\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
4.128 - completely. No facts are passed to $m@2$.
4.129 +\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
4.130 + remaining goals. No facts are passed to $m@2$.
4.131 \end{enumerate}
4.132
4.133 The only other proper way to affect pending goals is by $\SHOWNAME$ (or
4.134 @@ -668,17 +669,19 @@
4.135 or constitute some well-understood reduction to new sub-goals. Arbitrary
4.136 automatic proof tools that are prone leave a large number of badly structured
4.137 sub-goals are no help in continuing the proof document in any intelligible
4.138 -way. A much better technique would be to $\SHOWNAME$ some non-trivial
4.139 -reduction as an explicit rule, which is solved completely by some automated
4.140 -method, and then applied to some pending goal.
4.141 +way.
4.142 +%FIXME
4.143 +%A more appropriate technique would be to $\SHOWNAME$ some non-trivial
4.144 +%reduction as an explicit rule, which is solved completely by some automated
4.145 +%method, and then applied to some pending goal.
4.146
4.147 \medskip
4.148
4.149 Unless given explicitly by the user, the default initial method is
4.150 ``$default$'', which is usually set up to apply a single standard elimination
4.151 or introduction rule according to the topmost symbol involved. There is no
4.152 -separate default terminal method; in any case the final step is to solve all
4.153 -remaining goals by assumption, though.
4.154 +separate default terminal method. In any case, any goals left after that are
4.155 +solved by assumption as the very last step.
4.156
4.157 \begin{rail}
4.158 'proof' interest? meth? comment?
4.159 @@ -708,8 +711,8 @@
4.160 $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
4.161 some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
4.162 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
4.163 - abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
4.164 - methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
4.165 + abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
4.166 + though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
4.167 by expanding its definition; in many cases $\PROOF{m@1}$ is already
4.168 sufficient to see what is going wrong.
4.169 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
4.170 @@ -717,12 +720,12 @@
4.171 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
4.172 abbreviates $\BY{assumption}$.
4.173 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
4.174 - provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
4.175 - pretends to solve the goal without further ado. Of course, the result is a
4.176 - fake theorem only, involving some oracle in its internal derivation object
4.177 - (this is indicated as ``$[!]$'' in the printed result). The main
4.178 - application of $\isarkeyword{sorry}$ is to support experimentation and
4.179 - top-down proof development.
4.180 + provided that the \texttt{quick_and_dirty} flag is enabled,
4.181 + $\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of
4.182 + course, the result is a fake theorem only, involving some oracle in its
4.183 + internal derivation object (this is indicated as ``$[!]$'' in the printed
4.184 + result). The main application of $\isarkeyword{sorry}$ is to support
4.185 + experimentation and top-down proof development.
4.186 \end{descr}
4.187
4.188
4.189 @@ -772,13 +775,13 @@
4.190 \end{matharray}
4.191
4.192 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
4.193 -or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
4.194 -etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases,
4.195 -higher-order matching is invoked to bind extra-logical term variables, which
4.196 -may be either named schematic variables of the form $\Var{x}$, or nameless
4.197 -dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
4.198 -the $\LETNAME$ form the patterns occur on the left-hand side, while the
4.199 -$\ISNAME$ patterns are in postfix position.
4.200 +or by annotating assumptions or goal statements with a list of patterns
4.201 +$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to
4.202 +bind extra-logical term variables, which may be either named schematic
4.203 +variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
4.204 +(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
4.205 +patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
4.206 +postfix position.
4.207
4.208 Term abbreviations are quite different from actual local definitions as
4.209 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
4.210 @@ -807,7 +810,7 @@
4.211 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
4.212 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
4.213 object-logical statement. The latter two abstract over any meta-level
4.214 -parameters bound by $\Forall$.
4.215 +parameters.
4.216
4.217 Fact statements resulting from assumptions or finished goals are bound as
4.218 $\Var{this_prop}$\indexisarvar{this-prop},
4.219 @@ -816,7 +819,7 @@
4.220 $\Var{this}$ refers to an object-logic statement that is an application
4.221 $f(t)$, then $t$ is bound to the special text variable
4.222 ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
4.223 -this feature are calculational proofs (see \S\ref{sec:calculation}).
4.224 +the latter are calculational proofs (see \S\ref{sec:calculation}).
4.225
4.226
4.227 \subsection{Block structure}
4.228 @@ -834,8 +837,8 @@
4.229 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
4.230 different context within a sub-proof may be switched via $\isarkeyword{next}$,
4.231 which is just a single block-close followed by block-open again. Thus the
4.232 -effect of $\isarkeyword{next}$ is a local reset the proof
4.233 -context.\footnote{There is no goal focus involved here!}
4.234 +effect of $\isarkeyword{next}$ to reset the local proof context. There is no
4.235 +goal focus involved here!
4.236
4.237 For slightly more advanced applications, there are explicit block parentheses
4.238 as well. These typically achieve a stronger forward style of reasoning.
4.239 @@ -887,8 +890,8 @@
4.240 specifications are applied to a temporary context derived from the current
4.241 theory or proof; the result is discarded, i.e.\ attributes involved in
4.242 $thms$ do not have any permanent effect.
4.243 -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
4.244 - and print terms or propositions according to the current theory or proof
4.245 +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
4.246 + print terms or propositions according to the current theory or proof
4.247 context; the inferred type of $t$ is output as well. Note that these
4.248 commands are also useful in inspecting the current environment of term
4.249 abbreviations.
4.250 @@ -915,17 +918,16 @@
4.251 process.
4.252 \item [$\isarkeyword{pwd}~$] prints the current working directory.
4.253 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
4.254 - $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
4.255 + $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
4.256 theory given as $name$ argument. These commands are basically the same as
4.257 - the corresponding ML functions\footnote{For historic reasons, the original
4.258 - ML versions also change the theory context to that of the theory loaded.}
4.259 - (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar
4.260 - versions may load new- and old-style theories alike.
4.261 + the corresponding ML functions\footnote{The ML versions also change the
4.262 + implicit theory context to that of the theory loaded.} (see also
4.263 + \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may
4.264 + load new- and old-style theories alike.
4.265 \end{descr}
4.266
4.267 -Note that these system commands are scarcely used when working with the
4.268 -Proof~General interface, since loading of theories is done fully
4.269 -transparently.
4.270 +These system commands are scarcely used when working with the Proof~General
4.271 +interface, since loading of theories is done fully transparently.
4.272
4.273 %%% Local Variables:
4.274 %%% mode: latex
5.1 --- a/doc-src/IsarRef/refcard.tex Sat Oct 30 20:41:30 1999 +0200
5.2 +++ b/doc-src/IsarRef/refcard.tex Sun Oct 31 15:20:35 1999 +0100
5.3 @@ -14,13 +14,13 @@
5.4 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
5.5 $\BG~\dots~\EN$ & declare explicit blocks \\
5.6 $\isarcmd{next}$ & switch implicit blocks \\
5.7 - $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
5.8 - $\LET{p = t}$ & \text{abbreviate terms by matching} \\
5.9 + $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
5.10 + $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
5.11 \end{tabular}
5.12
5.13 \begin{matharray}{rcl}
5.14 - theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
5.15 - & \Or & \LEMMA{name}{form}~proof \\
5.16 + theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
5.17 + & \Or & \LEMMA{name}{prop}~proof \\
5.18 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
5.19 proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
5.20 stmt & = & \BG~stmt^*~\EN \\
5.21 @@ -28,11 +28,11 @@
5.22 & \Or & \NOTE{name}{name^+} \\
5.23 & \Or & \LET{term = term} \\[0.5ex]
5.24 & \Or & \FIX{var^+} \\
5.25 - & \Or & \ASSUME{name}{form^+}\\
5.26 + & \Or & \ASSUME{name}{prop^+}\\
5.27 & \Or & \THEN~goal{\dsh}stmt \\
5.28 & \Or & goal{\dsh}stmt \\
5.29 - goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
5.30 - & \Or & \SHOW{name}{form}~proof \\
5.31 + goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
5.32 + & \Or & \SHOW{name}{prop}~proof \\
5.33 \end{matharray}
5.34
5.35
5.36 @@ -44,8 +44,8 @@
5.37 \DOT & \equiv & \BY{assumption} \\
5.38 \HENCENAME & \equiv & \THEN~\HAVENAME \\
5.39 \THUSNAME & \equiv & \THEN~\SHOWNAME \\
5.40 - \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
5.41 - \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
5.42 + \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
5.43 + \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
5.44 \FROM{this} & \equiv & \THEN \\
5.45 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
5.46 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
5.47 @@ -67,7 +67,7 @@
5.48 \subsection{Diagnostic commands}
5.49
5.50 \begin{matharray}{ll}
5.51 - \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
5.52 + \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
5.53 \isarcmd{term}~t & \text{print term} \\
5.54 \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
5.55 \isarcmd{typ}~\tau & \text{print meta-level type} \\
5.56 @@ -78,22 +78,22 @@
5.57
5.58 \begin{tabular}{ll}
5.59 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
5.60 - $assumption$ & apply assumption \\
5.61 - $rule~a@1~\dots~a@n$ & apply some rule \\
5.62 + $assumption$ & apply some assumption \\
5.63 + $rule~a@1\;\dots\;a@n$ & apply some rule \\
5.64 $rule$ & apply standard rule (default for $\PROOFNAME$) \\
5.65 $induct~x$ & apply induction rule \\
5.66 - $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
5.67 + $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
5.68
5.69 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
5.70 $-$ & \text{no rules} \\
5.71 - $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
5.72 - $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
5.73 - $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
5.74 + $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
5.75 + $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
5.76 + $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
5.77
5.78 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
5.79 $simp$ & Simplifier \\
5.80 - $blast$, $fast$ & Classical reasoner \\
5.81 - $force$, $auto$ & Simplifier + Classical reasoner \\
5.82 + $blast$, $fast$ & Classical Reasoner \\
5.83 + $force$, $auto$ & Simplifier + Classical Reasoner \\
5.84 $arith$ & Arithmetic procedure \\
5.85 \end{tabular}
5.86
5.87 @@ -102,8 +102,8 @@
5.88
5.89 \begin{tabular}{ll}
5.90 \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
5.91 - $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
5.92 - $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
5.93 + $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
5.94 + $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\
5.95 $RS~b$ & resolve fact with rule \\
5.96 $standard$ & put into standard result form \\
5.97 $rulify$ & put into object-rule form \\
5.98 @@ -111,12 +111,11 @@
5.99
5.100 \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
5.101 $simp$ & declare Simplifier rules \\
5.102 - $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
5.103 - $iff$ & declare Simplifier + Classical reasoner rules \\
5.104 - $trans$ & calculational rules (general transitivity) \\
5.105 + $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
5.106 + $iff$ & declare Simplifier + Classical Reasoner rules \\
5.107 + $trans$ & declare calculational rules (general transitivity) \\
5.108 \end{tabular}
5.109
5.110 -
5.111 %%% Local Variables:
5.112 %%% mode: latex
5.113 %%% TeX-master: "isar-ref"