summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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