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   inductive ones, generating the standard infrastructure of derived

   733   concepts (primitive recursion etc.).

   735   \end{description}

   737   The induction and exhaustion theorems generated provide case names

   738   according to the constructors involved, while parameters are named

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

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

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

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

   744   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

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

   746   internally bound parameters).%

   747 \end{isamarkuptext}%

   748 \isamarkuptrue%

   749 %

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

   751 }

   752 \isamarkuptrue%

   753 %

   754 \begin{isamarkuptext}%

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

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

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

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

   759   admits operations that are polymorphic with respect to record

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

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

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

   763 \end{isamarkuptext}%

   764 \isamarkuptrue%

   765 %

   766 \isamarkupsubsection{Basic concepts%

   767 }

   768 \isamarkuptrue%

   769 %

   770 \begin{isamarkuptext}%

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

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

   774   \begin{center}

   775   \begin{tabular}{l|l|l}

   776     & record terms & record types \\ \hline

   777     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}}} \\

   778     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}}} &

   779       \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}}} \\

   780   \end{tabular}

   781   \end{center}

   783   \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}}}.

   785   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

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

   787   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}}}

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

   790   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

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

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

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

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

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

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

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

   798   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.

   799   Fixed records are special instances of record schemes, where

   800   ``\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}}}

   801   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

   802   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}}}.

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

   805   typed language like HOL work out:

   807   \begin{enumerate}

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

   810   variable,

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

   813   the logic as first-class values.

   815   \end{enumerate}

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

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

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

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

   821   The record package provides several standard operations like

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

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

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

   825   records in practice.%

   826 \end{isamarkuptext}%

   827 \isamarkuptrue%

   828 %

   829 \isamarkupsubsection{Record specifications%

   830 }

   831 \isamarkuptrue%

   832 %

   833 \begin{isamarkuptext}%

   834 \begin{matharray}{rcl}

   835     \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}}} \\

   836   \end{matharray}

   838   \begin{railoutput}

   839 \rail@begin{4}{}

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

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

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

   843 \rail@cr{2}

   844 \rail@bar

   845 \rail@nextbar{3}

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

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

   848 \rail@endbar

   849 \rail@plus

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

   851 \rail@nextplus{3}

   852 \rail@endplus

   853 \rail@end

   854 \end{railoutput}

   857   \begin{description}

   859   \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}}},

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

   861   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.

   863   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

   864   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

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

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

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

   868   the record name internally.

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

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

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

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

   874   merge multiple parent records!

   876   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

   877   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

   878   \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}}}.

   880   \end{description}%

   881 \end{isamarkuptext}%

   882 \isamarkuptrue%

   883 %

   884 \isamarkupsubsection{Record operations%

   885 }

   886 \isamarkuptrue%

   887 %

   888 \begin{isamarkuptext}%

   889 Any record definition of the form presented above produces certain

   890   standard operations.  Selectors and updates are provided for any

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

   892   cumulative record constructor functions.  To simplify the

   893   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}}}.

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

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

   898   \begin{matharray}{lll}

   899     \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}}} \\

   900     \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}}} \\

   901   \end{matharray}

   903   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

   904   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

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

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

   907   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.

   908   Thus commutativity of independent updates can be proven within the

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

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

   912   constructor function:

   914   \begin{matharray}{lll}

   915     \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}}} \\

   916   \end{matharray}

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

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

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

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

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

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

   924   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

   925   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}}},

   926   the above record operations will get the following types:

   928   \medskip

   929   \begin{tabular}{lll}

   930     \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}}} \\

   931     \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}}} \\

   932     \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}}} \\

   933   \end{tabular}

   934   \medskip

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

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

   938   record fragment consisting of exactly the new fields introduced here

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

   940   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.

   942   \medskip

   943   \begin{tabular}{lll}

   944     \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}}} \\

   945     \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}}} \\

   946     \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}}} \\

   947   \end{tabular}

   948   \medskip

   950   \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

   951   for root records.%

   952 \end{isamarkuptext}%

   953 \isamarkuptrue%

   954 %

   955 \isamarkupsubsection{Derived rules and proof tools%

   956 }

   957 \isamarkuptrue%

   958 %

   959 \begin{isamarkuptext}%

   960 The record package proves several results internally, declaring

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

   962   reason about record structures quite conveniently.  Assume that

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

   965   \begin{enumerate}

   967   \item Standard conversions for selectors or updates applied to

   968   record constructor terms are made part of the default Simplifier

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

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

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

   973   \item Selectors applied to updated records are automatically reduced

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

   975   standard Simplifier setup.

   977   \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

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

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

   981   \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,

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

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

   985   \item Representations of arbitrary record expressions as canonical

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

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

   988   fixed records, record schemes, more parts etc.

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

   991   sensible rule according to the type of the indicated record

   992   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.

   994   \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}

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

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

   998   \end{enumerate}%

   999 \end{isamarkuptext}%

  1000 \isamarkuptrue%

  1001 %

  1002 \isamarkupsection{Adhoc tuples%

  1003 }

  1004 \isamarkuptrue%

  1005 %

  1006 \begin{isamarkuptext}%

  1007 \begin{matharray}{rcl}

  1008     \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} \\

  1009   \end{matharray}

  1011   \begin{railoutput}

  1012 \rail@begin{2}{}

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

  1014 \rail@bar

  1015 \rail@nextbar{1}

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

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

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

  1019 \rail@endbar

  1020 \rail@end

  1021 \end{railoutput}

  1024   \begin{description}

  1026   \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

  1027   arguments in function applications to be represented canonically

  1028   according to their tuple type structure.

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

  1031   parameters introduced.

  1033   \end{description}%

  1034 \end{isamarkuptext}%

  1035 \isamarkuptrue%

  1036 %

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

  1038 }

  1039 \isamarkuptrue%

  1040 %

  1041 \begin{isamarkuptext}%

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

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

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

  1045   \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

  1046   \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

  1047   postulated that establish an isomorphism between the new type and

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

  1049   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

  1050   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

  1051   those type arguments.

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

  1054   of the particular set-theoretic interpretation of HOL

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

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

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

  1058   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

  1059   abbreviations, without any logical significance.

  1061   \begin{matharray}{rcl}

  1062     \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}}} \\

  1063   \end{matharray}

  1065   \begin{railoutput}

  1066 \rail@begin{2}{}

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

  1068 \rail@bar

  1069 \rail@nextbar{1}

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

  1071 \rail@endbar

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

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

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

  1075 \rail@end

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

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

  1078 \rail@bar

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

  1080 \rail@nextbar{1}

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

  1082 \rail@nextbar{2}

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

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

  1085 \rail@endbar

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

  1087 \rail@end

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

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

  1090 \rail@bar

  1091 \rail@nextbar{1}

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

  1093 \rail@endbar

  1094 \rail@end

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

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

  1097 \rail@bar

  1098 \rail@nextbar{1}

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

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

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

  1102 \rail@endbar

  1103 \rail@end

  1104 \end{railoutput}

  1107   \begin{description}

  1109   \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}}}

  1110   axiomatizes a type definition in the background theory of the

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

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

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

  1114   but no term variables.

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

  1117   constructor cannot depend on parameters or assumptions of the

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

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

  1120   which could result in different interpretations in target contexts:

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

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

  1123   contexts.

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

  1126   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

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

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

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

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

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

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

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

  1136   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}

  1137   provide the most basic characterization as a corresponding

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

  1139   \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

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

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

  1142   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}~/

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

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

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

  1146   respectively.

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

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

  1150   \isa{t} directly.

  1152   \end{description}

  1154   \begin{warn}

  1155   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

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

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

  1158   interpretation of such free-form axiomatizations can coexist with

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

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

  1161   \cite{MuellerNvOS99}).

  1162   \end{warn}%

  1163 \end{isamarkuptext}%

  1164 \isamarkuptrue%

  1165 %

  1166 \isamarkupsubsubsection{Examples%

  1167 }

  1168 \isamarkuptrue%

  1169 %

  1170 \begin{isamarkuptext}%

  1171 Type definitions permit the introduction of abstract data

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

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

  1174   of a type, this involves two steps:

  1176   \begin{enumerate}

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

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

  1180   based on this representation.

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

  1183   from the representation.

  1185   \end{enumerate}

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

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

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

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

  1192 \end{isamarkuptext}%

  1193 \isamarkuptrue%

  1194 \isacommand{typedef}\isamarkupfalse%

  1195 \ 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

  1196 %

  1197 \isadelimproof

  1198 \ \ %

  1199 \endisadelimproof

  1200 %

  1201 \isatagproof

  1202 \isacommand{by}\isamarkupfalse%

  1203 \ blast%

  1204 \endisatagproof

  1205 {\isafoldproof}%

  1206 %

  1207 \isadelimproof

  1208 \isanewline

  1209 %

  1210 \endisadelimproof

  1211 \isanewline

  1212 \isacommand{definition}\isamarkupfalse%

  1213 \ {\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

  1214 \isacommand{definition}\isamarkupfalse%

  1215 \ {\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

  1216 \isacommand{definition}\isamarkupfalse%

  1217 \ {\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

  1218 \isanewline

  1219 \isacommand{lemma}\isamarkupfalse%

  1220 \ 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

  1221 %

  1222 \isadelimproof

  1223 \ \ %

  1224 \endisadelimproof

  1225 %

  1226 \isatagproof

  1227 \isacommand{by}\isamarkupfalse%

  1228 \ {\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}}%

  1229 \endisatagproof

  1230 {\isafoldproof}%

  1231 %

  1232 \isadelimproof

  1233 \isanewline

  1234 %

  1235 \endisadelimproof

  1236 \isanewline

  1237 \isacommand{lemma}\isamarkupfalse%

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

  1239 \ \ \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

  1240 %

  1241 \isadelimproof

  1242 \ \ %

  1243 \endisadelimproof

  1244 %

  1245 \isatagproof

  1246 \isacommand{by}\isamarkupfalse%

  1247 \ {\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}}%

  1248 \endisatagproof

  1249 {\isafoldproof}%

  1250 %

  1251 \isadelimproof

  1252 %

  1253 \endisadelimproof

  1254 %

  1255 \begin{isamarkuptext}%

  1256 Note that such trivial constructions are better done with

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

  1258 \end{isamarkuptext}%

  1259 \isamarkuptrue%

  1260 \isacommand{datatype}\isamarkupfalse%

  1261 \ 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}}%

  1262 \begin{isamarkuptext}%

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

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

  1265 \end{isamarkuptext}%

  1266 \isamarkuptrue%

  1267 %

  1268 \isamarkupsection{Functorial structure of types%

  1269 }

  1270 \isamarkuptrue%

  1271 %

  1272 \begin{isamarkuptext}%

  1273 \begin{matharray}{rcl}

  1274     \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}}}

  1275   \end{matharray}

  1277   \begin{railoutput}

  1278 \rail@begin{2}{}

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

  1280 \rail@bar

  1281 \rail@nextbar{1}

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

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

  1284 \rail@endbar

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

  1286 \rail@end

  1287 \end{railoutput}

  1290   \begin{description}

  1292   \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

  1293   prove and register properties about the functorial structure of type

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

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

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

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

  1298   constructor, an explicit prefix can be given alternatively.

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

  1301   corresponding type constructor and must conform to the following

  1302   type pattern:

  1304   \begin{matharray}{lll}

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

  1306       \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}}} \\

  1307   \end{matharray}

  1309   \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

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

  1311   \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,

  1312   \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}}}.

  1314   \end{description}%

  1315 \end{isamarkuptext}%

  1316 \isamarkuptrue%

  1317 %

  1318 \isamarkupsection{Arithmetic proof support%

  1319 }

  1320 \isamarkuptrue%

  1321 %

  1322 \begin{isamarkuptext}%

  1323 \begin{matharray}{rcl}

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

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

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

  1327   \end{matharray}

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

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

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

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

  1334   always supplied to the arithmetic provers implicitly.

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

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

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

  1340   already invoked by the Simplifier.%

  1341 \end{isamarkuptext}%

  1342 \isamarkuptrue%

  1343 %

  1344 \isamarkupsection{Intuitionistic proof search%

  1345 }

  1346 \isamarkuptrue%

  1347 %

  1348 \begin{isamarkuptext}%

  1349 \begin{matharray}{rcl}

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

  1351   \end{matharray}

  1353   \begin{railoutput}

  1354 \rail@begin{2}{}

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

  1356 \rail@plus

  1357 \rail@nextplus{1}

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

  1359 \rail@endplus

  1360 \rail@end

  1361 \end{railoutput}

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

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

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

  1367   goal before commencing proof search.

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

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

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

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

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

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

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

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

  1377 \end{isamarkuptext}%

  1378 \isamarkuptrue%

  1379 %

  1380 \isamarkupsection{Coherent Logic%

  1381 }

  1382 \isamarkuptrue%

  1383 %

  1384 \begin{isamarkuptext}%

  1385 \begin{matharray}{rcl}

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

  1387   \end{matharray}

  1389   \begin{railoutput}

  1390 \rail@begin{2}{}

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

  1392 \rail@bar

  1393 \rail@nextbar{1}

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

  1395 \rail@endbar

  1396 \rail@end

  1397 \end{railoutput}

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

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

  1402   applications in confluence theory, lattice theory and projective

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

  1404   examples.%

  1405 \end{isamarkuptext}%

  1406 \isamarkuptrue%

  1407 %

  1408 \isamarkupsection{Proving propositions%

  1409 }

  1410 \isamarkuptrue%

  1411 %

  1412 \begin{isamarkuptext}%

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

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

  1415   These tools are available via the following commands.

  1417   \begin{matharray}{rcl}

  1418     \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}}} \\

  1419     \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}}} \\

  1420     \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}}} \\

  1421     \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}}}

  1422   \end{matharray}

  1424   \begin{railoutput}

  1425 \rail@begin{6}{}

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

  1427 \rail@bar

  1428 \rail@nextbar{1}

  1429 \rail@plus

  1430 \rail@bar

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

  1432 \rail@nextbar{2}

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

  1434 \rail@nextbar{3}

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

  1436 \rail@nextbar{4}

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

  1438 \rail@endbar

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

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

  1441 \rail@nextplus{5}

  1442 \rail@endplus

  1443 \rail@endbar

  1444 \rail@bar

  1445 \rail@nextbar{1}

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

  1447 \rail@endbar

  1448 \rail@end

  1449 \rail@begin{2}{}

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

  1451 \rail@bar

  1452 \rail@nextbar{1}

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

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

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

  1456 \rail@endbar

  1457 \rail@bar

  1458 \rail@nextbar{1}

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

  1460 \rail@endbar

  1461 \rail@bar

  1462 \rail@nextbar{1}

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

  1464 \rail@endbar

  1465 \rail@end

  1466 \rail@begin{2}{}

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

  1468 \rail@bar

  1469 \rail@nextbar{1}

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

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

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

  1473 \rail@endbar

  1474 \rail@end

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

  1476 \rail@plus

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

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

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

  1480 \rail@nextplus{1}

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

  1482 \rail@endplus

  1483 \rail@end

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

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

  1486 \rail@bar

  1487 \rail@nextbar{1}

  1488 \rail@plus

  1489 \rail@bar

  1490 \rail@nextbar{2}

  1491 \rail@bar

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

  1493 \rail@nextbar{3}

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

  1495 \rail@endbar

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

  1497 \rail@endbar

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

  1499 \rail@nextplus{4}

  1500 \rail@endplus

  1501 \rail@endbar

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

  1503 \rail@end

  1504 \end{railoutput}

  1505  % FIXME try: proper clasimpmod!?

  1506   % FIXME check args "value"

  1508   \begin{description}

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

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

  1512     in this way.

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

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

  1516     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}}},

  1517     \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

  1518     methods.

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

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

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

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

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

  1527   \end{description}%

  1528 \end{isamarkuptext}%

  1529 \isamarkuptrue%

  1530 %

  1531 \isamarkupsection{Checking and refuting propositions%

  1532 }

  1533 \isamarkuptrue%

  1534 %

  1535 \begin{isamarkuptext}%

  1536 Identifying incorrect propositions usually involves evaluation of

  1537   particular assignments and systematic counterexample search.  This

  1538   is supported by the following commands.

  1540   \begin{matharray}{rcl}

  1541     \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}}} \\

  1542     \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}}} \\

  1543     \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}}} \\

  1544     \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}}} \\

  1545     \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}}} \\

  1546     \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}}} \\

  1547     \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}}}

  1548   \end{matharray}

  1550   \begin{railoutput}

  1551 \rail@begin{2}{}

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

  1553 \rail@bar

  1554 \rail@nextbar{1}

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

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

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

  1558 \rail@endbar

  1559 \rail@bar

  1560 \rail@nextbar{1}

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

  1562 \rail@endbar

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

  1564 \rail@end

  1565 \rail@begin{3}{}

  1566 \rail@bar

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

  1568 \rail@nextbar{1}

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

  1570 \rail@nextbar{2}

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

  1572 \rail@endbar

  1573 \rail@bar

  1574 \rail@nextbar{1}

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

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

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

  1578 \rail@endbar

  1579 \rail@bar

  1580 \rail@nextbar{1}

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

  1582 \rail@endbar

  1583 \rail@end

  1584 \rail@begin{3}{}

  1585 \rail@bar

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

  1587 \rail@nextbar{1}

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

  1589 \rail@nextbar{2}

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

  1591 \rail@endbar

  1592 \rail@bar

  1593 \rail@nextbar{1}

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

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

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

  1597 \rail@endbar

  1598 \rail@end

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

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

  1601 \rail@plus

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

  1603 \rail@nextplus{1}

  1604 \rail@endplus

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

  1606 \rail@end

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

  1608 \rail@plus

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

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

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

  1612 \rail@nextplus{1}

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

  1614 \rail@endplus

  1615 \rail@end

  1616 \end{railoutput}

  1617  % FIXME check "value"

  1619   \begin{description}

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

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

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

  1624     Internally, the evaluation is performed by registered evaluators,

  1625     which are invoked sequentially until a result is returned.

  1626     Alternatively a specific evaluator can be selected using square

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

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

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

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

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

  1633     counterexamples using a series of assignments for its

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

  1635     can be selected explicitly using an optional goal index.

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

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

  1638     By default, quickcheck uses exhaustive testing.

  1639     A number of configuration options are supported for

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

  1642     \begin{description}

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

  1645       (e.g. exhaustive or random).

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

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

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

  1649     for assignment values.

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

  1652       these terms under the variable assignment found by quickcheck.

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

  1655     generated for each particular size.

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

  1658     structured proofs should be ignored.

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

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

  1663     instantiate type variables.

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

  1666     fulfilled the preconditions.

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

  1669     current size for assignment values.

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

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

  1674     \end{description}

  1676     These option can be given within square brackets.

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

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

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

  1682     counterexamples using a reduction to SAT. The following configuration

  1683     options are supported:

  1685     \begin{description}

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

  1688       models to search for.

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

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

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

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

  1695     Nonpositive values mean $\infty$.

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

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

  1700     structured proofs should be ignored.

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

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

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

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

  1708     \end{description}

  1710     These option can be given within square brackets.

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

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

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

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

  1717     \cite{isabelle-nitpick} for details.

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

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

  1722   \end{description}%

  1723 \end{isamarkuptext}%

  1724 \isamarkuptrue%

  1725 %

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

  1727 }

  1728 \isamarkuptrue%

  1729 %

  1730 \begin{isamarkuptext}%

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

  1732   induction in unstructured tactic scripts; see also

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

  1735   \begin{matharray}{rcl}

  1736     \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} \\

  1737     \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} \\

  1738     \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} \\

  1739     \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}}} \\

  1740   \end{matharray}

  1742   \begin{railoutput}

  1743 \rail@begin{2}{}

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

  1745 \rail@bar

  1746 \rail@nextbar{1}

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

  1748 \rail@endbar

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

  1750 \rail@bar

  1751 \rail@nextbar{1}

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

  1753 \rail@endbar

  1754 \rail@end

  1755 \rail@begin{3}{}

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

  1757 \rail@bar

  1758 \rail@nextbar{1}

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

  1760 \rail@endbar

  1761 \rail@bar

  1762 \rail@nextbar{1}

  1763 \rail@plus

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

  1765 \rail@nextplus{2}

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

  1767 \rail@endplus

  1768 \rail@endbar

  1769 \rail@bar

  1770 \rail@nextbar{1}

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

  1772 \rail@endbar

  1773 \rail@end

  1774 \rail@begin{3}{}

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

  1776 \rail@plus

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

  1778 \rail@nextplus{1}

  1779 \rail@endplus

  1780 \rail@bar

  1781 \rail@nextbar{1}

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

  1783 \rail@plus

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

  1785 \rail@nextplus{2}

  1786 \rail@endplus

  1787 \rail@endbar

  1788 \rail@end

  1789 \rail@begin{3}{}

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

  1791 \rail@plus

  1792 \rail@bar

  1793 \rail@nextbar{1}

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

  1795 \rail@endbar

  1796 \rail@plus

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

  1798 \rail@nextplus{1}

  1799 \rail@endplus

  1800 \rail@nextplus{2}

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

  1802 \rail@endplus

  1803 \rail@end

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

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

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

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

  1808 \rail@end

  1809 \end{railoutput}

  1812   \begin{description}

  1814   \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

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

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

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

  1819   These unstructured tactics feature both goal addressing and dynamic

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

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

  1822   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

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

  1824   being addressed.

  1826   \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

  1827   forward manner.

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

  1830   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

  1831   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

  1832   be generalized before applying the resulting rule.

  1834   \end{description}%

  1835 \end{isamarkuptext}%

  1836 \isamarkuptrue%

  1837 %

  1838 \isamarkupsection{Executable code%

  1839 }

  1840 \isamarkuptrue%

  1841 %

  1842 \begin{isamarkuptext}%

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

  1844   specifications.  In principle, execution could be simulated by

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

  1846   simplification.  Unfortunately, this approach is rather inefficient.

  1847   A more efficient way of executing specifications is to translate

  1848   them into a functional programming language such as ML.

  1850   Isabelle provides two generic frameworks to support code generation

  1851   from executable specifications.  Isabelle/HOL instantiates these

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

  1853 \end{isamarkuptext}%

  1854 \isamarkuptrue%

  1855 %

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

  1857 }

  1858 \isamarkuptrue%

  1859 %

  1860 \begin{isamarkuptext}%

  1861 This framework generates code from functional programs

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

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

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

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

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

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

  1868   Inductive specifications can be executed using the predicate

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

  1870   an introduction.

  1872   \begin{matharray}{rcl}

  1873     \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}}} \\

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

  1875     \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}}} \\

  1876     \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}}} \\

  1877     \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}}} \\

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

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

  1880     \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}}} \\

  1881     \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}}} \\

  1882     \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}}} \\

  1883     \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}}} \\

  1884     \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}}} \\

  1885     \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}}} \\

  1886     \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}}} \\

  1887     \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}}} \\

  1888     \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}}} \\

  1889     \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}}} \\

  1890     \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}}} \\

  1891     \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}}}

  1892   \end{matharray}

  1894   \begin{railoutput}

  1895 \rail@begin{11}{}

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

  1897 \rail@plus

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

  1899 \rail@nextplus{1}

  1900 \rail@endplus

  1901 \rail@cr{3}

  1902 \rail@bar

  1903 \rail@nextbar{4}

  1904 \rail@plus

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

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

  1907 \rail@bar

  1908 \rail@nextbar{5}

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

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

  1911 \rail@endbar

  1912 \rail@cr{7}

  1913 \rail@bar

  1914 \rail@nextbar{8}

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

  1916 \rail@bar

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

  1918 \rail@nextbar{9}

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

  1920 \rail@endbar

  1921 \rail@endbar

  1922 \rail@bar

  1923 \rail@nextbar{8}

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

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

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

  1927 \rail@endbar

  1928 \rail@nextplus{10}

  1929 \rail@endplus

  1930 \rail@endbar

  1931 \rail@end

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

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

  1934 \rail@end

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

  1936 \rail@bar

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

  1938 \rail@nextbar{1}

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

  1940 \rail@nextbar{2}

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

  1942 \rail@endbar

  1943 \rail@end

  1944 \rail@begin{1}{\isa{typeconstructor}}

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

  1946 \rail@end

  1947 \rail@begin{1}{\isa{class}}

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

  1949 \rail@end

  1950 \rail@begin{4}{\isa{target}}

  1951 \rail@bar

  1952 \rail@term{\isa{SML}}[]

  1953 \rail@nextbar{1}

  1954 \rail@term{\isa{OCaml}}[]

  1955 \rail@nextbar{2}

  1956 \rail@term{\isa{Haskell}}[]

  1957 \rail@nextbar{3}

  1958 \rail@term{\isa{Scala}}[]

  1959 \rail@endbar

  1960 \rail@end

  1961 \rail@begin{4}{}

  1962 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]

  1963 \rail@bar

  1964 \rail@nextbar{1}

  1965 \rail@bar

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

  1967 \rail@nextbar{2}

  1968 \rail@term{\isa{abstype}}[]

  1969 \rail@nextbar{3}

  1970 \rail@term{\isa{abstract}}[]

  1971 \rail@endbar

  1972 \rail@endbar

  1973 \rail@end

  1974 \rail@begin{2}{}

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

  1976 \rail@plus

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

  1978 \rail@nextplus{1}

  1979 \rail@endplus

  1980 \rail@end

  1981 \rail@begin{2}{}

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

  1983 \rail@plus

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

  1985 \rail@nextplus{1}

  1986 \rail@endplus

  1987 \rail@end

  1988 \rail@begin{2}{}

  1989 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]

  1990 \rail@bar

  1991 \rail@nextbar{1}

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

  1993 \rail@endbar

  1994 \rail@end

  1995 \rail@begin{2}{}

  1996 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]

  1997 \rail@bar

  1998 \rail@nextbar{1}

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

  2000 \rail@endbar

  2001 \rail@end

  2002 \rail@begin{3}{}

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

  2004 \rail@bar

  2005 \rail@nextbar{1}

  2006 \rail@plus

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

  2008 \rail@nextplus{2}

  2009 \rail@endplus

  2010 \rail@endbar

  2011 \rail@end

  2012 \rail@begin{3}{}

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

  2014 \rail@bar

  2015 \rail@nextbar{1}

  2016 \rail@plus

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

  2018 \rail@nextplus{2}

  2019 \rail@endplus

  2020 \rail@endbar

  2021 \rail@end

  2022 \rail@begin{7}{}

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

  2024 \rail@plus

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

  2026 \rail@nextplus{1}

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

  2028 \rail@endplus

  2029 \rail@cr{3}

  2030 \rail@plus

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

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

  2033 \rail@plus

  2034 \rail@bar

  2035 \rail@nextbar{4}

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

  2037 \rail@endbar

  2038 \rail@nextplus{5}

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

  2040 \rail@endplus

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

  2042 \rail@nextplus{6}

  2043 \rail@endplus

  2044 \rail@end

  2045 \rail@begin{7}{}

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

  2047 \rail@plus

  2048 \rail@nont{\isa{typeconstructor}}[]

  2049 \rail@nextplus{1}

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

  2051 \rail@endplus

  2052 \rail@cr{3}

  2053 \rail@plus

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

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

  2056 \rail@plus

  2057 \rail@bar

  2058 \rail@nextbar{4}

  2059 \rail@nont{\isa{syntax}}[]

  2060 \rail@endbar

  2061 \rail@nextplus{5}

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

  2063 \rail@endplus

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

  2065 \rail@nextplus{6}

  2066 \rail@endplus

  2067 \rail@end

  2068 \rail@begin{9}{}

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

  2070 \rail@plus

  2071 \rail@nont{\isa{class}}[]

  2072 \rail@nextplus{1}

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

  2074 \rail@endplus

  2075 \rail@cr{3}

  2076 \rail@plus

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

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

  2079 \rail@cr{5}

  2080 \rail@plus

  2081 \rail@bar

  2082 \rail@nextbar{6}

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

  2084 \rail@endbar

  2085 \rail@nextplus{7}

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

  2087 \rail@endplus

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

  2089 \rail@nextplus{8}

  2090 \rail@endplus

  2091 \rail@end

  2092 \rail@begin{7}{}

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

  2094 \rail@plus

  2095 \rail@nont{\isa{typeconstructor}}[]

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

  2097 \rail@nont{\isa{class}}[]

  2098 \rail@nextplus{1}

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

  2100 \rail@endplus

  2101 \rail@cr{3}

  2102 \rail@plus

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

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

  2105 \rail@plus

  2106 \rail@bar

  2107 \rail@nextbar{4}

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

  2109 \rail@endbar

  2110 \rail@nextplus{5}

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

  2112 \rail@endplus

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

  2114 \rail@nextplus{6}

  2115 \rail@endplus

  2116 \rail@end

  2117 \rail@begin{2}{}

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

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

  2120 \rail@plus

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

  2122 \rail@nextplus{1}

  2123 \rail@endplus

  2124 \rail@end

  2125 \rail@begin{1}{}

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

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

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

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

  2130 \rail@end

  2131 \rail@begin{2}{}

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

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

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

  2135 \rail@bar

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

  2137 \rail@nextbar{1}

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

  2139 \rail@endbar

  2140 \rail@end

  2141 \rail@begin{2}{}

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

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

  2144 \rail@plus

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

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

  2147 \rail@nextplus{1}

  2148 \rail@endplus

  2149 \rail@end

  2150 \rail@begin{11}{}

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

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

  2153 \rail@cr{2}

  2154 \rail@bar

  2155 \rail@nextbar{3}

  2156 \rail@term{\isa{\isakeyword{datatypes}}}[]

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

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

  2159 \rail@bar

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

  2161 \rail@nextbar{4}

  2162 \rail@plus

  2163 \rail@plus

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

  2165 \rail@nextplus{5}

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

  2167 \rail@endplus

  2168 \rail@nextplus{6}

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

  2170 \rail@endplus

  2171 \rail@endbar

  2172 \rail@endbar

  2173 \rail@cr{8}

  2174 \rail@bar

  2175 \rail@nextbar{9}

  2176 \rail@term{\isa{\isakeyword{functions}}}[]

  2177 \rail@plus

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

  2179 \rail@nextplus{10}

  2180 \rail@endplus

  2181 \rail@endbar

  2182 \rail@bar

  2183 \rail@nextbar{9}

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

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

  2186 \rail@endbar

  2187 \rail@end

  2188 \rail@begin{4}{\isa{syntax}}

  2189 \rail@bar

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

  2191 \rail@nextbar{1}

  2192 \rail@bar

  2193 \rail@term{\isa{\isakeyword{infix}}}[]

  2194 \rail@nextbar{2}

  2195 \rail@term{\isa{\isakeyword{infixl}}}[]

  2196 \rail@nextbar{3}

  2197 \rail@term{\isa{\isakeyword{infixr}}}[]

  2198 \rail@endbar

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

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

  2201 \rail@endbar

  2202 \rail@end

  2203 \end{railoutput}

  2206   \begin{description}

  2208   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} generates code for a given list

  2209   of constants in the specified target language(s).  If no

  2210   serialization instruction is given, only abstract code is generated

  2211   internally.

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

  2214   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

  2215   available by giving \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.

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

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

  2219   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} keyword; then \emph{all} code is

  2220   placed in this module.

  2222   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

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

  2224   directory, where code is generated in multiple files reflecting the

  2225   module hierarchy.  Omitting the file specification denotes standard

  2226   output.

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

  2229   \emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits

  2230   explicit module signatures.

  2232   For \emph{Haskell} a module name prefix may be given using the

  2233   ``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a

  2234   ``\verb|deriving (Read, Show)|'' clause to each appropriate

  2235   datatype declaration.

  2237   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option

  2238   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' deselects) a code equation for code generation.

  2239   Usually packages introducing code equations provide a reasonable

  2240   default setup for selection.  Variants \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstype{\isaliteral{22}{\isachardoublequote}}} and

  2241   \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstract{\isaliteral{22}{\isachardoublequote}}} declare abstract datatype certificates or

  2242   code equations on abstract datatype representations respectively.

  2244   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}} declares constants which are not

  2245   required to have a definition by means of code equations; if needed

  2246   these are implemented by program abort instead.

  2248   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}} specifies a constructor set

  2249   for a logical type.

  2251   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on

  2252   selected code equations and code generator datatypes.

  2254   \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option

  2255   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as

  2256   rewrite rules to any code equation during preprocessing.

  2258   \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

  2259   result of an evaluation.

  2261   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code

  2262   generator preprocessor.

  2264   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}} prints a list of theorems

  2265   representing the corresponding program containing all given

  2266   constants after preprocessing.

  2268   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes dependencies of

  2269   theorems representing the corresponding program containing all given

  2270   constants after preprocessing.

  2272   \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}} associates a list of constants

  2273   with target-specific serializations; omitting a serialization

  2274   deletes an existing serialization.

  2276   \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}} associates a list of type

  2277   constructors with target-specific serializations; omitting a

  2278   serialization deletes an existing serialization.

  2280   \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}} associates a list of classes

  2281   with target-specific class names; omitting a serialization deletes

  2282   an existing serialization.  This applies only to \emph{Haskell}.

  2284   \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}} declares a list of type

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

  2286   given target.  Omitting a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' deletes an existing

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

  2288   \emph{Haskell}.

  2290   \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}} declares a list of names as

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

  2292   generated code.

  2294   \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}} provides an auxiliary mechanism

  2295   to generate monadic code for Haskell.

  2297   \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}} adds arbitrary named content

  2298   (``include'') to generated code.  A ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' as last argument

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

  2301   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}} declares aliasings from one

  2302   module name onto another.

  2304   \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} without a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}''

  2305   argument compiles code into the system runtime environment and

  2306   modifies the code generator setup that future invocations of system

  2307   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

  2308   entities.  With a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}'' argument, the corresponding code

  2309   is generated into that specified file without modifying the code

  2310   generator setup.

  2312   \end{description}%

  2313 \end{isamarkuptext}%

  2314 \isamarkuptrue%

  2315 %

  2316 \isamarkupsubsection{The old code generator (S. Berghofer)%

  2317 }

  2318 \isamarkuptrue%

  2319 %

  2320 \begin{isamarkuptext}%

  2321 This framework generates code from both functional and

  2322   relational programs to SML, as explained below.

  2324   \begin{matharray}{rcl}

  2325     \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}}} \\

  2326     \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}}} \\

  2327     \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}}} \\

  2328     \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}}} \\

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

  2330   \end{matharray}

  2332   \begin{railoutput}

  2333 \rail@begin{11}{}

  2334 \rail@bar

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

  2336 \rail@nextbar{1}

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

  2338 \rail@endbar

  2339 \rail@bar

  2340 \rail@nextbar{1}

  2341 \rail@nont{\isa{modespec}}[]

  2342 \rail@endbar

  2343 \rail@bar

  2344 \rail@nextbar{1}

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

  2346 \rail@endbar

  2347 \rail@cr{3}

  2348 \rail@bar

  2349 \rail@nextbar{4}

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

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

  2352 \rail@endbar

  2353 \rail@bar

  2354 \rail@nextbar{4}

  2355 \rail@term{\isa{\isakeyword{imports}}}[]

  2356 \rail@plus

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

  2358 \rail@nextplus{5}

  2359 \rail@endplus

  2360 \rail@endbar

  2361 \rail@cr{7}

  2362 \rail@term{\isa{\isakeyword{contains}}}[]

  2363 \rail@bar

  2364 \rail@plus

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

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

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

  2368 \rail@nextplus{8}

  2369 \rail@endplus

  2370 \rail@nextbar{9}

  2371 \rail@plus

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

  2373 \rail@nextplus{10}

  2374 \rail@endplus

  2375 \rail@endbar

  2376 \rail@end

  2377 \rail@begin{2}{\isa{modespec}}

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

  2379 \rail@plus

  2380 \rail@nextplus{1}

  2381 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2382 \rail@endplus

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

  2384 \rail@end

  2385 \rail@begin{2}{}

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

  2387 \rail@plus

  2388 \rail@nont{\isa{codespec}}[]

  2389 \rail@nextplus{1}

  2390 \rail@endplus

  2391 \rail@end

  2392 \rail@begin{2}{\isa{codespec}}

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

  2394 \rail@nont{\isa{template}}[]

  2395 \rail@bar

  2396 \rail@nextbar{1}

  2397 \rail@nont{\isa{attachment}}[]

  2398 \rail@endbar

  2399 \rail@end

  2400 \rail@begin{2}{}

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

  2402 \rail@plus

  2403 \rail@nont{\isa{tycodespec}}[]

  2404 \rail@nextplus{1}

  2405 \rail@endplus

  2406 \rail@end

  2407 \rail@begin{2}{\isa{tycodespec}}

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

  2409 \rail@nont{\isa{template}}[]

  2410 \rail@bar

  2411 \rail@nextbar{1}

  2412 \rail@nont{\isa{attachment}}[]

  2413 \rail@endbar

  2414 \rail@end

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

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

  2417 \rail@end

  2418 \rail@begin{1}{\isa{template}}

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

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

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

  2422 \rail@end

  2423 \rail@begin{2}{\isa{attachment}}

  2424 \rail@term{\isa{attach}}[]

  2425 \rail@bar

  2426 \rail@nextbar{1}

  2427 \rail@nont{\isa{modespec}}[]

  2428 \rail@endbar

  2429 \rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]

  2430 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  2431 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]

  2432 \rail@end

  2433 \rail@begin{2}{}

  2434 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]

  2435 \rail@bar

  2436 \rail@nextbar{1}

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

  2438 \rail@endbar

  2439 \rail@end

  2440 \end{railoutput}%

  2441 \end{isamarkuptext}%

  2442 \isamarkuptrue%

  2443 %

  2444 \isamarkupsubsubsection{Invoking the code generator%

  2445 }

  2446 \isamarkuptrue%

  2447 %

  2448 \begin{isamarkuptext}%

  2449 The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}

  2450   and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to

  2451   \emph{incremental} and \emph{modular} code generation, respectively.

  2453   \begin{description}

  2455   \item [Modular] For each theory, an ML structure is generated,

  2456   containing the code generated from the constants defined in this

  2457   theory.

  2459   \item [Incremental] All the generated code is emitted into the same

  2460   structure.  This structure may import code from previously generated

  2461   structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.

  2462   Moreover, the generated structure may also be referred to in later

  2463   invocations of the code generator.

  2465   \end{description}

  2467   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}}}}

  2468   keywords, the user may specify an optional list of ``modes'' in

  2469   parentheses. These can be used to instruct the code generator to

  2470   emit additional code for special purposes, e.g.\ functions for

  2471   converting elements of generated datatypes to Isabelle terms, or

  2472   test data generators. The list of modes is followed by a module

  2473   name.  The module name is optional for modular code generation, but

  2474   must be specified for incremental code generation.

  2476   The code can either be written to a file, in which case a file name

  2477   has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded

  2478   directly into Isabelle's ML environment. In the latter case, the

  2479   \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results

  2480   interactively, for example.

  2482   The terms from which to generate code can be specified after the

  2483   \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just

  2484   as a list of terms. In the latter case, the code generator just

  2485   produces code for all constants and types occuring in the term, but

  2486   does not bind the compiled terms to ML identifiers.

  2488   Here is an example:%

  2489 \end{isamarkuptext}%

  2490 \isamarkuptrue%

  2491 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2492 \ Test\isanewline

  2493 \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}}%

  2494 \begin{isamarkuptext}%

  2495 \noindent This binds the result of compiling the given term to

  2496   the ML identifier \verb|Test.test|.%

  2497 \end{isamarkuptext}%

  2498 \isamarkuptrue%

  2499 %

  2500 \isadelimML

  2501 %

  2502 \endisadelimML

  2503 %

  2504 \isatagML

  2505 \isacommand{ML}\isamarkupfalse%

  2506 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2507 \isaantiq

  2508 assert{}%

  2509 \endisaantiq

  2510 \ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2511 \endisatagML

  2512 {\isafoldML}%

  2513 %

  2514 \isadelimML

  2515 %

  2516 \endisadelimML

  2517 %

  2518 \isamarkupsubsubsection{Configuring the code generator%

  2519 }

  2520 \isamarkuptrue%

  2521 %

  2522 \begin{isamarkuptext}%

  2523 When generating code for a complex term, the code generator

  2524   recursively calls itself for all subterms.  When it arrives at a

  2525   constant, the default strategy of the code generator is to look up

  2526   its definition and try to generate code for it.  Constants which

  2527   have no definitions that are immediately executable, may be

  2528   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

  2529   constant (given in usual term syntax -- an explicit type constraint

  2530   accounts for overloading), and a mixfix template describing the ML

  2531   code. The latter is very much the same as the mixfix templates used

  2532   when declaring new constants.  The most notable difference is that

  2533   terms may be included in the ML template using antiquotation

  2534   brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.

  2536   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.

  2538   For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of

  2539   Isabelle/HOL should be compiled to ML.%

  2540 \end{isamarkuptext}%

  2541 \isamarkuptrue%

  2542 \isacommand{typedecl}\isamarkupfalse%

  2543 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline

  2544 \isacommand{consts}\isamarkupfalse%

  2545 \ 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

  2546 \isanewline

  2547 \isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2548 \ 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

  2549 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2550 \ 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}}%

  2551 \begin{isamarkuptext}%

  2552 Sometimes, the code associated with a constant or type may

  2553   need to refer to auxiliary functions, which have to be emitted when

  2554   the constant is used. Code for such auxiliary functions can be

  2555   declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}

  2556   function can be implemented as follows:%

  2557 \end{isamarkuptext}%

  2558 \isamarkuptrue%

  2559 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2560 \ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline

  2561 \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}}%

  2562 \begin{isamarkuptext}%

  2563 If the code containing a call to \isa{wfrec} resides in an

  2564   ML structure different from the one containing the function

  2565   definition attached to \isa{wfrec}, the name of the ML structure

  2566   (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

  2567   the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not

  2568   executable.

  2570   \medskip Another possibility of configuring the code generator is to

  2571   register theorems to be used for code generation. Theorems can be

  2572   registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional

  2573   name as an argument, which indicates the format of the

  2574   theorem. Currently supported formats are equations (this is the

  2575   default when no name is specified) and horn clauses (this is

  2576   indicated by the name \texttt{ind}). The left-hand sides of

  2577   equations may only contain constructors and distinct variables,

  2578   whereas horn clauses must have the same format as introduction rules

  2579   of inductive definitions.

  2581   The following example specifies three equations from which to

  2582   generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also

  2583   \verb|~~/src/HOL/Nat.thy|).%

  2584 \end{isamarkuptext}%

  2585 \isamarkuptrue%

  2586 \isacommand{lemma}\isamarkupfalse%

  2587 \ {\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

  2588 \ \ \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

  2589 \ \ \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}}%

  2590 \isadelimproof

  2591 \ %

  2592 \endisadelimproof

  2593 %

  2594 \isatagproof

  2595 \isacommand{by}\isamarkupfalse%

  2596 \ simp{\isaliteral{5F}{\isacharunderscore}}all%

  2597 \endisatagproof

  2598 {\isafoldproof}%

  2599 %

  2600 \isadelimproof

  2601 %

  2602 \endisadelimproof

  2603 %

  2604 \isamarkupsubsubsection{Specific HOL code generators%

  2605 }

  2606 \isamarkuptrue%

  2607 %

  2608 \begin{isamarkuptext}%

  2609 The basic code generator framework offered by Isabelle/Pure

  2610   has already been extended with additional code generators for

  2611   specific HOL constructs. These include datatypes, recursive

  2612   functions and inductive relations. The code generator for inductive

  2613   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

  2614   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}}}'',

  2615   the above expression evaluates to a sequence of possible answers. If

  2616   all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates

  2617   to a boolean value.

  2619   The following example demonstrates this for beta-reduction on lambda

  2620   terms (see also \verb|~~/src/HOL/Proofs/Lambda/Lambda.thy|).%

  2621 \end{isamarkuptext}%

  2622 \isamarkuptrue%

  2623 \isacommand{datatype}\isamarkupfalse%

  2624 \ dB\ {\isaliteral{3D}{\isacharequal}}\isanewline

  2625 \ \ \ \ Var\ nat\isanewline

  2626 \ \ {\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

  2627 \ \ {\isaliteral{7C}{\isacharbar}}\ Abs\ dB\isanewline

  2628 \isanewline

  2629 \isacommand{primrec}\isamarkupfalse%

  2630 \ lift\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2631 \isakeyword{where}\isanewline

  2632 \ \ \ \ {\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

  2633 \ \ {\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

  2634 \ \ {\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

  2635 \isanewline

  2636 \isacommand{primrec}\isamarkupfalse%

  2637 \ 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

  2638 \isakeyword{where}\isanewline

  2639 \ \ \ \ {\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

  2640 \ \ \ \ \ \ {\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

  2641 \ \ {\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

  2642 \ \ {\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

  2643 \isanewline

  2644 \isacommand{inductive}\isamarkupfalse%

  2645 \ 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

  2646 \isakeyword{where}\isanewline

  2647 \ \ \ \ 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

  2648 \ \ {\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

  2649 \ \ {\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

  2650 \ \ {\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

  2651 \isanewline

  2652 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2653 \ Test\isanewline

  2654 \isakeyword{contains}\isanewline

  2655 \ \ 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

  2656 \ \ 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}}%

  2657 \begin{isamarkuptext}%

  2658 In the above example, \verb|Test.test1| evaluates to a boolean,

  2659   whereas \verb|Test.test2| is a lazy sequence whose elements can be

  2660   inspected separately.%

  2661 \end{isamarkuptext}%

  2662 \isamarkuptrue%

  2663 %

  2664 \isadelimML

  2665 %

  2666 \endisadelimML

  2667 %

  2668 \isatagML

  2669 \isacommand{ML}\isamarkupfalse%

  2670 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2671 \isaantiq

  2672 assert{}%

  2673 \endisaantiq

  2674 \ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

  2675 \isacommand{ML}\isamarkupfalse%

  2676 \ {\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

  2677 \isacommand{ML}\isamarkupfalse%

  2678 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2679 \isaantiq

  2680 assert{}%

  2681 \endisaantiq

  2682 \ {\isaliteral{28}{\isacharparenleft}}length\ results\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2683 \endisatagML

  2684 {\isafoldML}%

  2685 %

  2686 \isadelimML

  2687 %

  2688 \endisadelimML

  2689 %

  2690 \begin{isamarkuptext}%

  2691 \medskip The theory underlying the HOL code generator is described

  2692   more detailed in \cite{Berghofer-Nipkow:2002}. More examples that

  2693   illustrate the usage of the code generator can be found e.g.\ in

  2694   \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%

  2695 \end{isamarkuptext}%

  2696 \isamarkuptrue%

  2697 %

  2698 \isamarkupsection{Definition by specification \label{sec:hol-specification}%

  2699 }

  2700 \isamarkuptrue%

  2701 %

  2702 \begin{isamarkuptext}%

  2703 \begin{matharray}{rcl}

  2704     \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}}} \\

  2705     \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}}} \\

  2706   \end{matharray}

  2708   \begin{railoutput}

  2709 \rail@begin{6}{}

  2710 \rail@bar

  2711 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]

  2712 \rail@nextbar{1}

  2713 \rail@term{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}}[]

  2714 \rail@endbar

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

  2716 \rail@plus

  2717 \rail@nont{\isa{decl}}[]

  2718 \rail@nextplus{1}

  2719 \rail@endplus

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

  2721 \rail@cr{3}

  2722 \rail@plus

  2723 \rail@bar

  2724 \rail@nextbar{4}

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

  2726 \rail@endbar

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

  2728 \rail@nextplus{5}

  2729 \rail@endplus

  2730 \rail@end

  2731 \rail@begin{2}{\isa{decl}}

  2732 \rail@bar

  2733 \rail@nextbar{1}

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

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

  2736 \rail@endbar

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

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

  2739 \rail@term{\isa{\isakeyword{overloaded}}}[]

  2740 \rail@bar

  2741 \rail@nextbar{1}

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

  2743 \rail@endbar

  2744 \rail@end

  2745 \end{railoutput}

  2748   \begin{description}

  2750   \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up a

  2751   goal stating the existence of terms with the properties specified to

  2752   hold for the constants given in \isa{decls}.  After finishing the

  2753   proof, the theory will be augmented with definitions for the given

  2754   constants, as well as with theorems stating the properties for these

  2755   constants.

  2757   \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

  2758   a goal stating the existence of terms with the properties specified

  2759   to hold for the constants given in \isa{decls}.  After finishing

  2760   the proof, the theory will be augmented with axioms expressing the

  2761   properties given in the first place.

  2763   \item \isa{decl} declares a constant to be defined by the

  2764   specification given.  The definition for the constant \isa{c} is

  2765   bound to the name \isa{c{\isaliteral{5F}{\isacharunderscore}}def} unless a theorem name is given in

  2766   the declaration.  Overloaded constants should be declared as such.

  2768   \end{description}

  2770   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

  2771   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

  2772   user has explicitly proven it to be safe.  A practical issue must be

  2773   considered, though: After introducing two constants with the same

  2774   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove

  2775   that the two constants are, in fact, equal.  If this might be a

  2776   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}.%

  2777 \end{isamarkuptext}%

  2778 \isamarkuptrue%

  2779 %

  2780 \isadelimtheory

  2781 %

  2782 \endisadelimtheory

  2783 %

  2784 \isatagtheory

  2785 \isacommand{end}\isamarkupfalse%

  2786 %

  2787 \endisatagtheory

  2788 {\isafoldtheory}%

  2789 %

  2790 \isadelimtheory

  2791 %

  2792 \endisadelimtheory

  2793 \isanewline

  2794 \end{isabellebody}%

  2795 %%% Local Variables:

  2796 %%% mode: latex

  2797 %%% TeX-master: "root"

  2798 %%% End:

author	wenzelm
	Wed, 25 May 2011 22:21:38 +0200
changeset 44112	eb94cfaaf5d4
parent 44111	dfd4ef8e73f6
child 44113	66b189dc5b83
permissions	-rw-r--r--