doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
author wenzelm
Wed, 29 Dec 2010 20:41:33 +0100
changeset 41415 23533273220a
parent 40406 313a24b66a8d
child 42596 6c621a9d612a
permissions -rw-r--r--
tuned ML toplevel pp for type string: observe depth limit;

%
\begin{isabellebody}%
\def\isabellecontext{HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
\isakeyword{imports}\ 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{rail}
    'domain' parname? (dmspec + 'and')
    ;

    dmspec: typespec '=' (cons + '|')
    ;
    cons: name (type *) mixfix?
    ;
    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
  \end{rail}

  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: