26840

1 
%


2 
\begin{isabellebody}%


3 
\def\isabellecontext{HOL{\isacharunderscore}Specific}%


4 
%


5 
\isadelimtheory


6 
\isanewline


7 
\isanewline


8 
%


9 
\endisadelimtheory


10 
%


11 
\isatagtheory


12 
\isacommand{theory}\isamarkupfalse%


13 
\ HOL{\isacharunderscore}Specific\isanewline

26849

14 
\isakeyword{imports}\ Main\isanewline


15 
\isakeyword{begin}%


16 
\endisatagtheory


17 
{\isafoldtheory}%


18 
%


19 
\isadelimtheory


20 
%


21 
\endisadelimtheory


22 
%

26852

23 
\isamarkupchapter{Isabelle/HOL \label{ch:hol}%

26849

24 
}


25 
\isamarkuptrue%


26 
%


27 
\isamarkupsection{Primitive types \label{sec:holtypedef}%


28 
}


29 
\isamarkuptrue%


30 
%


31 
\begin{isamarkuptext}%


32 
\begin{matharray}{rcl}

26902

33 
\indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\


34 
\indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isartrans{theory}{proof(prove)} \\

26849

35 
\end{matharray}


36 


37 
\begin{rail}


38 
'typedecl' typespec infix?


39 
;


40 
'typedef' altname? abstype '=' repset


41 
;


42 


43 
altname: '(' (name  'open'  'open' name) ')'


44 
;


45 
abstype: typespec infix?


46 
;


47 
repset: term ('morphisms' name name)?


48 
;


49 
\end{rail}


50 


51 
\begin{descr}


52 

26902

53 
\item [\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of

26849

54 
Isabelle/Pure (see \secref{sec:typespure}), but also declares type


55 
arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an


56 
actual HOL type constructor. %FIXME check, update


57 

26902

58 
\item [\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}] sets up a goal stating nonemptiness of the set \isa{A}.

26849

59 
After finishing the proof, the theory will be augmented by a


60 
Gordon/HOLstyle type definition, which establishes a bijection


61 
between the representing set \isa{A} and the new type \isa{t}.


62 

26902

63 
Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base

26849

64 
name may be given in parentheses). The injection from type to set


65 
is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be

26902

66 
changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).

26849

67 


68 
Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a


69 
corresponding injection/surjection pair (in both directions). Rules


70 
\isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly


71 
more convenient view on the injectivity part, suitable for automated

26902

72 
proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}

26895

73 
declarations). Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and


74 
\isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views


75 
on surjectivity; these are already declared as set or type rules for

26902

76 
the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.

26849

77 


78 
An alternative name may be specified in parentheses; the default is


79 
to use \isa{t} as indicated before. The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''


80 
declaration suppresses a separate constant definition for the


81 
representing set.


82 


83 
\end{descr}


84 


85 
Note that raw type declarations are rarely used in practice; the


86 
main application is with experimental (or even axiomatic!) theory


87 
fragments. Instead of primitive HOL type definitions, userlevel

26902

88 
theories usually refer to higherlevel packages such as \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}} (see \secref{sec:holrecord}) or \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} (see \secref{sec:holdatatype}).%

26849

89 
\end{isamarkuptext}%


90 
\isamarkuptrue%


91 
%


92 
\isamarkupsection{Adhoc tuples%


93 
}


94 
\isamarkuptrue%


95 
%


96 
\begin{isamarkuptext}%


97 
\begin{matharray}{rcl}

26907

98 
\hyperlink{attribute.HOL.splitformat}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\

26849

99 
\end{matharray}


100 


101 
\begin{rail}


102 
'split\_format' (((name *) + 'and')  ('(' 'complete' ')'))


103 
;


104 
\end{rail}


105 


106 
\begin{descr}


107 

26907

108 
\item [\hyperlink{attribute.HOL.splitformat}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of

26849

109 
lowlevel tuple types into canonical form as specified by the


110 
arguments given; the \isa{i}th collection of arguments refers to


111 
occurrences in premise \isa{i} of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function


112 
applications to be represented canonically according to their tuple


113 
type structure.


114 


115 
Note that these operations tend to invent funny names for new local


116 
parameters to be introduced.


117 


118 
\end{descr}%


119 
\end{isamarkuptext}%


120 
\isamarkuptrue%


121 
%


122 
\isamarkupsection{Records \label{sec:holrecord}%


123 
}


124 
\isamarkuptrue%


125 
%


126 
\begin{isamarkuptext}%


127 
In principle, records merely generalize the concept of tuples, where


128 
components may be addressed by labels instead of just position. The


129 
logical infrastructure of records in Isabelle/HOL is slightly more


130 
advanced, though, supporting truly extensible record schemes. This


131 
admits operations that are polymorphic with respect to record


132 
extension, yielding ``objectoriented'' effects like (single)


133 
inheritance. See also \cite{NaraschewskiWTPHOLs98} for more


134 
details on objectoriented verification and record subtyping in HOL.%


135 
\end{isamarkuptext}%


136 
\isamarkuptrue%


137 
%


138 
\isamarkupsubsection{Basic concepts%


139 
}


140 
\isamarkuptrue%


141 
%


142 
\begin{isamarkuptext}%


143 
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records


144 
at the level of terms and types. The notation is as follows:


145 


146 
\begin{center}


147 
\begin{tabular}{lll}


148 
& record terms & record types \\ \hline


149 
fixed & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}} \\


150 
schematic & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} &


151 
\isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ M{\isasymrparr}{\isachardoublequote}} \\


152 
\end{tabular}


153 
\end{center}


154 


155 
\noindent The ASCII representation of \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} is \isa{{\isachardoublequote}{\isacharparenleft}{\isacharbar}\ x\ {\isacharequal}\ a\ {\isacharbar}{\isacharparenright}{\isachardoublequote}}.


156 


157 
A fixed record \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} has field \isa{x} of value


158 
\isa{a} and field \isa{y} of value \isa{b}. The corresponding


159 
type is \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}}, assuming that \isa{{\isachardoublequote}a\ {\isacharcolon}{\isacharcolon}\ A{\isachardoublequote}}


160 
and \isa{{\isachardoublequote}b\ {\isacharcolon}{\isacharcolon}\ B{\isachardoublequote}}.


161 


162 
A record scheme like \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} contains fields


163 
\isa{x} and \isa{y} as before, but also possibly further fields


164 
as indicated by the ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' notation (which is actually part


165 
of the syntax). The improper field ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' of a record


166 
scheme is called the \emph{more part}. Logically it is just a free


167 
variable, which is occasionally referred to as ``row variable'' in


168 
the literature. The more part of a record scheme may be


169 
instantiated by zero or more further components. For example, the

26852

170 
previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isasymrparr}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.

26849

171 
Fixed records are special instances of record schemes, where


172 
``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}


173 
element. In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation


174 
for \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}{\isachardoublequote}}.


175 


176 
\medskip Two key observations make extensible records in a simply


177 
typed language like HOL work out:


178 


179 
\begin{enumerate}


180 


181 
\item the more part is internalized, as a free term or type


182 
variable,


183 

26852

184 
\item field names are externalized, they cannot be accessed within


185 
the logic as firstclass values.

26849

186 


187 
\end{enumerate}


188 


189 
\medskip In Isabelle/HOL record types have to be defined explicitly,


190 
fixing their field names and types, and their (optional) parent


191 
record. Afterwards, records may be formed using above syntax, while


192 
obeying the canonical order of fields as given by their declaration.


193 
The record package provides several standard operations like


194 
selectors and updates. The common setup for various generic proof


195 
tools enable succinct reasoning patterns. See also the Isabelle/HOL


196 
tutorial \cite{isabelleholbook} for further instructions on using


197 
records in practice.%


198 
\end{isamarkuptext}%


199 
\isamarkuptrue%


200 
%


201 
\isamarkupsubsection{Record specifications%


202 
}


203 
\isamarkuptrue%


204 
%


205 
\begin{isamarkuptext}%


206 
\begin{matharray}{rcl}

26902

207 
\indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isartrans{theory}{theory} \\

26849

208 
\end{matharray}


209 


210 
\begin{rail}


211 
'record' typespec '=' (type '+')? (constdecl +)


212 
;


213 
\end{rail}


214 


215 
\begin{descr}


216 

26902

217 
\item [\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}] defines

26849

218 
extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},


219 
derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new


220 
field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc.


221 


222 
The type variables of \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i{\isachardoublequote}} need to be


223 
covered by the (distinct) parameters \isa{{\isachardoublequote}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isachardoublequote}}. Type constructor \isa{t} has to be new, while \isa{{\isasymtau}} needs to specify an instance of an existing record type. At


224 
least one new field \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} has to be specified.


225 
Basically, field names need to belong to a unique record. This is


226 
not a real restriction in practice, since fields are qualified by


227 
the record name internally.


228 


229 
The parent record specification \isa{{\isasymtau}} is optional; if omitted


230 
\isa{t} becomes a root record. The hierarchy of all records


231 
declared within a theory context forms a forest structure, i.e.\ a


232 
set of trees starting with a root record each. There is no way to


233 
merge multiple parent records!


234 


235 
For convenience, \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is made a


236 
type abbreviation for the fixed record type \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}}, likewise is \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharcomma}\ {\isasymzeta}{\isacharparenright}\ t{\isacharunderscore}scheme{\isachardoublequote}} made an abbreviation for


237 
\isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}}.


238 


239 
\end{descr}%


240 
\end{isamarkuptext}%


241 
\isamarkuptrue%


242 
%


243 
\isamarkupsubsection{Record operations%


244 
}


245 
\isamarkuptrue%


246 
%


247 
\begin{isamarkuptext}%


248 
Any record definition of the form presented above produces certain


249 
standard operations. Selectors and updates are provided for any


250 
field, including the improper one ``\isa{more}''. There are also


251 
cumulative record constructor functions. To simplify the


252 
presentation below, we assume for now that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is a root record with fields \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}.


253 


254 
\medskip \textbf{Selectors} and \textbf{updates} are available for


255 
any field (including ``\isa{more}''):


256 


257 
\begin{matharray}{lll}

26852

258 
\isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\


259 
\isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\

26849

260 
\end{matharray}


261 


262 
There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}. Further notation for


263 
repeated updates is also available: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}y\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}{\isasymlparr}z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}} may be written \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}. Note that


264 
because of postfix notation the order of fields shown here is


265 
reverse than in the actual term. Since repeated updates are just


266 
function applications, fields may be freely permuted in \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}, as far as logical equality is concerned.


267 
Thus commutativity of independent updates can be proven within the


268 
logic for any two fields, but not as a general theorem.


269 


270 
\medskip The \textbf{make} operation provides a cumulative record


271 
constructor function:


272 


273 
\begin{matharray}{lll}

26852

274 
\isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\

26849

275 
\end{matharray}


276 


277 
\medskip We now reconsider the case of nonroot records, which are


278 
derived of some parent. In general, the latter may depend on


279 
another parent as well, resulting in a list of \emph{ancestor


280 
records}. Appending the lists of fields of all ancestors results in


281 
a certain field prefix. The record package automatically takes care


282 
of this by lifting operations over this context of ancestor fields.


283 
Assuming that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} has ancestor


284 
fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}},


285 
the above record operations will get the following types:


286 

26852

287 
\medskip


288 
\begin{tabular}{lll}


289 
\isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\


290 
\isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\


291 
\isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\


292 
\end{tabular}


293 
\medskip

26849

294 

26852

295 
\noindent Some further operations address the extension aspect of a

26849

296 
derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a


297 
record fragment consisting of exactly the new fields introduced here


298 
(the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}


299 
takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.


300 

26852

301 
\medskip


302 
\begin{tabular}{lll}


303 
\isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\


304 
\isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\


305 
\isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\


306 
\end{tabular}


307 
\medskip

26849

308 


309 
\noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide


310 
for root records.%


311 
\end{isamarkuptext}%


312 
\isamarkuptrue%


313 
%


314 
\isamarkupsubsection{Derived rules and proof tools%


315 
}


316 
\isamarkuptrue%


317 
%


318 
\begin{isamarkuptext}%


319 
The record package proves several results internally, declaring


320 
these facts to appropriate proof tools. This enables users to


321 
reason about record structures quite conveniently. Assume that


322 
\isa{t} is a record type as specified above.


323 


324 
\begin{enumerate}


325 


326 
\item Standard conversions for selectors or updates applied to


327 
record constructor terms are made part of the default Simplifier


328 
context; thus proofs by reduction of basic operations merely require

26902

329 
the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules

26849

330 
are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, too.


331 


332 
\item Selectors applied to updated records are automatically reduced


333 
by an internal simplification procedure, which is also part of the


334 
standard Simplifier setup.


335 


336 
\item Inject equations of a form analogous to \isa{{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}\ {\isasymequiv}\ x\ {\isacharequal}\ x{\isacharprime}\ {\isasymand}\ y\ {\isacharequal}\ y{\isacharprime}{\isachardoublequote}} are declared to the Simplifier and Classical

26902

337 
Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules. These rules are available as

26849

338 
\isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}.


339 


340 
\item The introduction rule for record equality analogous to \isa{{\isachardoublequote}x\ r\ {\isacharequal}\ x\ r{\isacharprime}\ {\isasymLongrightarrow}\ y\ r\ {\isacharequal}\ y\ r{\isacharprime}\ {\isasymdots}\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ r{\isacharprime}{\isachardoublequote}} is declared to the Simplifier,

26902

341 
and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''.

26849

342 
The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}.


343 


344 
\item Representations of arbitrary record expressions as canonical

26902

345 
constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,

26849

346 
\secref{sec:casesinduct}). Several variations are available, for


347 
fixed records, record schemes, more parts etc.


348 


349 
The generic proof methods are sufficiently smart to pick the most


350 
sensible rule according to the type of the indicated record


351 
expression: users just need to apply something like ``\isa{{\isachardoublequote}{\isacharparenleft}cases\ r{\isacharparenright}{\isachardoublequote}}'' to a certain proof problem.


352 


353 
\item The derived record operations \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} are \emph{not}


354 
treated automatically, but usually need to be expanded by hand,


355 
using the collective fact \isa{{\isachardoublequote}t{\isachardot}defs{\isachardoublequote}}.


356 


357 
\end{enumerate}%


358 
\end{isamarkuptext}%


359 
\isamarkuptrue%


360 
%


361 
\isamarkupsection{Datatypes \label{sec:holdatatype}%


362 
}


363 
\isamarkuptrue%


364 
%


365 
\begin{isamarkuptext}%


366 
\begin{matharray}{rcl}

26902

367 
\indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\

27452

368 
\indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.repdatatype}{\hyperlink{command.HOL.repdatatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\

26849

369 
\end{matharray}


370 


371 
\begin{rail}


372 
'datatype' (dtspec + 'and')


373 
;

27452

374 
'rep\_datatype' ('(' (name +) ')')? (term +)

26849

375 
;


376 


377 
dtspec: parname? typespec infix? '=' (cons + '')


378 
;


379 
cons: name (type *) mixfix?


380 
\end{rail}


381 


382 
\begin{descr}


383 

26902

384 
\item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in

26849

385 
HOL.


386 

26907

387 
\item [\hyperlink{command.HOL.repdatatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as

26849

388 
inductive ones, generating the standard infrastructure of derived


389 
concepts (primitive recursion etc.).


390 


391 
\end{descr}


392 


393 
The induction and exhaustion theorems generated provide case names


394 
according to the constructors involved, while parameters are named


395 
after the types (see also \secref{sec:casesinduct}).


396 


397 
See \cite{isabelleHOL} for more details on datatypes, but beware of


398 
the oldstyle theory syntax being used there! Apart from proper


399 
proof methods for caseanalysis and induction, there are also

26907

400 
emulations of ML tactics \hyperlink{method.HOL.casetac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.inducttac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:holinducttac}; these admit

26849

401 
to refer directly to the internal structure of subgoals (including


402 
internally bound parameters).%


403 
\end{isamarkuptext}%


404 
\isamarkuptrue%


405 
%


406 
\isamarkupsection{Recursive functions \label{sec:recursion}%


407 
}


408 
\isamarkuptrue%


409 
%


410 
\begin{isamarkuptext}%


411 
\begin{matharray}{rcl}

26902

412 
\indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isarkeep{local{\dsh}theory} \\


413 
\indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isarkeep{local{\dsh}theory} \\


414 
\indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\


415 
\indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

26849

416 
\end{matharray}


417 


418 
\begin{rail}


419 
'primrec' target? fixes 'where' equations


420 
;


421 
equations: (thmdecl? prop + '')


422 
;

26987

423 
('fun'  'function') target? functionopts? fixes 'where' clauses

26849

424 
;


425 
clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '')


426 
;

26987

427 
functionopts: '(' (('sequential'  'domintros'  'tailrec'  'default' term) + ',') ')'

26849

428 
;


429 
'termination' ( term )?


430 
\end{rail}


431 


432 
\begin{descr}


433 

26902

434 
\item [\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}] defines primitive recursive

26849

435 
functions over datatypes, see also \cite{isabelleHOL}.


436 

26902

437 
\item [\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}] defines functions by general

26849

438 
wellfounded recursion. A detailed description with examples can be


439 
found in \cite{isabellefunction}. The function is specified by a


440 
set of (possibly conditional) recursive equations with arbitrary


441 
pattern matching. The command generates proof obligations for the


442 
completeness and the compatibility of patterns.


443 


444 
The defined function is considered partial, and the resulting


445 
simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule


446 
(named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain

26902

447 
predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}

26849

448 
command can then be used to establish that the function is total.


449 

26902

450 
\item [\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}] is a shorthand notation for


451 
``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by

26849

452 
automated proof attempts regarding pattern matching and termination.


453 
See \cite{isabellefunction} for further details.


454 

26902

455 
\item [\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f}] commences a

26849

456 
termination proof for the previously defined function \isa{f}. If


457 
this is omitted, the command refers to the most recent function


458 
definition. After the proof is closed, the recursive equations and


459 
the induction principle is established.


460 


461 
\end{descr}


462 


463 
%FIXME check


464 

27452

465 
Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}


466 
command accommodate

26849

467 
reasoning by induction (cf.\ \secref{sec:casesinduct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)


468 
refers to a specific induction rule, with parameters named according

27452

469 
to the userspecified equations.


470 
For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides


471 
with structural recursion on the datatype the recursion is carried


472 
out.


473 
Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of

26902

474 
\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).

26849

475 


476 
The equations provided by these packages may be referred later as


477 
theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)


478 
name of the functions defined. Individual equations may be named


479 
explicitly as well.


480 

26902

481 
The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following

26849

482 
options.


483 


484 
\begin{descr}


485 


486 
\item [\isa{sequential}] enables a preprocessor which


487 
disambiguates overlapping patterns by making them mutually disjoint.


488 
Earlier equations take precedence over later ones. This allows to


489 
give the specification in a format very similar to functional


490 
programming. Note that the resulting simplification and induction


491 
rules correspond to the transformed specification, not the one given


492 
originally. This usually means that each equation given by the user


493 
may result in several theroems. Also note that this automatic


494 
transformation only works for MLstyle datatype patterns.


495 


496 
\item [\isa{domintros}] enables the automated generation of


497 
introduction rules for the domain predicate. While mostly not


498 
needed, they can be helpful in some proofs about partial functions.


499 


500 
\item [\isa{tailrec}] generates the unconstrained recursive


501 
equations even without a termination proof, provided that the


502 
function is tailrecursive. This currently only works


503 


504 
\item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a


505 
(partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}


506 
whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.


507 


508 
\end{descr}%


509 
\end{isamarkuptext}%


510 
\isamarkuptrue%


511 
%


512 
\isamarkupsubsection{Proof methods related to recursive definitions%


513 
}


514 
\isamarkuptrue%


515 
%


516 
\begin{isamarkuptext}%


517 
\begin{matharray}{rcl}

26907

518 
\indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.patcompleteness}{\hyperlink{method.HOL.patcompleteness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\

26902

519 
\indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\

26907

520 
\indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographicorder}{\hyperlink{method.HOL.lexicographicorder}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\

26849

521 
\end{matharray}


522 


523 
\begin{rail}


524 
'relation' term


525 
;


526 
'lexicographic\_order' (clasimpmod *)


527 
;


528 
\end{rail}


529 


530 
\begin{descr}


531 

26907

532 
\item [\hyperlink{method.HOL.patcompleteness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to

26849

533 
solve goals regarding the completeness of pattern matching, as

26902

534 
required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\

26849

535 
\cite{isabellefunction}).


536 

26902

537 
\item [\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R}] introduces a termination

26849

538 
proof using the relation \isa{R}. The resulting proof state will


539 
contain goals expressing that \isa{R} is wellfounded, and that the


540 
arguments of recursive calls decrease with respect to \isa{R}.


541 
Usually, this method is used as the initial proof step of manual


542 
termination proofs.


543 

26907

544 
\item [\hyperlink{method.HOL.lexicographicorder}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully

26849

545 
automated termination proof by searching for a lexicographic


546 
combination of size measures on the arguments of the function. The

26902

547 
method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,

26849

548 
which it uses internally to prove local descents. The same context

26902

549 
modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see

26849

550 
\secref{sec:clasimp}.


551 


552 
In case of failure, extensive information is printed, which can help


553 
to analyse the situation (cf.\ \cite{isabellefunction}).


554 


555 
\end{descr}%


556 
\end{isamarkuptext}%


557 
\isamarkuptrue%


558 
%


559 
\isamarkupsubsection{Oldstyle recursive function definitions (TFL)%


560 
}


561 
\isamarkuptrue%


562 
%


563 
\begin{isamarkuptext}%

26907

564 
The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdeftc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.

26849

565 


566 
\begin{matharray}{rcl}

26902

567 
\indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\

26907

568 
\indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdeftc}{\hyperlink{command.HOL.recdeftc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\

26849

569 
\end{matharray}


570 


571 
\begin{rail}


572 
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?


573 
;


574 
recdeftc thmdecl? tc


575 
;


576 
hints: '(' 'hints' (recdefmod *) ')'


577 
;


578 
recdefmod: (('recdef\_simp'  'recdef\_cong'  'recdef\_wf') (()  'add'  'del') ':' thmrefs)  clasimpmod


579 
;


580 
tc: nameref ('(' nat ')')?


581 
;


582 
\end{rail}


583 


584 
\begin{descr}


585 

26902

586 
\item [\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}] defines general wellfounded

26849

587 
recursive functions (using the TFL package), see also


588 
\cite{isabelleHOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells


589 
TFL to recover from failed proof attempts, returning unfinished


590 
results. The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal

26902

591 
automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}

26849

592 
declarations (cf.\ \secref{sec:clasimp}) may be given to tune the


593 
context of the Simplifier (cf.\ \secref{sec:simplifier}) and


594 
Classical reasoner (cf.\ \secref{sec:classical}).


595 

26907

596 
\item [\hyperlink{command.HOL.recdeftc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the

26849

597 
proof for leftover termination condition number \isa{i} (default

26902

598 
1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of

26849

599 
constant \isa{c}.


600 

26902

601 
Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish

26849

602 
its internal proofs without manual intervention.


603 


604 
\end{descr}


605 

26902

606 
\medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared

26849

607 
globally, using the following attributes.


608 


609 
\begin{matharray}{rcl}

26907

610 
\indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdefsimp}{\hyperlink{attribute.HOL.recdefsimp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\


611 
\indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdefcong}{\hyperlink{attribute.HOL.recdefcong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\


612 
\indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdefwf}{\hyperlink{attribute.HOL.recdefwf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\

26849

613 
\end{matharray}


614 


615 
\begin{rail}


616 
('recdef\_simp'  'recdef\_cong'  'recdef\_wf') (()  'add'  'del')


617 
;


618 
\end{rail}%


619 
\end{isamarkuptext}%


620 
\isamarkuptrue%


621 
%


622 
\isamarkupsection{Inductive and coinductive definitions \label{sec:holinductive}%


623 
}


624 
\isamarkuptrue%


625 
%


626 
\begin{isamarkuptext}%


627 
An \textbf{inductive definition} specifies the least predicate (or


628 
set) \isa{R} closed under given rules: applying a rule to elements


629 
of \isa{R} yields a result within \isa{R}. For example, a


630 
structural operational semantics is an inductive definition of an


631 
evaluation relation.


632 


633 
Dually, a \textbf{coinductive definition} specifies the greatest


634 
predicate~/ set \isa{R} that is consistent with given rules: every


635 
element of \isa{R} can be seen as arising by applying a rule to


636 
elements of \isa{R}. An important example is using bisimulation


637 
relations to formalise equivalence of processes and infinite data


638 
structures.


639 


640 
\medskip The HOL package is related to the ZF one, which is


641 
described in a separate paper,\footnote{It appeared in CADE


642 
\cite{paulsonCADE}; a longer version is distributed with Isabelle.}


643 
which you should refer to in case of difficulties. The package is


644 
simpler than that of ZF thanks to implicit typechecking in HOL.


645 
The types of the (co)inductive predicates (or sets) determine the


646 
domain of the fixedpoint definition, and the package does not have


647 
to use inference rules for typechecking.


648 


649 
\begin{matharray}{rcl}

26902

650 
\indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\

26907

651 
\indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductiveset}{\hyperlink{command.HOL.inductiveset}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\

26902

652 
\indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\

26907

653 
\indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductiveset}{\hyperlink{command.HOL.coinductiveset}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\

26902

654 
\indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\

26849

655 
\end{matharray}


656 


657 
\begin{rail}


658 
('inductive'  'inductive\_set'  'coinductive'  'coinductive\_set') target? fixes ('for' fixes)? \\


659 
('where' clauses)? ('monos' thmrefs)?


660 
;


661 
clauses: (thmdecl? prop + '')


662 
;


663 
'mono' (()  'add'  'del')


664 
;


665 
\end{rail}


666 


667 
\begin{descr}


668 

26902

669 
\item [\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}] define (co)inductive predicates from the


670 
introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The


671 
optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the

26849

672 
(co)inductive predicates that remain fixed throughout the

26902

673 
definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains

26849

674 
\emph{monotonicity theorems}, which are required for each operator


675 
applied to a recursive set in the introduction rules. There


676 
\emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},


677 
for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!


678 

26907

679 
\item [\hyperlink{command.HOL.inductiveset}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductiveset}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}] are wrappers for to the previous commands,

26849

680 
allowing the definition of (co)inductive sets.


681 

26902

682 
\item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules. These


683 
rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.

26849

684 


685 
\end{descr}%


686 
\end{isamarkuptext}%


687 
\isamarkuptrue%


688 
%


689 
\isamarkupsubsection{Derived rules%


690 
}


691 
\isamarkuptrue%


692 
%


693 
\begin{isamarkuptext}%


694 
Each (co)inductive definition \isa{R} adds definitions to the


695 
theory and also proves some theorems:


696 


697 
\begin{description}


698 


699 
\item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven


700 
theorems, for the recursive predicates (or sets). The rules are


701 
also available individually, using the names given them in the


702 
theory file;


703 


704 
\item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule;


705 


706 
\item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction


707 
rule.


708 


709 
\end{description}


710 


711 
When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are


712 
defined simultaneously, the list of introduction rules is called


713 
\isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are


714 
called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list


715 
of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%


716 
\end{isamarkuptext}%


717 
\isamarkuptrue%


718 
%


719 
\isamarkupsubsection{Monotonicity theorems%


720 
}


721 
\isamarkuptrue%


722 
%


723 
\begin{isamarkuptext}%


724 
Each theory contains a default set of theorems that are used in


725 
monotonicity proofs. New rules can be added to this set via the

26902

726 
\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}

26849

727 
shows how this is done. In general, the following monotonicity


728 
theorems may be added:


729 


730 
\begin{itemize}


731 


732 
\item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving


733 
monotonicity of inductive definitions whose introduction rules have


734 
premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.


735 


736 
\item Monotonicity theorems for logical operators, which are of the


737 
general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}. For example, in


738 
the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is


739 
\[


740 
\infer{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymor}\ P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}\ {\isasymor}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}


741 
\]


742 


743 
\item De Morgan style equations for reasoning about the ``polarity''


744 
of expressions, e.g.


745 
\[


746 
\isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad


747 
\isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}


748 
\]


749 


750 
\item Equations for reducing complex operators to more primitive


751 
ones whose monotonicity can easily be proved, e.g.


752 
\[


753 
\isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad


754 
\isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}


755 
\]


756 


757 
\end{itemize}


758 


759 
%FIXME: Example of an inductive definition%


760 
\end{isamarkuptext}%


761 
\isamarkuptrue%


762 
%


763 
\isamarkupsection{Arithmetic proof support%


764 
}


765 
\isamarkuptrue%


766 
%


767 
\begin{isamarkuptext}%


768 
\begin{matharray}{rcl}

26902

769 
\indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\

26907

770 
\indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arithsplit}{\hyperlink{attribute.HOL.arithsplit}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\

26849

771 
\end{matharray}


772 

26902

773 
The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems

26849

774 
(on types \isa{nat}, \isa{int}, \isa{real}). Any current


775 
facts are inserted into the goal before running the procedure.


776 

26907

777 
The \hyperlink{attribute.HOL.arithsplit}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split

26895

778 
rules to be expanded before the arithmetic procedure is invoked.

26849

779 


780 
Note that a simpler (but faster) version of arithmetic reasoning is


781 
already performed by the Simplifier.%


782 
\end{isamarkuptext}%


783 
\isamarkuptrue%


784 
%

28603

785 
\isamarkupsection{Invoking automated reasoning tools  The Sledgehammer%


786 
}


787 
\isamarkuptrue%


788 
%


789 
\begin{isamarkuptext}%


790 
Isabelle/HOL includes a generic \emph{ATP manager} that allows


791 
external automated reasoning tools to crunch a pending goal.


792 
Supported provers include E\footnote{\url{http://www.eprover.org}},


793 
SPASS\footnote{\url{http://www.spassprover.org/}}, and Vampire.


794 
There is also a wrapper to invoke provers remotely via the


795 
SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgibin/SystemOnTPTP}}


796 
web service.


797 


798 
The problem passed to external provers consists of the goal together


799 
with a smart selection of lemmas from the current theory context.


800 
The result of a successful proof search is some source text that


801 
usually reconstructs the proof within Isabelle, without requiring


802 
external provers again. The Metis


803 
prover\footnote{\url{http://www.gilith.com/software/metis/}} that is


804 
integrated into Isabelle/HOL is being used here.


805 


806 
In this mode of operation, heavy means of automated reasoning are


807 
used as a strong relevance filter, while the main proof checking


808 
works via explicit inferences going through the Isabelle kernel.


809 
Moreover, rechecking Isabelle proof texts with already specified


810 
auxiliary facts is much faster than performing fully automated


811 
search over and over again.


812 


813 
\begin{matharray}{rcl}


814 
\indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\


815 
\indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.printatps}{\hyperlink{command.HOL.printatps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\


816 
\indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atpinfo}{\hyperlink{command.HOL.atpinfo}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\


817 
\indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atpkill}{\hyperlink{command.HOL.atpkill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\


818 
\indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\


819 
\end{matharray}


820 


821 
\begin{rail}


822 
'sledgehammer' (nameref *)


823 
;


824 


825 
'metis' thmrefs


826 
;


827 
\end{rail}


828 


829 
\begin{descr}


830 


831 
\item [\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}] invokes the specified automated theorem provers on


832 
the first subgoal. Provers are run in parallel, the first


833 
successful result is displayed, and the other attempts are


834 
terminated.


835 


836 
Provers are defined in the theory context, see also \hyperlink{command.HOL.printatps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as


837 
``ATP provers'' preference by the user interface.


838 


839 
There are additional preferences for timeout (default: 60 seconds),


840 
and the maximum number of independent prover processes (default: 5);


841 
excessive provers are automatically terminated.


842 


843 
\item [\hyperlink{command.HOL.printatps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated


844 
theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}


845 
command.


846 


847 
\item [\hyperlink{command.HOL.atpinfo}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently


848 
running provers, including elapsed runtime, and the remaining time


849 
until timeout.


850 


851 
\item [\hyperlink{command.HOL.atpkill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running


852 
provers.


853 


854 
\item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis


855 
prover with the given facts. Metis is an automated proof tool of


856 
medium strength, but is fully integrated into Isabelle/HOL, with


857 
explicit inferences going through the kernel. Thus its results are


858 
guaranteed to be ``correct by construction''.


859 


860 
Note that all facts used with Metis need to be specified as explicit


861 
arguments. There are no rule declarations as for other Isabelle


862 
provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.


863 


864 
\end{descr}%


865 
\end{isamarkuptext}%


866 
\isamarkuptrue%


867 
%

27124

868 
\isamarkupsection{Unstructured cases analysis and induction \label{sec:holinducttac}%

26849

869 
}


870 
\isamarkuptrue%


871 
%


872 
\begin{isamarkuptext}%

27124

873 
The following tools of Isabelle/HOL support cases analysis and


874 
induction in unstructured tactic scripts; see also


875 
\secref{sec:casesinduct} for proper Isar versions of similar ideas.

26849

876 


877 
\begin{matharray}{rcl}

26907

878 
\indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.casetac}{\hyperlink{method.HOL.casetac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\


879 
\indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.inducttac}{\hyperlink{method.HOL.inducttac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\


880 
\indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.indcases}{\hyperlink{method.HOL.indcases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\

27124

881 
\indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductivecases}{\hyperlink{command.HOL.inductivecases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{theory} \\

26849

882 
\end{matharray}


883 


884 
\begin{rail}


885 
'case\_tac' goalspec? term rule?


886 
;


887 
'induct\_tac' goalspec? (insts * 'and') rule?


888 
;


889 
'ind\_cases' (prop +) ('for' (name +)) ?


890 
;


891 
'inductive\_cases' (thmdecl? (prop +) + 'and')


892 
;


893 


894 
rule: ('rule' ':' thmref)


895 
;


896 
\end{rail}


897 


898 
\begin{descr}


899 

26907

900 
\item [\hyperlink{method.HOL.casetac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.inducttac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]

27124

901 
admit to reason about inductive types. Rules are selected according


902 
to the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} attributes, cf.\ \secref{sec:casesinduct}. The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.


903 


904 
These unstructured tactics feature both goal addressing and dynamic

26849

905 
instantiation. Note that named rule cases are \emph{not} provided

27124

906 
as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof


907 
methods (see \secref{sec:casesinduct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.inducttac}{\mbox{\isa{induct{\isacharunderscore}tac}}} does not handle structured rule


908 
statements, only the compact objectlogic conclusion of the subgoal


909 
being addressed.

26849

910 

26907

911 
\item [\hyperlink{method.HOL.indcases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductivecases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verbmk_cases operation. Rules are simplified in an unrestricted

26861

912 
forward manner.

26849

913 

26907

914 
While \hyperlink{method.HOL.indcases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the


915 
result immediately as elimination rules, \hyperlink{command.HOL.inductivecases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level


916 
for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.indcases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should

26849

917 
be generalized before applying the resulting rule.


918 


919 
\end{descr}%


920 
\end{isamarkuptext}%


921 
\isamarkuptrue%


922 
%


923 
\isamarkupsection{Executable code%


924 
}


925 
\isamarkuptrue%


926 
%


927 
\begin{isamarkuptext}%


928 
Isabelle/Pure provides two generic frameworks to support code


929 
generation from executable specifications. Isabelle/HOL


930 
instantiates these mechanisms in a way that is amenable to enduser


931 
applications.


932 


933 
One framework generates code from both functional and relational


934 
programs to SML. See \cite{isabelleHOL} for further information


935 
(this actually covers the newstyle theory format as well).


936 


937 
\begin{matharray}{rcl}

26902

938 
\indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\

26907

939 
\indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.codemodule}{\hyperlink{command.HOL.codemodule}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isartrans{theory}{theory} \\


940 
\indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.codelibrary}{\hyperlink{command.HOL.codelibrary}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isartrans{theory}{theory} \\


941 
\indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.constscode}{\hyperlink{command.HOL.constscode}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\


942 
\indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.typescode}{\hyperlink{command.HOL.typescode}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\

26902

943 
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\

26849

944 
\end{matharray}


945 


946 
\begin{rail}


947 
'value' term


948 
;


949 


950 
( 'code\_module'  'code\_library' ) modespec ? name ? \\


951 
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\


952 
'contains' ( ( name '=' term ) +  term + )


953 
;


954 


955 
modespec: '(' ( name * ) ')'


956 
;


957 


958 
'consts\_code' (codespec +)


959 
;


960 


961 
codespec: const template attachment ?


962 
;


963 


964 
'types\_code' (tycodespec +)


965 
;


966 


967 
tycodespec: name template attachment ?


968 
;


969 


970 
const: term


971 
;


972 


973 
template: '(' string ')'


974 
;


975 


976 
attachment: 'attach' modespec ? verblbrace text verbrbrace


977 
;


978 


979 
'code' (name)?


980 
;


981 
\end{rail}


982 


983 
\begin{descr}


984 

26902

985 
\item [\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t}] evaluates and prints a

26849

986 
term using the code generator.


987 


988 
\end{descr}


989 


990 
\medskip The other framework generates code from functional programs


991 
(including overloading using type classes) to SML \cite{SML}, OCaml


992 
\cite{OCaml} and Haskell \cite{haskellrevisedreport}.


993 
Conceptually, code generation is split up in three steps:


994 
\emph{selection} of code theorems, \emph{translation} into an


995 
abstract executable view and \emph{serialization} to a specific


996 
\emph{target language}. See \cite{isabellecodegen} for an


997 
introduction on how to use it.


998 


999 
\begin{matharray}{rcl}

26907

1000 
\indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.exportcode}{\hyperlink{command.HOL.exportcode}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\


1001 
\indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.codethms}{\hyperlink{command.HOL.codethms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\


1002 
\indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.codedeps}{\hyperlink{command.HOL.codedeps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\


1003 
\indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.codedatatype}{\hyperlink{command.HOL.codedatatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\


1004 
\indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.codeconst}{\hyperlink{command.HOL.codeconst}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\


1005 
\indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.codetype}{\hyperlink{command.HOL.codetype}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\


1006 
\indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.codeclass}{\hyperlink{command.HOL.codeclass}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\


1007 
\indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.codeinstance}{\hyperlink{command.HOL.codeinstance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\


1008 
\indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.codemonad}{\hyperlink{command.HOL.codemonad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\


1009 
\indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.codereserved}{\hyperlink{command.HOL.codereserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\


1010 
\indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.codeinclude}{\hyperlink{command.HOL.codeinclude}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\


1011 
\indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.codemodulename}{\hyperlink{command.HOL.codemodulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\

27103

1012 
\indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.codeabort}{\hyperlink{command.HOL.codeabort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isartrans{theory}{theory} \\

26907

1013 
\indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.printcodesetup}{\hyperlink{command.HOL.printcodesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~~proof} \\

26902

1014 
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\

26849

1015 
\end{matharray}


1016 


1017 
\begin{rail}


1018 
'export\_code' ( constexpr + ) ? \\


1019 
( ( 'in' target ( 'module\_name' string ) ? \\


1020 
( 'file' ( string  '' ) ) ? ( '(' args ')' ) ?) + ) ?


1021 
;


1022 


1023 
'code\_thms' ( constexpr + ) ?


1024 
;


1025 


1026 
'code\_deps' ( constexpr + ) ?


1027 
;


1028 


1029 
const: term


1030 
;


1031 


1032 
constexpr: ( const  'name.*'  '*' )


1033 
;


1034 


1035 
typeconstructor: nameref


1036 
;


1037 


1038 
class: nameref


1039 
;


1040 


1041 
target: 'OCaml'  'SML'  'Haskell'


1042 
;


1043 


1044 
'code\_datatype' const +


1045 
;


1046 


1047 
'code\_const' (const + 'and') \\


1048 
( ( '(' target ( syntax ? + 'and' ) ')' ) + )


1049 
;


1050 


1051 
'code\_type' (typeconstructor + 'and') \\


1052 
( ( '(' target ( syntax ? + 'and' ) ')' ) + )


1053 
;


1054 


1055 
'code\_class' (class + 'and') \\


1056 
( ( '(' target \\


1057 
( ( string ('where' \\


1058 
( const ( '=='  equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )


1059 
;


1060 


1061 
'code\_instance' (( typeconstructor '::' class ) + 'and') \\


1062 
( ( '(' target ( '' ? + 'and' ) ')' ) + )


1063 
;


1064 


1065 
'code\_monad' const const target


1066 
;


1067 


1068 
'code\_reserved' target ( string + )


1069 
;


1070 


1071 
'code\_include' target ( string ( string  '') )


1072 
;


1073 


1074 
'code\_modulename' target ( ( string string ) + )


1075 
;


1076 

27452

1077 
'code\_abort' ( const + )

26849

1078 
;


1079 


1080 
syntax: string  ( 'infix'  'infixl'  'infixr' ) nat string


1081 
;


1082 

28562

1083 
'code' ( 'inline' ) ? ( 'del' ) ?

26849

1084 
;


1085 
\end{rail}


1086 


1087 
\begin{descr}


1088 

26907

1089 
\item [\hyperlink{command.HOL.exportcode}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface

26849

1090 
for generating and serializing code: for a given list of constants,


1091 
code is generated for the specified target languages. Abstract code


1092 
is cached incrementally. If no constant is given, the currently


1093 
cached code is serialized. If no serialization instruction is


1094 
given, only abstract code is cached.


1095 


1096 
Constants may be specified by giving them literally, referring to


1097 
all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently


1098 
available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.


1099 


1100 
By default, for each involved theory one corresponding name space


1101 
module is generated. Alternativly, a module name may be specified

26907

1102 
after the \hyperlink{keyword.modulename}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is

26849

1103 
placed in this module.


1104 


1105 
For \emph{SML} and \emph{OCaml}, the file specification refers to a


1106 
single file; for \emph{Haskell}, it refers to a whole directory,


1107 
where code is generated in multiple files reflecting the module


1108 
hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard


1109 
output. For \emph{SML}, omitting the file specification compiles


1110 
code internally in the context of the current ML session.


1111 


1112 
Serializers take an optional list of arguments in parentheses. For


1113 
\emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verbderiving (Read, Show)'' clause to each appropriate datatype


1114 
declaration.


1115 

26907

1116 
\item [\hyperlink{command.HOL.codethms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems

26849

1117 
representing the corresponding program containing all given


1118 
constants; if no constants are given, the currently cached code


1119 
theorems are printed.


1120 

26907

1121 
\item [\hyperlink{command.HOL.codedeps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of

26849

1122 
theorems representing the corresponding program containing all given


1123 
constants; if no constants are given, the currently cached code


1124 
theorems are visualized.


1125 

26907

1126 
\item [\hyperlink{command.HOL.codedatatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set

26849

1127 
for a logical type.


1128 

26907

1129 
\item [\hyperlink{command.HOL.codeconst}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants

26849

1130 
with targetspecific serializations; omitting a serialization


1131 
deletes an existing serialization.


1132 

26907

1133 
\item [\hyperlink{command.HOL.codetype}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type

26849

1134 
constructors with targetspecific serializations; omitting a


1135 
serialization deletes an existing serialization.


1136 

26907

1137 
\item [\hyperlink{command.HOL.codeclass}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes

26849

1138 
with targetspecific class names; in addition, constants associated


1139 
with this class may be given targetspecific names used for instance


1140 
declarations; omitting a serialization deletes an existing


1141 
serialization. This applies only to \emph{Haskell}.


1142 

26907

1143 
\item [\hyperlink{command.HOL.codeinstance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type

26849

1144 
constructor / class instance relations as ``already present'' for a


1145 
given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing


1146 
``already present'' declaration. This applies only to


1147 
\emph{Haskell}.


1148 

26907

1149 
\item [\hyperlink{command.HOL.codemonad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary

27834

1150 
mechanism to generate monadic code for Haskell.

26849

1151 

26907

1152 
\item [\hyperlink{command.HOL.codereserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as

26849

1153 
reserved for a given target, preventing it to be shadowed by any


1154 
generated code.


1155 

26907

1156 
\item [\hyperlink{command.HOL.codeinclude}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content

27834

1157 
(``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument

26849

1158 
will remove an already added ``include''.


1159 

26907

1160 
\item [\hyperlink{command.HOL.codemodulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from

26849

1161 
one module name onto another.


1162 

27103

1163 
\item [\hyperlink{command.HOL.codeabort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which

27452

1164 
are not required to have a definition by means of defining equations;

27103

1165 
if needed these are implemented by program abort instead.

26849

1166 

28562

1167 
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or


1168 
with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for

26849

1169 
code generation. Usually packages introducing defining equations

27452

1170 
provide a reasonable default setup for selection.

26849

1171 

26902

1172 
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with

28562

1173 
option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are

26849

1174 
applied as rewrite rules to any defining equation during


1175 
preprocessing.


1176 

26907

1177 
\item [\hyperlink{command.HOL.printcodesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on

26849

1178 
selected defining equations, code generator datatypes and


1179 
preprocessor setup.


1180 


1181 
\end{descr}%


1182 
\end{isamarkuptext}%


1183 
\isamarkuptrue%


1184 
%

27047

1185 
\isamarkupsection{Definition by specification \label{sec:holspecification}%


1186 
}


1187 
\isamarkuptrue%


1188 
%


1189 
\begin{isamarkuptext}%


1190 
\begin{matharray}{rcl}


1191 
\indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\


1192 
\indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.axspecification}{\hyperlink{command.HOL.axspecification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\


1193 
\end{matharray}


