doc-src/IsarRef/Thy/HOLCF_Specific.thy
author wenzelm
Fri, 11 Jul 2008 23:17:23 +0200
changeset 27554 2deaa546ba0d
parent 26852 a31203f58b20
child 28761 9ec4482c9201
permissions -rw-r--r--
Sorts.weaken: abstract argument;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     1
(* $Id$ *)
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     2
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     3
theory HOLCF_Specific
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     4
imports HOLCF
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     5
begin
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     6
26852
a31203f58b20 misc tuning;
wenzelm
parents: 26841
diff changeset
     7
chapter {* Isabelle/HOLCF \label{ch:holcf} *}
26841
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
     8
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
     9
section {* Mixfix syntax for continuous operations *}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    10
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    11
text {*
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    12
  \begin{matharray}{rcl}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    13
    @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    14
  \end{matharray}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    15
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    16
  HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    17
  \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    18
  Isabelle mixfix syntax normally refers directly to the pure
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    19
  meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    20
  x"}.
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    21
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    22
  The HOLCF variant of @{command (HOLCF) "consts"} modifies that of
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    23
  Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    24
  involving continuous function types are treated specifically.  Any
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    25
  given syntax template is transformed internally, generating
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    26
  translation rules for the abstract and concrete representation of
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    27
  continuous application.  Note that mixing of HOLCF and Pure
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    28
  application is \emph{not} supported!
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    29
*}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    30
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    31
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    32
section {* Recursive domains *}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    33
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    34
text {*
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    35
  \begin{matharray}{rcl}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    36
    @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    37
  \end{matharray}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    38
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    39
  \begin{rail}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    40
    'domain' parname? (dmspec + 'and')
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    41
    ;
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    42
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    43
    dmspec: typespec '=' (cons + '|')
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    44
    ;
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    45
    cons: name (type *) mixfix?
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    46
    ;
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    47
    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    48
  \end{rail}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    49
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    50
  Recursive domains in HOLCF are analogous to datatypes in classical
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    51
  HOL (cf.\ \secref{sec:hol-datatype}).  Mutual recursion is
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    52
  supported, but no nesting nor arbitrary branching.  Domain
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    53
  constructors may be strict (default) or lazy, the latter admits to
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    54
  introduce infinitary objects in the typical LCF manner (e.g.\ lazy
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    55
  lists).  See also \cite{MuellerNvOS99} for a general discussion of
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    56
  HOLCF domains.
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    57
*}
6ac51a2f48e1 converted HOLCF specific elements;
wenzelm
parents: 26840
diff changeset
    58
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
    59
end