doc-src/IsarRef/pure.tex
 changeset 7987 d9aef93c0e32 parent 7981 5120a2a15d06 child 7988 feea893b47c7
     1.1 --- a/doc-src/IsarRef/pure.tex	Sat Oct 30 20:41:30 1999 +0200
1.2 +++ b/doc-src/IsarRef/pure.tex	Sun Oct 31 15:20:35 1999 +0100
1.3 @@ -370,10 +370,9 @@
1.4    afterwards.  Thus $text$ may actually change the theory as a side effect.
1.5
1.6  \item [$\isarkeyword{setup}~text$] changes the current theory context by
1.7 -  applying setup functions from $text$, which refers to an ML expression of
1.8 -  type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the
1.9 -  canonical way to initialize object-logic specific tools and packages written
1.10 -  in ML.
1.11 +  applying $text$, which refers to an ML expression of type $(theory \to 1.12 + theory)~list$.  The $\isarkeyword{setup}$ command is the canonical way to
1.13 +  initialize object-logic specific tools and packages written in ML.
1.14  \end{descr}
1.15
1.16
1.17 @@ -424,7 +423,7 @@
1.18
1.19  \section{Proof commands}
1.20
1.21 -Proof commands provide transitions of Isar/VM machine configurations, which
1.22 +Proof commands perform transitions of Isar/VM machine configurations, which
1.23  are block-structured, consisting of a stack of nodes with three main
1.24  components: logical proof context, current facts, and open goals.  Isar/VM
1.25  transitions are \emph{typed} according to the following three three different
1.26 @@ -434,16 +433,18 @@
1.27    to be \emph{proven}; the next command may refine it by some proof method
1.28    (read: tactic), and enter a sub-proof to establish the actual result.
1.29  \item [$proof(state)$] is like an internal theory mode: the context may be
1.30 -  augmented by \emph{stating} additional assumptions, intermediate result etc.
1.31 +  augmented by \emph{stating} additional assumptions, intermediate results
1.32 +  etc.
1.33  \item [$proof(chain)$] is intermediate between $proof(state)$ and
1.34 -  $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
1.35 -  picked up in order to be used when refining the goal claimed next.
1.36 +  $proof(prove)$: existing facts (i.e.\ the contents of the special $this$''
1.37 +  register) have been just picked up in order to be used when refining the
1.38 +  goal claimed next.
1.39  \end{descr}
1.40
1.41
1.42  \subsection{Proof markup commands}\label{sec:markup-prf}
1.43
1.44 -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
1.45 +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
1.46  \indexisarcmd{txt}\indexisarcmd{txt-raw}
1.47  \begin{matharray}{rcl}
1.48    \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
1.49 @@ -480,10 +481,10 @@
1.50  former closely correspond to Skolem constants, or meta-level universal
1.51  quantification as provided by the Isabelle/Pure logical framework.
1.52  Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
1.53 -a local object that may be used in the subsequent proof as any other variable
1.54 +a local value that may be used in the subsequent proof as any other variable
1.55  or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
1.56 -current context will be universally closed wrt.\ $x$ at the outermost level:
1.57 -$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
1.58 +context will be universally closed wrt.\ $x$ at the outermost level: $\edrv 1.59 +\All x \phi$ (this is expressed using Isabelle's meta-variables).
1.60
1.61  Similarly, introducing some assumption $\chi$ has two effects.  On the one
1.62  hand, a local theorem is created that may be used as a fact in subsequent
1.63 @@ -497,9 +498,9 @@
1.64  user.
1.65
1.66  Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
1.67 -combining $\FIX x$ with another kind of assumption that causes any
1.68 -hypothetical equation $x \equiv t$ to be eliminated by reflexivity.  Thus,
1.69 -exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
1.70 +combining $\FIX x$ with another version of assumption that causes any
1.71 +hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
1.72 +Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
1.73
1.74  \begin{rail}
1.75    'fix' (vars + 'and') comment?
1.76 @@ -530,7 +531,7 @@
1.77    these concatenated.
1.78  \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
1.79    In results exported from the context, $x$ is replaced by $t$.  Basically,
1.80 -  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
1.81 +  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
1.82    resulting hypothetical equation solved by reflexivity.
1.83
1.84    The default name for the definitional equation is $x_def$.
1.85 @@ -554,7 +555,7 @@
1.86  Any fact will usually be involved in further proofs, either as explicit
1.87  arguments of proof methods or when forward chaining towards the next goal via
1.88  $\THEN$ (and variants).  Note that the special theorem name
1.89 -$this$.\indexisarthm{this} refers to the most recently established facts.
1.90 +$this$\indexisarthm{this} refers to the most recently established facts.
1.91  \begin{rail}
1.92    'note' thmdef? thmrefs comment?
1.93    ;
1.94 @@ -596,8 +597,8 @@
1.95  \begin{matharray}{rcl}
1.96    \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
1.97    \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
1.98 -  \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
1.99 -  \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
1.100 +  \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.101 +  \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
1.102    \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
1.103    \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
1.104  \end{matharray}
1.105 @@ -605,7 +606,7 @@
1.106  Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
1.107  and $\LEMMANAME$.  New local goals may be claimed within proof mode as well.
1.108  Four variants are available, indicating whether the result is meant to solve
1.109 -some pending goal and whether forward chaining is employed.
1.110 +some pending goal or whether forward chaining is employed.
1.111
1.112  \begin{rail}
1.113    ('theorem' | 'lemma') goal
1.114 @@ -620,7 +621,7 @@
1.115  \begin{descr}
1.116  \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
1.117    eventually resulting in some theorem $\turn \phi$ put back into the theory.
1.118 -\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
1.119 +\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
1.120    lemma''.
1.121  \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
1.122    theorem with the current assumption context as hypotheses.
1.123 @@ -655,8 +656,8 @@
1.124    goal to a number of sub-goals that are to be solved later.  Facts are passed
1.125    to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
1.126
1.127 -\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
1.128 -  completely.  No facts are passed to $m@2$.
1.129 +\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
1.130 +  remaining goals.  No facts are passed to $m@2$.
1.131  \end{enumerate}
1.132
1.133  The only other proper way to affect pending goals is by $\SHOWNAME$ (or
1.134 @@ -668,17 +669,19 @@
1.135  or constitute some well-understood reduction to new sub-goals.  Arbitrary
1.136  automatic proof tools that are prone leave a large number of badly structured
1.137  sub-goals are no help in continuing the proof document in any intelligible
1.138 -way.  A much better technique would be to $\SHOWNAME$ some non-trivial
1.139 -reduction as an explicit rule, which is solved completely by some automated
1.140 -method, and then applied to some pending goal.
1.141 +way.
1.142 +%FIXME
1.143 +%A more appropriate technique would be to $\SHOWNAME$ some non-trivial
1.144 +%reduction as an explicit rule, which is solved completely by some automated
1.145 +%method, and then applied to some pending goal.
1.146
1.147  \medskip
1.148
1.149  Unless given explicitly by the user, the default initial method is
1.150  $default$'', which is usually set up to apply a single standard elimination
1.151  or introduction rule according to the topmost symbol involved.  There is no
1.152 -separate default terminal method; in any case the final step is to solve all
1.153 -remaining goals by assumption, though.
1.154 +separate default terminal method.  In any case, any goals left after that are
1.155 +solved by assumption as the very last step.
1.156
1.157  \begin{rail}
1.158    'proof' interest? meth? comment?
1.159 @@ -708,8 +711,8 @@
1.160    $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
1.161    some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
1.162  \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
1.163 -  abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
1.164 -  methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
1.165 +  abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
1.166 +  though.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
1.167    by expanding its definition; in many cases $\PROOF{m@1}$ is already
1.168    sufficient to see what is going wrong.
1.169  \item [$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
1.170 @@ -717,12 +720,12 @@
1.171  \item [$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
1.172    abbreviates $\BY{assumption}$.
1.173  \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
1.174 -  provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
1.175 -  pretends to solve the goal without further ado.  Of course, the result is a
1.176 -  fake theorem only, involving some oracle in its internal derivation object
1.177 -  (this is indicated as $[!]$'' in the printed result).  The main
1.178 -  application of $\isarkeyword{sorry}$ is to support experimentation and
1.179 -  top-down proof development.
1.180 +  provided that the \texttt{quick_and_dirty} flag is enabled,
1.181 +  $\isarkeyword{sorry}$ pretends to solve the goal without further ado.  Of
1.182 +  course, the result is a fake theorem only, involving some oracle in its
1.183 +  internal derivation object (this is indicated as $[!]$'' in the printed
1.184 +  result).  The main application of $\isarkeyword{sorry}$ is to support
1.185 +  experimentation and top-down proof development.
1.186  \end{descr}
1.187
1.188
1.189 @@ -772,13 +775,13 @@
1.190  \end{matharray}
1.191
1.192  Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
1.193 -or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
1.194 -etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$.  In both cases,
1.195 -higher-order matching is invoked to bind extra-logical term variables, which
1.196 -may be either named schematic variables of the form $\Var{x}$, or nameless
1.197 -dummies \texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
1.198 -the $\LETNAME$ form the patterns occur on the left-hand side, while the
1.199 -$\ISNAME$ patterns are in postfix position.
1.200 +or by annotating assumptions or goal statements with a list of patterns
1.201 +$\ISS{p@1\;\dots}{p@n}$.  In both cases, higher-order matching is invoked to
1.202 +bind extra-logical term variables, which may be either named schematic
1.203 +variables of the form $\Var{x}$, or nameless dummies \texttt{_}''
1.204 +(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
1.205 +patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
1.206 +postfix position.
1.207
1.208  Term abbreviations are quite different from actual local definitions as
1.209  introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
1.210 @@ -807,7 +810,7 @@
1.211  (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
1.212  (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
1.213  object-logical statement.  The latter two abstract over any meta-level
1.214 -parameters bound by $\Forall$.
1.215 +parameters.
1.216
1.217  Fact statements resulting from assumptions or finished goals are bound as
1.218  $\Var{this_prop}$\indexisarvar{this-prop},
1.219 @@ -816,7 +819,7 @@
1.220  $\Var{this}$ refers to an object-logic statement that is an application
1.221  $f(t)$, then $t$ is bound to the special text variable
1.222  $\dots$''\indexisarvar{\dots} (three dots).  The canonical application of
1.223 -this feature are calculational proofs (see \S\ref{sec:calculation}).
1.224 +the latter are calculational proofs (see \S\ref{sec:calculation}).
1.225
1.226
1.227  \subsection{Block structure}
1.228 @@ -834,8 +837,8 @@
1.229  again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
1.230  different context within a sub-proof may be switched via $\isarkeyword{next}$,
1.231  which is just a single block-close followed by block-open again.  Thus the
1.232 -effect of $\isarkeyword{next}$ is a local reset the proof
1.233 -context.\footnote{There is no goal focus involved here!}
1.234 +effect of $\isarkeyword{next}$ to reset the local proof context. There is no
1.235 +goal focus involved here!
1.236
1.237  For slightly more advanced applications, there are explicit block parentheses
1.238  as well.  These typically achieve a stronger forward style of reasoning.
1.239 @@ -887,8 +890,8 @@
1.240    specifications are applied to a temporary context derived from the current
1.241    theory or proof; the result is discarded, i.e.\ attributes involved in
1.242    $thms$ do not have any permanent effect.
1.243 -\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
1.244 -  and print terms or propositions according to the current theory or proof
1.245 +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
1.246 +  print terms or propositions according to the current theory or proof
1.247    context; the inferred type of $t$ is output as well.  Note that these
1.248    commands are also useful in inspecting the current environment of term
1.249    abbreviations.
1.250 @@ -915,17 +918,16 @@
1.251    process.
1.252  \item [$\isarkeyword{pwd}~$] prints the current working directory.
1.253  \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
1.254 -  $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
1.255 +  $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
1.256    theory given as $name$ argument.  These commands are basically the same as
1.257 -  the corresponding ML functions\footnote{For historic reasons, the original
1.258 -    ML versions also change the theory context to that of the theory loaded.}
1.259 -  (see also \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar
1.260 -  versions may load new- and old-style theories alike.
1.261 +  the corresponding ML functions\footnote{The ML versions also change the