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
   1.262 +    implicit theory context to that of the theory loaded.}  (see also
   1.263 +  \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
   1.264 +  load new- and old-style theories alike.
   1.265  \end{descr}
   1.266  
   1.267 -Note that these system commands are scarcely used when working with the
   1.268 -Proof~General interface, since loading of theories is done fully
   1.269 -transparently.
   1.270 +These system commands are scarcely used when working with the Proof~General
   1.271 +interface, since loading of theories is done fully transparently.
   1.272  
   1.273  %%% Local Variables: 
   1.274  %%% mode: latex