doc-src/Codegen/Thy/document/Inductive_Predicate.tex

-%
-\begin{isabellebody}%
-\def\isabellecontext{Inductive{\isaliteral{5F}{\isacharunderscore}}Predicate}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Inductive{\isaliteral{5F}{\isacharunderscore}}Predicate\isanewline
-\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}\isanewline
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isamarkupsection{Inductive Predicates \label{sec:inductive}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \isa{predicate\ compiler} is an extension of the code generator
-  which turns inductive specifications into equational ones, from
-  which in turn executable code can be generated.  The mechanisms of
-  this compiler are described in detail in
-  \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-
-  Consider the simple predicate \isa{append} given by these two
-  introduction rules:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isa{append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys\ ys} \\
-  \isa{append\ xs\ ys\ zs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ append\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}} command takes the name of the
-  inductive predicate and then you put a period to discharge a trivial
-  correctness proof.  The compiler infers possible modes for the
-  predicate and produces the derived code equations.  Modes annotate
-  which (parts of the) arguments are to be taken as input, and which
-  output. Modes are similar to types, but use the notation \isa{i}
-  for input and \isa{o} for output.
- 
-  For \isa{append}, the compiler can infer the following modes:
-  \begin{itemize}
-    \item \isa{i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
-    \item \isa{i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
-    \item \isa{o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
-  \end{itemize}
-  You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{values}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}zs{\isaliteral{2E}{\isachardot}}\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}\ zs{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent outputs \isa{{\isaliteral{7B}{\isacharbraceleft}}{\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{7D}{\isacharbraceright}}}, and%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{values}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ append\ xs\ ys\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent outputs \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent If you are only interested in the first elements of the
-  set comprehension (with respect to a depth-first search on the
-  introduction rules), you can pass an argument to \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
-  to specify the number of elements you want:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{values}\isamarkupfalse%
-\ {\isadigit{1}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ append\ xs\ ys\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{values}\isamarkupfalse%
-\ {\isadigit{3}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ append\ xs\ ys\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
-  comprehensions for which a mode has been inferred.
-
-  The code equations for a predicate are made available as theorems with
-  the suffix \isa{equation}, and can be inspected with:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{thm}\isamarkupfalse%
-\ append{\isaliteral{2E}{\isachardot}}equation%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent More advanced options are described in the following subsections.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Alternative names for functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-By default, the functions generated from a predicate are named after
-  the predicate with the mode mangled into the name (e.g., \isa{append{\isaliteral{5F}{\isacharunderscore}}i{\isaliteral{5F}{\isacharunderscore}}i{\isaliteral{5F}{\isacharunderscore}}o}).  You can specify your own names as follows:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}modes{\isaliteral{3A}{\isacharcolon}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ as\ concat{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ as\ split{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ as\ suffix{\isaliteral{29}{\isacharparenright}}\ append\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isamarkupsubsection{Alternative introduction rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Sometimes the introduction rules of an predicate are not executable
-  because they contain non-executable constants or specific modes
-  could not be inferred.  It is also possible that the introduction
-  rules yield a function that loops forever due to the execution in a
-  depth-first search manner.  Therefore, you can declare alternative
-  introduction rules for predicates with the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro}}}.  For example, the transitive closure is defined
-  by:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isa{{\isaliteral{22}{\isachardoublequote}}r\ a\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ tranclp\ r\ a\ b{\isaliteral{22}{\isachardoublequote}}}\\
-  \isa{{\isaliteral{22}{\isachardoublequote}}tranclp\ r\ a\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ b\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ tranclp\ r\ a\ c{\isaliteral{22}{\isachardoublequote}}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent These rules do not suit well for executing the transitive
-  closure with the mode \isa{{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, as
-  the second rule will cause an infinite loop in the recursive call.
-  This can be avoided using the following alternative rules which are
-  declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}r\ a\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ tranclp\ r\ a\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}r\ a\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ tranclp\ r\ b\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ tranclp\ r\ a\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{by}\isamarkupfalse%
-\ auto%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent After declaring all alternative rules for the transitive
-  closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}}}} as usual.  As you have
-  declared alternative rules for the predicate, you are urged to prove
-  that these introduction rules are complete, i.e., that you can
-  derive an elimination rule for the alternative rules:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ tranclp\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ tranclp\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isaliteral{5F}{\isacharunderscore}}tranclpE\ {\isaliteral{5B}{\isacharbrackleft}}OF\ tranclp{\isaliteral{2E}{\isachardot}}prems{\isaliteral{5D}{\isacharbrackright}}\ \isacommand{show}\isamarkupfalse%
-\ thesis\ \isacommand{by}\isamarkupfalse%
-\ metis\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Alternative rules can also be used for constants that have
-  not been defined inductively. For example, the lexicographic order
-  which is defined as:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-lexordp\ r\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\isanewline
-{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
-\isaindent{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ r\ a\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent To make it executable, you can derive the following two
-  rules and prove the elimination rule:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ u\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ u\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ a\ b\isanewline
-\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ lexordp%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isamarkupsubsection{Options for values%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In the presence of higher-order predicates, multiple modes for some
-  predicate could be inferred that are not disambiguated by the
-  pattern of the set comprehension.  To disambiguate the modes for the
-  arguments of a predicate, you can state the modes explicitly in the
-  \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command.  Consider the simple predicate \isa{succ}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{inductive}\isamarkupfalse%
-\ succ\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}succ\ {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}succ\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ succ\ {\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ succ\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent For this, the predicate compiler can infer modes \isa{o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, \isa{i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, \isa{o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} and
-  \isa{i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}.  The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
-  \isa{{\isaliteral{7B}{\isacharbraceleft}}n{\isaliteral{2E}{\isachardot}}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isaliteral{7D}{\isacharbraceright}}} loops, as multiple modes for the
-  predicate \isa{succ} are possible and here the first mode \isa{o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} is chosen. To choose another mode for the argument,
-  you can declare the mode for the argument between the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{values}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}mode{\isaliteral{3A}{\isacharcolon}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{1}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}n{\isaliteral{2E}{\isachardot}}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
-\isacommand{values}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}mode{\isaliteral{3A}{\isacharcolon}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{1}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}n{\isaliteral{2E}{\isachardot}}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isamarkupsubsection{Embedding into functional code within Isabelle/HOL%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-To embed the computation of an inductive predicate into functions
-  that are defined in Isabelle/HOL, you have a number of options:
-
-  \begin{itemize}
-
-    \item You want to use the first-order predicate with the mode
-      where all arguments are input. Then you can use the predicate directly, e.g.
-
-      \begin{quote}
-        \isa{valid{\isaliteral{5F}{\isacharunderscore}}suffix\ ys\ zs\ {\isaliteral{3D}{\isacharequal}}} \\
-        \isa{{\isaliteral{28}{\isacharparenleft}}if\ append\ {\isaliteral{5B}{\isacharbrackleft}}Suc\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}\ ys\ zs\ then\ Some\ ys\ else\ None{\isaliteral{29}{\isacharparenright}}}
-      \end{quote}
-
-    \item If you know that the execution returns only one value (it is
-      deterministic), then you can use the combinator \isa{Predicate{\isaliteral{2E}{\isachardot}}the}, e.g., a functional concatenation of lists is
-      defined with
-
-      \begin{quote}
-        \isa{functional{\isaliteral{5F}{\isacharunderscore}}concat\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ Predicate{\isaliteral{2E}{\isachardot}}the\ {\isaliteral{28}{\isacharparenleft}}append{\isaliteral{5F}{\isacharunderscore}}i{\isaliteral{5F}{\isacharunderscore}}i{\isaliteral{5F}{\isacharunderscore}}o\ xs\ ys{\isaliteral{29}{\isacharparenright}}}
-      \end{quote}
-
-      Note that if the evaluation does not return a unique value, it
-      raises a run-time error \isa{not{\isaliteral{5F}{\isacharunderscore}}unique}.
-
-  \end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Further Examples%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Further examples for compiling inductive predicates can be found in
-  the \isa{HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Predicate{\isaliteral{5F}{\isacharunderscore}}Compile{\isaliteral{5F}{\isacharunderscore}}ex{\isaliteral{2E}{\isachardot}}thy} theory file.  There are
-  also some examples in the Archive of Formal Proofs, notably in the
-  \isa{POPLmark{\isaliteral{2D}{\isacharminus}}deBruijn} and the \isa{FeatherweightJava}
-  sessions.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: