author krauss Tue Oct 26 12:19:01 2010 +0200 (2010-10-26) changeset 40171 1fa547166a1d parent 40170 751121d5ca35 child 40172 008dc2d2c395
basic documentation for command partial_function
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
1.3 @@ -548,6 +548,71 @@
1.4    \end{description}
1.5  *}
1.6
1.7 +subsection {* Functions with explicit partiality *}
1.8 +
1.9 +text {*
1.10 +  \begin{matharray}{rcl}
1.11 +    @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1.12 +    @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
1.13 +  \end{matharray}
1.14 +
1.15 +  \begin{rail}
1.16 +    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
1.17 +  \end{rail}
1.18 +
1.19 +  \begin{description}
1.20 +
1.21 +  \item @{command (HOL) "partial_function"} defines recursive
1.22 +  functions based on fixpoints in complete partial orders. No
1.23 +  termination proof is required from the user or constructed
1.24 +  internally. Instead, the possibility of non-termination is modelled
1.25 +  explicitly in the result type, which contains an explicit bottom
1.26 +  element.
1.27 +
1.28 +  Pattern matching and mutual recursion are currently not supported.
1.29 +  Thus, the specification consists of a single function described by a
1.30 +  single recursive equation.
1.31 +
1.32 +  There are no fixed syntactic restrictions on the body of the
1.33 +  function, but the induced functional must be provably monotonic
1.34 +  wrt.\ the underlying order.  The monotonicitity proof is performed
1.35 +  internally, and the definition is rejected when it fails. The proof
1.36 +  can be influenced by declaring hints using the
1.37 +  @{attribute (HOL) partial_function_mono} attribute.
1.38 +
1.39 +  The mandatory @{text mode} argument specifies the mode of operation
1.40 +  of the command, which directly corresponds to a complete partial
1.41 +  order on the result type. By default, the following modes are
1.42 +  defined:
1.43 +
1.44 +  \begin{description}
1.45 +  \item @{text option} defines functions that map into the @{type
1.46 +  option} type. Here, the value @{term None} is used to model a
1.47 +  non-terminating computation. Monotonicity requires that if @{term
1.48 +  None} is returned by a recursive call, then the overall result
1.49 +  must also be @{term None}. This is best achieved through the use of
1.50 +  the monadic operator @{const "Option.bind"}.
1.51 +
1.52 +  \item @{text tailrec} defines functions with an arbitrary result
1.53 +  type and uses the slightly degenerated partial order where @{term
1.54 +  "undefined"} is the bottom element.  Now, monotonicity requires that
1.55 +  if @{term undefined} is returned by a recursive call, then the
1.56 +  overall result must also be @{term undefined}. In practice, this is
1.57 +  only satisfied when each recursive call is a tail call, whose result
1.58 +  is directly returned. Thus, this mode of operation allows the
1.59 +  definition of arbitrary tail-recursive functions.
1.60 +  \end{description}
1.61 +
1.62 +  Experienced users may define new modes by instantiating the locale
1.63 +  @{const "partial_function_definitions"} appropriately.
1.64 +
1.65 +  \item @{attribute (HOL) partial_function_mono} declares rules for
1.66 +  use in the internal monononicity proofs of partial function
1.67 +  definitions.
1.68 +
1.69 +  \end{description}
1.70 +
1.71 +*}
1.72
1.73  subsection {* Old-style recursive function definitions (TFL) *}
1.74

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
2.3 @@ -558,6 +558,71 @@
2.4  \end{isamarkuptext}%
2.5  \isamarkuptrue%
2.6  %
2.7 +\isamarkupsubsection{Functions with explicit partiality%
2.8 +}
2.9 +\isamarkuptrue%
2.10 +%
2.11 +\begin{isamarkuptext}%
2.12 +\begin{matharray}{rcl}
2.13 +    \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
2.14 +    \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}}} & : & \isa{attribute} \\
2.15 +  \end{matharray}
2.16 +
2.17 +  \begin{rail}
2.18 +    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
2.19 +  \end{rail}
2.20 +
2.21 +  \begin{description}
2.22 +
2.23 +  \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}} defines recursive
2.24 +  functions based on fixpoints in complete partial orders. No
2.25 +  termination proof is required from the user or constructed
2.26 +  internally. Instead, the possibility of non-termination is modelled
2.27 +  explicitly in the result type, which contains an explicit bottom
2.28 +  element.
2.29 +
2.30 +  Pattern matching and mutual recursion are currently not supported.
2.31 +  Thus, the specification consists of a single function described by a
2.32 +  single recursive equation.
2.33 +
2.34 +  There are no fixed syntactic restrictions on the body of the
2.35 +  function, but the induced functional must be provably monotonic
2.36 +  wrt.\ the underlying order.  The monotonicitity proof is performed
2.37 +  internally, and the definition is rejected when it fails. The proof
2.38 +  can be influenced by declaring hints using the
2.40 +
2.41 +  The mandatory \isa{mode} argument specifies the mode of operation
2.42 +  of the command, which directly corresponds to a complete partial
2.43 +  order on the result type. By default, the following modes are
2.44 +  defined:
2.45 +
2.46 +  \begin{description}
2.47 +  \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
2.48 +  non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
2.49 +  must also be \isa{None}. This is best achieved through the use of
2.50 +  the monadic operator \isa{{\isachardoublequote}Option{\isachardot}bind{\isachardoublequote}}.
2.51 +
2.52 +  \item \isa{tailrec} defines functions with an arbitrary result
2.53 +  type and uses the slightly degenerated partial order where \isa{{\isachardoublequote}undefined{\isachardoublequote}} is the bottom element.  Now, monotonicity requires that
2.54 +  if \isa{undefined} is returned by a recursive call, then the
2.55 +  overall result must also be \isa{undefined}. In practice, this is
2.56 +  only satisfied when each recursive call is a tail call, whose result
2.57 +  is directly returned. Thus, this mode of operation allows the
2.58 +  definition of arbitrary tail-recursive functions.
2.59 +  \end{description}
2.60 +
2.61 +  Experienced users may define new modes by instantiating the locale
2.62 +  \isa{{\isachardoublequote}partial{\isacharunderscore}function{\isacharunderscore}definitions{\isachardoublequote}} appropriately.
2.63 +
2.64 +  \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} declares rules for
2.65 +  use in the internal monononicity proofs of partial function
2.66 +  definitions.
2.67 +
2.68 +  \end{description}%
2.69 +\end{isamarkuptext}%
2.70 +\isamarkuptrue%
2.71 +%
2.72  \isamarkupsubsection{Old-style recursive function definitions (TFL)%
2.73  }
2.74  \isamarkuptrue%