# HG changeset patch
# User krauss
# Date 1288088341 -7200
# Node ID 1fa547166a1d95dda7a24686dda0bd944ec0adb8
# Parent  751121d5ca3550155cee99f3fc61bb14a182e72c
basic documentation for command partial_function

diff -r 751121d5ca35 -r 1fa547166a1d doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
@@ -548,6 +548,71 @@
   \end{description}
 *}
 
+subsection {* Functions with explicit partiality *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
+  \end{matharray}
+
+  \begin{rail}
+    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
+  \end{rail}
+
+  \begin{description}
+
+  \item @{command (HOL) "partial_function"} defines recursive
+  functions based on fixpoints in complete partial orders. No
+  termination proof is required from the user or constructed
+  internally. Instead, the possibility of non-termination is modelled
+  explicitly in the result type, which contains an explicit bottom
+  element.
+
+  Pattern matching and mutual recursion are currently not supported.
+  Thus, the specification consists of a single function described by a
+  single recursive equation.
+
+  There are no fixed syntactic restrictions on the body of the
+  function, but the induced functional must be provably monotonic
+  wrt.\ the underlying order.  The monotonicitity proof is performed
+  internally, and the definition is rejected when it fails. The proof
+  can be influenced by declaring hints using the
+  @{attribute (HOL) partial_function_mono} attribute.
+
+  The mandatory @{text mode} argument specifies the mode of operation
+  of the command, which directly corresponds to a complete partial
+  order on the result type. By default, the following modes are
+  defined: 
+
+  \begin{description}
+  \item @{text option} defines functions that map into the @{type
+  option} type. Here, the value @{term None} is used to model a
+  non-terminating computation. Monotonicity requires that if @{term
+  None} is returned by a recursive call, then the overall result
+  must also be @{term None}. This is best achieved through the use of
+  the monadic operator @{const "Option.bind"}.
+  
+  \item @{text tailrec} defines functions with an arbitrary result
+  type and uses the slightly degenerated partial order where @{term
+  "undefined"} is the bottom element.  Now, monotonicity requires that
+  if @{term undefined} is returned by a recursive call, then the
+  overall result must also be @{term undefined}. In practice, this is
+  only satisfied when each recursive call is a tail call, whose result
+  is directly returned. Thus, this mode of operation allows the
+  definition of arbitrary tail-recursive functions.
+  \end{description}
+
+  Experienced users may define new modes by instantiating the locale
+  @{const "partial_function_definitions"} appropriately.
+
+  \item @{attribute (HOL) partial_function_mono} declares rules for
+  use in the internal monononicity proofs of partial function
+  definitions.
+
+  \end{description}
+
+*}
 
 subsection {* Old-style recursive function definitions (TFL) *}
 
diff -r 751121d5ca35 -r 1fa547166a1d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
@@ -558,6 +558,71 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Functions with explicit partiality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \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}} \\
+    \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} \\
+  \end{matharray}
+
+  \begin{rail}
+    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
+  \end{rail}
+
+  \begin{description}
+
+  \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}} defines recursive
+  functions based on fixpoints in complete partial orders. No
+  termination proof is required from the user or constructed
+  internally. Instead, the possibility of non-termination is modelled
+  explicitly in the result type, which contains an explicit bottom
+  element.
+
+  Pattern matching and mutual recursion are currently not supported.
+  Thus, the specification consists of a single function described by a
+  single recursive equation.
+
+  There are no fixed syntactic restrictions on the body of the
+  function, but the induced functional must be provably monotonic
+  wrt.\ the underlying order.  The monotonicitity proof is performed
+  internally, and the definition is rejected when it fails. The proof
+  can be influenced by declaring hints using the
+  \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} attribute.
+
+  The mandatory \isa{mode} argument specifies the mode of operation
+  of the command, which directly corresponds to a complete partial
+  order on the result type. By default, the following modes are
+  defined: 
+
+  \begin{description}
+  \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
+  non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
+  must also be \isa{None}. This is best achieved through the use of
+  the monadic operator \isa{{\isachardoublequote}Option{\isachardot}bind{\isachardoublequote}}.
+  
+  \item \isa{tailrec} defines functions with an arbitrary result
+  type and uses the slightly degenerated partial order where \isa{{\isachardoublequote}undefined{\isachardoublequote}} is the bottom element.  Now, monotonicity requires that
+  if \isa{undefined} is returned by a recursive call, then the
+  overall result must also be \isa{undefined}. In practice, this is
+  only satisfied when each recursive call is a tail call, whose result
+  is directly returned. Thus, this mode of operation allows the
+  definition of arbitrary tail-recursive functions.
+  \end{description}
+
+  Experienced users may define new modes by instantiating the locale
+  \isa{{\isachardoublequote}partial{\isacharunderscore}function{\isacharunderscore}definitions{\isachardoublequote}} appropriately.
+
+  \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} declares rules for
+  use in the internal monononicity proofs of partial function
+  definitions.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Old-style recursive function definitions (TFL)%
 }
 \isamarkuptrue%