doc-src/IsarRef/Thy/HOLCF_Specific.thy

tuned proof

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