wneuper/isa: doc-src/IsarRef/Thy/document/HOL

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{HOL{\isaliteral{5F}{\isacharunderscore}}Specific}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline

    12 \isakeyword{imports}\ Base\ Main\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

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

    22 }

    23 \isamarkuptrue%

    24 %

    25 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%

    26 }

    27 \isamarkuptrue%

    28 %

    29 \begin{isamarkuptext}%

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

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

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

    33   structural operational semantics is an inductive definition of an

    34   evaluation relation.

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

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

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

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

    40   relations to formalise equivalence of processes and infinite data

    41   structures.

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

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

    45   \cite{paulson-CADE}; a longer version is distributed with Isabelle.}

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

    47   simpler than that of ZF thanks to implicit type-checking in HOL.

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

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

    50   to use inference rules for type-checking.

    52   \begin{matharray}{rcl}

    53     \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

    54     \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

    55     \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

    56     \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

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

    58   \end{matharray}

    60   \begin{railoutput}

    61 \rail@begin{7}{}

    62 \rail@bar

    63 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]

    64 \rail@nextbar{1}

    65 \rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]

    66 \rail@nextbar{2}

    67 \rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]

    68 \rail@nextbar{3}

    69 \rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]

    70 \rail@endbar

    71 \rail@bar

    72 \rail@nextbar{1}

    73 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

    74 \rail@endbar

    75 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

    76 \rail@bar

    77 \rail@nextbar{1}

    78 \rail@term{\isa{\isakeyword{for}}}[]

    79 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

    80 \rail@endbar

    81 \rail@cr{5}

    82 \rail@bar

    83 \rail@nextbar{6}

    84 \rail@term{\isa{\isakeyword{where}}}[]

    85 \rail@nont{\isa{clauses}}[]

    86 \rail@endbar

    87 \rail@bar

    88 \rail@nextbar{6}

    89 \rail@term{\isa{\isakeyword{monos}}}[]

    90 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

    91 \rail@endbar

    92 \rail@end

    93 \rail@begin{3}{\isa{clauses}}

    94 \rail@plus

    95 \rail@bar

    96 \rail@nextbar{1}

    97 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

    98 \rail@endbar

    99 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   100 \rail@nextplus{2}

   101 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]

   102 \rail@endplus

   103 \rail@end

   104 \rail@begin{3}{}

   105 \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]

   106 \rail@bar

   107 \rail@nextbar{1}

   108 \rail@term{\isa{add}}[]

   109 \rail@nextbar{2}

   110 \rail@term{\isa{del}}[]

   111 \rail@endbar

   112 \rail@end

   113 \end{railoutput}

   116   \begin{description}

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

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

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

   121   (co)inductive predicates that remain fixed throughout the

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

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

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

   125   \emph{must} be a theorem of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}},

   126   for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!

   128   \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}} are wrappers for to the previous commands,

   129   allowing the definition of (co)inductive sets.

   131   \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules.  These

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

   134   \end{description}%

   135 \end{isamarkuptext}%

   136 \isamarkuptrue%

   137 %

   138 \isamarkupsubsection{Derived rules%

   139 }

   140 \isamarkuptrue%

   141 %

   142 \begin{isamarkuptext}%

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

   144   theory and also proves some theorems:

   146   \begin{description}

   148   \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven

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

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

   151   theory file;

   153   \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;

   155   \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction

   156   rule.

   158   \end{description}

   160   When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are

   161   defined simultaneously, the list of introduction rules is called

   162   \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}intros{\isaliteral{22}{\isachardoublequote}}}, the case analysis rules are

   163   called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}cases{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}cases{\isaliteral{22}{\isachardoublequote}}}, and the list

   164   of mutual induction rules is called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}inducts{\isaliteral{22}{\isachardoublequote}}}.%

   165 \end{isamarkuptext}%

   166 \isamarkuptrue%

   167 %

   168 \isamarkupsubsection{Monotonicity theorems%

   169 }

   170 \isamarkuptrue%

   171 %

   172 \begin{isamarkuptext}%

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

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

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

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

   177   theorems may be added:

   179   \begin{itemize}

   181   \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}}, for proving

   182   monotonicity of inductive definitions whose introduction rules have

   183   premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.

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

   186   general form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}.  For example, in

   187   the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is

   188   \[

   189   \infer{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}

   190   \]

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

   193   of expressions, e.g.

   194   \[

   195   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad

   196   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q{\isaliteral{22}{\isachardoublequote}}}

   197   \]

   199   \item Equations for reducing complex operators to more primitive

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

   201   \[

   202   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad

   203   \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ P\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}

   204   \]

   206   \end{itemize}

   208   %FIXME: Example of an inductive definition%

   209 \end{isamarkuptext}%

   210 \isamarkuptrue%

   211 %

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

   213 }

   214 \isamarkuptrue%

   215 %

   216 \begin{isamarkuptext}%

   217 \begin{matharray}{rcl}

   218     \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   219     \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   220     \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   221     \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   222   \end{matharray}

   224   \begin{railoutput}

   225 \rail@begin{2}{}

   226 \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]

   227 \rail@bar

   228 \rail@nextbar{1}

   229 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   230 \rail@endbar

   231 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   232 \rail@term{\isa{\isakeyword{where}}}[]

   233 \rail@nont{\isa{equations}}[]

   234 \rail@end

   235 \rail@begin{4}{}

   236 \rail@bar

   237 \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]

   238 \rail@nextbar{1}

   239 \rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]

   240 \rail@endbar

   241 \rail@bar

   242 \rail@nextbar{1}

   243 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   244 \rail@endbar

   245 \rail@bar

   246 \rail@nextbar{1}

   247 \rail@nont{\isa{functionopts}}[]

   248 \rail@endbar

   249 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   250 \rail@cr{3}

   251 \rail@term{\isa{\isakeyword{where}}}[]

   252 \rail@nont{\isa{equations}}[]

   253 \rail@end

   254 \rail@begin{3}{\isa{equations}}

   255 \rail@plus

   256 \rail@bar

   257 \rail@nextbar{1}

   258 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   259 \rail@endbar

   260 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   261 \rail@nextplus{2}

   262 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]

   263 \rail@endplus

   264 \rail@end

   265 \rail@begin{3}{\isa{functionopts}}

   266 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   267 \rail@plus

   268 \rail@bar

   269 \rail@term{\isa{sequential}}[]

   270 \rail@nextbar{1}

   271 \rail@term{\isa{domintros}}[]

   272 \rail@endbar

   273 \rail@nextplus{2}

   274 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]

   275 \rail@endplus

   276 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   277 \rail@end

   278 \rail@begin{2}{}

   279 \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]

   280 \rail@bar

   281 \rail@nextbar{1}

   282 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   283 \rail@endbar

   284 \rail@end

   285 \end{railoutput}

   288   \begin{description}

   290   \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive

   291   functions over datatypes, see also \cite{isabelle-HOL}.

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

   294   wellfounded recursion. A detailed description with examples can be

   295   found in \cite{isabelle-function}. The function is specified by a

   296   set of (possibly conditional) recursive equations with arbitrary

   297   pattern matching. The command generates proof obligations for the

   298   completeness and the compatibility of patterns.

   300   The defined function is considered partial, and the resulting

   301   simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule

   302   (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain

   303   predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}

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

   306   \item \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} is a shorthand notation for ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}sequential{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, followed by automated

   307   proof attempts regarding pattern matching and termination.  See

   308   \cite{isabelle-function} for further details.

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

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

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

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

   314   the induction principle is established.

   316   \end{description}

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

   319   command accommodate

   320   reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} (where \isa{c} is the name of the function definition)

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

   322   to the user-specified equations. Cases are numbered (starting from 1).

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

   325   with structural recursion on the datatype the recursion is carried

   326   out.

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

   329   theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)

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

   331   explicitly as well.

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

   334   options.

   336   \begin{description}

   338   \item \isa{sequential} enables a preprocessor which disambiguates

   339   overlapping patterns by making them mutually disjoint.  Earlier

   340   equations take precedence over later ones.  This allows to give the

   341   specification in a format very similar to functional programming.

   342   Note that the resulting simplification and induction rules

   343   correspond to the transformed specification, not the one given

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

   345   may result in several theorems.  Also note that this automatic

   346   transformation only works for ML-style datatype patterns.

   348   \item \isa{domintros} enables the automated generation of

   349   introduction rules for the domain predicate. While mostly not

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

   352   \end{description}%

   353 \end{isamarkuptext}%

   354 \isamarkuptrue%

   355 %

   356 \isamarkupsubsection{Proof methods related to recursive definitions%

   357 }

   358 \isamarkuptrue%

   359 %

   360 \begin{isamarkuptext}%

   361 \begin{matharray}{rcl}

   362     \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}}} & : & \isa{method} \\

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

   364     \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\

   365     \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\

   366   \end{matharray}

   368   \begin{railoutput}

   369 \rail@begin{1}{}

   370 \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]

   371 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   372 \rail@end

   373 \rail@begin{2}{}

   374 \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]

   375 \rail@plus

   376 \rail@nextplus{1}

   377 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]

   378 \rail@endplus

   379 \rail@end

   380 \rail@begin{2}{}

   381 \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]

   382 \rail@nont{\isa{orders}}[]

   383 \rail@plus

   384 \rail@nextplus{1}

   385 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]

   386 \rail@endplus

   387 \rail@end

   388 \rail@begin{4}{\isa{orders}}

   389 \rail@plus

   390 \rail@nextplus{1}

   391 \rail@bar

   392 \rail@term{\isa{max}}[]

   393 \rail@nextbar{2}

   394 \rail@term{\isa{min}}[]

   395 \rail@nextbar{3}

   396 \rail@term{\isa{ms}}[]

   397 \rail@endbar

   398 \rail@endplus

   399 \rail@end

   400 \end{railoutput}

   403   \begin{description}

   405   \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to

   406   solve goals regarding the completeness of pattern matching, as

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

   408   \cite{isabelle-function}).

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

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

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

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

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

   415   termination proofs.

   417   \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully

   418   automated termination proof by searching for a lexicographic

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

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

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

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

   423   \secref{sec:clasimp}.

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

   426   to analyse the situation (cf.\ \cite{isabelle-function}).

   428   \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,

   429   using a variation of the size-change principle, together with a

   430   graph decomposition technique (see \cite{krauss_phd} for details).

   431   Three kinds of orders are used internally: \isa{max}, \isa{min},

   432   and \isa{ms} (multiset), which is only available when the theory

   433   \isa{Multiset} is loaded. When no order kinds are given, they are

   434   tried in order. The search for a termination proof uses SAT solving

   435   internally.

   437  For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.

   439   \end{description}%

   440 \end{isamarkuptext}%

   441 \isamarkuptrue%

   442 %

   443 \isamarkupsubsection{Functions with explicit partiality%

   444 }

   445 \isamarkuptrue%

   446 %

   447 \begin{isamarkuptext}%

   448 \begin{matharray}{rcl}

   449     \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   450     \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}}} & : & \isa{attribute} \\

   451   \end{matharray}

   453   \begin{railoutput}

   454 \rail@begin{5}{}

   455 \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]

   456 \rail@bar

   457 \rail@nextbar{1}

   458 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   459 \rail@endbar

   460 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   461 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   462 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   463 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   464 \rail@cr{3}

   465 \rail@term{\isa{\isakeyword{where}}}[]

   466 \rail@bar

   467 \rail@nextbar{4}

   468 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   469 \rail@endbar

   470 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   471 \rail@end

   472 \end{railoutput}

   475   \begin{description}

   477   \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines

   478   recursive functions based on fixpoints in complete partial

   479   orders. No termination proof is required from the user or

   480   constructed internally. Instead, the possibility of non-termination

   481   is modelled explicitly in the result type, which contains an

   482   explicit bottom element.

   484   Pattern matching and mutual recursion are currently not supported.

   485   Thus, the specification consists of a single function described by a

   486   single recursive equation.

   488   There are no fixed syntactic restrictions on the body of the

   489   function, but the induced functional must be provably monotonic

   490   wrt.\ the underlying order.  The monotonicitity proof is performed

   491   internally, and the definition is rejected when it fails. The proof

   492   can be influenced by declaring hints using the

   493   \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.

   495   The mandatory \isa{mode} argument specifies the mode of operation

   496   of the command, which directly corresponds to a complete partial

   497   order on the result type. By default, the following modes are

   498   defined:

   500   \begin{description}

   501   \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a

   502   non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result

   503   must also be \isa{None}. This is best achieved through the use of

   504   the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.

   506   \item \isa{tailrec} defines functions with an arbitrary result

   507   type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element.  Now, monotonicity requires that

   508   if \isa{undefined} is returned by a recursive call, then the

   509   overall result must also be \isa{undefined}. In practice, this is

   510   only satisfied when each recursive call is a tail call, whose result

   511   is directly returned. Thus, this mode of operation allows the

   512   definition of arbitrary tail-recursive functions.

   513   \end{description}

   515   Experienced users may define new modes by instantiating the locale

   516   \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.

   518   \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for

   519   use in the internal monononicity proofs of partial function

   520   definitions.

   522   \end{description}%

   523 \end{isamarkuptext}%

   524 \isamarkuptrue%

   525 %

   526 \isamarkupsubsection{Old-style recursive function definitions (TFL)%

   527 }

   528 \isamarkuptrue%

   529 %

   530 \begin{isamarkuptext}%

   531 The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\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.

   533   \begin{matharray}{rcl}

   534     \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   535     \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   536   \end{matharray}

   538   \begin{railoutput}

   539 \rail@begin{5}{}

   540 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]

   541 \rail@bar

   542 \rail@nextbar{1}

   543 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   544 \rail@term{\isa{\isakeyword{permissive}}}[]

   545 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   546 \rail@endbar

   547 \rail@cr{3}

   548 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   549 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   550 \rail@plus

   551 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   552 \rail@nextplus{4}

   553 \rail@endplus

   554 \rail@bar

   555 \rail@nextbar{4}

   556 \rail@nont{\isa{hints}}[]

   557 \rail@endbar

   558 \rail@end

   559 \rail@begin{2}{}

   560 \rail@nont{\isa{recdeftc}}[]

   561 \rail@bar

   562 \rail@nextbar{1}

   563 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   564 \rail@endbar

   565 \rail@nont{\isa{tc}}[]

   566 \rail@end

   567 \rail@begin{2}{\isa{hints}}

   568 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   569 \rail@term{\isa{\isakeyword{hints}}}[]

   570 \rail@plus

   571 \rail@nextplus{1}

   572 \rail@cnont{\isa{recdefmod}}[]

   573 \rail@endplus

   574 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   575 \rail@end

   576 \rail@begin{4}{\isa{recdefmod}}

   577 \rail@bar

   578 \rail@bar

   579 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]

   580 \rail@nextbar{1}

   581 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]

   582 \rail@nextbar{2}

   583 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]

   584 \rail@endbar

   585 \rail@bar

   586 \rail@nextbar{1}

   587 \rail@term{\isa{add}}[]

   588 \rail@nextbar{2}

   589 \rail@term{\isa{del}}[]

   590 \rail@endbar

   591 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

   592 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

   593 \rail@nextbar{3}

   594 \rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]

   595 \rail@endbar

   596 \rail@end

   597 \rail@begin{2}{\isa{tc}}

   598 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   599 \rail@bar

   600 \rail@nextbar{1}

   601 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   602 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

   603 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   604 \rail@endbar

   605 \rail@end

   606 \end{railoutput}

   609   \begin{description}

   611   \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded

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

   613   \cite{isabelle-HOL}.  The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells

   614   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

   621   \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the

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

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

   624   constant \isa{c}.

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

   627   its internal proofs without manual intervention.

   629   \end{description}

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

   632   globally, using the following attributes.

   634   \begin{matharray}{rcl}

   635     \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}} & : & \isa{attribute} \\

   636     \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}} & : & \isa{attribute} \\

   637     \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\

   638   \end{matharray}

   640   \begin{railoutput}

   641 \rail@begin{3}{}

   642 \rail@bar

   643 \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]

   644 \rail@nextbar{1}

   645 \rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]

   646 \rail@nextbar{2}

   647 \rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]

   648 \rail@endbar

   649 \rail@bar

   650 \rail@nextbar{1}

   651 \rail@term{\isa{add}}[]

   652 \rail@nextbar{2}

   653 \rail@term{\isa{del}}[]

   654 \rail@endbar

   655 \rail@end

   656 \end{railoutput}%

   657 \end{isamarkuptext}%

   658 \isamarkuptrue%

   659 %

   660 \isamarkupsection{Datatypes \label{sec:hol-datatype}%

   661 }

   662 \isamarkuptrue%

   663 %

   664 \begin{isamarkuptext}%

   665 \begin{matharray}{rcl}

   666     \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   667     \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   668   \end{matharray}

   670   \begin{railoutput}

   671 \rail@begin{2}{}

   672 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]

   673 \rail@plus

   674 \rail@nont{\isa{spec}}[]

   675 \rail@nextplus{1}

   676 \rail@cterm{\isa{\isakeyword{and}}}[]

   677 \rail@endplus

   678 \rail@end

   679 \rail@begin{3}{}

   680 \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]

   681 \rail@bar

   682 \rail@nextbar{1}

   683 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   684 \rail@plus

   685 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   686 \rail@nextplus{2}

   687 \rail@endplus

   688 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   689 \rail@endbar

   690 \rail@plus

   691 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   692 \rail@nextplus{1}

   693 \rail@endplus

   694 \rail@end

   695 \rail@begin{2}{\isa{spec}}

   696 \rail@bar

   697 \rail@nextbar{1}

   698 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]

   699 \rail@endbar

   700 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]

   701 \rail@bar

   702 \rail@nextbar{1}

   703 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

   704 \rail@endbar

   705 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

   706 \rail@plus

   707 \rail@nont{\isa{cons}}[]

   708 \rail@nextplus{1}

   709 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]

   710 \rail@endplus

   711 \rail@end

   712 \rail@begin{2}{\isa{cons}}

   713 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   714 \rail@plus

   715 \rail@nextplus{1}

   716 \rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   717 \rail@endplus

   718 \rail@bar

   719 \rail@nextbar{1}

   720 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

   721 \rail@endbar

   722 \rail@end

   723 \end{railoutput}

   726   \begin{description}

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

   729   HOL.

   731   \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as

   732   datatypes.

   734   For foundational reasons, some basic types such as \isa{nat}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{bool} and \isa{unit} are

   735   introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}.  To

   736   recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules

   737   for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion

   738   combinators), such types may be represented as actual datatypes

   739   later.  This is done by specifying the constructors of the desired

   740   type, and giving a proof of the induction rule, distinctness and

   741   injectivity of constructors.

   743   For example, see \verb|~~/src/HOL/Sum_Type.thy| for the

   744   representation of the primitive sum type as fully-featured datatype.

   746   \end{description}

   748   The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide

   749   case names according to the given constructors, while parameters are

   750   named after the types (see also \secref{sec:cases-induct}).

   752   See \cite{isabelle-HOL} for more details on datatypes, but beware of

   753   the old-style theory syntax being used there!  Apart from proper

   754   proof methods for case-analysis and induction, there are also

   755   emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} available, see \secref{sec:hol-induct-tac}; these admit

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

   757   internally bound parameters).%

   758 \end{isamarkuptext}%

   759 \isamarkuptrue%

   760 %

   761 \isamarkupsubsubsection{Examples%

   762 }

   763 \isamarkuptrue%

   764 %

   765 \begin{isamarkuptext}%

   766 We define a type of finite sequences, with slightly different

   767   names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%

   768 \end{isamarkuptext}%

   769 \isamarkuptrue%

   770 \isacommand{datatype}\isamarkupfalse%

   771 \ {\isaliteral{27}{\isacharprime}}a\ seq\ {\isaliteral{3D}{\isacharequal}}\ Empty\ {\isaliteral{7C}{\isacharbar}}\ Seq\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ seq{\isaliteral{22}{\isachardoublequoteclose}}%

   772 \begin{isamarkuptext}%

   773 We can now prove some simple lemma by structural induction:%

   774 \end{isamarkuptext}%

   775 \isamarkuptrue%

   776 \isacommand{lemma}\isamarkupfalse%

   777 \ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   778 %

   779 \isadelimproof

   780 %

   781 \endisadelimproof

   782 %

   783 \isatagproof

   784 \isacommand{proof}\isamarkupfalse%

   785 \ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline

   786 \ \ \isacommand{case}\isamarkupfalse%

   787 \ Empty%

   788 \begin{isamarkuptxt}%

   789 This case can be proved using the simplifier: the freeness

   790     properties of the datatype are already declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rules.%

   791 \end{isamarkuptxt}%

   792 \isamarkuptrue%

   793 \ \ \isacommand{show}\isamarkupfalse%

   794 \ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ Empty\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Empty{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   795 \ \ \ \ \isacommand{by}\isamarkupfalse%

   796 \ simp\isanewline

   797 \isacommand{next}\isamarkupfalse%

   798 \isanewline

   799 \ \ \isacommand{case}\isamarkupfalse%

   800 \ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}%

   801 \begin{isamarkuptxt}%

   802 The step case is proved similarly.%

   803 \end{isamarkuptxt}%

   804 \isamarkuptrue%

   805 \ \ \isacommand{show}\isamarkupfalse%

   806 \ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Seq\ y\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   807 \ \ \ \ \isacommand{using}\isamarkupfalse%

   808 \ {\isaliteral{60}{\isacharbackquoteopen}}Seq\ y\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ ys{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{by}\isamarkupfalse%

   809 \ simp\isanewline

   810 \isacommand{qed}\isamarkupfalse%

   811 %

   812 \endisatagproof

   813 {\isafoldproof}%

   814 %

   815 \isadelimproof

   816 %

   817 \endisadelimproof

   818 %

   819 \begin{isamarkuptext}%

   820 Here is a more succinct version of the same proof:%

   821 \end{isamarkuptext}%

   822 \isamarkuptrue%

   823 \isacommand{lemma}\isamarkupfalse%

   824 \ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   825 %

   826 \isadelimproof

   827 \ \ %

   828 \endisadelimproof

   829 %

   830 \isatagproof

   831 \isacommand{by}\isamarkupfalse%

   832 \ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%

   833 \endisatagproof

   834 {\isafoldproof}%

   835 %

   836 \isadelimproof

   837 %

   838 \endisadelimproof

   839 %

   840 \isamarkupsection{Records \label{sec:hol-record}%

   841 }

   842 \isamarkuptrue%

   843 %

   844 \begin{isamarkuptext}%

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

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

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

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

   849   admits operations that are polymorphic with respect to record

   850   extension, yielding ``object-oriented'' effects like (single)

   851   inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more

   852   details on object-oriented verification and record subtyping in HOL.%

   853 \end{isamarkuptext}%

   854 \isamarkuptrue%

   855 %

   856 \isamarkupsubsection{Basic concepts%

   857 }

   858 \isamarkuptrue%

   859 %

   860 \begin{isamarkuptext}%

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

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

   864   \begin{center}

   865   \begin{tabular}{l|l|l}

   866     & record terms & record types \\ \hline

   867     fixed & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

   868     schematic & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} &

   869       \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ M{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

   870   \end{tabular}

   871   \end{center}

   873   \noindent The ASCII representation of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.

   875   A fixed record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} has field \isa{x} of value

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

   877   type is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, assuming that \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{22}{\isachardoublequote}}}

   878   and \isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{22}{\isachardoublequote}}}.

   880   A record scheme like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} contains fields

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

   882   as indicated by the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' notation (which is actually part

   883   of the syntax).  The improper field ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' of a record

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

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

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

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

   888   previous scheme may get instantiated to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{m{\isaliteral{27}{\isacharprime}}} refers to a different more part.

   889   Fixed records are special instances of record schemes, where

   890   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}

   891   element.  In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation

   892   for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.

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

   895   typed language like HOL work out:

   897   \begin{enumerate}

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

   900   variable,

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

   903   the logic as first-class values.

   905   \end{enumerate}

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

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

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

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

   911   The record package provides several standard operations like

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

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

   914   tutorial \cite{isabelle-hol-book} for further instructions on using

   915   records in practice.%

   916 \end{isamarkuptext}%

   917 \isamarkuptrue%

   918 %

   919 \isamarkupsubsection{Record specifications%

   920 }

   921 \isamarkuptrue%

   922 %

   923 \begin{isamarkuptext}%

   924 \begin{matharray}{rcl}

   925     \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   926   \end{matharray}

   928   \begin{railoutput}

   929 \rail@begin{4}{}

   930 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]

   931 \rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]

   932 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

   933 \rail@cr{2}

   934 \rail@bar

   935 \rail@nextbar{3}

   936 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   937 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]

   938 \rail@endbar

   939 \rail@plus

   940 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]

   941 \rail@nextplus{3}

   942 \rail@endplus

   943 \rail@end

   944 \end{railoutput}

   947   \begin{description}

   949   \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{2B}{\isacharplus}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} defines extensible record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}},

   950   derived from the optional parent record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} by adding new

   951   field components \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} etc.

   953   The type variables of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} need to be

   954   covered by the (distinct) parameters \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}.  Type constructor \isa{t} has to be new, while \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} needs to specify an instance of an existing record type.  At

   955   least one new field \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} has to be specified.

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

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

   958   the record name internally.

   960   The parent record specification \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is optional; if omitted

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

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

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

   964   merge multiple parent records!

   966   For convenience, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is made a

   967   type abbreviation for the fixed record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, likewise is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequote}}} made an abbreviation for

   968   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.

   970   \end{description}%

   971 \end{isamarkuptext}%

   972 \isamarkuptrue%

   973 %

   974 \isamarkupsubsection{Record operations%

   975 }

   976 \isamarkuptrue%

   977 %

   978 \begin{isamarkuptext}%

   979 Any record definition of the form presented above produces certain

   980   standard operations.  Selectors and updates are provided for any

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

   982   cumulative record constructor functions.  To simplify the

   983   presentation below, we assume for now that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is a root record with fields \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.

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

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

   988   \begin{matharray}{lll}

   989     \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\

   990     \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

   991   \end{matharray}

   993   There is special syntax for application of updates: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} abbreviates term \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{5F}{\isacharunderscore}}update\ a\ r{\isaliteral{22}{\isachardoublequote}}}.  Further notation for

   994   repeated updates is also available: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} may be written \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.  Note that

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

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

   997   function applications, fields may be freely permuted in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, as far as logical equality is concerned.

   998   Thus commutativity of independent updates can be proven within the

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

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

  1002   constructor function:

  1004   \begin{matharray}{lll}

  1005     \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1006   \end{matharray}

  1008   \medskip We now reconsider the case of non-root records, which are

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

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

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

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

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

  1014   Assuming that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} has ancestor

  1015   fields \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}},

  1016   the above record operations will get the following types:

  1018   \medskip

  1019   \begin{tabular}{lll}

  1020     \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\

  1021     \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1022     \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1023   \end{tabular}

  1024   \medskip

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

  1027   derived record scheme specifically: \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} produces a

  1028   record fragment consisting of exactly the new fields introduced here

  1029   (the result may serve as a more part elsewhere); \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}

  1030   takes a fixed record and adds a given more part; \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} restricts a record scheme to a fixed record.

  1032   \medskip

  1033   \begin{tabular}{lll}

  1034     \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1035     \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1036     \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\

  1037   \end{tabular}

  1038   \medskip

  1040   \noindent Note that \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} coincide

  1041   for root records.%

  1042 \end{isamarkuptext}%

  1043 \isamarkuptrue%

  1044 %

  1045 \isamarkupsubsection{Derived rules and proof tools%

  1046 }

  1047 \isamarkuptrue%

  1048 %

  1049 \begin{isamarkuptext}%

  1050 The record package proves several results internally, declaring

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

  1052   reason about record structures quite conveniently.  Assume that

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

  1055   \begin{enumerate}

  1057   \item Standard conversions for selectors or updates applied to

  1058   record constructor terms are made part of the default Simplifier

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

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

  1061   are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.

  1063   \item Selectors applied to updated records are automatically reduced

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

  1065   standard Simplifier setup.

  1067   \item Inject equations of a form analogous to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} are declared to the Simplifier and Classical

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

  1069   \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}iffs{\isaliteral{22}{\isachardoublequote}}}.

  1071   \item The introduction rule for record equality analogous to \isa{{\isaliteral{22}{\isachardoublequote}}x\ r\ {\isaliteral{3D}{\isacharequal}}\ x\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ r\ {\isaliteral{3D}{\isacharequal}}\ y\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} is declared to the Simplifier,

  1072   and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''.

  1073   The rule is called \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}equality{\isaliteral{22}{\isachardoublequote}}}.

  1075   \item Representations of arbitrary record expressions as canonical

  1076   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,

  1077   \secref{sec:cases-induct}).  Several variations are available, for

  1078   fixed records, record schemes, more parts etc.

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

  1081   sensible rule according to the type of the indicated record

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

  1084   \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not}

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

  1086   using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}.

  1088   \end{enumerate}%

  1089 \end{isamarkuptext}%

  1090 \isamarkuptrue%

  1091 %

  1092 \isamarkupsubsubsection{Examples%

  1093 }

  1094 \isamarkuptrue%

  1095 %

  1096 \begin{isamarkuptext}%

  1097 See \verb|~~/src/HOL/ex/Records.thy|, for example.%

  1098 \end{isamarkuptext}%

  1099 \isamarkuptrue%

  1100 %

  1101 \isamarkupsection{Adhoc tuples%

  1102 }

  1103 \isamarkuptrue%

  1104 %

  1105 \begin{isamarkuptext}%

  1106 \begin{matharray}{rcl}

  1107     \indexdef{HOL}{attribute}{split\_format}\hypertarget{attribute.HOL.split-format}{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\

  1108   \end{matharray}

  1110   \begin{railoutput}

  1111 \rail@begin{2}{}

  1112 \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]

  1113 \rail@bar

  1114 \rail@nextbar{1}

  1115 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1116 \rail@term{\isa{complete}}[]

  1117 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1118 \rail@endbar

  1119 \rail@end

  1120 \end{railoutput}

  1123   \begin{description}

  1125   \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}complete{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} causes

  1126   arguments in function applications to be represented canonically

  1127   according to their tuple type structure.

  1129   Note that this operation tends to invent funny names for new local

  1130   parameters introduced.

  1132   \end{description}%

  1133 \end{isamarkuptext}%

  1134 \isamarkuptrue%

  1135 %

  1136 \isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%

  1137 }

  1138 \isamarkuptrue%

  1139 %

  1140 \begin{isamarkuptext}%

  1141 A Gordon/HOL-style type definition is a certain axiom scheme

  1142   that identifies a new type with a subset of an existing type.  More

  1143   precisely, the new type is defined by exhibiting an existing type

  1144   \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves

  1145   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}.  Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset.  New functions are

  1146   postulated that establish an isomorphism between the new type and

  1147   the subset.  In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type

  1148   variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} which means that the type definition

  1149   produces a type constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} depending on

  1150   those type arguments.

  1152   The axiomatization can be considered a ``definition'' in the sense

  1153   of the particular set-theoretic interpretation of HOL

  1154   \cite{pitts93}, where the universe of types is required to be

  1155   downwards-closed wrt.\ arbitrary non-empty subsets.  Thus genuinely

  1156   new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range

  1157   of HOL models by construction.  Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic

  1158   abbreviations, without any logical significance.

  1160   \begin{matharray}{rcl}

  1161     \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  1162   \end{matharray}

  1164   \begin{railoutput}

  1165 \rail@begin{2}{}

  1166 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]

  1167 \rail@bar

  1168 \rail@nextbar{1}

  1169 \rail@nont{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}[]

  1170 \rail@endbar

  1171 \rail@nont{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}[]

  1172 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1173 \rail@nont{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}[]

  1174 \rail@end

  1175 \rail@begin{3}{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}

  1176 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1177 \rail@bar

  1178 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1179 \rail@nextbar{1}

  1180 \rail@term{\isa{\isakeyword{open}}}[]

  1181 \rail@nextbar{2}

  1182 \rail@term{\isa{\isakeyword{open}}}[]

  1183 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1184 \rail@endbar

  1185 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1186 \rail@end

  1187 \rail@begin{2}{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}

  1188 \rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]

  1189 \rail@bar

  1190 \rail@nextbar{1}

  1191 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

  1192 \rail@endbar

  1193 \rail@end

  1194 \rail@begin{2}{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}

  1195 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1196 \rail@bar

  1197 \rail@nextbar{1}

  1198 \rail@term{\isa{\isakeyword{morphisms}}}[]

  1199 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1200 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1201 \rail@endbar

  1202 \rail@end

  1203 \end{railoutput}

  1206   \begin{description}

  1208   \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}

  1209   axiomatizes a type definition in the background theory of the

  1210   current context, depending on a non-emptiness result of the set

  1211   \isa{A} that needs to be proven here.  The set \isa{A} may

  1212   contain type variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as specified on the LHS,

  1213   but no term variables.

  1215   Even though a local theory specification, the newly introduced type

  1216   constructor cannot depend on parameters or assumptions of the

  1217   context: this is structurally impossible in HOL.  In contrast, the

  1218   non-emptiness proof may use local assumptions in unusual situations,

  1219   which could result in different interpretations in target contexts:

  1220   the meaning of the bijection between the representing set \isa{A}

  1221   and the new type \isa{t} may then change in different application

  1222   contexts.

  1224   By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type

  1225   constructor \isa{t} for the new type, and a term constant \isa{t} for the representing set within the old type.  Use the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option to suppress a separate constant definition

  1226   altogether.  The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},

  1227   its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t}, unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.

  1229   The core axiomatization uses the locale predicate \isa{type{\isaliteral{5F}{\isacharunderscore}}definition} as defined in Isabelle/HOL.  Various basic

  1230   consequences of that are instantiated accordingly, re-using the

  1231   locale facts with names derived from the new type constructor.  Thus

  1232   the generic \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep} is turned into the specific

  1233   \isa{{\isaliteral{22}{\isachardoublequote}}Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{22}{\isachardoublequote}}}, for example.

  1235   Theorems \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep}, \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inverse}

  1236   provide the most basic characterization as a corresponding

  1237   injection/surjection pair (in both directions).  The derived rules

  1238   \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inject} provide a more convenient version of

  1239   injectivity, suitable for automated proof tools (e.g.\ in

  1240   declarations involving \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}).

  1241   Furthermore, the rules \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}cases}~/ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}induct}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}cases}~/

  1242   \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views on

  1243   surjectivity.  These rules are already declared as set or type rules

  1244   for the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods,

  1245   respectively.

  1247   An alternative name for the set definition (and other derived

  1248   entities) may be specified in parentheses; the default is to use

  1249   \isa{t} directly.

  1251   \end{description}

  1253   \begin{warn}

  1254   If you introduce a new type axiomatically, i.e.\ via \indexref{}{command}{typedecl}\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} and \indexref{}{command}{axiomatization}\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}, the minimum requirement

  1255   is that it has a non-empty model, to avoid immediate collapse of the

  1256   HOL logic.  Moreover, one needs to demonstrate that the

  1257   interpretation of such free-form axiomatizations can coexist with

  1258   that of the regular \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}} scheme, and any extension

  1259   that other people might have introduced elsewhere (e.g.\ in HOLCF

  1260   \cite{MuellerNvOS99}).

  1261   \end{warn}%

  1262 \end{isamarkuptext}%

  1263 \isamarkuptrue%

  1264 %

  1265 \isamarkupsubsubsection{Examples%

  1266 }

  1267 \isamarkuptrue%

  1268 %

  1269 \begin{isamarkuptext}%

  1270 Type definitions permit the introduction of abstract data

  1271   types in a safe way, namely by providing models based on already

  1272   existing types.  Given some abstract axiomatic description \isa{P}

  1273   of a type, this involves two steps:

  1275   \begin{enumerate}

  1277   \item Find an appropriate type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and subset \isa{A} which

  1278   has the desired properties \isa{P}, and make a type definition

  1279   based on this representation.

  1281   \item Prove that \isa{P} holds for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} by lifting \isa{P}

  1282   from the representation.

  1284   \end{enumerate}

  1286   You can later forget about the representation and work solely in

  1287   terms of the abstract properties \isa{P}.

  1289   \medskip The following trivial example pulls a three-element type

  1290   into existence within the formal logical environment of HOL.%

  1291 \end{isamarkuptext}%

  1292 \isamarkuptrue%

  1293 \isacommand{typedef}\isamarkupfalse%

  1294 \ three\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1295 %

  1296 \isadelimproof

  1297 \ \ %

  1298 \endisadelimproof

  1299 %

  1300 \isatagproof

  1301 \isacommand{by}\isamarkupfalse%

  1302 \ blast%

  1303 \endisatagproof

  1304 {\isafoldproof}%

  1305 %

  1306 \isadelimproof

  1307 \isanewline

  1308 %

  1309 \endisadelimproof

  1310 \isanewline

  1311 \isacommand{definition}\isamarkupfalse%

  1312 \ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1313 \isacommand{definition}\isamarkupfalse%

  1314 \ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1315 \isacommand{definition}\isamarkupfalse%

  1316 \ {\isaliteral{22}{\isachardoublequoteopen}}Three\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1317 \isanewline

  1318 \isacommand{lemma}\isamarkupfalse%

  1319 \ three{\isaliteral{5F}{\isacharunderscore}}distinct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1320 %

  1321 \isadelimproof

  1322 \ \ %

  1323 \endisadelimproof

  1324 %

  1325 \isatagproof

  1326 \isacommand{by}\isamarkupfalse%

  1327 \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%

  1328 \endisatagproof

  1329 {\isafoldproof}%

  1330 %

  1331 \isadelimproof

  1332 \isanewline

  1333 %

  1334 \endisadelimproof

  1335 \isanewline

  1336 \isacommand{lemma}\isamarkupfalse%

  1337 \ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\isanewline

  1338 \ \ \isakeyword{fixes}\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{obtains}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1339 %

  1340 \isadelimproof

  1341 \ \ %

  1342 \endisadelimproof

  1343 %

  1344 \isatagproof

  1345 \isacommand{by}\isamarkupfalse%

  1346 \ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%

  1347 \endisatagproof

  1348 {\isafoldproof}%

  1349 %

  1350 \isadelimproof

  1351 %

  1352 \endisadelimproof

  1353 %

  1354 \begin{isamarkuptext}%

  1355 Note that such trivial constructions are better done with

  1356   derived specification mechanisms such as \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}:%

  1357 \end{isamarkuptext}%

  1358 \isamarkuptrue%

  1359 \isacommand{datatype}\isamarkupfalse%

  1360 \ three{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Two{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Three{\isaliteral{27}{\isacharprime}}%

  1361 \begin{isamarkuptext}%

  1362 This avoids re-doing basic definitions and proofs from the

  1363   primitive \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} above.%

  1364 \end{isamarkuptext}%

  1365 \isamarkuptrue%

  1366 %

  1367 \isamarkupsection{Functorial structure of types%

  1368 }

  1369 \isamarkuptrue%

  1370 %

  1371 \begin{isamarkuptext}%

  1372 \begin{matharray}{rcl}

  1373     \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}

  1374   \end{matharray}

  1376   \begin{railoutput}

  1377 \rail@begin{2}{}

  1378 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]

  1379 \rail@bar

  1380 \rail@nextbar{1}

  1381 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1382 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1383 \rail@endbar

  1384 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1385 \rail@end

  1386 \end{railoutput}

  1389   \begin{description}

  1391   \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to

  1392   prove and register properties about the functorial structure of type

  1393   constructors.  These properties then can be used by other packages

  1394   to deal with those type constructors in certain type constructions.

  1395   Characteristic theorems are noted in the current local theory.  By

  1396   default, they are prefixed with the base name of the type

  1397   constructor, an explicit prefix can be given alternatively.

  1399   The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the

  1400   corresponding type constructor and must conform to the following

  1401   type pattern:

  1403   \begin{matharray}{lll}

  1404     \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &

  1405       \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\

  1406   \end{matharray}

  1408   \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct

  1409   type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}},

  1410   \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots,

  1411   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}.

  1413   \end{description}%

  1414 \end{isamarkuptext}%

  1415 \isamarkuptrue%

  1416 %

  1417 \isamarkupsection{Arithmetic proof support%

  1418 }

  1419 \isamarkuptrue%

  1420 %

  1421 \begin{isamarkuptext}%

  1422 \begin{matharray}{rcl}

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

  1424     \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\

  1425     \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\

  1426   \end{matharray}

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

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

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

  1432   The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are

  1433   always supplied to the arithmetic provers implicitly.

  1435   The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split

  1436   rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.

  1438   Note that a simpler (but faster) arithmetic prover is

  1439   already invoked by the Simplifier.%

  1440 \end{isamarkuptext}%

  1441 \isamarkuptrue%

  1442 %

  1443 \isamarkupsection{Intuitionistic proof search%

  1444 }

  1445 \isamarkuptrue%

  1446 %

  1447 \begin{isamarkuptext}%

  1448 \begin{matharray}{rcl}

  1449     \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\

  1450   \end{matharray}

  1452   \begin{railoutput}

  1453 \rail@begin{2}{}

  1454 \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]

  1455 \rail@plus

  1456 \rail@nextplus{1}

  1457 \rail@cnont{\hyperlink{syntax.rulemod}{\mbox{\isa{rulemod}}}}[]

  1458 \rail@endplus

  1459 \rail@end

  1460 \end{railoutput}

  1463   The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof

  1464   search, depending on specifically declared rules from the context,

  1465   or given as explicit arguments.  Chained facts are inserted into the

  1466   goal before commencing proof search.

  1468   Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},

  1469   \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the

  1470   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be

  1471   applied aggressively (without considering back-tracking later).

  1472   Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the

  1473   single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these).  An

  1474   explicit weight annotation may be given as well; otherwise the

  1475   number of rule premises will be taken into account here.%

  1476 \end{isamarkuptext}%

  1477 \isamarkuptrue%

  1478 %

  1479 \isamarkupsection{Coherent Logic%

  1480 }

  1481 \isamarkuptrue%

  1482 %

  1483 \begin{isamarkuptext}%

  1484 \begin{matharray}{rcl}

  1485     \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\

  1486   \end{matharray}

  1488   \begin{railoutput}

  1489 \rail@begin{2}{}

  1490 \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]

  1491 \rail@bar

  1492 \rail@nextbar{1}

  1493 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

  1494 \rail@endbar

  1495 \rail@end

  1496 \end{railoutput}

  1499   The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of

  1500   \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers

  1501   applications in confluence theory, lattice theory and projective

  1502   geometry.  See \verb|~~/src/HOL/ex/Coherent.thy| for some

  1503   examples.%

  1504 \end{isamarkuptext}%

  1505 \isamarkuptrue%

  1506 %

  1507 \isamarkupsection{Proving propositions%

  1508 }

  1509 \isamarkuptrue%

  1510 %

  1511 \begin{isamarkuptext}%

  1512 In addition to the standard proof methods, a number of diagnosis

  1513   tools search for proofs and provide an Isar proof snippet on success.

  1514   These tools are available via the following commands.

  1516   \begin{matharray}{rcl}

  1517     \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1518     \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1519     \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1520     \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}

  1521   \end{matharray}

  1523   \begin{railoutput}

  1524 \rail@begin{6}{}

  1525 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]

  1526 \rail@bar

  1527 \rail@nextbar{1}

  1528 \rail@plus

  1529 \rail@bar

  1530 \rail@term{\isa{simp}}[]

  1531 \rail@nextbar{2}

  1532 \rail@term{\isa{intro}}[]

  1533 \rail@nextbar{3}

  1534 \rail@term{\isa{elim}}[]

  1535 \rail@nextbar{4}

  1536 \rail@term{\isa{dest}}[]

  1537 \rail@endbar

  1538 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1539 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

  1540 \rail@nextplus{5}

  1541 \rail@endplus

  1542 \rail@endbar

  1543 \rail@bar

  1544 \rail@nextbar{1}

  1545 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  1546 \rail@endbar

  1547 \rail@end

  1548 \rail@begin{2}{}

  1549 \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]

  1550 \rail@bar

  1551 \rail@nextbar{1}

  1552 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1553 \rail@nont{\isa{args}}[]

  1554 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1555 \rail@endbar

  1556 \rail@bar

  1557 \rail@nextbar{1}

  1558 \rail@nont{\isa{facts}}[]

  1559 \rail@endbar

  1560 \rail@bar

  1561 \rail@nextbar{1}

  1562 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  1563 \rail@endbar

  1564 \rail@end

  1565 \rail@begin{2}{}

  1566 \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]

  1567 \rail@bar

  1568 \rail@nextbar{1}

  1569 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1570 \rail@nont{\isa{args}}[]

  1571 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1572 \rail@endbar

  1573 \rail@end

  1574 \rail@begin{2}{\isa{args}}

  1575 \rail@plus

  1576 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1577 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1578 \rail@nont{\isa{value}}[]

  1579 \rail@nextplus{1}

  1580 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]

  1581 \rail@endplus

  1582 \rail@end

  1583 \rail@begin{5}{\isa{facts}}

  1584 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1585 \rail@bar

  1586 \rail@nextbar{1}

  1587 \rail@plus

  1588 \rail@bar

  1589 \rail@nextbar{2}

  1590 \rail@bar

  1591 \rail@term{\isa{add}}[]

  1592 \rail@nextbar{3}

  1593 \rail@term{\isa{del}}[]

  1594 \rail@endbar

  1595 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1596 \rail@endbar

  1597 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

  1598 \rail@nextplus{4}

  1599 \rail@endplus

  1600 \rail@endbar

  1601 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1602 \rail@end

  1603 \end{railoutput}

  1604  % FIXME try: proper clasimpmod!?

  1605   % FIXME check args "value"

  1607   \begin{description}

  1609   \item \hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}} checks whether the current subgoals can

  1610     be solved directly by an existing theorem. Duplicate lemmas can be detected

  1611     in this way.

  1613   \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove a subgoal using a combination

  1614     of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.).

  1615     Additional facts supplied via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}},

  1616     \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof

  1617     methods.

  1619   \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external

  1620     automatic provers (resolution provers and SMT solvers). See the Sledgehammer

  1621     manual \cite{isabelle-sledgehammer} for details.

  1623   \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes

  1624     \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} configuration options persistently.

  1626   \end{description}%

  1627 \end{isamarkuptext}%

  1628 \isamarkuptrue%

  1629 %

  1630 \isamarkupsection{Checking and refuting propositions%

  1631 }

  1632 \isamarkuptrue%

  1633 %

  1634 \begin{isamarkuptext}%

  1635 Identifying incorrect propositions usually involves evaluation of

  1636   particular assignments and systematic counterexample search.  This

  1637   is supported by the following commands.

  1639   \begin{matharray}{rcl}

  1640     \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1641     \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1642     \indexdef{HOL}{command}{refute}\hypertarget{command.HOL.refute}{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1643     \indexdef{HOL}{command}{nitpick}\hypertarget{command.HOL.nitpick}{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1644     \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1645     \indexdef{HOL}{command}{refute\_params}\hypertarget{command.HOL.refute-params}{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1646     \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}

  1647   \end{matharray}

  1649   \begin{railoutput}

  1650 \rail@begin{2}{}

  1651 \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]

  1652 \rail@bar

  1653 \rail@nextbar{1}

  1654 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1655 \rail@nont{\isa{name}}[]

  1656 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1657 \rail@endbar

  1658 \rail@bar

  1659 \rail@nextbar{1}

  1660 \rail@nont{\isa{modes}}[]

  1661 \rail@endbar

  1662 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1663 \rail@end

  1664 \rail@begin{3}{}

  1665 \rail@bar

  1666 \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]

  1667 \rail@nextbar{1}

  1668 \rail@term{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}[]

  1669 \rail@nextbar{2}

  1670 \rail@term{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}[]

  1671 \rail@endbar

  1672 \rail@bar

  1673 \rail@nextbar{1}

  1674 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1675 \rail@nont{\isa{args}}[]

  1676 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1677 \rail@endbar

  1678 \rail@bar

  1679 \rail@nextbar{1}

  1680 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  1681 \rail@endbar

  1682 \rail@end

  1683 \rail@begin{3}{}

  1684 \rail@bar

  1685 \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]

  1686 \rail@nextbar{1}

  1687 \rail@term{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]

  1688 \rail@nextbar{2}

  1689 \rail@term{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]

  1690 \rail@endbar

  1691 \rail@bar

  1692 \rail@nextbar{1}

  1693 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]

  1694 \rail@nont{\isa{args}}[]

  1695 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]

  1696 \rail@endbar

  1697 \rail@end

  1698 \rail@begin{2}{\isa{modes}}

  1699 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1700 \rail@plus

  1701 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1702 \rail@nextplus{1}

  1703 \rail@endplus

  1704 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1705 \rail@end

  1706 \rail@begin{2}{\isa{args}}

  1707 \rail@plus

  1708 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1709 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1710 \rail@nont{\isa{value}}[]

  1711 \rail@nextplus{1}

  1712 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]

  1713 \rail@endplus

  1714 \rail@end

  1715 \end{railoutput}

  1716  % FIXME check "value"

  1718   \begin{description}

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

  1721     term; optionally \isa{modes} can be specified, which are

  1722     appended to the current print mode (see also \cite{isabelle-ref}).

  1723     Internally, the evaluation is performed by registered evaluators,

  1724     which are invoked sequentially until a result is returned.

  1725     Alternatively a specific evaluator can be selected using square

  1726     brackets; typical evaluators use the current set of code equations

  1727     to normalize and include \isa{simp} for fully symbolic evaluation

  1728     using the simplifier, \isa{nbe} for \emph{normalization by evaluation}

  1729     and \emph{code} for code generation in SML.

  1731   \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for

  1732     counterexamples using a series of assignments for its

  1733     free variables; by default the first subgoal is tested, an other

  1734     can be selected explicitly using an optional goal index.

  1735     Assignments can be chosen exhausting the search space upto a given

  1736     size or using a fixed number of random assignments in the search space.

  1737     By default, quickcheck uses exhaustive testing.

  1738     A number of configuration options are supported for

  1739     \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:

  1741     \begin{description}

  1743     \item[\isa{tester}] specifies how to explore the search space

  1744       (e.g. exhaustive or random).

  1745       An unknown configuration option is treated as an argument to tester,

  1746       making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.

  1747     \item[\isa{size}] specifies the maximum size of the search space

  1748     for assignment values.

  1750     \item[\isa{eval}] takes a term or a list of terms and evaluates

  1751       these terms under the variable assignment found by quickcheck.

  1753     \item[\isa{iterations}] sets how many sets of assignments are

  1754     generated for each particular size.

  1756     \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in

  1757     structured proofs should be ignored.

  1759     \item[\isa{timeout}] sets the time limit in seconds.

  1761     \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to

  1762     instantiate type variables.

  1764     \item[\isa{report}] if set quickcheck reports how many tests

  1765     fulfilled the preconditions.

  1767     \item[\isa{quiet}] if not set quickcheck informs about the

  1768     current size for assignment values.

  1770     \item[\isa{expect}] can be used to check if the user's

  1771     expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}).

  1773     \end{description}

  1775     These option can be given within square brackets.

  1777   \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes

  1778     \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.

  1780   \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for

  1781     counterexamples using a reduction to SAT. The following configuration

  1782     options are supported:

  1784     \begin{description}

  1786     \item[\isa{minsize}] specifies the minimum size (cardinality) of the

  1787       models to search for.

  1789     \item[\isa{maxsize}] specifies the maximum size (cardinality) of the

  1790       models to search for. Nonpositive values mean $\infty$.

  1792     \item[\isa{maxvars}] specifies the maximum number of Boolean variables

  1793     to use when transforming the term into a propositional formula.

  1794     Nonpositive values mean $\infty$.

  1796     \item[\isa{satsolver}] specifies the SAT solver to use.

  1798     \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in

  1799     structured proofs should be ignored.

  1801     \item[\isa{maxtime}] sets the time limit in seconds.

  1803     \item[\isa{expect}] can be used to check if the user's

  1804     expectation was met (\isa{genuine}, \isa{potential},

  1805     \isa{none}, or \isa{unknown}).

  1807     \end{description}

  1809     These option can be given within square brackets.

  1811   \item \hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}} changes

  1812     \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} configuration options persistently.

  1814   \item \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} tests the current goal for counterexamples

  1815     using a reduction to first-order relational logic. See the Nitpick manual

  1816     \cite{isabelle-nitpick} for details.

  1818   \item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes

  1819     \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.

  1821   \end{description}%

  1822 \end{isamarkuptext}%

  1823 \isamarkuptrue%

  1824 %

  1825 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%

  1826 }

  1827 \isamarkuptrue%

  1828 %

  1829 \begin{isamarkuptext}%

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

  1831   induction in unstructured tactic scripts; see also

  1832   \secref{sec:cases-induct} for proper Isar versions of similar ideas.

  1834   \begin{matharray}{rcl}

  1835     \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\

  1836     \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\

  1837     \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\

  1838     \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1839   \end{matharray}

  1841   \begin{railoutput}

  1842 \rail@begin{2}{}

  1843 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]

  1844 \rail@bar

  1845 \rail@nextbar{1}

  1846 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]

  1847 \rail@endbar

  1848 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1849 \rail@bar

  1850 \rail@nextbar{1}

  1851 \rail@nont{\isa{rule}}[]

  1852 \rail@endbar

  1853 \rail@end

  1854 \rail@begin{3}{}

  1855 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]

  1856 \rail@bar

  1857 \rail@nextbar{1}

  1858 \rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]

  1859 \rail@endbar

  1860 \rail@bar

  1861 \rail@nextbar{1}

  1862 \rail@plus

  1863 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]

  1864 \rail@nextplus{2}

  1865 \rail@cterm{\isa{\isakeyword{and}}}[]

  1866 \rail@endplus

  1867 \rail@endbar

  1868 \rail@bar

  1869 \rail@nextbar{1}

  1870 \rail@nont{\isa{rule}}[]

  1871 \rail@endbar

  1872 \rail@end

  1873 \rail@begin{3}{}

  1874 \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]

  1875 \rail@plus

  1876 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  1877 \rail@nextplus{1}

  1878 \rail@endplus

  1879 \rail@bar

  1880 \rail@nextbar{1}

  1881 \rail@term{\isa{\isakeyword{for}}}[]

  1882 \rail@plus

  1883 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1884 \rail@nextplus{2}

  1885 \rail@endplus

  1886 \rail@endbar

  1887 \rail@end

  1888 \rail@begin{3}{}

  1889 \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]

  1890 \rail@plus

  1891 \rail@bar

  1892 \rail@nextbar{1}

  1893 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

  1894 \rail@endbar

  1895 \rail@plus

  1896 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  1897 \rail@nextplus{1}

  1898 \rail@endplus

  1899 \rail@nextplus{2}

  1900 \rail@cterm{\isa{\isakeyword{and}}}[]

  1901 \rail@endplus

  1902 \rail@end

  1903 \rail@begin{1}{\isa{rule}}

  1904 \rail@term{\isa{rule}}[]

  1905 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  1906 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]

  1907 \rail@end

  1908 \end{railoutput}

  1911   \begin{description}

  1913   \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} admit

  1914   to reason about inductive types.  Rules are selected according to

  1915   the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}

  1916   attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.

  1918   These unstructured tactics feature both goal addressing and dynamic

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

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

  1921   methods (see \secref{sec:cases-induct}).  Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} does not handle structured rule

  1922   statements, only the compact object-logic conclusion of the subgoal

  1923   being addressed.

  1925   \item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted

  1926   forward manner.

  1928   While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} is a proof method to apply the

  1929   result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provides case split theorems at the theory level

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

  1931   be generalized before applying the resulting rule.

  1933   \end{description}%

  1934 \end{isamarkuptext}%

  1935 \isamarkuptrue%

  1936 %

  1937 \isamarkupsection{Executable code%

  1938 }

  1939 \isamarkuptrue%

  1940 %

  1941 \begin{isamarkuptext}%

  1942 For validation purposes, it is often useful to \emph{execute}

  1943   specifications.  In principle, execution could be simulated by

  1944   Isabelle's inference kernel, i.e. by a combination of resolution and

  1945   simplification.  Unfortunately, this approach is rather inefficient.

  1946   A more efficient way of executing specifications is to translate

  1947   them into a functional programming language such as ML.

  1949   Isabelle provides two generic frameworks to support code generation

  1950   from executable specifications.  Isabelle/HOL instantiates these

  1951   mechanisms in a way that is amenable to end-user applications.%

  1952 \end{isamarkuptext}%

  1953 \isamarkuptrue%

  1954 %

  1955 \isamarkupsubsection{The new code generator (F. Haftmann)%

  1956 }

  1957 \isamarkuptrue%

  1958 %

  1959 \begin{isamarkuptext}%

  1960 This framework generates code from functional programs

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

  1962   \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala

  1963   \cite{scala-overview-tech-report}.  Conceptually, code generation is

  1964   split up in three steps: \emph{selection} of code theorems,

  1965   \emph{translation} into an abstract executable view and

  1966   \emph{serialization} to a specific \emph{target language}.

  1967   Inductive specifications can be executed using the predicate

  1968   compiler which operates within HOL.  See \cite{isabelle-codegen} for

  1969   an introduction.

  1971   \begin{matharray}{rcl}

  1972     \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

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

  1974     \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1975     \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1976     \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1977     \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}} & : & \isa{attribute} \\

  1978     \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\

  1979     \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1980     \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1981     \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1982     \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1983     \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1984     \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1985     \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1986     \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1987     \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1988     \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1989     \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1990     \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}

  1991   \end{matharray}

  1993   \begin{railoutput}

  1994 \rail@begin{11}{}

  1995 \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]

  1996 \rail@plus

  1997 \rail@nont{\isa{constexpr}}[]

  1998 \rail@nextplus{1}

  1999 \rail@endplus

  2000 \rail@cr{3}

  2001 \rail@bar

  2002 \rail@nextbar{4}

  2003 \rail@plus

  2004 \rail@term{\isa{\isakeyword{in}}}[]

  2005 \rail@nont{\isa{target}}[]

  2006 \rail@bar

  2007 \rail@nextbar{5}

  2008 \rail@term{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}[]

  2009 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2010 \rail@endbar

  2011 \rail@cr{7}

  2012 \rail@bar

  2013 \rail@nextbar{8}

  2014 \rail@term{\isa{\isakeyword{file}}}[]

  2015 \rail@bar

  2016 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2017 \rail@nextbar{9}

  2018 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

  2019 \rail@endbar

  2020 \rail@endbar

  2021 \rail@bar

  2022 \rail@nextbar{8}

  2023 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2024 \rail@nont{\isa{args}}[]

  2025 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2026 \rail@endbar

  2027 \rail@nextplus{10}

  2028 \rail@endplus

  2029 \rail@endbar

  2030 \rail@end

  2031 \rail@begin{1}{\isa{const}}

  2032 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2033 \rail@end

  2034 \rail@begin{3}{\isa{constexpr}}

  2035 \rail@bar

  2036 \rail@nont{\isa{const}}[]

  2037 \rail@nextbar{1}

  2038 \rail@term{\isa{name{\isaliteral{2E}{\isachardot}}{\isaliteral{5F}{\isacharunderscore}}}}[]

  2039 \rail@nextbar{2}

  2040 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]

  2041 \rail@endbar

  2042 \rail@end

  2043 \rail@begin{1}{\isa{typeconstructor}}

  2044 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  2045 \rail@end

  2046 \rail@begin{1}{\isa{class}}

  2047 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  2048 \rail@end

  2049 \rail@begin{4}{\isa{target}}

  2050 \rail@bar

  2051 \rail@term{\isa{SML}}[]

  2052 \rail@nextbar{1}

  2053 \rail@term{\isa{OCaml}}[]

  2054 \rail@nextbar{2}

  2055 \rail@term{\isa{Haskell}}[]

  2056 \rail@nextbar{3}

  2057 \rail@term{\isa{Scala}}[]

  2058 \rail@endbar

  2059 \rail@end

  2060 \rail@begin{4}{}

  2061 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]

  2062 \rail@bar

  2063 \rail@nextbar{1}

  2064 \rail@bar

  2065 \rail@term{\isa{del}}[]

  2066 \rail@nextbar{2}

  2067 \rail@term{\isa{abstype}}[]

  2068 \rail@nextbar{3}

  2069 \rail@term{\isa{abstract}}[]

  2070 \rail@endbar

  2071 \rail@endbar

  2072 \rail@end

  2073 \rail@begin{2}{}

  2074 \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]

  2075 \rail@plus

  2076 \rail@nont{\isa{const}}[]

  2077 \rail@nextplus{1}

  2078 \rail@endplus

  2079 \rail@end

  2080 \rail@begin{2}{}

  2081 \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]

  2082 \rail@plus

  2083 \rail@nont{\isa{const}}[]

  2084 \rail@nextplus{1}

  2085 \rail@endplus

  2086 \rail@end

  2087 \rail@begin{2}{}

  2088 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]

  2089 \rail@bar

  2090 \rail@nextbar{1}

  2091 \rail@term{\isa{del}}[]

  2092 \rail@endbar

  2093 \rail@end

  2094 \rail@begin{2}{}

  2095 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]

  2096 \rail@bar

  2097 \rail@nextbar{1}

  2098 \rail@term{\isa{del}}[]

  2099 \rail@endbar

  2100 \rail@end

  2101 \rail@begin{3}{}

  2102 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]

  2103 \rail@bar

  2104 \rail@nextbar{1}

  2105 \rail@plus

  2106 \rail@nont{\isa{constexpr}}[]

  2107 \rail@nextplus{2}

  2108 \rail@endplus

  2109 \rail@endbar

  2110 \rail@end

  2111 \rail@begin{3}{}

  2112 \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]

  2113 \rail@bar

  2114 \rail@nextbar{1}

  2115 \rail@plus

  2116 \rail@nont{\isa{constexpr}}[]

  2117 \rail@nextplus{2}

  2118 \rail@endplus

  2119 \rail@endbar

  2120 \rail@end

  2121 \rail@begin{7}{}

  2122 \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]

  2123 \rail@plus

  2124 \rail@nont{\isa{const}}[]

  2125 \rail@nextplus{1}

  2126 \rail@cterm{\isa{\isakeyword{and}}}[]

  2127 \rail@endplus

  2128 \rail@cr{3}

  2129 \rail@plus

  2130 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2131 \rail@nont{\isa{target}}[]

  2132 \rail@plus

  2133 \rail@bar

  2134 \rail@nextbar{4}

  2135 \rail@nont{\isa{syntax}}[]

  2136 \rail@endbar

  2137 \rail@nextplus{5}

  2138 \rail@cterm{\isa{\isakeyword{and}}}[]

  2139 \rail@endplus

  2140 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2141 \rail@nextplus{6}

  2142 \rail@endplus

  2143 \rail@end

  2144 \rail@begin{7}{}

  2145 \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]

  2146 \rail@plus

  2147 \rail@nont{\isa{typeconstructor}}[]

  2148 \rail@nextplus{1}

  2149 \rail@cterm{\isa{\isakeyword{and}}}[]

  2150 \rail@endplus

  2151 \rail@cr{3}

  2152 \rail@plus

  2153 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2154 \rail@nont{\isa{target}}[]

  2155 \rail@plus

  2156 \rail@bar

  2157 \rail@nextbar{4}

  2158 \rail@nont{\isa{syntax}}[]

  2159 \rail@endbar

  2160 \rail@nextplus{5}

  2161 \rail@cterm{\isa{\isakeyword{and}}}[]

  2162 \rail@endplus

  2163 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2164 \rail@nextplus{6}

  2165 \rail@endplus

  2166 \rail@end

  2167 \rail@begin{9}{}

  2168 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]

  2169 \rail@plus

  2170 \rail@nont{\isa{class}}[]

  2171 \rail@nextplus{1}

  2172 \rail@cterm{\isa{\isakeyword{and}}}[]

  2173 \rail@endplus

  2174 \rail@cr{3}

  2175 \rail@plus

  2176 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2177 \rail@nont{\isa{target}}[]

  2178 \rail@cr{5}

  2179 \rail@plus

  2180 \rail@bar

  2181 \rail@nextbar{6}

  2182 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2183 \rail@endbar

  2184 \rail@nextplus{7}

  2185 \rail@cterm{\isa{\isakeyword{and}}}[]

  2186 \rail@endplus

  2187 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2188 \rail@nextplus{8}

  2189 \rail@endplus

  2190 \rail@end

  2191 \rail@begin{7}{}

  2192 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]

  2193 \rail@plus

  2194 \rail@nont{\isa{typeconstructor}}[]

  2195 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  2196 \rail@nont{\isa{class}}[]

  2197 \rail@nextplus{1}

  2198 \rail@cterm{\isa{\isakeyword{and}}}[]

  2199 \rail@endplus

  2200 \rail@cr{3}

  2201 \rail@plus

  2202 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2203 \rail@nont{\isa{target}}[]

  2204 \rail@plus

  2205 \rail@bar

  2206 \rail@nextbar{4}

  2207 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

  2208 \rail@endbar

  2209 \rail@nextplus{5}

  2210 \rail@cterm{\isa{\isakeyword{and}}}[]

  2211 \rail@endplus

  2212 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2213 \rail@nextplus{6}

  2214 \rail@endplus

  2215 \rail@end

  2216 \rail@begin{2}{}

  2217 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]

  2218 \rail@nont{\isa{target}}[]

  2219 \rail@plus

  2220 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2221 \rail@nextplus{1}

  2222 \rail@endplus

  2223 \rail@end

  2224 \rail@begin{1}{}

  2225 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]

  2226 \rail@nont{\isa{const}}[]

  2227 \rail@nont{\isa{const}}[]

  2228 \rail@nont{\isa{target}}[]

  2229 \rail@end

  2230 \rail@begin{2}{}

  2231 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]

  2232 \rail@nont{\isa{target}}[]

  2233 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2234 \rail@bar

  2235 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2236 \rail@nextbar{1}

  2237 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

  2238 \rail@endbar

  2239 \rail@end

  2240 \rail@begin{2}{}

  2241 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]

  2242 \rail@nont{\isa{target}}[]

  2243 \rail@plus

  2244 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2245 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2246 \rail@nextplus{1}

  2247 \rail@endplus

  2248 \rail@end

  2249 \rail@begin{11}{}

  2250 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]

  2251 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2252 \rail@cr{2}

  2253 \rail@bar

  2254 \rail@nextbar{3}

  2255 \rail@term{\isa{\isakeyword{datatypes}}}[]

  2256 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2257 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  2258 \rail@bar

  2259 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]

  2260 \rail@nextbar{4}

  2261 \rail@plus

  2262 \rail@plus

  2263 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2264 \rail@nextplus{5}

  2265 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]

  2266 \rail@endplus

  2267 \rail@nextplus{6}

  2268 \rail@cterm{\isa{\isakeyword{and}}}[]

  2269 \rail@endplus

  2270 \rail@endbar

  2271 \rail@endbar

  2272 \rail@cr{8}

  2273 \rail@bar

  2274 \rail@nextbar{9}

  2275 \rail@term{\isa{\isakeyword{functions}}}[]

  2276 \rail@plus

  2277 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2278 \rail@nextplus{10}

  2279 \rail@endplus

  2280 \rail@endbar

  2281 \rail@bar

  2282 \rail@nextbar{9}

  2283 \rail@term{\isa{\isakeyword{file}}}[]

  2284 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2285 \rail@endbar

  2286 \rail@end

  2287 \rail@begin{4}{\isa{syntax}}

  2288 \rail@bar

  2289 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2290 \rail@nextbar{1}

  2291 \rail@bar

  2292 \rail@term{\isa{\isakeyword{infix}}}[]

  2293 \rail@nextbar{2}

  2294 \rail@term{\isa{\isakeyword{infixl}}}[]

  2295 \rail@nextbar{3}

  2296 \rail@term{\isa{\isakeyword{infixr}}}[]

  2297 \rail@endbar

  2298 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  2299 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2300 \rail@endbar

  2301 \rail@end

  2302 \end{railoutput}

  2305   \begin{description}

  2307   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} generates code for a given list

  2308   of constants in the specified target language(s).  If no

  2309   serialization instruction is given, only abstract code is generated

  2310   internally.

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

  2313   all executable contants within a certain theory by giving \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, or referring to \emph{all} executable constants currently

  2314   available by giving \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.

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

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

  2318   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} keyword; then \emph{all} code is

  2319   placed in this module.

  2321   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

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

  2323   directory, where code is generated in multiple files reflecting the

  2324   module hierarchy.  Omitting the file specification denotes standard

  2325   output.

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

  2328   \emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits

  2329   explicit module signatures.

  2331   For \emph{Haskell} a module name prefix may be given using the

  2332   ``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a

  2333   ``\verb|deriving (Read, Show)|'' clause to each appropriate

  2334   datatype declaration.

  2336   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option

  2337   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' deselects) a code equation for code generation.

  2338   Usually packages introducing code equations provide a reasonable

  2339   default setup for selection.  Variants \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstype{\isaliteral{22}{\isachardoublequote}}} and

  2340   \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstract{\isaliteral{22}{\isachardoublequote}}} declare abstract datatype certificates or

  2341   code equations on abstract datatype representations respectively.

  2343   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}} declares constants which are not

  2344   required to have a definition by means of code equations; if needed

  2345   these are implemented by program abort instead.

  2347   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}} specifies a constructor set

  2348   for a logical type.

  2350   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on

  2351   selected code equations and code generator datatypes.

  2353   \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option

  2354   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as

  2355   rewrite rules to any code equation during preprocessing.

  2357   \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}} declares (or with option ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as rewrite rules to any

  2358   result of an evaluation.

  2360   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code

  2361   generator preprocessor.

  2363   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}} prints a list of theorems

  2364   representing the corresponding program containing all given

  2365   constants after preprocessing.

  2367   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes dependencies of

  2368   theorems representing the corresponding program containing all given

  2369   constants after preprocessing.

  2371   \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}} associates a list of constants

  2372   with target-specific serializations; omitting a serialization

  2373   deletes an existing serialization.

  2375   \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}} associates a list of type

  2376   constructors with target-specific serializations; omitting a

  2377   serialization deletes an existing serialization.

  2379   \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}} associates a list of classes

  2380   with target-specific class names; omitting a serialization deletes

  2381   an existing serialization.  This applies only to \emph{Haskell}.

  2383   \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}} declares a list of type

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

  2385   given target.  Omitting a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' deletes an existing

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

  2387   \emph{Haskell}.

  2389   \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}} declares a list of names as

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

  2391   generated code.

  2393   \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}} provides an auxiliary mechanism

  2394   to generate monadic code for Haskell.

  2396   \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}} adds arbitrary named content

  2397   (``include'') to generated code.  A ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' as last argument

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

  2400   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}} declares aliasings from one

  2401   module name onto another.

  2403   \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} without a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}''

  2404   argument compiles code into the system runtime environment and

  2405   modifies the code generator setup that future invocations of system

  2406   runtime code generation referring to one of the ``\isa{{\isaliteral{22}{\isachardoublequote}}datatypes{\isaliteral{22}{\isachardoublequote}}}'' or ``\isa{{\isaliteral{22}{\isachardoublequote}}functions{\isaliteral{22}{\isachardoublequote}}}'' entities use these precompiled

  2407   entities.  With a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}'' argument, the corresponding code

  2408   is generated into that specified file without modifying the code

  2409   generator setup.

  2411   \end{description}%

  2412 \end{isamarkuptext}%

  2413 \isamarkuptrue%

  2414 %

  2415 \isamarkupsubsection{The old code generator (S. Berghofer)%

  2416 }

  2417 \isamarkuptrue%

  2418 %

  2419 \begin{isamarkuptext}%

  2420 This framework generates code from both functional and

  2421   relational programs to SML, as explained below.

  2423   \begin{matharray}{rcl}

  2424     \indexdef{}{command}{code\_module}\hypertarget{command.code-module}{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  2425     \indexdef{}{command}{code\_library}\hypertarget{command.code-library}{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  2426     \indexdef{}{command}{consts\_code}\hypertarget{command.consts-code}{\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  2427     \indexdef{}{command}{types\_code}\hypertarget{command.types-code}{\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  2428     \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\

  2429   \end{matharray}

  2431   \begin{railoutput}

  2432 \rail@begin{11}{}

  2433 \rail@bar

  2434 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]

  2435 \rail@nextbar{1}

  2436 \rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]

  2437 \rail@endbar

  2438 \rail@bar

  2439 \rail@nextbar{1}

  2440 \rail@nont{\isa{modespec}}[]

  2441 \rail@endbar

  2442 \rail@bar

  2443 \rail@nextbar{1}

  2444 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2445 \rail@endbar

  2446 \rail@cr{3}

  2447 \rail@bar

  2448 \rail@nextbar{4}

  2449 \rail@term{\isa{\isakeyword{file}}}[]

  2450 \rail@nont{\isa{name}}[]

  2451 \rail@endbar

  2452 \rail@bar

  2453 \rail@nextbar{4}

  2454 \rail@term{\isa{\isakeyword{imports}}}[]

  2455 \rail@plus

  2456 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2457 \rail@nextplus{5}

  2458 \rail@endplus

  2459 \rail@endbar

  2460 \rail@cr{7}

  2461 \rail@term{\isa{\isakeyword{contains}}}[]

  2462 \rail@bar

  2463 \rail@plus

  2464 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2465 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  2466 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2467 \rail@nextplus{8}

  2468 \rail@endplus

  2469 \rail@nextbar{9}

  2470 \rail@plus

  2471 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2472 \rail@nextplus{10}

  2473 \rail@endplus

  2474 \rail@endbar

  2475 \rail@end

  2476 \rail@begin{2}{\isa{modespec}}

  2477 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2478 \rail@plus

  2479 \rail@nextplus{1}

  2480 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2481 \rail@endplus

  2482 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2483 \rail@end

  2484 \rail@begin{2}{}

  2485 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]

  2486 \rail@plus

  2487 \rail@nont{\isa{codespec}}[]

  2488 \rail@nextplus{1}

  2489 \rail@endplus

  2490 \rail@end

  2491 \rail@begin{2}{\isa{codespec}}

  2492 \rail@nont{\isa{const}}[]

  2493 \rail@nont{\isa{template}}[]

  2494 \rail@bar

  2495 \rail@nextbar{1}

  2496 \rail@nont{\isa{attachment}}[]

  2497 \rail@endbar

  2498 \rail@end

  2499 \rail@begin{2}{}

  2500 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]

  2501 \rail@plus

  2502 \rail@nont{\isa{tycodespec}}[]

  2503 \rail@nextplus{1}

  2504 \rail@endplus

  2505 \rail@end

  2506 \rail@begin{2}{\isa{tycodespec}}

  2507 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2508 \rail@nont{\isa{template}}[]

  2509 \rail@bar

  2510 \rail@nextbar{1}

  2511 \rail@nont{\isa{attachment}}[]

  2512 \rail@endbar

  2513 \rail@end

  2514 \rail@begin{1}{\isa{const}}

  2515 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2516 \rail@end

  2517 \rail@begin{1}{\isa{template}}

  2518 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2519 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2520 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2521 \rail@end

  2522 \rail@begin{2}{\isa{attachment}}

  2523 \rail@term{\isa{attach}}[]

  2524 \rail@bar

  2525 \rail@nextbar{1}

  2526 \rail@nont{\isa{modespec}}[]

  2527 \rail@endbar

  2528 \rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]

  2529 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  2530 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]

  2531 \rail@end

  2532 \rail@begin{2}{}

  2533 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]

  2534 \rail@bar

  2535 \rail@nextbar{1}

  2536 \rail@nont{\isa{name}}[]

  2537 \rail@endbar

  2538 \rail@end

  2539 \end{railoutput}%

  2540 \end{isamarkuptext}%

  2541 \isamarkuptrue%

  2542 %

  2543 \isamarkupsubsubsection{Invoking the code generator%

  2544 }

  2545 \isamarkuptrue%

  2546 %

  2547 \begin{isamarkuptext}%

  2548 The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}

  2549   and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to

  2550   \emph{incremental} and \emph{modular} code generation, respectively.

  2552   \begin{description}

  2554   \item [Modular] For each theory, an ML structure is generated,

  2555   containing the code generated from the constants defined in this

  2556   theory.

  2558   \item [Incremental] All the generated code is emitted into the same

  2559   structure.  This structure may import code from previously generated

  2560   structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.

  2561   Moreover, the generated structure may also be referred to in later

  2562   invocations of the code generator.

  2564   \end{description}

  2566   After the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}} and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}

  2567   keywords, the user may specify an optional list of ``modes'' in

  2568   parentheses. These can be used to instruct the code generator to

  2569   emit additional code for special purposes, e.g.\ functions for

  2570   converting elements of generated datatypes to Isabelle terms, or

  2571   test data generators. The list of modes is followed by a module

  2572   name.  The module name is optional for modular code generation, but

  2573   must be specified for incremental code generation.

  2575   The code can either be written to a file, in which case a file name

  2576   has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded

  2577   directly into Isabelle's ML environment. In the latter case, the

  2578   \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results

  2579   interactively, for example.

  2581   The terms from which to generate code can be specified after the

  2582   \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just

  2583   as a list of terms. In the latter case, the code generator just

  2584   produces code for all constants and types occuring in the term, but

  2585   does not bind the compiled terms to ML identifiers.

  2587   Here is an example:%

  2588 \end{isamarkuptext}%

  2589 \isamarkuptrue%

  2590 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2591 \ Test\isanewline

  2592 \isakeyword{contains}\ test\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}foldl\ op\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%

  2593 \begin{isamarkuptext}%

  2594 \noindent This binds the result of compiling the given term to

  2595   the ML identifier \verb|Test.test|.%

  2596 \end{isamarkuptext}%

  2597 \isamarkuptrue%

  2598 %

  2599 \isadelimML

  2600 %

  2601 \endisadelimML

  2602 %

  2603 \isatagML

  2604 \isacommand{ML}\isamarkupfalse%

  2605 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2606 \isaantiq

  2607 assert{}%

  2608 \endisaantiq

  2609 \ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2610 \endisatagML

  2611 {\isafoldML}%

  2612 %

  2613 \isadelimML

  2614 %

  2615 \endisadelimML

  2616 %

  2617 \isamarkupsubsubsection{Configuring the code generator%

  2618 }

  2619 \isamarkuptrue%

  2620 %

  2621 \begin{isamarkuptext}%

  2622 When generating code for a complex term, the code generator

  2623   recursively calls itself for all subterms.  When it arrives at a

  2624   constant, the default strategy of the code generator is to look up

  2625   its definition and try to generate code for it.  Constants which

  2626   have no definitions that are immediately executable, may be

  2627   associated with a piece of ML code manually using the \indexref{}{command}{consts\_code}\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}} command.  It takes a list whose elements consist of a

  2628   constant (given in usual term syntax -- an explicit type constraint

  2629   accounts for overloading), and a mixfix template describing the ML

  2630   code. The latter is very much the same as the mixfix templates used

  2631   when declaring new constants.  The most notable difference is that

  2632   terms may be included in the ML template using antiquotation

  2633   brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.

  2635   A similar mechanism is available for types: \indexref{}{command}{types\_code}\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}} associates type constructors with specific ML code.

  2637   For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of

  2638   Isabelle/HOL should be compiled to ML.%

  2639 \end{isamarkuptext}%

  2640 \isamarkuptrue%

  2641 \isacommand{typedecl}\isamarkupfalse%

  2642 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline

  2643 \isacommand{consts}\isamarkupfalse%

  2644 \ Pair\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2645 \isanewline

  2646 \isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2647 \ prod\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2648 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2649 \ Pair\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%

  2650 \begin{isamarkuptext}%

  2651 Sometimes, the code associated with a constant or type may

  2652   need to refer to auxiliary functions, which have to be emitted when

  2653   the constant is used. Code for such auxiliary functions can be

  2654   declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}

  2655   function can be implemented as follows:%

  2656 \end{isamarkuptext}%

  2657 \isamarkuptrue%

  2658 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2659 \ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline

  2660 \isakeyword{attach}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ fun\ wfrec\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}wfrec\ f{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2661 \begin{isamarkuptext}%

  2662 If the code containing a call to \isa{wfrec} resides in an

  2663   ML structure different from the one containing the function

  2664   definition attached to \isa{wfrec}, the name of the ML structure

  2665   (followed by a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}'')  is inserted in place of ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}{\isaliteral{22}{\isachardoublequote}}}'' in the above template.  The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''  means that

  2666   the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not

  2667   executable.

  2669   \medskip Another possibility of configuring the code generator is to

  2670   register theorems to be used for code generation. Theorems can be

  2671   registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional

  2672   name as an argument, which indicates the format of the

  2673   theorem. Currently supported formats are equations (this is the

  2674   default when no name is specified) and horn clauses (this is

  2675   indicated by the name \texttt{ind}). The left-hand sides of

  2676   equations may only contain constructors and distinct variables,

  2677   whereas horn clauses must have the same format as introduction rules

  2678   of inductive definitions.

  2680   The following example specifies three equations from which to

  2681   generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also

  2682   \verb|~~/src/HOL/Nat.thy|).%

  2683 \end{isamarkuptext}%

  2684 \isamarkuptrue%

  2685 \isacommand{lemma}\isamarkupfalse%

  2686 \ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Suc\ m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2687 \ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2688 \ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}%

  2689 \isadelimproof

  2690 \ %

  2691 \endisadelimproof

  2692 %

  2693 \isatagproof

  2694 \isacommand{by}\isamarkupfalse%

  2695 \ simp{\isaliteral{5F}{\isacharunderscore}}all%

  2696 \endisatagproof

  2697 {\isafoldproof}%

  2698 %

  2699 \isadelimproof

  2700 %

  2701 \endisadelimproof

  2702 %

  2703 \isamarkupsubsubsection{Specific HOL code generators%

  2704 }

  2705 \isamarkuptrue%

  2706 %

  2707 \begin{isamarkuptext}%

  2708 The basic code generator framework offered by Isabelle/Pure

  2709   has already been extended with additional code generators for

  2710   specific HOL constructs. These include datatypes, recursive

  2711   functions and inductive relations. The code generator for inductive

  2712   relations can handle expressions of the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{22}{\isachardoublequote}}} is an inductively defined relation. If at

  2713   least one of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is a dummy pattern ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'',

  2714   the above expression evaluates to a sequence of possible answers. If

  2715   all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates

  2716   to a boolean value.

  2718   The following example demonstrates this for beta-reduction on lambda

  2719   terms (see also \verb|~~/src/HOL/Proofs/Lambda/Lambda.thy|).%

  2720 \end{isamarkuptext}%

  2721 \isamarkuptrue%

  2722 \isacommand{datatype}\isamarkupfalse%

  2723 \ dB\ {\isaliteral{3D}{\isacharequal}}\isanewline

  2724 \ \ \ \ Var\ nat\isanewline

  2725 \ \ {\isaliteral{7C}{\isacharbar}}\ App\ dB\ dB\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6465677265653E}{\isasymdegree}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{2}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2726 \ \ {\isaliteral{7C}{\isacharbar}}\ Abs\ dB\isanewline

  2727 \isanewline

  2728 \isacommand{primrec}\isamarkupfalse%

  2729 \ lift\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2730 \isakeyword{where}\isanewline

  2731 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ k\ then\ Var\ i\ else\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2732 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ lift\ s\ k\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ lift\ t\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2733 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Abs\ s{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}lift\ s\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2734 \isanewline

  2735 \isacommand{primrec}\isamarkupfalse%

  2736 \ subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2737 \isakeyword{where}\isanewline

  2738 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

  2739 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}\ i\ then\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ if\ i\ {\isaliteral{3D}{\isacharequal}}\ k\ then\ s\ else\ Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2740 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2741 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Abs\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{5B}{\isacharbrackleft}}lift\ s\ {\isadigit{0}}\ {\isaliteral{2F}{\isacharslash}}\ k{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2742 \isanewline

  2743 \isacommand{inductive}\isamarkupfalse%

  2744 \ beta\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2745 \isakeyword{where}\isanewline

  2746 \ \ \ \ beta{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ s{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{2F}{\isacharslash}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2747 \ \ {\isaliteral{7C}{\isacharbar}}\ appL{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2748 \ \ {\isaliteral{7C}{\isacharbar}}\ appR{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2749 \ \ {\isaliteral{7C}{\isacharbar}}\ abs{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Abs\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Abs\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2750 \isanewline

  2751 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2752 \ Test\isanewline

  2753 \isakeyword{contains}\isanewline

  2754 \ \ test{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Var\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2755 \ \ test{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}%

  2756 \begin{isamarkuptext}%

  2757 In the above example, \verb|Test.test1| evaluates to a boolean,

  2758   whereas \verb|Test.test2| is a lazy sequence whose elements can be

  2759   inspected separately.%

  2760 \end{isamarkuptext}%

  2761 \isamarkuptrue%

  2762 %

  2763 \isadelimML

  2764 %

  2765 \endisadelimML

  2766 %

  2767 \isatagML

  2768 \isacommand{ML}\isamarkupfalse%

  2769 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2770 \isaantiq

  2771 assert{}%

  2772 \endisaantiq

  2773 \ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

  2774 \isacommand{ML}\isamarkupfalse%

  2775 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ results\ {\isaliteral{3D}{\isacharequal}}\ DSeq{\isaliteral{2E}{\isachardot}}list{\isaliteral{5F}{\isacharunderscore}}of\ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{2}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

  2776 \isacommand{ML}\isamarkupfalse%

  2777 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2778 \isaantiq

  2779 assert{}%

  2780 \endisaantiq

  2781 \ {\isaliteral{28}{\isacharparenleft}}length\ results\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2782 \endisatagML

  2783 {\isafoldML}%

  2784 %

  2785 \isadelimML

  2786 %

  2787 \endisadelimML

  2788 %

  2789 \begin{isamarkuptext}%

  2790 \medskip The theory underlying the HOL code generator is described

  2791   more detailed in \cite{Berghofer-Nipkow:2002}. More examples that

  2792   illustrate the usage of the code generator can be found e.g.\ in

  2793   \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%

  2794 \end{isamarkuptext}%

  2795 \isamarkuptrue%

  2796 %

  2797 \isamarkupsection{Definition by specification \label{sec:hol-specification}%

  2798 }

  2799 \isamarkuptrue%

  2800 %

  2801 \begin{isamarkuptext}%

  2802 \begin{matharray}{rcl}

  2803     \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  2804     \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

  2805   \end{matharray}

  2807   \begin{railoutput}

  2808 \rail@begin{6}{}

  2809 \rail@bar

  2810 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]

  2811 \rail@nextbar{1}

  2812 \rail@term{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}}[]

  2813 \rail@endbar

  2814 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2815 \rail@plus

  2816 \rail@nont{\isa{decl}}[]

  2817 \rail@nextplus{1}

  2818 \rail@endplus

  2819 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2820 \rail@cr{3}

  2821 \rail@plus

  2822 \rail@bar

  2823 \rail@nextbar{4}

  2824 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

  2825 \rail@endbar

  2826 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  2827 \rail@nextplus{5}

  2828 \rail@endplus

  2829 \rail@end

  2830 \rail@begin{2}{\isa{decl}}

  2831 \rail@bar

  2832 \rail@nextbar{1}

  2833 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2834 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  2835 \rail@endbar

  2836 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2837 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2838 \rail@term{\isa{\isakeyword{overloaded}}}[]

  2839 \rail@bar

  2840 \rail@nextbar{1}

  2841 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2842 \rail@endbar

  2843 \rail@end

  2844 \end{railoutput}

  2847   \begin{description}

  2849   \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up a

  2850   goal stating the existence of terms with the properties specified to

  2851   hold for the constants given in \isa{decls}.  After finishing the

  2852   proof, the theory will be augmented with definitions for the given

  2853   constants, as well as with theorems stating the properties for these

  2854   constants.

  2856   \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up

  2857   a goal stating the existence of terms with the properties specified

  2858   to hold for the constants given in \isa{decls}.  After finishing

  2859   the proof, the theory will be augmented with axioms expressing the

  2860   properties given in the first place.

  2862   \item \isa{decl} declares a constant to be defined by the

  2863   specification given.  The definition for the constant \isa{c} is

  2864   bound to the name \isa{c{\isaliteral{5F}{\isacharunderscore}}def} unless a theorem name is given in

  2865   the declaration.  Overloaded constants should be declared as such.

  2867   \end{description}

  2869   Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by

  2870   construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}} does introduce axioms, but only after the

  2871   user has explicitly proven it to be safe.  A practical issue must be

  2872   considered, though: After introducing two constants with the same

  2873   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove

  2874   that the two constants are, in fact, equal.  If this might be a

  2875   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}.%

  2876 \end{isamarkuptext}%

  2877 \isamarkuptrue%

  2878 %

  2879 \isadelimtheory

  2880 %

  2881 \endisadelimtheory

  2882 %

  2883 \isatagtheory

  2884 \isacommand{end}\isamarkupfalse%

  2885 %

  2886 \endisatagtheory

  2887 {\isafoldtheory}%

  2888 %

  2889 \isadelimtheory

  2890 %

  2891 \endisadelimtheory

  2892 \isanewline

  2893 \end{isabellebody}%

  2894 %%% Local Variables:

  2895 %%% mode: latex

  2896 %%% TeX-master: "root"

  2897 %%% End:

author	wenzelm
	Thu, 26 May 2011 14:24:26 +0200
changeset 44115	6891e8a8d748
parent 44114	6834af822a8b
child 44116	a5bbc11474f9
permissions	-rw-r--r--