--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Mon Nov 08 00:00:47 2010 +0100
@@ -1,6 +1,6 @@
%
\begin{isabellebody}%
-\def\isabellecontext{Inductive{\isacharunderscore}Predicate}%
+\def\isabellecontext{Inductive{\isaliteral{5F}{\isacharunderscore}}Predicate}%
%
\isadelimtheory
%
@@ -8,7 +8,7 @@
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
-\ Inductive{\isacharunderscore}Predicate\isanewline
+\ Inductive{\isaliteral{5F}{\isacharunderscore}}Predicate\isanewline
\isakeyword{imports}\ Setup\isanewline
\isakeyword{begin}\isanewline
%
@@ -55,8 +55,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys} \\
- \isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
+\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%
%
@@ -68,7 +68,7 @@
\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{\isacharunderscore}pred}}}}}:%
+\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%
%
@@ -77,8 +77,8 @@
\endisadelimquote
%
\isatagquote
-\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
+\ append\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
@@ -88,7 +88,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name of the
+\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
@@ -98,9 +98,9 @@
For \isa{append}, the compiler can infer the following modes:
\begin{itemize}
- \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
- \item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
- \item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+ \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}%
@@ -112,7 +112,7 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\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}%
%
@@ -121,7 +121,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and%
+\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%
%
@@ -131,7 +131,7 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\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}%
%
@@ -140,7 +140,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.%
+\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%
%
@@ -158,9 +158,9 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\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}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\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}%
%
@@ -183,7 +183,7 @@
%
\isatagquote
\isacommand{thm}\isamarkupfalse%
-\ append{\isachardot}equation%
+\ append{\isaliteral{2E}{\isachardot}}equation%
\endisatagquote
{\isafoldquote}%
%
@@ -202,7 +202,7 @@
%
\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{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}). You can specify your own names as follows:%
+ 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%
%
@@ -211,10 +211,10 @@
\endisadelimquote
%
\isatagquote
-\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
-\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool\ as\ concat{\isacharcomma}\isanewline
-\ \ o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ split{\isacharcomma}\isanewline
-\ \ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+\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}%
@@ -233,7 +233,7 @@
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{\isacharunderscore}pred{\isacharunderscore}intro}}}. For example, the transitive closure is defined
+ 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%
@@ -245,8 +245,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{{\isachardoublequote}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequote}}\\
- \isa{{\isachardoublequote}tranclp\ r\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequote}}%
+\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%
%
@@ -259,10 +259,10 @@
%
\begin{isamarkuptext}%
\noindent These rules do not suit well for executing the transitive
- closure with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as
+ 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{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
+ 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%
%
@@ -272,9 +272,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequoteclose}\isanewline
+\ {\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
@@ -286,7 +286,7 @@
%
\begin{isamarkuptext}%
\noindent After declaring all alternative rules for the transitive
- closure, you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual. As you have
+ 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:%
@@ -298,14 +298,14 @@
\endisadelimquote
%
\isatagquote
-\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
\ tranclp\isanewline
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ tranclp\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ tranclp{\isachardot}prems{\isacharbrackright}\ \isacommand{show}\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%
@@ -332,10 +332,10 @@
%
\begin{isamarkuptext}%
\begin{isabelle}%
-lexord\ r\ {\isacharequal}\isanewline
-{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
-\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
-\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%
+lexord\ r\ {\isaliteral{3D}{\isacharequal}}\isanewline
+{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ }{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
+\isaindent{\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}%
\end{isabelle}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -359,13 +359,13 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\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}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
-\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{code{\isacharunderscore}pred}\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\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
\ lexord%
\endisatagquote
{\isafoldquote}%
@@ -393,12 +393,12 @@
%
\isatagquote
\isacommand{inductive}\isamarkupfalse%
-\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ 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{\isacharunderscore}pred}\isamarkupfalse%
-\ succ\ \isacommand{{\isachardot}}\isamarkupfalse%
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
+\ succ\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
@@ -408,10 +408,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and
- \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}. The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}
- \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple modes for the
- predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool} is chosen. To choose another mode for the argument,
+\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%
@@ -422,9 +422,9 @@
%
\isatagquote
\isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
+\ {\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%
-\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\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}%
%
@@ -446,20 +446,20 @@
where all arguments are input. Then you can use the predicate directly, e.g.
\begin{quote}
- \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}} \\
- \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
+ \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{\isachardot}the}, e.g., a functional concatenation of lists 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{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
+ \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{\isacharunderscore}unique}.
+ raises a run-time error \isa{not{\isaliteral{5F}{\isacharunderscore}}unique}.
\end{itemize}%
\end{isamarkuptext}%
@@ -471,9 +471,9 @@
%
\begin{isamarkuptext}%
Further examples for compiling inductive predicates can be found in
- the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isachardot}thy} theory file. There are
+ 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{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
+ \isa{POPLmark{\isaliteral{2D}{\isacharminus}}deBruijn} and the \isa{FeatherweightJava}
sessions.%
\end{isamarkuptext}%
\isamarkuptrue%