--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 11:21:53 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 13:11:47 2007 +0200
@@ -332,14 +332,11 @@
\begin{isamarkuptext}%
\noindent which displays a table of constant with corresponding
defining equations (the additional stuff displayed
- shall not bother us for the moment). If this table does
- not provide at least one defining
- equation for a particular constant, the table of primitive
- definitions is searched
- whether it provides one.
+ shall not bother us for the moment).
The typical HOL tools are already set up in a way that
- function definitions introduced by \isa{{\isasymFUN}},
+ function definitions introduced by \isa{{\isasymDEFINITION}},
+ \isa{{\isasymFUN}},
\isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
\isa{{\isasymRECDEF}} are implicitly propagated
to this defining equation table. Specific theorems may be
@@ -1154,9 +1151,9 @@
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
-\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
\isadelimproof
\ %
@@ -1173,6 +1170,9 @@
\endisadelimproof
\isanewline
\isanewline
+\isacommand{lemmas}\isamarkupfalse%
+\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
+\isanewline
\isacommand{lemma}\isamarkupfalse%
\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -1184,7 +1184,7 @@
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
-\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
@@ -1242,7 +1242,10 @@
restrictive sort constraints than the underlying instance relation
between class and type constructor as long as the whole system of
constraints is coregular; code theorems violating coregularity
- are rejected immediately.%
+ are rejected immediately. Consequently, it might be necessary
+ to delete disturbing theorems in the code theorem table,
+ as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
+ and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1430,7 +1433,7 @@
expects dictionaries (namely an \emph{eq} dictionary) but
has also been given a customary serialization.
- The solution to this dilemma:%
+ \fixme[needs rewrite] The solution to this dilemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -1456,9 +1459,7 @@
\begin{isamarkuptext}%
\lstsml{Thy/examples/dirty_set.ML}
- Reflexive defining equations by convention are dropped.
- But their presence prevents primitive definitions to be
- used as defining equations:%
+ Reflexive defining equations by convention are dropped:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
@@ -1697,12 +1698,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T|
+ \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T|
\end{mldecls}
\begin{description}
- \item \verb|CodegenData.lazy|~\isa{f} turns an abstract
+ \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract
theorem computation \isa{f} into a suspension of theorems.
\end{description}%
@@ -1822,7 +1823,7 @@
\indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
\indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
\indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
- \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\
+ \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\
\indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\
\end{mldecls}
@@ -1837,8 +1838,8 @@
\item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s}
reads a constant as a concrete term expression \isa{s}.
- \item \verb|CodegenFunc.typ_func|~\isa{thm}
- extracts the type of a constant in a defining equation \isa{thm}.
+ \item \verb|CodegenFunc.head_func|~\isa{thm}
+ extracts the constant and its type from a defining equation \isa{thm}.
\item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm}
rewrites a defining equation \isa{thm} with a set of rewrite