doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 30172 afdf7808cfd0
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ HOLCF{\isacharunderscore}Specific\isanewline
    12 \isakeyword{imports}\ HOLCF\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Isabelle/HOLCF \label{ch:holcf}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Mixfix syntax for continuous operations%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \begin{isamarkuptext}%
    30 \begin{matharray}{rcl}
    31     \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    32   \end{matharray}
    33 
    34   HOLCF provides a separate type for continuous functions \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}{\isachardoublequote}}, with an explicit application operator \isa{{\isachardoublequote}f\ {\isasymcdot}\ x{\isachardoublequote}}.
    35   Isabelle mixfix syntax normally refers directly to the pure
    36   meta-level function type \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}{\isachardoublequote}}, with application \isa{{\isachardoublequote}f\ x{\isachardoublequote}}.
    37 
    38   The HOLCF variant of \hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}} modifies that of
    39   Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
    40   involving continuous function types are treated specifically.  Any
    41   given syntax template is transformed internally, generating
    42   translation rules for the abstract and concrete representation of
    43   continuous application.  Note that mixing of HOLCF and Pure
    44   application is \emph{not} supported!%
    45 \end{isamarkuptext}%
    46 \isamarkuptrue%
    47 %
    48 \isamarkupsection{Recursive domains%
    49 }
    50 \isamarkuptrue%
    51 %
    52 \begin{isamarkuptext}%
    53 \begin{matharray}{rcl}
    54     \indexdef{HOLCF}{command}{domain}\hypertarget{command.HOLCF.domain}{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    55   \end{matharray}
    56 
    57   \begin{rail}
    58     'domain' parname? (dmspec + 'and')
    59     ;
    60 
    61     dmspec: typespec '=' (cons + '|')
    62     ;
    63     cons: name (type *) mixfix?
    64     ;
    65     dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    66   \end{rail}
    67 
    68   Recursive domains in HOLCF are analogous to datatypes in classical
    69   HOL (cf.\ \secref{sec:hol-datatype}).  Mutual recursion is
    70   supported, but no nesting nor arbitrary branching.  Domain
    71   constructors may be strict (default) or lazy, the latter admits to
    72   introduce infinitary objects in the typical LCF manner (e.g.\ lazy
    73   lists).  See also \cite{MuellerNvOS99} for a general discussion of
    74   HOLCF domains.%
    75 \end{isamarkuptext}%
    76 \isamarkuptrue%
    77 %
    78 \isadelimtheory
    79 %
    80 \endisadelimtheory
    81 %
    82 \isatagtheory
    83 \isacommand{end}\isamarkupfalse%
    84 %
    85 \endisatagtheory
    86 {\isafoldtheory}%
    87 %
    88 \isadelimtheory
    89 %
    90 \endisadelimtheory
    91 \isanewline
    92 \end{isabellebody}%
    93 %%% Local Variables:
    94 %%% mode: latex
    95 %%% TeX-master: "root"
    96 %%% End: