5 chapter {* Isabelle/HOLCF \label{ch:holcf} *}
7 section {* Mixfix syntax for continuous operations *}
10 \begin{matharray}{rcl}
11 @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
14 HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
15 \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
16 Isabelle mixfix syntax normally refers directly to the pure
17 meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
20 The HOLCF variant of @{command (HOLCF) "consts"} modifies that of
21 Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
22 involving continuous function types are treated specifically. Any
23 given syntax template is transformed internally, generating
24 translation rules for the abstract and concrete representation of
25 continuous application. Note that mixing of HOLCF and Pure
26 application is \emph{not} supported!
30 section {* Recursive domains *}
33 \begin{matharray}{rcl}
34 @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
38 'domain' parname? (dmspec + 'and')
41 dmspec: typespec '=' (cons + '|')
43 cons: name (type *) mixfix?
45 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
48 Recursive domains in HOLCF are analogous to datatypes in classical
49 HOL (cf.\ \secref{sec:hol-datatype}). Mutual recursion is
50 supported, but no nesting nor arbitrary branching. Domain
51 constructors may be strict (default) or lazy, the latter admits to
52 introduce infinitary objects in the typical LCF manner (e.g.\ lazy
53 lists). See also \cite{MuellerNvOS99} for a general discussion of