theory HOLCF_Specific
imports Base 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}
@{rail "
@@{command (HOLCF) domain} @{syntax parname}? (spec + @'and')
;
spec: @{syntax typespec} '=' (cons + '|')
;
cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
;
dtrules: @'distinct' @{syntax thmrefs} @'inject' @{syntax thmrefs}
@'induction' @{syntax thmrefs}
"}
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