7046

1 

7167

2 
\chapter{Isabelle/HOL Tools and Packages}\label{ch:holtools}

7135

3 


4 
\section{Primitive types}


5 

7141

6 
\indexisarcmd{typedecl}\indexisarcmd{typedef}


7 
\begin{matharray}{rcl}


8 
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\


9 
\isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\


10 
\end{matharray}


11 


12 
\begin{rail}


13 
'typedecl' typespec infix? comment?


14 
;


15 
'typedef' parname? typespec infix? \\ '=' term comment?


16 
;


17 
\end{rail}


18 

7167

19 
\begin{descr}

7141

20 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original


21 
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:typespure}), but


22 
also declares type arity $t :: (term, \dots, term) term$, making $t$ an


23 
actual HOL type constructor.


24 
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating


25 
nonemptiness of the set $A$. After finishing the proof, the theory will be

7175

26 
augmented by a Gordon/HOLstyle type definition. See \cite{isabelleHOL}

7335

27 
for more information. Note that userlevel theories usually do not directly


28 
refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced


29 
packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and

7175

30 
$\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).

7167

31 
\end{descr}

7141

32 


33 


34 
\section{Records}\label{sec:record}


35 


36 
%FIXME record_split method


37 
\indexisarcmd{record}


38 
\begin{matharray}{rcl}


39 
\isarcmd{record} & : & \isartrans{theory}{theory} \\


40 
\end{matharray}


41 


42 
\begin{rail}


43 
'record' typespec '=' (type '+')? (field +)


44 
;

7135

45 

7141

46 
field: name '::' type comment?


47 
;


48 
\end{rail}


49 

7167

50 
\begin{descr}

7141

51 
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]


52 
defines extensible record type $(\vec\alpha)t$, derived from the optional


53 
parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.

7335

54 
See \cite{isabelleHOL,NaraschewskiWTPHOLs98} for more information only


55 
simplytyped extensible records.

7167

56 
\end{descr}

7141

57 


58 


59 
\section{Datatypes}\label{sec:datatype}


60 

7167

61 
\indexisarcmd{datatype}\indexisarcmd{repdatatype}

7141

62 
\begin{matharray}{rcl}


63 
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\


64 
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\


65 
\end{matharray}


66 


67 
\railalias{repdatatype}{rep\_datatype}


68 
\railterm{repdatatype}


69 


70 
\begin{rail}

7175

71 
'datatype' (parname? typespec infix? \\ '=' (constructor + '') + 'and')

7141

72 
;


73 
repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs


74 
;


75 

7175

76 
constructor: name (type * ) mixfix? comment?

7141

77 
;


78 
\end{rail}


79 

7167

80 
\begin{descr}

7319

81 
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.


82 
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive


83 
ones, generating the standard infrastructure of derived concepts (primitive


84 
recursion etc.).

7167

85 
\end{descr}

7141

86 

7319

87 
See \cite{isabelleHOL} for more details on datatypes. Note that the theory

7335

88 
syntax above has been slightly simplified over the old version, usually


89 
requiring more quotes and less parentheses.

7319

90 

7135

91 


92 
\section{Recursive functions}


93 

7141

94 
\indexisarcmd{primrec}\indexisarcmd{recdef}


95 
\begin{matharray}{rcl}


96 
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\


97 
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\


98 
%FIXME


99 
% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\


100 
\end{matharray}


101 


102 
\begin{rail}


103 
'primrec' parname? (thmdecl? prop comment? + )


104 
;


105 
'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?


106 
;


107 
\end{rail}


108 

7167

109 
\begin{descr}

7319

110 
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over


111 
datatypes.


112 
\item [$\isarkeyword{recdef}$] defines general wellfounded recursive


113 
functions (using the TFL package).

7167

114 
\end{descr}

7141

115 

7335

116 
See \cite{isabelleHOL} for more information on both mechanisms.

7319

117 

7141

118 

7135

119 
\section{(Co)Inductive sets}


120 

7167

121 
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductivecases}

7141

122 
\begin{matharray}{rcl}


123 
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\


124 
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\


125 
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\


126 
\end{matharray}


127 


128 
\railalias{condefs}{con\_defs}


129 
\railalias{indcases}{inductive\_cases}


130 
\railterm{condefs,indcases}


131 


132 
\begin{rail}


133 
('inductive'  'coinductive') (term comment? +) \\


134 
'intrs' attributes? (thmdecl? prop comment? +) \\


135 
'monos' thmrefs comment? \\ condefs thmrefs comment?


136 
;


137 
indcases thmdef? nameref ':' \\ (prop +) comment?


138 
;


139 
\end{rail}


140 

7167

141 
\begin{descr}

7319

142 
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define


143 
(co)inductive sets from the given introduction rules.


144 
\item [$\isarkeyword{inductive_cases}$] creates simplified instances of


145 
elimination rules of (co)inductive sets.

7167

146 
\end{descr}

7141

147 

7319

148 
See \cite{isabelleHOL} for more information. Note that


149 
$\isarkeyword{inductive_cases}$ corresponds to the ML function


150 
\texttt{mk_cases}.


151 

7141

152 


153 
\section{Proof by induction}


154 

7319

155 
\indexisarmeth{induct}


156 
\begin{matharray}{rcl}


157 
induct & : & \isarmeth \\


158 
\end{matharray}


159 


160 
The $induct$ method provides a uniform interface to induction over datatypes,

7507

161 
inductive sets, recursive functions etc. Basically, it is just an interface

7319

162 
to the $rule$ method applied to appropriate instances of the corresponding


163 
induction rules.


164 


165 
\begin{rail}


166 
'induct' (inst * 'and') kind?


167 
;


168 


169 
inst: term term?


170 
;

7507

171 
kind: ('type'  'set'  'function'  'rule') ':' nameref

7319

172 
;


173 
\end{rail}


174 


175 
\begin{descr}


176 
\item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the

7507

177 
induction rule specified by $kind$ and instantiated by $insts$. The rule is


178 
either that of some type, set, or recursive function (defined via TFL), or


179 
given explicitly.


180 


181 
The instantiation basically consists of a list of $P$ $x$ (induction


182 
predicate and variable) specifications, where $P$ is optional. If $kind$ is

7466

183 
omitted, the default is to pick a datatype induction rule according to the


184 
type of some induction variable, which may not be omitted that case.

7319

185 
\end{descr}

7141

186 

7046

187 

7390

188 
\section{Arithmetic}


189 


190 
\indexisarmeth{arith}


191 
\begin{matharray}{rcl}


192 
arith & : & \isarmeth \\


193 
\end{matharray}


194 


195 
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,


196 
$real$). Note that a simpler (but faster) version of arithmetic reasoning is


197 
already performed by the Simplifier.


198 


199 

7046

200 
%%% Local Variables:


201 
%%% mode: latex


202 
%%% TeXmaster: "isarref"


203 
%%% End:
