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