author | wenzelm |
Thu, 13 Apr 2000 15:11:41 +0200 | |
changeset 8706 | d81088481ec6 |
parent 8704 | f76f41f24c44 |
child 8811 | 6ec0c8f9d68d |
permissions | -rw-r--r-- |
7135 | 1 |
|
7167 | 2 |
\chapter{Generic Tools and Packages}\label{ch:gen-tools} |
3 |
||
8517 | 4 |
\section{Axiomatic Type Classes}\label{sec:axclass} |
7167 | 5 |
|
8517 | 6 |
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes} |
7167 | 7 |
\begin{matharray}{rcl} |
8517 | 8 |
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ |
9 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ |
|
10 |
intro_classes & : & \isarmeth \\ |
|
7167 | 11 |
\end{matharray} |
12 |
||
8517 | 13 |
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} |
14 |
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic |
|
8547 | 15 |
may make use of this light-weight mechanism of abstract theories |
16 |
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on \emph{Using Axiomatic |
|
17 |
Type Classes in Isabelle} that is part of the standard Isabelle |
|
18 |
documentation. |
|
8517 | 19 |
%FIXME cite |
20 |
||
7167 | 21 |
\begin{rail} |
8517 | 22 |
'axclass' classdecl (axmdecl prop comment? +) |
23 |
; |
|
24 |
'instance' (nameref '<' nameref | nameref '::' simplearity) comment? |
|
7167 | 25 |
; |
26 |
\end{rail} |
|
27 |
||
28 |
\begin{descr} |
|
8517 | 29 |
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type |
30 |
class as the intersection of existing classes, with additional axioms |
|
31 |
holding. Class axioms may not contain more than one type variable. The |
|
32 |
class axioms (with implicit sort constraints added) are bound to the given |
|
33 |
names. Furthermore a class introduction rule is generated, which is |
|
34 |
employed by method $intro_classes$ to support instantiation proofs of this |
|
35 |
class. |
|
7321 | 36 |
|
8517 | 37 |
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: |
8547 | 38 |
(\vec s)c$] setup a goal stating a class relation or type arity. The proof |
39 |
would usually proceed by $intro_classes$, and then establish the |
|
8517 | 40 |
characteristic theorems of the type classes involved. After finishing the |
41 |
proof, the theory will be augmented by a type signature declaration |
|
42 |
corresponding to the resulting theorem. |
|
43 |
\item [$intro_classes$] repeatedly expands all class introduction rules of |
|
44 |
this theory. |
|
7167 | 45 |
\end{descr} |
46 |
||
7315 | 47 |
|
48 |
\section{Calculational proof}\label{sec:calculation} |
|
49 |
||
8619 | 50 |
\indexisarcmd{also}\indexisarcmd{finally} |
51 |
\indexisarcmd{moreover}\indexisarcmd{ultimately} |
|
52 |
\indexisaratt{trans} |
|
7315 | 53 |
\begin{matharray}{rcl} |
54 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
55 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
8619 | 56 |
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ |
57 |
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
7315 | 58 |
trans & : & \isaratt \\ |
59 |
\end{matharray} |
|
60 |
||
61 |
Calculational proof is forward reasoning with implicit application of |
|
62 |
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains |
|
7391 | 63 |
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating |
7897 | 64 |
results obtained by transitivity composed with the current result. Command |
65 |
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the |
|
66 |
final $calculation$ by forward chaining towards the next goal statement. Both |
|
67 |
commands require valid current facts, i.e.\ may occur only after commands that |
|
68 |
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of |
|
8619 | 69 |
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are |
70 |
similar to $\ALSO$ and $\FINALLY$, but only collect further results in |
|
71 |
$calculation$ without applying any rules yet. |
|
7315 | 72 |
|
73 |
Also note that the automatic term abbreviation ``$\dots$'' has its canonical |
|
8619 | 74 |
application with calculational proofs. It refers to the argument\footnote{The |
75 |
argument of a curried infix expression is its right-hand side.} of the |
|
76 |
preceding statement. |
|
7315 | 77 |
|
78 |
Isabelle/Isar calculations are implicitly subject to block structure in the |
|
79 |
sense that new threads of calculational reasoning are commenced for any new |
|
80 |
block (as opened by a local goal, for example). This means that, apart from |
|
81 |
being able to nest calculations, there is no separate \emph{begin-calculation} |
|
82 |
command required. |
|
83 |
||
8619 | 84 |
\medskip |
85 |
||
86 |
The Isar calculation proof commands may be defined as |
|
87 |
follows:\footnote{Internal bookkeeping such as proper handling of |
|
88 |
block-structure has been suppressed.} |
|
89 |
\begin{matharray}{rcl} |
|
90 |
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\ |
|
91 |
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\ |
|
92 |
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ |
|
93 |
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ |
|
94 |
\ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\ |
|
95 |
\end{matharray} |
|
96 |
||
7315 | 97 |
\begin{rail} |
98 |
('also' | 'finally') transrules? comment? |
|
99 |
; |
|
8619 | 100 |
('moreover' | 'ultimately') comment? |
101 |
; |
|
8507 | 102 |
'trans' (() | 'add' | 'del') |
7315 | 103 |
; |
104 |
||
105 |
transrules: '(' thmrefs ')' interest? |
|
106 |
; |
|
107 |
\end{rail} |
|
108 |
||
109 |
\begin{descr} |
|
8547 | 110 |
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as |
7315 | 111 |
follows. The first occurrence of $\ALSO$ in some calculational thread |
7905 | 112 |
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
7335 | 113 |
level of block-structure updates $calculation$ by some transitivity rule |
7458 | 114 |
applied to $calculation$ and $this$ (in that order). Transitivity rules are |
8547 | 115 |
picked from the current context plus those given as explicit arguments (the |
116 |
latter have precedence). |
|
7315 | 117 |
|
8547 | 118 |
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
7315 | 119 |
$\ALSO$, and concludes the current calculational thread. The final result |
120 |
is exhibited as fact for forward chaining towards the next goal. Basically, |
|
7987 | 121 |
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
122 |
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and |
|
123 |
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding |
|
124 |
calculational proofs. |
|
7315 | 125 |
|
8619 | 126 |
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, |
127 |
but collect results only, without applying rules. |
|
128 |
||
8547 | 129 |
\item [$trans$] declares theorems as transitivity rules. |
7315 | 130 |
\end{descr} |
131 |
||
132 |
||
8483 | 133 |
\section{Named local contexts (cases)}\label{sec:cases} |
134 |
||
135 |
\indexisarcmd{case}\indexisarcmd{print-cases} |
|
136 |
\indexisaratt{case-names}\indexisaratt{params} |
|
137 |
\begin{matharray}{rcl} |
|
138 |
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
8517 | 139 |
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
8483 | 140 |
case_names & : & \isaratt \\ |
141 |
params & : & \isaratt \\ |
|
142 |
\end{matharray} |
|
143 |
||
144 |
Basically, Isar proof contexts are built up explicitly using commands like |
|
145 |
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical |
|
146 |
verification tasks this can become hard to manage, though. In particular, a |
|
147 |
large number of local contexts may emerge from case analysis or induction over |
|
148 |
inductive sets and types. |
|
149 |
||
150 |
\medskip |
|
151 |
||
152 |
The $\CASENAME$ command provides a shorthand to refer to certain parts of |
|
153 |
logical context symbolically. Proof methods may provide an environment of |
|
8507 | 154 |
named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of |
155 |
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
8483 | 156 |
|
157 |
It is important to note that $\CASENAME$ does \emph{not} provide any means to |
|
158 |
peek at the current goal state, which is treated as strictly non-observable in |
|
159 |
Isar! Instead, the cases considered here usually emerge in a canonical way |
|
160 |
from certain pieces of specification that appear in the theory somewhere else |
|
161 |
(e.g.\ in an inductive definition, or recursive function). See also |
|
162 |
\S\ref{sec:induct-method} for more details of how this works in HOL. |
|
163 |
||
164 |
\medskip |
|
165 |
||
166 |
Named cases may be exhibited in the current proof context only if both the |
|
8547 | 167 |
proof method and the rules involved support this. Case names and parameters |
168 |
of basic rules may be declared by hand as well, by using appropriate |
|
169 |
attributes. Thus variant versions of rules that have been derived manually |
|
170 |
may be used in advanced case analysis later. |
|
8483 | 171 |
|
172 |
\railalias{casenames}{case\_names} |
|
173 |
\railterm{casenames} |
|
174 |
||
175 |
\begin{rail} |
|
176 |
'case' nameref attributes? |
|
177 |
; |
|
178 |
casenames (name + ) |
|
179 |
; |
|
180 |
'params' ((name * ) + 'and') |
|
181 |
; |
|
182 |
\end{rail} |
|
8547 | 183 |
%FIXME bug in rail |
8483 | 184 |
|
185 |
\begin{descr} |
|
8507 | 186 |
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, |
8547 | 187 |
as provided by an appropriate proof method (such as $cases$ and $induct$ in |
188 |
Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$ |
|
189 |
abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
8483 | 190 |
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
8547 | 191 |
state, using Isar proof language notation. This is a diagnostic command; |
192 |
$undo$ does not apply. |
|
8483 | 193 |
\item [$case_names~\vec c$] declares names for the local contexts of premises |
8547 | 194 |
of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises. |
8483 | 195 |
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
8547 | 196 |
premises $1, \dots, n$ of some theorem. An empty list of names may be given |
197 |
to skip positions, leaving the present parameters unchanged. |
|
8483 | 198 |
\end{descr} |
199 |
||
200 |
||
8517 | 201 |
\section{Generalized existence} |
7135 | 202 |
|
8517 | 203 |
\indexisarcmd{obtain} |
7135 | 204 |
\begin{matharray}{rcl} |
8517 | 205 |
\isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\ |
206 |
\end{matharray} |
|
207 |
||
208 |
Generalized existence reasoning means that additional elements with certain |
|
209 |
properties are introduced, together with a soundness proof of that context |
|
210 |
change (the rest of the main goal is left unchanged). |
|
211 |
||
8547 | 212 |
Syntactically, the $\OBTAINNAME$ language element is like an initial proof |
213 |
method to the present goal, followed by a proof of its additional claim, |
|
214 |
followed by the actual context commands (using the syntax of $\FIXNAME$ and |
|
215 |
$\ASSUMENAME$, see \S\ref{sec:proof-context}). |
|
8517 | 216 |
|
217 |
\begin{rail} |
|
218 |
'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and') |
|
219 |
; |
|
220 |
\end{rail} |
|
221 |
||
8547 | 222 |
$\OBTAINNAME$ is defined as a derived Isar command as follows; here the |
8517 | 223 |
preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for |
224 |
forward chaining. |
|
225 |
\begin{matharray}{l} |
|
226 |
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex] |
|
227 |
\quad \PROOF{succeed} \\ |
|
228 |
\qquad \DEF{}{thesis \equiv \psi} \\ |
|
229 |
\qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\ |
|
230 |
\qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\ |
|
231 |
\quad \NEXT \\ |
|
232 |
\qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\ |
|
7135 | 233 |
\end{matharray} |
234 |
||
8517 | 235 |
Typically, the soundness proof is relatively straight-forward, often just by |
236 |
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or |
|
237 |
$\BY{blast}$ (see \S\ref{sec:classical-auto}). Note that the ``$that$'' |
|
238 |
presumption above is usually declared as simplification and (unsafe) |
|
8547 | 239 |
introduction rule, depending on the object-logic's policy, |
240 |
though.\footnote{HOL and HOLCF do this already.} |
|
8517 | 241 |
|
242 |
The original goal statement is wrapped into a local definition in order to |
|
243 |
avoid any automated tools descending into it. Usually, any statement would |
|
8547 | 244 |
admit the intended reduction anyway; only in very rare cases $thesis_def$ has |
245 |
to be expanded to complete the soundness proof. |
|
8517 | 246 |
|
247 |
\medskip |
|
248 |
||
249 |
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be |
|
250 |
meta-logical existential quantifiers and conjunctions. This concept has a |
|
251 |
broad range of useful applications, ranging from plain elimination (or even |
|
252 |
introduction) of object-level existentials and conjunctions, to elimination |
|
253 |
over results of symbolic evaluation of recursive definitions, for example. |
|
254 |
||
255 |
||
256 |
\section{Miscellaneous methods and attributes} |
|
257 |
||
258 |
\indexisarmeth{unfold}\indexisarmeth{fold} |
|
259 |
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} |
|
260 |
\indexisarmeth{fail}\indexisarmeth{succeed} |
|
261 |
\begin{matharray}{rcl} |
|
262 |
unfold & : & \isarmeth \\ |
|
263 |
fold & : & \isarmeth \\[0.5ex] |
|
264 |
erule^* & : & \isarmeth \\ |
|
265 |
drule^* & : & \isarmeth \\ |
|
266 |
frule^* & : & \isarmeth \\[0.5ex] |
|
267 |
succeed & : & \isarmeth \\ |
|
268 |
fail & : & \isarmeth \\ |
|
269 |
\end{matharray} |
|
7135 | 270 |
|
271 |
\begin{rail} |
|
8517 | 272 |
('fold' | 'unfold' | 'erule' | 'drule' | 'frule') thmrefs |
7135 | 273 |
; |
274 |
\end{rail} |
|
275 |
||
7167 | 276 |
\begin{descr} |
8547 | 277 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given |
8517 | 278 |
meta-level definitions throughout all goals; any facts provided are inserted |
279 |
into the goal and subject to rewriting as well. |
|
8547 | 280 |
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the |
281 |
basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by |
|
8517 | 282 |
elim-resolution, destruct-resolution, and forward-resolution, respectively |
283 |
\cite{isabelle-ref}. These are improper method, mainly for experimentation |
|
284 |
and emulating tactic scripts. |
|
7335 | 285 |
|
8517 | 286 |
Different modes of basic rule application are usually expressed in Isar at |
287 |
the proof language level, rather than via implicit proof state |
|
8547 | 288 |
manipulations. For example, a proper single-step elimination would be done |
8517 | 289 |
using the basic $rule$ method, with forward chaining of current facts. |
290 |
\item [$succeed$] yields a single (unchanged) result; it is the identity of |
|
291 |
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
292 |
\item [$fail$] yields an empty result sequence; it is the identity of the |
|
293 |
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
7167 | 294 |
\end{descr} |
7135 | 295 |
|
8517 | 296 |
|
297 |
\indexisaratt{standard} |
|
298 |
\indexisaratt{elimify} |
|
299 |
||
300 |
\indexisaratt{RS}\indexisaratt{COMP} |
|
301 |
\indexisaratt{where} |
|
302 |
\indexisaratt{tag}\indexisaratt{untag} |
|
303 |
\indexisaratt{transfer} |
|
304 |
\indexisaratt{export} |
|
305 |
\indexisaratt{unfold}\indexisaratt{fold} |
|
306 |
\begin{matharray}{rcl} |
|
307 |
tag & : & \isaratt \\ |
|
308 |
untag & : & \isaratt \\[0.5ex] |
|
309 |
RS & : & \isaratt \\ |
|
310 |
COMP & : & \isaratt \\[0.5ex] |
|
311 |
where & : & \isaratt \\[0.5ex] |
|
312 |
unfold & : & \isaratt \\ |
|
313 |
fold & : & \isaratt \\[0.5ex] |
|
314 |
standard & : & \isaratt \\ |
|
315 |
elimify & : & \isaratt \\ |
|
316 |
export^* & : & \isaratt \\ |
|
317 |
transfer & : & \isaratt \\[0.5ex] |
|
318 |
\end{matharray} |
|
319 |
||
320 |
\begin{rail} |
|
321 |
'tag' (nameref+) |
|
322 |
; |
|
323 |
'untag' name |
|
324 |
; |
|
325 |
('RS' | 'COMP') nat? thmref |
|
326 |
; |
|
327 |
'where' (name '=' term * 'and') |
|
328 |
; |
|
329 |
('unfold' | 'fold') thmrefs |
|
330 |
; |
|
331 |
\end{rail} |
|
332 |
||
333 |
\begin{descr} |
|
334 |
\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some |
|
335 |
theorem. Tags may be any list of strings that serve as comment for some |
|
336 |
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the |
|
337 |
result). The first string is considered the tag name, the rest its |
|
338 |
arguments. Note that untag removes any tags of the same name. |
|
8547 | 339 |
\item [$RS~n~a$ and $COMP~n~a$] compose rules. $RS$ resolves with the $n$-th |
340 |
premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting |
|
341 |
process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in |
|
342 |
\cite[\S5]{isabelle-ref}). |
|
8517 | 343 |
\item [$where~\vec x = \vec t$] perform named instantiation of schematic |
344 |
variables occurring in a theorem. Unlike instantiation tactics (such as |
|
345 |
\texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables |
|
346 |
have to be specified (e.g.\ $\Var{x@3}$). |
|
347 |
||
8547 | 348 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given |
8517 | 349 |
meta-level definitions throughout a rule. |
350 |
||
351 |
\item [$standard$] puts a theorem into the standard form of object-rules, just |
|
352 |
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}). |
|
353 |
||
354 |
\item [$elimify$] turns an destruction rule into an elimination, just as the |
|
355 |
ML function \texttt{make\_elim} (see \cite{isabelle-ref}). |
|
356 |
||
357 |
\item [$export$] lifts a local result out of the current proof context, |
|
358 |
generalizing all fixed variables and discharging all assumptions. Note that |
|
8547 | 359 |
proper incremental export is already done as part of the basic Isar |
360 |
machinery. This attribute is mainly for experimentation. |
|
8517 | 361 |
|
362 |
\item [$transfer$] promotes a theorem to the current theory context, which has |
|
8547 | 363 |
to enclose the former one. This is done automatically whenever rules are |
364 |
joined by inference. |
|
8517 | 365 |
|
366 |
\end{descr} |
|
7135 | 367 |
|
368 |
||
369 |
\section{The Simplifier} |
|
370 |
||
7321 | 371 |
\subsection{Simplification methods}\label{sec:simp} |
7315 | 372 |
|
8483 | 373 |
\indexisarmeth{simp}\indexisarmeth{simp-all} |
7315 | 374 |
\begin{matharray}{rcl} |
375 |
simp & : & \isarmeth \\ |
|
8483 | 376 |
simp_all & : & \isarmeth \\ |
7315 | 377 |
\end{matharray} |
378 |
||
8483 | 379 |
\railalias{simpall}{simp\_all} |
380 |
\railterm{simpall} |
|
381 |
||
8704 | 382 |
\railalias{noasm}{no\_asm} |
383 |
\railterm{noasm} |
|
384 |
||
385 |
\railalias{noasmsimp}{no\_asm\_simp} |
|
386 |
\railterm{noasmsimp} |
|
387 |
||
388 |
\railalias{noasmuse}{no\_asm\_use} |
|
389 |
\railterm{noasmuse} |
|
390 |
||
7315 | 391 |
\begin{rail} |
8706 | 392 |
('simp' | simpall) ('!' ?) opt? (simpmod * ) |
7315 | 393 |
; |
394 |
||
8706 | 395 |
opt: (noasm | noasmsimp | noasmuse) ':' |
8704 | 396 |
; |
8483 | 397 |
simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs |
7315 | 398 |
; |
399 |
\end{rail} |
|
400 |
||
7321 | 401 |
\begin{descr} |
8547 | 402 |
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
8594 | 403 |
according to the arguments given. Note that the \railtterm{only} modifier |
8547 | 404 |
first removes all other rewrite rules, congruences, and looper tactics |
8594 | 405 |
(including splits), and then behaves like \railtterm{add}. |
7321 | 406 |
|
8594 | 407 |
The \railtterm{split} modifiers add or delete rules for the Splitter (see |
8483 | 408 |
also \cite{isabelle-ref}), the default is to add. This works only if the |
409 |
Simplifier method has been properly setup to include the Splitter (all major |
|
410 |
object logics such HOL, HOLCF, FOL, ZF do this already). |
|
411 |
||
8594 | 412 |
The \railtterm{other} modifier ignores its arguments. Nevertheless, |
8547 | 413 |
additional kinds of rules may be declared by including appropriate |
414 |
attributes in the specification. |
|
8483 | 415 |
\item [$simp_all$] is similar to $simp$, but acts on all goals. |
7321 | 416 |
\end{descr} |
417 |
||
8704 | 418 |
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac} |
8706 | 419 |
internally \cite[\S10]{isabelle-ref}, which means that assumptions are both |
420 |
simplified as well as used in simplifying the conclusion. In structured |
|
421 |
proofs this is usually quite well behaved in practice: just the local premises |
|
422 |
of the actual goal are involved, additional facts may inserted via explicit |
|
423 |
forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The full context of |
|
424 |
assumptions is only included if the ``$!$'' (bang) argument is given, which |
|
425 |
should be used with some care, though. |
|
7321 | 426 |
|
8704 | 427 |
Additional Simplifier options may be specified to tune the behavior even |
428 |
further: $no_asm$ means assumptions are ignored completely (cf.\ |
|
429 |
\texttt{simp_tac}), $no_asm_simp$ means assumptions are used in the |
|
430 |
simplification of the conclusion but are not themselves simplified (cf.\ |
|
431 |
\texttt{asm_simp_tac}), and $no_asm_use$ means assumptions are simplified but |
|
432 |
are not used in the simplification of each other or the conclusion (cf. |
|
433 |
\texttt{full_simp_tac}). |
|
434 |
||
435 |
\medskip |
|
436 |
||
437 |
The Splitter package is usually configured to work as part of the Simplifier. |
|
438 |
There is no separate $split$ method available. The effect of repeatedly |
|
439 |
applying \texttt{split_tac} can be simulated by |
|
440 |
$(simp~only\colon~split\colon~\vec a)$. |
|
8483 | 441 |
|
442 |
||
443 |
\subsection{Declaring rules} |
|
444 |
||
8667 | 445 |
\indexisarcmd{print-simpset} |
8638 | 446 |
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} |
7321 | 447 |
\begin{matharray}{rcl} |
8667 | 448 |
print_simpset & : & \isarkeep{theory~|~proof} \\ |
7321 | 449 |
simp & : & \isaratt \\ |
8483 | 450 |
split & : & \isaratt \\ |
8638 | 451 |
cong & : & \isaratt \\ |
7321 | 452 |
\end{matharray} |
453 |
||
454 |
\begin{rail} |
|
8638 | 455 |
('simp' | 'split' | 'cong') (() | 'add' | 'del') |
7321 | 456 |
; |
457 |
\end{rail} |
|
458 |
||
459 |
\begin{descr} |
|
8667 | 460 |
\item [$print_simpset$] prints the collection of rules declared to the |
461 |
Simplifier, which is also known as ``simpset'' internally |
|
462 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
|
8547 | 463 |
\item [$simp$] declares simplification rules. |
464 |
\item [$split$] declares split rules. |
|
8638 | 465 |
\item [$cong$] declares congruence rules. |
7321 | 466 |
\end{descr} |
7319 | 467 |
|
7315 | 468 |
|
469 |
\subsection{Forward simplification} |
|
470 |
||
7391 | 471 |
\indexisaratt{simplify}\indexisaratt{asm-simplify} |
472 |
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify} |
|
7315 | 473 |
\begin{matharray}{rcl} |
474 |
simplify & : & \isaratt \\ |
|
475 |
asm_simplify & : & \isaratt \\ |
|
476 |
full_simplify & : & \isaratt \\ |
|
477 |
asm_full_simplify & : & \isaratt \\ |
|
478 |
\end{matharray} |
|
479 |
||
7321 | 480 |
These attributes provide forward rules for simplification, which should be |
8547 | 481 |
used only very rarely. There are no separate options for declaring |
7905 | 482 |
simplification rules locally. |
483 |
||
484 |
See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more |
|
485 |
information. |
|
7315 | 486 |
|
487 |
||
7135 | 488 |
\section{The Classical Reasoner} |
489 |
||
7335 | 490 |
\subsection{Basic methods}\label{sec:classical-basic} |
7321 | 491 |
|
7974 | 492 |
\indexisarmeth{rule}\indexisarmeth{intro} |
493 |
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} |
|
7321 | 494 |
\begin{matharray}{rcl} |
495 |
rule & : & \isarmeth \\ |
|
496 |
intro & : & \isarmeth \\ |
|
497 |
elim & : & \isarmeth \\ |
|
498 |
contradiction & : & \isarmeth \\ |
|
499 |
\end{matharray} |
|
500 |
||
501 |
\begin{rail} |
|
8547 | 502 |
('rule' | 'intro' | 'elim') thmrefs? |
7321 | 503 |
; |
504 |
\end{rail} |
|
505 |
||
506 |
\begin{descr} |
|
7466 | 507 |
\item [$rule$] as offered by the classical reasoner is a refinement over the |
8517 | 508 |
primitive one (see \S\ref{sec:pure-meth-att}). In case that no rules are |
7466 | 509 |
provided as arguments, it automatically determines elimination and |
7321 | 510 |
introduction rules from the context (see also \S\ref{sec:classical-mod}). |
8517 | 511 |
This is made the default method for basic proof steps, such as $\PROOFNAME$ |
512 |
and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and |
|
513 |
\S\ref{sec:pure-meth-att}. |
|
7321 | 514 |
|
7466 | 515 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
7905 | 516 |
elim-resolution, after having inserted any facts. Omitting the arguments |
8547 | 517 |
refers to any suitable rules declared in the context, otherwise only the |
518 |
explicitly given ones may be applied. The latter form admits better control |
|
519 |
of what actually happens, thus it is very appropriate as an initial method |
|
520 |
for $\PROOFNAME$ that splits up certain connectives of the goal, before |
|
521 |
entering the actual sub-proof. |
|
7458 | 522 |
|
7466 | 523 |
\item [$contradiction$] solves some goal by contradiction, deriving any result |
524 |
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may |
|
525 |
appear in either order. |
|
7321 | 526 |
\end{descr} |
527 |
||
528 |
||
7981 | 529 |
\subsection{Automated methods}\label{sec:classical-auto} |
7315 | 530 |
|
7321 | 531 |
\indexisarmeth{blast} |
7391 | 532 |
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best} |
7321 | 533 |
\begin{matharray}{rcl} |
534 |
blast & : & \isarmeth \\ |
|
535 |
fast & : & \isarmeth \\ |
|
536 |
best & : & \isarmeth \\ |
|
537 |
slow & : & \isarmeth \\ |
|
538 |
slow_best & : & \isarmeth \\ |
|
539 |
\end{matharray} |
|
540 |
||
541 |
\railalias{slowbest}{slow\_best} |
|
542 |
\railterm{slowbest} |
|
543 |
||
544 |
\begin{rail} |
|
7905 | 545 |
'blast' ('!' ?) nat? (clamod * ) |
7321 | 546 |
; |
7905 | 547 |
('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * ) |
7321 | 548 |
; |
549 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
550 |
clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs |
7321 | 551 |
; |
552 |
\end{rail} |
|
553 |
||
554 |
\begin{descr} |
|
555 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} |
|
7335 | 556 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a |
7321 | 557 |
user-supplied search bound (default 20). |
558 |
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical |
|
7335 | 559 |
reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc). |
7321 | 560 |
\end{descr} |
561 |
||
562 |
Any of above methods support additional modifiers of the context of classical |
|
8517 | 563 |
rules. Their semantics is analogous to the attributes given in |
8547 | 564 |
\S\ref{sec:classical-mod}. Facts provided by forward chaining are |
565 |
inserted\footnote{These methods usually cannot make proper use of actual rules |
|
566 |
inserted that way, though.} into the goal before doing the search. The |
|
567 |
``!''~argument causes the full context of assumptions to be included as well. |
|
568 |
This is slightly less hazardous than for the Simplifier (see |
|
569 |
\S\ref{sec:simp}). |
|
7321 | 570 |
|
7315 | 571 |
|
7981 | 572 |
\subsection{Combined automated methods} |
7315 | 573 |
|
7321 | 574 |
\indexisarmeth{auto}\indexisarmeth{force} |
575 |
\begin{matharray}{rcl} |
|
576 |
force & : & \isarmeth \\ |
|
577 |
auto & : & \isarmeth \\ |
|
578 |
\end{matharray} |
|
579 |
||
580 |
\begin{rail} |
|
7905 | 581 |
('force' | 'auto') ('!' ?) (clasimpmod * ) |
7321 | 582 |
; |
7315 | 583 |
|
8483 | 584 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' | |
585 |
('split' (() | 'add' | 'del')) | |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
586 |
(('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs |
7321 | 587 |
\end{rail} |
7315 | 588 |
|
7321 | 589 |
\begin{descr} |
590 |
\item [$force$ and $auto$] provide access to Isabelle's combined |
|
591 |
simplification and classical reasoning tactics. See \texttt{force_tac} and |
|
592 |
\texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information. The |
|
593 |
modifier arguments correspond to those given in \S\ref{sec:simp} and |
|
7905 | 594 |
\S\ref{sec:classical-auto}. Just note that the ones related to the |
8594 | 595 |
Simplifier are prefixed by \railtterm{simp} here. |
7987 | 596 |
|
597 |
Facts provided by forward chaining are inserted into the goal before doing |
|
598 |
the search. The ``!''~argument causes the full context of assumptions to be |
|
599 |
included as well. |
|
7321 | 600 |
\end{descr} |
601 |
||
7987 | 602 |
|
8483 | 603 |
\subsection{Declaring rules}\label{sec:classical-mod} |
7135 | 604 |
|
8667 | 605 |
\indexisarcmd{print-claset} |
7391 | 606 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} |
607 |
\indexisaratt{iff}\indexisaratt{delrule} |
|
7321 | 608 |
\begin{matharray}{rcl} |
8667 | 609 |
print_claset & : & \isarkeep{theory~|~proof} \\ |
7321 | 610 |
intro & : & \isaratt \\ |
611 |
elim & : & \isaratt \\ |
|
612 |
dest & : & \isaratt \\ |
|
7391 | 613 |
iff & : & \isaratt \\ |
7321 | 614 |
delrule & : & \isaratt \\ |
615 |
\end{matharray} |
|
7135 | 616 |
|
7321 | 617 |
\begin{rail} |
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
618 |
('intro' | 'elim' | 'dest') (() | '?' | '??') |
7321 | 619 |
; |
8638 | 620 |
'iff' (() | 'add' | 'del') |
7321 | 621 |
\end{rail} |
7135 | 622 |
|
7321 | 623 |
\begin{descr} |
8667 | 624 |
\item [$print_claset$] prints the collection of rules declared to the |
625 |
Classical Reasoner, which is also known as ``simpset'' internally |
|
626 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
|
8517 | 627 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and |
628 |
destruct rules, respectively. By default, rules are considered as |
|
629 |
\emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as |
|
630 |
\emph{extra} (i.e.\ not applied in the search-oriented automated methods, |
|
631 |
but only in single-step methods such as $rule$). |
|
7335 | 632 |
|
8547 | 633 |
\item [$iff$] declares equations both as rules for the Simplifier and |
634 |
Classical Reasoner. |
|
7391 | 635 |
|
7335 | 636 |
\item [$delrule$] deletes introduction or elimination rules from the context. |
637 |
Note that destruction rules would have to be turned into elimination rules |
|
7321 | 638 |
first, e.g.\ by using the $elimify$ attribute. |
639 |
\end{descr} |
|
7135 | 640 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
641 |
|
7135 | 642 |
%%% Local Variables: |
643 |
%%% mode: latex |
|
644 |
%%% TeX-master: "isar-ref" |
|
645 |
%%% End: |