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