7135

1 

7167

2 
\chapter{Generic Tools and Packages}\label{ch:gentools}


3 

7315

4 
\section{Basic proof methods}\label{sec:puremeth}

7167

5 


6 
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$$}\indexisarmeth{assumption}


7 
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}


8 
\indexisarmeth{rule}\indexisarmeth{erule}


9 
\begin{matharray}{rcl}


10 
 & : & \isarmeth \\


11 
assumption & : & \isarmeth \\

7321

12 
finish & : & \isarmeth \\[0.5ex]


13 
rule & : & \isarmeth \\


14 
erule^* & : & \isarmeth \\[0.5ex]

7167

15 
fold & : & \isarmeth \\

7321

16 
unfold & : & \isarmeth \\[0.5ex]


17 
fail & : & \isarmeth \\


18 
succeed & : & \isarmeth \\

7167

19 
\end{matharray}


20 


21 
\begin{rail}


22 
('fold'  'unfold'  'rule'  'erule') thmrefs


23 
;


24 
\end{rail}


25 


26 
\begin{descr}

7321

27 
\item [``$$''] does nothing but insert the forward chaining facts as premises


28 
into the goal. Note that command $\PROOFNAME$ without any method given


29 
actually performs a single reduction step using the $rule$ method (see


30 
below); thus a plain \emph{donothing} proof step would be $\PROOF{}$


31 
rather than $\PROOFNAME$ alone.


32 
\item [$assumption$] solves some goal by assumption (after inserting the


33 
goal's facts).


34 
\item [$finish$] solves all remaining goals by assumption; this is the default


35 
terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be


36 
spelled out explicitly.


37 
\item [$rule~thms$] applies some rule given as argument in backward manner;


38 
facts are used to reduce the rule before applying it to the goal. Thus


39 
$rule$ without facts is plain \emph{introduction}, while with facts it


40 
becomes an \emph{elimination}.


41 


42 
Note that the classical reasoner introduces another version of $rule$ that


43 
is able to pick appropriate rules automatically, whenever explicit $thms$


44 
are omitted (see \S\ref{sec:classicalbasic}) . That method is the default


45 
one for proof steps such as $\PROOFNAME$ and ``$\DDOT$'' (two dots).


46 


47 
\item [$erule~thms$] is similar to $rule$, but applies rules by


48 
elimresolution. This is an improper method, mainly for experimentation and


49 
porting of old script. Actual elimination proofs are usually done with


50 
$rule$ (single step) or $elim$ (multiple steps, see


51 
\S\ref{sec:classicalbasic}).


52 


53 
\item [$unfold~thms$ and $fold~thms$] expand and fold back again metalevel


54 
definitions $thms$ throughout all goals; facts may not be given.

7167

55 

7321

56 
\item [$fail$] yields an empty result sequence; it is the identify of the


57 
``\texttt{}'' method combinator.


58 


59 
\item [$succeed$] yields a singleton result, which is unchanged except for the


60 
change from $prove$ mode back to $state$; it is the identify of the


61 
``\texttt{,}'' method combinator.


62 
\end{descr}

7167

63 

7315

64 


65 
\section{Miscellaneous attributes}


66 

7167

67 
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}


68 
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}


69 
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}


70 
\begin{matharray}{rcl}


71 
tag & : & \isaratt \\

7321

72 
untag & : & \isaratt \\[0.5ex]


73 
OF & : & \isaratt \\

7167

74 
RS & : & \isaratt \\

7321

75 
COMP & : & \isaratt \\[0.5ex]

7167

76 
where & : & \isaratt \\

7321

77 
of & : & \isaratt \\[0.5ex]

7167

78 
standard & : & \isaratt \\


79 
elimify & : & \isaratt \\

7321

80 
export & : & \isaratt \\

7167

81 
transfer & : & \isaratt \\


82 
\end{matharray}


83 


84 
\begin{rail}


85 
('tag'  'untag') (nameref+)


86 
;


87 
'OF' thmrefs


88 
;

7321

89 
('RS'  'COMP') nat? thmref

7167

90 
;

7175

91 
'of' (inst * ) ('concl' ':' (inst * ))?

7167

92 
;

7321

93 
'where' (name '=' term * 'and')


94 
;

7167

95 


96 
inst: underscore  term


97 
;


98 
\end{rail}


99 


100 
\begin{descr}

7321

101 
\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,


102 
respectively. Tags may be any list of strings that serve as comment for


103 
some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the


104 
result).


105 
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies


106 
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelleref}, but note


107 
the reversed order). $RS$ resolves with the $n$th premise of $thm$; $COMP$


108 
is a version of $RS$ that does not include the automatic lifting process


109 
that is normally desired (see \texttt{RS} and \texttt{COMP} in


110 
\cite[\S5]{isabelleref}).


111 


112 
\item [$of~ts$ and $where~insts$] perform positional and named instantiation,


113 
respectively. The terms given in $of$ are substituted for any variables


114 
occurring in a theorem from left to right; ``\texttt{_}'' (underscore)


115 
indicates to skip a position.


116 


117 
\item [$standard$] puts a theorem into the standard form of objectrules, just


118 
as the ML function \texttt{standard} (see \cite[\S5]{isabelleref}).


119 


120 
\item [$elimify$] turns an destruction rule (such as projection $conjunct@1$


121 
into an elimination.


122 


123 
\item [$export$] lifts a local result out of the current proof context,


124 
generalizing all fixed variables and discharging all assumptions. Export is


125 
usually done automatically behind the scenes. This attribute is mainly for


126 
experimentation.


127 


128 
\item [$transfer$] promotes a theorem to the current theory context, which has


129 
to enclose the former one. Normally, this is done automatically when rules


130 
are joined by inference.


131 

7167

132 
\end{descr}


133 

7315

134 


135 
\section{Calculational proof}\label{sec:calculation}


136 


137 
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}


138 
\begin{matharray}{rcl}


139 
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\


140 
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\


141 
trans & : & \isaratt \\


142 
\end{matharray}


143 


144 
Calculational proof is forward reasoning with implicit application of


145 
transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains


146 
an auxiliary register $calculation$\indexisarreg{calculation} for accumulating


147 
results obtained by transitivity obtained together with the current facts.


148 
Command $\ALSO$ updates $calculation$ from the most recent result, while


149 
$\FINALLY$ exhibits the final result by forward chaining towards the next goal


150 
statement. Both commands require valid current facts, i.e.\ may occur only


151 
after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or


152 
some finished $\HAVENAME$ or $\SHOWNAME$.


153 


154 
Also note that the automatic term abbreviation ``$\dots$'' has its canonical


155 
application with calculational proofs. It automatically refers to the


156 
argument\footnote{The argument of a curried infix expression is its righthand


157 
side.} of the preceding statement.


158 


159 
Isabelle/Isar calculations are implicitly subject to block structure in the


160 
sense that new threads of calculational reasoning are commenced for any new


161 
block (as opened by a local goal, for example). This means that, apart from


162 
being able to nest calculations, there is no separate \emph{begincalculation}


163 
command required.


164 


165 
\begin{rail}


166 
('also'  'finally') transrules? comment?


167 
;


168 
'trans' (()  'add' ':'  'del' ':') thmrefs


169 
;


170 


171 
transrules: '(' thmrefs ')' interest?


172 
;


173 
\end{rail}


174 


175 
\begin{descr}


176 
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as


177 
follows. The first occurrence of $\ALSO$ in some calculational thread


178 
initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the


179 
\emph{same} level of blockstructure updates $calculation$ by some


180 
transitivity rule applied to $calculation$ and $facts$ (in that order).


181 
Transitivity rules are picked from the current context plus those given as


182 
$thms$ (the latter have precedence).


183 


184 
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as


185 
$\ALSO$, and concludes the current calculational thread. The final result


186 
is exhibited as fact for forward chaining towards the next goal. Basically,


187 
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof


188 
idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.


189 


190 
\item [Attribute $trans$] maintains the set of transitivity rules of the


191 
theory or proof context, by adding or deleting the theorems provided as


192 
arguments. The default is adding of rules.


193 
\end{descr}


194 


195 
See theory \texttt{HOL/Isar_examples/Group} for a simple applications of


196 
calculations for basic equational reasoning.


197 
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced


198 
calculational steps in combination with natural deduction.


199 


200 

7135

201 
\section{Axiomatic Type Classes}\label{sec:axclass}


202 


203 
\indexisarcmd{axclass}\indexisarcmd{instance}


204 
\begin{matharray}{rcl}


205 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\


206 
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

7319

207 
expand_classes & : & \isarmeth \\

7135

208 
\end{matharray}


209 


210 
Axiomatic type classes are provided by Isabelle/Pure as a purely


211 
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus


212 
any object logic may make use of this lightweight mechanism for abstract


213 
theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a


214 
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of


215 
the standard Isabelle documentation.


216 


217 
\begin{rail}


218 
'axclass' classdecl (axmdecl prop comment? +)


219 
;


220 
'instance' (nameref '<' nameref  nameref '::' simplearity) comment?


221 
;


222 
\end{rail}


223 

7167

224 
\begin{descr}

7321

225 
\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the


226 
intersection of existing classes, with additional axioms holding. Class


227 
axioms may not contain more than one type variable. The class axioms (with


228 
implicit sort constraints added) are bound to the given names. Furthermore


229 
a class introduction rule is generated, which is employed by method


230 
$expand_classes$ in support instantiation proofs of this class.


231 

7135

232 
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <


233 
c@2$] setup up a goal stating the class relation or type arity. The proof


234 
would usually proceed by the $expand_classes$ method, and then establish the

7141

235 
characteristic theorems of the type classes involved. After finishing the


236 
proof the theory will be augmented by a type signature declaration

7135

237 
corresponding to the resulting theorem.

7319

238 
\item [Method $expand_classes$] iteratively expands the class introduction


239 
rules

7167

240 
\end{descr}

7135

241 

7319

242 
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using


243 
axiomatic type classes, including instantiation proofs.

7135

244 


245 


246 
\section{The Simplifier}


247 

7321

248 
\subsection{Simplification methods}\label{sec:simp}

7315

249 

7321

250 
\indexisarmeth{simp}\indexisarmeth{asm_simp}

7315

251 
\begin{matharray}{rcl}


252 
simp & : & \isarmeth \\


253 
asm_simp & : & \isarmeth \\


254 
\end{matharray}


255 


256 
\begin{rail}

7319

257 
'simp' (simpmod * )

7315

258 
;


259 


260 
simpmod: ('add'  'del'  'only'  'other') ':' thmrefs


261 
;


262 
\end{rail}


263 

7321

264 
\begin{descr}


265 
\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after


266 
modifying the context as follows adding or deleting given rules. The


267 
\railtoken{only} modifier first removes all other rewrite rules and


268 
congruences, and then is like \railtoken{add}. In contrast,


269 
\railtoken{other} ignores its arguments; nevertheless there may be


270 
sideeffects on the context via attributes. This provides a back door for


271 
arbitrary manipulation of the context.


272 


273 
Both of these methods are based on \texttt{asm_full_simp_tac}, see


274 
\cite[\S10]{isabelleref}.


275 
\end{descr}


276 


277 
\subsection{Modifying the context}


278 


279 
\indexisaratt{simp}


280 
\begin{matharray}{rcl}


281 
simp & : & \isaratt \\


282 
\end{matharray}


283 


284 
\begin{rail}


285 
'simp' (()  'add'  'del')


286 
;


287 
\end{rail}


288 


289 
\begin{descr}


290 
\item [Attribute $simp$] adds or deletes rules from the theory or proof


291 
context. The default is to add rules.


292 
\end{descr}

7319

293 

7315

294 


295 
\subsection{Forward simplification}


296 


297 
\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}


298 
\begin{matharray}{rcl}


299 
simplify & : & \isaratt \\


300 
asm_simplify & : & \isaratt \\


301 
full_simplify & : & \isaratt \\


302 
asm_full_simplify & : & \isaratt \\


303 
\end{matharray}


304 

7321

305 
These attributes provide forward rules for simplification, which should be


306 
used very rarely. See the ML function of the same name in


307 
\cite[\S10]{isabelleref} for more information.

7315

308 


309 

7135

310 
\section{The Classical Reasoner}


311 

7321

312 
\subsection{Basic step methods}\label{sec:classicalbasic}


313 


314 
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}


315 
\begin{matharray}{rcl}


316 
rule & : & \isarmeth \\


317 
intro & : & \isarmeth \\


318 
elim & : & \isarmeth \\


319 
contradiction & : & \isarmeth \\


320 
\end{matharray}


321 


322 
\begin{rail}


323 
('rule'  'intro'  'elim') thmrefs


324 
;


325 
\end{rail}


326 


327 
\begin{descr}


328 
\item [Method $rule$] as offered by the classical reasoner is a refinement


329 
over the primitive one (see \S\ref{sec:puremeth}). In the case that no


330 
rules are provided as arguments, it automatically determines elimination and


331 
introduction rules from the context (see also \S\ref{sec:classicalmod}).


332 
In that form it is the default method for basic proof steps.


333 


334 
\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro or


335 
elimresolution, after having inserted the facts. Omitting the arguments


336 
refers to any suitable rules from the context, otherwise only the explicitly


337 
given ones may be applied. The latter form admits better control of what is


338 
actually happening, thus it is appropriate as an initial proof method that


339 
splits up certain connectives of the goal, before entering the subproof.


340 


341 
\item [Method $contradiction$] solves some goal by contradiction: both $A$ and


342 
$\neg A$ have to be present in the assumptions.


343 
\end{descr}


344 


345 


346 
\subsection{Automatic methods}\label{sec:classicalauto}

7315

347 

7321

348 
\indexisarmeth{blast}


349 
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}


350 
\begin{matharray}{rcl}


351 
blast & : & \isarmeth \\


352 
fast & : & \isarmeth \\


353 
best & : & \isarmeth \\


354 
slow & : & \isarmeth \\


355 
slow_best & : & \isarmeth \\


356 
\end{matharray}


357 


358 
\railalias{slowbest}{slow\_best}


359 
\railterm{slowbest}


360 


361 
\begin{rail}


362 
'blast' nat? (clamod * )


363 
;


364 
('fast'  'best'  'slow'  slowbest) (clamod * )


365 
;


366 


367 
clamod: (('intro'  'elim'  'dest') (()  '!'  '!!')  'del') ':' thmrefs


368 
;


369 
\end{rail}


370 


371 
\begin{descr}


372 
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}


373 
in \cite[\S11]{isabelleref}). The optional argument specifies a applies a


374 
usersupplied search bound (default 20).


375 
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical


376 
reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in


377 
\cite[\S11]{isabelleref}).


378 
\end{descr}


379 


380 
Any of above methods support additional modifiers of the context of classical


381 
rules. There semantics is analogous to the attributes given in


382 
\S\ref{sec:classicalmod}.


383 

7315

384 


385 
\subsection{Combined automatic methods}


386 

7321

387 
\indexisarmeth{auto}\indexisarmeth{force}


388 
\begin{matharray}{rcl}


389 
force & : & \isarmeth \\


390 
auto & : & \isarmeth \\


391 
\end{matharray}


392 


393 
\begin{rail}


394 
('force'  'auto') (clasimpmod * )


395 
;

7315

396 

7321

397 
clasimpmod: ('simp' ('add'  'del'  'only')  other 


398 
(('intro'  'elim'  'dest') (()  '!'  '!!')  'del')) ':' thmrefs


399 
\end{rail}

7315

400 

7321

401 
\begin{descr}


402 
\item [$force$ and $auto$] provide access to Isabelle's combined


403 
simplification and classical reasoning tactics. See \texttt{force_tac} and


404 
\texttt{auto_tac} in \cite[\S11]{isabelleref} for more information. The


405 
modifier arguments correspond to those given in \S\ref{sec:simp} and


406 
\S\ref{sec:classicalauto}.


407 
\end{descr}


408 


409 
\subsection{Modifying the context}\label{sec:classicalmod}

7135

410 

7321

411 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}


412 
\begin{matharray}{rcl}


413 
intro & : & \isaratt \\


414 
elim & : & \isaratt \\


415 
dest & : & \isaratt \\


416 
delrule & : & \isaratt \\


417 
\end{matharray}

7135

418 

7321

419 
\begin{rail}


420 
('intro'  'elim'  'dest') (()  '!'  '!!')


421 
;


422 
\end{rail}

7135

423 

7321

424 
\begin{descr}


425 
\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,


426 
and destruct rules, respectively. By default, rules are considered as


427 
\emph{safe}, while a single ``!'' classifies as \emph{unsafe}, and ``!!'' as


428 
\emph{extra} (i.e.\ not applied in the searchoriented automatic methods).


429 


430 
\item [Attribute $delrule$] deletes introduction or elimination rules from the


431 
context. Destruction rules would have to be turned into elimination rules


432 
first, e.g.\ by using the $elimify$ attribute.


433 
\end{descr}

7135

434 


435 


436 
%%% Local Variables:


437 
%%% mode: latex


438 
%%% TeXmaster: "isarref"


439 
%%% End:
