theory HOLCF_Specific

imports HOLCF

begin

chapter {* Isabelle/HOLCF \label{ch:holcf} *}

section {* Mixfix syntax for continuous operations *}

text {*

  \begin{matharray}{rcl}

    @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\

  \end{matharray}

  HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>

  \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.

  Isabelle mixfix syntax normally refers directly to the pure

  meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f

  x"}.

  The HOLCF variant of @{command (HOLCF) "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!

*}

section {* Recursive domains *}

text {*

  \begin{matharray}{rcl}

    @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\

  \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