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 
fail & : & \isarmeth \\


11 
succeed & : & \isarmeth \\


12 
 & : & \isarmeth \\


13 
assumption & : & \isarmeth \\


14 
finish & : & \isarmeth \\


15 
fold & : & \isarmeth \\


16 
unfold & : & \isarmeth \\


17 
rule & : & \isarmeth \\


18 
erule^* & : & \isarmeth \\


19 
\end{matharray}


20 


21 
\begin{rail}


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


23 
;


24 
\end{rail}


25 


26 
\begin{descr}


27 
\item [$ $]


28 
\end{descr}


29 


30 
FIXME


31 


32 
%FIXME sort


33 
%FIXME thmref (single)


34 
%FIXME var vs. term


35 

7315

36 


37 
\section{Miscellaneous attributes}


38 

7167

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


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


41 
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}


42 
\begin{matharray}{rcl}


43 
tag & : & \isaratt \\


44 
untag & : & \isaratt \\


45 
COMP & : & \isaratt \\


46 
RS & : & \isaratt \\


47 
OF & : & \isaratt \\


48 
where & : & \isaratt \\


49 
of & : & \isaratt \\


50 
standard & : & \isaratt \\


51 
elimify & : & \isaratt \\


52 
transfer & : & \isaratt \\


53 
export & : & \isaratt \\


54 
\end{matharray}


55 


56 
\begin{rail}


57 
('tag'  'untag') (nameref+)


58 
;

7175

59 
\end{rail}


60 


61 
\begin{rail}

7167

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


63 
;


64 
'OF' thmrefs


65 
;

7175

66 
\end{rail}


67 


68 
\begin{rail}


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

7167

70 
;

7175

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

7167

72 
;


73 


74 
inst: underscore  term


75 
;


76 
\end{rail}


77 


78 
\begin{descr}


79 
\item [$ $]


80 
\end{descr}


81 


82 
FIXME

7135

83 

7315

84 


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


86 


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


88 
\begin{matharray}{rcl}


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


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


91 
trans & : & \isaratt \\


92 
\end{matharray}


93 


94 
Calculational proof is forward reasoning with implicit application of


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


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


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


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


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


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


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


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


103 


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


105 
application with calculational proofs. It automatically refers to the


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


107 
side.} of the preceding statement.


108 


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


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


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


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


113 
command required.


114 


115 
\begin{rail}


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


117 
;


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


119 
;


120 


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


122 
;


123 
\end{rail}


124 


125 
\begin{descr}


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


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


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


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


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


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


132 
$thms$ (the latter have precedence).


133 


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


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


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


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


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


139 


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


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


142 
arguments. The default is adding of rules.


143 
\end{descr}


144 


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


146 
calculations for basic equational reasoning.


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


148 
calculational steps in combination with natural deduction.


149 


150 

7135

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


152 


153 
\indexisarcmd{axclass}\indexisarcmd{instance}


154 
\begin{matharray}{rcl}


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


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


157 
\end{matharray}


158 


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


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


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


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


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


164 
the standard Isabelle documentation.


165 


166 
\begin{rail}


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


168 
;


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


170 
;


171 
\end{rail}


172 

7167

173 
\begin{descr}

7135

174 
\item [$\isarkeyword{axclass}~$] FIXME


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


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


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

7141

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


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

7135

180 
corresponding to the resulting theorem.

7167

181 
\end{descr}

7135

182 


183 


184 


185 
\section{The Simplifier}


186 

7315

187 
\subsection{Simplification methods}


188 


189 
\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}


190 
\begin{matharray}{rcl}


191 
simp & : & \isarmeth \\


192 
asm_simp & : & \isarmeth \\


193 
simp & : & \isaratt \\


194 
\end{matharray}


195 


196 
\begin{rail}


197 
'simp' (simpmod+)?


198 
;


199 


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


201 
;


202 
\end{rail}


203 


204 


205 
\subsection{Forward simplification}


206 


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


208 
\begin{matharray}{rcl}


209 
simplify & : & \isaratt \\


210 
asm_simplify & : & \isaratt \\


211 
full_simplify & : & \isaratt \\


212 
asm_full_simplify & : & \isaratt \\


213 
\end{matharray}


214 


215 
FIXME


216 


217 

7135

218 
\section{The Classical Reasoner}


219 

7315

220 
\subsection{Single step methods}


221 


222 
\subsection{Automatic methods}


223 


224 
\subsection{Combined automatic methods}


225 


226 
\subsection{Modifying the context}


227 


228 

7135

229 


230 
%\indexisarcmd{}


231 
%\begin{matharray}{rcl}


232 
% \isarcmd{} & : & \isartrans{}{} \\


233 
%\end{matharray}


234 


235 
%\begin{rail}


236 


237 
%\end{rail}


238 

7167

239 
%\begin{descr}

7135

240 
%\item [$ $]

7167

241 
%\end{descr}

7135

242 


243 


244 
%%% Local Variables:


245 
%%% mode: latex


246 
%%% TeXmaster: "isarref"


247 
%%% End:
