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

1 %

     2 \begin{isabellebody}%

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

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

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

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

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

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

    22 }

    23 \isamarkuptrue%

    24 %

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

    26 }

    27 \isamarkuptrue%

    28 %

    29 \begin{isamarkuptext}%

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

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

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

    33   structural operational semantics is an inductive definition of an

    34   evaluation relation.

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

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

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

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

    40   relations to formalise equivalence of processes and infinite data

    41   structures.

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

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

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

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

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

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

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

    50   to use inference rules for type-checking.

    52   \begin{matharray}{rcl}

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

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

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

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

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

    58   \end{matharray}

    60   \begin{railoutput}

    61 \rail@begin{7}{}

    62 \rail@bar

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

    64 \rail@nextbar{1}

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

    66 \rail@nextbar{2}

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

    68 \rail@nextbar{3}

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

    70 \rail@endbar

    71 \rail@bar

    72 \rail@nextbar{1}

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

    74 \rail@endbar

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

    76 \rail@bar

    77 \rail@nextbar{1}

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

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

    80 \rail@endbar

    81 \rail@cr{5}

    82 \rail@bar

    83 \rail@nextbar{6}

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

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

    86 \rail@endbar

    87 \rail@bar

    88 \rail@nextbar{6}

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

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

    91 \rail@endbar

    92 \rail@end

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

    94 \rail@plus

    95 \rail@bar

    96 \rail@nextbar{1}

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

    98 \rail@endbar

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

   100 \rail@nextplus{2}

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

   102 \rail@endplus

   103 \rail@end

   104 \rail@begin{3}{}

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

   106 \rail@bar

   107 \rail@nextbar{1}

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

   109 \rail@nextbar{2}

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

   111 \rail@endbar

   112 \rail@end

   113 \end{railoutput}

   116   \begin{description}

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

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

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

   121   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

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

   129   allowing the definition of (co)inductive sets.

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

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

   134   \end{description}%

   135 \end{isamarkuptext}%

   136 \isamarkuptrue%

   137 %

   138 \isamarkupsubsection{Derived rules%

   139 }

   140 \isamarkuptrue%

   141 %

   142 \begin{isamarkuptext}%

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

   144   theory and also proves some theorems:

   146   \begin{description}

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

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

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

   151   theory file;

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

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

   156   rule.

   158   \end{description}

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

   161   defined simultaneously, the list of introduction rules is called

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

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

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

   165 \end{isamarkuptext}%

   166 \isamarkuptrue%

   167 %

   168 \isamarkupsubsection{Monotonicity theorems%

   169 }

   170 \isamarkuptrue%

   171 %

   172 \begin{isamarkuptext}%

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

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

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

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

   177   theorems may be added:

   179   \begin{itemize}

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

   182   monotonicity of inductive definitions whose introduction rules have

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

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

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

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

   188   \[

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

   190   \]

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

   193   of expressions, e.g.

   194   \[

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

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

   197   \]

   199   \item Equations for reducing complex operators to more primitive

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

   201   \[

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

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

   204   \]

   206   \end{itemize}

   208   %FIXME: Example of an inductive definition%

   209 \end{isamarkuptext}%

   210 \isamarkuptrue%

   211 %

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

   213 }

   214 \isamarkuptrue%

   215 %

   216 \begin{isamarkuptext}%

   217 \begin{matharray}{rcl}

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

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

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

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

   222   \end{matharray}

   224   \begin{railoutput}

   225 \rail@begin{2}{}

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

   227 \rail@bar

   228 \rail@nextbar{1}

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

   230 \rail@endbar

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

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

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

   234 \rail@end

   235 \rail@begin{4}{}

   236 \rail@bar

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

   238 \rail@nextbar{1}

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

   240 \rail@endbar

   241 \rail@bar

   242 \rail@nextbar{1}

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

   244 \rail@endbar

   245 \rail@bar

   246 \rail@nextbar{1}

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

   248 \rail@endbar

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

   250 \rail@cr{3}

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

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

   253 \rail@end

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

   255 \rail@plus

   256 \rail@bar

   257 \rail@nextbar{1}

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

   259 \rail@endbar

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

   261 \rail@nextplus{2}

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

   263 \rail@endplus

   264 \rail@end

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

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

   267 \rail@plus

   268 \rail@bar

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

   270 \rail@nextbar{1}

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

   272 \rail@endbar

   273 \rail@nextplus{2}

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

   275 \rail@endplus

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

   277 \rail@end

   278 \rail@begin{2}{}

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

   280 \rail@bar

   281 \rail@nextbar{1}

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

   283 \rail@endbar

   284 \rail@end

   285 \end{railoutput}

   288   \begin{description}

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

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

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

   294   wellfounded recursion. A detailed description with examples can be

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

   296   set of (possibly conditional) recursive equations with arbitrary

   297   pattern matching. The command generates proof obligations for the

   298   completeness and the compatibility of patterns.

   300   The defined function is considered partial, and the resulting

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

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

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

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

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

   307   proof attempts regarding pattern matching and termination.  See

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

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

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

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

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

   314   the induction principle is established.

   316   \end{description}

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

   319   command accommodate

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

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

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

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

   325   with structural recursion on the datatype the recursion is carried

   326   out.

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

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

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

   331   explicitly as well.

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

   334   options.

   336   \begin{description}

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

   339   overlapping patterns by making them mutually disjoint.  Earlier

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

   341   specification in a format very similar to functional programming.

   342   Note that the resulting simplification and induction rules

   343   correspond to the transformed specification, not the one given

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

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

   346   transformation only works for ML-style datatype patterns.

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

   349   introduction rules for the domain predicate. While mostly not

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

   352   \end{description}%

   353 \end{isamarkuptext}%

   354 \isamarkuptrue%

   355 %

   356 \isamarkupsubsection{Proof methods related to recursive definitions%

   357 }

   358 \isamarkuptrue%

   359 %

   360 \begin{isamarkuptext}%

   361 \begin{matharray}{rcl}

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

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

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

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

   366   \end{matharray}

   368   \begin{railoutput}

   369 \rail@begin{1}{}

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

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

   372 \rail@end

   373 \rail@begin{2}{}

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

   375 \rail@plus

   376 \rail@nextplus{1}

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

   378 \rail@endplus

   379 \rail@end

   380 \rail@begin{2}{}

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

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

   383 \rail@plus

   384 \rail@nextplus{1}

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

   386 \rail@endplus

   387 \rail@end

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

   389 \rail@plus

   390 \rail@nextplus{1}

   391 \rail@bar

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

   393 \rail@nextbar{2}

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

   395 \rail@nextbar{3}

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

   397 \rail@endbar

   398 \rail@endplus

   399 \rail@end

   400 \end{railoutput}

   403   \begin{description}

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

   406   solve goals regarding the completeness of pattern matching, as

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

   408   \cite{isabelle-function}).

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

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

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

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

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

   415   termination proofs.

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

   418   automated termination proof by searching for a lexicographic

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

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

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

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

   423   \secref{sec:clasimp}.

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

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

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

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

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

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

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

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

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

   435   internally.

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

   439   \end{description}%

   440 \end{isamarkuptext}%

   441 \isamarkuptrue%

   442 %

   443 \isamarkupsubsection{Functions with explicit partiality%

   444 }

   445 \isamarkuptrue%

   446 %

   447 \begin{isamarkuptext}%

   448 \begin{matharray}{rcl}

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

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

   451   \end{matharray}

   453   \begin{railoutput}

   454 \rail@begin{5}{}

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

   456 \rail@bar

   457 \rail@nextbar{1}

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

   459 \rail@endbar

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

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

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

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

   464 \rail@cr{3}

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

   466 \rail@bar

   467 \rail@nextbar{4}

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

   469 \rail@endbar

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

   471 \rail@end

   472 \end{railoutput}

   475   \begin{description}

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

   478   recursive functions based on fixpoints in complete partial

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

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

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

   482   explicit bottom element.

   484   Pattern matching and mutual recursion are currently not supported.

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

   486   single recursive equation.

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

   489   function, but the induced functional must be provably monotonic

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

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

   492   can be influenced by declaring hints using the

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

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

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

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

   498   defined:

   500   \begin{description}

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

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

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

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

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

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

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

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

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

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

   512   definition of arbitrary tail-recursive functions.

   513   \end{description}

   515   Experienced users may define new modes by instantiating the locale

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

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

   519   use in the internal monononicity proofs of partial function

   520   definitions.

   522   \end{description}%

   523 \end{isamarkuptext}%

   524 \isamarkuptrue%

   525 %

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

   527 }

   528 \isamarkuptrue%

   529 %

   530 \begin{isamarkuptext}%

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

   533   \begin{matharray}{rcl}

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

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

   536   \end{matharray}

   538   \begin{railoutput}

   539 \rail@begin{5}{}

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

   541 \rail@bar

   542 \rail@nextbar{1}

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

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

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

   546 \rail@endbar

   547 \rail@cr{3}

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

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

   550 \rail@plus

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

   552 \rail@nextplus{4}

   553 \rail@endplus

   554 \rail@bar

   555 \rail@nextbar{4}

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

   557 \rail@endbar

   558 \rail@end

   559 \rail@begin{2}{}

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

   561 \rail@bar

   562 \rail@nextbar{1}

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

   564 \rail@endbar

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

   566 \rail@end

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

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

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

   570 \rail@plus

   571 \rail@nextplus{1}

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

   573 \rail@endplus

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

   575 \rail@end

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

   577 \rail@bar

   578 \rail@bar

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

   580 \rail@nextbar{1}

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

   582 \rail@nextbar{2}

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

   584 \rail@endbar

   585 \rail@bar

   586 \rail@nextbar{1}

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

   588 \rail@nextbar{2}

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

   590 \rail@endbar

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

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

   593 \rail@nextbar{3}

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

   595 \rail@endbar

   596 \rail@end

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

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

   599 \rail@bar

   600 \rail@nextbar{1}

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

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

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

   604 \rail@endbar

   605 \rail@end

   606 \end{railoutput}

   609   \begin{description}

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

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

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

   614   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

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

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

   624   constant \isa{c}.

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

   627   its internal proofs without manual intervention.

   629   \end{description}

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

   632   globally, using the following attributes.

   634   \begin{matharray}{rcl}

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

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

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

   638   \end{matharray}

   640   \begin{railoutput}

   641 \rail@begin{3}{}

   642 \rail@bar

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

   644 \rail@nextbar{1}

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

   646 \rail@nextbar{2}

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

   648 \rail@endbar

   649 \rail@bar

   650 \rail@nextbar{1}

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

   652 \rail@nextbar{2}

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

   654 \rail@endbar

   655 \rail@end

   656 \end{railoutput}%

   657 \end{isamarkuptext}%

   658 \isamarkuptrue%

   659 %

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

   661 }

   662 \isamarkuptrue%

   663 %

   664 \begin{isamarkuptext}%

   665 \begin{matharray}{rcl}

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

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

   668   \end{matharray}

   670   \begin{railoutput}

   671 \rail@begin{2}{}

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

   673 \rail@plus

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

   675 \rail@nextplus{1}

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

   677 \rail@endplus

   678 \rail@end

   679 \rail@begin{3}{}

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

   681 \rail@bar

   682 \rail@nextbar{1}

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

   684 \rail@plus

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

   686 \rail@nextplus{2}

   687 \rail@endplus

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

   689 \rail@endbar

   690 \rail@plus

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

   692 \rail@nextplus{1}

   693 \rail@endplus

   694 \rail@end

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

   696 \rail@bar

   697 \rail@nextbar{1}

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

   699 \rail@endbar

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

   701 \rail@bar

   702 \rail@nextbar{1}

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

   704 \rail@endbar

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

   706 \rail@plus

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

   708 \rail@nextplus{1}

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

   710 \rail@endplus

   711 \rail@end

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

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

   714 \rail@plus

   715 \rail@nextplus{1}

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

   717 \rail@endplus

   718 \rail@bar

   719 \rail@nextbar{1}

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

   721 \rail@endbar

   722 \rail@end

   723 \end{railoutput}

   726   \begin{description}

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

   729   HOL.

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

   732   datatypes.

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

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

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

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

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

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

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

   741   injectivity of constructors.

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

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

   746   \end{description}

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

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

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

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

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

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

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

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

   757   internally bound parameters).%

   758 \end{isamarkuptext}%

   759 \isamarkuptrue%

   760 %

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

   762 }

   763 \isamarkuptrue%

   764 %

   765 \begin{isamarkuptext}%

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

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

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

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

   770   admits operations that are polymorphic with respect to record

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

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

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

   774 \end{isamarkuptext}%

   775 \isamarkuptrue%

   776 %

   777 \isamarkupsubsection{Basic concepts%

   778 }

   779 \isamarkuptrue%

   780 %

   781 \begin{isamarkuptext}%

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

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

   785   \begin{center}

   786   \begin{tabular}{l|l|l}

   787     & record terms & record types \\ \hline

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

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

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

   791   \end{tabular}

   792   \end{center}

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

   796   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

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

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

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

   801   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

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

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

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

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

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

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

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

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

   810   Fixed records are special instances of record schemes, where

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

   812   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

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

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

   816   typed language like HOL work out:

   818   \begin{enumerate}

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

   821   variable,

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

   824   the logic as first-class values.

   826   \end{enumerate}

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

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

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

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

   832   The record package provides several standard operations like

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

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

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

   836   records in practice.%

   837 \end{isamarkuptext}%

   838 \isamarkuptrue%

   839 %

   840 \isamarkupsubsection{Record specifications%

   841 }

   842 \isamarkuptrue%

   843 %

   844 \begin{isamarkuptext}%

   845 \begin{matharray}{rcl}

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

   847   \end{matharray}

   849   \begin{railoutput}

   850 \rail@begin{4}{}

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

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

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

   854 \rail@cr{2}

   855 \rail@bar

   856 \rail@nextbar{3}

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

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

   859 \rail@endbar

   860 \rail@plus

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

   862 \rail@nextplus{3}

   863 \rail@endplus

   864 \rail@end

   865 \end{railoutput}

   868   \begin{description}

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

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

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

   874   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

   875   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

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

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

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

   879   the record name internally.

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

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

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

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

   885   merge multiple parent records!

   887   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

   888   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

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

   891   \end{description}%

   892 \end{isamarkuptext}%

   893 \isamarkuptrue%

   894 %

   895 \isamarkupsubsection{Record operations%

   896 }

   897 \isamarkuptrue%

   898 %

   899 \begin{isamarkuptext}%

   900 Any record definition of the form presented above produces certain

   901   standard operations.  Selectors and updates are provided for any

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

   903   cumulative record constructor functions.  To simplify the

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

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

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

   909   \begin{matharray}{lll}

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

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

   912   \end{matharray}

   914   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

   915   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

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

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

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

   919   Thus commutativity of independent updates can be proven within the

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

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

   923   constructor function:

   925   \begin{matharray}{lll}

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

   927   \end{matharray}

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

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

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

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

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

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

   935   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

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

   937   the above record operations will get the following types:

   939   \medskip

   940   \begin{tabular}{lll}

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

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

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

   944   \end{tabular}

   945   \medskip

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

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

   949   record fragment consisting of exactly the new fields introduced here

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

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

   953   \medskip

   954   \begin{tabular}{lll}

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

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

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

   958   \end{tabular}

   959   \medskip

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

   962   for root records.%

   963 \end{isamarkuptext}%

   964 \isamarkuptrue%

   965 %

   966 \isamarkupsubsection{Derived rules and proof tools%

   967 }

   968 \isamarkuptrue%

   969 %

   970 \begin{isamarkuptext}%

   971 The record package proves several results internally, declaring

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

   973   reason about record structures quite conveniently.  Assume that

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

   976   \begin{enumerate}

   978   \item Standard conversions for selectors or updates applied to

   979   record constructor terms are made part of the default Simplifier

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

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

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

   984   \item Selectors applied to updated records are automatically reduced

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

   986   standard Simplifier setup.

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

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

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

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

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

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

   996   \item Representations of arbitrary record expressions as canonical

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

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

   999   fixed records, record schemes, more parts etc.

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

  1002   sensible rule according to the type of the indicated record

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

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

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

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

  1009   \end{enumerate}%

  1010 \end{isamarkuptext}%

  1011 \isamarkuptrue%

  1012 %

  1013 \isamarkupsection{Adhoc tuples%

  1014 }

  1015 \isamarkuptrue%

  1016 %

  1017 \begin{isamarkuptext}%

  1018 \begin{matharray}{rcl}

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

  1020   \end{matharray}

  1022   \begin{railoutput}

  1023 \rail@begin{2}{}

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

  1025 \rail@bar

  1026 \rail@nextbar{1}

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

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

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

  1030 \rail@endbar

  1031 \rail@end

  1032 \end{railoutput}

  1035   \begin{description}

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

  1038   arguments in function applications to be represented canonically

  1039   according to their tuple type structure.

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

  1042   parameters introduced.

  1044   \end{description}%

  1045 \end{isamarkuptext}%

  1046 \isamarkuptrue%

  1047 %

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

  1049 }

  1050 \isamarkuptrue%

  1051 %

  1052 \begin{isamarkuptext}%

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

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

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

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

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

  1058   postulated that establish an isomorphism between the new type and

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

  1060   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

  1061   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

  1062   those type arguments.

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

  1065   of the particular set-theoretic interpretation of HOL

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

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

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

  1069   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

  1070   abbreviations, without any logical significance.

  1072   \begin{matharray}{rcl}

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

  1074   \end{matharray}

  1076   \begin{railoutput}

  1077 \rail@begin{2}{}

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

  1079 \rail@bar

  1080 \rail@nextbar{1}

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

  1082 \rail@endbar

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

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

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

  1086 \rail@end

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

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

  1089 \rail@bar

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

  1091 \rail@nextbar{1}

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

  1093 \rail@nextbar{2}

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

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

  1096 \rail@endbar

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

  1098 \rail@end

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

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

  1101 \rail@bar

  1102 \rail@nextbar{1}

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

  1104 \rail@endbar

  1105 \rail@end

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

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

  1108 \rail@bar

  1109 \rail@nextbar{1}

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

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

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

  1113 \rail@endbar

  1114 \rail@end

  1115 \end{railoutput}

  1118   \begin{description}

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

  1121   axiomatizes a type definition in the background theory of the

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

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

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

  1125   but no term variables.

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

  1128   constructor cannot depend on parameters or assumptions of the

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

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

  1131   which could result in different interpretations in target contexts:

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

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

  1134   contexts.

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

  1137   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

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

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

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

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

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

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

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

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

  1148   provide the most basic characterization as a corresponding

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

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

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

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

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

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

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

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

  1157   respectively.

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

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

  1161   \isa{t} directly.

  1163   \end{description}

  1165   \begin{warn}

  1166   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

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

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

  1169   interpretation of such free-form axiomatizations can coexist with

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

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

  1172   \cite{MuellerNvOS99}).

  1173   \end{warn}%

  1174 \end{isamarkuptext}%

  1175 \isamarkuptrue%

  1176 %

  1177 \isamarkupsubsubsection{Examples%

  1178 }

  1179 \isamarkuptrue%

  1180 %

  1181 \begin{isamarkuptext}%

  1182 Type definitions permit the introduction of abstract data

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

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

  1185   of a type, this involves two steps:

  1187   \begin{enumerate}

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

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

  1191   based on this representation.

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

  1194   from the representation.

  1196   \end{enumerate}

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

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

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

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

  1203 \end{isamarkuptext}%

  1204 \isamarkuptrue%

  1205 \isacommand{typedef}\isamarkupfalse%

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

  1207 %

  1208 \isadelimproof

  1209 \ \ %

  1210 \endisadelimproof

  1211 %

  1212 \isatagproof

  1213 \isacommand{by}\isamarkupfalse%

  1214 \ blast%

  1215 \endisatagproof

  1216 {\isafoldproof}%

  1217 %

  1218 \isadelimproof

  1219 \isanewline

  1220 %

  1221 \endisadelimproof

  1222 \isanewline

  1223 \isacommand{definition}\isamarkupfalse%

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

  1225 \isacommand{definition}\isamarkupfalse%

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

  1227 \isacommand{definition}\isamarkupfalse%

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

  1229 \isanewline

  1230 \isacommand{lemma}\isamarkupfalse%

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

  1232 %

  1233 \isadelimproof

  1234 \ \ %

  1235 \endisadelimproof

  1236 %

  1237 \isatagproof

  1238 \isacommand{by}\isamarkupfalse%

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

  1240 \endisatagproof

  1241 {\isafoldproof}%

  1242 %

  1243 \isadelimproof

  1244 \isanewline

  1245 %

  1246 \endisadelimproof

  1247 \isanewline

  1248 \isacommand{lemma}\isamarkupfalse%

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

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

  1251 %

  1252 \isadelimproof

  1253 \ \ %

  1254 \endisadelimproof

  1255 %

  1256 \isatagproof

  1257 \isacommand{by}\isamarkupfalse%

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

  1259 \endisatagproof

  1260 {\isafoldproof}%

  1261 %

  1262 \isadelimproof

  1263 %

  1264 \endisadelimproof

  1265 %

  1266 \begin{isamarkuptext}%

  1267 Note that such trivial constructions are better done with

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

  1269 \end{isamarkuptext}%

  1270 \isamarkuptrue%

  1271 \isacommand{datatype}\isamarkupfalse%

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

  1273 \begin{isamarkuptext}%

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

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

  1276 \end{isamarkuptext}%

  1277 \isamarkuptrue%

  1278 %

  1279 \isamarkupsection{Functorial structure of types%

  1280 }

  1281 \isamarkuptrue%

  1282 %

  1283 \begin{isamarkuptext}%

  1284 \begin{matharray}{rcl}

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

  1286   \end{matharray}

  1288   \begin{railoutput}

  1289 \rail@begin{2}{}

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

  1291 \rail@bar

  1292 \rail@nextbar{1}

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

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

  1295 \rail@endbar

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

  1297 \rail@end

  1298 \end{railoutput}

  1301   \begin{description}

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

  1304   prove and register properties about the functorial structure of type

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

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

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

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

  1309   constructor, an explicit prefix can be given alternatively.

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

  1312   corresponding type constructor and must conform to the following

  1313   type pattern:

  1315   \begin{matharray}{lll}

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

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

  1318   \end{matharray}

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

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

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

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

  1325   \end{description}%

  1326 \end{isamarkuptext}%

  1327 \isamarkuptrue%

  1328 %

  1329 \isamarkupsection{Arithmetic proof support%

  1330 }

  1331 \isamarkuptrue%

  1332 %

  1333 \begin{isamarkuptext}%

  1334 \begin{matharray}{rcl}

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

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

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

  1338   \end{matharray}

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

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

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

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

  1345   always supplied to the arithmetic provers implicitly.

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

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

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

  1351   already invoked by the Simplifier.%

  1352 \end{isamarkuptext}%

  1353 \isamarkuptrue%

  1354 %

  1355 \isamarkupsection{Intuitionistic proof search%

  1356 }

  1357 \isamarkuptrue%

  1358 %

  1359 \begin{isamarkuptext}%

  1360 \begin{matharray}{rcl}

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

  1362   \end{matharray}

  1364   \begin{railoutput}

  1365 \rail@begin{2}{}

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

  1367 \rail@plus

  1368 \rail@nextplus{1}

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

  1370 \rail@endplus

  1371 \rail@end

  1372 \end{railoutput}

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

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

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

  1378   goal before commencing proof search.

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

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

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

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

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

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

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

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

  1388 \end{isamarkuptext}%

  1389 \isamarkuptrue%

  1390 %

  1391 \isamarkupsection{Coherent Logic%

  1392 }

  1393 \isamarkuptrue%

  1394 %

  1395 \begin{isamarkuptext}%

  1396 \begin{matharray}{rcl}

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

  1398   \end{matharray}

  1400   \begin{railoutput}

  1401 \rail@begin{2}{}

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

  1403 \rail@bar

  1404 \rail@nextbar{1}

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

  1406 \rail@endbar

  1407 \rail@end

  1408 \end{railoutput}

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

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

  1413   applications in confluence theory, lattice theory and projective

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

  1415   examples.%

  1416 \end{isamarkuptext}%

  1417 \isamarkuptrue%

  1418 %

  1419 \isamarkupsection{Proving propositions%

  1420 }

  1421 \isamarkuptrue%

  1422 %

  1423 \begin{isamarkuptext}%

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

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

  1426   These tools are available via the following commands.

  1428   \begin{matharray}{rcl}

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

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

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

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

  1433   \end{matharray}

  1435   \begin{railoutput}

  1436 \rail@begin{6}{}

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

  1438 \rail@bar

  1439 \rail@nextbar{1}

  1440 \rail@plus

  1441 \rail@bar

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

  1443 \rail@nextbar{2}

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

  1445 \rail@nextbar{3}

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

  1447 \rail@nextbar{4}

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

  1449 \rail@endbar

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

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

  1452 \rail@nextplus{5}

  1453 \rail@endplus

  1454 \rail@endbar

  1455 \rail@bar

  1456 \rail@nextbar{1}

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

  1458 \rail@endbar

  1459 \rail@end

  1460 \rail@begin{2}{}

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

  1462 \rail@bar

  1463 \rail@nextbar{1}

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

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

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

  1467 \rail@endbar

  1468 \rail@bar

  1469 \rail@nextbar{1}

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

  1471 \rail@endbar

  1472 \rail@bar

  1473 \rail@nextbar{1}

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

  1475 \rail@endbar

  1476 \rail@end

  1477 \rail@begin{2}{}

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

  1479 \rail@bar

  1480 \rail@nextbar{1}

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

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

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

  1484 \rail@endbar

  1485 \rail@end

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

  1487 \rail@plus

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

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

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

  1491 \rail@nextplus{1}

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

  1493 \rail@endplus

  1494 \rail@end

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

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

  1497 \rail@bar

  1498 \rail@nextbar{1}

  1499 \rail@plus

  1500 \rail@bar

  1501 \rail@nextbar{2}

  1502 \rail@bar

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

  1504 \rail@nextbar{3}

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

  1506 \rail@endbar

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

  1508 \rail@endbar

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

  1510 \rail@nextplus{4}

  1511 \rail@endplus

  1512 \rail@endbar

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

  1514 \rail@end

  1515 \end{railoutput}

  1516  % FIXME try: proper clasimpmod!?

  1517   % FIXME check args "value"

  1519   \begin{description}

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

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

  1523     in this way.

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

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

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

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

  1529     methods.

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

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

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

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

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

  1538   \end{description}%

  1539 \end{isamarkuptext}%

  1540 \isamarkuptrue%

  1541 %

  1542 \isamarkupsection{Checking and refuting propositions%

  1543 }

  1544 \isamarkuptrue%

  1545 %

  1546 \begin{isamarkuptext}%

  1547 Identifying incorrect propositions usually involves evaluation of

  1548   particular assignments and systematic counterexample search.  This

  1549   is supported by the following commands.

  1551   \begin{matharray}{rcl}

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

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

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

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

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

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

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

  1559   \end{matharray}

  1561   \begin{railoutput}

  1562 \rail@begin{2}{}

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

  1564 \rail@bar

  1565 \rail@nextbar{1}

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

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

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

  1569 \rail@endbar

  1570 \rail@bar

  1571 \rail@nextbar{1}

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

  1573 \rail@endbar

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

  1575 \rail@end

  1576 \rail@begin{3}{}

  1577 \rail@bar

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

  1579 \rail@nextbar{1}

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

  1581 \rail@nextbar{2}

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

  1583 \rail@endbar

  1584 \rail@bar

  1585 \rail@nextbar{1}

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

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

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

  1589 \rail@endbar

  1590 \rail@bar

  1591 \rail@nextbar{1}

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

  1593 \rail@endbar

  1594 \rail@end

  1595 \rail@begin{3}{}

  1596 \rail@bar

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

  1598 \rail@nextbar{1}

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

  1600 \rail@nextbar{2}

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

  1602 \rail@endbar

  1603 \rail@bar

  1604 \rail@nextbar{1}

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

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

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

  1608 \rail@endbar

  1609 \rail@end

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

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

  1612 \rail@plus

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

  1614 \rail@nextplus{1}

  1615 \rail@endplus

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

  1617 \rail@end

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

  1619 \rail@plus

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

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

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

  1623 \rail@nextplus{1}

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

  1625 \rail@endplus

  1626 \rail@end

  1627 \end{railoutput}

  1628  % FIXME check "value"

  1630   \begin{description}

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

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

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

  1635     Internally, the evaluation is performed by registered evaluators,

  1636     which are invoked sequentially until a result is returned.

  1637     Alternatively a specific evaluator can be selected using square

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

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

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

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

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

  1644     counterexamples using a series of assignments for its

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

  1646     can be selected explicitly using an optional goal index.

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

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

  1649     By default, quickcheck uses exhaustive testing.

  1650     A number of configuration options are supported for

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

  1653     \begin{description}

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

  1656       (e.g. exhaustive or random).

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

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

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

  1660     for assignment values.

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

  1663       these terms under the variable assignment found by quickcheck.

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

  1666     generated for each particular size.

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

  1669     structured proofs should be ignored.

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

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

  1674     instantiate type variables.

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

  1677     fulfilled the preconditions.

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

  1680     current size for assignment values.

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

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

  1685     \end{description}

  1687     These option can be given within square brackets.

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

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

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

  1693     counterexamples using a reduction to SAT. The following configuration

  1694     options are supported:

  1696     \begin{description}

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

  1699       models to search for.

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

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

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

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

  1706     Nonpositive values mean $\infty$.

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

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

  1711     structured proofs should be ignored.

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

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

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

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

  1719     \end{description}

  1721     These option can be given within square brackets.

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

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

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

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

  1728     \cite{isabelle-nitpick} for details.

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

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

  1733   \end{description}%

  1734 \end{isamarkuptext}%

  1735 \isamarkuptrue%

  1736 %

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

  1738 }

  1739 \isamarkuptrue%

  1740 %

  1741 \begin{isamarkuptext}%

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

  1743   induction in unstructured tactic scripts; see also

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

  1746   \begin{matharray}{rcl}

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

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

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

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

  1751   \end{matharray}

  1753   \begin{railoutput}

  1754 \rail@begin{2}{}

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

  1756 \rail@bar

  1757 \rail@nextbar{1}

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

  1759 \rail@endbar

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

  1761 \rail@bar

  1762 \rail@nextbar{1}

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

  1764 \rail@endbar

  1765 \rail@end

  1766 \rail@begin{3}{}

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

  1768 \rail@bar

  1769 \rail@nextbar{1}

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

  1771 \rail@endbar

  1772 \rail@bar

  1773 \rail@nextbar{1}

  1774 \rail@plus

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

  1776 \rail@nextplus{2}

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

  1778 \rail@endplus

  1779 \rail@endbar

  1780 \rail@bar

  1781 \rail@nextbar{1}

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

  1783 \rail@endbar

  1784 \rail@end

  1785 \rail@begin{3}{}

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

  1787 \rail@plus

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

  1789 \rail@nextplus{1}

  1790 \rail@endplus

  1791 \rail@bar

  1792 \rail@nextbar{1}

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

  1794 \rail@plus

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

  1796 \rail@nextplus{2}

  1797 \rail@endplus

  1798 \rail@endbar

  1799 \rail@end

  1800 \rail@begin{3}{}

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

  1802 \rail@plus

  1803 \rail@bar

  1804 \rail@nextbar{1}

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

  1806 \rail@endbar

  1807 \rail@plus

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

  1809 \rail@nextplus{1}

  1810 \rail@endplus

  1811 \rail@nextplus{2}

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

  1813 \rail@endplus

  1814 \rail@end

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

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

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

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

  1819 \rail@end

  1820 \end{railoutput}

  1823   \begin{description}

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

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

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

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

  1830   These unstructured tactics feature both goal addressing and dynamic

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

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

  1833   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

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

  1835   being addressed.

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

  1838   forward manner.

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

  1841   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

  1842   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

  1843   be generalized before applying the resulting rule.

  1845   \end{description}%

  1846 \end{isamarkuptext}%

  1847 \isamarkuptrue%

  1848 %

  1849 \isamarkupsection{Executable code%

  1850 }

  1851 \isamarkuptrue%

  1852 %

  1853 \begin{isamarkuptext}%

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

  1855   specifications.  In principle, execution could be simulated by

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

  1857   simplification.  Unfortunately, this approach is rather inefficient.

  1858   A more efficient way of executing specifications is to translate

  1859   them into a functional programming language such as ML.

  1861   Isabelle provides two generic frameworks to support code generation

  1862   from executable specifications.  Isabelle/HOL instantiates these

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

  1864 \end{isamarkuptext}%

  1865 \isamarkuptrue%

  1866 %

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

  1868 }

  1869 \isamarkuptrue%

  1870 %

  1871 \begin{isamarkuptext}%

  1872 This framework generates code from functional programs

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

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

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

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

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

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

  1879   Inductive specifications can be executed using the predicate

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

  1881   an introduction.

  1883   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1903   \end{matharray}

  1905   \begin{railoutput}

  1906 \rail@begin{11}{}

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

  1908 \rail@plus

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

  1910 \rail@nextplus{1}

  1911 \rail@endplus

  1912 \rail@cr{3}

  1913 \rail@bar

  1914 \rail@nextbar{4}

  1915 \rail@plus

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

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

  1918 \rail@bar

  1919 \rail@nextbar{5}

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

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

  1922 \rail@endbar

  1923 \rail@cr{7}

  1924 \rail@bar

  1925 \rail@nextbar{8}

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

  1927 \rail@bar

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

  1929 \rail@nextbar{9}

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

  1931 \rail@endbar

  1932 \rail@endbar

  1933 \rail@bar

  1934 \rail@nextbar{8}

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

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

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

  1938 \rail@endbar

  1939 \rail@nextplus{10}

  1940 \rail@endplus

  1941 \rail@endbar

  1942 \rail@end

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

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

  1945 \rail@end

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

  1947 \rail@bar

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

  1949 \rail@nextbar{1}

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

  1951 \rail@nextbar{2}

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

  1953 \rail@endbar

  1954 \rail@end

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

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

  1957 \rail@end

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

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

  1960 \rail@end

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

  1962 \rail@bar

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

  1964 \rail@nextbar{1}

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

  1966 \rail@nextbar{2}

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

  1968 \rail@nextbar{3}

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

  1970 \rail@endbar

  1971 \rail@end

  1972 \rail@begin{4}{}

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

  1974 \rail@bar

  1975 \rail@nextbar{1}

  1976 \rail@bar

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

  1978 \rail@nextbar{2}

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

  1980 \rail@nextbar{3}

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

  1982 \rail@endbar

  1983 \rail@endbar

  1984 \rail@end

  1985 \rail@begin{2}{}

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

  1987 \rail@plus

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

  1989 \rail@nextplus{1}

  1990 \rail@endplus

  1991 \rail@end

  1992 \rail@begin{2}{}

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

  1994 \rail@plus

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

  1996 \rail@nextplus{1}

  1997 \rail@endplus

  1998 \rail@end

  1999 \rail@begin{2}{}

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

  2001 \rail@bar

  2002 \rail@nextbar{1}

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

  2004 \rail@endbar

  2005 \rail@end

  2006 \rail@begin{2}{}

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

  2008 \rail@bar

  2009 \rail@nextbar{1}

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

  2011 \rail@endbar

  2012 \rail@end

  2013 \rail@begin{3}{}

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

  2015 \rail@bar

  2016 \rail@nextbar{1}

  2017 \rail@plus

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

  2019 \rail@nextplus{2}

  2020 \rail@endplus

  2021 \rail@endbar

  2022 \rail@end

  2023 \rail@begin{3}{}

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

  2025 \rail@bar

  2026 \rail@nextbar{1}

  2027 \rail@plus

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

  2029 \rail@nextplus{2}

  2030 \rail@endplus

  2031 \rail@endbar

  2032 \rail@end

  2033 \rail@begin{7}{}

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

  2035 \rail@plus

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

  2037 \rail@nextplus{1}

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

  2039 \rail@endplus

  2040 \rail@cr{3}

  2041 \rail@plus

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

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

  2044 \rail@plus

  2045 \rail@bar

  2046 \rail@nextbar{4}

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

  2048 \rail@endbar

  2049 \rail@nextplus{5}

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

  2051 \rail@endplus

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

  2053 \rail@nextplus{6}

  2054 \rail@endplus

  2055 \rail@end

  2056 \rail@begin{7}{}

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

  2058 \rail@plus

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

  2060 \rail@nextplus{1}

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

  2062 \rail@endplus

  2063 \rail@cr{3}

  2064 \rail@plus

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

  2066 \rail@nont{\isa{target}}[]

  2067 \rail@plus

  2068 \rail@bar

  2069 \rail@nextbar{4}

  2070 \rail@nont{\isa{syntax}}[]

  2071 \rail@endbar

  2072 \rail@nextplus{5}

  2073 \rail@cterm{\isa{\isakeyword{and}}}[]

  2074 \rail@endplus

  2075 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2076 \rail@nextplus{6}

  2077 \rail@endplus

  2078 \rail@end

  2079 \rail@begin{9}{}

  2080 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]

  2081 \rail@plus

  2082 \rail@nont{\isa{class}}[]

  2083 \rail@nextplus{1}

  2084 \rail@cterm{\isa{\isakeyword{and}}}[]

  2085 \rail@endplus

  2086 \rail@cr{3}

  2087 \rail@plus

  2088 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2089 \rail@nont{\isa{target}}[]

  2090 \rail@cr{5}

  2091 \rail@plus

  2092 \rail@bar

  2093 \rail@nextbar{6}

  2094 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2095 \rail@endbar

  2096 \rail@nextplus{7}

  2097 \rail@cterm{\isa{\isakeyword{and}}}[]

  2098 \rail@endplus

  2099 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2100 \rail@nextplus{8}

  2101 \rail@endplus

  2102 \rail@end

  2103 \rail@begin{7}{}

  2104 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]

  2105 \rail@plus

  2106 \rail@nont{\isa{typeconstructor}}[]

  2107 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  2108 \rail@nont{\isa{class}}[]

  2109 \rail@nextplus{1}

  2110 \rail@cterm{\isa{\isakeyword{and}}}[]

  2111 \rail@endplus

  2112 \rail@cr{3}

  2113 \rail@plus

  2114 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2115 \rail@nont{\isa{target}}[]

  2116 \rail@plus

  2117 \rail@bar

  2118 \rail@nextbar{4}

  2119 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

  2120 \rail@endbar

  2121 \rail@nextplus{5}

  2122 \rail@cterm{\isa{\isakeyword{and}}}[]

  2123 \rail@endplus

  2124 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2125 \rail@nextplus{6}

  2126 \rail@endplus

  2127 \rail@end

  2128 \rail@begin{2}{}

  2129 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]

  2130 \rail@nont{\isa{target}}[]

  2131 \rail@plus

  2132 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2133 \rail@nextplus{1}

  2134 \rail@endplus

  2135 \rail@end

  2136 \rail@begin{1}{}

  2137 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]

  2138 \rail@nont{\isa{const}}[]

  2139 \rail@nont{\isa{const}}[]

  2140 \rail@nont{\isa{target}}[]

  2141 \rail@end

  2142 \rail@begin{2}{}

  2143 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]

  2144 \rail@nont{\isa{target}}[]

  2145 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2146 \rail@bar

  2147 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2148 \rail@nextbar{1}

  2149 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]

  2150 \rail@endbar

  2151 \rail@end

  2152 \rail@begin{2}{}

  2153 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]

  2154 \rail@nont{\isa{target}}[]

  2155 \rail@plus

  2156 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2157 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2158 \rail@nextplus{1}

  2159 \rail@endplus

  2160 \rail@end

  2161 \rail@begin{11}{}

  2162 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]

  2163 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2164 \rail@cr{2}

  2165 \rail@bar

  2166 \rail@nextbar{3}

  2167 \rail@term{\isa{\isakeyword{datatypes}}}[]

  2168 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2169 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  2170 \rail@bar

  2171 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]

  2172 \rail@nextbar{4}

  2173 \rail@plus

  2174 \rail@plus

  2175 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2176 \rail@nextplus{5}

  2177 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]

  2178 \rail@endplus

  2179 \rail@nextplus{6}

  2180 \rail@cterm{\isa{\isakeyword{and}}}[]

  2181 \rail@endplus

  2182 \rail@endbar

  2183 \rail@endbar

  2184 \rail@cr{8}

  2185 \rail@bar

  2186 \rail@nextbar{9}

  2187 \rail@term{\isa{\isakeyword{functions}}}[]

  2188 \rail@plus

  2189 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2190 \rail@nextplus{10}

  2191 \rail@endplus

  2192 \rail@endbar

  2193 \rail@bar

  2194 \rail@nextbar{9}

  2195 \rail@term{\isa{\isakeyword{file}}}[]

  2196 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2197 \rail@endbar

  2198 \rail@end

  2199 \rail@begin{4}{\isa{syntax}}

  2200 \rail@bar

  2201 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2202 \rail@nextbar{1}

  2203 \rail@bar

  2204 \rail@term{\isa{\isakeyword{infix}}}[]

  2205 \rail@nextbar{2}

  2206 \rail@term{\isa{\isakeyword{infixl}}}[]

  2207 \rail@nextbar{3}

  2208 \rail@term{\isa{\isakeyword{infixr}}}[]

  2209 \rail@endbar

  2210 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

  2211 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2212 \rail@endbar

  2213 \rail@end

  2214 \end{railoutput}

  2217   \begin{description}

  2219   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} generates code for a given list

  2220   of constants in the specified target language(s).  If no

  2221   serialization instruction is given, only abstract code is generated

  2222   internally.

  2224   Constants may be specified by giving them literally, referring to

  2225   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

  2226   available by giving \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.

  2228   By default, for each involved theory one corresponding name space

  2229   module is generated.  Alternativly, a module name may be specified

  2230   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} keyword; then \emph{all} code is

  2231   placed in this module.

  2233   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

  2234   refers to a single file; for \emph{Haskell}, it refers to a whole

  2235   directory, where code is generated in multiple files reflecting the

  2236   module hierarchy.  Omitting the file specification denotes standard

  2237   output.

  2239   Serializers take an optional list of arguments in parentheses.  For

  2240   \emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits

  2241   explicit module signatures.

  2243   For \emph{Haskell} a module name prefix may be given using the

  2244   ``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a

  2245   ``\verb|deriving (Read, Show)|'' clause to each appropriate

  2246   datatype declaration.

  2248   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option

  2249   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' deselects) a code equation for code generation.

  2250   Usually packages introducing code equations provide a reasonable

  2251   default setup for selection.  Variants \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstype{\isaliteral{22}{\isachardoublequote}}} and

  2252   \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstract{\isaliteral{22}{\isachardoublequote}}} declare abstract datatype certificates or

  2253   code equations on abstract datatype representations respectively.

  2255   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}} declares constants which are not

  2256   required to have a definition by means of code equations; if needed

  2257   these are implemented by program abort instead.

  2259   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}} specifies a constructor set

  2260   for a logical type.

  2262   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on

  2263   selected code equations and code generator datatypes.

  2265   \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option

  2266   ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as

  2267   rewrite rules to any code equation during preprocessing.

  2269   \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

  2270   result of an evaluation.

  2272   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code

  2273   generator preprocessor.

  2275   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}} prints a list of theorems

  2276   representing the corresponding program containing all given

  2277   constants after preprocessing.

  2279   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes dependencies of

  2280   theorems representing the corresponding program containing all given

  2281   constants after preprocessing.

  2283   \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}} associates a list of constants

  2284   with target-specific serializations; omitting a serialization

  2285   deletes an existing serialization.

  2287   \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}} associates a list of type

  2288   constructors with target-specific serializations; omitting a

  2289   serialization deletes an existing serialization.

  2291   \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}} associates a list of classes

  2292   with target-specific class names; omitting a serialization deletes

  2293   an existing serialization.  This applies only to \emph{Haskell}.

  2295   \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}} declares a list of type

  2296   constructor / class instance relations as ``already present'' for a

  2297   given target.  Omitting a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' deletes an existing

  2298   ``already present'' declaration.  This applies only to

  2299   \emph{Haskell}.

  2301   \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}} declares a list of names as

  2302   reserved for a given target, preventing it to be shadowed by any

  2303   generated code.

  2305   \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}} provides an auxiliary mechanism

  2306   to generate monadic code for Haskell.

  2308   \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}} adds arbitrary named content

  2309   (``include'') to generated code.  A ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' as last argument

  2310   will remove an already added ``include''.

  2312   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}} declares aliasings from one

  2313   module name onto another.

  2315   \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} without a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}''

  2316   argument compiles code into the system runtime environment and

  2317   modifies the code generator setup that future invocations of system

  2318   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

  2319   entities.  With a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}'' argument, the corresponding code

  2320   is generated into that specified file without modifying the code

  2321   generator setup.

  2323   \end{description}%

  2324 \end{isamarkuptext}%

  2325 \isamarkuptrue%

  2326 %

  2327 \isamarkupsubsection{The old code generator (S. Berghofer)%

  2328 }

  2329 \isamarkuptrue%

  2330 %

  2331 \begin{isamarkuptext}%

  2332 This framework generates code from both functional and

  2333   relational programs to SML, as explained below.

  2335   \begin{matharray}{rcl}

  2336     \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}}} \\

  2337     \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}}} \\

  2338     \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}}} \\

  2339     \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}}} \\

  2340     \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\

  2341   \end{matharray}

  2343   \begin{railoutput}

  2344 \rail@begin{11}{}

  2345 \rail@bar

  2346 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]

  2347 \rail@nextbar{1}

  2348 \rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]

  2349 \rail@endbar

  2350 \rail@bar

  2351 \rail@nextbar{1}

  2352 \rail@nont{\isa{modespec}}[]

  2353 \rail@endbar

  2354 \rail@bar

  2355 \rail@nextbar{1}

  2356 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2357 \rail@endbar

  2358 \rail@cr{3}

  2359 \rail@bar

  2360 \rail@nextbar{4}

  2361 \rail@term{\isa{\isakeyword{file}}}[]

  2362 \rail@nont{\isa{name}}[]

  2363 \rail@endbar

  2364 \rail@bar

  2365 \rail@nextbar{4}

  2366 \rail@term{\isa{\isakeyword{imports}}}[]

  2367 \rail@plus

  2368 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2369 \rail@nextplus{5}

  2370 \rail@endplus

  2371 \rail@endbar

  2372 \rail@cr{7}

  2373 \rail@term{\isa{\isakeyword{contains}}}[]

  2374 \rail@bar

  2375 \rail@plus

  2376 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2377 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  2378 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2379 \rail@nextplus{8}

  2380 \rail@endplus

  2381 \rail@nextbar{9}

  2382 \rail@plus

  2383 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2384 \rail@nextplus{10}

  2385 \rail@endplus

  2386 \rail@endbar

  2387 \rail@end

  2388 \rail@begin{2}{\isa{modespec}}

  2389 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2390 \rail@plus

  2391 \rail@nextplus{1}

  2392 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2393 \rail@endplus

  2394 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2395 \rail@end

  2396 \rail@begin{2}{}

  2397 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]

  2398 \rail@plus

  2399 \rail@nont{\isa{codespec}}[]

  2400 \rail@nextplus{1}

  2401 \rail@endplus

  2402 \rail@end

  2403 \rail@begin{2}{\isa{codespec}}

  2404 \rail@nont{\isa{const}}[]

  2405 \rail@nont{\isa{template}}[]

  2406 \rail@bar

  2407 \rail@nextbar{1}

  2408 \rail@nont{\isa{attachment}}[]

  2409 \rail@endbar

  2410 \rail@end

  2411 \rail@begin{2}{}

  2412 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]

  2413 \rail@plus

  2414 \rail@nont{\isa{tycodespec}}[]

  2415 \rail@nextplus{1}

  2416 \rail@endplus

  2417 \rail@end

  2418 \rail@begin{2}{\isa{tycodespec}}

  2419 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2420 \rail@nont{\isa{template}}[]

  2421 \rail@bar

  2422 \rail@nextbar{1}

  2423 \rail@nont{\isa{attachment}}[]

  2424 \rail@endbar

  2425 \rail@end

  2426 \rail@begin{1}{\isa{const}}

  2427 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2428 \rail@end

  2429 \rail@begin{1}{\isa{template}}

  2430 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2431 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]

  2432 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2433 \rail@end

  2434 \rail@begin{2}{\isa{attachment}}

  2435 \rail@term{\isa{attach}}[]

  2436 \rail@bar

  2437 \rail@nextbar{1}

  2438 \rail@nont{\isa{modespec}}[]

  2439 \rail@endbar

  2440 \rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]

  2441 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  2442 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]

  2443 \rail@end

  2444 \rail@begin{2}{}

  2445 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]

  2446 \rail@bar

  2447 \rail@nextbar{1}

  2448 \rail@nont{\isa{name}}[]

  2449 \rail@endbar

  2450 \rail@end

  2451 \end{railoutput}%

  2452 \end{isamarkuptext}%

  2453 \isamarkuptrue%

  2454 %

  2455 \isamarkupsubsubsection{Invoking the code generator%

  2456 }

  2457 \isamarkuptrue%

  2458 %

  2459 \begin{isamarkuptext}%

  2460 The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}

  2461   and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to

  2462   \emph{incremental} and \emph{modular} code generation, respectively.

  2464   \begin{description}

  2466   \item [Modular] For each theory, an ML structure is generated,

  2467   containing the code generated from the constants defined in this

  2468   theory.

  2470   \item [Incremental] All the generated code is emitted into the same

  2471   structure.  This structure may import code from previously generated

  2472   structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.

  2473   Moreover, the generated structure may also be referred to in later

  2474   invocations of the code generator.

  2476   \end{description}

  2478   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}}}}

  2479   keywords, the user may specify an optional list of ``modes'' in

  2480   parentheses. These can be used to instruct the code generator to

  2481   emit additional code for special purposes, e.g.\ functions for

  2482   converting elements of generated datatypes to Isabelle terms, or

  2483   test data generators. The list of modes is followed by a module

  2484   name.  The module name is optional for modular code generation, but

  2485   must be specified for incremental code generation.

  2487   The code can either be written to a file, in which case a file name

  2488   has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded

  2489   directly into Isabelle's ML environment. In the latter case, the

  2490   \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results

  2491   interactively, for example.

  2493   The terms from which to generate code can be specified after the

  2494   \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just

  2495   as a list of terms. In the latter case, the code generator just

  2496   produces code for all constants and types occuring in the term, but

  2497   does not bind the compiled terms to ML identifiers.

  2499   Here is an example:%

  2500 \end{isamarkuptext}%

  2501 \isamarkuptrue%

  2502 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2503 \ Test\isanewline

  2504 \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}}%

  2505 \begin{isamarkuptext}%

  2506 \noindent This binds the result of compiling the given term to

  2507   the ML identifier \verb|Test.test|.%

  2508 \end{isamarkuptext}%

  2509 \isamarkuptrue%

  2510 %

  2511 \isadelimML

  2512 %

  2513 \endisadelimML

  2514 %

  2515 \isatagML

  2516 \isacommand{ML}\isamarkupfalse%

  2517 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2518 \isaantiq

  2519 assert{}%

  2520 \endisaantiq

  2521 \ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2522 \endisatagML

  2523 {\isafoldML}%

  2524 %

  2525 \isadelimML

  2526 %

  2527 \endisadelimML

  2528 %

  2529 \isamarkupsubsubsection{Configuring the code generator%

  2530 }

  2531 \isamarkuptrue%

  2532 %

  2533 \begin{isamarkuptext}%

  2534 When generating code for a complex term, the code generator

  2535   recursively calls itself for all subterms.  When it arrives at a

  2536   constant, the default strategy of the code generator is to look up

  2537   its definition and try to generate code for it.  Constants which

  2538   have no definitions that are immediately executable, may be

  2539   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

  2540   constant (given in usual term syntax -- an explicit type constraint

  2541   accounts for overloading), and a mixfix template describing the ML

  2542   code. The latter is very much the same as the mixfix templates used

  2543   when declaring new constants.  The most notable difference is that

  2544   terms may be included in the ML template using antiquotation

  2545   brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.

  2547   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.

  2549   For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of

  2550   Isabelle/HOL should be compiled to ML.%

  2551 \end{isamarkuptext}%

  2552 \isamarkuptrue%

  2553 \isacommand{typedecl}\isamarkupfalse%

  2554 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline

  2555 \isacommand{consts}\isamarkupfalse%

  2556 \ 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

  2557 \isanewline

  2558 \isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2559 \ 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

  2560 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2561 \ 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}}%

  2562 \begin{isamarkuptext}%

  2563 Sometimes, the code associated with a constant or type may

  2564   need to refer to auxiliary functions, which have to be emitted when

  2565   the constant is used. Code for such auxiliary functions can be

  2566   declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}

  2567   function can be implemented as follows:%

  2568 \end{isamarkuptext}%

  2569 \isamarkuptrue%

  2570 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%

  2571 \ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline

  2572 \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}}%

  2573 \begin{isamarkuptext}%

  2574 If the code containing a call to \isa{wfrec} resides in an

  2575   ML structure different from the one containing the function

  2576   definition attached to \isa{wfrec}, the name of the ML structure

  2577   (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

  2578   the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not

  2579   executable.

  2581   \medskip Another possibility of configuring the code generator is to

  2582   register theorems to be used for code generation. Theorems can be

  2583   registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional

  2584   name as an argument, which indicates the format of the

  2585   theorem. Currently supported formats are equations (this is the

  2586   default when no name is specified) and horn clauses (this is

  2587   indicated by the name \texttt{ind}). The left-hand sides of

  2588   equations may only contain constructors and distinct variables,

  2589   whereas horn clauses must have the same format as introduction rules

  2590   of inductive definitions.

  2592   The following example specifies three equations from which to

  2593   generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also

  2594   \verb|~~/src/HOL/Nat.thy|).%

  2595 \end{isamarkuptext}%

  2596 \isamarkuptrue%

  2597 \isacommand{lemma}\isamarkupfalse%

  2598 \ {\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

  2599 \ \ \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

  2600 \ \ \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}}%

  2601 \isadelimproof

  2602 \ %

  2603 \endisadelimproof

  2604 %

  2605 \isatagproof

  2606 \isacommand{by}\isamarkupfalse%

  2607 \ simp{\isaliteral{5F}{\isacharunderscore}}all%

  2608 \endisatagproof

  2609 {\isafoldproof}%

  2610 %

  2611 \isadelimproof

  2612 %

  2613 \endisadelimproof

  2614 %

  2615 \isamarkupsubsubsection{Specific HOL code generators%

  2616 }

  2617 \isamarkuptrue%

  2618 %

  2619 \begin{isamarkuptext}%

  2620 The basic code generator framework offered by Isabelle/Pure

  2621   has already been extended with additional code generators for

  2622   specific HOL constructs. These include datatypes, recursive

  2623   functions and inductive relations. The code generator for inductive

  2624   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

  2625   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}}}'',

  2626   the above expression evaluates to a sequence of possible answers. If

  2627   all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates

  2628   to a boolean value.

  2630   The following example demonstrates this for beta-reduction on lambda

  2631   terms (see also \verb|~~/src/HOL/Proofs/Lambda/Lambda.thy|).%

  2632 \end{isamarkuptext}%

  2633 \isamarkuptrue%

  2634 \isacommand{datatype}\isamarkupfalse%

  2635 \ dB\ {\isaliteral{3D}{\isacharequal}}\isanewline

  2636 \ \ \ \ Var\ nat\isanewline

  2637 \ \ {\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

  2638 \ \ {\isaliteral{7C}{\isacharbar}}\ Abs\ dB\isanewline

  2639 \isanewline

  2640 \isacommand{primrec}\isamarkupfalse%

  2641 \ lift\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2642 \isakeyword{where}\isanewline

  2643 \ \ \ \ {\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

  2644 \ \ {\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

  2645 \ \ {\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

  2646 \isanewline

  2647 \isacommand{primrec}\isamarkupfalse%

  2648 \ 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

  2649 \isakeyword{where}\isanewline

  2650 \ \ \ \ {\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

  2651 \ \ \ \ \ \ {\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

  2652 \ \ {\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

  2653 \ \ {\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

  2654 \isanewline

  2655 \isacommand{inductive}\isamarkupfalse%

  2656 \ 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

  2657 \isakeyword{where}\isanewline

  2658 \ \ \ \ 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

  2659 \ \ {\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

  2660 \ \ {\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

  2661 \ \ {\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

  2662 \isanewline

  2663 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%

  2664 \ Test\isanewline

  2665 \isakeyword{contains}\isanewline

  2666 \ \ 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

  2667 \ \ 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}}%

  2668 \begin{isamarkuptext}%

  2669 In the above example, \verb|Test.test1| evaluates to a boolean,

  2670   whereas \verb|Test.test2| is a lazy sequence whose elements can be

  2671   inspected separately.%

  2672 \end{isamarkuptext}%

  2673 \isamarkuptrue%

  2674 %

  2675 \isadelimML

  2676 %

  2677 \endisadelimML

  2678 %

  2679 \isatagML

  2680 \isacommand{ML}\isamarkupfalse%

  2681 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2682 \isaantiq

  2683 assert{}%

  2684 \endisaantiq

  2685 \ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

  2686 \isacommand{ML}\isamarkupfalse%

  2687 \ {\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

  2688 \isacommand{ML}\isamarkupfalse%

  2689 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %

  2690 \isaantiq

  2691 assert{}%

  2692 \endisaantiq

  2693 \ {\isaliteral{28}{\isacharparenleft}}length\ results\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%

  2694 \endisatagML

  2695 {\isafoldML}%

  2696 %

  2697 \isadelimML

  2698 %

  2699 \endisadelimML

  2700 %

  2701 \begin{isamarkuptext}%

  2702 \medskip The theory underlying the HOL code generator is described

  2703   more detailed in \cite{Berghofer-Nipkow:2002}. More examples that

  2704   illustrate the usage of the code generator can be found e.g.\ in

  2705   \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%

  2706 \end{isamarkuptext}%

  2707 \isamarkuptrue%

  2708 %

  2709 \isamarkupsection{Definition by specification \label{sec:hol-specification}%

  2710 }

  2711 \isamarkuptrue%

  2712 %

  2713 \begin{isamarkuptext}%

  2714 \begin{matharray}{rcl}

  2715     \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}}} \\

  2716     \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}}} \\

  2717   \end{matharray}

  2719   \begin{railoutput}

  2720 \rail@begin{6}{}

  2721 \rail@bar

  2722 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]

  2723 \rail@nextbar{1}

  2724 \rail@term{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}}[]

  2725 \rail@endbar

  2726 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2727 \rail@plus

  2728 \rail@nont{\isa{decl}}[]

  2729 \rail@nextplus{1}

  2730 \rail@endplus

  2731 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2732 \rail@cr{3}

  2733 \rail@plus

  2734 \rail@bar

  2735 \rail@nextbar{4}

  2736 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

  2737 \rail@endbar

  2738 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  2739 \rail@nextplus{5}

  2740 \rail@endplus

  2741 \rail@end

  2742 \rail@begin{2}{\isa{decl}}

  2743 \rail@bar

  2744 \rail@nextbar{1}

  2745 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  2746 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

  2747 \rail@endbar

  2748 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  2749 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  2750 \rail@term{\isa{\isakeyword{overloaded}}}[]

  2751 \rail@bar

  2752 \rail@nextbar{1}

  2753 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  2754 \rail@endbar

  2755 \rail@end

  2756 \end{railoutput}

  2759   \begin{description}

  2761   \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up a

  2762   goal stating the existence of terms with the properties specified to

  2763   hold for the constants given in \isa{decls}.  After finishing the

  2764   proof, the theory will be augmented with definitions for the given

  2765   constants, as well as with theorems stating the properties for these

  2766   constants.

  2768   \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

  2769   a goal stating the existence of terms with the properties specified

  2770   to hold for the constants given in \isa{decls}.  After finishing

  2771   the proof, the theory will be augmented with axioms expressing the

  2772   properties given in the first place.

  2774   \item \isa{decl} declares a constant to be defined by the

  2775   specification given.  The definition for the constant \isa{c} is

  2776   bound to the name \isa{c{\isaliteral{5F}{\isacharunderscore}}def} unless a theorem name is given in

  2777   the declaration.  Overloaded constants should be declared as such.

  2779   \end{description}

  2781   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

  2782   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

  2783   user has explicitly proven it to be safe.  A practical issue must be

  2784   considered, though: After introducing two constants with the same

  2785   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove

  2786   that the two constants are, in fact, equal.  If this might be a

  2787   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}.%

  2788 \end{isamarkuptext}%

  2789 \isamarkuptrue%

  2790 %

  2791 \isadelimtheory

  2792 %

  2793 \endisadelimtheory

  2794 %

  2795 \isatagtheory

  2796 \isacommand{end}\isamarkupfalse%

  2797 %

  2798 \endisatagtheory

  2799 {\isafoldtheory}%

  2800 %

  2801 \isadelimtheory

  2802 %

  2803 \endisadelimtheory

  2804 \isanewline

  2805 \end{isabellebody}%

  2806 %%% Local Variables:

  2807 %%% mode: latex

  2808 %%% TeX-master: "root"

  2809 %%% End:

author	wenzelm
	Thu, 26 May 2011 13:37:11 +0200
changeset 44113	66b189dc5b83
parent 44112	eb94cfaaf5d4
child 44114	6834af822a8b
permissions	-rw-r--r--