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