wenzelm@7135
|
1 |
|
wenzelm@7167
|
2 |
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
|
wenzelm@7167
|
3 |
|
wenzelm@8517
|
4 |
\section{Axiomatic Type Classes}\label{sec:axclass}
|
wenzelm@7167
|
5 |
|
wenzelm@8904
|
6 |
%FIXME
|
wenzelm@8904
|
7 |
% - qualified names
|
wenzelm@8904
|
8 |
% - class intro rules;
|
wenzelm@8904
|
9 |
% - class axioms;
|
wenzelm@8904
|
10 |
|
wenzelm@8517
|
11 |
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
|
wenzelm@7167
|
12 |
\begin{matharray}{rcl}
|
wenzelm@8517
|
13 |
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
|
wenzelm@8517
|
14 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
|
wenzelm@8517
|
15 |
intro_classes & : & \isarmeth \\
|
wenzelm@7167
|
16 |
\end{matharray}
|
wenzelm@7167
|
17 |
|
wenzelm@8517
|
18 |
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
|
wenzelm@8517
|
19 |
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
|
wenzelm@8547
|
20 |
may make use of this light-weight mechanism of abstract theories
|
wenzelm@8901
|
21 |
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
|
wenzelm@8901
|
22 |
classes in isabelle \cite{isabelle-axclass} that is part of the standard
|
wenzelm@8901
|
23 |
Isabelle documentation.
|
wenzelm@8517
|
24 |
|
wenzelm@7167
|
25 |
\begin{rail}
|
wenzelm@8517
|
26 |
'axclass' classdecl (axmdecl prop comment? +)
|
wenzelm@8517
|
27 |
;
|
wenzelm@8517
|
28 |
'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
|
wenzelm@7167
|
29 |
;
|
wenzelm@7167
|
30 |
\end{rail}
|
wenzelm@7167
|
31 |
|
wenzelm@7167
|
32 |
\begin{descr}
|
wenzelm@8517
|
33 |
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
|
wenzelm@8517
|
34 |
class as the intersection of existing classes, with additional axioms
|
wenzelm@8517
|
35 |
holding. Class axioms may not contain more than one type variable. The
|
wenzelm@8517
|
36 |
class axioms (with implicit sort constraints added) are bound to the given
|
wenzelm@8517
|
37 |
names. Furthermore a class introduction rule is generated, which is
|
wenzelm@8517
|
38 |
employed by method $intro_classes$ to support instantiation proofs of this
|
wenzelm@8517
|
39 |
class.
|
wenzelm@9614
|
40 |
|
wenzelm@8517
|
41 |
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
|
wenzelm@8547
|
42 |
(\vec s)c$] setup a goal stating a class relation or type arity. The proof
|
wenzelm@8547
|
43 |
would usually proceed by $intro_classes$, and then establish the
|
wenzelm@8517
|
44 |
characteristic theorems of the type classes involved. After finishing the
|
wenzelm@8517
|
45 |
proof, the theory will be augmented by a type signature declaration
|
wenzelm@8517
|
46 |
corresponding to the resulting theorem.
|
wenzelm@8517
|
47 |
\item [$intro_classes$] repeatedly expands all class introduction rules of
|
wenzelm@8517
|
48 |
this theory.
|
wenzelm@7167
|
49 |
\end{descr}
|
wenzelm@7167
|
50 |
|
wenzelm@7315
|
51 |
|
wenzelm@7315
|
52 |
\section{Calculational proof}\label{sec:calculation}
|
wenzelm@7315
|
53 |
|
wenzelm@8619
|
54 |
\indexisarcmd{also}\indexisarcmd{finally}
|
wenzelm@8619
|
55 |
\indexisarcmd{moreover}\indexisarcmd{ultimately}
|
wenzelm@9606
|
56 |
\indexisarcmd{print-trans-rules}\indexisaratt{trans}
|
wenzelm@7315
|
57 |
\begin{matharray}{rcl}
|
wenzelm@7315
|
58 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7315
|
59 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
|
wenzelm@8619
|
60 |
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@8619
|
61 |
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
|
wenzelm@9606
|
62 |
\isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7315
|
63 |
trans & : & \isaratt \\
|
wenzelm@7315
|
64 |
\end{matharray}
|
wenzelm@7315
|
65 |
|
wenzelm@7315
|
66 |
Calculational proof is forward reasoning with implicit application of
|
wenzelm@7315
|
67 |
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains
|
wenzelm@7391
|
68 |
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
|
wenzelm@7897
|
69 |
results obtained by transitivity composed with the current result. Command
|
wenzelm@7897
|
70 |
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
|
wenzelm@7897
|
71 |
final $calculation$ by forward chaining towards the next goal statement. Both
|
wenzelm@7897
|
72 |
commands require valid current facts, i.e.\ may occur only after commands that
|
wenzelm@7897
|
73 |
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
|
wenzelm@8619
|
74 |
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are
|
wenzelm@8619
|
75 |
similar to $\ALSO$ and $\FINALLY$, but only collect further results in
|
wenzelm@8619
|
76 |
$calculation$ without applying any rules yet.
|
wenzelm@7315
|
77 |
|
wenzelm@7315
|
78 |
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
|
wenzelm@8619
|
79 |
application with calculational proofs. It refers to the argument\footnote{The
|
wenzelm@8619
|
80 |
argument of a curried infix expression is its right-hand side.} of the
|
wenzelm@8619
|
81 |
preceding statement.
|
wenzelm@7315
|
82 |
|
wenzelm@7315
|
83 |
Isabelle/Isar calculations are implicitly subject to block structure in the
|
wenzelm@7315
|
84 |
sense that new threads of calculational reasoning are commenced for any new
|
wenzelm@7315
|
85 |
block (as opened by a local goal, for example). This means that, apart from
|
wenzelm@7315
|
86 |
being able to nest calculations, there is no separate \emph{begin-calculation}
|
wenzelm@7315
|
87 |
command required.
|
wenzelm@7315
|
88 |
|
wenzelm@8619
|
89 |
\medskip
|
wenzelm@8619
|
90 |
|
wenzelm@8619
|
91 |
The Isar calculation proof commands may be defined as
|
wenzelm@8619
|
92 |
follows:\footnote{Internal bookkeeping such as proper handling of
|
wenzelm@8619
|
93 |
block-structure has been suppressed.}
|
wenzelm@8619
|
94 |
\begin{matharray}{rcl}
|
wenzelm@8619
|
95 |
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\
|
wenzelm@9606
|
96 |
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
|
wenzelm@8619
|
97 |
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\
|
wenzelm@8619
|
98 |
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
|
wenzelm@8619
|
99 |
\ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
|
wenzelm@8619
|
100 |
\end{matharray}
|
wenzelm@8619
|
101 |
|
wenzelm@7315
|
102 |
\begin{rail}
|
wenzelm@7315
|
103 |
('also' | 'finally') transrules? comment?
|
wenzelm@7315
|
104 |
;
|
wenzelm@8619
|
105 |
('moreover' | 'ultimately') comment?
|
wenzelm@8619
|
106 |
;
|
wenzelm@8507
|
107 |
'trans' (() | 'add' | 'del')
|
wenzelm@7315
|
108 |
;
|
wenzelm@7315
|
109 |
|
wenzelm@7315
|
110 |
transrules: '(' thmrefs ')' interest?
|
wenzelm@7315
|
111 |
;
|
wenzelm@7315
|
112 |
\end{rail}
|
wenzelm@7315
|
113 |
|
wenzelm@7315
|
114 |
\begin{descr}
|
wenzelm@8547
|
115 |
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
|
wenzelm@7315
|
116 |
follows. The first occurrence of $\ALSO$ in some calculational thread
|
wenzelm@7905
|
117 |
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
|
wenzelm@7335
|
118 |
level of block-structure updates $calculation$ by some transitivity rule
|
wenzelm@7458
|
119 |
applied to $calculation$ and $this$ (in that order). Transitivity rules are
|
wenzelm@8547
|
120 |
picked from the current context plus those given as explicit arguments (the
|
wenzelm@8547
|
121 |
latter have precedence).
|
wenzelm@9614
|
122 |
|
wenzelm@8547
|
123 |
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
|
wenzelm@7315
|
124 |
$\ALSO$, and concludes the current calculational thread. The final result
|
wenzelm@7315
|
125 |
is exhibited as fact for forward chaining towards the next goal. Basically,
|
wenzelm@7987
|
126 |
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
|
wenzelm@7987
|
127 |
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
|
wenzelm@7987
|
128 |
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
|
wenzelm@7987
|
129 |
calculational proofs.
|
wenzelm@9614
|
130 |
|
wenzelm@8619
|
131 |
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
|
wenzelm@8619
|
132 |
but collect results only, without applying rules.
|
wenzelm@9614
|
133 |
|
wenzelm@9606
|
134 |
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
|
wenzelm@9606
|
135 |
rules declared in the current context.
|
wenzelm@9614
|
136 |
|
wenzelm@8547
|
137 |
\item [$trans$] declares theorems as transitivity rules.
|
wenzelm@9614
|
138 |
|
wenzelm@7315
|
139 |
\end{descr}
|
wenzelm@7315
|
140 |
|
wenzelm@7315
|
141 |
|
wenzelm@8483
|
142 |
\section{Named local contexts (cases)}\label{sec:cases}
|
wenzelm@8483
|
143 |
|
wenzelm@8483
|
144 |
\indexisarcmd{case}\indexisarcmd{print-cases}
|
wenzelm@8483
|
145 |
\indexisaratt{case-names}\indexisaratt{params}
|
wenzelm@8483
|
146 |
\begin{matharray}{rcl}
|
wenzelm@8483
|
147 |
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@8517
|
148 |
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\
|
wenzelm@8483
|
149 |
case_names & : & \isaratt \\
|
wenzelm@8483
|
150 |
params & : & \isaratt \\
|
wenzelm@8483
|
151 |
\end{matharray}
|
wenzelm@8483
|
152 |
|
wenzelm@8483
|
153 |
Basically, Isar proof contexts are built up explicitly using commands like
|
wenzelm@8483
|
154 |
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical
|
wenzelm@8483
|
155 |
verification tasks this can become hard to manage, though. In particular, a
|
wenzelm@8483
|
156 |
large number of local contexts may emerge from case analysis or induction over
|
wenzelm@8483
|
157 |
inductive sets and types.
|
wenzelm@8483
|
158 |
|
wenzelm@8483
|
159 |
\medskip
|
wenzelm@8483
|
160 |
|
wenzelm@8483
|
161 |
The $\CASENAME$ command provides a shorthand to refer to certain parts of
|
wenzelm@8483
|
162 |
logical context symbolically. Proof methods may provide an environment of
|
wenzelm@8507
|
163 |
named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of
|
wenzelm@8507
|
164 |
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
|
wenzelm@8483
|
165 |
|
wenzelm@8483
|
166 |
It is important to note that $\CASENAME$ does \emph{not} provide any means to
|
wenzelm@8483
|
167 |
peek at the current goal state, which is treated as strictly non-observable in
|
wenzelm@8483
|
168 |
Isar! Instead, the cases considered here usually emerge in a canonical way
|
wenzelm@8483
|
169 |
from certain pieces of specification that appear in the theory somewhere else
|
wenzelm@8483
|
170 |
(e.g.\ in an inductive definition, or recursive function). See also
|
wenzelm@8483
|
171 |
\S\ref{sec:induct-method} for more details of how this works in HOL.
|
wenzelm@8483
|
172 |
|
wenzelm@8483
|
173 |
\medskip
|
wenzelm@8483
|
174 |
|
wenzelm@8483
|
175 |
Named cases may be exhibited in the current proof context only if both the
|
wenzelm@8547
|
176 |
proof method and the rules involved support this. Case names and parameters
|
wenzelm@8547
|
177 |
of basic rules may be declared by hand as well, by using appropriate
|
wenzelm@8547
|
178 |
attributes. Thus variant versions of rules that have been derived manually
|
wenzelm@8547
|
179 |
may be used in advanced case analysis later.
|
wenzelm@8483
|
180 |
|
wenzelm@8483
|
181 |
\railalias{casenames}{case\_names}
|
wenzelm@8483
|
182 |
\railterm{casenames}
|
wenzelm@8483
|
183 |
|
wenzelm@8483
|
184 |
\begin{rail}
|
wenzelm@8483
|
185 |
'case' nameref attributes?
|
wenzelm@8483
|
186 |
;
|
wenzelm@8483
|
187 |
casenames (name + )
|
wenzelm@8483
|
188 |
;
|
wenzelm@8483
|
189 |
'params' ((name * ) + 'and')
|
wenzelm@8483
|
190 |
;
|
wenzelm@8483
|
191 |
\end{rail}
|
wenzelm@8547
|
192 |
%FIXME bug in rail
|
wenzelm@8483
|
193 |
|
wenzelm@8483
|
194 |
\begin{descr}
|
wenzelm@8507
|
195 |
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
|
wenzelm@8547
|
196 |
as provided by an appropriate proof method (such as $cases$ and $induct$ in
|
wenzelm@8547
|
197 |
Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$
|
wenzelm@8547
|
198 |
abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
|
wenzelm@8483
|
199 |
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
|
wenzelm@8547
|
200 |
state, using Isar proof language notation. This is a diagnostic command;
|
wenzelm@8547
|
201 |
$undo$ does not apply.
|
wenzelm@8483
|
202 |
\item [$case_names~\vec c$] declares names for the local contexts of premises
|
wenzelm@8547
|
203 |
of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
|
wenzelm@8483
|
204 |
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
|
wenzelm@8547
|
205 |
premises $1, \dots, n$ of some theorem. An empty list of names may be given
|
wenzelm@8547
|
206 |
to skip positions, leaving the present parameters unchanged.
|
wenzelm@9614
|
207 |
|
wenzelm@9614
|
208 |
Note that the default usage of case rules does \emph{not} directly expose
|
wenzelm@9614
|
209 |
parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
|
wenzelm@8483
|
210 |
\end{descr}
|
wenzelm@8483
|
211 |
|
wenzelm@8483
|
212 |
|
wenzelm@9614
|
213 |
\section{Generalized existence}\label{sec:obtain}
|
wenzelm@7135
|
214 |
|
wenzelm@8517
|
215 |
\indexisarcmd{obtain}
|
wenzelm@7135
|
216 |
\begin{matharray}{rcl}
|
wenzelm@9480
|
217 |
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
|
wenzelm@7135
|
218 |
\end{matharray}
|
wenzelm@7135
|
219 |
|
wenzelm@9480
|
220 |
Generalized existence means that additional elements with certain properties
|
wenzelm@9480
|
221 |
may introduced in the current context. Technically, the $\OBTAINNAME$
|
wenzelm@9480
|
222 |
language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
|
wenzelm@9480
|
223 |
also see \S\ref{sec:proof-context}), together with a soundness proof of its
|
wenzelm@9480
|
224 |
additional claim. According to the nature of existential reasoning,
|
wenzelm@9480
|
225 |
assumptions get eliminated from any result exported from the context later,
|
wenzelm@9480
|
226 |
provided that the corresponding parameters do \emph{not} occur in the
|
wenzelm@9480
|
227 |
conclusion.
|
wenzelm@7135
|
228 |
|
wenzelm@7135
|
229 |
\begin{rail}
|
wenzelm@8517
|
230 |
'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
|
wenzelm@7135
|
231 |
;
|
wenzelm@8517
|
232 |
\end{rail}
|
wenzelm@8517
|
233 |
|
wenzelm@9480
|
234 |
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
|
wenzelm@9480
|
235 |
shall refer to (optional) facts indicated for forward chaining.
|
wenzelm@8517
|
236 |
\begin{matharray}{l}
|
wenzelm@9480
|
237 |
\langle facts~\vec b\rangle \\
|
wenzelm@9480
|
238 |
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
|
wenzelm@9480
|
239 |
\quad \BG \\
|
wenzelm@9480
|
240 |
\qquad \FIX{thesis} \\
|
wenzelm@9480
|
241 |
\qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
|
wenzelm@9480
|
242 |
\qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
|
wenzelm@9480
|
243 |
\quad \EN \\
|
wenzelm@9606
|
244 |
\quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
|
wenzelm@8517
|
245 |
\end{matharray}
|
wenzelm@8517
|
246 |
|
wenzelm@8517
|
247 |
Typically, the soundness proof is relatively straight-forward, often just by
|
wenzelm@8517
|
248 |
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
|
wenzelm@9480
|
249 |
$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$''
|
wenzelm@9480
|
250 |
reduction above is declared as simplification and introduction rule.
|
wenzelm@8517
|
251 |
|
wenzelm@8517
|
252 |
\medskip
|
wenzelm@8517
|
253 |
|
wenzelm@8517
|
254 |
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
|
wenzelm@8517
|
255 |
meta-logical existential quantifiers and conjunctions. This concept has a
|
wenzelm@8517
|
256 |
broad range of useful applications, ranging from plain elimination (or even
|
wenzelm@8517
|
257 |
introduction) of object-level existentials and conjunctions, to elimination
|
wenzelm@8517
|
258 |
over results of symbolic evaluation of recursive definitions, for example.
|
wenzelm@9480
|
259 |
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
|
wenzelm@9480
|
260 |
where the result is treated as an assumption.
|
wenzelm@8517
|
261 |
|
wenzelm@8517
|
262 |
|
wenzelm@8517
|
263 |
\section{Miscellaneous methods and attributes}
|
wenzelm@8517
|
264 |
|
wenzelm@9606
|
265 |
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
|
wenzelm@8517
|
266 |
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
|
wenzelm@8517
|
267 |
\indexisarmeth{fail}\indexisarmeth{succeed}
|
wenzelm@8517
|
268 |
\begin{matharray}{rcl}
|
wenzelm@8517
|
269 |
unfold & : & \isarmeth \\
|
wenzelm@8517
|
270 |
fold & : & \isarmeth \\[0.5ex]
|
wenzelm@9606
|
271 |
insert^* & : & \isarmeth \\[0.5ex]
|
wenzelm@8517
|
272 |
erule^* & : & \isarmeth \\
|
wenzelm@8517
|
273 |
drule^* & : & \isarmeth \\
|
wenzelm@8517
|
274 |
frule^* & : & \isarmeth \\[0.5ex]
|
wenzelm@8517
|
275 |
succeed & : & \isarmeth \\
|
wenzelm@8517
|
276 |
fail & : & \isarmeth \\
|
wenzelm@8517
|
277 |
\end{matharray}
|
wenzelm@8517
|
278 |
|
wenzelm@8517
|
279 |
\begin{rail}
|
wenzelm@9606
|
280 |
('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs
|
wenzelm@7135
|
281 |
;
|
wenzelm@7135
|
282 |
\end{rail}
|
wenzelm@7135
|
283 |
|
wenzelm@7167
|
284 |
\begin{descr}
|
wenzelm@8547
|
285 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
|
wenzelm@8517
|
286 |
meta-level definitions throughout all goals; any facts provided are inserted
|
wenzelm@8517
|
287 |
into the goal and subject to rewriting as well.
|
wenzelm@8547
|
288 |
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
|
wenzelm@8547
|
289 |
basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
|
wenzelm@8517
|
290 |
elim-resolution, destruct-resolution, and forward-resolution, respectively
|
wenzelm@8517
|
291 |
\cite{isabelle-ref}. These are improper method, mainly for experimentation
|
wenzelm@8517
|
292 |
and emulating tactic scripts.
|
wenzelm@9614
|
293 |
|
wenzelm@8517
|
294 |
Different modes of basic rule application are usually expressed in Isar at
|
wenzelm@8517
|
295 |
the proof language level, rather than via implicit proof state
|
wenzelm@8547
|
296 |
manipulations. For example, a proper single-step elimination would be done
|
wenzelm@8517
|
297 |
using the basic $rule$ method, with forward chaining of current facts.
|
wenzelm@9606
|
298 |
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
|
wenzelm@9606
|
299 |
state. Note that current facts indicated for forward chaining are ignored.
|
wenzelm@8517
|
300 |
\item [$succeed$] yields a single (unchanged) result; it is the identity of
|
wenzelm@8517
|
301 |
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
|
wenzelm@8517
|
302 |
\item [$fail$] yields an empty result sequence; it is the identity of the
|
wenzelm@8517
|
303 |
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
|
wenzelm@7167
|
304 |
\end{descr}
|
wenzelm@7135
|
305 |
|
wenzelm@8517
|
306 |
|
wenzelm@8517
|
307 |
\indexisaratt{standard}
|
wenzelm@8517
|
308 |
\indexisaratt{elimify}
|
wenzelm@9232
|
309 |
\indexisaratt{no-vars}
|
wenzelm@8517
|
310 |
|
wenzelm@9614
|
311 |
\indexisaratt{THEN}\indexisaratt{COMP}
|
wenzelm@8517
|
312 |
\indexisaratt{where}
|
wenzelm@8517
|
313 |
\indexisaratt{tag}\indexisaratt{untag}
|
wenzelm@8517
|
314 |
\indexisaratt{export}
|
wenzelm@8517
|
315 |
\indexisaratt{unfold}\indexisaratt{fold}
|
wenzelm@8517
|
316 |
\begin{matharray}{rcl}
|
wenzelm@8517
|
317 |
tag & : & \isaratt \\
|
wenzelm@8517
|
318 |
untag & : & \isaratt \\[0.5ex]
|
wenzelm@9614
|
319 |
THEN & : & \isaratt \\
|
wenzelm@8517
|
320 |
COMP & : & \isaratt \\[0.5ex]
|
wenzelm@8517
|
321 |
where & : & \isaratt \\[0.5ex]
|
wenzelm@8517
|
322 |
unfold & : & \isaratt \\
|
wenzelm@8517
|
323 |
fold & : & \isaratt \\[0.5ex]
|
wenzelm@8517
|
324 |
standard & : & \isaratt \\
|
wenzelm@8517
|
325 |
elimify & : & \isaratt \\
|
wenzelm@9232
|
326 |
no_vars & : & \isaratt \\
|
wenzelm@8517
|
327 |
export^* & : & \isaratt \\
|
wenzelm@8517
|
328 |
\end{matharray}
|
wenzelm@8517
|
329 |
|
wenzelm@8517
|
330 |
\begin{rail}
|
wenzelm@8517
|
331 |
'tag' (nameref+)
|
wenzelm@8517
|
332 |
;
|
wenzelm@8517
|
333 |
'untag' name
|
wenzelm@8517
|
334 |
;
|
wenzelm@9614
|
335 |
('THEN' | 'COMP') nat? thmref
|
wenzelm@8517
|
336 |
;
|
wenzelm@8517
|
337 |
'where' (name '=' term * 'and')
|
wenzelm@8517
|
338 |
;
|
wenzelm@8517
|
339 |
('unfold' | 'fold') thmrefs
|
wenzelm@8517
|
340 |
;
|
wenzelm@8517
|
341 |
\end{rail}
|
wenzelm@8517
|
342 |
|
wenzelm@8517
|
343 |
\begin{descr}
|
wenzelm@8517
|
344 |
\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
|
wenzelm@8517
|
345 |
theorem. Tags may be any list of strings that serve as comment for some
|
wenzelm@8517
|
346 |
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
|
wenzelm@8517
|
347 |
result). The first string is considered the tag name, the rest its
|
wenzelm@8517
|
348 |
arguments. Note that untag removes any tags of the same name.
|
wenzelm@9614
|
349 |
\item [$THEN~n~a$ and $COMP~n~a$] compose rules. $THEN$ resolves with the
|
wenzelm@9614
|
350 |
$n$-th premise of $a$; the $COMP$ version skips the automatic lifting
|
wenzelm@8547
|
351 |
process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
|
wenzelm@8547
|
352 |
\cite[\S5]{isabelle-ref}).
|
wenzelm@8517
|
353 |
\item [$where~\vec x = \vec t$] perform named instantiation of schematic
|
wenzelm@9606
|
354 |
variables occurring in a theorem. Unlike instantiation tactics such as
|
wenzelm@9606
|
355 |
$rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
|
wenzelm@8517
|
356 |
have to be specified (e.g.\ $\Var{x@3}$).
|
wenzelm@9614
|
357 |
|
wenzelm@8547
|
358 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
|
wenzelm@8517
|
359 |
meta-level definitions throughout a rule.
|
wenzelm@9614
|
360 |
|
wenzelm@8517
|
361 |
\item [$standard$] puts a theorem into the standard form of object-rules, just
|
wenzelm@8517
|
362 |
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
|
wenzelm@9614
|
363 |
|
wenzelm@8517
|
364 |
\item [$elimify$] turns an destruction rule into an elimination, just as the
|
wenzelm@8517
|
365 |
ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
|
wenzelm@9614
|
366 |
|
wenzelm@9232
|
367 |
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
|
wenzelm@9232
|
368 |
for tuning output of pretty printed theorems.
|
wenzelm@9614
|
369 |
|
wenzelm@8517
|
370 |
\item [$export$] lifts a local result out of the current proof context,
|
wenzelm@8517
|
371 |
generalizing all fixed variables and discharging all assumptions. Note that
|
wenzelm@8547
|
372 |
proper incremental export is already done as part of the basic Isar
|
wenzelm@8547
|
373 |
machinery. This attribute is mainly for experimentation.
|
wenzelm@9614
|
374 |
|
wenzelm@8517
|
375 |
\end{descr}
|
wenzelm@7135
|
376 |
|
wenzelm@7135
|
377 |
|
wenzelm@9606
|
378 |
\section{Tactic emulations}\label{sec:tactics}
|
wenzelm@9606
|
379 |
|
wenzelm@9606
|
380 |
The following improper proof methods emulate traditional tactics. These admit
|
wenzelm@9606
|
381 |
direct access to the goal state, which is normally considered harmful! In
|
wenzelm@9606
|
382 |
particular, this may involve both numbered goal addressing (default 1), and
|
wenzelm@9606
|
383 |
dynamic instantiation within the scope of some subgoal.
|
wenzelm@9606
|
384 |
|
wenzelm@9606
|
385 |
\begin{warn}
|
wenzelm@9606
|
386 |
Dynamic instantiations are read and type-checked according to a subgoal of
|
wenzelm@9606
|
387 |
the current dynamic goal state, rather than the static proof context! In
|
wenzelm@9606
|
388 |
particular, locally fixed variables and term abbreviations may not be
|
wenzelm@9606
|
389 |
included in the term specifications. Thus schematic variables are left to
|
wenzelm@9606
|
390 |
be solved by unification with certain parts of the subgoal involved.
|
wenzelm@9606
|
391 |
\end{warn}
|
wenzelm@9606
|
392 |
|
wenzelm@9606
|
393 |
Note that the tactic emulation proof methods in Isabelle/Isar are consistently
|
wenzelm@9606
|
394 |
named $foo_tac$.
|
wenzelm@9606
|
395 |
|
wenzelm@9606
|
396 |
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
|
wenzelm@9606
|
397 |
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
|
wenzelm@9606
|
398 |
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
|
wenzelm@9642
|
399 |
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
|
wenzelm@9614
|
400 |
\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
|
wenzelm@9606
|
401 |
\begin{matharray}{rcl}
|
wenzelm@9606
|
402 |
rule_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
403 |
erule_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
404 |
drule_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
405 |
frule_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
406 |
cut_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
407 |
thin_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
408 |
subgoal_tac^* & : & \isarmeth \\
|
wenzelm@9614
|
409 |
rename_tac^* & : & \isarmeth \\
|
wenzelm@9614
|
410 |
rotate_tac^* & : & \isarmeth \\
|
wenzelm@9606
|
411 |
tactic^* & : & \isarmeth \\
|
wenzelm@9606
|
412 |
\end{matharray}
|
wenzelm@9606
|
413 |
|
wenzelm@9606
|
414 |
\railalias{ruletac}{rule\_tac}
|
wenzelm@9606
|
415 |
\railterm{ruletac}
|
wenzelm@9606
|
416 |
|
wenzelm@9606
|
417 |
\railalias{eruletac}{erule\_tac}
|
wenzelm@9606
|
418 |
\railterm{eruletac}
|
wenzelm@9606
|
419 |
|
wenzelm@9606
|
420 |
\railalias{druletac}{drule\_tac}
|
wenzelm@9606
|
421 |
\railterm{druletac}
|
wenzelm@9606
|
422 |
|
wenzelm@9606
|
423 |
\railalias{fruletac}{frule\_tac}
|
wenzelm@9606
|
424 |
\railterm{fruletac}
|
wenzelm@9606
|
425 |
|
wenzelm@9606
|
426 |
\railalias{cuttac}{cut\_tac}
|
wenzelm@9606
|
427 |
\railterm{cuttac}
|
wenzelm@9606
|
428 |
|
wenzelm@9606
|
429 |
\railalias{thintac}{thin\_tac}
|
wenzelm@9606
|
430 |
\railterm{thintac}
|
wenzelm@9606
|
431 |
|
wenzelm@9606
|
432 |
\railalias{subgoaltac}{subgoal\_tac}
|
wenzelm@9606
|
433 |
\railterm{subgoaltac}
|
wenzelm@9606
|
434 |
|
wenzelm@9614
|
435 |
\railalias{renametac}{rename\_tac}
|
wenzelm@9614
|
436 |
\railterm{renametac}
|
wenzelm@9614
|
437 |
|
wenzelm@9614
|
438 |
\railalias{rotatetac}{rotate\_tac}
|
wenzelm@9614
|
439 |
\railterm{rotatetac}
|
wenzelm@9614
|
440 |
|
wenzelm@9606
|
441 |
\begin{rail}
|
wenzelm@9606
|
442 |
( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
|
wenzelm@9606
|
443 |
( insts thmref | thmrefs )
|
wenzelm@9606
|
444 |
;
|
wenzelm@9606
|
445 |
subgoaltac goalspec? (prop +)
|
wenzelm@9606
|
446 |
;
|
wenzelm@9614
|
447 |
renametac goalspec? (name +)
|
wenzelm@9614
|
448 |
;
|
wenzelm@9614
|
449 |
rotatetac goalspec? int?
|
wenzelm@9614
|
450 |
;
|
wenzelm@9606
|
451 |
'tactic' text
|
wenzelm@9606
|
452 |
;
|
wenzelm@9606
|
453 |
|
wenzelm@9606
|
454 |
insts: ((name '=' term) + 'and') 'in'
|
wenzelm@9606
|
455 |
;
|
wenzelm@9606
|
456 |
\end{rail}
|
wenzelm@9606
|
457 |
|
wenzelm@9606
|
458 |
\begin{descr}
|
wenzelm@9606
|
459 |
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
|
wenzelm@9606
|
460 |
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
|
wenzelm@9606
|
461 |
\cite[\S3]{isabelle-ref}).
|
wenzelm@9614
|
462 |
|
wenzelm@9606
|
463 |
Note that multiple rules may be only given there is no instantiation. Then
|
wenzelm@9606
|
464 |
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see
|
wenzelm@9606
|
465 |
\cite[\S3]{isabelle-ref}).
|
wenzelm@9606
|
466 |
\item [$cut_tac$] inserts facts into the proof state as assumption of a
|
wenzelm@9606
|
467 |
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note
|
wenzelm@9606
|
468 |
that the scope of schmatic variables is spread over the main goal statement.
|
wenzelm@9606
|
469 |
Instantiations may be given as well, see also ML tactic
|
wenzelm@9606
|
470 |
\texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
|
wenzelm@9606
|
471 |
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
|
wenzelm@9606
|
472 |
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in
|
wenzelm@9606
|
473 |
\cite[\S3]{isabelle-ref}.
|
wenzelm@9606
|
474 |
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See
|
wenzelm@9606
|
475 |
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
|
wenzelm@9606
|
476 |
\cite[\S3]{isabelle-ref}.
|
wenzelm@9614
|
477 |
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list
|
wenzelm@9614
|
478 |
$\vec x$, which refers to the \emph{suffix} of variables.
|
wenzelm@9614
|
479 |
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
|
wenzelm@9614
|
480 |
from right to left if $n$ is positive, and from left to right if $n$ is
|
wenzelm@9614
|
481 |
negative; the default value is $1$. See also \texttt{rotate_tac} in
|
wenzelm@9614
|
482 |
\cite[\S3]{isabelle-ref}.
|
wenzelm@9606
|
483 |
\item [$tactic~text$] produces a proof method from any ML text of type
|
wenzelm@9606
|
484 |
\texttt{tactic}. Apart from the usual ML environment and the current
|
wenzelm@9606
|
485 |
implicit theory context, the ML code may refer to the following locally
|
wenzelm@9606
|
486 |
bound values:
|
wenzelm@9606
|
487 |
|
wenzelm@9606
|
488 |
%%FIXME ttbox produces too much trailing space (why?)
|
wenzelm@9606
|
489 |
{\footnotesize\begin{verbatim}
|
wenzelm@9606
|
490 |
val ctxt : Proof.context
|
wenzelm@9606
|
491 |
val facts : thm list
|
wenzelm@9606
|
492 |
val thm : string -> thm
|
wenzelm@9606
|
493 |
val thms : string -> thm list
|
wenzelm@9606
|
494 |
\end{verbatim}}
|
wenzelm@9606
|
495 |
Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
|
wenzelm@9606
|
496 |
indicates any current facts for forward-chaining, and
|
wenzelm@9606
|
497 |
\texttt{thm}~/~\texttt{thms} retrieve named facts (including global
|
wenzelm@9606
|
498 |
theorems) from the context.
|
wenzelm@9606
|
499 |
\end{descr}
|
wenzelm@9606
|
500 |
|
wenzelm@9606
|
501 |
|
wenzelm@9614
|
502 |
\section{The Simplifier}\label{sec:simplifier}
|
wenzelm@7135
|
503 |
|
wenzelm@7321
|
504 |
\subsection{Simplification methods}\label{sec:simp}
|
wenzelm@7315
|
505 |
|
wenzelm@8483
|
506 |
\indexisarmeth{simp}\indexisarmeth{simp-all}
|
wenzelm@7315
|
507 |
\begin{matharray}{rcl}
|
wenzelm@7315
|
508 |
simp & : & \isarmeth \\
|
wenzelm@8483
|
509 |
simp_all & : & \isarmeth \\
|
wenzelm@7315
|
510 |
\end{matharray}
|
wenzelm@7315
|
511 |
|
wenzelm@8483
|
512 |
\railalias{simpall}{simp\_all}
|
wenzelm@8483
|
513 |
\railterm{simpall}
|
wenzelm@8483
|
514 |
|
wenzelm@8704
|
515 |
\railalias{noasm}{no\_asm}
|
wenzelm@8704
|
516 |
\railterm{noasm}
|
wenzelm@8704
|
517 |
|
wenzelm@8704
|
518 |
\railalias{noasmsimp}{no\_asm\_simp}
|
wenzelm@8704
|
519 |
\railterm{noasmsimp}
|
wenzelm@8704
|
520 |
|
wenzelm@8704
|
521 |
\railalias{noasmuse}{no\_asm\_use}
|
wenzelm@8704
|
522 |
\railterm{noasmuse}
|
wenzelm@8704
|
523 |
|
wenzelm@7315
|
524 |
\begin{rail}
|
wenzelm@8706
|
525 |
('simp' | simpall) ('!' ?) opt? (simpmod * )
|
wenzelm@7315
|
526 |
;
|
wenzelm@7315
|
527 |
|
wenzelm@8811
|
528 |
opt: '(' (noasm | noasmsimp | noasmuse) ')'
|
wenzelm@8704
|
529 |
;
|
wenzelm@9711
|
530 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
|
wenzelm@9847
|
531 |
'split' (() | 'add' | 'del')) ':' thmrefs
|
wenzelm@7315
|
532 |
;
|
wenzelm@7315
|
533 |
\end{rail}
|
wenzelm@7315
|
534 |
|
wenzelm@7321
|
535 |
\begin{descr}
|
wenzelm@8547
|
536 |
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
|
wenzelm@8594
|
537 |
according to the arguments given. Note that the \railtterm{only} modifier
|
wenzelm@8547
|
538 |
first removes all other rewrite rules, congruences, and looper tactics
|
wenzelm@8594
|
539 |
(including splits), and then behaves like \railtterm{add}.
|
wenzelm@9711
|
540 |
|
wenzelm@9711
|
541 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
|
wenzelm@9711
|
542 |
rules (see also \cite{isabelle-ref}), the default is to add.
|
wenzelm@9711
|
543 |
|
wenzelm@9711
|
544 |
\medskip The \railtterm{split} modifiers add or delete rules for the
|
wenzelm@9711
|
545 |
Splitter (see also \cite{isabelle-ref}), the default is to add. This works
|
wenzelm@9711
|
546 |
only if the Simplifier method has been properly setup to include the
|
wenzelm@9711
|
547 |
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
|
wenzelm@8483
|
548 |
\item [$simp_all$] is similar to $simp$, but acts on all goals.
|
wenzelm@7321
|
549 |
\end{descr}
|
wenzelm@7321
|
550 |
|
wenzelm@8704
|
551 |
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
|
wenzelm@8706
|
552 |
internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
|
wenzelm@8706
|
553 |
simplified as well as used in simplifying the conclusion. In structured
|
wenzelm@8706
|
554 |
proofs this is usually quite well behaved in practice: just the local premises
|
wenzelm@8706
|
555 |
of the actual goal are involved, additional facts may inserted via explicit
|
wenzelm@8706
|
556 |
forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The full context of
|
wenzelm@8706
|
557 |
assumptions is only included if the ``$!$'' (bang) argument is given, which
|
wenzelm@8706
|
558 |
should be used with some care, though.
|
wenzelm@7321
|
559 |
|
wenzelm@8704
|
560 |
Additional Simplifier options may be specified to tune the behavior even
|
wenzelm@9614
|
561 |
further: $(no_asm)$ means assumptions are ignored completely (cf.\
|
wenzelm@8811
|
562 |
\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
|
wenzelm@9614
|
563 |
simplification of the conclusion but are not themselves simplified (cf.\
|
wenzelm@8811
|
564 |
\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
|
wenzelm@8811
|
565 |
but are not used in the simplification of each other or the conclusion (cf.
|
wenzelm@8704
|
566 |
\texttt{full_simp_tac}).
|
wenzelm@8704
|
567 |
|
wenzelm@8704
|
568 |
\medskip
|
wenzelm@8704
|
569 |
|
wenzelm@8704
|
570 |
The Splitter package is usually configured to work as part of the Simplifier.
|
wenzelm@9711
|
571 |
The effect of repeatedly applying \texttt{split_tac} can be simulated by
|
wenzelm@9711
|
572 |
$(simp~only\colon~split\colon~\vec a)$. There is also a separate $split$
|
wenzelm@9711
|
573 |
method available for single-step case splitting, see \S\ref{sec:basic-eq}.
|
wenzelm@8483
|
574 |
|
wenzelm@8483
|
575 |
|
wenzelm@8483
|
576 |
\subsection{Declaring rules}
|
wenzelm@8483
|
577 |
|
wenzelm@8667
|
578 |
\indexisarcmd{print-simpset}
|
wenzelm@8638
|
579 |
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
|
wenzelm@7321
|
580 |
\begin{matharray}{rcl}
|
wenzelm@8667
|
581 |
print_simpset & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7321
|
582 |
simp & : & \isaratt \\
|
wenzelm@9711
|
583 |
cong & : & \isaratt \\
|
wenzelm@8483
|
584 |
split & : & \isaratt \\
|
wenzelm@7321
|
585 |
\end{matharray}
|
wenzelm@7321
|
586 |
|
wenzelm@7321
|
587 |
\begin{rail}
|
wenzelm@9711
|
588 |
('simp' | 'cong' | 'split') (() | 'add' | 'del')
|
wenzelm@7321
|
589 |
;
|
wenzelm@7321
|
590 |
\end{rail}
|
wenzelm@7321
|
591 |
|
wenzelm@7321
|
592 |
\begin{descr}
|
wenzelm@8667
|
593 |
\item [$print_simpset$] prints the collection of rules declared to the
|
wenzelm@8667
|
594 |
Simplifier, which is also known as ``simpset'' internally
|
wenzelm@8667
|
595 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
|
wenzelm@8547
|
596 |
\item [$simp$] declares simplification rules.
|
wenzelm@8638
|
597 |
\item [$cong$] declares congruence rules.
|
wenzelm@9711
|
598 |
\item [$split$] declares case split rules.
|
wenzelm@7321
|
599 |
\end{descr}
|
wenzelm@7319
|
600 |
|
wenzelm@7315
|
601 |
|
wenzelm@7315
|
602 |
\subsection{Forward simplification}
|
wenzelm@7315
|
603 |
|
wenzelm@7391
|
604 |
\indexisaratt{simplify}\indexisaratt{asm-simplify}
|
wenzelm@7391
|
605 |
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
|
wenzelm@7315
|
606 |
\begin{matharray}{rcl}
|
wenzelm@7315
|
607 |
simplify & : & \isaratt \\
|
wenzelm@7315
|
608 |
asm_simplify & : & \isaratt \\
|
wenzelm@7315
|
609 |
full_simplify & : & \isaratt \\
|
wenzelm@7315
|
610 |
asm_full_simplify & : & \isaratt \\
|
wenzelm@7315
|
611 |
\end{matharray}
|
wenzelm@7315
|
612 |
|
wenzelm@7321
|
613 |
These attributes provide forward rules for simplification, which should be
|
wenzelm@8547
|
614 |
used only very rarely. There are no separate options for declaring
|
wenzelm@7905
|
615 |
simplification rules locally.
|
wenzelm@7905
|
616 |
|
wenzelm@7905
|
617 |
See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
|
wenzelm@7905
|
618 |
information.
|
wenzelm@7315
|
619 |
|
wenzelm@7315
|
620 |
|
wenzelm@9711
|
621 |
\section{Basic equational reasoning}\label{sec:basic-eq}
|
wenzelm@9614
|
622 |
|
wenzelm@9703
|
623 |
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
|
wenzelm@9614
|
624 |
\begin{matharray}{rcl}
|
wenzelm@9614
|
625 |
subst & : & \isarmeth \\
|
wenzelm@9614
|
626 |
hypsubst^* & : & \isarmeth \\
|
wenzelm@9703
|
627 |
split & : & \isarmeth \\
|
wenzelm@9614
|
628 |
symmetric & : & \isaratt \\
|
wenzelm@9614
|
629 |
\end{matharray}
|
wenzelm@9614
|
630 |
|
wenzelm@9614
|
631 |
\begin{rail}
|
wenzelm@9614
|
632 |
'subst' thmref
|
wenzelm@9614
|
633 |
;
|
wenzelm@9799
|
634 |
'split' ('(' 'asm' ')')? thmrefs
|
wenzelm@9703
|
635 |
;
|
wenzelm@9614
|
636 |
\end{rail}
|
wenzelm@9614
|
637 |
|
wenzelm@9614
|
638 |
These methods and attributes provide basic facilities for equational reasoning
|
wenzelm@9614
|
639 |
that are intended for specialized applications only. Normally, single step
|
wenzelm@9614
|
640 |
reasoning would be performed by calculation (see \S\ref{sec:calculation}),
|
wenzelm@9614
|
641 |
while the Simplifier is the canonical tool for automated normalization (see
|
wenzelm@9614
|
642 |
\S\ref{sec:simplifier}).
|
wenzelm@9614
|
643 |
|
wenzelm@9614
|
644 |
\begin{descr}
|
wenzelm@9614
|
645 |
\item [$subst~thm$] performs a single substitution step using rule $thm$,
|
wenzelm@9614
|
646 |
which may be either a meta or object equality.
|
wenzelm@9614
|
647 |
\item [$hypsubst$] performs substitution using some assumption.
|
wenzelm@9703
|
648 |
\item [$split~thms$] performs single-step case splitting using rules $thms$.
|
wenzelm@9799
|
649 |
By default, splitting is performed in the conclusion of a goal; the $asm$
|
wenzelm@9799
|
650 |
option indicates to operate on assumptions instead.
|
wenzelm@9799
|
651 |
|
wenzelm@9703
|
652 |
Note that the $simp$ method already involves repeated application of split
|
wenzelm@9703
|
653 |
rules as declared in the current context (see \S\ref{sec:simp}).
|
wenzelm@9614
|
654 |
\item [$symmetric$] applies the symmetry rule of meta or object equality.
|
wenzelm@9614
|
655 |
\end{descr}
|
wenzelm@9614
|
656 |
|
wenzelm@9614
|
657 |
|
wenzelm@9847
|
658 |
\section{The Classical Reasoner}\label{sec:classical}
|
wenzelm@7135
|
659 |
|
wenzelm@7335
|
660 |
\subsection{Basic methods}\label{sec:classical-basic}
|
wenzelm@7315
|
661 |
|
wenzelm@7974
|
662 |
\indexisarmeth{rule}\indexisarmeth{intro}
|
wenzelm@7974
|
663 |
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
|
wenzelm@7321
|
664 |
\begin{matharray}{rcl}
|
wenzelm@7321
|
665 |
rule & : & \isarmeth \\
|
wenzelm@7321
|
666 |
intro & : & \isarmeth \\
|
wenzelm@7321
|
667 |
elim & : & \isarmeth \\
|
wenzelm@7321
|
668 |
contradiction & : & \isarmeth \\
|
wenzelm@7321
|
669 |
\end{matharray}
|
wenzelm@7321
|
670 |
|
wenzelm@7321
|
671 |
\begin{rail}
|
wenzelm@8547
|
672 |
('rule' | 'intro' | 'elim') thmrefs?
|
wenzelm@7321
|
673 |
;
|
wenzelm@7321
|
674 |
\end{rail}
|
wenzelm@7321
|
675 |
|
wenzelm@7321
|
676 |
\begin{descr}
|
wenzelm@7466
|
677 |
\item [$rule$] as offered by the classical reasoner is a refinement over the
|
wenzelm@8517
|
678 |
primitive one (see \S\ref{sec:pure-meth-att}). In case that no rules are
|
wenzelm@7466
|
679 |
provided as arguments, it automatically determines elimination and
|
wenzelm@7321
|
680 |
introduction rules from the context (see also \S\ref{sec:classical-mod}).
|
wenzelm@8517
|
681 |
This is made the default method for basic proof steps, such as $\PROOFNAME$
|
wenzelm@8517
|
682 |
and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
|
wenzelm@8517
|
683 |
\S\ref{sec:pure-meth-att}.
|
wenzelm@9614
|
684 |
|
wenzelm@7466
|
685 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
|
wenzelm@7905
|
686 |
elim-resolution, after having inserted any facts. Omitting the arguments
|
wenzelm@8547
|
687 |
refers to any suitable rules declared in the context, otherwise only the
|
wenzelm@8547
|
688 |
explicitly given ones may be applied. The latter form admits better control
|
wenzelm@8547
|
689 |
of what actually happens, thus it is very appropriate as an initial method
|
wenzelm@8547
|
690 |
for $\PROOFNAME$ that splits up certain connectives of the goal, before
|
wenzelm@8547
|
691 |
entering the actual sub-proof.
|
wenzelm@9614
|
692 |
|
wenzelm@7466
|
693 |
\item [$contradiction$] solves some goal by contradiction, deriving any result
|
wenzelm@7466
|
694 |
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
|
wenzelm@7466
|
695 |
appear in either order.
|
wenzelm@7321
|
696 |
\end{descr}
|
wenzelm@7321
|
697 |
|
wenzelm@7321
|
698 |
|
wenzelm@7981
|
699 |
\subsection{Automated methods}\label{sec:classical-auto}
|
wenzelm@7321
|
700 |
|
wenzelm@9799
|
701 |
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
|
wenzelm@9799
|
702 |
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
|
wenzelm@7321
|
703 |
\begin{matharray}{rcl}
|
wenzelm@9780
|
704 |
blast & : & \isarmeth \\
|
wenzelm@9780
|
705 |
fast & : & \isarmeth \\
|
wenzelm@9799
|
706 |
slow & : & \isarmeth \\
|
wenzelm@9780
|
707 |
best & : & \isarmeth \\
|
wenzelm@9780
|
708 |
safe & : & \isarmeth \\
|
wenzelm@9780
|
709 |
clarify & : & \isarmeth \\
|
wenzelm@7321
|
710 |
\end{matharray}
|
wenzelm@7321
|
711 |
|
wenzelm@7321
|
712 |
\begin{rail}
|
wenzelm@7905
|
713 |
'blast' ('!' ?) nat? (clamod * )
|
wenzelm@7321
|
714 |
;
|
wenzelm@9799
|
715 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * )
|
wenzelm@7321
|
716 |
;
|
wenzelm@7321
|
717 |
|
wenzelm@9408
|
718 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
|
wenzelm@7321
|
719 |
;
|
wenzelm@7321
|
720 |
\end{rail}
|
wenzelm@7321
|
721 |
|
wenzelm@7321
|
722 |
\begin{descr}
|
wenzelm@7321
|
723 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
|
wenzelm@7335
|
724 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a
|
wenzelm@9606
|
725 |
user-supplied search bound (default 20). Note that $blast$ is the only
|
wenzelm@9606
|
726 |
classical proof procedure in Isabelle that can handle actual object-logic
|
wenzelm@9606
|
727 |
rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
|
wenzelm@9606
|
728 |
facts).
|
wenzelm@9799
|
729 |
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
|
wenzelm@9799
|
730 |
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac},
|
wenzelm@9799
|
731 |
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
|
wenzelm@9799
|
732 |
\cite[\S11]{isabelle-ref} for more information.
|
wenzelm@7321
|
733 |
\end{descr}
|
wenzelm@7321
|
734 |
|
wenzelm@7321
|
735 |
Any of above methods support additional modifiers of the context of classical
|
wenzelm@8517
|
736 |
rules. Their semantics is analogous to the attributes given in
|
wenzelm@8547
|
737 |
\S\ref{sec:classical-mod}. Facts provided by forward chaining are
|
wenzelm@8547
|
738 |
inserted\footnote{These methods usually cannot make proper use of actual rules
|
wenzelm@8547
|
739 |
inserted that way, though.} into the goal before doing the search. The
|
wenzelm@8547
|
740 |
``!''~argument causes the full context of assumptions to be included as well.
|
wenzelm@8547
|
741 |
This is slightly less hazardous than for the Simplifier (see
|
wenzelm@8547
|
742 |
\S\ref{sec:simp}).
|
wenzelm@7321
|
743 |
|
wenzelm@7315
|
744 |
|
wenzelm@9847
|
745 |
\subsection{Combined automated methods}\label{sec:clasimp}
|
wenzelm@7315
|
746 |
|
wenzelm@9799
|
747 |
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
|
wenzelm@9799
|
748 |
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
|
wenzelm@7321
|
749 |
\begin{matharray}{rcl}
|
wenzelm@9606
|
750 |
auto & : & \isarmeth \\
|
wenzelm@7321
|
751 |
force & : & \isarmeth \\
|
wenzelm@9438
|
752 |
clarsimp & : & \isarmeth \\
|
wenzelm@9606
|
753 |
fastsimp & : & \isarmeth \\
|
wenzelm@9799
|
754 |
slowsimp & : & \isarmeth \\
|
wenzelm@9799
|
755 |
bestsimp & : & \isarmeth \\
|
wenzelm@7321
|
756 |
\end{matharray}
|
wenzelm@7315
|
757 |
|
wenzelm@7321
|
758 |
\begin{rail}
|
wenzelm@9780
|
759 |
'auto' '!'? (nat nat)? (clasimpmod * )
|
wenzelm@9780
|
760 |
;
|
wenzelm@9799
|
761 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * )
|
wenzelm@7321
|
762 |
;
|
wenzelm@7315
|
763 |
|
wenzelm@9711
|
764 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
|
wenzelm@9847
|
765 |
('cong' | 'split' | 'iff') (() | 'add' | 'del') |
|
wenzelm@9408
|
766 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
|
wenzelm@7321
|
767 |
\end{rail}
|
wenzelm@7135
|
768 |
|
wenzelm@7321
|
769 |
\begin{descr}
|
wenzelm@9799
|
770 |
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
|
wenzelm@9799
|
771 |
provide access to Isabelle's combined simplification and classical reasoning
|
wenzelm@9799
|
772 |
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac},
|
wenzelm@9799
|
773 |
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
|
wenzelm@9799
|
774 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The
|
wenzelm@9799
|
775 |
modifier arguments correspond to those given in \S\ref{sec:simp} and
|
wenzelm@9606
|
776 |
\S\ref{sec:classical-auto}. Just note that the ones related to the
|
wenzelm@9606
|
777 |
Simplifier are prefixed by \railtterm{simp} here.
|
wenzelm@9614
|
778 |
|
wenzelm@7987
|
779 |
Facts provided by forward chaining are inserted into the goal before doing
|
wenzelm@7987
|
780 |
the search. The ``!''~argument causes the full context of assumptions to be
|
wenzelm@7987
|
781 |
included as well.
|
wenzelm@7321
|
782 |
\end{descr}
|
wenzelm@7135
|
783 |
|
wenzelm@7987
|
784 |
|
wenzelm@8483
|
785 |
\subsection{Declaring rules}\label{sec:classical-mod}
|
wenzelm@7135
|
786 |
|
wenzelm@8667
|
787 |
\indexisarcmd{print-claset}
|
wenzelm@7391
|
788 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
|
wenzelm@7391
|
789 |
\indexisaratt{iff}\indexisaratt{delrule}
|
wenzelm@7321
|
790 |
\begin{matharray}{rcl}
|
wenzelm@8667
|
791 |
print_claset & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7321
|
792 |
intro & : & \isaratt \\
|
wenzelm@7321
|
793 |
elim & : & \isaratt \\
|
wenzelm@7321
|
794 |
dest & : & \isaratt \\
|
wenzelm@7391
|
795 |
iff & : & \isaratt \\
|
wenzelm@7321
|
796 |
delrule & : & \isaratt \\
|
wenzelm@7321
|
797 |
\end{matharray}
|
wenzelm@7321
|
798 |
|
wenzelm@7321
|
799 |
\begin{rail}
|
wenzelm@9408
|
800 |
('intro' | 'elim' | 'dest') ('!' | () | '?')
|
wenzelm@7321
|
801 |
;
|
wenzelm@8638
|
802 |
'iff' (() | 'add' | 'del')
|
wenzelm@7321
|
803 |
\end{rail}
|
wenzelm@7321
|
804 |
|
wenzelm@7321
|
805 |
\begin{descr}
|
wenzelm@8667
|
806 |
\item [$print_claset$] prints the collection of rules declared to the
|
wenzelm@8667
|
807 |
Classical Reasoner, which is also known as ``simpset'' internally
|
wenzelm@8667
|
808 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
|
wenzelm@8517
|
809 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
|
wenzelm@8517
|
810 |
destruct rules, respectively. By default, rules are considered as
|
wenzelm@9408
|
811 |
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
|
wenzelm@9408
|
812 |
single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
|
wenzelm@9408
|
813 |
applied in the search-oriented automated methods, but only in single-step
|
wenzelm@9408
|
814 |
methods such as $rule$).
|
wenzelm@9614
|
815 |
|
wenzelm@8547
|
816 |
\item [$iff$] declares equations both as rules for the Simplifier and
|
wenzelm@8547
|
817 |
Classical Reasoner.
|
wenzelm@7391
|
818 |
|
wenzelm@7335
|
819 |
\item [$delrule$] deletes introduction or elimination rules from the context.
|
wenzelm@7335
|
820 |
Note that destruction rules would have to be turned into elimination rules
|
wenzelm@7321
|
821 |
first, e.g.\ by using the $elimify$ attribute.
|
wenzelm@7321
|
822 |
\end{descr}
|
wenzelm@7135
|
823 |
|
wenzelm@8203
|
824 |
|
wenzelm@9614
|
825 |
%%% Local Variables:
|
wenzelm@7135
|
826 |
%%% mode: latex
|
wenzelm@7135
|
827 |
%%% TeX-master: "isar-ref"
|
wenzelm@9614
|
828 |
%%% End:
|