--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Tue Aug 28 12:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Base\ HOLCF\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Isabelle/HOLCF \label{ch:holcf}%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Mixfix syntax for continuous operations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- HOLCF provides a separate type for continuous functions \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}}, with an explicit application operator \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C63646F743E}{\isasymcdot}}\ x{\isaliteral{22}{\isachardoublequote}}}.
- Isabelle mixfix syntax normally refers directly to the pure
- meta-level function type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}}, with application \isa{{\isaliteral{22}{\isachardoublequote}}f\ x{\isaliteral{22}{\isachardoublequote}}}.
-
- The HOLCF variant of \hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}} modifies that of
- Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
- involving continuous function types are treated specifically. Any
- given syntax template is transformed internally, generating
- translation rules for the abstract and concrete representation of
- continuous application. Note that mixing of HOLCF and Pure
- application is \emph{not} supported!%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Recursive domains%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{HOLCF}{command}{domain}\hypertarget{command.HOLCF.domain}{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
-\rail@endbar
-\rail@plus
-\rail@nont{\isa{spec}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{\isakeyword{and}}}[]
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{spec}}
-\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
-\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@plus
-\rail@nont{\isa{cons}}[]
-\rail@nextplus{1}
-\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{cons}}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
-\rail@endplus
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{\isa{dtrules}}
-\rail@term{\isa{\isakeyword{distinct}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@term{\isa{\isakeyword{inject}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@term{\isa{\isakeyword{induction}}}[]
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@end
-\end{railoutput}
-
-
- Recursive domains in HOLCF are analogous to datatypes in classical
- HOL (cf.\ \secref{sec:hol-datatype}). Mutual recursion is
- supported, but no nesting nor arbitrary branching. Domain
- constructors may be strict (default) or lazy, the latter admits to
- introduce infinitary objects in the typical LCF manner (e.g.\ lazy
- lists). See also \cite{MuellerNvOS99} for a general discussion of
- HOLCF domains.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: